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