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)"
  by (simp_all add: Hoare_def inf_fun_def)

theorem hoare_assume:
  "(⊨ P {| [.R.] |} Q) = (P ⊓ R ≤ Q)"
  apply (simp add: Hoare_def assume_def)
  apply safe
  apply (case_tac "(inf P R) ≤ (inf (sup (- R) Q) R)")
  apply (simp add: inf_sup_distrib2)
  apply (simp add: le_infI1)
  apply (case_tac "(sup (-R) (inf P R)) ≤ sup (- R) Q")
  apply (simp add: sup_inf_distrib1)
  by (simp add: le_supI2)

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

theorem hoare_pre:
  "R ≤ P ⟹ ⊨ P {| S |} Q ⟹ ⊨ R {| S |} Q"
  by (simp add: Hoare_def)

theorem hoare_Sup:
  "(∀ p ∈ P . ⊨ p {| S |} q) = ⊨ Sup P {| S |} q"
  apply (simp add: Hoare_def, safe, simp add: Sup_least)
  apply (rule_tac y = "⨆P" in order_trans, simp_all)
  by (simp add: Sup_upper)
  
lemma hoare_magic [simp]: "⊨ P {| ⊤ |} Q" 
  by (simp add: Hoare_def top_fun_def)

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 = ⊤"
  by (simp add: post_fun_def)

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 (simp_all add: Hoare_def)
  apply (simp_all add: le_fun_def)
  apply (simp add: assert_def, 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)
  apply (simp add: assert_def)
  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)))"
  by (simp add: fun_eq_iff image_comp)

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])
  apply (simp add: Sup_less_assert)
  apply (drule_tac x = "{. Sup_less p w .} ∘ post_fun y" in spec, safe)
  apply simp
  by (simp add: hoare_refinement_post)

theorem "(∀ t . ⊨ ({s . t ∈ R s}) {|S|} q) ⟹ ⊨ ({:R:} p) {| S |} q"
  apply (simp add: Hoare_def angelic_def subset_eq)
  by auto

end