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