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 ⟶ c↓s)"

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 MGT⇩t :: "com ⇒ state assn × com × state assn" where
  [simp]: "MGT⇩t c = (λz s. z = s ∧ c↓s, c, λz t. z -c→ t)"

lemma MGT_implies_complete:
 "{} ⊢⇩t MGT⇩t c ⟹ {} ⊨⇩t {P}c{Q} ⟹ {} ⊢⇩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 ↓ 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 MGT⇩t CALL ⟹ C ⊢⇩t MGT⇩t 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 -com1→s & com2↓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 ↓ 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 = (c↓s ∧ (∀t. s -c→ t ⟶ cs⇓t))"

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

lemma execs_pres_termi: "⟦ ([c],s) →⇧* (c'#cs',s'); c↓s ⟧ ⟹ 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). body↓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); ∃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
 "∀i≤LEAST 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:
 "c↓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↓s) ∧ (s,t) ∈ termi_call_steps, CALL, λz s. z -body→ s)} ⊢⇩t
 {λz s. (z=s ∧ body↓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↓t & (∃cs. ([body], t) →⇧* (c2#cs,s)) & z -c1→s & c2↓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 ↓ 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↓s) ∧ (s,t) ∈ termi_call_steps, CALL, λz s. z -body→ s)} ⊢⇩t
 {λz s. (z=s ∧ body↓s) ∧ s = t} body {λz s. z -body→ s}"
apply(rule strengthen_pre[OF _ CALL_lemma])
apply blast
done

lemma MGT_CALL: "{} ⊢⇩t MGT⇩t CALL"
apply(simp add: MGT⇩t_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