# Theory PsHoare

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

theory PsHoare
imports PsLang
(*  Title:       Inductive definition of Hoare logic    Author:      Tobias Nipkow, 2001/2006    Maintainer:  Tobias Nipkow*)theory PsHoare imports PsLang beginsubsection{* 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" ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" 50) where "\<Turnstile> {P}c{Q} ≡ (∀s t z. s -c-> t --> P z s --> Q z t)"definition valids :: "'a cntxt => bool" ("|\<Turnstile> _" 50) where "|\<Turnstile> D ≡ (∀(P,c,Q) ∈ D. \<Turnstile> {P}c{Q})"definition nvalid :: "nat => 'a assn => com => 'a assn => bool" ("\<Turnstile>_ {(1_)}/ (_)/ {(1_)}" 50) where "\<Turnstile>n {P}c{Q} ≡ (∀s t z. s -c-n-> t --> 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})"text{* We now need an additional notion ofvalidity \mbox{@{text"C |\<Turnstile> D"}} where @{term D} is a set as well. Thereason is that we can now have mutually recursive procedures whosecorrectness needs to be established by simultaneous induction. Insteadof sets of Hoare triples we may think of conjunctions. We define both@{text"C |\<Turnstile> D"} and its relativized version: *}definition cvalids :: "'a cntxt => 'a cntxt => bool" ("_ |\<Turnstile>/ _" 50) where  "C |\<Turnstile> D <-> |\<Turnstile> C --> |\<Turnstile> D"definition cnvalids :: "'a cntxt => nat => 'a cntxt => bool" ("_ |\<Turnstile>'__/ _" 50) where  "C |\<Turnstile>_n D <-> |\<Turnstile>_n C --> |\<Turnstile>_n D"text{*Our Hoare logic now defines judgements of the form @{text"C \<tturnstile>D"} where both @{term C} and @{term D} are (potentially infinite) setsof Hoare triples; @{text"C \<turnstile> {P}c{Q}"} is simply an abbreviation for@{text"C \<tturnstile> {(P,c,Q)}"}.*}inductive  hoare :: "'a cntxt => 'a cntxt => bool" ("_ \<tturnstile>/ _" 50)  and hoare3 :: "'a cntxt => 'a assn => com => 'a assn => bool" ("_ \<turnstile>/ ({(1_)}/ (_)/ {(1_)})" 50)where  "C \<turnstile> {P}c{Q}  ≡  C \<tturnstile> {(P,c,Q)}"| Do:  "C \<turnstile> {λz s. ∀t ∈ f s . P z t} Do f {P}"| Semi: "[| C \<turnstile> {P}c{Q}; C \<turnstile> {Q}d{R} |] ==> C \<turnstile> {P} c;d {R}"| If: "[| C \<turnstile> {λz s. P z s ∧ b s}c{Q}; C \<turnstile> {λz s. P z s ∧ ¬b s}d{Q}  |] ==>      C \<turnstile> {P} IF b THEN c ELSE d {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,c,Q) ∈ C. ∃p. c = CALL p;     C \<tturnstile> {(P,b,Q). ∃p. (P,CALL p,Q) ∈ C ∧ b = body p} |]  ==> {} \<tturnstile> C"| Asm: "(P,CALL p,Q) ∈ C ==> C \<turnstile> {P} CALL p {Q}"| ConjI: "∀(P,c,Q) ∈ D. C \<turnstile> {P}c{Q}  ==>  C \<tturnstile> D"| ConjE: "[| C \<tturnstile> D; (P,c,Q) ∈ D |] ==> C \<turnstile> {P}c{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}"monos split_betalemmas valid_defs = valid_def valids_def cvalids_def                    nvalid_def nvalids_def cnvalids_deftheorem "C \<tturnstile> D  ==>  C |\<Turnstile> D"txt{*\noindent As before, we prove a generalization of @{prop"C |\<Turnstile> D"},namely @{prop"∀n. C |\<Turnstile>_n D"}, by induction on @{prop"C \<tturnstile> D"}, with aninduction on @{term n} in the @{term CALL} case.*}apply(subgoal_tac "∀n. C |\<Turnstile>_n D")apply(unfold valid_defs exec_iff_execn[THEN eq_reflection]) apply fastapply(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 fastapply simpapply fastapply simpapply fastapply fastapply fastforcedonedefinition 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\<turnstile> {P}c{Q}  |] ==> C\<turnstile> {P'}c{Q}";by(rule hoare.Conseq, assumption, blast)lemma MGT_implies_complete:  "{} \<tturnstile> {MGT c} ==> \<Turnstile> {P}c{Q} ==> {} \<turnstile> {P}c{Q::state assn}";apply(unfold MGT_def)apply (erule hoare.Conseq)apply(simp add: valid_defs)donelemma MGT_lemma: "∀p. C \<tturnstile> {MGT(CALL p)}  ==>  C \<tturnstile> {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 simpapply(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 clarsimpapply(rename_tac s t)apply(erule_tac x = s in allE)apply clarsimpapply(erule converse_rtrancl_induct) apply(blast intro:exec.intros)apply(fast elim:exec.WhileTrue)apply(fastforce intro: hoare.Local elim!: hoare.Conseq)donelemma MGT_body: "(P, CALL p, Q) = MGT (CALL pa) ==> C \<tturnstile> {MGT (body p)} ==> C \<turnstile> {P} body p {Q}"apply clarsimpdonedeclare MGT_def[simp del]lemma MGT_CALL: "{} \<tturnstile> {mgt. ∃p. mgt = MGT(CALL p)}"apply (rule hoare.Call) apply(fastforce simp add:MGT_def)apply(rule hoare.ConjI)apply clarsimpapply (erule MGT_body)apply(rule MGT_lemma)apply(unfold MGT_def)apply(fast intro: hoare.Asm)donetheorem Complete: "\<Turnstile> {P}c{Q}  ==>  {} \<turnstile> {P}c{Q::state assn}";apply(rule MGT_implies_complete) prefer 2 apply assumptionapply (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)doneend