Theory utp_hoare

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 "`p1 ⇒ p2`" and "⦃p2⦄C⦃q⦄u"
  shows "⦃p1⦄C⦃q⦄u" 
  using assms by rel_auto
    
lemma post_weak_hoare_r:
  assumes "⦃p⦄C⦃q2⦄u" and "`q2 ⇒ q1`"
  shows "⦃p⦄C⦃q1⦄u" 
  using assms by rel_auto

lemma hoare_r_conseq: "⟦ `p1 ⇒ p2`; ⦃p2⦄S⦃q2⦄u; `q2 ⇒ q1` ⟧ ⟹ ⦃p1⦄S⦃q1⦄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 ⦃∃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⦄Q1⦃s⦄u ; ⦃s⦄Q2⦃r⦄u ⟧ ⟹ ⦃p⦄Q1 ;; Q2⦃r⦄u"
  by rel_auto

lemma seq_hoare_invariant [hoare_safe]: "⟦ ⦃p⦄Q1⦃p⦄u ; ⦃p⦄Q2⦃p⦄u ⟧ ⟹ ⦃p⦄Q1 ;; Q2⦃p⦄u"
  by rel_auto

lemma seq_hoare_stronger_pre_1 [hoare_safe]: 
  "⟦ ⦃p ∧ q⦄Q1⦃p ∧ q⦄u ; ⦃p ∧ q⦄Q2⦃q⦄u ⟧ ⟹ ⦃p ∧ q⦄Q1 ;; Q2⦃q⦄u"
  by rel_auto

lemma seq_hoare_stronger_pre_2 [hoare_safe]: 
  "⟦ ⦃p ∧ q⦄Q1⦃p ∧ q⦄u ; ⦃p ∧ q⦄Q2⦃p⦄u ⟧ ⟹ ⦃p ∧ q⦄Q1 ;; Q2⦃p⦄u"
  by rel_auto
    
lemma seq_hoare_inv_r_2 [hoare]: "⟦ ⦃p⦄Q1⦃q⦄u ; ⦃q⦄Q2⦃q⦄u ⟧ ⟹ ⦃p⦄Q1 ;; Q2⦃q⦄u"
  by rel_auto

lemma seq_hoare_inv_r_3 [hoare]: "⟦ ⦃p⦄Q1⦃p⦄u ; ⦃p⦄Q2⦃q⦄u ⟧ ⟹ ⦃p⦄Q1 ;; Q2⦃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⋆⦃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⊥ 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⊥ 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⌉< ⇒ ⌈p⌉<`"
    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