Theory KAD.Domain_Semiring

(* Title:      Domain Semirings
   Author:     Victor B. F. Gomes, Walter Guttmann, Peter Höfner, Georg Struth, Tjark Weber
   Maintainer: Walter Guttmann <walter.guttman at canterbury.ac.nz>
               Georg Struth <g.struth at sheffield.ac.uk>
               Tjark Weber <tjark.weber at it.uu.se>
*)

section ‹Domain Semirings›

theory Domain_Semiring
imports Kleene_Algebra.Kleene_Algebra

begin

subsection ‹Domain Semigroups and Domain Monoids›

class domain_op =
  fixes domain_op :: "'a ⇒ 'a" ("d")

text ‹First we define the class of domain semigroups. Axioms are taken from~\<^cite>‹"DesharnaisJipsenStruth"›.›

class domain_semigroup = semigroup_mult + domain_op +
  assumes dsg1 [simp]: "d x ⋅ x = x"
  and dsg2 [simp]: "d (x ⋅ d y) = d (x ⋅ y)"
  and dsg3 [simp]: "d (d x ⋅ y) = d x ⋅ d y"
  and dsg4: "d x ⋅ d y = d y ⋅ d x"

begin

lemma domain_invol [simp]: "d (d x) = d x"
proof -
  have "d (d x) = d (d (d x ⋅ x))"
    by simp
  also have "... = d (d x ⋅ d x)"
    using dsg3 by presburger
  also have "... = d (d x ⋅ x)"
    by simp
  finally show ?thesis
    by simp
qed

text ‹The next lemmas show that domain elements form semilattices.›

lemma dom_el_idem [simp]: "d x ⋅ d x = d x"
proof -
  have "d x ⋅ d x = d (d x ⋅ x)"
    using dsg3 by presburger
  thus ?thesis
    by simp
qed

lemma dom_mult_closed [simp]: "d (d x ⋅ d y) = d x ⋅ d y"
  by simp

lemma dom_lc3 [simp]: "d x ⋅ d (x ⋅ y) = d (x ⋅ y)"
proof -
  have "d x ⋅ d (x ⋅ y) = d (d x ⋅ x ⋅ y)"
    using dsg3 mult_assoc by presburger
  thus ?thesis
    by simp
qed

lemma d_fixpoint: "(∃y. x = d y) ⟷ x = d x"
  by auto

lemma d_type: "∀P. (∀x. x = d x ⟶ P x) ⟷ (∀x. P (d x))"
  by (metis domain_invol)

text ‹We define the semilattice ordering on domain semigroups and explore the semilattice of domain elements from the order point of view.›

definition ds_ord :: "'a ⇒ 'a ⇒ bool" (infix "⊑" 50) where
  "x ⊑ y ⟷ x = d x ⋅ y"

lemma ds_ord_refl: "x ⊑ x"
  by (simp add: ds_ord_def)

lemma ds_ord_trans: "x ⊑ y ⟹ y ⊑ z ⟹ x ⊑ z"
proof -
  assume "x ⊑ y" and a: "y ⊑ z"
  hence b: "x = d x ⋅ y"
    using ds_ord_def by blast
  hence "x = d x ⋅ d y ⋅ z"
    using a ds_ord_def mult_assoc by force
  also have "... = d (d x ⋅ y) ⋅ z"
    by simp
  also have "... = d x ⋅ z"
    using b by auto
  finally show ?thesis
    using ds_ord_def by blast
qed

lemma ds_ord_antisym: "x ⊑ y ⟹ y ⊑ x ⟹ x = y"
proof -
  assume a: "x ⊑ y" and "y ⊑ x"
  hence b: "y = d y ⋅ x"
    using ds_ord_def by auto
  have "x = d x ⋅ d y ⋅ x"
    using a b ds_ord_def mult_assoc by force
  also have "... = d y ⋅ x"
    by (metis (full_types) b dsg3 dsg4)
  thus ?thesis
    using b calculation by presburger
qed

text ‹This relation is indeed an order.›

sublocale ds: ordering ‹(⊑)› ‹λx y. x ⊑ y ∧ x ≠ y›
proof
  show ‹x ⊑ y ∧ x ≠ y ⟷ x ⊑ y ∧ x ≠ y› for x y
    by (rule refl)
  show "x ⊑ x" for x
    by (rule ds_ord_refl)
  show "x ⊑ y ⟹ y ⊑ z ⟹ x ⊑ z" for x y z
    by (rule ds_ord_trans)
  show "x ⊑ y ⟹ y ⊑ x ⟹ x = y" for x y
    by (rule ds_ord_antisym)
qed

declare ds.refl [simp]

lemma ds_ord_eq: "x ⊑ d x ⟷ x = d x"
  by (simp add: ds_ord_def)

lemma "x ⊑ y ⟹ z ⋅ x ⊑ z ⋅ y"
(*nitpick [expect=genuine]*)
oops

lemma ds_ord_iso_right: "x ⊑ y ⟹ x ⋅ z ⊑ y ⋅ z"
proof -
  assume "x ⊑ y"
  hence a: "x = d x ⋅ y"
    by (simp add: ds_ord_def)
  hence "x ⋅ z = d x ⋅ y ⋅ z"
    by auto
  also have "... = d (d x ⋅ y ⋅ z) ⋅ d x ⋅ y ⋅ z"
    using dsg1 mult_assoc by presburger
  also have "... = d (x ⋅ z) ⋅ d x ⋅ y ⋅ z"
    using a by presburger
  finally show ?thesis
    using ds_ord_def dsg4 mult_assoc by auto
qed

text ‹The order on domain elements could as well be defined based on multiplication/meet.›

lemma ds_ord_sl_ord: "d x ⊑ d y ⟷ d x ⋅ d y = d x"
  using ds_ord_def by auto

lemma ds_ord_1: "d (x ⋅ y) ⊑ d x"
  by (simp add: ds_ord_sl_ord dsg4)

lemma ds_subid_aux: "d x ⋅ y ⊑ y"
  by (simp add: ds_ord_def mult_assoc)

lemma "y ⋅ d x ⊑ y"
(*nitpick [expect=genuine]*)
oops

lemma ds_dom_iso: "x ⊑ y ⟹ d x ⊑ d y"
proof -
  assume "x ⊑ y"
  hence "x = d x ⋅ y"
    by (simp add: ds_ord_def)
  hence "d x = d (d x ⋅ y)"
    by presburger
  also have "... = d x ⋅ d y"
    by simp
  finally show ?thesis
    using ds_ord_sl_ord by auto
qed

lemma ds_dom_llp: "x ⊑ d y ⋅ x ⟷ d x ⊑ d y"
proof
  assume "x ⊑ d y ⋅ x"
  hence "x = d y ⋅ x"
    by (simp add: ds_subid_aux ds.antisym)
  hence "d x = d (d y ⋅ x)"
    by presburger
  thus "d x ⊑ d y"
    using ds_ord_sl_ord dsg4 by force
next
  assume "d x ⊑ d y"
  thus "x ⊑ d y ⋅ x"
    by (metis (no_types) ds_ord_iso_right dsg1)
qed

lemma ds_dom_llp_strong: "x = d y ⋅ x ⟷ d x ⊑ d y"
  using ds.eq_iff
  by (simp add: ds_dom_llp ds.eq_iff ds_subid_aux)

definition refines :: "'a ⇒ 'a ⇒ bool"
  where "refines x y ≡ d y ⊑ d x ∧ (d y) ⋅ x ⊑ y"

lemma refines_refl: "refines x x"
  using refines_def by simp

lemma refines_trans: "refines x y ⟹ refines y z ⟹ refines x z"
  unfolding refines_def
  by (metis domain_invol ds.trans dsg1 dsg3 ds_ord_def)

lemma refines_antisym: "refines x y ⟹ refines y x ⟹ x = y"
  apply (rule ds.antisym)
   apply (simp_all add: refines_def)
   apply (metis ds_dom_llp_strong)
  apply (metis ds_dom_llp_strong)
  done

sublocale ref: ordering "refines" "λx y. (refines x y ∧ x ≠ y)"
proof
  show "⋀x y. refines x y ∧ x ≠ y ⟷ refines x y ∧ x ≠ y"
    ..
  show "⋀x. refines x x"
    by (rule refines_refl)
  show "⋀x y z. refines x y ⟹ refines y z ⟹ refines x z"
    by (rule refines_trans)
  show "⋀x y. refines x y ⟹ refines y x ⟹ x = y"
    by (rule refines_antisym)
qed

end

text ‹We expand domain semigroups to domain monoids.›

class domain_monoid = monoid_mult + domain_semigroup
begin

lemma dom_one [simp]: "d 1 = 1"
proof -
  have "1 = d 1 ⋅ 1"
    using dsg1 by presburger
  thus ?thesis
    by simp
qed

lemma ds_subid_eq: "x ⊑ 1 ⟷ x = d x"
  by (simp add: ds_ord_def)

end

subsection ‹Domain Near-Semirings›

text ‹The axioms for domain near-semirings are taken from~\<^cite>‹"DesharnaisStruthAMAST"›.›

class domain_near_semiring = ab_near_semiring + plus_ord + domain_op +
  assumes dns1 [simp]: "d x ⋅ x = x"
  and dns2 [simp]: "d (x ⋅ d y) = d(x ⋅ y)"
  and dns3 [simp]: "d (x + y) = d x + d y"
  and dns4: "d x ⋅ d y = d y ⋅ d x"
  and dns5 [simp]: "d x ⋅ (d x + d y) = d x"

begin

text ‹Domain near-semirings are automatically dioids; addition is idempotent.›

subclass near_dioid
proof
  show "⋀x. x + x = x"
  proof -
    fix x
    have a: "d x = d x ⋅ d (x + x)"
      using dns3 dns5 by presburger
    have "d (x + x) = d (x + x + (x + x)) ⋅ d (x + x)"
      by (metis (no_types) dns3  dns4 dns5)
    hence "d (x + x) = d (x + x) + d (x + x)"
      by simp
    thus "x + x = x"
      by (metis a dns1 dns4 distrib_right')
  qed
qed

text ‹Next we prepare to show that domain near-semirings are domain semigroups.›

lemma dom_iso: "x ≤ y ⟹ d x ≤ d y"
  using order_prop by auto

lemma dom_add_closed [simp]: "d (d x + d y) = d x + d y"
proof -
  have "d (d x + d y) = d (d x) + d (d y)"
    by simp
  thus ?thesis
    by (metis dns1 dns2 dns3 dns4)
qed

lemma dom_absorp_2 [simp]: "d x + d x ⋅ d y = d x"
proof -
  have "d x + d x ⋅ d y = d x ⋅ d x + d x ⋅ d y"
    by (metis add_idem' dns5)
  also have "... = (d x + d y) ⋅ d x"
    by (simp add: dns4)
  also have "... = d x ⋅ (d x + d y)"
    by (metis dom_add_closed dns4)
  finally show ?thesis
    by simp
qed

lemma dom_1: "d (x ⋅ y) ≤ d x"
proof -
  have "d (x ⋅ y) = d (d x ⋅ d (x ⋅ y))"
    by (metis dns1 dns2 mult_assoc)
  also have "... ≤ d (d x) + d (d x ⋅ d (x ⋅ y))"
    by simp
  also have "... = d (d x + d x ⋅ d (x ⋅ y))"
    using dns3  by presburger
  also have "... = d (d x)"
    by simp
  finally show ?thesis
    by (metis dom_add_closed add_idem')
qed

lemma dom_subid_aux2: "d x ⋅ y ≤ y"
proof -
  have "d x ⋅ y ≤ d (x + d y) ⋅ y"
    by (simp add: mult_isor)
  also have "... = (d x + d (d y)) ⋅ d y ⋅ y"
    using dns1 dns3 mult_assoc by presburger
  also have "... = (d y + d y ⋅ d x) ⋅ y"
    by (simp add: dns4 add_commute)
  finally show ?thesis
    by simp
qed

lemma dom_glb: "d x ≤ d y ⟹ d x ≤ d z ⟹ d x ≤ d y ⋅ d z"
  by (metis dns5 less_eq_def mult_isor)

lemma dom_glb_eq: "d x ≤ d y ⋅ d z ⟷ d x ≤ d y ∧ d x ≤ d z"
proof -
  have "d x ≤ d z ⟶ d x ≤ d z"
    by meson
  then show ?thesis
    by (metis (no_types) dom_absorp_2 dom_glb dom_subid_aux2 local.dual_order.trans local.join.sup.coboundedI2)
qed

lemma dom_ord: "d x ≤ d y ⟷ d x ⋅ d y = d x"
proof
  assume "d x ≤ d y"
  hence "d x + d y = d y"
    by (simp add: less_eq_def)
  thus "d x ⋅ d y = d x"
    by (metis dns5)
next
  assume "d x ⋅ d y = d x"
  thus "d x ≤ d y"
    by (metis dom_subid_aux2)
qed

lemma dom_export [simp]: "d (d x ⋅ y) = d x ⋅ d y"
proof (rule order.antisym)
  have "d (d x ⋅ y) = d (d (d x ⋅ y)) ⋅ d (d x ⋅ y)"
    using dns1 by presburger
  also have "... = d (d x ⋅ d y) ⋅ d (d x ⋅ y)"
    by (metis dns1 dns2 mult_assoc)
  finally show a: "d (d x ⋅ y) ≤ d x ⋅ d y"
    by (metis (no_types) dom_add_closed dom_glb dom_1 add_idem' dns2 dns4)
  have "d (d x ⋅ y) = d (d x ⋅ y) ⋅ d x"
    using a dom_glb_eq dom_ord by force
  hence "d x ⋅ d y = d (d x ⋅ y) ⋅ d y"
    by (metis dns1 dns2 mult_assoc)
  thus "d x ⋅ d y ≤ d (d x ⋅ y)"
    using a dom_glb_eq dom_ord by auto
qed

subclass domain_semigroup
 by (unfold_locales, auto simp: dns4)

text ‹We compare the domain semigroup ordering with that of the dioid.›

lemma d_two_orders: "d x ⊑ d y ⟷ d x ≤ d y"
  by (simp add: dom_ord ds_ord_sl_ord)

lemma two_orders: "x ⊑ y ⟹ x ≤ y"
  by (metis dom_subid_aux2 ds_ord_def)

lemma "x ≤ y ⟹ x ⊑ y"
(*nitpick [expect=genuine]*)
oops

text ‹Next we prove additional properties.›

lemma dom_subdist: "d x ≤ d (x + y)"
  by simp

lemma dom_distrib: "d x + d y ⋅ d z = (d x + d y) ⋅ (d x + d z)"
proof -
  have "(d x + d y) ⋅ (d x + d z) = d x ⋅ (d x + d z) + d y ⋅ (d x + d z)"
    using distrib_right' by blast
  also have "... = d x + (d x + d z) ⋅ d y"
    by (metis (no_types) dns3 dns5 dsg4)
  also have "... = d x + d x ⋅ d y + d z ⋅ d y"
    using add_assoc' distrib_right' by presburger
  finally show ?thesis
    by (simp add: dsg4)
qed

lemma dom_llp1: "x ≤ d y ⋅ x ⟹ d x ≤ d y"
proof -
  assume "x ≤ d y ⋅ x"
  hence "d x ≤ d (d y ⋅ x)"
    using dom_iso by blast
  also have "... = d y ⋅ d x"
    by simp
  finally show "d x ≤ d y"
    by (simp add: dom_glb_eq)
qed

lemma dom_llp2: "d x ≤ d y ⟹ x ≤ d y ⋅ x"
  using d_two_orders local.ds_dom_llp two_orders by blast

lemma dom_llp: "x ≤ d y ⋅ x ⟷ d x ≤ d y"
  using dom_llp1 dom_llp2 by blast

end

text ‹We expand domain near-semirings by an additive unit, using slightly different axioms.›

class domain_near_semiring_one = ab_near_semiring_one + plus_ord + domain_op +
  assumes dnso1 [simp]: "x + d x ⋅ x = d x ⋅ x"
  and dnso2 [simp]: "d (x ⋅ d y) = d (x ⋅ y)"
  and dnso3 [simp]: "d x + 1 = 1"
  and dnso4 [simp]: "d (x + y) = d x + d y"
  and dnso5: "d x ⋅ d y = d y ⋅ d x"

begin

text ‹The previous axioms are derivable.›

subclass domain_near_semiring
proof
  show a: "⋀x. d x ⋅ x = x"
    by (metis add_commute local.dnso3 local.distrib_right' local.dnso1 local.mult_onel)
  show "⋀x y. d (x ⋅ d y) = d (x ⋅ y)"
    by simp
  show "⋀x y. d (x + y) = d x + d y"
    by simp
  show "⋀x y. d x ⋅ d y = d y ⋅ d x"
    by (simp add: dnso5)
  show "⋀x y. d x ⋅ (d x + d y) = d x"
  proof -
    fix x y
    have "⋀x. 1 + d x = 1"
      using add_commute dnso3 by presburger
    thus "d x ⋅ (d x + d y) = d x"
      by (metis (no_types) a dnso2 dnso4 dnso5 distrib_right' mult_onel)
  qed
qed

subclass domain_monoid ..

lemma dom_subid: "d x ≤ 1"
  by (simp add: less_eq_def)

end

text ‹We add a left unit of multiplication.›

class domain_near_semiring_one_zerol = ab_near_semiring_one_zerol + domain_near_semiring_one +
  assumes dnso6 [simp]: "d 0 = 0"

begin

lemma domain_very_strict: "d x = 0 ⟷ x = 0"
  by (metis annil dns1 dnso6)

lemma dom_weakly_local: "x ⋅ y = 0 ⟷ x ⋅ d y = 0"
proof -
  have "x ⋅ y = 0 ⟷ d (x ⋅ y) = 0"
    by (simp add: domain_very_strict)
  also have "... ⟷ d (x ⋅ d y) = 0"
    by simp
  finally show ?thesis
    using domain_very_strict by blast
qed

end

subsection ‹Domain Pre-Dioids›

text ‹
  Pre-semirings with one and a left zero are automatically dioids.
  Hence there is no point defining domain pre-semirings separately from domain dioids. The axioms
are once again from~\<^cite>‹"DesharnaisStruthAMAST"›.
›

class domain_pre_dioid_one = pre_dioid_one + domain_op +
  assumes dpd1 : "x ≤ d x ⋅ x"
  and dpd2 [simp]: "d (x ⋅ d y) = d (x ⋅ y)"
  and dpd3 [simp]: "d x ≤ 1"
  and dpd4 [simp]: "d (x + y) = d x + d y"

begin

text ‹We prepare to show that every domain pre-dioid with one is a domain near-dioid with one.›

lemma dns1'' [simp]: "d x ⋅ x = x"
proof (rule order.antisym)
  show "d x ⋅ x ≤ x"
    using dpd3  mult_isor by fastforce
  show "x ≤ d x ⋅ x "
    by (simp add: dpd1)
qed

lemma d_iso: "x ≤ y ⟹ d x ≤ d y"
  by (metis dpd4 less_eq_def)

lemma domain_1'': "d (x ⋅ y) ≤ d x"
proof -
  have "d (x ⋅ y) = d (x ⋅ d y)"
    by simp
  also have "... ≤ d (x ⋅ 1)"
    by (meson d_iso dpd3 mult_isol)
  finally show ?thesis
    by simp
qed

lemma domain_export'' [simp]: "d (d x ⋅ y) = d x ⋅ d y"
proof (rule order.antisym)
  have one: "d (d x ⋅ y) ≤ d x"
    by (metis dpd2 domain_1'' mult_onel)
  have two: "d (d x ⋅ y) ≤ d y"
    using d_iso dpd3 mult_isor by fastforce
  have "d (d x ⋅ y) = d (d (d x ⋅ y)) ⋅ d (d x ⋅ y)"
    by simp
  also have "... = d (d x ⋅ y) ⋅ d (d x ⋅ y)"
    by (metis dns1'' dpd2 mult_assoc)
  thus "d (d x ⋅ y) ≤ d x ⋅ d y"
    using mult_isol_var one two by force
next
  have "d x ⋅ d y ≤ 1"
    by (metis dpd3  mult_1_right mult_isol order.trans)
  thus "d x ⋅ d y ≤ d (d x ⋅ y)"
    by (metis dns1'' dpd2 mult_isol mult_oner)
qed

lemma dom_subid_aux1'': "d x ⋅ y ≤ y"
proof -
  have "d x ⋅ y ≤ 1 ⋅ y"
    using dpd3 mult_isor by blast
  thus ?thesis
    by simp
qed

lemma dom_subid_aux2'': "x ⋅ d y ≤ x"
  using dpd3 mult_isol by fastforce

lemma d_comm: "d x ⋅ d y = d y ⋅ d x"
proof (rule order.antisym)
  have "d x ⋅ d y = (d x ⋅ d y) ⋅ (d x ⋅ d y)"
    by (metis dns1'' domain_export'')
  thus "d x ⋅ d y ≤ d y ⋅ d x"
    by (metis dom_subid_aux1'' dom_subid_aux2'' mult_isol_var)
next
  have "d y ⋅ d x = (d y ⋅ d x) ⋅ (d y ⋅ d x)"
    by (metis dns1'' domain_export'')
  thus "d y ⋅ d x ≤ d x ⋅ d y"
    by (metis dom_subid_aux1'' dom_subid_aux2'' mult_isol_var)
qed

subclass domain_near_semiring_one
  by (unfold_locales, auto simp: d_comm local.join.sup.absorb2)

lemma domain_subid: "x ≤ 1 ⟹ x ≤ d x"
  by (metis dns1 mult_isol mult_oner)

lemma d_preserves_equation: "d y ⋅ x ≤ x ⋅ d z ⟷ d y ⋅ x = d y ⋅ x ⋅ d z"
  by (metis dom_subid_aux2'' order.antisym local.dom_el_idem local.dom_subid_aux2 local.order_prop local.subdistl mult_assoc)

lemma d_restrict_iff: "(x ≤ y) ⟷ (x ≤ d x ⋅ y)"
  by (metis dom_subid_aux2 dsg1 less_eq_def order_trans subdistl)

lemma d_restrict_iff_1: "(d x ⋅ y ≤ z) ⟷ (d x ⋅ y ≤ d x ⋅ z)"
  by (metis dom_subid_aux2 domain_1'' domain_invol dsg1 mult_isol_var order_trans)

end

text ‹We add once more a left unit of multiplication.›

class domain_pre_dioid_one_zerol = domain_pre_dioid_one + pre_dioid_one_zerol +
  assumes dpd5 [simp]: "d 0 = 0"

begin

subclass domain_near_semiring_one_zerol
  by (unfold_locales, simp)

end

subsection ‹Domain Semirings›

text ‹We do not consider domain semirings without units separately at the moment. The axioms are taken from from~\<^cite>‹"DesharnaisStruthSCP"››

class domain_semiringl = semiring_one_zerol + plus_ord + domain_op +
  assumes dsr1 [simp]: "x + d x ⋅ x = d x ⋅ x"
  and dsr2 [simp]: "d (x ⋅ d y) = d (x ⋅ y)"
  and dsr3 [simp]: "d x + 1 = 1"
  and dsr4 [simp]: "d 0 = 0"
  and dsr5 [simp]: "d (x + y) = d x + d y"

begin

text ‹Every domain semiring is automatically a domain pre-dioid with one and left zero.›

subclass dioid_one_zerol
  by (standard, metis add_commute dsr1 dsr3 distrib_left mult_oner)

subclass domain_pre_dioid_one_zerol
  by (standard, auto simp: less_eq_def)

end

class domain_semiring = domain_semiringl + semiring_one_zero

subsection ‹The Algebra of Domain Elements›

text ‹We show that the domain elements of a domain semiring form a distributive lattice. Unfortunately we cannot prove this within the type class of domain semirings.›

typedef (overloaded)  'a d_element = "{x :: 'a :: domain_semiring. x = d x}"
  by (rule_tac x = 1 in exI, simp add: domain_subid ds.eq_iff)

setup_lifting type_definition_d_element

instantiation d_element :: (domain_semiring) bounded_lattice

begin

lift_definition less_eq_d_element :: "'a d_element ⇒ 'a d_element ⇒ bool" is "(≤)" .

lift_definition less_d_element :: "'a d_element ⇒ 'a d_element ⇒ bool" is "(<)" .

lift_definition bot_d_element :: "'a d_element" is 0
  by simp

lift_definition top_d_element :: "'a d_element" is 1
  by simp

lift_definition inf_d_element :: "'a d_element ⇒ 'a d_element ⇒ 'a d_element" is "(⋅)"
  by (metis dsg3)

lift_definition sup_d_element :: "'a d_element ⇒ 'a d_element ⇒ 'a d_element" is "(+)"
  by simp

instance
  apply (standard; transfer)
  apply (simp add: less_le_not_le)+
  apply (metis dom_subid_aux2'')
  apply (metis dom_subid_aux2)
  apply (metis dom_glb)
  apply simp+
  by (metis dom_subid)

end

instance d_element :: (domain_semiring) distrib_lattice
  by (standard, transfer, metis dom_distrib)

subsection ‹Domain Semirings with a Greatest Element›

text ‹If there is a greatest element in the semiring, then we have another equality.›

class domain_semiring_top = domain_semiring + order_top

begin

notation top ("⊤")

lemma kat_equivalence_greatest: "d x ≤ d y ⟷ x ≤ d y ⋅ ⊤"
proof
  assume "d x ≤ d y"
  thus "x ≤ d y ⋅ ⊤"
    by (metis dsg1 mult_isol_var top_greatest)
next
  assume "x ≤ d y ⋅ ⊤"
  thus "d x ≤ d y"
    using dom_glb_eq dom_iso by fastforce
qed

end

subsection ‹Forward Diamond Operators›

context domain_semiringl

begin

text ‹We define a forward diamond operator over a domain semiring. A more modular consideration is not given at the moment.›

definition fd :: "'a ⇒ 'a ⇒ 'a" ("( |_⟩ _)" [61,81] 82) where
  "|x⟩ y = d (x ⋅ y)"

lemma fdia_d_simp [simp]: "|x⟩ d y = |x⟩ y"
  by (simp add: fd_def)

lemma fdia_dom [simp]: "|x⟩ 1 = d x"
  by (simp add: fd_def)

lemma fdia_add1: "|x⟩ (y + z) = |x⟩ y + |x⟩ z"
  by (simp add: fd_def distrib_left)

lemma fdia_add2: "|x + y⟩ z = |x⟩ z + |y⟩ z"
  by (simp add: fd_def distrib_right)

lemma fdia_mult: "|x ⋅ y⟩ z = |x⟩ |y⟩ z"
  by (simp add: fd_def mult_assoc)

lemma fdia_one [simp]: "|1⟩ x = d x"
  by (simp add: fd_def)

lemma fdemodalisation1: "d z ⋅ |x⟩ y = 0 ⟷ d z ⋅ x ⋅ d y = 0"
proof -
  have "d z ⋅ |x⟩ y = 0 ⟷ d z ⋅ d (x ⋅ y) = 0"
    by (simp add: fd_def)
  also have "... ⟷ d z ⋅ x ⋅ y = 0"
    by (metis annil dnso6 dsg1 dsg3 mult_assoc)
  finally show ?thesis
    using dom_weakly_local by auto
qed

lemma fdemodalisation2: "|x⟩ y ≤ d z ⟷ x ⋅ d y ≤ d z ⋅ x"
proof
  assume "|x⟩ y ≤ d z"
  hence a: "d (x ⋅ d y) ≤ d z"
    by (simp add: fd_def)
  have "x ⋅ d y = d (x ⋅ d y) ⋅ x ⋅ d y"
    using dsg1 mult_assoc by presburger
  also have "... ≤ d z ⋅ x ⋅ d y"
    using a calculation dom_llp2 mult_assoc by auto
  finally show "x ⋅ d y ≤ d z ⋅ x"
    using dom_subid_aux2'' order_trans by blast
next
  assume "x ⋅ d y ≤ d z ⋅ x"
  hence "d (x ⋅ d y) ≤ d (d z ⋅ d x)"
    using dom_iso by fastforce
  also have "... ≤ d (d z)"
    using domain_1'' by blast
  finally show "|x⟩ y ≤ d z"
    by (simp add: fd_def)
qed

lemma fd_iso1: "d x ≤ d y ⟹ |z⟩ x ≤ |z⟩ y"
  using fd_def local.dom_iso local.mult_isol by fastforce

lemma fd_iso2: "x ≤ y ⟹ |x⟩ z ≤ |y⟩ z"
  by (simp add: fd_def dom_iso mult_isor)

lemma fd_zero_var [simp]: "|0⟩ x = 0"
  by (simp add: fd_def)

lemma fd_subdist_1: "|x⟩ y ≤ |x⟩ (y + z)"
  by (simp add: fd_iso1)

lemma fd_subdist_2: "|x⟩ (d y ⋅ d z) ≤ |x⟩ y"
  by (simp add: fd_iso1 dom_subid_aux2'')

lemma fd_subdist: "|x⟩ (d y ⋅ d z) ≤ |x⟩ y ⋅ |x⟩ z"
  using fd_def fd_iso1 fd_subdist_2 dom_glb dom_subid_aux2 by auto

lemma fdia_export_1: "d y ⋅ |x⟩ z = |d y ⋅ x⟩ z"
  by (simp add: fd_def mult_assoc)

end

context domain_semiring

begin

lemma fdia_zero [simp]: "|x⟩ 0 = 0"
  by (simp add: fd_def)

end

subsection ‹Domain Kleene Algebras›

text ‹We add the Kleene star to our considerations. Special domain axioms are not needed.›

class domain_left_kleene_algebra = left_kleene_algebra_zerol + domain_semiringl

begin

lemma dom_star [simp]: "d (x⇧⋆) = 1"
proof -
  have "d (x⇧⋆) = d (1 + x ⋅ x⇧⋆)"
    by simp
  also have "... = d 1 + d (x ⋅ x⇧⋆)"
    using dns3 by blast
  finally show ?thesis
    using add_commute local.dsr3 by auto
qed

lemma fdia_star_unfold [simp]: "|1⟩ y + |x⟩ |x⇧⋆⟩ y = |x⇧⋆⟩ y"
proof -
  have "|1⟩ y + |x⟩ |x⇧⋆⟩ y = |1 + x ⋅ x⇧⋆⟩ y"
    using local.fdia_add2 local.fdia_mult by presburger
  thus ?thesis
    by simp
qed

lemma fdia_star_unfoldr [simp]: "|1⟩ y + |x⇧⋆⟩ |x⟩ y = |x⇧⋆⟩ y"
proof -
  have "|1⟩ y + |x⇧⋆⟩ |x⟩ y = |1 + x⇧⋆ ⋅ x⟩ y"
    using fdia_add2 fdia_mult by presburger
  thus ?thesis
    by simp
qed

lemma fdia_star_unfold_var [simp]: "d y + |x⟩ |x⇧⋆⟩ y = |x⇧⋆⟩ y"
proof -
  have "d y + |x⟩ |x⇧⋆⟩ y = |1⟩ y + |x⟩ |x⇧⋆⟩ y"
    by simp
  also have "... = |1 + x ⋅ x⇧⋆⟩ y"
    using fdia_add2 fdia_mult by presburger
  finally show ?thesis
    by simp
qed

lemma fdia_star_unfoldr_var [simp]: "d y + |x⇧⋆⟩ |x⟩ y = |x⇧⋆⟩ y"
proof -
  have "d y + |x⇧⋆⟩ |x⟩ y = |1⟩ y + |x⇧⋆⟩ |x⟩ y"
    by simp
  also have "... = |1 + x⇧⋆ ⋅ x⟩ y"
    using fdia_add2 fdia_mult by presburger
  finally show ?thesis
    by simp
qed

lemma fdia_star_induct_var: "|x⟩ y ≤ d y ⟹ |x⇧⋆⟩ y ≤ d y"
proof -
  assume a1: "|x⟩ y ≤ d y"
  hence "x ⋅ d y ≤ d y ⋅ x"
    by (simp add: fdemodalisation2)
  hence "x⇧⋆ ⋅ d y ≤ d y ⋅ x⇧⋆"
    by (simp add: star_sim1)
  thus ?thesis
    by (simp add: fdemodalisation2)
qed

lemma fdia_star_induct: "d z + |x⟩ y ≤ d y ⟹ |x⇧⋆⟩ z ≤ d y"
proof -
  assume a: "d z + |x⟩ y ≤ d y"
  hence b: "d z ≤ d y" and c: "|x⟩ y ≤ d y"
    apply (simp add: local.join.le_supE)
    using a by auto
  hence d: "|x⇧⋆⟩ z ≤ |x⇧⋆⟩ y"
    using fd_def fd_iso1 by auto
  have "|x⇧⋆⟩ y ≤ d y"
    using c fdia_star_induct_var by blast
  thus ?thesis
    using d by fastforce
qed

lemma fdia_star_induct_eq: "d z + |x⟩ y = d y ⟹ |x⇧⋆⟩ z ≤ d y"
  by (simp add: fdia_star_induct)

end

class domain_kleene_algebra = kleene_algebra + domain_semiring

begin

subclass domain_left_kleene_algebra ..

end

end