Quelle  DRA.thy

(* 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^\<infinity> = x^\<infinity>"
  and coinduction: "y ≤ z + x ⋅ y ⟶ y ≤ x^\<infinity> ⋅ z"
  and isolation [simp]: "x^\<star> + x^\<infinity> ⋅ 0 = x^\<infinity>"
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^\<infinity>"

text ‹Simple/basic lemmas about the iteration operator›

lemma iteration_refl: "1 ≤ x^\<infinity>"
  using local.iteration_unfoldl local.order_prop by blast

lemma iteration_1l: "x ⋅ x^\<infinity> ≤ x^\<infinity>"
  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^\<infinity>"
proof -
  have "x ≤ x ⋅ x^\<infinity>"
    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^\<infinity>)^\<infinity> = x^\<infinity>"
(*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^\<infinity> = y ⋅ x^\<infinity>"
  by (metis distrib_left mult.assoc mult_oner iteration_unfoldl)

lemma iteration_unfoldl_distr [simp]: " y + x ⋅ x^\<infinity> ⋅ y = x^\<infinity> ⋅ y"
  by (metis distrib_right' mult_1_left iteration_unfoldl)

lemma iteration_unfoldl' [simp]: "z ⋅ y + z ⋅ x ⋅ x^\<infinity> ⋅ y = z ⋅ x^\<infinity> ⋅ y"
  by (metis iteration_unfoldl_distl local.distrib_right)

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

lemma iteration_induct: "x ⋅ x^\<infinity> ≤ x^\<infinity> ⋅ x"
proof -
  have "x + x ⋅ (x ⋅ x^\<infinity>) = x ⋅ x^\<infinity>"
    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^\<star> ≤ x^\<infinity>"
  by (simp add: local.star_inductl_one)

lemma iteration_subdist: "x^\<infinity> ≤ (x + y)^\<infinity>"
  by (metis add_assoc' distrib_right' mult_oner coinduction join.sup_ge1 iteration_unfoldl)

lemma iteration_iso: "x ≤ y ==> x^\<infinity> ≤ y^\<infinity>"
  using iteration_subdist local.order_prop by auto
 
lemma iteration_unfoldr [simp]: "1 + x^\<infinity> ⋅ x = x^\<infinity>"
  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^\<infinity> ⋅ x = y ⋅ x^\<infinity>"
  by (metis distrib_left mult.assoc mult_oner iteration_unfoldr)

lemma iteration_unfoldr_distr [simp]: " y + x^\<infinity> ⋅ x ⋅ y = x^\<infinity> ⋅ y"
  by (metis iteration_unfoldl_distr iteration_unfoldr_distl)

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

lemma iteration_double [simp]: "(x^\<infinity>)^\<infinity> = ⊤"
  by (simp add: iteration_iso iteration_refl order.eq_iff top_ref)

lemma star_iteration [simp]: "(x^\<star>)^\<infinity> = ⊤"
  by (simp add: iteration_iso order.eq_iff top_ref)

lemma iteration_star [simp]: "(x^\<infinity>)^\<star> = x^\<infinity>"
  by (metis (no_types) iteration_idem iteration_refl local.star_inductr_var_eq2 local.sup_id_star1)

lemma iteration_star2 [simp]: "x^\<star> ⋅ x^\<infinity> = x^\<infinity>"
proof -
  have f1: "(x^\<infinity>)^\<star> ⋅ x^\<star> = x^\<infinity>"
    by (metis (no_types) it_ext iteration_induct iteration_star local.bubble_sort local.join.sup.absorb1)
  have "x^\<infinity> = x^\<infinity> ⋅ x^\<infinity>"
    by simp
  hence "x^\<star> ⋅ x^\<infinity> = x^\<star> ⋅ (x^\<infinity>)^\<star> ⋅ (x^\<star> ⋅ (x^\<infinity>)^\<star>)^\<star>"
    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^\<infinity> = 1"
  by (metis add_zeror annil iteration_unfoldl)

lemma iteration_annil [simp]: "(x ⋅ 0)^\<infinity> = 1 + x ⋅ 0"
  by (metis annil iteration_unfoldl mult.assoc)

lemma iteration_subdenest: "x^\<infinity> ⋅ y^\<infinity> ≤ (x + y)^\<infinity>"
  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^\<infinity> ⋅ ⊤ = ⊤"
  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^\<infinity> ≤ x^\<infinity> ⋅ z"
proof -
  assume assms: "z ⋅ y ≤ x ⋅ z"
  have "z ⋅ y^\<infinity> = z + z ⋅ y ⋅ y^\<infinity>"
    by simp
  also have "... ≤ z + x ⋅ z ⋅ y^\<infinity>"
    by (metis assms add.commute add_iso mult_isor)
  finally show "z ⋅ y^\<infinity> ≤ x^\<infinity> ⋅ 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^\<infinity> ⋅ z ≤ z ⋅ x^\<infinity>"
(*nitpick [expect=genuine]*)
oops
  
text ‹Next, we prove some sliding laws.›

lemma iteration_slide_var: "x ⋅ (y ⋅ x)^\<infinity> ≤ (x ⋅ y)^\<infinity> ⋅ x"
  by (simp add: iteration_sim mult_assoc)

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

lemma iteration_slide: "x ⋅ (y ⋅ x)^\<infinity> = (x ⋅ y)^\<infinity> ⋅ x"
  by (metis iteration_prod_unfold iteration_unfoldl_distr distrib_left mult_1_right mult.assoc)

lemma star_iteration_slide [simp]: " y^\<star> ⋅ (x^\<star> ⋅ y)^\<infinity> = (x^\<star> ⋅ y)^\<infinity>"
  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)^\<infinity> ≤ x^\<infinity> ⋅ (y ⋅ x^\<infinity>)^\<infinity>"
proof -
  have "(x + y)^\<infinity> = x ⋅ (x + y)^\<infinity> + y ⋅ (x + y)^\<infinity> + 1"
    by (metis add.commute distrib_right' iteration_unfoldl)
  hence "(x + y)^\<infinity> ≤ x^\<infinity> ⋅ (y ⋅ (x + y)^\<infinity> + 1)"
    by (metis add_assoc' join.sup_least join.sup_ge1 join.sup_ge2 coinduction)
  moreover hence "x^\<infinity> ⋅ (y ⋅ (x + y)^\<infinity> + 1) ≤ x^\<infinity> ⋅ (y ⋅ x^\<infinity>)^\<infinity>"
    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)^\<infinity> = x^\<infinity> ⋅ (y ⋅ x^\<infinity>)^\<infinity>"
proof -
  have "x^\<infinity> ⋅ (y ⋅ x^\<infinity>)^\<infinity> ≤ x ⋅ x^\<infinity> ⋅ (y ⋅ x^\<infinity>)^\<infinity> + y ⋅ x^\<infinity> ⋅ (y ⋅ x^\<infinity>)^\<infinity> + 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 \<subseteq> 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^\<star> ⋅ x ⋅ (x + y)^\<infinity> + y^\<infinity> = (x + y)^\<infinity>"
proof -
  have "(x + y)^\<infinity> = y^\<infinity> ⋅ x ⋅ (y^\<infinity> ⋅ x)^\<infinity> ⋅ y^\<infinity> + y^\<infinity>"
    by (metis add.commute iteration_denest iteration_slide iteration_unfoldl_distr)
  also have "... = y^\<star> ⋅ x ⋅ (y^\<infinity> ⋅ x)^\<infinity> ⋅ y^\<infinity> + y^\<infinity> ⋅ 0 + y^\<infinity>"
    by (metis isolation mult.assoc distrib_right' annil mult.assoc)
  also have "... = y^\<star> ⋅ x ⋅ (y^\<infinity> ⋅ x)^\<infinity> ⋅ y^\<infinity> + y^\<infinity>"
    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^\<star> ⋅ x)^\<infinity> ⋅ y^\<infinity> = (x + y)^\<infinity>"
proof (rule order.antisym)
  have  "(y^\<star> ⋅ x)^\<infinity> ⋅ y^\<infinity> ≤ (y^\<infinity> ⋅ x)^\<infinity> ⋅ y^\<infinity>"
    by (simp add: iteration_iso iteration_ref_star local.mult_isor)
  thus  "(y^\<star> ⋅ x)^\<infinity> ⋅ y^\<infinity> ≤ (x + y)^\<infinity>"
    by (metis iteration_denest iteration_slide local.join.sup_commute)
  have "(x + y)^\<infinity> = y^\<infinity> + y^\<star> ⋅ x ⋅ (x + y)^\<infinity>"
    by (metis iteration_denest2 local.join.sup_commute)
  thus "(x + y)^\<infinity> ≤ (y^\<star> ⋅ x)^\<infinity> ⋅ y^\<infinity>"
    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)^\<infinity> = x^\<infinity> ⋅ y^\<infinity>"
proof -
  assume "y ⋅ x ≤ x ⋅ y"
  hence "y^\<star> ⋅ x ≤ x⋅(x + y)^\<star>"
    by (metis star_sim1 add.commute mult_isol order_trans star_subdist)
  hence "y^\<star> ⋅ x ⋅ (x + y)^\<infinity> + y^\<infinity> ≤ x ⋅ (x + y)^\<infinity> + y^\<infinity>"
    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^\<infinity> ⋅ x^\<infinity> ≤ x^\<infinity> ⋅ y^\<infinity>"
  by (metis add.commute iteration_sep iteration_subdenest)

lemma iteration_sep2: "y ⋅ x ≤ x ⋅ y^\<star> ==> (x + y)^\<infinity> = x^\<infinity> ⋅ y^\<infinity>"
proof - 
  assume "y ⋅ x ≤ x ⋅ y^\<star>"
  hence "y^\<star> ⋅ (y^\<star> ⋅ x)^\<infinity> ⋅ y^\<infinity> ≤ x^\<infinity> ⋅ y^\<star> ⋅ y^\<infinity>"
    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^\<infinity> ⋅ y^\<star> ⋅ y^\<infinity> ≤ x^\<infinity> ⋅ y^\<infinity>"
    by (metis eq_refl mult.assoc iteration_star2)
  moreover have "(y^\<star> ⋅ x)^\<infinity> ⋅ y^\<infinity> ≤ y^\<star> ⋅ (y^\<star> ⋅ x)^\<infinity> ⋅ y^\<infinity>"
    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)^\<infinity> = x^\<infinity> ⋅ y^\<infinity>"
proof -
  assume "y ⋅ x ≤ x ⋅ (x + y)"
  hence "y^\<star> ⋅ x ≤ x ⋅ (x + y)^\<star>"
    by (metis star_sim1)
  hence "y^\<star> ⋅ x ⋅ (x + y)^\<infinity> + y^\<infinity> ≤ x ⋅ (x + y)^\<star> ⋅ (x + y)^\<infinity> + y^\<infinity>"
    by (metis add_iso mult_isor)
  hence "(x + y)^\<infinity> ≤ x^\<infinity> ⋅ y^\<infinity>"
    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^\<star> ==> (x + y + z)^\<infinity> = x^\<infinity> ⋅ (y + z)^\<infinity>"
proof -
  assume assms: "y ⋅ 0 = 0" "z ⋅ x = 0" "y ⋅ x ≤ (x + z) ⋅ y^\<star>"
  have "y ⋅ y^\<star> ⋅ z ≤ y^\<star> ⋅ z ⋅ y^\<star>"
    by (metis mult_isor star_1l mult_oner order_trans star_plus_one subdistl)
  have "y^\<star> ⋅ z ⋅ x ≤ x ⋅ y^\<star> ⋅ z"
    by (metis join.bot_least assms(1) assms(2) independence1 mult.assoc)
  have "y ⋅ (x + y^\<star> ⋅ z) ≤ (x + z) ⋅ y^\<star> + y ⋅ y^\<star> ⋅ z"
    by (metis assms(3) distrib_left mult.assoc add_iso)
  also have "... ≤ (x + y^\<star> ⋅ z) ⋅ y^\<star> + y ⋅ y^\<star> ⋅ z" 
    by (metis star_ref join.sup.mono eq_refl mult_1_left mult_isor)
  also have "... ≤ (x + y^\<star> ⋅ z) ⋅ y^\<star> + y^\<star> ⋅ z ⋅ y^\<star>" using ‹y ⋅ y^\⋆ ⋅ z ≤ y^\⋆ ⋅ z ⋅ y^\⋆›
    by (metis add.commute add_iso)
  finally have "y ⋅ (x + y^\<star> ⋅ z) ≤ (x + y^\<star> ⋅ z) ⋅ y^\<star>"
    by (metis add.commute add_idem' add.left_commute distrib_right)
  moreover have "(x + y + z)^\<infinity> ≤ (x + y + y^\<star> ⋅ z)^\<infinity>"
    by (metis star_ref join.sup.mono eq_refl mult_1_left mult_isor iteration_iso)  
  moreover have "... = (x + y^\<star> ⋅ z)^\<infinity> ⋅ y^\<infinity>"
    by (metis add_commute calculation(1) iteration_sep2 local.add_left_comm)
  moreover have "... = x^\<infinity> ⋅ (y^\<star> ⋅ z)^\<infinity> ⋅ y^\<infinity>" using ‹y^\⋆ ⋅ z ⋅ x ≤ x ⋅ y^\⋆ ⋅ z›
    by (metis iteration_sep mult.assoc)
  ultimately have "(x + y + z)^\<infinity> ≤ x^\<infinity> ⋅ (y + z)^\<infinity>"
    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^\<infinity> ⋅ y = y"
(*nitpick*)
oops

lemma iteration_idep: "x ⋅ y = 0 ==> x ⋅ y^\<infinity> = x"
  by (metis add_zeror annil iteration_unfoldl_distl)

text ‹Nitpick refutes the next lemma.›

lemma "y ⋅ w ≤ x ⋅ y + z ==> y ⋅ w^\<infinity> ≤ x^\<infinity> ⋅ 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^\<infinity> = b^\<star>"
  shows "s' ⋅ (a' + b)^\<infinity> ⋅ e' ≤ s ⋅ a^\<infinity> ⋅ e"
proof -
  have "z ⋅ b^\<star> ≤ z"
    by (metis assms(4) star_inductr_var)
  have "(z ⋅ a') ⋅ b^\<star> ≤ (a ⋅ z) ⋅ b^\<star>"
    by (metis assms(3) mult.assoc mult_isor)
  hence "z ⋅ (a' ⋅ b^\<star>)^\<infinity> ≤ a^\<infinity> ⋅ z" using ‹z ⋅ b^\⋆ ≤ z›
    by (metis mult.assoc mult_isol order_trans iteration_sim mult.assoc)
  have "s' ⋅ (a' + b)^\<infinity> ⋅ e' ≤ s' ⋅ b^\<star> ⋅ (a' ⋅ b^\<star>)^\<infinity> ⋅ e'"
    by (metis add.commute assms(5) eq_refl iteration_denest mult.assoc)
  also have "... ≤ s ⋅ z ⋅ b^\<star> ⋅ (a' ⋅ b^\<star>)^\<infinity> ⋅ e'"
    by (metis assms(1) mult_isor)
  also have "... ≤ s ⋅ z ⋅ (a' ⋅ b^\<star>)^\<infinity> ⋅ e'" using ‹z ⋅ b^\⋆ ≤ z›
    by (metis mult.assoc mult_isol mult_isor)
  also have "... ≤ s ⋅ a^\<infinity> ⋅ 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