Theory PHoareTotal

(*  Title:       Inductive definition of Hoare logic for total correctness
    Author:      Tobias Nipkow, 2001/2006
    Maintainer:  Tobias Nipkow
*)

theory PHoareTotal imports PHoare PTermi begin

subsection{* Hoare logic for total correctness *}

text{*Validity is defined as expected:*} 

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
 ctvalid :: "'a cntxt => 'a assn => com => 'a assn => bool"
            ("(_ /\<Turnstile>⇩t {(1_)}/ (_)/ {(1_))}" 50) where
 "C \<Turnstile>⇩t {P}c{Q} <-> (∀(P',c',Q') ∈ C. \<Turnstile>⇩t {P'}c'{Q'}) --> \<Turnstile>⇩t {P}c{Q}"


inductive
  thoare :: "'a cntxt => 'a assn => com => 'a assn => bool"
   ("(_ \<turnstile>⇩t/ ({(1_)}/ (_)/ {(1_)}))" [50,0,0,0] 50)
where
  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;  ∀s'. {(λz s. P z s ∧ (s,s') ∈ r, CALL, Q)}
                 \<turnstile>⇩t {λz s. P z s ∧ s = s'} body {Q}|]
   ==> {} \<turnstile>⇩t {P} CALL {Q}"

| Asm: "{(P,CALL,Q)} \<turnstile>⇩t {P} CALL {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}"

| 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}"

abbreviation hoare1 :: "'a cntxt => 'a assn × com × 'a assn => bool" ("_ \<turnstile>⇩t _") where
  "C \<turnstile>⇩t x ≡ C \<turnstile>⇩t {fst x}fst (snd x){snd (snd x)}"


text{* The side condition in our rule of consequence looks quite different
from the one by Kleymann, but the two are in fact equivalent:*}

lemma "((∀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)))
        = (∀z s. P z s --> (∀t.∃z'. P' z' s ∧ (Q' z' t --> Q z t)))"
by blast

text{* The key difference to the work by Kleymann (and America and de
Boer) is that soundness and completeness are shown for arbitrary,
i.e.\ unbounded nondeterminism.  This is a significant extension and
appears to have been an open problem. The details are found below and
are explained in a separate paper~\cite{Nipkow-CSL02}. *}

lemma 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 valid_defs

lemma [iff]:
"(\<Turnstile>⇩t {λz s. ∃n. P n z s}c{Q}) = (∀n. \<Turnstile>⇩t {P n}c{Q})"
apply(unfold tvalid_defs)
apply fast
done

lemma [iff]:
"(\<Turnstile>⇩t {λz s. P z s ∧ P'}c{Q}) = (P' --> \<Turnstile>⇩t {P}c{Q})"
apply(unfold tvalid_defs)
apply fast
done

lemma [iff]: "(\<Turnstile>⇩t {P}CALL{Q}) = (\<Turnstile>⇩t {P}body{Q})"
apply(unfold tvalid_defs)
apply fast
done

theorem "C \<turnstile>⇩t {P}c{Q}  ==>  C \<Turnstile>⇩t {P}c{Q}"
apply(erule thoare.induct)
       apply(simp only:tvalid_defs)
       apply fast
      apply(simp only:tvalid_defs)
      apply fast
     apply(simp only:tvalid_defs)
     apply clarsimp
    prefer 3
    apply(simp add:tvalid_defs)
   prefer 3
   apply(simp only:tvalid_defs)
   apply blast
  apply(simp only: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
 apply(simp (no_asm_use) add:ctvalid_def)
 apply(subgoal_tac "!n. \<Turnstile>⇩t {λz s. P z s & s=n} body {Q}")
  apply(simp (no_asm_use) add:tvalid_defs)
  apply blast
 apply(rule allI)
 apply(erule wf_induct)
 apply(unfold tvalid_defs)
 apply fast
apply fast
done


definition 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(simp add: MGT⇣t_def)
apply (erule thoare.Conseq)
apply(simp add: tvalid_defs)
apply blast
done

lemma 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: "C \<turnstile>⇩t MGT⇣t CALL ==> C \<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 simp
 apply(fast elim:exec.WhileTrue)
apply(fast intro: rtrancl_refl)
done


inductive_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#cs,s) -> (body#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#cs,s) -> (cs',s')"
 "((LOCAL f;c;g)#cs,s) -> (cs',s')"

lemma [iff]: "¬ ([],s) -> u"
by (induct u) blast

lemma 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)+
done

lemma app_execs: "(cs,s) ->⇧* (cs',s') ==> (cs@cs2,s) ->⇧* (cs'@cs2,s')"
apply(erule rtrancl_induct2)
 apply blast
apply(blast intro:app_exec rtrancl_trans)
done

lemma 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)
done

inductive
  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)
apply(blast intro:execs.intros exec.intros)
apply(blast intro:execs.intros exec.intros)
apply(blast intro:execs.intros exec.intros)
done


theorem 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)
  apply blast
 apply(blast intro:while_termiE while_termiE2 exec.WhileTrue)
apply blast
done

lemma execs_pres_termis: "(cs,s) ->⇧* (cs',s') ==> cs\<Down>s --> cs'\<Down>s'"
apply(erule rtrancl_induct2)
 apply blast
apply(blast dest:exec1_pres_termis)
done

lemma 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 blast
done

definition
 termi_call_steps :: "(state × state)set" where
"termi_call_steps = {(t,s). body\<down>s ∧ (∃cs. ([body], s) ->⇧* (CALL # 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 clarify
apply(erule trancl_induct)
 apply blast
apply(blast intro:trancl_trans)
done


lemma 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 blast
apply(clarsimp)
apply(rule_tac x="λi. case i of 0 => y | Suc i => fa i" in exI)
apply simp
apply clarify
apply(case_tac i)
 apply simp_all
done

lemma 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 clarify
apply(erule_tac x = 0 in allE)
apply simp
done

lemma [iff]: "¬ inf [Do f] s"
apply(unfold inf_def)
apply clarify
apply(frule_tac x = 0 in spec)
apply(erule_tac x = 1 in allE)
apply(case_tac "fa (Suc 0)")
apply clarsimp
done

lemma [iff]: "inf ((c1;c2)#cs) s = inf (c1#c2#cs) s"
apply(unfold inf_def)
apply(rule iffI)
apply clarify
apply(rule_tac x = "λi. f(Suc i)" in exI)
apply(frule_tac x = 0 in spec)
apply(case_tac "f (Suc 0)")
apply clarsimp
apply clarify
apply(rule_tac x = "λi. case i of 0 => ((c1;c2)#cs,s) | Suc i => f i" in exI)
apply(simp split:nat.split)
done

lemma [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 clarsimp
apply clarsimp
apply(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)
done

lemma [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 clarsimp
apply (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)
done

lemma [iff]: "inf (CALL#cs) s =  inf (body#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 clarsimp
apply clarsimp
apply(rule_tac x = "λi. case i of 0 => (CALL#cs,s) | Suc i => f i" in exI)
apply(simp add: exec1.intros split:nat.split)
done

lemma [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 clarsimp
apply (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)
done

lemma exec1_only1_aux: "(ccs,s) -> (cs',t) ==>
                    ∀c cs. ccs = c#cs --> (∃cs1. cs' = cs1 @ cs)"
apply(erule exec1.induct)
apply blast
apply force+
done

lemma 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)+
done

lemma 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 simp
apply (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 simp
apply(blast dest:exec1_drop_suffix)
done

lemma 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 simp
apply simp
done

lemma 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)
done

lemma 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 simp
apply clarsimp
apply(drule order_le_imp_less_or_eq)
apply(erule disjE)
 prefer 2
 apply simp
apply simp
apply(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 simp
apply(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 clarsimp
apply clarsimp
apply(case_tac cs1)
 apply simp
apply simp
done

lemma 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 blast
apply(erule least_aux,assumption)
 apply(fast intro: LeastI)
apply clarify
apply(drule not_less_Least)
apply blast
done

lemma 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)
done

lemma 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 simp
apply(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 force
apply clarsimp
apply(case_tac p)
 apply blast
apply(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 clarsimp
apply(drule exec1_only1)
apply clarsimp
done

lemma 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)
done

lemma 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 clarsimp
apply(rule wf_trancl)
apply(simp only:wf_iff_no_infinite_down_chain)
apply(clarify)
apply simp
apply(drule renumber)
apply(fold inf_def)
apply(simp add: termi_impl_not_inf)
done

primrec cseq :: "(nat => state) => nat => com list" where
  "cseq S 0 = []"
| "cseq S (Suc i) = (SOME cs. ([body], S i) ->⇧* (CALL # cs, 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 simp
apply(subgoal_tac "∃Cs. Cs 0 = [] & (∀i. (body # Cs i,S i) ->⇧* (CALL # Cs(i+1), S(i+1)))")
prefer 2
 apply(rule_tac x = "cseq S" in exI)
 apply clarsimp
 apply(erule_tac x=i in allE)
 apply(clarify)
 apply(erule_tac P = "λcs.([body],S i) ->⇧* (CALL # cs, S(Suc i))" in someI2)
 apply(fastforce dest:app_execs)
apply clarify
apply(subgoal_tac "∀i. ((body # Cs i,S i), (body # Cs(i+1), S(i+1))) : exec1^+")
 prefer 2
 apply(blast intro:rtrancl_into_trancl1)
apply(subgoal_tac "∃f. f 0 = ([body],S 0) ∧ (∀i. (f i, f(i+1)) : exec1^+)")
 prefer 2
 apply(rule_tac x = "λi.(body#Cs i,S i)" in exI)
 apply blast
apply(blast dest:termi_impl_no_inf_chain)
done

lemma CALL_lemma:
"{(λz s. (z=s ∧ body\<down>s) ∧ (s,t) ∈ termi_call_steps, CALL, λz s. z -body-> s)} \<turnstile>⇩t
 {λz s. (z=s ∧ body\<down>t) ∧ (∃cs. ([body],t) ->⇧* (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\<down>t & (EX cs. ([body], t) ->⇧* (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-> ta")
       prefer 2
       apply(blast intro: exec1.Semi exec_impl_execs rtrancl_trans)
      apply(subgoal_tac "([body], t) ->⇧* (c2 # cs, ta)")
       prefer 2
       apply(blast intro:exec1.Semi[THEN r_into_rtrancl] exec_impl_execs rtrancl_trans)
      apply(subgoal_tac "([body], t) ->⇧* (c2 # cs, ta)")
       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 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)
(*Var*)
 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
apply(rename_tac b c)
apply(rule_tac P' = "λz s. (z,s) ∈ ({(s,t). b s ∧ s -c-> t})^* ∧ body \<down> t ∧
           (∃cs. ([body], t) ->⇧* ((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 simp
 apply(fast elim:exec.WhileTrue)
apply(fast intro: rtrancl_refl)
done

lemma CALL_cor:
"{(λz s. (z=s ∧ body\<down>s) ∧ (s,t) ∈ termi_call_steps, CALL, λz s. z -body-> s)} \<turnstile>⇩t
 {λz s. (z=s ∧ body\<down>s) ∧ s = t} body {λz s. z -body-> s}"
apply(rule strengthen_pre[OF _ CALL_lemma])
apply blast
done

lemma MGT_CALL: "{} \<turnstile>⇩t MGT⇣t CALL"
apply(simp add: MGT⇣t_def)
apply(blast intro:thoare.Call wf_termi_call_steps CALL_cor)
done


theorem "{} \<Turnstile>⇩t {P}c{Q}  ==>  {} \<turnstile>⇩t {P}c{Q::state assn}"
apply(erule MGT_implies_complete[OF MGT_lemma[OF MGT_CALL]])
done

end