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