Theory DRAT

(* Title:      Demonic refinement algebra
   Author:     Alasdair Armstrong, Victor B. F. Gomes, Georg Struth
   Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
*)

section ‹Demonic Refinement Algebra with Tests›

theory DRAT
  imports KAT Kleene_Algebra.DRA
begin

text ‹
  In this section, we define demonic refinement algebras with tests and prove the most important theorems from
  the literature. In this context, tests are also known as guards.
›

class drat = dra + test_semiring_zerol
begin

subclass kat_zerol ..

text ‹
  An assertion is a mapping from a guard to a subset similar to tests, but it aborts if the predicate does
  not hold.
›

definition assertion :: "'a ⇒ 'a" (‹_⇧^o› [101] 100) where
  "test p ⟹ p⇧^o = !p⋅⊤ + 1"

lemma asg: "⟦test p; test q⟧ ⟹ q ≤ 1 ∧ 1 ≤ p⇧^o"
  by (simp add: assertion_def local.test_subid)

lemma assertion_isol: "test p ⟹ y ≤ p⇧^o⋅x ⟷ p⋅y ≤ x"
proof
  assume assms: "test p" "y ≤ p⇧^o⋅x"
  hence "p⋅y ≤ p⋅!p⋅⊤⋅x + p⋅x"
    by (metis add_commute assertion_def local.distrib_left local.iteration_prod_unfold local.iteration_unfoldl_distr local.mult_isol local.top_mult_annil mult_assoc)
  also have "... ≤ x"
    by (simp add: assms(1) local.test_restrictl)
  finally show "p⋅y ≤ x"
    by metis
next
  assume assms: "test p" "p⋅y ≤ x"
  hence "p⇧^o⋅p⋅y = !p⋅⊤⋅p⋅y + p⋅y"
    by (metis assertion_def distrib_right' mult_1_left mult.assoc)
  also have "... = !p⋅⊤ + p⋅y"
    by (metis mult.assoc top_mult_annil)
  moreover have "p⇧^o⋅p⋅y ≤ p⇧^o⋅x"
    by (metis assms(2) mult.assoc mult_isol)
  moreover have "!p⋅y + p⋅y ≤ !p⋅⊤ + p⋅y"
    using local.add_iso local.top_elim by blast
  ultimately show "y ≤ p⇧^o⋅x"    
    by (metis add.commute assms(1) distrib_right' mult_1_left order_trans test_add_comp)
qed

lemma assertion_isor: "test p ⟹ y ≤ x⋅p ⟷ y⋅p⇧^o ≤ x"
proof
  assume assms: "test p" "y ≤ x⋅p"
  hence "y⋅p⇧^o ≤ x⋅p⋅!p⋅⊤ + x⋅p"
    by (metis mult_isor assertion_def assms(1) distrib_left mult_1_right mult.assoc)
  also have "... ≤ x"
    by (metis assms(1) local.iteration_idep local.join.sup.absorb_iff1 local.join.sup_commute local.join.sup_ge2 local.mult_1_right local.mult_isol_var local.mult_isor local.mult_onel local.test_add_comp local.test_comp_mult2 mult_assoc)
  finally show "y⋅p⇧^o ≤ x"
    by metis
next
  assume assms: "test p" "y⋅p⇧^o ≤ x"
  have "y ≤ y⋅(!p⋅⊤ + p)"
    by (metis join.sup_mono mult_isol order_refl order_refl top_elim add.commute assms(1) mult_1_right test_add_comp)
  also have "... = y⋅p⇧^o⋅p"
    by (metis assertion_def assms(1) distrib_right' mult_1_left mult.assoc top_mult_annil)
  finally show "y ≤ x⋅p"
    by (metis assms(2) mult_isor order_trans)
qed

lemma assertion_iso: "⟦test p; test q⟧ ⟹ x⋅q⇧^o ≤ p⇧^o⋅x ⟷ p⋅x ≤ x⋅q"
  by (metis assertion_isol assertion_isor mult.assoc)

lemma total_correctness: "⟦test p; test q⟧ ⟹ p⋅x⋅!q = 0 ⟷ x⋅!q ≤ !p⋅⊤"
  apply standard
  apply (metis local.test_eq4 local.top_elim mult_assoc)
  by (metis annil order.antisym test_comp_mult2 join.bot_least mult_assoc mult_isol)

lemma test_iteration_sim: "⟦test p; p⋅x ≤ x⋅p⟧ ⟹ p⋅x⇧^∞ ≤ x⇧^∞⋅p"
  by (metis iteration_sim)

lemma test_iteration_annir: "test p ⟹ !p⋅(p⋅x)⇧^∞ = !p"
  by (metis annil test_comp_mult1 iteration_idep mult.assoc)

text ‹Next we give an example of a program transformation from von Wright~\<^cite>‹"Wright02"›.›

lemma loop_refinement: "⟦test p; test q⟧ ⟹ (p⋅x)⇧^∞⋅!p ≤ (p⋅q⋅x)⇧^∞⋅!(p⋅q)⋅(p⋅x)⇧^∞⋅!p"
proof -
  assume assms: "test p" "test q"
  hence "(p⋅x)⇧^∞⋅!p = ((p⋅q) + !(p⋅q))⋅(p⋅x)⇧^∞⋅!p"
    by (simp add: local.test_mult_closed)
  also have "... = (p⋅q)⋅(p⋅x)⇧^∞⋅!p + !(p⋅q)⋅(p⋅x)⇧^∞⋅!p"
    by (metis distrib_right')
  also have "... = (p⋅q)⋅!p + (p⋅q)⋅(p⋅x)⋅(p⋅x)⇧^∞⋅!p + !(p⋅q)⋅(p⋅x)⇧^∞⋅!p"
    by (metis iteration_unfoldr_distr mult.assoc iteration_unfold_eq distrib_left mult.assoc)
  also have "... = (p⋅q)⋅(p⋅x)⋅(p⋅x)⇧^∞⋅!p + !(p⋅q)⋅(p⋅x)⇧^∞⋅!p"
    by (metis assms less_eq_def test_preserve2 join.bot_least)
  finally have "(p⋅x)⇧^∞⋅!p ≤ p⋅q⋅x⋅(p⋅x)⇧^∞⋅!p + !(p⋅q)⋅(p⋅x)⇧^∞⋅!p"
    by (metis assms(1) assms(2) order.eq_iff local.test_mult_comm_var local.test_preserve mult_assoc)
  thus ?thesis
    by (metis coinduction add.commute mult.assoc)
qed

text ‹Finally, we prove different versions of Back's atomicity refinement theorem for action systems.›

lemma atom_step1: "r⋅b ≤ b⋅r ⟹ (a + b + r)⇧^∞ = b⇧^∞⋅r⇧^∞⋅(a⋅b⇧^∞⋅r⇧^∞)⇧^∞"
  apply (subgoal_tac "(a + b + r)⇧^∞ = (b + r)⇧^∞⋅(a⋅(b + r)⇧^∞)⇧^∞")
  apply (metis iteration_sep mult.assoc)
  by (metis add_assoc' add.commute iteration_denest)

 
lemma atom_step2: 
  assumes "s = s⋅q" "q⋅b = 0" "r⋅q ≤ q⋅r" "q⋅l ≤ l⋅q" "r⇧^∞ = r⇧^⋆" "test q"
  shows "s⋅l⇧^∞⋅b⇧^∞⋅r⇧^∞⋅q⋅(a⋅b⇧^∞⋅r⇧^∞⋅q)⇧^∞ ≤ s⋅l⇧^∞⋅r⇧^∞⋅(a⋅b⇧^∞⋅q⋅r⇧^∞)⇧^∞"
proof -
  have "s⋅l⇧^∞⋅b⇧^∞⋅r⇧^∞⋅q⋅(a⋅b⇧^∞⋅r⇧^∞⋅q)⇧^∞ ≤ s⋅l⇧^∞⋅b⇧^∞⋅r⇧^∞⋅q⋅(a⋅b⇧^∞⋅q⋅r⇧^∞)⇧^∞"
    by (metis assms(3) assms(5) star_sim1 mult.assoc mult_isol iteration_iso)
  also have "... ≤ s⋅q⋅l⇧^∞⋅b⇧^∞⋅r⇧^∞⋅(a⋅b⇧^∞⋅q⋅r⇧^∞)⇧^∞"
    using assms(1) assms(6) local.mult_isor local.test_restrictr by auto
  also have "... ≤ s⋅l⇧^∞⋅q⋅b⇧^∞⋅r⇧^∞⋅(a⋅b⇧^∞⋅q⋅r⇧^∞)⇧^∞"
    by (metis assms(4) iteration_sim mult.assoc mult_double_iso mult_double_iso)
  also have "... ≤ s⋅l⇧^∞⋅r⇧^∞⋅q⋅r⇧^∞⋅(a⋅b⇧^∞⋅q⋅r⇧^∞)⇧^∞" 
    by (metis assms(2) join.bot_least iteration_sim mult.assoc mult_double_iso)
  also have "... ≤ s⋅l⇧^∞⋅r⇧^∞⋅(a⋅b⇧^∞⋅q⋅r⇧^∞)⇧^∞"
    by (metis assms(6) mult.assoc mult_isol test_restrictl iteration_idem mult.assoc)
  finally show "s⋅l⇧^∞⋅b⇧^∞⋅r⇧^∞⋅q⋅(a⋅b⇧^∞⋅r⇧^∞⋅q)⇧^∞ ≤ s⋅l⇧^∞⋅r⇧^∞⋅(a⋅b⇧^∞⋅q⋅r⇧^∞)⇧^∞"
    by metis
qed

lemma atom_step3: 
  assumes "r⋅l ≤ l⋅r" "a⋅l ≤ l⋅a" "b⋅l ≤ l⋅b" "q⋅l ≤ l⋅q" "b⇧^∞ = b⇧^⋆"
  shows "l⇧^∞⋅r⇧^∞⋅(a⋅b⇧^∞⋅q⋅r⇧^∞)⇧^∞ = (a⋅b⇧^∞⋅q + l + r)⇧^∞"
proof -
  have "(a⋅b⇧^∞⋅q + r)⋅l ≤ a⋅b⇧^∞⋅l⋅q + l⋅r"
    by (metis distrib_right join.sup_mono assms(1,4) mult.assoc mult_isol)
  also have "... ≤ a⋅l⋅b⇧^∞⋅q + l⋅r"
    by (metis assms(3) assms(5) star_sim1 add_iso mult.assoc mult_double_iso)
  also have "... ≤ l⋅(a⋅b⇧^∞⋅q + r)"
    by (metis add_iso assms(2) mult_isor distrib_left mult.assoc)
  finally have "(a⋅b⇧^∞⋅q + r)⋅l ≤ l⋅(a⋅b⇧^∞⋅q + r)"
    by metis
  moreover have "l⇧^∞⋅r⇧^∞⋅(a⋅b⇧^∞⋅q⋅r⇧^∞)⇧^∞ = l⇧^∞⋅(a⋅b⇧^∞⋅q + r)⇧^∞"
    by (metis add.commute mult.assoc iteration_denest)
  ultimately show ?thesis
    by (metis add.commute add.left_commute iteration_sep)
qed

text ‹
  This is Back's atomicity refinement theorem, as specified by von Wright~\cite {Wright02}.
›

theorem atom_ref_back: 
  assumes "s = s⋅q" "a = q⋅a" "q⋅b = 0"
          "r⋅b ≤ b⋅r" "r⋅l ≤ l⋅r" "r⋅q ≤ q⋅r"
          "a⋅l ≤ l⋅a" "b⋅l ≤ l⋅b" "q⋅l ≤ l⋅q"
          "r⇧^∞ = r⇧^⋆" "b⇧^∞ = b⇧^⋆" "test q"
  shows "s⋅(a + b + r + l)⇧^∞⋅q ≤ s⋅(a⋅b⇧^∞⋅q + r + l)⇧^∞"
proof -
  have "(a + b + r)⋅l ≤ l⋅(a + b + r)"
    by (metis join.sup_mono distrib_right' assms(5) assms(7) assms(8) distrib_left)
  hence "s⋅(l + a + b + r)⇧^∞⋅q = s⋅l⇧^∞⋅(a + b + r)⇧^∞⋅q"
    by (metis add.commute add.left_commute mult.assoc iteration_sep)
  also have "... ≤ s⋅l⇧^∞⋅b⇧^∞⋅r⇧^∞⋅q⋅(a⋅b⇧^∞⋅r⇧^∞⋅q)⇧^∞"
    by (metis assms(2,4,10,11) atom_step1 iteration_slide eq_refl mult.assoc)
  also have "... ≤ s⋅l⇧^∞⋅r⇧^∞⋅(a⋅b⇧^∞⋅q⋅r⇧^∞)⇧^∞" 
    by (metis assms(1) assms(10) assms(12) assms(3) assms(6) assms(9) atom_step2)
  also have "... ≤ s⋅(a⋅b⇧^∞⋅q + l + r)⇧^∞"
    by (metis assms(11) assms(5) assms(7) assms(8) assms(9) atom_step3 eq_refl mult.assoc)
  finally show ?thesis
    by (metis add.commute add.left_commute)
qed

text ‹
  This variant is due to H\"ofner, Struth and Sutcliffe~\<^cite>‹"HofnerSS09"›.
›

theorem atom_ref_back_struth: 
  assumes "s ≤ s⋅q" "a ≤ q⋅a" "q⋅b = 0"
          "r⋅b ≤ b⋅r" "r⋅q ≤ q⋅r"
          "(a + r + b)⋅l ≤ l⋅(a + r + b)" "q⋅l ≤ l⋅q"
          "r⇧^∞ = r⇧^⋆" "q ≤ 1"
  shows "s⋅(a + b + r + l)⇧^∞⋅q ≤ s⋅(a⋅b⇧^∞⋅q + r + l)⇧^∞"
proof -
  have "s⋅(a + b + r + l)⇧^∞⋅q = s⋅l⇧^∞⋅(a + b + r)⇧^∞⋅q"
    by (metis add.commute add.left_commute assms(6) iteration_sep mult.assoc)
  also have "... = s⋅l⇧^∞⋅(b + r)⇧^∞⋅(a⋅(b + r)⇧^∞)⇧^∞⋅q"
    by (metis add_assoc' add.commute iteration_denest add.commute mult.assoc)
  also have "... = s⋅l⇧^∞⋅b⇧^∞⋅r⇧^∞⋅(a⋅b⇧^∞⋅r⇧^∞)⇧^∞⋅q"
    by (metis assms(4) iteration_sep mult.assoc)
  also have "... ≤ s⋅l⇧^∞⋅b⇧^∞⋅r⇧^∞⋅(q⋅a⋅b⇧^∞⋅r⇧^∞)⇧^∞⋅q"
    by (metis assms(2) iteration_iso mult_isol_var eq_refl order_refl)
  also have "... = s⋅l⇧^∞⋅b⇧^∞⋅r⇧^∞⋅q⋅(a⋅b⇧^∞⋅r⇧^∞⋅q)⇧^∞"
    by (metis iteration_slide mult.assoc)
  also have "... ≤ s⋅q⋅l⇧^∞⋅b⇧^∞⋅r⇧^∞⋅q⋅(a⋅b⇧^∞⋅r⇧^∞⋅q)⇧^∞"
    by (metis assms(1) mult_isor)
  also have "... ≤ s⋅l⇧^∞⋅q⋅b⇧^∞⋅r⇧^∞⋅q⋅(a⋅b⇧^∞⋅r⇧^∞⋅q)⇧^∞"
    by (metis assms(7) iteration_sim mult.assoc mult_double_iso)
  also have "... ≤ s⋅l⇧^∞⋅q⋅r⇧^∞⋅q⋅(a⋅b⇧^∞⋅r⇧^∞⋅q)⇧^∞"
    by (metis assms(3) iteration_idep mult.assoc order_refl)
  also have "... ≤ s⋅l⇧^∞⋅q⋅r⇧^∞⋅q⋅(a⋅b⇧^∞⋅r⇧^⋆⋅q)⇧^∞"
    by (metis assms(8) eq_refl)
  also have "... ≤ s⋅l⇧^∞⋅q⋅r⇧^∞⋅q⋅(a⋅b⇧^∞⋅q⋅r⇧^⋆)⇧^∞"
    by (metis assms(5) iteration_iso mult.assoc mult_isol star_sim1)
  also have "... = s⋅l⇧^∞⋅q⋅r⇧^∞⋅q⋅(a⋅b⇧^∞⋅q⋅r⇧^∞)⇧^∞"
    by (metis assms(8))
  also have "... ≤ s⋅l⇧^∞⋅r⇧^∞⋅q⋅(a⋅b⇧^∞⋅q⋅r⇧^∞)⇧^∞"
    by (metis assms(9) mult_1_right mult_double_iso mult_isor)
  also have "... ≤ s⋅l⇧^∞⋅r⇧^∞⋅(a⋅b⇧^∞⋅q⋅r⇧^∞)⇧^∞"
    by (metis assms(9) mult_1_right mult_double_iso)
  also have "... = s⋅l⇧^∞⋅(a⋅b⇧^∞⋅q + r)⇧^∞"
    by (metis add.commute mult.assoc iteration_denest)
  also have "... ≤ s⋅(a⋅b⇧^∞⋅q + r + l)⇧^∞"
    by (metis add.commute iteration_subdenest mult.assoc mult_isol)
  finally show ?thesis .
qed
    

text ‹Finally, we prove Cohen's~\<^cite>‹"Cohen00"› variation of the atomicity refinement theorem.›

lemma atom_ref_cohen: 
  assumes "r⋅p⋅y ≤ y⋅r" "y⋅p⋅l ≤ l⋅y" "r⋅p⋅l ≤ l⋅r"
          "p⋅r⋅!p = 0" "p⋅l⋅!p = 0" "!p⋅l⋅p = 0"
          "y⋅0 = 0" "r⋅0 = 0" "test p"
  shows "(y + r + l)⇧^∞ = (p⋅l)⇧^∞⋅(y + !p⋅l + r⋅!p)⇧^∞⋅(r⋅p)⇧^∞"
proof -    
  have "(y + r)⋅p⋅l ≤ l⋅y + l⋅r"
    by (metis distrib_right' join.sup_mono assms(2) assms(3))
  hence stepA: "(y + r)⋅p⋅l ≤ (p⋅l + !p⋅l)⋅(y + r)⇧^⋆"
    by (metis assms(9) distrib_left distrib_right' mult_1_left mult_isol order_trans star_ext test_add_comp)
  have subStepB: "(!p⋅l + y + p⋅r + !p⋅r)⇧^∞ = (!p⋅l + y + r⋅p + r⋅!p)⇧^∞"
    by (metis add_assoc' annil assms(8) assms(9) distrib_left distrib_right' star_slide star_subid test_add_comp join.bot_least)
  have "r⋅p⋅(y + r⋅!p + !p⋅l) ≤ y⋅(r⋅p + r⋅!p)"
    by (metis assms(1,4,9) distrib_left add_0_left add.commute annil mult.assoc test_comp_mult2 distrib_left mult_oner test_add_comp)
  also have "... ≤ (y + r⋅!p + !p⋅l)⋅(r⋅p + (y + r⋅!p + !p⋅l))"
    by (meson local.eq_refl local.join.sup_ge1 local.join.sup_ge2 local.join.sup_mono local.mult_isol_var local.order_trans)
  finally have "r⋅p⋅(y + r⋅!p + !p⋅l) ≤ (y + r⋅!p + !p⋅l)⋅(y + r⋅!p + !p⋅l + r⋅p)" 
    by (metis add.commute)
  hence stepB: "(!p⋅l + y + p⋅r + !p⋅r)⇧^∞ = (y + !p⋅l + r⋅!p)⇧^∞⋅(r⋅p)⇧^∞" 
    by (metis subStepB iteration_sep3[of "r⋅p" "y + r⋅!p + !p⋅l"]  add_assoc' add.commute)
  have "(y + r + l)⇧^∞ = (p⋅l + !p⋅l + y + r)⇧^∞"
    by (metis add_comm add.left_commute assms(9) distrib_right' mult_onel test_add_comp)
  also have "... = (p⋅l)⇧^∞⋅(!p⋅l + y + r)⇧^∞" using stepA
    by (metis assms(6-8) annil add.assoc add_0_left distrib_right' add.commute mult.assoc iteration_sep4[of "y+r" "!p⋅l" "p⋅l"])
  also have "... = (p⋅l)⇧^∞⋅(!p⋅l + y + p⋅r + !p⋅r)⇧^∞"
    by (metis add.commute assms(9) combine_common_factor mult_1_left test_add_comp)
  finally show ?thesis using stepB
    by (metis mult.assoc)
qed
end

end