Session Abstract-Hoare-Logics

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"c1;c2"} \qquad @{term"IF b THEN c1 ELSE c2"}
 \qquad @{term"WHILE b DO c"}
\end{center}
instead of @{term[source]"Semi c1 c2"}, @{term[source]"Cond b c1 c2"}
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 (c1;c2) R = wp c1 (wp c2 R)"
apply(unfold wp_def)
apply(rule ext)
apply blast
done

lemma [simp]:
 "wp (IF b THEN c1 ELSE c2) Q = (λs. wp (if b s then c1 else c2) 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(simp add:unfold_while)
apply(blast intro:exec.intros)
apply(simp add:unfold_while)
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!]:(*>*) " c1  s0; s1. s0 -c1 s1  c2  s1   (c1;c2)  s0"

| (*<*)IfT[intro,simp]:(*>*) "  b s; c1  s   IF b THEN c1 ELSE c2  s"
| (*<*)IfF[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"

| (*<*)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]: "(LOCAL f;c;g  s) = (c  f s)"
by(fast elim: termi.cases intro:termi.intros)

lemma termi_while_lemma[rule_format]:
 "wfk 
 (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  cs)"

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" ("wpt") where
  "wpt c Q = (λs. wp c Q s  cs)"

lemmas wp_defs = wp_def wpt_def

lemma [simp]: "wpt (Do f) Q = (λs. (t  f s. Q t)  f s  {})"
by(simp add: wpt_def)

lemma [simp]: "wpt (c1;c2) R = wpt c1 (wpt c2 R)"
apply(unfold wp_defs)
apply(rule ext)
apply blast
done

lemma [simp]:
 "wpt (IF b THEN c1 ELSE c2) Q = (λs. wpt (if b s then c1 else c2) Q s)"
apply(unfold wp_defs)
apply(rule ext)
apply auto
done

lemma [simp]: "wpt (LOCAL f;c;g) Q = (λs. wpt 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 {wpt 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 (simp add:wp_defs unfold_while)
apply(rule allI)
apply(rule strengthen_pre)
 prefer 2
 apply fast
apply(clarsimp simp add: wp_defs)
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(simp add:execn.intros)
    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 intro:exec.intros exec_mono simp add:max_def)
         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(fastforce elim:execn.WhileTrue exec_mono simp add:max_def)
     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(simp add: MGT_def)
apply (erule hoare.Conseq)
apply(simp add: valid_defs)
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(simp add: MGT_def)
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]:
 "wfk 
 (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  cs)"

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


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

| Call:
  "wf r;  s'. {(λz s. P z s  (s,s')  r, CALL, Q)}
                 t {λz s. P z s  s = s'} body {Q}
    {} t {P} CALL {Q}"

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

| Conseq:
  " C t {P'}c{Q'};
     (s t. (z. P' z s  Q' z t)  (z. P z s  Q z t)) 
     (s. (z. P z s)  (z. P' z s)) 
    C t {P}c{Q}"

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

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


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

lemma "((s t. (z. P' z s  Q' z t)  (z. P z s  Q z t)) 
            (s. (z. P z s)  (z. P' z s)))
        = (z s. P z s  (t.z'. P' z' s  (Q' z' t  Q z t)))"
by blast

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

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

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


lemmas tvalid_defs = tvalid_def ctvalid_def valid_defs

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

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

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

theorem "C t {P}c{Q}    C t {P}c{Q}"
apply(erule thoare.induct)
       apply(simp only:tvalid_defs)
       apply fast
      apply(simp only:tvalid_defs)
      apply fast
     apply(simp only:tvalid_defs)
     apply clarsimp
    prefer 3
    apply(simp add:tvalid_defs)
   prefer 3
   apply(simp only:tvalid_defs)
   apply blast
  apply(simp only:tvalid_defs)
  apply(rule impI, rule conjI)
   apply(rule allI)
   apply(erule wf_induct)
   apply clarify
   apply(drule unfold_while[THEN iffD1])
   apply (simp split: if_split_asm)
   apply fast
  apply(rule allI, rule allI)
  apply(erule wf_induct)
  apply clarify
  apply(case_tac "b x")
   prefer 2
   apply (erule termi.WhileFalse)
  apply(rule termi.WhileTrue, assumption)
   apply fast
  apply (subgoal_tac "(t,x):r")
   apply fast
  apply blast
 apply(simp (no_asm_use) add:ctvalid_def)
 apply(subgoal_tac "n. t {λz s. P z s  s=n} body {Q}")
  apply(simp (no_asm_use) add:tvalid_defs)
  apply blast
 apply(rule allI)
 apply(erule wf_induct)
 apply(unfold tvalid_defs)
 apply fast
apply fast
done


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

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

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

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

lemma MGT_lemma: "C t MGTt CALL  C t MGTt c"
apply (simp)
apply(induct_tac c)
     apply (rule strengthen_pre[OF _ thoare.Do])
     apply blast
    apply(rename_tac com1 com2)
    apply(rule_tac Q = "λz s. z -com1s & com2s" in thoare.Semi)
     apply(erule thoare.Conseq)
     apply fast
    apply(erule thoare.Conseq)
    apply fast
   apply(rule thoare.If)
    apply(erule thoare.Conseq)
    apply simp
   apply(erule thoare.Conseq)
   apply simp
  defer
  apply simp
 apply(fast intro:thoare.Local elim!: thoare.Conseq)
apply(rename_tac b c)
apply(rule_tac P' = "λz s. (z,s)  ({(s,t). b s  s -c t})^* 
                           WHILE b DO c  s" in thoare.Conseq)
 apply(rule_tac thoare.While[OF wf_termi])
 apply(rule allI)
 apply(erule thoare.Conseq)
 apply(fastforce intro:rtrancl_into_rtrancl dest:while_termiE while_termiE2)
apply(rule conjI)
 apply clarsimp
 apply(erule_tac x = s in allE)
 apply clarsimp
 apply(erule converse_rtrancl_induct)
  apply simp
 apply(fast elim:exec.WhileTrue)
apply(fast intro: rtrancl_refl)
done


inductive_set
  exec1 :: "((com list × state) × (com list × state))set"
  and exec1' :: "(com list × state)  (com list × state)  bool"  ("_  _" [81,81] 100)
where
  "cs0  cs1  (cs0,cs1) : exec1"

| Do[iff]: "t  f s  ((Do f)#cs,s)  (cs,t)"

| Semi[iff]: "((c1;c2)#cs,s)  (c1#c2#cs,s)"

| IfTrue:   "b s  ((IF b THEN c1 ELSE c2)#cs,s)  (c1#cs,s)"
| IfFalse: "¬b s  ((IF b THEN c1 ELSE c2)#cs,s)  (c2#cs,s)"

| WhileFalse: "¬b s  ((WHILE b DO c)#cs,s)  (cs,s)"
| WhileTrue:   "b s  ((WHILE b DO c)#cs,s)  (c#(WHILE b DO c)#cs,s)"

| Call[iff]: "(CALL#cs,s)  (body#cs,s)"

| Local[iff]: "((LOCAL f;c;g)#cs,s)  (c # Do(λt. {g s t})#cs, f s)"

abbreviation
  exectr :: "(com list × state)  (com list × state)  bool"   ("_ * _" [81,81] 100)
  where "cs0 * cs1  (cs0,cs1) : exec1^*"

inductive_cases exec1E[elim!]:
 "([],s)  (cs',s')"
 "(Do f#cs,s)  (cs',s')"
 "((c1;c2)#cs,s)  (cs',s')"
 "((IF b THEN c1 ELSE c2)#cs,s)  (cs',s')"
 "((WHILE b DO c)#cs,s)  (cs',s')"
 "(CALL#cs,s)  (cs',s')"
 "((LOCAL f;c;g)#cs,s)  (cs',s')"

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

lemma app_exec: "(cs,s)  (cs',s')  (cs@cs2,s)  (cs'@cs2,s')"
apply(erule exec1.induct)
       apply(simp_all del:fun_upd_apply)
   apply(blast intro:exec1.intros)+
done

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

lemma exec_impl_execs[rule_format]:
 "s -c s'  cs. (c#cs,s) * (cs,s')"
apply(erule exec.induct)
         apply blast
        apply(blast intro:rtrancl_trans)
       apply(blast intro:exec1.IfTrue rtrancl_trans)
      apply(blast intro:exec1.IfFalse rtrancl_trans)
     apply(blast intro:exec1.WhileFalse rtrancl_trans)
    apply(blast intro:exec1.WhileTrue rtrancl_trans)
   apply(blast intro: rtrancl_trans)
apply(blast intro: rtrancl_trans)
done

inductive
  execs :: "state  com list  state  bool"   ("_/ =_/ _" [50,0,50] 50)
where
  "s =[] s"
| "s -c t  t =cs u  s =c#cs u"

inductive_cases [elim!]:
 "s =[] t"
 "s =c#cs t"

theorem exec1s_impl_execs: "(cs,s) * ([],t)  s =cs t"
apply(erule converse_rtrancl_induct2)
 apply(rule execs.intros)
apply(erule exec1.cases)
apply(blast intro:execs.intros)
apply(blast intro:execs.intros)
apply(fastforce intro:execs.intros)
apply(fastforce intro:execs.intros)
apply(blast intro:execs.intros exec.intros)
apply(blast intro:execs.intros exec.intros)
apply(blast intro:execs.intros exec.intros)
apply(blast intro:execs.intros exec.intros)
done


theorem exec1s_impl_exec: "([c],s) * ([],t)  s -c t"
by(blast dest: exec1s_impl_execs)

primrec termis :: "com list  state  bool" (infixl "" 60) where
  "[]s = True"
| "c#cs  s = (cs  (t. s -c t  cst))"

lemma exec1_pres_termis: "(cs,s)  (cs',s')  css  cs's'"
apply(erule exec1.induct)
       apply(simp_all)
  apply blast
 apply(blast intro:while_termiE while_termiE2 exec.WhileTrue)
apply blast
done

lemma execs_pres_termis: "(cs,s) * (cs',s')  css  cs's'"
apply(erule rtrancl_induct2)
 apply blast
apply(blast dest:exec1_pres_termis)
done

lemma execs_pres_termi: " ([c],s) * (c'#cs',s'); cs   c's'"
apply(insert execs_pres_termis[of "[c]" _ "c'#cs'",simplified])
apply blast
done

definition
 termi_call_steps :: "(state × state)set" where
"termi_call_steps = {(t,s). bodys  (cs. ([body], s) * (CALL # cs, t))}"

lemma lem:
  "y. (a,y)r+  P a  P y  ((b,a)  {(y,x). P x  (x,y):r}+) = ((b,a)  {(y,x). P x  (x,y)r+})"
apply(rule iffI)
 apply clarify
 apply(erule trancl_induct)
  apply blast
 apply(blast intro:trancl_trans)
apply clarify
apply(erule trancl_induct)
 apply blast
apply(blast intro:trancl_trans)
done


lemma renumber_aux:
 "i. (a,f i) : r^*  (f i,f(Suc i)) : r; (a,b) : r^*   b = f 0  (f. f 0 = a & (i. (f i, f(Suc i)) : r))"
apply(erule converse_rtrancl_induct)
 apply blast
apply(clarsimp)
apply(rule_tac x="λi. case i of 0  y | Suc i  fa i" in exI)
apply simp
apply clarify
apply(case_tac i)
 apply simp_all
done

lemma renumber:
 "i. (a,f i) : r^*  (f i,f(Suc i)) : r  f. f 0 = a & (i. (f i, f(Suc i)) : r)"
by(blast dest:renumber_aux)


definition inf :: "com list  state  bool" where
"inf cs s  (f. f 0 = (cs,s)  (i. f i  f(Suc i)))"

lemma [iff]: "¬ inf [] s"
apply(unfold inf_def)
apply clarify
apply(erule_tac x = 0 in allE)
apply simp
done

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

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

lemma [iff]: "inf ((IF b THEN c1 ELSE c2)#cs) s =
              inf ((if b s then c1 else c2)#cs) s"
apply(unfold inf_def)
apply(rule iffI)
 apply clarsimp
 apply(frule_tac x = 0 in spec)
 apply (case_tac "f (Suc 0)")
 apply(rule conjI)
  apply clarsimp
  apply(rule_tac x = "λi. f(Suc i)" in exI)
  apply clarsimp
 apply clarsimp
 apply(rule_tac x = "λi. f(Suc i)" in exI)
 apply clarsimp
apply clarsimp
apply(rule_tac x = "λi. case i of 0  ((IF b THEN c1 ELSE c2)#cs,s) | Suc i  f i" in exI)
apply(simp add: exec1.intros split:nat.split)
done

lemma [simp]:
 "inf ((WHILE b DO c)#cs) s =
  (if b s then inf (c#(WHILE b DO c)#cs) s else inf cs s)"
apply(unfold inf_def)
apply(rule iffI)
 apply clarsimp
 apply(frule_tac x = 0 in spec)
 apply (case_tac "f (Suc 0)")
 apply(rule conjI)
  apply clarsimp
  apply(rule_tac x = "λi. f(Suc i)" in exI)
  apply clarsimp
 apply clarsimp
 apply(rule_tac x = "λi. f(Suc i)" in exI)
 apply clarsimp
apply (clarsimp split:if_splits)
 apply(rule_tac x = "λi. case i of 0  ((WHILE b DO c)#cs,s) | Suc i  f i" in exI)
 apply(simp add: exec1.intros split:nat.split)
apply(rule_tac x = "λi. case i of 0  ((WHILE b DO c)#cs,s) | Suc i  f i" in exI)
apply(simp add: exec1.intros split:nat.split)
done

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

lemma [iff]: "inf ((LOCAL f;c;g)#cs) s =
              inf (c#Do(λt. {g s t})#cs) (f s)"
apply(unfold inf_def)
apply(rule iffI)
 apply clarsimp
 apply(rename_tac F)
 apply(frule_tac x = 0 in spec)
 apply (case_tac "F (Suc 0)")
 apply clarsimp
 apply(rule_tac x = "λi. F(Suc i)" in exI)
 apply clarsimp
apply (clarsimp)
apply(rename_tac F)
apply(rule_tac x = "λi. case i of 0  ((LOCAL f;c;g)#cs,s) | Suc i  F i" in exI)
apply(simp add: exec1.intros split:nat.split)
done

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

lemma exec1_only1: "(c#cs,s)  (cs',t)  cs1. cs' = cs1 @ cs"
by(blast dest:exec1_only1_aux)

lemma exec1_drop_suffix_aux:
"(cs12,s)  (cs1'2,s')  cs1 cs2 cs1'.
 cs12 = cs1@cs2 & cs1'2 = cs1'@cs2 & cs1  []  (cs1,s)  (cs1',s')"
apply(erule exec1.induct)
       apply (force intro:exec1.intros simp add: neq_Nil_conv)+
done

lemma exec1_drop_suffix:
 "(cs1@cs2,s)  (cs1'@cs2,s')  cs1  []  (cs1,s)  (cs1',s')"
by(blast dest:exec1_drop_suffix_aux)

lemma execs_drop_suffix[rule_format(no_asm)]:
  " f 0 = (c#cs,s);i. f(i)  f(Suc i)  
   (i<k. p i  [] & fst(f i) = p i@cs)  fst(f k) = p k@cs
    ([c],s) * (p k,snd(f k))"
apply(induct_tac k)
 apply simp
apply (clarsimp)
apply(erule rtrancl_into_rtrancl)
apply(erule_tac x = n in allE)
apply(erule_tac x = n in allE)
apply(case_tac "f n")
apply(case_tac "f(Suc n)")
apply simp
apply(blast dest:exec1_drop_suffix)
done

lemma execs_drop_suffix0:
  " f 0 = (c#cs,s);i. f(i)  f(Suc i); i<k. p i  [] & fst(f i) = p i@cs;
     fst(f k) = cs; p k = []   ([c],s) * ([],snd(f k))"
apply(drule execs_drop_suffix,assumption,assumption)
 apply simp
apply simp
done

lemma skolemize1: "x. P x  (y. Q x y)  f.x. P x  Q x (f x)"
apply(rule_tac x = "λx. SOME y. Q x y" in exI)
apply(fast intro:someI2)
done

lemma least_aux: "f 0 = (c # cs, s); i. f i  f (Suc i);
        fst(f k) = cs; i<k. fst(f i)  cs
        i  k. (p. (p  []) = (i < k) & fst(f i) = p @ cs)"
apply(rule allI)
apply(induct_tac i)
 apply simp
 apply (rule ccontr)
 apply simp
apply clarsimp
apply(drule order_le_imp_less_or_eq)
apply(erule disjE)
 prefer 2
 apply simp
apply simp
apply(erule_tac x = n in allE)
apply(erule_tac x = "Suc n" in allE)
apply(case_tac "f n")
apply(case_tac "f(Suc n)")
apply simp
apply(rename_tac sn csn1 sn1)
apply (clarsimp simp add: neq_Nil_conv)
apply(drule exec1_only1)
apply (clarsimp simp add: neq_Nil_conv)
apply(erule disjE)
 apply clarsimp
apply clarsimp
apply(case_tac cs1)
 apply simp
apply simp
done

lemma least_lem: "f 0 = (c#cs,s); i. f i  f(Suc i); i. fst(f i) = cs 
        k. fst(f k) = cs & ([c],s) * ([],snd(f k))"
apply(rule_tac x="LEAST i. fst(f i) = cs" in exI)
apply(rule conjI)
 apply(fast intro: LeastI)
apply(subgoal_tac
 "iLEAST i. fst (f i) = cs. p. ((p  []) = (i<(LEAST i. fst (f i) = cs))) & fst(f i) = p@cs")
 apply(drule skolemize1)
 apply clarify
 apply(rename_tac p)
 apply(erule_tac p=p in execs_drop_suffix0, assumption)
   apply (blast dest:order_less_imp_le)
  apply(fast intro: LeastI)
 apply(erule thin_rl)
 apply(erule_tac x = "LEAST j. fst (f j) = fst (f i)" in allE)
 apply blast
apply(erule least_aux,assumption)
 apply(fast intro: LeastI)
apply clarify
apply(drule not_less_Least)
apply blast
done

lemma skolemize2: "x.y. P x y  f.x. P x (f x)"
apply(rule_tac x = "λx. SOME y. P x y" in exI)
apply(fast intro:someI2)
done

lemma inf_cases: "inf (c#cs) s  inf [c] s  (t. s -c t  inf cs t)"
apply(unfold inf_def)
apply (clarsimp del: disjCI)
apply(case_tac "i. fst(f i) = cs")
 apply(rule disjI2)
 apply(drule least_lem, assumption, assumption)
 apply clarify
 apply(drule exec1s_impl_exec)
 apply(case_tac "f k")
 apply simp
 apply (rule exI, rule conjI, assumption)
 apply(rule_tac x="λi. f(i+k)" in exI)
 apply (clarsimp)
apply(rule disjI1)
apply simp
apply(subgoal_tac "i. p. p  []  fst(f i) = p@cs")
 apply(drule skolemize2)
 apply clarify
 apply(rename_tac p)
 apply(rule_tac x = "λi. (p i, snd(f i))" in exI)
 apply(rule conjI)
  apply(erule_tac x = 0 in allE, erule conjE)
  apply simp
 apply clarify
 apply(erule_tac x = i in allE)
 apply(erule_tac x = i in allE)
 apply(frule_tac x = i in spec)
 apply(erule_tac x = "Suc i" in allE)
 apply(case_tac "f i")
 apply(case_tac "f(Suc i)")
 apply clarsimp
 apply(blast intro:exec1_drop_suffix)
apply(clarify)
apply(induct_tac i)
 apply force
apply clarsimp
apply(case_tac p)
 apply blast
apply(erule_tac x=n in allE)
apply(erule_tac x="Suc n" in allE)
apply(case_tac "f n")
apply(case_tac "f(Suc n)")
apply clarsimp
apply(drule exec1_only1)
apply clarsimp
done

lemma termi_impl_not_inf: "c  s  ¬ inf [c] s"
apply(erule termi.induct)
        (*Do*)
        apply clarify
       (*Semi*)
       apply(blast dest:inf_cases)
      (* Cond *)
      apply clarsimp
     apply clarsimp
    (*While*)
    apply clarsimp
   apply(fastforce dest:inf_cases)
  (*Call*)
  apply blast
(*Local*)
apply(blast dest:inf_cases)
done

lemma termi_impl_no_inf_chain:
 "cs  ¬(f. f 0 = ([c],s)  (i::nat. (f i, f(i+1)) : exec1^+))"
apply(subgoal_tac "wf({(y,x). ([c],s) * x & x  y}^+)")
 apply(simp only:wf_iff_no_infinite_down_chain)
 apply(erule contrapos_nn)
 apply clarify
 apply(subgoal_tac "i. ([c], s) * f i")
  prefer 2
  apply(rule allI)
  apply(induct_tac i)
   apply simp
  apply simp
  apply(blast intro: trancl_into_rtrancl rtrancl_trans)
 apply(rule_tac x=f in exI)
 apply clarify
 apply(drule_tac x=i in spec)
 apply(subst lem)
  apply(blast intro: trancl_into_rtrancl rtrancl_trans)
 apply clarsimp
apply(rule wf_trancl)
apply(simp only:wf_iff_no_infinite_down_chain)
apply(clarify)
apply simp
apply(drule renumber)
apply(fold inf_def)
apply(simp add: termi_impl_not_inf)
done

primrec cseq :: "(nat  state)  nat  com list" where
  "cseq S 0 = []"
| "cseq S (Suc i) = (SOME cs. ([body], S i) * (CALL # cs, S(i+1))) @ cseq S i"

lemma wf_termi_call_steps: "wf termi_call_steps"
apply(unfold termi_call_steps_def)
apply(simp only:wf_iff_no_infinite_down_chain)
apply(clarify)
apply(rename_tac S)
apply simp
apply(subgoal_tac "Cs. Cs 0 = [] & (i. (body # Cs i,S i) * (CALL # Cs(i+1), S(i+1)))")
prefer 2
 apply(rule_tac x = "cseq S" in exI)
 apply clarsimp
 apply(erule_tac x=i in allE)
 apply(clarify)
 apply(erule_tac P = "λcs.([body],S i) * (CALL # cs, S(Suc i))" in someI2)
 apply(fastforce dest:app_execs)
apply clarify
apply(subgoal_tac "i. ((body # Cs i,S i), (body # Cs(i+1), S(i+1))) : exec1^+")
 prefer 2
 apply(blast intro:rtrancl_into_trancl1)
apply(subgoal_tac "f. f 0 = ([body],S 0)  (i. (f i, f(i+1)) : exec1^+)")
 prefer 2
 apply(rule_tac x = "λi.(body#Cs i,S i)" in exI)
 apply blast
apply(blast dest:termi_impl_no_inf_chain)
done

lemma CALL_lemma:
"{(λz s. (z=s  bodys)  (s,t)  termi_call_steps, CALL, λz s. z -body s)} t
 {λz s. (z=s  bodyt)  (cs. ([body],t) * (c#cs,s))} c {λz s. z -c s}"
apply(induct_tac c)
(*Do*)
     apply (rule strengthen_pre[OF _ thoare.Do])
     apply(blast dest: execs_pres_termi)
(*Semi*)
    apply(rename_tac c1 c2)
    apply(rule_tac Q = "λz s. bodyt & (cs. ([body], t) * (c2#cs,s)) & z -c1s & c2s" in thoare.Semi)
     apply(erule thoare.Conseq)
     apply(rule conjI)
      apply clarsimp
      apply(subgoal_tac "s -c1 ta")
       prefer 2
       apply(blast intro: exec1.Semi exec_impl_execs rtrancl_trans)
      apply(subgoal_tac "([body], t) * (c2 # cs, ta)")
       prefer 2
       apply(blast intro:exec1.Semi[THEN r_into_rtrancl] exec_impl_execs rtrancl_trans)
      apply(subgoal_tac "([body], t) * (c2 # cs, ta)")
       prefer 2
       apply(blast intro: exec_impl_execs rtrancl_trans)
      apply(blast intro:exec_impl_execs rtrancl_trans execs_pres_termi)
     apply(fast intro: exec1.Semi rtrancl_trans)
    apply(erule thoare.Conseq)
    apply blast
(*Call*)
   prefer 3
   apply(simp only:termi_call_steps_def)
   apply(rule thoare.Conseq[OF thoare.Asm])
   apply(blast dest: execs_pres_termi)
(*If*)
  apply(rule thoare.If)
   apply(erule thoare.Conseq)
   apply simp
   apply(blast intro: exec1.IfTrue rtrancl_trans)
  apply(erule thoare.Conseq)
  apply simp
  apply(blast intro: exec1.IfFalse rtrancl_trans)
(*Var*)
 defer
 apply simp
 apply(rule thoare.Local)
 apply(rule allI)
 apply(erule thoare.Conseq)
 apply (clarsimp)
 apply(rule conjI)
  apply (clarsimp)
  apply(drule rtrancl_trans[OF _ r_into_rtrancl[OF exec1.Local]])
  apply(fast)
 apply (clarsimp)
 apply(drule rtrancl_trans[OF _ r_into_rtrancl[OF exec1.Local]])
 apply blast
apply(rename_tac b c)
apply(rule_tac P' = "λz s. (z,s)  ({(s,t). b s  s -c t})^*  body  t 
           (cs. ([body], t) * ((WHILE b DO c) # cs, s))" in thoare.Conseq)
 apply(rule_tac thoare.While[OF wf_termi])
 apply(rule allI)
 apply(erule thoare.Conseq)
 apply clarsimp
 apply(rule conjI)
  apply clarsimp
  apply(rule conjI)
   apply(blast intro: rtrancl_trans exec1.WhileTrue)
  apply(rule conjI)
   apply(rule exI, rule rtrancl_trans, assumption)
   apply(blast intro: exec1.WhileTrue exec_impl_execs rtrancl_trans)
  apply(rule conjI)
   apply(blast intro:execs_pres_termi)
  apply(blast intro: exec1.WhileTrue exec_impl_execs rtrancl_trans)
 apply(blast intro: exec1.WhileTrue exec_impl_execs rtrancl_trans)
apply(rule conjI)
 apply clarsimp
 apply(erule_tac x = s in allE)
 apply clarsimp
 apply(erule impE)
  apply blast
 apply clarify
 apply(erule_tac a=s in converse_rtrancl_induct)
  apply simp
 apply(fast elim:exec.WhileTrue)
apply(fast intro: rtrancl_refl)
done

lemma CALL_cor:
"{(λz s. (z=s  bodys)  (s,t)  termi_call_steps, CALL, λz s. z -body s)} t
 {λz s. (z=s  bodys)  s = t} body {λz s. z -body s}"
apply(rule strengthen_pre[OF _ CALL_lemma])
apply blast
done

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


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

end

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(simp add:execn.intros)
  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 intro:exec.intros exec_mono simp add:max_def)
      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(fastforce elim:execn.WhileTrue exec_mono simp add:max_def)
  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)
apply(simp add: valid_defs)
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(fastforce simp add:MGT_def)
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])
apply(simp add:MGT_def fun_eq_iff)
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]:
 "wfk 
 (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  cs)"

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(simp add:tvalid_defs)
      apply fast
     apply(simp only:tvalid_defs)
     apply clarsimp
    prefer 3
    apply(simp add:tvalid_defs)
    apply fast
   prefer 3
   apply(simp add:tvalid_defs)
   apply blast
  apply(simp add:tvalid_defs)
  apply(rule impI, rule conjI)
   apply(rule allI)
   apply(erule wf_induct)
   apply clarify
   apply(drule unfold_while[THEN iffD1])
   apply (simp split: 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(simp add:tvalid_defs)
apply fast

apply(simp (no_asm_use) add:tvalid_defs)
apply fast

apply(simp add:tvalid_defs)
apply fast

apply(simp (no_asm_use) add:valids_def ctvalid_def cvalids_def)
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(simp (no_asm_use) add:tvalid_defs)
 apply fast
apply(rule allI)
apply(erule_tac wf_induct)
apply(simp add:split_paired_all)
apply(rename_tac q pre)
apply(erule allE, erule allE, erule conjE, erule impE)
 prefer 2
 apply assumption
apply(rotate_tac 1, erule thin_rl)
apply(unfold tvalid_defs)
apply fast
done

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

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

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

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

lemma MGT_lemma: "p. {} |⊢t {MGTt(CALL p)}    {} |⊢t {MGTt c}"
apply (simp)
apply(induct_tac c)
     apply (rule strengthen_pre[OF _ thoare.Do])
     apply blast
    apply(rename_tac com1 com2)
    apply(rule_tac Q = "λz s. z -com1s & com2s" in thoare.Semi)
     apply(erule thoare.Conseq)
     apply fast
    apply(erule thoare.Conseq)
    apply fast
   apply(rule thoare.If)
    apply(erule thoare.Conseq)
    apply simp
   apply(erule thoare.Conseq)
   apply simp
  defer
  apply simp
 apply(fast intro:thoare.Local elim!: thoare.Conseq)
apply(rename_tac b c)
apply(rule_tac P' = "λz s. (z,s)  ({(s,t). b s  s -c t})^* 
                           WHILE b DO c  s" in thoare.Conseq)
 apply(rule_tac thoare.While[OF wf_termi])
 apply(rule allI)
 apply(erule thoare.Conseq)
 apply(fastforce intro:rtrancl_into_rtrancl dest:while_termiE while_termiE2)
apply(rule conjI)
 apply clarsimp
 apply(erule_tac x = s in allE)
 apply clarsimp
 apply(erule converse_rtrancl_induct)
  apply(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 = (cs  (t. s -c t  cst))"

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

lemma execs_pres_termi: " ([c],s) * (c'#cs',s'); cs   c's'"
apply(insert execs_pres_termis[of "[c]" _ "c'#cs'",simplified])
apply blast
done

definition  termi_call_steps :: "((pname × state) × (pname × state))set" where
  "termi_call_steps =
    {((q,t),(p,s)). body ps  (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)
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 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)
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 force+
done

lemma exec1_only1: "(c#cs,s)  (cs',t)  cs1. cs' = cs1 @ cs"
by(blast dest:exec1_only1_aux)

lemma exec1_drop_suffix_aux:
"(cs12,s)  (cs1'2,s')  cs1 cs2 cs1'.
 cs12 = cs1@cs2 & cs1'2 = cs1'@cs2 & cs1  []  (cs1,s)  (cs1',s')"
apply(erule exec1.induct)
       apply (force intro:exec1.intros simp add: neq_Nil_conv)+
done

lemma exec1_drop_suffix:
 "(cs1@cs2,s)  (cs1'@cs2,s')  cs1  []  (cs1,s)  (cs1',s')"
by(blast dest:exec1_drop_suffix_aux)

lemma execs_drop_suffix[rule_format(no_asm)]:
  " f 0 = (c#cs,s);i. f(i)  f(Suc i)  
   (i<k. p i  [] & fst(f i) = p i@cs)  fst(f k) = p k@cs
    ([c],s) * (p k,snd(f k))"
apply(induct_tac k)
 apply simp
apply (clarsimp)
apply(erule rtrancl_into_rtrancl)
apply(erule_tac x = n in allE)
apply(erule_tac x = n in allE)
apply(case_tac "f n")
apply(case_tac "f(Suc n)")
apply simp
apply(blast dest:exec1_drop_suffix)
done

lemma execs_drop_suffix0:
  " f 0 = (c#cs,s);i. f(i)  f(Suc i); i<k. p i  [] & fst(f i) = p i@cs;
     fst(f k) = cs; p k = []   ([c],s) * ([],snd(f k))"
apply(drule execs_drop_suffix,assumption,assumption)
 apply simp
apply simp
done

lemma skolemize1: "x. P x  (y. Q x y)  f.x. P x  Q x (f x)"
apply(rule_tac x = "λx. SOME y. Q x y" in exI)
apply(fast intro:someI2)
done

lemma least_aux: "f 0 = (c # cs, s); i. f i  f (Suc i);
        fst(f k) = cs; i<k. fst(f i)  cs
        i  k. (p. (p  []) = (i < k) & fst(f i) = p @ cs)"
apply(rule allI)
apply(induct_tac i)
 apply simp
 apply (rule ccontr)
 apply simp
apply clarsimp
apply(drule order_le_imp_less_or_eq)
apply(erule disjE)
 prefer 2
 apply simp
apply simp
apply(erule_tac x = n in allE)
apply(erule_tac x = "Suc n" in allE)
apply(case_tac "f n")
apply(case_tac "f(Suc n)")
apply simp
apply(rename_tac sn csn1 sn1)
apply (clarsimp simp add: neq_Nil_conv)
apply(drule exec1_only1)
apply (clarsimp simp add: neq_Nil_conv)
apply(erule disjE)
 apply clarsimp
apply clarsimp
apply(case_tac cs1)
 apply simp
apply simp
done

lemma least_lem: "f 0 = (c#cs,s); i. f i  f(Suc i); i. fst(f i) = cs 
        k. fst(f k) = cs & ([c],s) * ([],snd(f k))"
apply(rule_tac x="LEAST i. fst(f i) = cs" in exI)
apply(rule conjI)
 apply(fast intro: LeastI)
apply(subgoal_tac
 "iLEAST i. fst (f i) = cs. p. ((p  []) = (i<(LEAST i. fst (f i) = cs))) & fst(f i) = p@cs")
 apply(drule skolemize1)
 apply clarify
 apply(rename_tac p)
 apply(erule_tac p=p in execs_drop_suffix0, assumption)
   apply (blast dest:order_less_imp_le)
  apply(fast intro: LeastI)
 apply(erule thin_rl)
 apply(erule_tac x = "LEAST j. fst (f j) = fst (f i)" in allE)
 apply blast
apply(erule least_aux,assumption)
 apply(fast intro: LeastI)
apply clarify
apply(drule not_less_Least)
apply blast
done

lemma skolemize2: "x.y. P x y  f.x. P x (f x)"
apply(rule_tac x = "λx. SOME y. P x y" in exI)
apply(fast intro:someI2)
done

lemma inf_cases: "inf (c#cs) s  inf [c] s  (t. s -c t  inf cs t)"
apply(unfold inf_def)
apply (clarsimp del: disjCI)
apply(case_tac "i. fst(f i) = cs")
 apply(rule disjI2)
 apply(drule least_lem, assumption, assumption)
 apply clarify
 apply(drule exec1s_impl_exec)
 apply(case_tac "f k")
 apply simp
 apply (rule exI, rule conjI, assumption)
 apply(rule_tac x="λi. f(i+k)" in exI)
 apply (clarsimp)
apply(rule disjI1)
apply simp
apply(subgoal_tac "i. p. p  []  fst(f i) = p@cs")
 apply(drule skolemize2)
 apply clarify
 apply(rename_tac p)
 apply(rule_tac x = "λi. (p i, snd(f i))" in exI)
 apply(rule conjI)
  apply(erule_tac x = 0 in allE, erule conjE)
  apply simp
 apply clarify
 apply(erule_tac x = i in allE)
 apply(erule_tac x = i in allE)
 apply(frule_tac x = i in spec)
 apply(erule_tac x = "Suc i" in allE)
 apply(case_tac "f i")
 apply(case_tac "f(Suc i)")
 apply clarsimp
 apply(blast intro:exec1_drop_suffix)
apply(clarify)
apply(induct_tac i)
 apply force
apply clarsimp
apply(case_tac p)
 apply blast
apply(erule_tac x=n in allE)
apply(erule_tac x="Suc n" in allE)
apply(case_tac "f n")
apply(case_tac "f(Suc n)")
apply clarsimp
apply(drule exec1_only1)
apply clarsimp
done

lemma termi_impl_not_inf: "c  s  ¬ inf [c] s"
apply(erule termi.induct)
        (*Do*)
        apply clarify
       (*Semi*)
       apply(blast dest:inf_cases)
      (* Cond *)
      apply clarsimp
     apply clarsimp
    (*While*)
    apply clarsimp
   apply(fastforce dest:inf_cases)
  (*Call*)
  apply blast
 (*Local*)
 apply(blast dest:inf_cases)
done

lemma termi_impl_no_inf_chain:
 "cs  ¬(f. f 0 = ([c],s)  (i::nat. (f i, f(i+1)) : exec1^+))"
apply(subgoal_tac "wf({(y,x). ([c],s) * x & x  y}^+)")
 apply(simp only:wf_iff_no_infinite_down_chain)
 apply(erule contrapos_nn)
 apply clarify
 apply(subgoal_tac "i. ([c], s) * f i")
  prefer 2
  apply(rule allI)
  apply(induct_tac i)
   apply simp
  apply simp
  apply(blast intro: trancl_into_rtrancl rtrancl_trans)
 apply(rule_tac x=f in exI)
 apply clarify
 apply(drule_tac x=i in spec)
 apply(subst lem)
  apply(blast intro: trancl_into_rtrancl rtrancl_trans)
 apply clarsimp
apply(rule wf_trancl)
apply(simp only:wf_iff_no_infinite_down_chain)
apply(clarify)
apply simp
apply(drule renumber)
apply(fold inf_def)
apply(simp add: termi_impl_not_inf)
done

primrec cseq :: "(nat  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(simp add:split_def)
apply clarify
apply(drule termi_impl_no_inf_chain)
apply simp
apply blast
done

lemma CALL_lemma:
"(p. {(λz s. (z=s  body ps)  ((p,s),(q,pre))  termi_call_steps, CALL p,
        λz s. z -body p s)}) t
 {λz s. (z=s  body qpre)  (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 qpre & (cs. ([body q], pre) * (c2#cs,s)) & z -c1s & c2s" 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 qpre 
           (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 ps)  ((p,s),(q,pre))  termi_call_steps, CALL p,
        λz s. z -body p s)}) t
 {λz s. (z=s  body qs)  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. {MGTt(CALL p)})"
apply(simp add: MGTt_def)
apply(rule thoare.Call)
apply(rule wf_termi_call_steps)
apply clarify
apply(rule CALL_cor)
done

lemma MGT_CALL1: "p. {} |⊢t {MGTt(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