Theory DRA

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

section ‹Demonic Refinement Algebras›

theory DRA
  imports Kleene_Algebra 
begin

text ‹
  A demonic refinement algebra *DRA)~\<^cite>‹"vonwright04refinement"› is a Kleene algebra without right annihilation plus 
  an operation for possibly infinite iteration.
›
class dra = kleene_algebra_zerol +
  fixes strong_iteration :: "'a ⇒ 'a" ("_⇧^∞" [101] 100)
  assumes iteration_unfoldl [simp] : "1 + x ⋅ x⇧^∞ = x⇧^∞"
  and coinduction: "y ≤ z + x ⋅ y ⟶ y ≤ x⇧^∞ ⋅ z"
  and isolation [simp]: "x⇧^⋆ + x⇧^∞ ⋅ 0 = x⇧^∞"
begin

text ‹$\top$ is an abort statement, defined as an infinite skip. It is the maximal element of any DRA.›

abbreviation top_elem :: "'a" ("⊤") where "⊤ ≡ 1⇧^∞"

text ‹Simple/basic lemmas about the iteration operator›

lemma iteration_refl: "1 ≤ x⇧^∞"
  using local.iteration_unfoldl local.order_prop by blast

lemma iteration_1l: "x ⋅ x⇧^∞ ≤ x⇧^∞"
  by (metis local.iteration_unfoldl local.join.sup.cobounded2)

lemma top_ref: "x ≤ ⊤"
proof -
  have "x ≤ 1 + 1 ⋅ x"
    by simp
  thus ?thesis
    using local.coinduction by fastforce
qed

lemma it_ext: "x ≤ x⇧^∞"
proof -
  have "x ≤ x ⋅ x⇧^∞"
    using iteration_refl local.mult_isol by fastforce
  thus ?thesis
    by (metis (full_types) local.isolation local.join.sup.coboundedI1 local.star_ext)
qed

lemma it_idem [simp]: "(x⇧^∞)⇧^∞ = x⇧^∞"
(*nitpick [expect=genuine]*)
oops

lemma top_mult_annil [simp]: "⊤ ⋅ x = ⊤"
  by (simp add: local.coinduction local.order.antisym top_ref)

lemma top_add_annil [simp]: "⊤ + x = ⊤"
  by (simp add: local.join.sup.absorb1 top_ref)

lemma top_elim: "x ⋅ y ≤ x ⋅ ⊤"
  by (simp add: local.mult_isol top_ref)

lemma iteration_unfoldl_distl [simp]: " y + y ⋅ x ⋅ x⇧^∞ = y ⋅ x⇧^∞"
  by (metis distrib_left mult.assoc mult_oner iteration_unfoldl)

lemma iteration_unfoldl_distr [simp]: " y + x ⋅ x⇧^∞ ⋅ y = x⇧^∞ ⋅ y"
  by (metis distrib_right' mult_1_left iteration_unfoldl)

lemma iteration_unfoldl' [simp]: "z ⋅ y + z ⋅ x ⋅ x⇧^∞ ⋅ y = z ⋅ x⇧^∞ ⋅ y"
  by (metis iteration_unfoldl_distl local.distrib_right)

lemma iteration_idem [simp]: "x⇧^∞ ⋅ x⇧^∞ = x⇧^∞"
proof (rule order.antisym)
  have "x⇧^∞ ⋅ x⇧^∞ ≤ 1 + x ⋅ x⇧^∞ ⋅ x⇧^∞"
    by (metis add_assoc iteration_unfoldl_distr local.eq_refl local.iteration_unfoldl local.subdistl_eq mult_assoc)
  thus "x⇧^∞ ⋅ x⇧^∞ ≤ x⇧^∞"
    using local.coinduction mult_assoc by fastforce
  show "x⇧^∞ ≤  x⇧^∞ ⋅ x⇧^∞"
    using local.coinduction by auto
qed

lemma iteration_induct: "x ⋅ x⇧^∞ ≤ x⇧^∞ ⋅ x"
proof -
  have "x + x ⋅ (x ⋅ x⇧^∞) = x ⋅ x⇧^∞"
    by (metis (no_types) local.distrib_left local.iteration_unfoldl local.mult_oner)
  thus ?thesis
    by (simp add: local.coinduction)
qed

lemma iteration_ref_star: "x⇧^⋆ ≤ x⇧^∞"
  by (simp add: local.star_inductl_one)

lemma iteration_subdist: "x⇧^∞ ≤ (x + y)⇧^∞"
  by (metis add_assoc' distrib_right' mult_oner coinduction join.sup_ge1 iteration_unfoldl)

lemma iteration_iso: "x ≤ y ⟹ x⇧^∞ ≤ y⇧^∞"
  using iteration_subdist local.order_prop by auto
 
lemma iteration_unfoldr [simp]: "1 + x⇧^∞ ⋅ x = x⇧^∞"
  by (metis add_0_left annil eq_refl isolation mult.assoc iteration_idem iteration_unfoldl iteration_unfoldl_distr star_denest star_one star_prod_unfold star_slide tc)

lemma iteration_unfoldr_distl [simp]: " y + y ⋅ x⇧^∞ ⋅ x = y ⋅ x⇧^∞"
  by (metis distrib_left mult.assoc mult_oner iteration_unfoldr)

lemma iteration_unfoldr_distr [simp]: " y + x⇧^∞ ⋅ x ⋅ y = x⇧^∞ ⋅ y"
  by (metis iteration_unfoldl_distr iteration_unfoldr_distl)

lemma iteration_unfold_eq: "x⇧^∞ ⋅ x = x ⋅ x⇧^∞"
  by (metis iteration_unfoldl_distr iteration_unfoldr_distl)
  
lemma iteration_unfoldr' [simp]: "z ⋅ y + z ⋅ x⇧^∞ ⋅ x ⋅ y = z ⋅ x⇧^∞ ⋅ y"
  by (metis distrib_left mult.assoc iteration_unfoldr_distr)

lemma iteration_double [simp]: "(x⇧^∞)⇧^∞ = ⊤"
  by (simp add: iteration_iso iteration_refl order.eq_iff top_ref)

lemma star_iteration [simp]: "(x⇧^⋆)⇧^∞ = ⊤"
  by (simp add: iteration_iso order.eq_iff top_ref)

lemma iteration_star [simp]: "(x⇧^∞)⇧^⋆ = x⇧^∞"
  by (metis (no_types) iteration_idem iteration_refl local.star_inductr_var_eq2 local.sup_id_star1)

lemma iteration_star2 [simp]: "x⇧^⋆ ⋅ x⇧^∞ = x⇧^∞"
proof -
  have f1: "(x⇧^∞)⇧^⋆ ⋅ x⇧^⋆ = x⇧^∞"
    by (metis (no_types) it_ext iteration_induct iteration_star local.bubble_sort local.join.sup.absorb1)
  have "x⇧^∞ = x⇧^∞ ⋅ x⇧^∞"
    by simp
  hence "x⇧^⋆ ⋅ x⇧^∞ = x⇧^⋆ ⋅ (x⇧^∞)⇧^⋆ ⋅ (x⇧^⋆ ⋅ (x⇧^∞)⇧^⋆)⇧^⋆"
    using f1 by (metis (no_types) iteration_star local.star_denest_var_4 mult_assoc)
  thus ?thesis
    using f1 by (metis (no_types) iteration_star local.star_denest_var_4 local.star_denest_var_8)
qed

lemma iteration_zero [simp]: "0⇧^∞ = 1"
  by (metis add_zeror annil iteration_unfoldl)

lemma iteration_annil [simp]: "(x ⋅ 0)⇧^∞ = 1 + x ⋅ 0"
  by (metis annil iteration_unfoldl mult.assoc)

lemma iteration_subdenest: "x⇧^∞ ⋅ y⇧^∞ ≤ (x + y)⇧^∞"
  by (metis add_commute iteration_idem iteration_subdist local.mult_isol_var)
  
lemma sup_id_top: "1 ≤ y ⟹ y ⋅ ⊤ = ⊤"
  using order.eq_iff local.mult_isol_var top_ref by fastforce

lemma iteration_top [simp]: "x⇧^∞ ⋅ ⊤ = ⊤"
  by (simp add: iteration_refl sup_id_top)

text ‹Next, we prove some simulation laws for data refinement.›

lemma iteration_sim: "z ⋅ y ≤ x ⋅ z ⟹ z ⋅ y⇧^∞ ≤ x⇧^∞ ⋅ z"
proof -
  assume assms: "z ⋅ y ≤ x ⋅ z"
  have "z ⋅ y⇧^∞ = z + z ⋅ y ⋅ y⇧^∞"
    by simp
  also have "... ≤ z + x ⋅ z ⋅ y⇧^∞"
    by (metis assms add.commute add_iso mult_isor)
  finally show "z ⋅ y⇧^∞ ≤ x⇧^∞ ⋅ z"
    by (simp add: local.coinduction mult_assoc)
qed

text ‹Nitpick gives a counterexample to the dual simulation law.›

lemma "y ⋅ z ≤ z ⋅ x ⟹ y⇧^∞ ⋅ z ≤ z ⋅ x⇧^∞"
(*nitpick [expect=genuine]*)
oops
  
text ‹Next, we prove some sliding laws.›

lemma iteration_slide_var: "x ⋅ (y ⋅ x)⇧^∞ ≤ (x ⋅ y)⇧^∞ ⋅ x"
  by (simp add: iteration_sim mult_assoc)

lemma iteration_prod_unfold [simp]: "1 + y ⋅ (x ⋅ y)⇧^∞ ⋅ x = (y ⋅ x)⇧^∞"
proof (rule order.antisym)
  have "1 + y ⋅ (x ⋅ y)⇧^∞ ⋅ x ≤ 1 + (y ⋅ x)⇧^∞ ⋅ y ⋅ x"
    using iteration_slide_var local.join.sup_mono local.mult_isor by blast
  thus "1 + y ⋅ (x ⋅ y)⇧^∞ ⋅ x ≤  (y ⋅ x)⇧^∞"
    by (simp add: mult_assoc)
  have "(y ⋅ x)⇧^∞ = 1 + y ⋅ x ⋅ (y ⋅ x)⇧^∞"
    by simp
  thus "(y ⋅ x)⇧^∞ ≤ 1 + y ⋅ (x ⋅ y)⇧^∞ ⋅ x"
    by (metis iteration_sim local.eq_refl local.join.sup.mono local.mult_isol mult_assoc)
qed

lemma iteration_slide: "x ⋅ (y ⋅ x)⇧^∞ = (x ⋅ y)⇧^∞ ⋅ x"
  by (metis iteration_prod_unfold iteration_unfoldl_distr distrib_left mult_1_right mult.assoc)

lemma star_iteration_slide [simp]: " y⇧^⋆ ⋅ (x⇧^⋆ ⋅ y)⇧^∞ = (x⇧^⋆ ⋅ y)⇧^∞"
  by (metis iteration_star2 local.conway.dagger_unfoldl_distr local.join.sup.orderE local.mult_isor local.star_invol local.star_subdist local.star_trans_eq)

text ‹The following laws are called denesting laws.›

lemma iteration_sub_denest: "(x + y)⇧^∞ ≤ x⇧^∞ ⋅ (y ⋅ x⇧^∞)⇧^∞"
proof -
  have "(x + y)⇧^∞ = x ⋅ (x + y)⇧^∞ + y ⋅ (x + y)⇧^∞ + 1"
    by (metis add.commute distrib_right' iteration_unfoldl)
  hence "(x + y)⇧^∞ ≤ x⇧^∞ ⋅ (y ⋅ (x + y)⇧^∞ + 1)"
    by (metis add_assoc' join.sup_least join.sup_ge1 join.sup_ge2 coinduction)
  moreover hence "x⇧^∞ ⋅ (y ⋅ (x + y)⇧^∞ + 1) ≤ x⇧^∞ ⋅ (y ⋅ x⇧^∞)⇧^∞"
    by (metis add_iso mult.assoc mult_isol add.commute coinduction mult_oner mult_isol)
  ultimately show ?thesis
    using local.order_trans by blast
qed

lemma iteration_denest: "(x + y)⇧^∞ = x⇧^∞ ⋅ (y ⋅ x⇧^∞)⇧^∞"
proof -
  have "x⇧^∞ ⋅ (y ⋅ x⇧^∞)⇧^∞ ≤ x ⋅ x⇧^∞ ⋅ (y ⋅ x⇧^∞)⇧^∞ + y ⋅ x⇧^∞ ⋅ (y ⋅ x⇧^∞)⇧^∞ + 1"
    by (metis add.commute iteration_unfoldl_distr add_assoc' add.commute iteration_unfoldl order_refl)
  thus ?thesis
    by (metis add.commute iteration_sub_denest order.antisym coinduction distrib_right' iteration_sub_denest mult.assoc mult_oner order.antisym)
qed
(*
end

sublocale dra ⊆ conway_zerol strong_iteration 
  apply (unfold_locales)
  apply (simp add: iteration_denest iteration_slide)
  apply simp
  by (simp add: iteration_sim)


context dra
begin
*)
lemma iteration_denest2 [simp]: "y⇧^⋆ ⋅ x ⋅ (x + y)⇧^∞ + y⇧^∞ = (x + y)⇧^∞"
proof -
  have "(x + y)⇧^∞ = y⇧^∞ ⋅ x ⋅ (y⇧^∞ ⋅ x)⇧^∞ ⋅ y⇧^∞ + y⇧^∞"
    by (metis add.commute iteration_denest iteration_slide iteration_unfoldl_distr)
  also have "... = y⇧^⋆ ⋅ x ⋅ (y⇧^∞ ⋅ x)⇧^∞ ⋅ y⇧^∞ + y⇧^∞ ⋅ 0 + y⇧^∞"
    by (metis isolation mult.assoc distrib_right' annil mult.assoc)
  also have "... = y⇧^⋆ ⋅ x ⋅ (y⇧^∞ ⋅ x)⇧^∞ ⋅ y⇧^∞ + y⇧^∞"
    by (metis add.assoc distrib_left mult_1_right add_0_left mult_1_right)
  finally show ?thesis
    by (metis add.commute iteration_denest iteration_slide mult.assoc)
qed

lemma iteration_denest3: "(y⇧^⋆ ⋅ x)⇧^∞ ⋅ y⇧^∞ = (x + y)⇧^∞"
proof (rule order.antisym)
  have  "(y⇧^⋆ ⋅ x)⇧^∞ ⋅ y⇧^∞ ≤ (y⇧^∞ ⋅ x)⇧^∞ ⋅ y⇧^∞"
    by (simp add: iteration_iso iteration_ref_star local.mult_isor)
  thus  "(y⇧^⋆ ⋅ x)⇧^∞ ⋅ y⇧^∞ ≤ (x + y)⇧^∞"
    by (metis iteration_denest iteration_slide local.join.sup_commute)
  have "(x + y)⇧^∞ = y⇧^∞ + y⇧^⋆ ⋅ x ⋅ (x + y)⇧^∞"
    by (metis iteration_denest2 local.join.sup_commute)
  thus "(x + y)⇧^∞ ≤ (y⇧^⋆ ⋅ x)⇧^∞ ⋅ y⇧^∞"
    by (simp add: local.coinduction) 
qed

text ‹Now we prove separation laws for reasoning about distributed systems in the context of action systems.›

lemma iteration_sep: "y ⋅ x ≤ x ⋅ y ⟹ (x + y)⇧^∞ = x⇧^∞ ⋅ y⇧^∞"
proof -
  assume "y ⋅ x ≤ x ⋅ y"
  hence "y⇧^⋆ ⋅ x ≤ x⋅(x + y)⇧^⋆"
    by (metis star_sim1 add.commute mult_isol order_trans star_subdist)
  hence "y⇧^⋆ ⋅ x ⋅ (x + y)⇧^∞ + y⇧^∞ ≤ x ⋅ (x + y)⇧^∞ + y⇧^∞"
    by (metis mult_isor mult.assoc iteration_star2 join.sup.mono eq_refl)
  thus ?thesis
    by (metis iteration_denest2 add.commute coinduction add.commute less_eq_def iteration_subdenest)
qed

lemma iteration_sim2: "y ⋅ x ≤ x ⋅ y ⟹ y⇧^∞ ⋅ x⇧^∞ ≤ x⇧^∞ ⋅ y⇧^∞"
  by (metis add.commute iteration_sep iteration_subdenest)

lemma iteration_sep2: "y ⋅ x ≤ x ⋅ y⇧^⋆ ⟹ (x + y)⇧^∞ = x⇧^∞ ⋅ y⇧^∞"
proof - 
  assume "y ⋅ x ≤ x ⋅ y⇧^⋆"
  hence "y⇧^⋆ ⋅ (y⇧^⋆ ⋅ x)⇧^∞ ⋅ y⇧^∞ ≤ x⇧^∞ ⋅ y⇧^⋆ ⋅ y⇧^∞"
    by (metis mult.assoc mult_isor iteration_sim star_denest_var_2 star_sim1 star_slide_var star_trans_eq tc_eq)
  moreover have "x⇧^∞ ⋅ y⇧^⋆ ⋅ y⇧^∞ ≤ x⇧^∞ ⋅ y⇧^∞"
    by (metis eq_refl mult.assoc iteration_star2)
  moreover have "(y⇧^⋆ ⋅ x)⇧^∞ ⋅ y⇧^∞ ≤ y⇧^⋆ ⋅ (y⇧^⋆ ⋅ x)⇧^∞ ⋅ y⇧^∞"
    by (metis mult_isor mult_onel star_ref)
  ultimately show ?thesis
    by (metis order.antisym iteration_denest3 iteration_subdenest order_trans)
qed

lemma iteration_sep3: "y ⋅ x ≤ x ⋅ (x + y) ⟹ (x + y)⇧^∞ = x⇧^∞ ⋅ y⇧^∞"
proof -
  assume "y ⋅ x ≤ x ⋅ (x + y)"
  hence "y⇧^⋆ ⋅ x ≤ x ⋅ (x + y)⇧^⋆"
    by (metis star_sim1)
  hence "y⇧^⋆ ⋅ x ⋅ (x + y)⇧^∞ + y⇧^∞ ≤ x ⋅ (x + y)⇧^⋆ ⋅ (x + y)⇧^∞ + y⇧^∞"
    by (metis add_iso mult_isor)
  hence "(x + y)⇧^∞ ≤ x⇧^∞ ⋅ y⇧^∞"
    by (metis mult.assoc iteration_denest2 iteration_star2 add.commute coinduction)
  thus ?thesis
    by (metis add.commute less_eq_def iteration_subdenest)
qed

lemma iteration_sep4: "y ⋅ 0 = 0 ⟹ z ⋅ x = 0 ⟹ y ⋅ x ≤ (x + z) ⋅ y⇧^⋆ ⟹ (x + y + z)⇧^∞ = x⇧^∞ ⋅ (y + z)⇧^∞"
proof -
  assume assms: "y ⋅ 0 = 0" "z ⋅ x = 0" "y ⋅ x ≤ (x + z) ⋅ y⇧^⋆"
  have "y ⋅ y⇧^⋆ ⋅ z ≤ y⇧^⋆ ⋅ z ⋅ y⇧^⋆"
    by (metis mult_isor star_1l mult_oner order_trans star_plus_one subdistl)
  have "y⇧^⋆ ⋅ z ⋅ x ≤ x ⋅ y⇧^⋆ ⋅ z"
    by (metis join.bot_least assms(1) assms(2) independence1 mult.assoc)
  have "y ⋅ (x + y⇧^⋆ ⋅ z) ≤ (x + z) ⋅ y⇧^⋆ + y ⋅ y⇧^⋆ ⋅ z"
    by (metis assms(3) distrib_left mult.assoc add_iso)
  also have "... ≤ (x + y⇧^⋆ ⋅ z) ⋅ y⇧^⋆ + y ⋅ y⇧^⋆ ⋅ z" 
    by (metis star_ref join.sup.mono eq_refl mult_1_left mult_isor)
  also have "... ≤ (x + y⇧^⋆ ⋅ z) ⋅ y⇧^⋆ + y⇧^⋆ ⋅ z  ⋅ y⇧^⋆" using ‹y ⋅ y⇧^⋆ ⋅ z ≤ y⇧^⋆ ⋅ z ⋅ y⇧^⋆›
    by (metis add.commute add_iso)
  finally have "y ⋅ (x + y⇧^⋆ ⋅ z) ≤ (x + y⇧^⋆ ⋅ z) ⋅ y⇧^⋆"
    by (metis add.commute add_idem' add.left_commute distrib_right)
  moreover have "(x + y + z)⇧^∞ ≤ (x + y + y⇧^⋆ ⋅ z)⇧^∞"
    by (metis star_ref join.sup.mono eq_refl mult_1_left mult_isor iteration_iso)  
  moreover have "... = (x + y⇧^⋆ ⋅ z)⇧^∞ ⋅ y⇧^∞"
    by (metis add_commute calculation(1) iteration_sep2 local.add_left_comm)
  moreover have "... = x⇧^∞ ⋅ (y⇧^⋆ ⋅ z)⇧^∞ ⋅ y⇧^∞" using ‹y⇧^⋆ ⋅ z ⋅ x ≤ x ⋅ y⇧^⋆ ⋅ z›
    by (metis iteration_sep mult.assoc)
  ultimately have "(x + y + z)⇧^∞ ≤ x⇧^∞ ⋅ (y + z)⇧^∞"
    by (metis add.commute mult.assoc iteration_denest3)
  thus ?thesis
    by (metis add.commute add.left_commute less_eq_def iteration_subdenest)
qed

text ‹Finally, we prove some blocking laws.›

text ‹Nitpick refutes the next lemma.›

lemma "x ⋅ y = 0 ⟹ x⇧^∞ ⋅ y = y"
(*nitpick*)
oops

lemma iteration_idep: "x ⋅ y = 0 ⟹ x ⋅ y⇧^∞ = x"
  by (metis add_zeror annil iteration_unfoldl_distl)

text ‹Nitpick refutes the next lemma.›

lemma "y ⋅ w ≤ x ⋅ y + z ⟹ y ⋅ w⇧^∞ ≤ x⇧^∞ ⋅ z"
(*nitpick [expect=genuine]*)
oops

text ‹At the end of this file, we consider a data refinement example from von Wright~\<^cite>‹"Wright02"›.›

lemma data_refinement:
  assumes "s' ≤ s ⋅ z" and "z ⋅ e' ≤ e" and "z ⋅ a' ≤ a ⋅ z" and "z ⋅ b ≤ z" and "b⇧^∞ = b⇧^⋆"
  shows "s' ⋅ (a' + b)⇧^∞ ⋅ e' ≤ s ⋅ a⇧^∞ ⋅ e"
proof -
  have "z ⋅ b⇧^⋆ ≤ z"
    by (metis assms(4) star_inductr_var)
  have "(z ⋅ a') ⋅ b⇧^⋆ ≤ (a ⋅ z) ⋅ b⇧^⋆"
    by (metis assms(3) mult.assoc mult_isor)
  hence "z ⋅ (a' ⋅ b⇧^⋆)⇧^∞ ≤  a⇧^∞ ⋅ z" using ‹z ⋅ b⇧^⋆ ≤ z›
    by (metis mult.assoc mult_isol order_trans iteration_sim mult.assoc)
  have "s' ⋅ (a' + b)⇧^∞ ⋅ e' ≤ s' ⋅ b⇧^⋆ ⋅ (a' ⋅ b⇧^⋆)⇧^∞ ⋅ e'"
    by (metis add.commute assms(5) eq_refl iteration_denest mult.assoc)
  also have "... ≤ s ⋅ z ⋅ b⇧^⋆ ⋅ (a' ⋅ b⇧^⋆)⇧^∞ ⋅ e'"
    by (metis assms(1) mult_isor)
  also have "... ≤ s ⋅ z ⋅ (a' ⋅ b⇧^⋆)⇧^∞ ⋅ e'" using ‹z ⋅ b⇧^⋆ ≤ z›
    by (metis mult.assoc mult_isol mult_isor)
  also have "... ≤ s ⋅ a⇧^∞ ⋅ z ⋅ e'" using ‹z ⋅ (a' ⋅ b⇧^⋆)⇧^∞ ≤  a⇧^∞ ⋅ z›
    by (metis mult.assoc mult_isol mult_isor)
  finally show ?thesis
    by (metis assms(2) mult.assoc mult_isol mult.assoc mult_isol order_trans)
qed

end

end