# Theory PHoare

Up to index of Isabelle/HOL/Abstract-Hoare-Logics

theory PHoare
imports PLang
(*  Title:       Inductive definition of Hoare logic    Author:      Tobias Nipkow, 2001/2006    Maintainer:  Tobias Nipkow*)theory PHoare imports PLang beginsubsection{* Hoare logic for partial correctness *}text{*Taking auxiliary variables seriously means that assertions mustnow depend on them as well as on the state. Initially we do not fixthe type of auxiliary variables but parameterize the type ofassertions with a type variable @{typ 'a}:*}type_synonym 'a assn = "'a => state => bool"text{*The second major change is the need to reason about Hoaretriples in a context: proofs about recursive procedures are conductedby induction where we assume that all @{term CALL}s satisfy the givenpre/postconditions and have to show that the body does as well. Theassumption 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 willalways be empty or a singleton set. With multiple procedures, largersets can arise.Now that we have contexts, validity becomes more complicated. Ordinaryvalidity (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" ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" 50) where     "\<Turnstile> {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 definedas follows:*}definition valids :: "'a cntxt => bool" ("|\<Turnstile> _" 50) where  [simp]: "|\<Turnstile> C ≡ (∀(P,c,Q) ∈ C. \<Turnstile> {P}c{Q})"definition cvalid :: "'a cntxt => 'a assn => com => 'a assn => bool" ("_ \<Turnstile>/ {(1_)}/ (_)/ {(1_)}" 50) where  "C \<Turnstile> {P}c{Q} <-> |\<Turnstile> C --> \<Turnstile> {P}c{Q}"text{*\noindent Note that @{prop"{} \<Turnstile> {P}c{Q}"} is equivalent to@{prop"\<Turnstile> {P}c{Q}"}.Unfortunately, this is not the end of it. As we have twosemantics, @{text"-c->"} and @{text"-c-n->"}, we also need a second notionof validity parameterized with the recursion depth @{term n}:*}definition nvalid :: "nat => 'a assn => com => 'a assn => bool" ("\<Turnstile>_ {(1_)}/ (_)/ {(1_)}" 50) where  "\<Turnstile>n {P}c{Q} ≡ (∀s t. s -c-n-> t --> (∀z. P z s --> Q z t))"definition nvalids :: "nat => 'a cntxt => bool" ("|\<Turnstile>'__/ _" 50) where  "|\<Turnstile>_n C ≡ (∀(P,c,Q) ∈ C. \<Turnstile>n {P}c{Q})"definition cnvalid :: "'a cntxt => nat => 'a assn => com => 'a assn => bool" ("_ \<Turnstile>_/ {(1_)}/ (_)/ {(1_)}" 50) where  "C \<Turnstile>n {P}c{Q} <-> |\<Turnstile>_n C --> \<Turnstile>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" ("_ \<turnstile>/ ({(1_)}/ (_)/ {(1_)})" 50)where   (*<*)Do:(*>*)"C \<turnstile> {λz s. ∀t ∈ f s . P z t} Do f {P}" | (*<*)Semi:(*>*)"[| C \<turnstile> {P}c1{Q}; C \<turnstile> {Q}c2{R} |] ==> C \<turnstile> {P} c1;c2 {R}" | (*<*)If:(*>*)"[| C \<turnstile> {λz s. P z s ∧ b s}c1{Q};  C \<turnstile> {λz s. P z s ∧ ¬b s}c2{Q}  |]   ==> C \<turnstile> {P} IF b THEN c1 ELSE c2 {Q}" | (*<*)While:(*>*)"C \<turnstile> {λz s. P z s ∧ b s} c {P}   ==> C \<turnstile> {P} WHILE b DO c {λz s. P z s ∧ ¬b s}" | (*<*)Conseq:(*>*)"[| C \<turnstile> {P'}c{Q'};  ∀s t. (∀z. P' z s --> Q' z t) --> (∀z. P z s --> Q z t) |]   ==> C \<turnstile> {P}c{Q}" | (*<*)Call:(*>*)"{(P,CALL,Q)} \<turnstile> {P}body{Q} ==> {} \<turnstile> {P} CALL {Q}" | (*<*)Asm:(*>*)"{(P,CALL,Q)} \<turnstile> {P} CALL {Q}" | (*<*)Local:(*>*) "[| ∀s'. C \<turnstile> {λz s. P z s' ∧ s = f s'} c {λz t. Q z (g s' t)} |] ==>        C \<turnstile> {P} LOCAL f;c;g {Q}"abbreviation hoare1 :: "'a cntxt => 'a assn × com × 'a assn => bool" ("_ \<turnstile> _") where  "C \<turnstile> x ≡ C \<turnstile> {fst x}fst (snd x){snd (snd x)}"text{*\noindent The first four rules are familiar, except for their adaptationto auxiliary variables. The @{term CALL} rule embodies induction andhas already been motivated above. Note that it is only applicable ifthe context is empty. This shows that we never need nested induction.For the same reason the assumption rule (the last rule) is stated withjust 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\<turnstile> {P}c{Q}  |] ==> C\<turnstile> {P'}c{Q}"by(rule hoare.Conseq, assumption, blast)lemmas valid_defs = valid_def valids_def cvalid_def                    nvalid_def nvalids_def cnvalid_deftheorem hoare_sound: "C \<turnstile> {P}c{Q}  ==>  C \<Turnstile> {P}c{Q}"txt{*\noindent requires a generalization: @{prop"∀n. C \<Turnstile>n{P}c{Q}"} is proved instead, from which the actual theorem followsdirectly via lemma @{thm[source]exec_iff_execn} in \S\ref{sec:proc1-lang}.The generalizationis proved by induction on @{term c}. The reason for the generalizationis that soundness of the @{term CALL} rule is proved by induction on themaximal call depth, i.e.\ @{term n}.*}apply(subgoal_tac "∀n. C \<Turnstile>n {P}c{Q}")apply(unfold valid_defs exec_iff_execn) apply fastapply(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 blastapply autodonetext{*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 auxiliaryvariable, which is simply there to record the value of the program variablesbefore execution of a command. This is exactly what, for example, VDM offersby allowing you to refer to the pre-value of a variable in apostcondition. The intuition behind @{term"MGT c"} isthat it completely describes the operational behaviour of @{term c}.  It iseasy to see that, in the presence of the new consequence rule,\mbox{@{prop"{} \<turnstile> MGT c"}} implies completeness:*}lemma MGT_implies_complete: "{} \<turnstile> MGT c  ==>  {} \<Turnstile> {P}c{Q}  ==>  {} \<turnstile> {P}c{Q::state assn}"apply(simp add: MGT_def)apply (erule hoare.Conseq)apply(simp add: valid_defs)donetext{* In order to discharge @{prop"{} \<turnstile> MGT c"} one proves*}lemma MGT_lemma: "C \<turnstile> MGT CALL  ==>  C \<turnstile> 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)donetext{*\noindent The proof is by induction on @{term c}. In the @{termWhile}-case it is easy to show that @{term"λz t. (z,t) ∈ ({(s,t). bs ∧ s -c-> t})^*"} is invariant. The precondition \mbox{@{term[source]"λz s. z=s"}}establishes the invariant and a reflexive transitive closureinduction shows that the invariant conjoined with @{prop"¬b t"}implies the postcondition \mbox{@{term"λz t. z -WHILE b DO c-> t"}}. Theremaining cases are trivial.Using the @{thm[source]MGT_lemma} (together with the @{text CALL} and theassumption rule) one can easily derive *}lemma MGT_CALL: "{} \<turnstile> 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)donetext{*\noindent Using the @{thm[source]MGT_lemma} once more we obtain@{prop"{} \<turnstile> MGT c"} and thus by @{thm[source]MGT_implies_complete}completeness.*}theorem "{} \<Turnstile> {P}c{Q}  ==>  {} \<turnstile> {P}c{Q::state assn}"apply(erule MGT_implies_complete[OF MGT_lemma[OF MGT_CALL]])doneend