Quelle  utp_hoare.thy

section ‹ Relational Hoare calculus ›

theory utp_hoare
  imports 
    utp_rel_laws
    utp_theory
begin

subsection ‹ Hoare Triple Definitions and Tactics ›

definition hoare_r :: "'α cond ==> 'α hrel ==> 'α cond ==> bool" (‹{_}/ _/ {_}_u›) where
"{p}Q{r}_u = ((⌈p⌉_< ==> ⌈r⌉_>) ⊑ Q)"

declare hoare_r_def [upred_defs]

named_theorems hoare and hoare_safe

method hoare_split uses hr = 
  ((simp add: assigns_comp)?, ― ‹ Combine Assignments where possible ›
   (auto
    intro: hoare intro!: hoare_safe hr
    simp add: conj_comm conj_assoc usubst unrest))[1] ― ‹ Apply Hoare logic laws ›

method hoare_auto uses hr = (hoare_split hr: hr; (rel_simp)?, auto?)

subsection ‹ Basic Laws ›

lemma hoare_meaning:
  "{P}S{Q}_u = (∀ s s'. [P]_e s ∧ [S]_e (s, s') ⟶ [Q]_e s')"
  by (rel_auto)

lemma hoare_assume: "{P}S{Q}_u ==> ?[P] ;; S = ?[P] ;; S ;; ?[Q]"
  by (rel_auto)

lemma hoare_r_conj [hoare_safe]: "[ {p}Q{r}_u; {p}Q{s}_u ] ==> {p}Q{r ∧ s}_u"
  by rel_auto

lemma hoare_r_weaken_pre [hoare]:
  "{p}Q{r}_u ==> {p ∧ q}Q{r}_u"
  "{q}Q{r}_u ==> {p ∧ q}Q{r}_u"
  by rel_auto+

lemma pre_str_hoare_r:
  assumes "`p<sub>1</sub> ==> p<sub>2</sub>`" and "{p₂}C{q}_u"
  shows "{p₁}C{q}_u" 
  using assms by rel_auto
    
lemma post_weak_hoare_r:
  assumes "{p}C{q₂}_u" and "`q<sub>2</sub> ==> q<sub>1</sub>`"
  shows "{p}C{q₁}_u" 
  using assms by rel_auto

lemma hoare_r_conseq: "[ `p<sub>1</sub> ==> p<sub>2</sub>`; {p₂}S{q₂}_u; `q<sub>2</sub> ==> q<sub>1</sub>` ] ==> {p₁}S{q₁}_u"
  by rel_auto

subsection ‹ Assignment Laws ›

lemma assigns_hoare_r [hoare_safe]: "`p ==> σ † q` ==> {p}⟨σ⟩_a{q}_u"
  by rel_auto

lemma assigns_backward_hoare_r: 
  "{σ † p}⟨σ⟩_a{p}_u"
  by rel_auto

lemma assign_floyd_hoare_r:
  assumes "vwb_lens x"
  shows "{p} assign_r x e {\<exists>v ∙ p[«v¬/x] ∧ &x =_u e[«v¬/x]}_u"
  using assms
  by (rel_auto, metis vwb_lens_wb wb_lens.get_put)

lemma assigns_init_hoare [hoare_safe]:
  "[ vwb_lens x; x ♯ p; x ♯ v; {&x =_u v ∧ p}S{q}_u ] ==> {p}x := v ;; S{q}_u"
  by (rel_auto)

lemma skip_hoare_r [hoare_safe]: "{p}II{p}_u"
  by rel_auto

lemma skip_hoare_impl_r [hoare_safe]: "`p ==> q` ==> {p}II{q}_u"
  by rel_auto  

subsection ‹ Sequence Laws ›

lemma seq_hoare_r: "[ {p}Q₁{s}_u ; {s}Q₂{r}_u ] ==> {p}Q₁ ;; Q₂{r}_u"
  by rel_auto

lemma seq_hoare_invariant [hoare_safe]: "[ {p}Q₁{p}_u ; {p}Q₂{p}_u ] ==> {p}Q₁ ;; Q₂{p}_u"
  by rel_auto

lemma seq_hoare_stronger_pre_1 [hoare_safe]: 
  "[ {p ∧ q}Q₁{p ∧ q}_u ; {p ∧ q}Q₂{q}_u ] ==> {p ∧ q}Q₁ ;; Q₂{q}_u"
  by rel_auto

lemma seq_hoare_stronger_pre_2 [hoare_safe]: 
  "[ {p ∧ q}Q₁{p ∧ q}_u ; {p ∧ q}Q₂{p}_u ] ==> {p ∧ q}Q₁ ;; Q₂{p}_u"
  by rel_auto
    
lemma seq_hoare_inv_r_2 [hoare]: "[ {p}Q₁{q}_u ; {q}Q₂{q}_u ] ==> {p}Q₁ ;; Q₂{q}_u"
  by rel_auto

lemma seq_hoare_inv_r_3 [hoare]: "[ {p}Q₁{p}_u ; {p}Q₂{q}_u ] ==> {p}Q₁ ;; Q₂{q}_u"
  by rel_auto

subsection ‹ Conditional Laws ›

lemma cond_hoare_r [hoare_safe]: "[ {b ∧ p}S{q}_u ; {¬b ∧ p}T{q}_u ] ==> {p}S ◃ b ▹_r T{q}_u"
  by rel_auto

lemma cond_hoare_r_wp: 
  assumes "{p'}S{q}_u" and "{p''}T{q}_u"
  shows "{(b ∧ p') ∨ (¬b ∧ p'')}S ◃ b ▹_r T{q}_u"
  using assms by pred_simp

lemma cond_hoare_r_sp:
  assumes ‹{b ∧ p}S{q}_u› and ‹{¬b ∧ p}T{s}_u›
  shows ‹{p}S ◃ b ▹_r T{q ∨ s}_u›
  using assms by pred_simp

subsection ‹ Recursion Laws ›

lemma nu_hoare_r_partial: 
  assumes induct_step:
    "∧ st P. {p}P{q}_u ==> {p}F P{q}_u"   
  shows "{p}ν F {q}_u"  
  by (meson hoare_r_def induct_step lfp_lowerbound order_refl)

lemma mu_hoare_r:
  assumes WF: "wf R"
  assumes M:"mono F"  
  assumes induct_step:
    "∧ st P. {p ∧ (e,«st¬)_u ∈_u «R¬}P{q}_u ==> {p ∧ e =_u «st¬}F P{q}_u"   
  shows "{p}μ F {q}_u"  
  unfolding hoare_r_def
proof (rule mu_rec_total_utp_rule[OF WF M , of _ e ], goal_cases)
  case (1 st)
  then show ?case 
    using induct_step[unfolded hoare_r_def, of "(⌈p⌉_< ∧ (⌈e⌉_<, «st¬)_u ∈_u «R¬ ==> ⌈q⌉_>)" st]
    by (simp add: alpha)    
qed
    
lemma mu_hoare_r':
  assumes WF: "wf R"
  assumes M:"mono F"  
  assumes induct_step:
    "∧ st P. {p ∧ (e,«st¬)_u ∈_u «R¬} P {q}_u ==> {p ∧ e =_u «st¬} F P {q}_u" 
  assumes I0: "`p' ==> p`"  
  shows "{p'} μ F {q}_u"
  by (meson I0 M WF induct_step mu_hoare_r pre_str_hoare_r)

subsection ‹ Iteration Rules ›

lemma iter_hoare_r: "{P}S{P}_u ==> {P}S^\<star>{P}_u"
  by (rel_simp', metis (mono_tags, lifting) mem_Collect_eq rtrancl_induct)

lemma while_hoare_r [hoare_safe]:
  assumes "{p ∧ b}S{p}_u"
  shows "{p}while b do S od{¬b ∧ p}_u"
  using assms
  by (simp add: while_top_def hoare_r_def, rule_tac lfp_lowerbound) (rel_auto)

lemma while_invr_hoare_r [hoare_safe]:
  assumes "{p ∧ b}S{p}_u" "`pre ==> p`" "`(¬b ∧ p) ==> post`"
  shows "{pre}while b invr p do S od{post}_u"
  by (metis assms hoare_r_conseq while_hoare_r while_inv_def)

lemma while_r_minimal_partial:
  assumes seq_step: "`p ==> invar`"
  assumes induct_step: "{invar∧ b} C {invar}_u"  
  shows "{p}while b do C od{¬b ∧ invar}_u"
  using induct_step pre_str_hoare_r seq_step while_hoare_r by blast

lemma approx_chain: 
  "(⊓n::nat. ⌈p ∧ v <_u «n¬⌉_<) = ⌈p⌉_<"
  by (rel_auto)

text ‹ Total correctness law for Hoare logic, based on constructive chains. This is limited to
 variants that have naturals numbers as their range. ›
    
lemma while_term_hoare_r:
  assumes "∧ z::nat. {p ∧ b ∧ v =_u «z¬}S{p ∧ v <_u «z¬}_u"
  shows "{p}while_\<bottom> b do S od{¬b ∧ p}_u"
proof -
  have "(⌈p⌉_< ==> ⌈¬ b ∧ p⌉_>) ⊑ (μ X ∙ S ;; X ◃ b ▹_r II)"
  proof (rule mu_refine_intro)

    from assms show "(⌈p⌉_< ==> ⌈¬ b ∧ p⌉_>) ⊑ S ;; (⌈p⌉_< ==> ⌈¬ b ∧ p⌉_>) ◃ b ▹_r II"
      by (rel_auto)

    let ?E = "λ n. ⌈p ∧ v <_u «n¬⌉_<"
    show "(⌈p⌉_< ∧ (μ X ∙ S ;; X ◃ b ▹_r II)) = (⌈p⌉_< ∧ (ν X ∙ S ;; X ◃ b ▹_r II))"
    proof (rule constr_fp_uniq[where E="?E"])

      show "(⊓n. ?E(n)) = ⌈p⌉_<"
        by (rel_auto)
          
      show "mono (λX. S ;; X ◃ b ▹_r II)"
        by (simp add: cond_mono monoI seqr_mono)
          
      show "constr (λX. S ;; X ◃ b ▹_r II) ?E"
      proof (rule constrI)
        
        show "chain ?E"
        proof (rule chainI)
          show "⌈p ∧ v <_u «0¬⌉_< = false"
            by (rel_auto)
          show "∧i. ⌈p ∧ v <_u «Suc i¬⌉_< ⊑ ⌈p ∧ v <_u «i¬⌉_<"
            by (rel_auto)
        qed
          
        from assms
        show "∧X n. (S ;; X ◃ b ▹_r II ∧ ⌈p ∧ v <_u «n + 1¬⌉_<) =
                     (S ;; (X ∧ ⌈p ∧ v <_u «n¬⌉_<) ◃ b ▹_r II ∧ ⌈p ∧ v <_u «n + 1¬⌉_<)"
          apply (rel_auto)
          using less_antisym less_trans apply blast
          done
      qed  
    qed
  qed

  thus ?thesis
    by (simp add: hoare_r_def while_bot_def)
qed

lemma while_vrt_hoare_r [hoare_safe]:
  assumes "∧ z::nat. {p ∧ b ∧ v =_u «z¬}S{p ∧ v <_u «z¬}_u" "`pre ==> p`" "`(¬b ∧ p) ==> post`"
  shows "{pre}while b invr p vrt v do S od{post}_u"
  apply (rule hoare_r_conseq[OF assms(2) _ assms(3)])
  apply (simp add: while_vrt_def)
  apply (rule while_term_hoare_r[where v="v", OF assms(1)]) 
  done
  
text ‹ General total correctness law based on well-founded induction ›
        
lemma while_wf_hoare_r:
  assumes WF: "wf R"
  assumes I0: "`pre ==> p`"
  assumes induct_step:"∧ st. {b ∧ p ∧ e =_u «st¬}Q{p ∧ (e, «st¬)_u ∈_u «R¬}_u"
  assumes PHI:"`(¬b ∧ p) ==> post`"  
  shows "{pre}while_\<bottom> b invr p do Q od{post}_u"
unfolding hoare_r_def while_inv_bot_def while_bot_def
proof (rule pre_weak_rel[of _ "⌈p⌉_<" ])
  from I0 show "`⌈pre⌉<sub><</sub> ==> ⌈p⌉<sub><</sub>`"
    by rel_auto
  show "(⌈p⌉_< ==> ⌈post⌉_>) ⊑ (μ X ∙ Q ;; X ◃ b ▹_r II)"
  proof (rule mu_rec_total_utp_rule[where e=e, OF WF])
    show "Monotonic (λX. Q ;; X ◃ b ▹_r II)"
      by (simp add: closure)
    have induct_step': "∧ st. (⌈b ∧ p ∧ e =_u «st¬ ⌉_< ==> (⌈p ∧ (e,«st¬)_u ∈_u «R¬ ⌉_> )) ⊑ Q"
      using induct_step by rel_auto  
    with PHI
    show "∧st. (⌈p⌉_< ∧ ⌈e⌉_< =_u «st¬ ==> ⌈post⌉_>) ⊑ Q ;; (⌈p⌉_< ∧ (⌈e⌉_<, «st¬)_u ∈_u «R¬ ==> ⌈post⌉_>) ◃ b ▹_r II" 
      by (rel_auto)
  qed       
qed

subsection ‹ Frame Rules ›

text ‹ Frame rule: If starting $S$ in a state satisfying $p establishes q$ in the final state, then
 we can insert an invariant predicate $r$ when $S$ is framed by $a$, provided that $r$ does not
 refer to variables in the frame, and $q$ does not refer to variables outside the frame. ›

lemma frame_hoare_r:
  assumes "vwb_lens a" "a ♯ r" "a ♮ q" "{p}P{q}_u"  
  shows "{p ∧ r}a:[P]{q ∧ r}_u"
  using assms
  by (rel_auto, metis)

lemma frame_strong_hoare_r [hoare_safe]: 
  assumes "vwb_lens a" "a ♯ r" "a ♮ q" "{p ∧ r}S{q}_u"
  shows "{p ∧ r}a:[S]{q ∧ r}_u"
  using assms by (rel_auto, metis)

lemma frame_hoare_r' [hoare_safe]: 
  assumes "vwb_lens a" "a ♯ r" "a ♮ q" "{r ∧ p}S{q}_u"
  shows "{r ∧ p}a:[S]{r ∧ q}_u"
  using assms
  by (simp add: frame_strong_hoare_r utp_pred_laws.inf.commute)

lemma antiframe_hoare_r:
  assumes "vwb_lens a" "a ♮ r" "a ♯ q" "{p}P{q}_u"  
  shows "{p ∧ r} a:[P] {q ∧ r}_u"
  using assms by (rel_auto, metis)
    
lemma antiframe_strong_hoare_r:
  assumes "vwb_lens a" "a ♮ r" "a ♯ q" "{p ∧ r}P{q}_u"  
  shows "{p ∧ r} a:[P] {q ∧ r}_u"
  using assms by (rel_auto, metis)
  
end