Quelle  Hoare.thy

(* Author: Tobias Nipkow *)

section "Hoare Logic"

subsection "Hoare Logic for Partial Correctness"

theory Hoare imports Big_Step begin

type_synonym assn = "state ==> bool"

definition
hoare_valid :: "assn ==> com ==> assn ==> bool" (‹⊨ {(1_)}/ (_)/ {(1_)}› 50) where
"⊨ {P}c{Q} = (∀s t. P s ∧ (c,s) ==> t ⟶ Q t)"

abbreviation state_subst :: "state ==> aexp ==> vname ==> state"
  (‹_[_'/_]› [1000,0,0] 999)
where "s[a/x] == s(x := aval a s)"

inductive
  hoare :: "assn ==> com ==> assn ==> bool" (‹⊨ ({(1_)}/ (_)/ {(1_)})› 50)
where
Skip: "⊨ {P} SKIP {P}"  |

Assign:  "⊨ {λs. P(s[a/x])} x::=a {P}"  |

Seq: "[ ⊨ {P} c🪙1 {Q}; ⊨ {Q} c🪙2 {R} ]
      ==> ⊨ {P} c🪙1;;c🪙2 {R}"  |

If: "[ ⊨ {λs. P s ∧ bval b s} c🪙1 {Q}; ⊨ {λs. P s ∧ ¬ bval b s} c🪙2 {Q} ]
     ==> ⊨ {P} IF b THEN c🪙1 ELSE c🪙2 {Q}"  |

While: "⊨ {λs. P s ∧ bval b s} c {P} ==>
        ⊨ {P} WHILE b DO c {λs. P s ∧ ¬ bval b s}"  |

conseq: "[ ∀s. P' s ⟶ P s; ⊨ {P} c {Q}; ∀s. Q s ⟶ Q' s ]
        ==> ⊨ {P'} c {Q'}"

lemmas [simp] = hoare.Skip hoare.Assign hoare.Seq If

lemmas [intro!] = hoare.Skip hoare.Assign hoare.Seq hoare.If

lemma strengthen_pre:
  "[ ∀s. P' s ⟶ P s; ⊨ {P} c {Q} ] ==> ⊨ {P'} c {Q}"
by (blast intro: conseq)

lemma weaken_post:
  "[ ⊨ {P} c {Q}; ∀s. Q s ⟶ Q' s ] ==> ⊨ {P} c {Q'}"
by (blast intro: conseq)

text‹The assignment and While rule are awkward to use in actual proofs
 because their pre and postcondition are of a very special form and the actual
 goal would have to match this form exactly. Therefore we derive two variants
 with arbitrary pre and postconditions.›

lemma Assign': "∀s. P s ⟶ Q(s[a/x]) ==> ⊨ {P} x ::= a {Q}"
by (simp add: strengthen_pre[OF _ Assign])

lemma While':
assumes "⊨ {λs. P s ∧ bval b s} c {P}" and "∀s. P s ∧ ¬ bval b s ⟶ Q s"
shows "⊨ {P} WHILE b DO c {Q}"
by(rule weaken_post[OF While[OF assms(1)] assms(2)])

end