Theory DataRefinementIBP.Hoare

section ‹Hoare Triples›

theory Hoare
imports Statements
begin

text ‹
A hoare triple for $p,q\in \mathit{State}\ \mathit{set}$, and
$S : \mathit{State}\ \mathit{set} \to \mathit{State}\ \mathit{set}$ is valid,
denoted $\models p \{|S|\} q$, if every execution of $S$ starting from state $s\in p$
always terminates, and if it terminates in state $s'$, then $s'\in q$. When $S$ is
modeled as a predicate transformer, this definition is equivalent to requiring that
$p$ is a subset of the initial states from which the execution of $S$ is guaranteed
to terminate in $q$, that is $p \subseteq S\ q$.

The formal definition of a valid hoare triple only assumes that $p$ (and also $S\ q$) ranges
over a complete lattice.
›

definition
Hoare :: "'a::complete_distrib_lattice ⇒ ('b ⇒ 'a) ⇒ 'b ⇒ bool" ("⊨ (_){| _ |}(_)" [0,0,900] 900) where
"⊨ p {|S|} q = (p ≤ (S q))"

theorem hoare_sequential:
"mono S ⟹ (⊨ p {| S o T |} r) = ( (∃ q. ⊨ p {| S |} q ∧ ⊨ q {| T |} r))"
by (metis (no_types) Hoare_def monoD o_def order_refl order_trans)

theorem hoare_choice:
"⊨ p {| S ⊓ T |} q = (⊨ p {| S |} q ∧ ⊨ p {| T |} q)"

theorem hoare_assume:
"(⊨ P {| [.R.] |} Q) = (P ⊓ R ≤ Q)"
apply safe
apply (case_tac "(inf P R) ≤ (inf (sup (- R) Q) R)")
apply (case_tac "(sup (-R) (inf P R)) ≤ sup (- R) Q")

theorem hoare_mono:
"mono S ⟹ Q ≤ R ⟹ ⊨ P {| S |} Q ⟹ ⊨ P {| S |} R"
apply (rule_tac y = "S Q" in order_trans)
by auto

theorem hoare_pre:
"R ≤ P ⟹ ⊨ P {| S |} Q ⟹ ⊨ R {| S |} Q"

theorem hoare_Sup:
"(∀ p ∈ P . ⊨ p {| S |} q) = ⊨ Sup P {| S |} q"
apply (rule_tac y = "⨆P" in order_trans, simp_all)

lemma hoare_magic [simp]: "⊨ P {| ⊤ |} Q"

lemma hoare_demonic: "⊨ P {| [:R:] |} Q = (∀ s . s ∈ P ⟶  R s ⊆ Q)"
apply (unfold Hoare_def demonic_def)
by auto

lemma hoare_not_guard:
"mono (S :: (_::order_bot) ⇒ _) ⟹ ⊨ p {| S |} q = ⊨ (p ⊔ (- grd S)) {| S |} q"
apply (simp add: Hoare_def grd_def, safe)
apply (drule monoD)
by auto

subsection ‹Hoare rule for recursive statements›

text ‹
A statement $S$ is refined by another statement $S'$ if $\models p \{| S' |\} q$
is true for all $p$ and $q$ such that  $\models p \{| S |\} q$ is true. This
is equivalent to $S \le S'$.

Next theorem can be used to prove refinement of a recursive program. A recursive
program is modeled as the least fixpoint of a monotonic mapping from predicate
transformers to predicate transformers.
›

theorem lfp_wf_induction:
"mono f ⟹ (∀ w . (p w) ≤ f (Sup_less p w)) ⟹ Sup (range p) ≤ lfp f"
apply (rule fp_wf_induction, simp_all)
by (drule lfp_unfold, simp)

definition
"post_fun (p::'a::order) q = (if p ≤ q then ⊤ else ⊥)"

lemma post_mono [simp]: "mono (post_fun p :: (_::{order_bot,order_top}))"
apply (simp add: post_fun_def  mono_def, safe)
apply (subgoal_tac "p ≤ y", simp)
by (rule_tac y = x in order_trans, simp_all)

lemma post_top [simp]: "post_fun p p = ⊤"

lemma post_refin [simp]: "mono S ⟹ ((S p)::'a::bounded_lattice) ⊓ (post_fun p) x ≤ S x"
apply (simp add: le_fun_def post_fun_def, safe)
by (rule_tac f = S in monoD, simp_all)

text ‹
Next theorem shows the equivalence between the validity of Hoare
triples and refinement statements. This theorem together with the
theorem for refinement of recursive programs will be used to prove
a Hoare rule for recursive programs.
›

theorem hoare_refinement_post:
"mono f ⟹  (⊨ x {| f |} y) = ({.x.} o (post_fun y) ≤ f)"
apply safe
apply (rule_tac y = "f y ⊓ post_fun y xa" in order_trans, simp_all)
apply (rule_tac y = "x" in order_trans, simp_all)
by (drule_tac x = "y" in spec, simp)

text ‹
Next theorem gives a Hoare rule for recursive programs. If we can prove correct the unfolding
of the recursive definition applid to a program $f$, $\models p\ w\ \{| F\ f |\}\ y$, assumming
that $f$ is correct when starting from $p\ v$, $v<w$, $\models SUP-L\ p\ w\ \{| f |\}\ y$, then
the recursive program is correct $\models SUP\ p\ \{| lfp\ F |\}\ y$
›

lemma assert_Sup: "{.⨆ (X::'a::complete_distrib_lattice set).} = ⨆ (assert  X)"
by (simp add: fun_eq_iff assert_def Sup_inf image_comp)

lemma assert_Sup_range: "{.⨆ (range (p::'W ⇒ 'a::complete_distrib_lattice)).} = ⨆ (range (assert o p))"
by (simp add: fun_eq_iff assert_def SUP_inf image_comp)

lemma Sup_range_comp: "(⨆ range p) o S = ⨆ (range (λ w . ((p w) o S)))"

lemma Sup_less_comp: "(Sup_less P) w o S = Sup_less (λ w . ((P w) o S)) w"
apply (simp add: Sup_less_def fun_eq_iff, safe)
apply (subgoal_tac "((λf. f (S x))  {y. ∃v<w. ∀x. y x = P v x}) = ((λf. f x)  {y. ∃v<w. ∀x. y x = P v (S x)})")
apply (auto cong del: SUP_cong_simp)
done

lemma Sup_less_assert: "Sup_less (λw. {. (p w)::'a::complete_distrib_lattice .}) w = {.Sup_less p w.}"
apply (simp add: Sup_less_def assert_Sup image_def)
apply (subgoal_tac "{y. ∃v<w. y = {. p v .}} = {y. ∃x. (∃v<w. x = p v) ∧ y = {. x .}}")
apply (auto simp add: image_def cong del: SUP_cong_simp)
done

declare mono_comp[simp]

theorem hoare_fixpoint:
"mono_mono F ⟹
(!! w f . mono f ∧ ⊨ Sup_less p w {| f |} y ⟹ ⊨ p w {| F f |} y) ⟹ ⊨ (Sup (range p)) {| lfp F |} y"
apply (simp add: mono_mono_def hoare_refinement_post assert_Sup_range Sup_range_comp)
apply (rule lfp_wf_induction)
apply auto
apply (simp add: Sup_less_comp [THEN sym])
`