Theory HoareEx
section "Correctness of Hoare by Fixpoint Reasoning"
theory HoareEx imports Denotational begin
text ‹
An example from the HOLCF paper by Müller, Nipkow, Oheimb, Slotosch
\<^cite>‹MuellerNvOS99›. It demonstrates fixpoint reasoning by showing
the correctness of the Hoare rule for while-loops.
›
type_synonym assn = "state ⇒ bool"
definition
hoare_valid :: "[assn, com, assn] ⇒ bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where
"|= {P} c {Q} = (∀s t. P s ∧ D c⋅(Discr s) = Def t ⟶ Q t)"
lemma WHILE_rule_sound:
"|= {A} c {A} ⟹ |= {A} WHILE b DO c {λs. A s ∧ ¬ bval b s}"
apply (unfold hoare_valid_def)
apply (simp (no_asm))
apply (rule fix_ind)
apply (simp (no_asm))
apply (simp (no_asm))
apply (simp (no_asm))
apply blast
done
end