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" ("t {(1_)}/ (_)/ {(1_)}" 50) where
    "t {P}c{Q}    {P}c{Q}  (z s. P z s  cs)"

definition
 ctvalid :: "'a cntxt  'a assn  com  'a assn  bool"
            ("(_ /t {(1_)}/ (_)/ {(1_))}" 50) where
 "C t {P}c{Q}  ((P',c',Q')  C. t {P'}c'{Q'})  t {P}c{Q}"


inductive
  thoare :: "'a cntxt  'a assn  com  'a assn  bool"
   ("(_ t/ ({(1_)}/ (_)/ {(1_)}))" [50,0,0,0] 50)
where
  Do: "C t {λz s. (t  f s . P z t)  f s  {}} Do f {P}"
| Semi: " C t {P}c1{Q}; C t {Q}c2{R}   C t {P} c1;c2 {R}"
| If: " C t {λz s. P z s  b s}c{Q}; C t {λz s. P z s  ~b s}d{Q}   
      C t {P} IF b THEN c ELSE d {Q}"
| While:
  "wf r;  s'. C t {λz s. P z s  b s  s' = s} c {λz s. P z s  (s,s')  r}
    C 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)}
                 t {λz s. P z s  s = s'} body {Q}
    {} t {P} CALL {Q}"

| Asm: "{(P,CALL,Q)} t {P} CALL {Q}"

| Conseq:
  " C 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 t {P}c{Q}"

| Local: " s'. C t {λz s. P z s'  s = f s'} c {λz t. Q z (g s' t)}  
        C t {P} LOCAL f;c;g {Q}"

abbreviation hoare1 :: "'a cntxt  'a assn × com × 'a assn  bool" ("_ t _") where
  "C t x  C 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 t {P}c{Q}    C t {P'}c{Q}"
by(rule thoare.Conseq, assumption, blast)

lemma weaken_post:
 " C t {P}c{Q}; z s. Q z s  Q' z s   C t {P}c{Q'}"
by(erule thoare.Conseq, blast)


lemmas tvalid_defs = tvalid_def ctvalid_def valid_defs

lemma [iff]:
"(t {λz s. n. P n z s}c{Q}) = (n. t {P n}c{Q})"
apply(unfold tvalid_defs)
apply fast
done

lemma [iff]:
"(t {λz s. P z s  P'}c{Q}) = (P'  t {P}c{Q})"
apply(unfold tvalid_defs)
apply fast
done

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

theorem "C t {P}c{Q}    C 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: if_split_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. 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 MGTt :: "com  state assn × com × state assn" where
  [simp]: "MGTt c = (λz s. z = s  cs, c, λz t. z -c t)"

lemma MGT_implies_complete:
 "{} t MGTt c  {} t {P}c{Q}  {} t {P}c{Q::state assn}"
apply(simp add: MGTt_def)
apply (erule thoare.Conseq)
apply(simp add: tvalid_defs)
apply blast
done

lemma while_termiE: " WHILE b DO c  s; b s   c  s"
by(erule termi.cases, auto)

lemma while_termiE2:
  " WHILE b DO c  s; b s; s -c t   WHILE b DO c  t"
by(erule termi.cases, auto)

lemma MGT_lemma: "C t MGTt CALL  C t MGTt c"
apply (simp)
apply(induct_tac c)
     apply (rule strengthen_pre[OF _ thoare.Do])
     apply blast
    apply(rename_tac com1 com2)
    apply(rule_tac Q = "λz s. z -com1s & com2s" 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  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 "" 60) where
  "[]s = True"
| "c#cs  s = (cs  (t. s -c t  cst))"

lemma exec1_pres_termis: "(cs,s)  (cs',s')  css  cs'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')  css  cs's'"
apply(erule rtrancl_induct2)
 apply blast
apply(blast dest:exec1_pres_termis)
done

lemma execs_pres_termi: " ([c],s) * (c'#cs',s'); cs   c'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). bodys  (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); i. fst(f i) = cs 
        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
 "iLEAST i. fst (f i) = cs. 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 "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  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:
 "cs  ¬(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  bodys)  (s,t)  termi_call_steps, CALL, λz s. z -body s)} t
 {λz s. (z=s  bodyt)  (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. bodyt & (cs. ([body], t) * (c2#cs,s)) & z -c1s & c2s" 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  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  bodys)  (s,t)  termi_call_steps, CALL, λz s. z -body s)} t
 {λz s. (z=s  bodys)  s = t} body {λz s. z -body s}"
apply(rule strengthen_pre[OF _ CALL_lemma])
apply blast
done

lemma MGT_CALL: "{} t MGTt CALL"
apply(simp add: MGTt_def)
apply(blast intro:thoare.Call wf_termi_call_steps CALL_cor)
done


theorem "{} t {P}c{Q}    {} t {P}c{Q::state assn}"
apply(erule MGT_implies_complete[OF MGT_lemma[OF MGT_CALL]])
done

end