# Theory PsHoareTotal

Up to index of Isabelle/HOL/Abstract-Hoare-Logics

theory PsHoareTotal
imports PsHoare PsTermi
`(*  Title:       Inductive definition of Hoare logic for total correctness    Author:      Tobias Nipkow, 2001/2006    Maintainer:  Tobias Nipkow*)theory PsHoareTotal imports PsHoare PsTermi beginsubsection{* Hoare logic for total correctness *}definition tvalid :: "'a assn => com => 'a assn => bool" ("\<Turnstile>⇩t {(1_)}/ (_)/ {(1_)}" 50) where    "\<Turnstile>⇩t {P}c{Q} <-> \<Turnstile> {P}c{Q} ∧ (∀z s. P z s --> c\<down>s)"definition valids :: "'a cntxt => bool" ("|\<Turnstile>⇩t _" 50) where "|\<Turnstile>⇩t D <-> (∀(P,c,Q) ∈ D. \<Turnstile>⇩t {P}c{Q})"definition ctvalid :: "'a cntxt => 'a assn => com => 'a assn => bool"            ("(_ /\<Turnstile>⇩t {(1_)}/ (_)/ {(1_))}" 50) where "C \<Turnstile>⇩t {P}c{Q} <-> |\<Turnstile>⇩t C -->  \<Turnstile>⇩t {P}c{Q}"definition cvalids :: "'a cntxt => 'a cntxt => bool" ("_ |\<Turnstile>⇩t/ _" 50) where  "C |\<Turnstile>⇩t D <-> |\<Turnstile>⇩t C --> |\<Turnstile>⇩t D"inductive  thoare :: "'a cntxt => 'a cntxt => bool" ("(_ |\<turnstile>⇩t/ _)" 50)  and thoare' :: "'a cntxt => 'a assn => com => 'a assn => bool"    ("(_ \<turnstile>⇩t/ ({(1_)}/ (_)/ {(1_)}))" [50,0,0,0] 50)where "C \<turnstile>⇩t {P}c{Q}  ≡  C |\<turnstile>⇩t {(P,c,Q)}"| Do: "C \<turnstile>⇩t {λz s. (∀t ∈ f s . P z t) ∧ f s ≠ {}} Do f {P}"| Semi: "[| C \<turnstile>⇩t {P}c1{Q}; C \<turnstile>⇩t {Q}c2{R} |] ==> C \<turnstile>⇩t {P} c1;c2 {R}"| If: "[| C \<turnstile>⇩t {λz s. P z s ∧ b s}c{Q}; C \<turnstile>⇩t {λz s. P z s ∧ ~b s}d{Q}  |] ==>      C \<turnstile>⇩t {P} IF b THEN c ELSE d {Q}"| While:(*>*)  "[|wf r;  ∀s'. C \<turnstile>⇩t {λz s. P z s ∧ b s ∧ s' = s} c {λz s. P z s ∧ (s,s') ∈ r}|]   ==> C \<turnstile>⇩t {P} WHILE b DO c {λz s. P z s ∧ ¬b s}"| Call:  "[| wf r;     ∀q pre.       (\<Union>p. {(λz s. P p z s ∧ ((p,s),(q,pre)) ∈ r,CALL p,Q p)})       \<turnstile>⇩t {λz s. P q z s ∧ s = pre} body q {Q q} |]   ==> {} |\<turnstile>⇩t \<Union>p. {(P p, CALL p, Q p)}"| Asm: "(P,CALL p,Q) ∈ C ==> C \<turnstile>⇩t {P} CALL p {Q}"| Conseq:  "[| C \<turnstile>⇩t {P'}c{Q'};     (∀s t. (∀z. P' z s --> Q' z t) --> (∀z. P z s --> Q z t)) ∧     (∀s. (∃z. P z s) --> (∃z. P' z s)) |]   ==> C \<turnstile>⇩t {P}c{Q}"| ConjI: "∀(P,c,Q) ∈ D. C \<turnstile>⇩t {P}c{Q}  ==>  C |\<turnstile>⇩t D"| ConjE: "[| C |\<turnstile>⇩t D; (P,c,Q) ∈ D |] ==> C \<turnstile>⇩t {P}c{Q}"| Local: "[| ∀s'. C \<turnstile>⇩t {λz s. P z s' ∧ s = f s'} c {λz t. Q z (g s' t)} |] ==>        C \<turnstile>⇩t {P} LOCAL f;c;g {Q}"monos split_betalemma strengthen_pre: "[| ∀z s. P' z s --> P z s; C \<turnstile>⇩t {P}c{Q}  |] ==> C \<turnstile>⇩t {P'}c{Q}"by(rule thoare.Conseq, assumption, blast)lemma weaken_post: "[| C \<turnstile>⇩t {P}c{Q}; ∀z s. Q z s --> Q' z s |] ==> C \<turnstile>⇩t {P}c{Q'}"by(erule thoare.Conseq, blast)theorems tvalid_defs = tvalid_def ctvalid_def valids_def cvalids_def valid_defslemma [iff]:"(\<Turnstile>⇩t {λz s. ∃n. P n z s}c{Q}) = (∀n. \<Turnstile>⇩t {P n}c{Q})"apply(unfold tvalid_defs)apply fastdonelemma [iff]:"(\<Turnstile>⇩t {λz s. P z s ∧ P'}c{Q}) = (P' --> \<Turnstile>⇩t {P}c{Q})"apply(unfold tvalid_defs)apply fastdonelemma [iff]: "(\<Turnstile>⇩t {P}CALL p{Q}) = (\<Turnstile>⇩t {P}body p{Q})"apply(unfold tvalid_defs)apply fastdonelemma unfold_while: "(s -WHILE b DO c-> u) =  (s -IF b THEN c;WHILE b DO c ELSE Do(λs. {s})-> u)"by(auto elim: exec.cases intro:exec.intros split:split_if_asm)theorem "C |\<turnstile>⇩t D  ==>  C |\<Turnstile>⇩t D"apply(erule thoare.induct)       apply(simp only:tvalid_defs)       apply fast      apply(simp add:tvalid_defs)      apply fast     apply(simp only:tvalid_defs)     apply clarsimp    prefer 3    apply(simp add:tvalid_defs)    apply fast   prefer 3   apply(simp add:tvalid_defs)   apply blast  apply(simp add:tvalid_defs)  apply(rule impI, rule conjI)   apply(rule allI)   apply(erule wf_induct)   apply clarify   apply(drule unfold_while[THEN iffD1])   apply (simp split add:split_if_asm)   apply fast  apply(rule allI, rule allI)  apply(erule wf_induct)  apply clarify  apply(case_tac "b x")   prefer 2   apply (erule termi.WhileFalse)  apply(rule termi.WhileTrue, assumption)   apply fast  apply (subgoal_tac "(t,x):r")   apply fast  apply blast deferapply(simp add:tvalid_defs)apply fastapply(simp (no_asm_use) add:tvalid_defs)apply fastapply(simp add:tvalid_defs)apply fastapply(simp (no_asm_use) add:valids_def ctvalid_def cvalids_def)apply(rule allI)apply(rename_tac q)apply(subgoal_tac "∀pre. \<Turnstile>⇩t {λz s. P (fst(q,pre)) z s & s=(snd(q,pre))} body (fst(q,pre)) {Q (fst(q,pre))}") apply(simp (no_asm_use) add:tvalid_defs) apply fastapply(rule allI)apply(erule_tac wf_induct)apply(simp add:split_paired_all)apply(rename_tac q pre)apply(erule allE, erule allE, erule conjE, erule impE) prefer 2 apply assumptionapply(rotate_tac 1, erule thin_rl)apply(unfold tvalid_defs)apply fastdonedefinition MGT⇣t :: "com => state assn × com × state assn" where  [simp]: "MGT⇣t c = (λz s. z = s ∧ c\<down>s, c, λz t. z -c-> t)"lemma MGT_implies_complete: "{} |\<turnstile>⇩t {MGT⇣t c} ==> {} \<Turnstile>⇩t {P}c{Q} ==> {} \<turnstile>⇩t {P}c{Q::state assn}"apply(unfold MGT⇣t_def)apply (erule thoare.Conseq)apply(simp add: tvalid_defs)apply blastdonelemma while_termiE: "[| WHILE b DO c \<down> s; b s |] ==> c \<down> s"by(erule termi.cases, auto)lemma while_termiE2: "[| WHILE b DO c \<down> s; b s; s -c-> t |] ==> WHILE b DO c \<down> t"by(erule termi.cases, auto)lemma MGT_lemma: "∀p. {} |\<turnstile>⇩t {MGT⇣t(CALL p)}  ==>  {} |\<turnstile>⇩t {MGT⇣t c}"apply (simp)apply(induct_tac c)     apply (rule strengthen_pre[OF _ thoare.Do])     apply blast    apply(rule_tac Q = "λz s. z -com1->s & com2\<down>s" in thoare.Semi)     apply(erule thoare.Conseq)     apply fast    apply(erule thoare.Conseq)    apply fast   apply(rule thoare.If)    apply(erule thoare.Conseq)    apply simp   apply(erule thoare.Conseq)   apply simp  defer  apply simp apply(fast intro:thoare.Local elim!: thoare.Conseq)apply(rename_tac b c)apply(rule_tac P' = "λz s. (z,s) ∈ ({(s,t). b s ∧ s -c-> t})^* ∧                           WHILE b DO c \<down> s" in thoare.Conseq) apply(rule_tac thoare.While[OF wf_termi]) apply(rule allI) apply(erule thoare.Conseq) apply(fastforce intro:rtrancl_into_rtrancl dest:while_termiE while_termiE2)apply(rule conjI) apply clarsimp apply(erule_tac x = s in allE) apply clarsimp apply(erule converse_rtrancl_induct)  apply(erule exec.WhileFalse) apply(fast elim:exec.WhileTrue)apply(fast intro: rtrancl_refl)doneinductive_set  exec1 :: "((com list × state) × (com list × state))set"  and exec1' :: "(com list × state) => (com list × state) => bool"  ("_ -> _" [81,81] 100)where  "cs0 -> cs1 ≡ (cs0,cs1) : exec1"| Do[iff]: "t ∈ f s ==> ((Do f)#cs,s) -> (cs,t)"| Semi[iff]: "((c1;c2)#cs,s) -> (c1#c2#cs,s)"| IfTrue:   "b s ==> ((IF b THEN c1 ELSE c2)#cs,s) -> (c1#cs,s)"| IfFalse: "¬b s ==> ((IF b THEN c1 ELSE c2)#cs,s) -> (c2#cs,s)"| WhileFalse: "¬b s ==> ((WHILE b DO c)#cs,s) -> (cs,s)"| WhileTrue:   "b s ==> ((WHILE b DO c)#cs,s) -> (c#(WHILE b DO c)#cs,s)"| Call[iff]: "(CALL p#cs,s) -> (body p#cs,s)"| Local[iff]: "((LOCAL f;c;g)#cs,s) -> (c # Do(λt. {g s t})#cs, f s)"abbreviation  exectr :: "(com list × state) => (com list × state) => bool"  ("_ ->⇧* _" [81,81] 100)  where "cs0 ->⇧* cs1 ≡ (cs0,cs1) : exec1^*"inductive_cases exec1E[elim!]: "([],s) -> (cs',s')" "(Do f#cs,s) -> (cs',s')" "((c1;c2)#cs,s) -> (cs',s')" "((IF b THEN c1 ELSE c2)#cs,s) -> (cs',s')" "((WHILE b DO c)#cs,s) -> (cs',s')" "(CALL p#cs,s) -> (cs',s')" "((LOCAL f;c;g)#cs,s) -> (cs',s')"lemma [iff]: "¬ ([],s) -> u"by (induct u) blastlemma app_exec: "(cs,s) -> (cs',s') ==> (cs@cs2,s) -> (cs'@cs2,s')"apply(erule exec1.induct)       apply(simp_all del:fun_upd_apply)   apply(blast intro:exec1.intros)+donelemma app_execs: "(cs,s) ->⇧* (cs',s') ==> (cs@cs2,s) ->⇧* (cs'@cs2,s')"apply(erule rtrancl_induct2) apply blastapply(blast intro:app_exec rtrancl_trans)donelemma exec_impl_execs[rule_format]: "s -c-> s' ==> ∀cs. (c#cs,s) ->⇧* (cs,s')"apply(erule exec.induct)         apply blast        apply(blast intro:rtrancl_trans)       apply(blast intro:exec1.IfTrue rtrancl_trans)      apply(blast intro:exec1.IfFalse rtrancl_trans)     apply(blast intro:exec1.WhileFalse rtrancl_trans)    apply(blast intro:exec1.WhileTrue rtrancl_trans)   apply(blast intro: rtrancl_trans)apply(blast intro: rtrancl_trans)doneinductive  execs :: "state => com list => state => bool"  ("_/ =_=>/ _" [50,0,50] 50)where  "s =[]=> s"| "s -c-> t ==> t =cs=> u ==> s =c#cs=> u"inductive_cases [elim!]: "s =[]=> t" "s =c#cs=> t"theorem exec1s_impl_execs: "(cs,s) ->⇧* ([],t) ==> s =cs=> t"apply(erule converse_rtrancl_induct2) apply(rule execs.intros)apply(erule exec1.cases)apply(blast intro:execs.intros)apply(blast intro:execs.intros)apply(fastforce intro:execs.intros)apply(fastforce intro:execs.intros)apply(blast intro:execs.intros exec.intros)+donetheorem exec1s_impl_exec: "([c],s) ->⇧* ([],t) ==> s -c-> t"by(blast dest: exec1s_impl_execs)primrec termis :: "com list => state => bool" (infixl "\<Down>" 60) where  "[]\<Down>s = True"| "c#cs \<Down> s = (c\<down>s ∧ (∀t. s -c-> t --> cs\<Down>t))"lemma exec1_pres_termis: "(cs,s) -> (cs',s') ==> cs\<Down>s --> cs'\<Down>s'"apply(erule exec1.induct)       apply(simp_all del:fun_upd_apply)   apply blast  apply(blast intro:exec.WhileFalse) apply(blast intro:while_termiE while_termiE2 exec.WhileTrue)apply blastdonelemma execs_pres_termis: "(cs,s) ->⇧* (cs',s') ==> cs\<Down>s --> cs'\<Down>s'"apply(erule rtrancl_induct2) apply blastapply(blast dest:exec1_pres_termis)donelemma execs_pres_termi: "[| ([c],s) ->⇧* (c'#cs',s'); c\<down>s |] ==> c'\<down>s'"apply(insert execs_pres_termis[of "[c]" _ "c'#cs'",simplified])apply blastdonedefinition  termi_call_steps :: "((pname × state) × (pname × state))set" where  "termi_call_steps =    {((q,t),(p,s)). body p\<down>s ∧ (∃cs. ([body p], s) ->⇧* (CALL q# cs, t))}"lemma lem:  "!y. (a,y):r⇧+ --> P a --> P y ==> ((b,a) : {(y,x). P x ∧ (x,y):r}⇧+) = ((b,a) : {(y,x). P x ∧ (x,y):r⇧+})"apply(rule iffI) apply clarify apply(erule trancl_induct)  apply blast apply(blast intro:trancl_trans)apply clarifyapply(erule trancl_induct) apply blastapply(blast intro:trancl_trans)donelemma renumber_aux: "[|∀i. (a,f i) : r^* ∧ (f i,f(Suc i)) : r; (a,b) : r^* |] ==> b = f 0 --> (∃f. f 0 = a & (∀i. (f i, f(Suc i)) : r))"apply(erule converse_rtrancl_induct) apply blastapply(clarsimp)apply(rule_tac x="λi. case i of 0 => y | Suc i => fa i" in exI)apply simpapply clarifyapply(case_tac i) apply simp_alldonelemma renumber: "∀i. (a,f i) : r^* ∧ (f i,f(Suc i)) : r ==> ∃f. f 0 = a & (∀i. (f i, f(Suc i)) : r)"by(blast dest:renumber_aux)definition inf :: "com list => state => bool" where  "inf cs s <-> (∃f. f 0 = (cs,s) ∧ (∀i. f i -> f(Suc i)))"lemma [iff]: "¬ inf [] s"apply(unfold inf_def)apply clarifyapply(erule_tac x = 0 in allE)apply simpdonelemma [iff]: "¬ inf [Do f] s"apply(unfold inf_def)apply clarifyapply(frule_tac x = 0 in spec)apply(erule_tac x = 1 in allE)apply (case_tac "fa (Suc 0)")apply clarsimpdonelemma [iff]: "inf ((c1;c2)#cs) s = inf (c1#c2#cs) s"apply(unfold inf_def)apply(rule iffI)apply clarifyapply(rule_tac x = "λi. f(Suc i)" in exI)apply(frule_tac x = 0 in spec)apply (case_tac "f (Suc 0)")apply clarsimpapply clarifyapply(rule_tac x = "λi. case i of 0 => ((c1;c2)#cs,s) | Suc i => f i" in exI)apply(simp split:nat.split)donelemma [iff]: "inf ((IF b THEN c1 ELSE c2)#cs) s =              inf ((if b s then c1 else c2)#cs) s"apply(unfold inf_def)apply(rule iffI) apply clarsimp apply(frule_tac x = 0 in spec) apply (case_tac "f (Suc 0)") apply(rule conjI)  apply clarsimp  apply(rule_tac x = "λi. f(Suc i)" in exI)  apply clarsimp apply clarsimp apply(rule_tac x = "λi. f(Suc i)" in exI) apply clarsimpapply clarsimpapply(rule_tac x = "λi. case i of 0 => ((IF b THEN c1 ELSE c2)#cs,s) | Suc i => f i" in exI)apply(simp add: exec1.intros split:nat.split)donelemma [simp]: "inf ((WHILE b DO c)#cs) s =  (if b s then inf (c#(WHILE b DO c)#cs) s else inf cs s)"apply(unfold inf_def)apply(rule iffI) apply clarsimp apply(frule_tac x = 0 in spec) apply (case_tac "f (Suc 0)") apply(rule conjI)  apply clarsimp  apply(rule_tac x = "λi. f(Suc i)" in exI)  apply clarsimp apply clarsimp apply(rule_tac x = "λi. f(Suc i)" in exI) apply clarsimpapply (clarsimp split:if_splits) apply(rule_tac x = "λi. case i of 0 => ((WHILE b DO c)#cs,s) | Suc i => f i" in exI) apply(simp add: exec1.intros split:nat.split)apply(rule_tac x = "λi. case i of 0 => ((WHILE b DO c)#cs,s) | Suc i => f i" in exI)apply(simp add: exec1.intros split:nat.split)donelemma [iff]: "inf (CALL p#cs) s =  inf (body p#cs) s"apply(unfold inf_def)apply(rule iffI) apply clarsimp apply(frule_tac x = 0 in spec) apply (case_tac "f (Suc 0)") apply clarsimp apply(rule_tac x = "λi. f(Suc i)" in exI) apply clarsimpapply clarsimpapply(rule_tac x = "λi. case i of 0 => (CALL p#cs,s) | Suc i => f i" in exI)apply(simp add: exec1.intros split:nat.split)donelemma [iff]: "inf ((LOCAL f;c;g)#cs) s =              inf (c#Do(λt. {g s t})#cs) (f s)"apply(unfold inf_def)apply(rule iffI) apply clarsimp apply(rename_tac F) apply(frule_tac x = 0 in spec) apply (case_tac "F (Suc 0)") apply clarsimp apply(rule_tac x = "λi. F(Suc i)" in exI) apply clarsimpapply (clarsimp)apply(rename_tac F)apply(rule_tac x = "λi. case i of 0 => ((LOCAL f;c;g)#cs,s) | Suc i => F i" in exI)apply(simp add: exec1.intros split:nat.split)donelemma exec1_only1_aux: "(ccs,s) -> (cs',t) ==>                    ∀c cs. ccs = c#cs --> (∃cs1. cs' = cs1 @ cs)"apply(erule exec1.induct)apply force+donelemma exec1_only1: "(c#cs,s) -> (cs',t) ==> ∃cs1. cs' = cs1 @ cs"by(blast dest:exec1_only1_aux)lemma exec1_drop_suffix_aux:"(cs12,s) -> (cs1'2,s') ==> !cs1 cs2 cs1'. cs12 = cs1@cs2 & cs1'2 = cs1'@cs2 & cs1 ≠ [] --> (cs1,s) -> (cs1',s')"apply(erule exec1.induct)       apply (force intro:exec1.intros simp add: neq_Nil_conv)+donelemma exec1_drop_suffix: "(cs1@cs2,s) -> (cs1'@cs2,s') ==> cs1 ≠ [] ==> (cs1,s) -> (cs1',s')"by(blast dest:exec1_drop_suffix_aux)lemma execs_drop_suffix[rule_format(no_asm)]:  "[| f 0 = (c#cs,s);!i. f(i) -> f(Suc i) |] ==>   (!i<k. p i ≠ [] & fst(f i) = p i@cs) --> fst(f k) = p k@cs   --> ([c],s) ->⇧* (p k,snd(f k))"apply(induct_tac k) apply simpapply (clarsimp)apply(erule rtrancl_into_rtrancl)apply(erule_tac x = n in allE)apply(erule_tac x = n in allE)apply(case_tac "f n")apply(case_tac "f(Suc n)")apply simpapply(blast dest:exec1_drop_suffix)donelemma execs_drop_suffix0:  "[| f 0 = (c#cs,s);!i. f(i) -> f(Suc i); !i<k. p i ≠ [] & fst(f i) = p i@cs;     fst(f k) = cs; p k = [] |] ==> ([c],s) ->⇧* ([],snd(f k))"apply(drule execs_drop_suffix,assumption,assumption) apply simpapply simpdonelemma skolemize1: "∀x. P x --> (∃y. Q x y) ==> ∃f.∀x. P x --> Q x (f x)"apply(rule_tac x = "λx. SOME y. Q x y" in exI)apply(fast intro:someI2)donelemma least_aux: "[|f 0 = (c # cs, s); ∀i. f i -> f (Suc i);        fst(f k) = cs; !i<k. fst(f i) ≠ cs|]       ==> ∀i ≤ k. (∃p. (p ≠ []) = (i < k) & fst(f i) = p @ cs)"apply(rule allI)apply(induct_tac i) apply simp apply (rule ccontr) apply simpapply clarsimpapply(drule order_le_imp_less_or_eq)apply(erule disjE) prefer 2 apply simpapply simpapply(erule_tac x = n in allE)apply(erule_tac x = "Suc n" in allE)apply(case_tac "f n")apply(case_tac "f(Suc n)")apply simpapply(rename_tac sn csn1 sn1)apply (clarsimp simp add: neq_Nil_conv)apply(drule exec1_only1)apply (clarsimp simp add: neq_Nil_conv)apply(erule disjE) apply clarsimpapply clarsimpapply(case_tac cs1) apply simpapply simpdonelemma least_lem: "[|f 0 = (c#cs,s); !i. f i -> f(Suc i); EX i. fst(f i) = cs |]       ==> EX k. fst(f k) = cs & ([c],s) ->⇧* ([],snd(f k))"apply(rule_tac x="LEAST i. fst(f i) = cs" in exI)apply(rule conjI) apply(fast intro: LeastI)apply(subgoal_tac "!i<=LEAST i. fst (f i) = cs. EX p. ((p ≠ []) = (i<(LEAST i. fst (f i) = cs))) & fst(f i) = p@cs") apply(drule skolemize1) apply clarify apply(rename_tac p) apply(erule_tac p=p in execs_drop_suffix0, assumption)   apply (blast dest:order_less_imp_le)  apply(fast intro: LeastI) apply(erule thin_rl) apply(erule_tac x = "LEAST j. fst (f j) = fst (f i)" in allE) apply blastapply(erule least_aux,assumption) apply(fast intro: LeastI)apply clarifyapply(drule not_less_Least)apply blastdonelemma skolemize2: "∀x.∃y. P x y ==> ∃f.∀x. P x (f x)"apply(rule_tac x = "λx. SOME y. P x y" in exI)apply(fast intro:someI2)donelemma inf_cases: "inf (c#cs) s ==> inf [c] s ∨ (∃t. s -c-> t ∧ inf cs t)"apply(unfold inf_def)apply (clarsimp del: disjCI)apply(case_tac "EX i. fst(f i) = cs") apply(rule disjI2) apply(drule least_lem, assumption, assumption) apply clarify apply(drule exec1s_impl_exec) apply(case_tac "f k") apply simp apply (rule exI, rule conjI, assumption) apply(rule_tac x="λi. f(i+k)" in exI) apply (clarsimp)apply(rule disjI1)apply simpapply(subgoal_tac "∀i. ∃p. p ≠ [] ∧ fst(f i) = p@cs") apply(drule skolemize2) apply clarify apply(rename_tac p) apply(rule_tac x = "λi. (p i, snd(f i))" in exI) apply(rule conjI)  apply(erule_tac x = 0 in allE, erule conjE)  apply simp apply clarify apply(erule_tac x = i in allE) apply(erule_tac x = i in allE) apply(frule_tac x = i in spec) apply(erule_tac x = "Suc i" in allE) apply(case_tac "f i") apply(case_tac "f(Suc i)") apply clarsimp apply(blast intro:exec1_drop_suffix)apply(clarify)apply(induct_tac i) apply forceapply clarsimpapply(case_tac p) apply blastapply(erule_tac x=n in allE)apply(erule_tac x="Suc n" in allE)apply(case_tac "f n")apply(case_tac "f(Suc n)")apply clarsimpapply(drule exec1_only1)apply clarsimpdonelemma termi_impl_not_inf: "c \<down> s ==> ¬ inf [c] s"apply(erule termi.induct)        (*Do*)        apply clarify       (*Semi*)       apply(blast dest:inf_cases)      (* Cond *)      apply clarsimp     apply clarsimp    (*While*)    apply clarsimp   apply(fastforce dest:inf_cases)  (*Call*)  apply blast (*Local*) apply(blast dest:inf_cases)donelemma termi_impl_no_inf_chain: "c\<down>s ==> ¬(∃f. f 0 = ([c],s) ∧ (∀i::nat. (f i, f(i+1)) : exec1^+))"apply(subgoal_tac "wf({(y,x). ([c],s) ->⇧* x & x -> y}^+)") apply(simp only:wf_iff_no_infinite_down_chain) apply(erule contrapos_nn) apply clarify apply(subgoal_tac "!i. ([c], s) ->⇧* f i")  prefer 2  apply(rule allI)  apply(induct_tac i)   apply simp  apply simp  apply(blast intro: trancl_into_rtrancl rtrancl_trans) apply(rule_tac x=f in exI) apply clarify apply(drule_tac x=i in spec) apply(subst lem)  apply(blast intro: trancl_into_rtrancl rtrancl_trans) apply clarsimpapply(rule wf_trancl)apply(simp only:wf_iff_no_infinite_down_chain)apply(clarify)apply simpapply(drule renumber)apply(fold inf_def)apply(simp add: termi_impl_not_inf)doneprimrec cseq :: "(nat => pname × state) => nat => com list" where  "cseq S 0 = []"|  "cseq S (Suc i) = (SOME cs. ([body(fst(S i))], snd(S i)) ->⇧*                              (CALL(fst(S(i+1)))# cs, snd(S(i+1)))) @ cseq S i"lemma wf_termi_call_steps: "wf termi_call_steps"apply(unfold termi_call_steps_def)apply(simp only:wf_iff_no_infinite_down_chain)apply(clarify)apply(rename_tac S)apply simpapply(subgoal_tac "∃Cs. Cs 0 = [] & (∀i. (body(fst(S i)) # Cs i,snd(S i)) ->⇧*                        (CALL(fst(S(i+1)))# Cs(i+1), snd(S(i+1))))")prefer 2 apply(rule_tac x = "cseq S" in exI) apply clarsimp apply(erule_tac x=i in allE) apply clarsimp apply(rename_tac q t p s cs) apply(erule_tac P = "λcs.([body p],s) ->⇧* (CALL q# cs, t)" in someI2) apply(fastforce dest:app_execs)apply clarifyapply(subgoal_tac "∀i. ((body(fst(S i))# Cs i,snd(S i)), (body(fst(S(i+1)))# Cs(i+1), snd(S(i+1)))) : exec1^+") prefer 2 apply(blast intro:rtrancl_into_trancl1)apply(subgoal_tac "∃f. f 0 = ([body(fst(S 0))],snd(S 0)) ∧ (∀i. (f i, f(i+1)) : exec1^+)") prefer 2 apply(rule_tac x = "λi.(body(fst(S i))#Cs i,snd(S i))" in exI) apply blastapply(erule_tac x=0 in allE)apply(simp add:split_def)apply clarifyapply(drule termi_impl_no_inf_chain)apply simpapply blastdonelemma CALL_lemma:"(\<Union>p. {(λz s. (z=s ∧ body p\<down>s) ∧ ((p,s),(q,pre)) ∈ termi_call_steps, CALL p,        λz s. z -body p-> s)}) \<turnstile>⇩t {λz s. (z=s ∧ body q\<down>pre) ∧ (∃cs. ([body q],pre) ->⇧* (c#cs,s))} c {λz s. z -c-> s}"apply(induct_tac c)(*Do*)     apply (rule strengthen_pre[OF _ thoare.Do])     apply(blast dest: execs_pres_termi)(*Semi*)    apply(rename_tac c1 c2)    apply(rule_tac Q = "λz s. body q\<down>pre & (EX cs. ([body q], pre) ->⇧* (c2#cs,s)) & z -c1->s & c2\<down>s" in thoare.Semi)     apply(erule thoare.Conseq)     apply(rule conjI)      apply clarsimp      apply(subgoal_tac "s -c1-> t")       prefer 2       apply(blast intro: exec1.Semi exec_impl_execs rtrancl_trans)      apply(subgoal_tac "([body q], pre) ->⇧* (c2 # cs, t)")       prefer 2       apply(blast intro:exec1.Semi[THEN r_into_rtrancl] exec_impl_execs rtrancl_trans)      apply(subgoal_tac "([body q], pre) ->⇧* (c2 # cs, t)")       prefer 2       apply(blast intro: exec_impl_execs rtrancl_trans)      apply(blast intro:exec_impl_execs rtrancl_trans execs_pres_termi)     apply(fast intro: exec1.Semi rtrancl_trans)    apply(erule thoare.Conseq)    apply blast(*Call*)   prefer 3   apply(simp only:termi_call_steps_def)   apply(rule thoare.Conseq[OF thoare.Asm])    apply blast   apply(blast dest: execs_pres_termi)(*If*)  apply(rule thoare.If)   apply(erule thoare.Conseq)   apply simp   apply(blast intro: exec1.IfTrue rtrancl_trans)  apply(erule thoare.Conseq)  apply simp  apply(blast intro: exec1.IfFalse rtrancl_trans)(*Local*) defer apply simp apply(rule thoare.Local) apply(rule allI) apply(erule thoare.Conseq) apply (clarsimp) apply(rule conjI)  apply (clarsimp)  apply(drule rtrancl_trans[OF _ r_into_rtrancl[OF exec1.Local]])  apply(fast) apply (clarsimp) apply(drule rtrancl_trans[OF _ r_into_rtrancl[OF exec1.Local]]) apply blast(*While*)apply(rename_tac b c)apply(rule_tac P' = "λz s. (z,s) ∈ ({(s,t). b s ∧ s -c-> t})^* ∧ body q\<down>pre ∧           (∃cs. ([body q], pre) ->⇧* ((WHILE b DO c) # cs, s))" in thoare.Conseq) apply(rule_tac thoare.While[OF wf_termi]) apply(rule allI) apply(erule thoare.Conseq) apply clarsimp apply(rule conjI)  apply clarsimp  apply(rule conjI)   apply(blast intro: rtrancl_trans exec1.WhileTrue)  apply(rule conjI)   apply(rule exI, rule rtrancl_trans, assumption)   apply(blast intro: exec1.WhileTrue exec_impl_execs rtrancl_trans)  apply(rule conjI)   apply(blast intro:execs_pres_termi)  apply(blast intro: exec1.WhileTrue exec_impl_execs rtrancl_trans) apply(blast intro: exec1.WhileTrue exec_impl_execs rtrancl_trans)apply(rule conjI) apply clarsimp apply(erule_tac x = s in allE) apply clarsimp apply(erule impE)  apply blast apply clarify apply(erule_tac a=s in converse_rtrancl_induct)  apply(erule exec.WhileFalse) apply(fast elim:exec.WhileTrue)apply(fast intro: rtrancl_refl)donelemma CALL_cor:"(\<Union>p. {(λz s. (z=s ∧ body p\<down>s) ∧ ((p,s),(q,pre)) ∈ termi_call_steps, CALL p,        λz s. z -body p-> s)}) \<turnstile>⇩t {λz s. (z=s ∧ body q\<down>s) ∧ s = pre} body q {λz s. z -body q-> s}"apply(rule strengthen_pre[OF _ CALL_lemma])apply blastdonelemma MGT_CALL: "{} |\<turnstile>⇩t (\<Union>p. {MGT⇣t(CALL p)})"apply(simp add: MGT⇣t_def)apply(rule thoare.Call)apply(rule wf_termi_call_steps)apply clarifyapply(rule CALL_cor)donelemma MGT_CALL1: "∀p. {} |\<turnstile>⇩t {MGT⇣t(CALL p)}"by(fastforce intro:MGT_CALL[THEN ConjE])theorem "{} \<Turnstile>⇩t {P}c{Q}  ==>  {} \<turnstile>⇩t {P}c{Q::state assn}"apply(erule MGT_implies_complete[OF MGT_lemma[OF MGT_CALL1]])doneend`