# Theory Lang

(*  Title:       A while language
Author:      Tobias Nipkow, 2001/2006
Maintainer:  Tobias Nipkow
*)

section "Hoare Logics for While"

theory Lang imports Main begin

subsection‹The language \label{sec:lang}›

text‹We start by declaring a type of states:›

typedecl state

text‹\noindent
Our approach is completely parametric in the state space.
We define expressions (‹bexp›) as functions from states
to the booleans:›

type_synonym bexp = "state ⇒ bool"

text‹
Instead of modelling the syntax of boolean expressions, we
model their semantics. The (abstract and concrete)
syntax of our programming is defined as a recursive datatype:
›

datatype com = Do "(state ⇒ state set)"
| Semi  com com            ("_; _"  [60, 60] 10)
| Cond  bexp com com     ("IF _ THEN _ ELSE _"  60)
| While bexp com           ("WHILE _ DO _"  60)
| Local "(state ⇒ state)" com "(state ⇒ state ⇒ state)"
("LOCAL _; _; _" [0,0,60] 60)

text‹\noindent Statements in this language are called
\emph{commands}.  They are modelled as terms of type @{typ
com}. @{term"Do f"} represents an atomic nondeterministic command that
changes the state from @{term s} to some element of @{term"f s"}.
Thus the command that does nothing, often called \texttt{skip}, can be
represented by @{term"Do(λs. {s})"}. Again we have chosen to model the
semantics rather than the syntax, which simplifies matters
enormously. Of course it means that we can no longer talk about
certain syntactic matters, but that is just fine.

The constructors @{term Semi}, @{term Cond} and @{term While}
represent sequential composition, conditional and while-loop.
The annotations allow us to write
\begin{center}
@{term"c⇩1;c⇩2"} \qquad @{term"IF b THEN c⇩1 ELSE c⇩2"}
\end{center}
instead of @{term[source]"Semi c⇩1 c⇩2"}, @{term[source]"Cond b c⇩1 c⇩2"}
and @{term[source]"While b c"}.

The command @{term"LOCAL f;c;g"} applies function ‹f› to the state,
executes @{term c}, and then combines initial and final state via function
‹g›. More below.
The semantics of commands is defined inductively by a so-called
big-step semantics.›

inductive
exec :: "state ⇒ com ⇒ state ⇒ bool" ("_/ -_→/ _" [50,0,50] 50)
where
(*<*)Do:(*>*)"t ∈ f s ⟹ s -Do f→ t"

| (*<*)Semi:(*>*)"⟦ s0 -c1→ s1; s1 -c2→ s2 ⟧ ⟹ s0 -c1;c2→ s2"

| (*<*)IfT:(*>*)"⟦  b s; s -c1→ t ⟧ ⟹ s -IF b THEN c1 ELSE c2→ t"
| (*<*)IfF:(*>*)"⟦ ¬b s; s -c2→ t ⟧ ⟹ s -IF b THEN c1 ELSE c2→ t"

| (*<*)WhileF:(*>*)"¬b s ⟹ s -WHILE b DO c→ s"
| (*<*)WhileT:(*>*)"⟦ b s; s -c→ t; t -WHILE b DO c→ u ⟧ ⟹ s -WHILE b DO c→ u"

| (*<*)Local:(*>*) "f s -c→ t ⟹ s -LOCAL f; c; g→ g s t"

text‹Assuming that the state is a function from variables to values,
the declaration of a new local variable ‹x› with inital value
‹a› can be modelled as
‹LOCAL (λs. s(x := a s)); c; (λs t. t(x := s x))›.›

lemma exec_Do_iff[iff]: "(s -Do f→ t) = (t ∈ f s)"
by(auto elim: exec.cases intro:exec.intros)

lemma [iff]: "(s -c;d→ u) = (∃t. s -c→ t ∧ t -d→ u)"
by(best elim: exec.cases intro:exec.intros)

lemma [iff]: "(s -IF b THEN c ELSE d→ t) =
(s -if b s then c else d→ t)"
apply auto
apply(blast elim: exec.cases intro:exec.intros)+
done

lemma [iff]: "(s -LOCAL f; c; g→ u) = (∃t. f s -c→ t ∧ u = g s t)"
by(fastforce elim: exec.cases intro:exec.intros)

lemma 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:if_split_asm)

lemma while_lemma[rule_format]:
"s -w→ t ⟹ ∀b c. w = WHILE b DO c ∧ P s ∧
(∀s s'. P s ∧ b s ∧ s -c→ s' ⟶ P s') ⟶ P t ∧ ¬b t"
apply(erule exec.induct)
apply clarify+
defer
apply clarify+
apply(subgoal_tac "P t")
apply blast
apply blast
done

lemma while_rule:
"⟦s -WHILE b DO c→ t; P s; ∀s s'. P s ∧ b s ∧ s -c→ s' ⟶ P s'⟧
⟹ P t ∧ ¬b t"
apply(drule while_lemma)
prefer 2 apply assumption
apply blast
done

end


# Theory Hoare

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

theory Hoare imports Lang begin

subsection‹Hoare logic for partial correctness›

text‹We continue our semantic approach by modelling assertions just
like boolean expressions, i.e.\ as functions:›

type_synonym assn = "state ⇒ bool"

text‹Hoare triples are triples of the form ‹{P} c {Q}›, where
the assertions ‹P› and ‹Q› are the so-called pre and
postconditions. Such a triple is \emph{valid} (denoted by ‹⊨›)
iff every (terminating) execution starting in a state satisfying ‹P›
ends up in a state satisfying ‹Q›:›

definition
hoare_valid :: "assn ⇒ com ⇒ assn ⇒ bool" ("⊨ {(1_)}/ (_)/ {(1_)}" 50) where
"⊨ {P}c{Q} ⟷ (∀s t. s -c→ t ⟶ P s ⟶ Q t)"

text‹\noindent
This notion of validity is called \emph{partial correctness} because
it does not require termination of @{term c}.

Provability in Hoare logic is indicated by ‹⊢› and defined
inductively:›

inductive
hoare :: "assn ⇒ com ⇒ assn ⇒ bool" ("⊢ ({(1_)}/ (_)/ {(1_)})" 50)
where
(*<*)Do:(*>*)"⊢ {λs. ∀t ∈ f s. P t} Do f {P}"

| (*<*)Semi:(*>*)"⟦ ⊢ {P}c1{Q};  ⊢ {Q}c2{R} ⟧  ⟹  ⊢ {P} c1;c2 {R}"

| (*<*)If:(*>*)"⟦ ⊢ {λs. P s ∧ b s} c1 {Q};  ⊢ {λs. P s ∧ ¬b s} c2 {Q} ⟧
⟹ ⊢ {P} IF b THEN c1 ELSE c2 {Q}"

| (*<*)While:(*>*)"⊢ {λs. P s ∧ b s} c {P}  ⟹  ⊢ {P} WHILE b DO c {λs. P s ∧ ¬b s}"

| (*<*)Conseq:(*>*)"⟦ ∀s. P' s ⟶ P s;  ⊢ {P}c{Q};  ∀s. Q s ⟶ Q' s  ⟧  ⟹  ⊢ {P'}c{Q'}"

| (*<*)Local:(*>*) "⟦ ⋀s. P s ⟹ P' s (f s); ∀s. ⊢ {P' s} c {Q ∘ (g s)} ⟧ ⟹
⊢ {P} LOCAL f;c;g {Q}"

text‹Soundness is proved by induction on the derivation of @{prop"⊢
{P} c {Q}"}:›

theorem hoare_sound: "⊢ {P}c{Q}  ⟹  ⊨ {P}c{Q}"
apply(unfold hoare_valid_def)
apply(erule hoare.induct)
apply blast
apply blast
apply clarsimp
apply clarify
apply(drule while_rule)
prefer 3
apply (assumption, assumption, blast)
apply blast
apply clarify
apply(erule allE)
apply clarify
apply(erule allE)
apply(erule allE)
apply(erule impE)
apply assumption
apply simp
apply(erule mp)
apply(simp)
done

text‹
Completeness is not quite as straightforward, but still easy. The
proof is best explained in terms of the \emph{weakest precondition}:›

definition
wp :: "com ⇒ assn ⇒ assn" where
"wp c Q = (λs. ∀t. s -c→ t ⟶ Q t)"

text‹\noindent Dijkstra calls this the weakest \emph{liberal}
precondition to emphasize that it corresponds to partial
correctness. We use weakest precondition'' all the time and let the
context determine if we talk about partial or total correctness ---
the latter is introduced further below.

The following lemmas about @{term wp} are easily derived:
›

lemma [simp]: "wp (Do f) Q = (λs. ∀t ∈ f s. Q(t))"
apply(unfold wp_def)
apply(rule ext)
apply blast
done

lemma [simp]: "wp (c⇩1;c⇩2) R = wp c⇩1 (wp c⇩2 R)"
apply(unfold wp_def)
apply(rule ext)
apply blast
done

lemma [simp]:
"wp (IF b THEN c⇩1 ELSE c⇩2) Q = (λs. wp (if b s then c⇩1 else c⇩2) Q s)"
apply(unfold wp_def)
apply(rule ext)
apply auto
done

lemma wp_while:
"wp (WHILE b DO c) Q =
(λs. if b s then wp (c;WHILE b DO c) Q s else Q s)"
apply(rule ext)
apply(unfold wp_def)
apply auto
apply(blast intro:exec.intros)
apply(blast intro:exec.intros)
done

lemma [simp]:
"wp (LOCAL f;c;g) Q = (λs. wp c (Q o (g s)) (f s))"
apply(unfold wp_def)
apply(rule ext)
apply auto
done

lemma strengthen_pre: "⟦ ∀s. P' s ⟶ P s; ⊢ {P}c{Q}  ⟧ ⟹ ⊢ {P'}c{Q}"
by(erule hoare.Conseq, assumption, blast)

lemma weaken_post: "⟦ ⊢ {P}c{Q}; ∀s. Q s ⟶ Q' s  ⟧ ⟹ ⊢ {P}c{Q'}"
apply(rule hoare.Conseq)
apply(fast, assumption, assumption)
done

text‹By induction on @{term c} one can easily prove›

lemma wp_is_pre[rule_format]: "⊢ {wp c Q} c {Q}"
apply (induct c arbitrary: Q)
apply simp_all

apply(blast intro:hoare.Do hoare.Conseq)

apply(blast intro:hoare.Semi hoare.Conseq)

apply(blast intro:hoare.If hoare.Conseq)

apply(rule weaken_post)
apply(rule hoare.While)
apply(rule strengthen_pre)
prefer 2
apply blast
apply(clarify)
apply(drule fun_eq_iff[THEN iffD1, OF wp_while, THEN spec, THEN iffD1])
apply simp
apply(clarify)
apply(drule fun_eq_iff[THEN iffD1, OF wp_while, THEN spec, THEN iffD1])
apply(simp split:if_split_asm)

apply(fast intro!: hoare.Local)
done

text‹\noindent
from which completeness follows more or less directly via the
rule of consequence:›

theorem hoare_relative_complete: "⊨ {P}c{Q}  ⟹  ⊢ {P}c{Q}"
apply (rule strengthen_pre[OF _ wp_is_pre])
apply(unfold hoare_valid_def wp_def)
apply blast
done

end


# Theory Termi

(*  Title:       Inductive definition of termination
Author:      Tobias Nipkow, 2001/2006
Maintainer:  Tobias Nipkow
*)

theory Termi imports Lang begin

subsection‹Termination›

text‹Although partial correctness appeals because of its simplicity,
in many cases one would like the additional assurance that the command
is guaranteed to termiate if started in a state that satisfies the
precondition. Even to express this we need to define when a command is
guaranteed to terminate. We can do this without modifying our existing
semantics by merely adding a second inductively defined judgement
‹c↓s› that expresses guaranteed termination of @{term c}
started in state @{term s}:›

inductive
termi :: "com ⇒ state ⇒ bool" (infixl "↓" 50)
where
(*<*)Do[iff]:(*>*) "f s ≠ {} ⟹ Do f ↓ s"

| (*<*)Semi[intro!]:(*>*) "⟦ c⇩1 ↓ s⇩0; ∀s⇩1. s⇩0 -c⇩1→ s⇩1 ⟶ c⇩2 ↓ s⇩1 ⟧ ⟹ (c⇩1;c⇩2) ↓ s⇩0"

| (*<*)IfT[intro,simp]:(*>*) "⟦  b s; c⇩1 ↓ s ⟧ ⟹ IF b THEN c⇩1 ELSE c⇩2 ↓ s"
| (*<*)IfF[intro,simp]:(*>*) "⟦ ¬b s; c⇩2 ↓ s ⟧ ⟹ IF b THEN c⇩1 ELSE c⇩2 ↓ s"

| (*<*)WhileFalse:(*>*) "¬b s ⟹ WHILE b DO c ↓ s"
| (*<*)WhileTrue:(*>*) "⟦ b s; c ↓ s; ∀t. s -c→ t ⟶ WHILE b DO c ↓ t ⟧ ⟹ WHILE b DO c ↓ s"

| (*<*)Local:(*>*) "c ↓ f s ⟹ LOCAL f;c;g ↓ s"

lemma [iff]: "Do f ↓ s = (f s ≠ {})"
apply(rule iffI)
prefer 2
apply(best intro:termi.intros)
apply(erule termi.cases)
apply blast+
done

lemma [iff]: "((c⇩1;c⇩2) ↓ s⇩0) = (c⇩1 ↓ s⇩0 ∧ (∀s⇩1. s⇩0 -c⇩1→ s⇩1 ⟶ c⇩2 ↓ s⇩1))"
apply(rule iffI)
prefer 2
apply(best intro:termi.intros)
apply(erule termi.cases)
apply blast+
done

lemma [iff]: "(IF b THEN c⇩1 ELSE c⇩2 ↓ s) =
((if b s then c⇩1 else c⇩2) ↓ s)"
apply simp
apply(rule conjI)
apply(rule impI)
apply(rule iffI)
prefer 2
apply(blast intro:termi.intros)
apply(erule termi.cases)
apply blast+
apply(rule impI)
apply(rule iffI)
prefer 2
apply(blast intro:termi.intros)
apply(erule termi.cases)
apply blast+
done

lemma [iff]: "(LOCAL f;c;g ↓ s) = (c ↓ f s)"
by(fast elim: termi.cases intro:termi.intros)

lemma termi_while_lemma[rule_format]:
"w↓fk ⟹
(∀k b c. fk = f k ∧ w = WHILE b DO c ∧ (∀i. f i -c→ f(Suc i))
⟶ (∃i. ¬b(f i)))"
apply(erule termi.induct)
apply simp_all
apply blast
apply blast
done

lemma termi_while:
"⟦ (WHILE b DO c) ↓ f k;  ∀i. f i -c→ f(Suc i) ⟧ ⟹ ∃i. ¬b(f i)"
by(blast intro:termi_while_lemma)

lemma wf_termi: "wf {(t,s). WHILE b DO c ↓ s ∧ b s ∧ s -c→ t}"
apply(subst wf_iff_no_infinite_down_chain)
apply(rule notI)
apply clarsimp
apply(insert termi_while)
apply blast
done

end


# Theory HoareTotal

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

theory HoareTotal imports Hoare Termi begin

subsection‹Hoare logic for total correctness›

text‹
Now that we have termination, we can define
total validity, ‹⊨⇩t›, as partial validity and guaranteed termination:›

definition
hoare_tvalid :: "assn ⇒ com ⇒ assn ⇒ bool" ("⊨⇩t {(1_)}/ (_)/ {(1_)}" 50) where
"⊨⇩t {P}c{Q} ⟷ ⊨ {P}c{Q} ∧ (∀s. P s ⟶ c↓s)"

text‹Proveability of Hoare triples in the proof system for total
correctness is written ‹⊢⇩t {P}c{Q}› and defined
inductively. The rules for ‹⊢⇩t› differ from those for
‹⊢› only in the one place where nontermination can arise: the
@{term While}-rule.›

inductive
thoare :: "assn ⇒ com ⇒ assn ⇒ bool" ("⊢⇩t ({(1_)}/ (_)/ {(1_)})" 50)
where
Do:  "⊢⇩t {λs. (∀t ∈ f s. P t) ∧ f s ≠ {}} Do f {P}"
| Semi: "⟦ ⊢⇩t {P}c{Q}; ⊢⇩t {Q}d{R} ⟧ ⟹ ⊢⇩t {P} c;d {R}"
| If: "⟦ ⊢⇩t {λs. P s ∧ b s}c{Q}; ⊢⇩t {λs. P s ∧ ~b s}d{Q}  ⟧ ⟹
⊢⇩t {P} IF b THEN c ELSE d {Q}"
| While:
"⟦wf r;  ∀s'. ⊢⇩t {λs. P s ∧ b s ∧ s' = s} c {λs. P s ∧ (s,s') ∈ r}⟧
⟹ ⊢⇩t {P} WHILE b DO c {λs. P s ∧ ¬b s}"
| Conseq: "⟦ ∀s. P' s ⟶ P s; ⊢⇩t {P}c{Q}; ∀s. Q s ⟶ Q' s  ⟧ ⟹
⊢⇩t {P'}c{Q'}"

| Local: "(!!s. P s ⟹ P' s (f s)) ⟹ ∀p. ⊢⇩t {P' p} c {Q o (g p)} ⟹
⊢⇩t {P} LOCAL f;c;g {Q}"

text‹\noindent The@{term While}- rule is like the one for partial
correctness but it requires additionally that with every execution of
the loop body a wellfounded relation (@{prop"wf r"}) on the state
space decreases.

The soundness theorem›

(* Tried to use this lemma to simplify the soundness proof.
But "⊢⇩t {P}c{Q} ⟹ (!s. P s ⟶ c↓s)" is not provable because too weak
lemma total_implies_partial: "⊢⇩t {P} c {Q} ⟹ ⊢ {P} c {Q}"
apply(erule thoare.induct)
apply(rule hoare.intros)
apply (clarify) apply assumption
apply(rule hoare.intros)
apply blast
apply(blast intro:hoare.intros)
apply(blast intro:hoare.intros)
defer
apply(blast intro:hoare.intros)
apply(blast intro:hoare.intros)
apply(rule hoare.intros)
apply(rule hoare_relative_complete)
apply(unfold hoare_valid_def)
apply(clarify)
apply(erule allE, erule conjE)
apply(drule hoare_sound)
apply(unfold hoare_valid_def)
apply(blast)
done
*)

theorem "⊢⇩t {P}c{Q}  ⟹  ⊨⇩t {P}c{Q}"
apply(unfold hoare_tvalid_def hoare_valid_def)
apply(erule thoare.induct)
apply blast
apply blast
apply clarsimp
defer
apply blast
apply(rule conjI)
apply clarify
apply(erule allE)
apply clarify
apply(erule allE, erule allE, erule impE, erule asm_rl)
apply simp
apply(erule mp)
apply(simp)
apply blast
apply(rule conjI)
apply(rule allI)
apply(erule wf_induct)
apply clarify
apply(drule unfold_while[THEN iffD1])
apply (simp split: if_split_asm)
apply blast
apply(rule allI)
apply(erule wf_induct)
apply clarify
apply(case_tac "b x")
apply (blast intro: termi.WhileTrue)
apply (erule termi.WhileFalse)
done
(*>*)

text‹\noindent In the @{term While}-case we perform a
local proof by wellfounded induction over the given relation @{term r}.

The completeness proof proceeds along the same lines as the one for partial
correctness. First we have to strengthen our notion of weakest precondition
to take termination into account:›

definition
wpt :: "com ⇒ assn ⇒ assn" ("wp⇩t") where
"wp⇩t c Q = (λs. wp c Q s ∧ c↓s)"

lemmas wp_defs = wp_def wpt_def

lemma [simp]: "wp⇩t (Do f) Q = (λs. (∀t ∈ f s. Q t) ∧ f s ≠ {})"

lemma [simp]: "wp⇩t (c⇩1;c⇩2) R = wp⇩t c⇩1 (wp⇩t c⇩2 R)"
apply(unfold wp_defs)
apply(rule ext)
apply blast
done

lemma [simp]:
"wp⇩t (IF b THEN c⇩1 ELSE c⇩2) Q = (λs. wp⇩t (if b s then c⇩1 else c⇩2) Q s)"
apply(unfold wp_defs)
apply(rule ext)
apply auto
done

lemma [simp]: "wp⇩t (LOCAL f;c;g) Q = (λs. wp⇩t c (Q o (g s)) (f s))"
apply(unfold wp_defs)
apply(rule ext)
apply auto
done

lemma strengthen_pre: "⟦ ∀s. P' s ⟶ P s; ⊢⇩t {P}c{Q}  ⟧ ⟹ ⊢⇩t {P'}c{Q}"
by(erule thoare.Conseq, assumption, blast)

lemma weaken_post: "⟦ ⊢⇩t {P}c{Q}; ∀s. Q s ⟶ Q' s  ⟧ ⟹ ⊢⇩t {P}c{Q'}"
apply(rule thoare.Conseq)
apply(fast, assumption, assumption)
done

inductive_cases [elim!]: "WHILE b DO c ↓ s"

lemma wp_is_pre[rule_format]: "⊢⇩t {wp⇩t c Q} c {Q}"
apply (induct c arbitrary: Q)
apply simp_all
apply(blast intro:thoare.Do thoare.Conseq)
apply(blast intro:thoare.Semi thoare.Conseq)
apply(blast intro:thoare.If thoare.Conseq)
defer
apply(fastforce intro!: thoare.Local)
apply(rename_tac b c Q)
apply(rule weaken_post)
apply(rule_tac b=b and c=c in thoare.While)
apply(rule_tac b=b and c=c in wf_termi)
defer
apply(rule allI)
apply(rule strengthen_pre)
prefer 2
apply fast
apply(blast intro:exec.intros)
done

text‹\noindent The @{term While}-case is interesting because we now have to furnish a
suitable wellfounded relation. Of course the execution of the loop
body directly yields the required relation.
The actual completeness theorem follows directly, in the same manner
as for partial correctness.›

theorem "⊨⇩t {P}c{Q} ⟹ ⊢⇩t {P}c{Q}"
apply (rule strengthen_pre[OF _ wp_is_pre])
apply(unfold hoare_tvalid_def hoare_valid_def wp_defs)
apply blast
done

end


# Theory PLang

(*  Title:       One procedure
Author:      Tobias Nipkow, 2001/2006
Maintainer:  Tobias Nipkow
*)

section "Hoare Logics for 1 Procedure"

theory PLang imports Main begin

subsection‹The language›

typedecl state

type_synonym bexp = "state ⇒ bool"

datatype com = Do "(state ⇒ state set)"
| Semi  com com            ("_; _"  [60, 60] 10)
| Cond  bexp com com     ("IF _ THEN _ ELSE _"  60)
| While bexp com           ("WHILE _ DO _"  60)
| CALL
| Local "(state ⇒ state)" com "(state ⇒ state ⇒ state)"
("LOCAL _; _; _" [0,0,60] 60)

text‹\noindent There is only one parameterless procedure in the program. Hence
@{term CALL} does not even need to mention the procedure name. There
is no separate syntax for procedure declarations. Instead we declare a HOL
constant that represents the body of the one procedure in the program.›

consts body :: com

text‹\noindent
As before, command execution is described by transitions
‹s -c→ t›. The only new rule is the one for @{term CALL} ---
it requires no comment:›

inductive
exec :: "state ⇒ com ⇒ state ⇒ bool"  ("_/ -_→/ _" [50,0,50] 50)
where
Do:     "t ∈ f s ⟹ s -Do f→ t"

| Semi:   "⟦ s0 -c1→ s1; s1 -c2→ s2 ⟧
⟹ s0 -c1;c2→ s2"

| IfTrue:  "⟦ b s;  s -c1→ t ⟧ ⟹ s -IF b THEN c1 ELSE c2→ t"
| IfFalse: "⟦ ¬b s; s -c2→ t ⟧ ⟹ s -IF b THEN c1 ELSE c2→ t"

| WhileFalse: "¬b s ⟹ s -WHILE b DO c→ s"
| WhileTrue:  "⟦ b s; s -c→ t; t -WHILE b DO c→ u ⟧
⟹ s -WHILE b DO c→ u"

| "s -body→ t ⟹ s -CALL→ t"

| Local: "f s -c→ t ⟹ s -LOCAL f; c; g→ g s t"

lemma [iff]: "(s -Do f→ t) = (t ∈ f s)"
by(auto elim: exec.cases intro:exec.intros)

lemma [iff]: "(s -c;d→ u) = (∃t. s -c→ t ∧ t -d→ u)"
by(auto elim: exec.cases intro:exec.intros)

lemma [iff]: "(s -IF b THEN c ELSE d→ t) =
(s -if b s then c else d→ t)"
apply(rule iffI)
apply(auto elim: exec.cases intro:exec.intros)
apply(auto intro:exec.intros split:if_split_asm)
done

lemma 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:if_split_asm)

lemma [iff]: "(s -CALL→ t) = (s -body→ t)"
by(blast elim: exec.cases intro:exec.intros)

lemma [iff]: "(s -LOCAL f; c; g→ u) = (∃t. f s -c→ t ∧ u = g s t)"
by(fastforce elim: exec.cases intro:exec.intros)

lemma [simp]: "¬b s ⟹ s -WHILE b DO c→ s"
by(fast intro:exec.intros)

lemma WhileI: "⟦b s; s -c→ t; t -WHILE b DO c→ u⟧ ⟹ s -WHILE b DO c→ u"
by(fastforce elim:exec.WhileTrue)
(*>*)

text‹This semantics turns out not to be fine-grained
enough. The soundness proof for the Hoare logic below proceeds by
induction on the call depth during execution. To make this work we
define a second semantics \mbox{‹s -c-n→ t›} which expresses that the
execution uses at most @{term n} nested procedure invocations, where
@{term n} is a natural number. The rules are straightforward: @{term
n} is just passed around, except for procedure calls, where it is
decremented:›

inductive
execn :: "state ⇒ com ⇒ nat ⇒ state ⇒ bool"   ("_/ -_-_→/ _" [50,0,0,50] 50)
where
"t ∈ f s ⟹ s -Do f-n→ t"

| "⟦ s0 -c1-n→ s1; s1 -c2-n→ s2 ⟧ ⟹ s0 -c1;c2-n→ s2"

| "⟦  b s; s -c1-n→ t ⟧ ⟹ s -IF b THEN c1 ELSE c2-n→ t"
| "⟦ ¬b s; s -c2-n→ t ⟧ ⟹ s -IF b THEN c1 ELSE c2-n→ t"

| (*<*)WhileFalse:(*>*)"¬b s ⟹ s -WHILE b DO c-n→ s"
| (*<*)WhileTrue:(*>*)"⟦b s; s -c-n→ t; t -WHILE b DO c-n→ u⟧ ⟹ s -WHILE b DO c-n→ u"

| "s -body-n→ t ⟹ s -CALL-Suc n→ t"

| "f s -c-n→ t ⟹ s -LOCAL f; c; g-n→ g s t"

lemma [iff]: "(s -Do f-n→ t) = (t ∈ f s)"
by(auto elim: execn.cases intro:execn.intros)

lemma [iff]: "(s -c1;c2-n→ u) = (∃t. s -c1-n→ t ∧ t -c2-n→ u)"
by(best elim: execn.cases intro:execn.intros)

lemma [iff]: "(s -IF b THEN c ELSE d-n→ t) =
(s -if b s then c else d-n→ t)"
apply auto
apply(blast elim: execn.cases intro:execn.intros)+
done

lemma [iff]: "(s -CALL- 0→ t) = False"
by(blast elim: execn.cases intro:execn.intros)

lemma [iff]: "(s -CALL-Suc n→ t) = (s -body-n→ t)"
by(blast elim: execn.cases intro:execn.intros)

lemma [iff]: "(s -LOCAL f; c; g-n→ u) = (∃t. f s -c-n→ t ∧ u = g s t)"
by(auto elim: execn.cases intro:execn.intros)

text‹\noindent By induction on @{prop"s -c-m→ t"} we show
monotonicity w.r.t.\ the call depth:›

lemma exec_mono[rule_format]: "s -c-m→ t ⟹ ∀n. m ≤ n ⟶ s -c-n→ t"
apply(erule execn.induct)
apply(blast)
apply(blast)
apply(simp)
apply(simp)
apply(blast intro:execn.intros)
apply(clarify)
apply(rename_tac m)
apply(case_tac m)
apply simp
apply simp
apply blast
done

text‹\noindent With the help of this lemma we prove the expected
relationship between the two semantics:›

lemma exec_iff_execn: "(s -c→ t) = (∃n. s -c-n→ t)"
apply(rule iffI)
apply(erule exec.induct)
apply blast
apply clarify
apply(rename_tac m n)
apply(rule_tac x = "max m n" in exI)
apply fastforce
apply fastforce
apply(blast intro:execn.intros)
apply clarify
apply(rename_tac m n)
apply(rule_tac x = "max m n" in exI)
apply blast
apply blast
apply(erule exE, erule execn.induct)
apply blast
apply blast
apply fastforce
apply fastforce
apply(erule exec.WhileFalse)
apply(blast intro: exec.intros)
apply blast
apply blast
done

lemma while_lemma[rule_format]:
"s -w-n→ t ⟹ ∀b c. w = WHILE b DO c ∧ P s ∧
(∀s s'. P s ∧ b s ∧ s -c-n→ s' ⟶ P s') ⟶ P t ∧ ¬b t"
apply(erule execn.induct)
apply clarify+
defer
apply clarify+
apply(subgoal_tac "P t")
apply blast
apply blast
done

lemma while_rule:
"⟦s -WHILE b DO c-n→ t; P s; ⋀s s'. ⟦P s; b s; s -c-n→ s' ⟧ ⟹ P s'⟧
⟹ P t ∧ ¬b t"
apply(drule while_lemma)
prefer 2 apply assumption
apply blast
done

end


# Theory PHoare

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

theory PHoare imports PLang begin

subsection‹Hoare logic for partial correctness›

text‹Taking auxiliary variables seriously means that assertions must
now depend on them as well as on the state. Initially we do not fix
the type of auxiliary variables but parameterize the type of
assertions with a type variable @{typ 'a}:›

type_synonym 'a assn = "'a ⇒ state ⇒ bool"

text‹
The second major change is the need to reason about Hoare
triples in a context: proofs about recursive procedures are conducted
by induction where we assume that all @{term CALL}s satisfy the given
pre/postconditions and have to show that the body does as well. The
assumption is stored in a context, which is a set of Hoare triples:›

type_synonym 'a cntxt = "('a assn × com × 'a assn)set"

text‹\noindent In the presence of only a single procedure the context will
always be empty or a singleton set. With multiple procedures, larger
sets can arise.

Now that we have contexts, validity becomes more complicated. Ordinary
validity (w.r.t.\ partial correctness) is still what it used to be,
except that we have to take auxiliary variables into account as well:
›

definition
valid :: "'a assn ⇒ com ⇒ 'a assn ⇒ bool" ("⊨ {(1_)}/ (_)/ {(1_)}" 50) where
"⊨ {P}c{Q} ⟷ (∀s t. s -c→ t ⟶ (∀z. P z s ⟶ Q z t))"

text‹\noindent Auxiliary variables are always denoted by @{term z}.

Validity of a context and validity of a Hoare triple in a context are defined
as follows:›

definition
valids :: "'a cntxt ⇒ bool" ("|⊨ _" 50) where
[simp]: "|⊨ C ≡ (∀(P,c,Q) ∈ C. ⊨ {P}c{Q})"

definition
cvalid :: "'a cntxt ⇒ 'a assn ⇒ com ⇒ 'a assn ⇒ bool" ("_ ⊨/ {(1_)}/ (_)/ {(1_)}" 50) where
"C ⊨ {P}c{Q} ⟷ |⊨ C ⟶ ⊨ {P}c{Q}"

text‹\noindent Note that @{prop"{} ⊨ {P}c{Q}"} is equivalent to
@{prop"⊨ {P}c{Q}"}.

Unfortunately, this is not the end of it. As we have two
semantics, ‹-c→› and ‹-c-n→›, we also need a second notion
of validity parameterized with the recursion depth @{term n}:›

definition
nvalid :: "nat ⇒ 'a assn ⇒ com ⇒ 'a assn ⇒ bool" ("⊨_ {(1_)}/ (_)/ {(1_)}" 50) where
"⊨n {P}c{Q} ≡ (∀s t. s -c-n→ t ⟶ (∀z. P z s ⟶ Q z t))"

definition
nvalids :: "nat ⇒ 'a cntxt ⇒ bool" ("|⊨'__/ _" 50) where
"|⊨_n C ≡ (∀(P,c,Q) ∈ C. ⊨n {P}c{Q})"

definition
cnvalid :: "'a cntxt ⇒ nat ⇒ 'a assn ⇒ com ⇒ 'a assn ⇒ bool" ("_ ⊨_/ {(1_)}/ (_)/ {(1_)}" 50) where
"C ⊨n {P}c{Q} ⟷ |⊨_n C ⟶ ⊨n {P}c{Q}"

text‹Finally we come to the proof system for deriving triples in a context:›

inductive
hoare :: "'a cntxt ⇒ 'a assn ⇒ com ⇒ 'a assn ⇒ bool" ("_ ⊢/ ({(1_)}/ (_)/ {(1_)})" 50)
where
(*<*)Do:(*>*)"C ⊢ {λz s. ∀t ∈ f s . P z t} Do f {P}"

| (*<*)Semi:(*>*)"⟦ C ⊢ {P}c1{Q}; C ⊢ {Q}c2{R} ⟧ ⟹ C ⊢ {P} c1;c2 {R}"

| (*<*)If:(*>*)"⟦ C ⊢ {λz s. P z s ∧ b s}c1{Q};  C ⊢ {λz s. P z s ∧ ¬b s}c2{Q}  ⟧
⟹ C ⊢ {P} IF b THEN c1 ELSE c2 {Q}"

| (*<*)While:(*>*)"C ⊢ {λz s. P z s ∧ b s} c {P}
⟹ C ⊢ {P} WHILE b DO c {λz s. P z s ∧ ¬b s}"

| (*<*)Conseq:(*>*)"⟦ C ⊢ {P'}c{Q'};  ∀s t. (∀z. P' z s ⟶ Q' z t) ⟶ (∀z. P z s ⟶ Q z t) ⟧
⟹ C ⊢ {P}c{Q}"

| (*<*)Call:(*>*)"{(P,CALL,Q)} ⊢ {P}body{Q} ⟹ {} ⊢ {P} CALL {Q}"

| (*<*)Asm:(*>*)"{(P,CALL,Q)} ⊢ {P} CALL {Q}"
| (*<*)Local:(*>*) "⟦ ∀s'. C ⊢ {λz s. P z s' ∧ s = f s'} c {λz t. Q z (g s' t)} ⟧ ⟹
C ⊢ {P} LOCAL f;c;g {Q}"

abbreviation hoare1 :: "'a cntxt ⇒ 'a assn × com × 'a assn ⇒ bool" ("_ ⊢ _") where
"C ⊢ x ≡ C ⊢ {fst x}fst (snd x){snd (snd x)}"

text‹\noindent The first four rules are familiar, except for their adaptation
to auxiliary variables. The @{term CALL} rule embodies induction and
has already been motivated above. Note that it is only applicable if
the context is empty. This shows that we never need nested induction.
For the same reason the assumption rule (the last rule) is stated with
just a singleton context.

The rule of consequence is explained in the accompanying paper.
›

lemma strengthen_pre:
"⟦ ∀z s. P' z s ⟶ P z s; C⊢ {P}c{Q}  ⟧ ⟹ C⊢ {P'}c{Q}"
by(rule hoare.Conseq, assumption, blast)

lemmas valid_defs = valid_def valids_def cvalid_def
nvalid_def nvalids_def cnvalid_def

theorem hoare_sound: "C ⊢ {P}c{Q}  ⟹  C ⊨ {P}c{Q}"
txt‹\noindent requires a generalization: @{prop"∀n. C ⊨n
{P}c{Q}"} is proved instead, from which the actual theorem follows
directly via lemma @{thm[source]exec_iff_execn} in \S\ref{sec:proc1-lang}.
The generalization
is proved by induction on @{term c}. The reason for the generalization
is that soundness of the @{term CALL} rule is proved by induction on the
maximal call depth, i.e.\ @{term n}.›
apply(subgoal_tac "∀n. C ⊨n {P}c{Q}")
apply(unfold valid_defs exec_iff_execn)
apply fast
apply(erule hoare.induct)
apply simp
apply fast
apply simp
apply clarify
apply(drule while_rule)
prefer 3
apply (assumption, assumption)
apply fast
apply fast
prefer 2
apply simp
apply(rule allI, rule impI)
apply(induct_tac n)
apply blast
apply clarify
apply (simp(no_asm_use))
apply blast
apply auto
done

text‹
The completeness proof employs the notion of a \emph{most general triple} (or
\emph{most general formula}):›

definition
MGT :: "com ⇒ state assn × com × state assn" where
"MGT c = (λz s. z = s, c, λz t. z -c→ t)"

declare MGT_def[simp]

text‹\noindent Note that the type of @{term z} has been identified with
@{typ state}.  This means that for every state variable there is an auxiliary
variable, which is simply there to record the value of the program variables
before execution of a command. This is exactly what, for example, VDM offers
by allowing you to refer to the pre-value of a variable in a
postcondition. The intuition behind @{term"MGT c"} is
that it completely describes the operational behaviour of @{term c}.  It is
easy to see that, in the presence of the new consequence rule,
\mbox{@{prop"{} ⊢ MGT c"}} implies completeness:›

lemma MGT_implies_complete:
"{} ⊢ MGT c  ⟹  {} ⊨ {P}c{Q}  ⟹  {} ⊢ {P}c{Q::state assn}"
apply (erule hoare.Conseq)
done

text‹In order to discharge @{prop"{} ⊢ MGT c"} one proves›

lemma MGT_lemma: "C ⊢ MGT CALL  ⟹  C ⊢ MGT c"
apply (simp)
apply(induct_tac c)
apply (rule strengthen_pre[OF _ hoare.Do])
apply blast
apply(blast intro:hoare.Semi hoare.Conseq)
apply(rule hoare.If)
apply(erule hoare.Conseq)
apply simp
apply(erule hoare.Conseq)
apply simp
prefer 2
apply simp
apply(rename_tac b c)
apply(rule hoare.Conseq)
apply(rule_tac P = "λz s. (z,s) ∈ ({(s,t). b s ∧ s -c→ t})^*"
in hoare.While)
apply(erule hoare.Conseq)
apply(blast intro:rtrancl_into_rtrancl)
apply clarsimp
apply(rename_tac s t)
apply(erule_tac x = s in allE)
apply clarsimp
apply(erule converse_rtrancl_induct)
apply simp
apply(fast elim:exec.WhileTrue)
apply(fastforce intro: hoare.Local elim!: hoare.Conseq)
done

text‹\noindent The proof is by induction on @{term c}. In the @{term
While}-case it is easy to show that @{term"λz t. (z,t) ∈ ({(s,t). b
s ∧ s -c→ t})^*"} is invariant. The precondition \mbox{@{term[source]"λz s. z=s"}}
establishes the invariant and a reflexive transitive closure
induction shows that the invariant conjoined with @{prop"¬b t"}
implies the postcondition \mbox{@{term"λz t. z -WHILE b DO c→ t"}}. The
remaining cases are trivial.

Using the @{thm[source]MGT_lemma} (together with the ‹CALL› and the
assumption rule) one can easily derive›

lemma MGT_CALL: "{} ⊢ MGT CALL"
apply (rule hoare.Call)
apply (rule hoare.Conseq[OF MGT_lemma[simplified], OF hoare.Asm])
apply (fast intro:exec.intros)
done

text‹\noindent Using the @{thm[source]MGT_lemma} once more we obtain
@{prop"{} ⊢ MGT c"} and thus by @{thm[source]MGT_implies_complete}
completeness.›

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

end


# Theory PTermi

(*  Title:      Inductive definition of termination
Author:      Tobias Nipkow, 2001/2006
Maintainer:  Tobias Nipkow
*)
theory PTermi imports PLang begin

subsection‹Termination›

inductive
termi :: "com ⇒ state ⇒ bool" (infixl "↓" 50)
where
Do[iff]: "f s ≠ {} ⟹ Do f ↓ s"
| Semi[intro!]:   "⟦ c1 ↓ s0; ⋀s1. s0 -c1→ s1 ⟹ c2 ↓ s1 ⟧
⟹ (c1;c2) ↓ s0"

| IfTrue[intro,simp]: "⟦ b s; c1 ↓ s ⟧ ⟹ IF b THEN c1 ELSE c2 ↓ s"
| IfFalse[intro,simp]: "⟦ ¬b s; c2 ↓ s ⟧ ⟹ IF b THEN c1 ELSE c2 ↓ s"

| WhileFalse: "¬b s ⟹ WHILE b DO c ↓ s"

| WhileTrue:  "⟦ b s; c ↓ s; ⋀t. s -c→ t ⟹ WHILE b DO c ↓ t ⟧
⟹ WHILE b DO c ↓ s"
| "body ↓ s ⟹ CALL ↓ s"

| Local: "c ↓ f s ⟹ LOCAL f;c;g ↓ s"

lemma [iff]: "(Do f ↓ s) = (f s ≠ {})"
apply(rule iffI)
prefer 2
apply(best intro:termi.intros)
apply(erule termi.cases)
apply blast+
done

lemma [iff]: "((c1;c2) ↓ s0) = (c1 ↓ s0 ∧ (∀s1. s0 -c1→ s1 ⟶ c2 ↓ s1))"
apply(rule iffI)
prefer 2
apply(best intro:termi.intros)
apply(erule termi.cases)
apply blast+
done

lemma [iff]: "(IF b THEN c1 ELSE c2 ↓ s) =
((if b s then c1 else c2) ↓ s)"
apply simp
apply(rule conjI)
apply(rule impI)
apply(rule iffI)
prefer 2
apply(blast intro:termi.intros)
apply(erule termi.cases)
apply blast+
apply(rule impI)
apply(rule iffI)
prefer 2
apply(blast intro:termi.intros)
apply(erule termi.cases)
apply blast+
done

lemma [iff]: "(CALL ↓ s) = (body ↓ s)"
by(fast elim: termi.cases intro:termi.intros)

lemma [iff]: "(LOCAL f;c;g ↓ s) = (c ↓ f s)"
by(fast elim: termi.cases intro:termi.intros)

lemma termi_while_lemma[rule_format]:
"w↓fk ⟹
(∀k b c. fk = f k ∧ w = WHILE b DO c ∧ (∀i. f i -c→ f(Suc i))
⟶ (∃i. ¬b(f i)))"
apply(erule termi.induct)
apply simp_all
apply blast
apply blast
done

lemma termi_while:
"⟦ (WHILE b DO c) ↓ f k;  ∀i. f i -c→ f(Suc i) ⟧ ⟹ ∃i. ¬b(f i)"
by(blast intro:termi_while_lemma)

lemma wf_termi: "wf {(t,s). WHILE b DO c ↓ s ∧ b s ∧ s -c→ t}"
apply(subst wf_iff_no_infinite_down_chain)
apply(rule notI)
apply clarsimp
apply(insert termi_while)
apply blast
done

end


# 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
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(subgoal_tac "∀n. ⊨⇩t {λz s. P z s ∧ s=n} body {Q}")
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 (erule thoare.Conseq)
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)
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(rule_tac x = "λi. case i of 0 ⇒ ((WHILE b DO c)#cs,s) | Suc i ⇒ f i" in exI)
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)
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)
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(drule exec1_only1)
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)
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(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



# Theory PsLang

(*  Title:       Mutually recursive procedures
Author:      Tobias Nipkow, 2001/2006
Maintainer:  Tobias Nipkow
*)

section "Hoare Logics for Mutually Recursive Procedure"

theory PsLang imports Main begin

subsection‹The language›

typedecl state
typedecl pname

type_synonym bexp = "state ⇒ bool"

datatype
com = Do "state ⇒ state set"
| Semi  com com          ("_; _"  [60, 60] 10)
| Cond  bexp com com     ("IF _ THEN _ ELSE _"  60)
| While bexp com         ("WHILE _ DO _"  60)
| CALL pname
| Local "(state ⇒ state)" com "(state ⇒ state ⇒ state)"
("LOCAL _; _; _" [0,0,60] 60)

consts body :: "pname ⇒ com"

text‹We generalize from a single procedure to a whole set of
procedures following the ideas of von Oheimb~\cite{Oheimb-FSTTCS99}.
The basic setup is modified only in a few places:
\begin{itemize}
\item We introduce a new basic type @{typ pname} of procedure names.
\item Constant @{term body} is now of type @{typ"pname ⇒ com"}.
\item The @{term CALL} command now has an argument of type @{typ pname},
the name of the procedure that is to be called.
\end{itemize}
›

inductive
exec :: "state ⇒ com ⇒ state ⇒ bool"   ("_/ -_→/ _" [50,0,50] 50)
where
Do:     "t ∈ f s ⟹ s -Do f→ t"

| Semi:   "⟦ s0 -c1→ s1; s1 -c2→ s2 ⟧ ⟹ s0 -c1;c2→ s2"

| IfTrue:  "⟦ b s;  s -c1→ t ⟧ ⟹ s -IF b THEN c1 ELSE c2→ t"
| IfFalse: "⟦ ¬b s; s -c2→ t ⟧ ⟹ s -IF b THEN c1 ELSE c2→ t"

| WhileFalse: "¬b s ⟹ s -WHILE b DO c→ s"
| WhileTrue:  "⟦ b s; s -c→ t; t -WHILE b DO c→ u ⟧
⟹ s -WHILE b DO c→ u"

| Call: "s -body p→ t ⟹ s -CALL p→ t"

| Local: "f s -c→ t ⟹ s -LOCAL f; c; g→ g s t"

lemma [iff]: "(s -Do f→ t) = (t ∈ f s)"
by(auto elim: exec.cases intro:exec.intros)

lemma [iff]: "(s -c;d→ u) = (∃t. s -c→ t ∧ t -d→ u)"
by(auto elim: exec.cases intro:exec.intros)

lemma [iff]: "(s -IF b THEN c ELSE d→ t) =
(s -if b s then c else d→ t)"
apply(rule iffI)
apply(auto elim: exec.cases intro:exec.intros)
apply(auto intro:exec.intros split:if_split_asm)
done

lemma [iff]: "(s -CALL p→ t) = (s -body p→ t)"
by(blast elim: exec.cases intro:exec.intros)

lemma [iff]: "(s -LOCAL f; c; g→ u) = (∃t. f s -c→ t ∧ u = g s t)"
by(fastforce elim: exec.cases intro:exec.intros)

inductive
execn :: "state ⇒ com ⇒ nat ⇒ state ⇒ bool"   ("_/ -_-_→/ _" [50,0,0,50] 50)
where
Do:     "t ∈ f s ⟹ s -Do f-n→ t"

| Semi:   "⟦ s0 -c0-n→ s1; s1 -c1-n→ s2 ⟧ ⟹ s0 -c0;c1-n→ s2"

| IfTrue: "⟦ b s; s -c0-n→ t ⟧ ⟹ s -IF b THEN c0 ELSE c1-n→ t"

| IfFalse: "⟦ ¬b s; s -c1-n→ t ⟧ ⟹ s -IF b THEN c0 ELSE c1-n→ t"

| WhileFalse: "¬b s ⟹ s -WHILE b DO c-n→ s"

| WhileTrue:  "⟦ b s; s -c-n→ t; t -WHILE b DO c-n→ u ⟧
⟹ s -WHILE b DO c-n→ u"

| Call:  "s -body p-n→ t ⟹ s -CALL p-Suc n→ t"

| Local: "f s -c-n→ t ⟹ s -LOCAL f; c; g-n→ g s t"

lemma [iff]: "(s -Do f-n→ t) = (t ∈ f s)"
by(auto elim: execn.cases intro:execn.intros)

lemma [iff]: "(s -c1;c2-n→ u) = (∃t. s -c1-n→ t ∧ t -c2-n→ u)"
by(best elim: execn.cases intro:execn.intros)

lemma [iff]: "(s -IF b THEN c ELSE d-n→ t) =
(s -if b s then c else d-n→ t)"
apply auto
apply(blast elim: execn.cases intro:execn.intros)+
done

lemma [iff]: "(s -CALL p- 0→ t) = False"
by(blast elim: execn.cases intro:execn.intros)

lemma [iff]: "(s -CALL p-Suc n→ t) = (s -body p-n→ t)"
by(blast elim: execn.cases intro:execn.intros)

lemma [iff]: "(s -LOCAL f; c; g-n→ u) = (∃t. f s -c-n→ t ∧ u = g s t)"
by(auto elim: execn.cases intro:execn.intros)

lemma exec_mono[rule_format]: "s -c-m→ t ⟹ ∀n. m ≤ n ⟶ s -c-n→ t"
apply(erule execn.induct)
apply(blast)
apply(blast)
apply(simp)
apply(simp)
apply(blast intro:execn.intros)
apply(clarify)
apply(rename_tac m)
apply(case_tac m)
apply simp
apply simp
apply blast
done

lemma exec_iff_execn: "(s -c→ t) = (∃n. s -c-n→ t)"
apply(rule iffI)
apply(erule exec.induct)
apply blast
apply clarify
apply(rename_tac m n)
apply(rule_tac x = "max m n" in exI)
apply fastforce
apply fastforce
apply(blast intro:execn.intros)
apply clarify
apply(rename_tac m n)
apply(rule_tac x = "max m n" in exI)
apply blast
apply blast
apply(erule exE, erule execn.induct)
apply blast
apply blast
apply fastforce
apply fastforce
apply(erule exec.WhileFalse)
apply(blast intro: exec.intros)
apply blast
apply blast
done

lemma while_lemma[rule_format]:
"s -w-n→ t ⟹ ∀b c. w = WHILE b DO c ∧ P s ∧
(∀s s'. P s ∧ b s ∧ s -c-n→ s' ⟶ P s') ⟶ P t ∧ ¬b t"
apply(erule execn.induct)
apply clarify+
defer
apply clarify+
apply(subgoal_tac "P t")
apply blast
apply blast
done

lemma while_rule:
"⟦s -WHILE b DO c-n→ t; P s; ⋀s s'. ⟦P s; b s; s -c-n→ s' ⟧ ⟹ P s'⟧
⟹ P t ∧ ¬b t"
apply(drule while_lemma)
prefer 2 apply assumption
apply blast
done

end


# Theory PsHoare

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

theory PsHoare imports PsLang begin

subsection‹Hoare logic for partial correctness›

type_synonym 'a assn = "'a ⇒ state ⇒ bool"
type_synonym 'a cntxt = "('a assn × com × 'a assn)set"

definition
valid :: "'a assn ⇒ com ⇒ 'a assn ⇒ bool" ("⊨ {(1_)}/ (_)/ {(1_)}" 50) where
"⊨ {P}c{Q} ≡ (∀s t z. s -c→ t ⟶ P z s ⟶ Q z t)"

definition
valids :: "'a cntxt ⇒ bool" ("|⊨ _" 50) where
"|⊨ D ≡ (∀(P,c,Q) ∈ D. ⊨ {P}c{Q})"

definition
nvalid :: "nat ⇒ 'a assn ⇒ com ⇒ 'a assn ⇒ bool" ("⊨_ {(1_)}/ (_)/ {(1_)}" 50) where
"⊨n {P}c{Q} ≡ (∀s t z. s -c-n→ t ⟶ P z s ⟶ Q z t)"

definition
nvalids :: "nat ⇒ 'a cntxt ⇒ bool" ("|⊨'__/ _" 50) where
"|⊨_n C ≡ (∀(P,c,Q) ∈ C. ⊨n {P}c{Q})"

text‹We now need an additional notion of
validity \mbox{‹C |⊨ D›} where @{term D} is a set as well. The
reason is that we can now have mutually recursive procedures whose
correctness needs to be established by simultaneous induction. Instead
of sets of Hoare triples we may think of conjunctions. We define both
‹C |⊨ D› and its relativized version:›

definition
cvalids :: "'a cntxt ⇒ 'a cntxt ⇒ bool" ("_ |⊨/ _" 50) where
"C |⊨ D ⟷ |⊨ C ⟶ |⊨ D"

definition
cnvalids :: "'a cntxt ⇒ nat ⇒ 'a cntxt ⇒ bool" ("_ |⊨'__/ _" 50) where
"C |⊨_n D ⟷ |⊨_n C ⟶ |⊨_n D"

text‹Our Hoare logic now defines judgements of the form ‹C ⊩
D› where both @{term C} and @{term D} are (potentially infinite) sets
of Hoare triples; ‹C ⊢ {P}c{Q}› is simply an abbreviation for
‹C ⊩ {(P,c,Q)}›.›

inductive
hoare :: "'a cntxt ⇒ 'a cntxt ⇒ bool" ("_ ⊩/ _" 50)
and hoare3 :: "'a cntxt ⇒ 'a assn ⇒ com ⇒ 'a assn ⇒ bool" ("_ ⊢/ ({(1_)}/ (_)/ {(1_)})" 50)
where
"C ⊢ {P}c{Q}  ≡  C ⊩ {(P,c,Q)}"
| Do:  "C ⊢ {λz s. ∀t ∈ f s . P z t} Do f {P}"
| Semi: "⟦ C ⊢ {P}c{Q}; C ⊢ {Q}d{R} ⟧ ⟹ C ⊢ {P} c;d {R}"
| If: "⟦ C ⊢ {λz s. P z s ∧ b s}c{Q}; C ⊢ {λz s. P z s ∧ ¬b s}d{Q}  ⟧ ⟹
C ⊢ {P} IF b THEN c ELSE d {Q}"
| While: "C ⊢ {λz s. P z s ∧ b s} c {P} ⟹
C ⊢ {P} WHILE b DO c {λz s. P z s ∧ ¬b s}"

| Conseq: "⟦ C ⊢ {P'}c{Q'};
∀s t. (∀z. P' z s ⟶ Q' z t) ⟶ (∀z. P z s ⟶ Q z t) ⟧ ⟹
C ⊢ {P}c{Q}"

| Call: "⟦ ∀(P,c,Q) ∈ C. ∃p. c = CALL p;
C ⊩ {(P,b,Q). ∃p. (P,CALL p,Q) ∈ C ∧ b = body p} ⟧
⟹ {} ⊩ C"

| Asm: "(P,CALL p,Q) ∈ C ⟹ C ⊢ {P} CALL p {Q}"

| ConjI: "∀(P,c,Q) ∈ D. C ⊢ {P}c{Q}  ⟹  C ⊩ D"
| ConjE: "⟦ C ⊩ D; (P,c,Q) ∈ D ⟧ ⟹ C ⊢ {P}c{Q}"

| Local: "⟦ ∀s'. C ⊢ {λz s. P z s' ∧ s = f s'} c {λz t. Q z (g s' t)} ⟧ ⟹
C ⊢ {P} LOCAL f;c;g {Q}"
monos split_beta

lemmas valid_defs = valid_def valids_def cvalids_def
nvalid_def nvalids_def cnvalids_def

theorem "C ⊩ D  ⟹  C |⊨ D"

txt‹\noindent As before, we prove a generalization of @{prop"C |⊨ D"},
namely @{prop"∀n. C |⊨_n D"}, by induction on @{prop"C ⊩ D"}, with an
induction on @{term n} in the @{term CALL} case.›

apply(subgoal_tac "∀n. C |⊨_n D")
apply(unfold valid_defs exec_iff_execn[THEN eq_reflection])
apply fast
apply(erule hoare.induct)
apply simp
apply simp
apply fast
apply simp
apply clarify
apply(drule while_rule)
prefer 3
apply (assumption, assumption)
apply simp
apply simp
apply fast
apply(rule allI, rule impI)
apply(induct_tac n)
apply force
apply clarify
apply(frule bspec, assumption)
apply (simp(no_asm_use))
apply fast
apply simp
apply fast

apply simp
apply fast

apply fast

apply fastforce
done

definition MGT :: "com ⇒ state assn × com × state assn" where
[simp]: "MGT c = (λz s. z = s, c, λz t. z -c→ t)"

lemma strengthen_pre:
"⟦ ∀z s. P' z s ⟶ P z s; C⊢ {P}c{Q}  ⟧ ⟹ C⊢ {P'}c{Q}"
by(rule hoare.Conseq, assumption, blast)

lemma MGT_implies_complete:
"{} ⊩ {MGT c} ⟹ ⊨ {P}c{Q} ⟹ {} ⊢ {P}c{Q::state assn}"
apply(unfold MGT_def)
apply (erule hoare.Conseq)
done

lemma MGT_lemma: "∀p. C ⊩ {MGT(CALL p)}  ⟹  C ⊩ {MGT c}"
apply (simp)
apply(induct_tac c)
apply (rule strengthen_pre[OF _ hoare.Do])
apply blast
apply simp
apply (rule hoare.Semi)
apply blast
apply (rule hoare.Conseq)
apply blast
apply blast
apply clarsimp
apply(rule hoare.If)
apply(rule hoare.Conseq)
apply blast
apply simp
apply(rule hoare.Conseq)
apply blast
apply simp
prefer 2
apply simp
apply(rename_tac b c)
apply(rule hoare.Conseq)
apply(rule_tac P = "λz s. (z,s) ∈ ({(s,t). b s ∧ s -c→ t})^*"
in hoare.While)
apply(erule hoare.Conseq)
apply(blast intro:rtrancl_into_rtrancl)
apply clarsimp
apply(rename_tac s t)
apply(erule_tac x = s in allE)
apply clarsimp
apply(erule converse_rtrancl_induct)
apply(blast intro:exec.intros)
apply(fast elim:exec.WhileTrue)

apply(fastforce intro: hoare.Local elim!: hoare.Conseq)
done

lemma MGT_body: "(P, CALL p, Q) = MGT (CALL pa) ⟹ C ⊩ {MGT (body p)} ⟹ C ⊢ {P} body p {Q}"
apply clarsimp
done

declare MGT_def[simp del]

lemma MGT_CALL: "{} ⊩ {mgt. ∃p. mgt = MGT(CALL p)}"
apply (rule hoare.Call)
apply(rule hoare.ConjI)
apply clarsimp
apply (erule MGT_body)
apply(rule MGT_lemma)
apply(unfold MGT_def)
apply(fast intro: hoare.Asm)
done

theorem Complete: "⊨ {P}c{Q}  ⟹  {} ⊢ {P}c{Q::state assn}"
apply(rule MGT_implies_complete)
prefer 2
apply assumption
apply (rule MGT_lemma)
apply(rule allI)
apply(unfold MGT_def)
apply(rule hoare.ConjE[OF MGT_CALL])
done

end


# Theory PsTermi

(*  Title:      Inductive definition of termination
Author:      Tobias Nipkow, 2001/2006
Maintainer:  Tobias Nipkow
*)
theory PsTermi imports PsLang begin

subsection‹Termination›

inductive
termi :: "com ⇒ state ⇒ bool" (infixl "↓" 50)
where
Do[iff]: "f s ≠ {} ⟹ Do f ↓ s"
| Semi[intro!]:   "⟦ c1 ↓ s0; ⋀s1. s0 -c1→ s1 ⟹ c2 ↓ s1 ⟧
⟹ (c1;c2) ↓ s0"

| IfTrue[intro,simp]: "⟦ b s; c1 ↓ s ⟧ ⟹ IF b THEN c1 ELSE c2 ↓ s"
| IfFalse[intro,simp]: "⟦ ¬b s; c2 ↓ s ⟧ ⟹ IF b THEN c1 ELSE c2 ↓ s"

| WhileFalse: "¬b s ⟹ WHILE b DO c ↓ s"

| WhileTrue:  "⟦ b s; c ↓ s; ⋀t. s -c→ t ⟹ WHILE b DO c ↓ t ⟧
⟹ WHILE b DO c ↓ s"

| "body p ↓ s ⟹ CALL p ↓ s"

| Local: "c ↓ f s ⟹ LOCAL f;c;g ↓ s"

lemma [iff]: "(Do f ↓ s) = (f s ≠ {})"
apply(rule iffI)
prefer 2
apply(best intro:termi.intros)
apply(erule termi.cases)
apply blast+
done

lemma [iff]: "((c1;c2) ↓ s0) = (c1 ↓ s0 ∧ (∀s1. s0 -c1→ s1 ⟶ c2 ↓ s1))"
apply(rule iffI)
prefer 2
apply(best intro:termi.intros)
apply(erule termi.cases)
apply blast+
done

lemma [iff]: "(IF b THEN c1 ELSE c2 ↓ s) =
((if b s then c1 else c2) ↓ s)"
apply simp
apply(rule conjI)
apply(rule impI)
apply(rule iffI)
prefer 2
apply(blast intro:termi.intros)
apply(erule termi.cases)
apply blast+
apply(rule impI)
apply(rule iffI)
prefer 2
apply(blast intro:termi.intros)
apply(erule termi.cases)
apply blast+
done

lemma [iff]: "(CALL p ↓ s) = (body p ↓ s)"
by(fast elim: termi.cases intro:termi.intros)

lemma [iff]: "(LOCAL f;c;g ↓ s) = (c ↓ f s)"
by(fast elim: termi.cases intro:termi.intros)

lemma termi_while_lemma[rule_format]:
"w↓fk ⟹
(∀k b c. fk = f k ∧ w = WHILE b DO c ∧ (∀i. f i -c→ f(Suc i))
⟶ (∃i. ¬b(f i)))"
apply(erule termi.induct)
apply simp_all
apply blast
apply blast
done

lemma termi_while:
"⟦ (WHILE b DO c) ↓ f k;  ∀i. f i -c→ f(Suc i) ⟧ ⟹ ∃i. ¬b(f i)"
by(blast intro:termi_while_lemma)

lemma wf_termi: "wf {(t,s). WHILE b DO c ↓ s ∧ b s ∧ s -c→ t}"
apply(subst wf_iff_no_infinite_down_chain)
apply(rule notI)
apply clarsimp
apply(insert termi_while)
apply blast
done

end


# Theory PsHoareTotal

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

theory PsHoareTotal imports PsHoare PsTermi begin

subsection‹Hoare logic for total correctness›

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
valids :: "'a cntxt ⇒ bool" ("|⊨⇩t _" 50) where
"|⊨⇩t D ⟷ (∀(P,c,Q) ∈ D. ⊨⇩t {P}c{Q})"

definition
ctvalid :: "'a cntxt ⇒ 'a assn ⇒ com ⇒ 'a assn ⇒ bool"
("(_ /⊨⇩t {(1_)}/ (_)/ {(1_))}" 50) where
"C ⊨⇩t {P}c{Q} ⟷ |⊨⇩t C ⟶  ⊨⇩t {P}c{Q}"

definition
cvalids :: "'a cntxt ⇒ 'a cntxt ⇒ bool" ("_ |⊨⇩t/ _" 50) where
"C |⊨⇩t D ⟷ |⊨⇩t C ⟶ |⊨⇩t D"

inductive
thoare :: "'a cntxt ⇒ 'a cntxt ⇒ bool" ("(_ |⊢⇩t/ _)" 50)
and thoare' :: "'a cntxt ⇒ 'a assn ⇒ com ⇒ 'a assn ⇒ bool"
("(_ ⊢⇩t/ ({(1_)}/ (_)/ {(1_)}))" [50,0,0,0] 50)
where
"C ⊢⇩t {P}c{Q}  ≡  C |⊢⇩t {(P,c,Q)}"
| 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;
∀q pre.
(⋃p. {(λz s. P p z s ∧ ((p,s),(q,pre)) ∈ r,CALL p,Q p)})
⊢⇩t {λz s. P q z s ∧ s = pre} body q {Q q} ⟧
⟹ {} |⊢⇩t ⋃p. {(P p, CALL p, Q p)}"

| Asm: "(P,CALL p,Q) ∈ C ⟹ C ⊢⇩t {P} CALL p {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}"

| ConjI: "∀(P,c,Q) ∈ D. C ⊢⇩t {P}c{Q}  ⟹  C |⊢⇩t D"
| ConjE: "⟦ C |⊢⇩t D; (P,c,Q) ∈ D ⟧ ⟹ 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}"
monos split_beta

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 valids_def cvalids_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 p{Q}) = (⊨⇩t {P}body p{Q})"
apply(unfold tvalid_defs)
apply fast
done

lemma 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:if_split_asm)

theorem "C |⊢⇩t D  ⟹  C |⊨⇩t D"
apply(erule thoare.induct)
apply(simp only:tvalid_defs)
apply fast
apply fast
apply(simp only:tvalid_defs)
apply clarsimp
prefer 3
apply fast
prefer 3
apply blast
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

defer

apply fast

apply fast

apply fast

apply(rule allI)
apply(rename_tac q)
apply(subgoal_tac "∀pre. ⊨⇩t {λz s. P (fst(q,pre)) z s & s=(snd(q,pre))} body (fst(q,pre)) {Q (fst(q,pre))}")
apply fast
apply(rule allI)
apply(erule_tac wf_induct)
apply(rename_tac q pre)
apply(erule allE, erule allE, erule conjE, erule impE)
prefer 2
apply assumption
apply(rotate_tac 1, erule thin_rl)
apply(unfold tvalid_defs)
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(unfold MGT⇩t_def)
apply (erule thoare.Conseq)
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: "∀p. {} |⊢⇩t {MGT⇩t(CALL p)}  ⟹  {} |⊢⇩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(erule exec.WhileFalse)
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 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) 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)+
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 del:fun_upd_apply)
apply blast
apply(blast intro:exec.WhileFalse)
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 :: "((pname × state) × (pname × state))set" where
"termi_call_steps =
{((q,t),(p,s)). body p↓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 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)
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(rule_tac x = "λi. case i of 0 ⇒ ((WHILE b DO c)#cs,s) | Suc i ⇒ f i" in exI)
done

lemma [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 clarsimp
apply clarsimp
apply(rule_tac x = "λi. case i of 0 ⇒ (CALL p#cs,s) | Suc i ⇒ f i" in exI)
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)
done

lemma exec1_only1_aux: "(ccs,s) → (cs',t) ⟹
∀c cs. ccs = c#cs ⟶ (∃cs1. cs' = cs1 @ cs)"
apply(erule exec1.induct)
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(drule exec1_only1)
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)
done

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

lemma CALL_lemma:
"(⋃p. {(λz s. (z=s ∧ body p↓s) ∧ ((p,s),(q,pre)) ∈ termi_call_steps, CALL p,
λz s. z -body p→ s)}) ⊢⇩t
{λz s. (z=s ∧ body q↓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↓pre & (∃cs. ([body q], pre) →⇧* (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→ 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↓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)
done

lemma CALL_cor:
"(⋃p. {(λz s. (z=s ∧ body p↓s) ∧ ((p,s),(q,pre)) ∈ termi_call_steps, CALL p,
λz s. z -body p→ s)}) ⊢⇩t
{λz s. (z=s ∧ body q↓s) ∧ s = pre} body q {λz s. z -body q→ s}"
apply(rule strengthen_pre[OF _ CALL_lemma])
apply blast
done

lemma MGT_CALL: "{} |⊢⇩t (⋃p. {MGT⇩t(CALL p)})"
apply(rule thoare.Call)
apply(rule wf_termi_call_steps)
apply clarify
apply(rule CALL_cor)
done

lemma MGT_CALL1: "∀p. {} |⊢⇩t {MGT⇩t(CALL p)}"
by(fastforce intro:MGT_CALL[THEN ConjE])

theorem "{} ⊨⇩t {P}c{Q}  ⟹  {} ⊢⇩t {P}c{Q::state assn}"
apply(erule MGT_implies_complete[OF MGT_lemma[OF MGT_CALL1]])
done

end