Theory KAD.Antidomain_Semiring

(* Title:      Antidomain 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 ‹Antidomain Semirings›

theory Antidomain_Semiring
imports Domain_Semiring
begin

subsection ‹Antidomain Monoids›

text ‹We axiomatise antidomain monoids, using the axioms of~cite"DesharnaisJipsenStruth".›

class antidomain_op =
  fixes antidomain_op :: "'a  'a" ("ad")

class antidomain_left_monoid = monoid_mult + antidomain_op +
  assumes am1 [simp]: "ad x  x = ad 1"
  and am2: "ad x  ad y = ad y  ad x"
  and am3 [simp]: "ad (ad x)  x = x"
  and am4 [simp]: "ad (x  y)  ad (x  ad y) = ad x"
  and am5 [simp]: "ad (x  y)  x  ad y = ad (x  y)  x"

begin

no_notation domain_op ("d")
no_notation zero_class.zero ("0")

text ‹We define a zero element and operations of domain and addition.›

definition a_zero :: "'a" ("0") where
  "0 = ad 1"

definition am_d :: "'a  'a" ("d") where
   "d x = ad (ad x)"

definition am_add_op :: "'a  'a  'a" (infixl "" 65) where
  "x  y  ad (ad x  ad y)"

lemma a_d_zero [simp]: "ad x  d x = 0"
  by (metis am1 am2 a_zero_def am_d_def)

lemma a_d_one [simp]: "d x  ad x = 1"
  by (metis am1 am3 mult_1_right am_d_def am_add_op_def)

lemma n_annil [simp]: "0  x = 0"
proof -
  have "0  x = d x  ad x  x"
    by (simp add: a_zero_def am_d_def)
  also have "... = d x  0"
    by (metis am1 mult_assoc a_zero_def)
  thus ?thesis
    by (metis am1 am2 am3 mult_assoc a_zero_def)
qed

lemma a_mult_idem [simp]: "ad x  ad x = ad x"
proof -
  have "ad x  ad x = ad (1  x)  1  ad x"
    by simp
  also have "... = ad (1  x)  1"
    using am5 by blast
  finally show ?thesis
    by simp
qed

lemma a_add_idem [simp]: "ad x  ad x = ad x"
  by (metis am1 am3 am4 mult_1_right am_add_op_def)

text ‹The next three axioms suffice to show that the domain elements form a Boolean algebra.›

lemma a_add_comm: "x  y = y  x"
  using am2 am_add_op_def by auto

lemma a_add_assoc: "x  (y  z) = (x  y)  z"
proof -
  have "x y. ad x  ad (x  y) = ad x"
    by (metis a_mult_idem am2 am4 mult_assoc)
  thus ?thesis
    by (metis a_add_comm am_add_op_def local.am3 local.am4 mult_assoc)
qed

lemma huntington [simp]: "ad (x  y)  ad (x  ad y) = ad x"
  using a_add_idem am_add_op_def by auto

lemma a_absorb1 [simp]: "(ad x  ad y)  ad x = ad x"
  by (metis a_add_idem a_mult_idem am4 mult_assoc am_add_op_def)

lemma a_absorb2 [simp]: "ad x  ad x  ad y = ad x"
proof -
  have "ad (ad x)  ad (ad x  ad y) = ad (ad x)"
    by (metis (no_types) a_mult_idem local.am4 local.mult.semigroup_axioms semigroup.assoc)
  then show ?thesis
    using a_add_idem am_add_op_def by auto
qed

text ‹The distributivity laws remain to be proved; our proofs follow those of Maddux~cite"maddux".›

lemma prod_split [simp]: "ad x  ad y  ad x  d y = ad x"
  using a_add_idem am_d_def am_add_op_def by auto

lemma sum_split [simp]: "(ad x  ad y)  (ad x  d y) = ad x"
  using a_add_idem am_d_def am_add_op_def by fastforce

lemma a_comp_simp [simp]: "(ad x  ad y)  d x = ad y  d x"
proof -
  have f1: "(ad x  ad y)  d x = ad (ad (ad x)  ad (ad y))  ad (ad x)  ad (ad (ad y))"
    by (simp add: am_add_op_def am_d_def)
  have f2: "ad y = ad (ad (ad y))"
    using a_add_idem am_add_op_def by auto
  have "ad y = ad (ad (ad x)  ad (ad y))  ad y"
    by (metis (no_types) a_absorb1 a_add_comm am_add_op_def)
  then show ?thesis
    using f2 f1 by (simp add: am_d_def local.am2 local.mult.semigroup_axioms semigroup.assoc)
qed

lemma a_distrib1: "ad x  (ad y  ad z) = ad x  ad y  ad x  ad z"
proof -
  have f1: "a. ad (ad (ad (a::'a))  ad (ad a)) = ad a"
    using a_add_idem am_add_op_def by auto
  have f2: "a aa. ad ((a::'a)  aa)  (a  ad aa) = ad (a  aa)  a"
    using local.am5 mult_assoc by auto
  have f3: "a. ad (ad (ad (a::'a))) = ad a"
    using f1 by simp
  have "a. ad (a::'a)  ad a = ad a"
    by simp
  then have "a aa. ad (ad (ad (a::'a)  ad aa)) = ad aa  ad a"
    using f3 f2 by (metis (no_types) local.am2 local.am4 mult_assoc)
  then have  "ad x  (ad y  ad z) = ad x  (ad y  ad z)  ad y  ad x  (ad y  ad z)  d y"
    using am_add_op_def am_d_def local.am2 local.am4 by presburger
  also have "... = ad x  ad y  ad x  (ad y  ad z)  d y"
    by (simp add: mult_assoc)
  also have "... = ad x  ad y  ad x  ad z  d y"
    by (simp add: mult_assoc)
  also have "... = ad x  ad y  ad x  ad y  ad z  ad x  ad z  d y"
    by (metis a_add_idem a_mult_idem local.am4 mult_assoc am_add_op_def)
  also have "... = ad x  ad y  (ad x  ad z  ad y  ad x  ad z  d y)"
    by (metis am2 mult_assoc a_add_assoc)
  finally show ?thesis
    by (metis a_add_idem a_mult_idem am4 am_d_def am_add_op_def)
qed

lemma a_distrib2: "ad x  ad y  ad z = (ad x  ad y)  (ad x  ad z)"
proof -
  have f1: "a aa ab. ad (ad (ad (a::'a)  ad aa)  ad (ad a  ad ab)) = ad a  ad (ad (ad aa)  ad (ad ab))"
    using a_distrib1 am_add_op_def by auto
  have "a. ad (ad (ad (a::'a))) = ad a"
    by (metis a_absorb2 a_mult_idem am_add_op_def)
  then have "ad (ad (ad x)  ad (ad y))  ad (ad (ad x)  ad (ad z)) = ad (ad (ad x)  ad (ad y  ad z))"
    using f1 by (metis (full_types))
  then show ?thesis
    by (simp add: am_add_op_def)
qed

lemma aa_loc [simp]: "d (x  d y) = d (x  y)"
proof -
  have f1: "x  d y  y = x  y"
    by (metis am3 mult_assoc am_d_def)
  have f2: "w z. ad (w  z)  (w  ad z) = ad (w  z)  w"
    by (metis am5 mult_assoc)
  hence f3: "z. ad (x  y)  (x  z) = ad (x  y)  (x  (ad (ad (ad y)  y)  z))"
    using f1 by (metis (no_types) mult_assoc am_d_def)
  have "ad (x  ad (ad y))  (x  y) = 0" using f1
    by (metis am1 mult_assoc n_annil a_zero_def am_d_def)
  thus ?thesis
    by (metis a_d_zero am_d_def f3 local.am1 local.am2 local.am3 local.am4)
qed

lemma a_loc [simp]: "ad (x  d y) = ad (x  y)"
proof -
  have "a. ad (ad (ad (a::'a))) = ad a"
    using am_add_op_def am_d_def prod_split by auto
  then show ?thesis
    by (metis (full_types) aa_loc am_d_def)
qed

lemma d_a_export [simp]: "d (ad x  y) = ad x  d y"
proof -
  have f1: "a aa. ad ((a::'a)  ad (ad aa)) = ad (a  aa)"
    using a_loc am_d_def by auto
  have "a. ad (ad (a::'a)  a) = 1"
    using a_d_one am_add_op_def am_d_def by auto
  then have "a aa. ad (ad (ad (a::'a)  ad aa)) = ad a  ad aa"
    using f1 by (metis a_distrib2 am_add_op_def local.mult_1_left)
  then show ?thesis
    using f1 by (metis (no_types) am_d_def)
qed

text ‹Every antidomain monoid is a domain monoid.›

sublocale dm: domain_monoid am_d "(⋅)" 1
  apply (unfold_locales)
  apply (simp add: am_d_def)
  apply simp
  using am_d_def d_a_export apply auto[1]
  by (simp add: am_d_def local.am2)

lemma ds_ord_iso1: "x  y  z  x  z  y"
(*nitpick [expect=genuine]*)
oops

lemma a_very_costrict: "ad x = 1  x = 0"
proof
  assume a: "ad x = 1"
  hence "0 = ad x  x"
    using a_zero_def by force
  thus "x = 0"
    by (simp add: a)
next
  assume "x = 0"
  thus "ad x = 1"
    using a_zero_def am_d_def dm.dom_one by auto
qed

lemma a_weak_loc: "x  y = 0  x  d y = 0"
proof -
  have "x  y = 0  ad (x  y) = 1"
    by (simp add: a_very_costrict)
  also have "...  ad (x  d y) = 1"
    by simp
  finally show ?thesis
    using a_very_costrict by blast
qed

lemma a_closure [simp]: "d (ad x) = ad x"
  using a_add_idem am_add_op_def am_d_def by auto

lemma a_d_mult_closure [simp]: "d (ad x  ad y) = ad x  ad y"
  by simp

lemma kat_3': "d x  y  ad z = 0  d x  y = d x  y  d z"
  by (metis dm.dom_one local.am5 local.mult_1_left a_zero_def am_d_def)

lemma s4 [simp]: "ad x  ad (ad x  y) = ad x  ad y"
proof -
  have "a aa. ad (a::'a)  ad (ad aa) = ad (ad (ad a  aa))"
    using am_d_def d_a_export by presburger
  then have "a aa. ad (ad (a::'a))  ad aa = ad (ad (ad aa  a))"
    using local.am2 by presburger
  then show ?thesis
    by (metis a_comp_simp a_d_mult_closure am_add_op_def am_d_def local.am2)
qed

end

class antidomain_monoid = antidomain_left_monoid +
  assumes am6 [simp]: "x  ad 1 = ad 1"

begin

lemma kat_3_equiv: "d x  y  ad z = 0  d x  y = d x  y  d z"
  apply standard
  apply (metis kat_3')
  by (simp add: mult_assoc a_zero_def am_d_def)

no_notation a_zero ("0")
no_notation am_d ("d")

end

subsection ‹Antidomain Near-Semirings›

text ‹We define antidomain near-semirings. We do not consider units separately. The axioms are taken from~cite"DesharnaisStruthAMAST".›

notation zero_class.zero ("0")

class antidomain_near_semiring = ab_near_semiring_one_zerol + antidomain_op + plus_ord +
  assumes ans1 [simp]: "ad x  x = 0"
  and ans2 [simp]: "ad (x  y) + ad (x  ad (ad y)) = ad (x  ad (ad y))"
  and ans3 [simp]: "ad (ad x) + ad x = 1"
  and ans4 [simp]: "ad (x + y) = ad x  ad y"

begin

definition ans_d :: "'a  'a" ("d") where
   "d x = ad (ad x)"

lemma a_a_one [simp]: "d 1 = 1"
proof -
  have "d 1 = d 1 + 0"
    by simp
  also have "... = d 1 + ad 1"
    by (metis ans1 mult_1_right)
  finally show ?thesis
    by (simp add: ans_d_def)
qed

lemma a_very_costrict': "ad x = 1  x = 0"
proof
  assume "ad x = 1"
  hence "x = ad x  x"
    by simp
  thus "x = 0"
    by auto
next
  assume "x = 0"
  hence "ad x = ad 0"
    by blast
  thus "ad x = 1"
    by (metis a_a_one ans_d_def local.ans1 local.mult_1_right)
qed

lemma one_idem [simp]: "1 + 1 = 1"
proof -
  have "1 + 1 = d 1 + d 1"
    by simp
  also have "... = ad (ad 1  1) + ad (ad 1  d 1)"
    using a_a_one ans_d_def by auto
  also have "... = ad (ad 1  d 1)"
    using ans_d_def local.ans2 by presburger
  also have "... = ad (ad 1  1)"
    by simp
  also have "... = d 1"
    by (simp add: ans_d_def)
  finally show ?thesis
    by simp
qed

text ‹Every antidomain near-semiring is automatically a dioid, and therefore ordered.›

subclass near_dioid_one_zerol
proof
  show "x. x + x = x"
  proof -
    fix x
    have "x + x = 1  x + 1  x"
      by simp
    also have "... = (1 + 1)  x"
      using distrib_right' by presburger
    finally show "x + x = x"
      by simp
  qed
qed

lemma d1_a [simp]: "d x  x = x"
proof -
  have "x = (d x + ad x)  x"
    by (simp add: ans_d_def)
  also have "... = d x  x + ad x  x"
    using distrib_right' by blast
  also have "... = d x  x + 0"
    by simp
  finally show ?thesis
    by auto
qed

lemma a_comm: "ad x  ad y = ad y  ad x"
  using add_commute ans4 by fastforce

lemma a_subid: "ad x  1"
  using local.ans3 local.join.sup_ge2 by fastforce

lemma a_subid_aux1: "ad x  y  y"
  using a_subid mult_isor by fastforce

lemma a_subdist: "ad (x + y)  ad x"
  by (metis a_subid_aux1 ans4 add_comm)

lemma a_antitone: "x  y  ad y  ad x"
  using a_subdist local.order_prop by auto

lemma a_mul_d [simp]: "ad x  d x = 0"
  by (metis a_comm ans_d_def local.ans1)

lemma a_gla1: "ad x  y = 0  ad x  ad y"
proof -
  assume "ad x  y = 0"
  hence a: "ad x  d y = 0"
    by (metis a_subid a_very_costrict' ans_d_def local.ans2 local.join.sup.order_iff)
  have "ad x = (d y + ad y )  ad x"
    by (simp add: ans_d_def)
  also have "... = d y  ad x + ad y  ad x"
    using distrib_right' by blast
  also have "... = ad x  d y + ad x  ad y"
    using a_comm ans_d_def by auto
  also have "... = ad x  ad y"
    by (simp add: a)
  finally show "ad x  ad y"
    by (metis a_subid_aux1)
qed

lemma a_gla2: "ad x  ad y  ad x  y = 0"
proof -
  assume "ad x  ad y"
  hence "ad x  y  ad y  y"
    using mult_isor by blast
  thus ?thesis
    by (simp add: join.le_bot)
qed

lemma a2_eq [simp]: "ad (x  d y) = ad (x  y)"
proof (rule order.antisym)
  show "ad (x  y)  ad (x  d y)"
    by (simp add: ans_d_def local.less_eq_def)
next
  show "ad (x  d y)  ad (x  y)"
    by (metis a_gla1 a_mul_d ans1 d1_a mult_assoc)
qed

lemma a_export' [simp]: "ad (ad x  y) = d x + ad y"
proof (rule order.antisym)
  have "ad (ad x  y)  ad x  d y = 0"
    by (simp add: a_gla2 local.mult.semigroup_axioms semigroup.assoc)
  hence a: "ad (ad x  y)  d y  ad (ad x)"
    by (metis a_comm a_gla1 ans4 mult_assoc ans_d_def)
  have "ad (ad x  y) = ad (ad x  y)  d y + ad (ad x  y)  ad y"
    by (metis (no_types) add_commute ans3 ans4 distrib_right' mult_onel ans_d_def)
  thus "ad (ad x  y)  d x + ad y"
    by (metis a_subid_aux1 a join.sup_mono ans_d_def)
next
  show "d x + ad y  ad (ad x  y)"
    by (metis a2_eq a_antitone a_comm a_subid_aux1 join.sup_least ans_d_def)
qed

text ‹Every antidomain near-semiring is a domain near-semiring.›

sublocale dnsz: domain_near_semiring_one_zerol "(+)" "(⋅)" 1 0 "ans_d" "(≤)" "(<)"
  apply (unfold_locales)
  apply simp
  using a2_eq ans_d_def apply auto[1]
  apply (simp add: a_subid ans_d_def local.join.sup_absorb2)
  apply (simp add: ans_d_def)
  apply (simp add: a_comm ans_d_def)
  using a_a_one a_very_costrict' ans_d_def by force

lemma a_idem [simp]: "ad x  ad x = ad x"
proof -
  have "ad x = (d x + ad x )  ad x"
    by (simp add: ans_d_def)
  also have "... = d x  ad x + ad x  ad x"
    using distrib_right' by blast
  finally show ?thesis
    by (simp add: ans_d_def)
qed

lemma a_3_var [simp]: "ad x  ad y  (x + y) = 0"
  by (metis ans1 ans4)

lemma a_3 [simp]: "ad x  ad y  d (x + y) = 0"
  by (metis a_mul_d ans4)

lemma a_closure' [simp]: "d (ad x) = ad x"
proof -
  have "d (ad x) = ad (1  d x)"
    by (simp add: ans_d_def)
  also have "... = ad (1  x)"
    using a2_eq by blast
  finally show ?thesis
    by simp
qed

text ‹The following counterexamples show that some of the antidomain monoid axioms do not need to hold.›

lemma "x  ad 1 = ad 1"
(*nitpick [expect=genuine]*)
oops

lemma "ad (x  y)  ad (x  ad y) = ad x"
(*nitpick [expect=genuine]*)
oops

lemma "ad (x  y)  ad (x  ad y) = ad x"
(*nitpick [expect=genuine]*)
oops

lemma phl_seq_inv: "d v  x  y  ad w = 0  z. d v  x  d z = 0  ad z  y  ad w = 0"
proof -
  assume "d v  x  y  ad w = 0"
  hence "d v  x  d (y  ad w) = 0  ad (y  ad w)  y  ad w = 0"
    by (metis dnsz.dom_weakly_local local.ans1 mult_assoc)
  thus "z. d v  x  d z = 0  ad z  y  ad w = 0"
    by blast
qed

lemma a_fixpoint: "ad x = x  (y. y = 0)"
proof -
  assume a1: "ad x = x"
  { fix aa :: 'a
    have "aa = 0"
      using a1 by (metis (no_types) a_mul_d ans_d_def local.annil local.ans3 local.join.sup.idem local.mult_1_left)
  }
  then show ?thesis
    by blast
qed

no_notation ans_d ("d")

end

subsection ‹Antidomain Pre-Dioids›

text ‹Antidomain pre-diods are based on a different set of axioms, which are again taken from~cite"DesharnaisStruthAMAST".›

class antidomain_pre_dioid = pre_dioid_one_zerol + antidomain_op +
  assumes apd1 [simp]: "ad x  x = 0"
  and apd2 [simp]: "ad (x  y)  ad (x  ad (ad y))"
  and apd3 [simp]: "ad (ad x) + ad x = 1"

begin

definition apd_d :: "'a  'a" ("d") where
   "d x = ad (ad x)"

lemma a_very_costrict'': "ad x = 1  x = 0"
  by (metis add_commute local.add_zerol order.antisym local.apd1 local.apd3 local.join.bot_least local.mult_1_right local.phl_skip)

lemma a_subid': "ad x  1"
  using local.apd3 local.join.sup_ge2 by fastforce

lemma d1_a' [simp]: "d x  x = x"
proof -
  have "x = (d x + ad x)  x"
    by (simp add: apd_d_def)
  also have "... = d x  x + ad x  x"
    using distrib_right' by blast
  also have "... = d x  x + 0"
    by simp
  finally show ?thesis
    by auto
qed

lemma a_subid_aux1': "ad x  y  y"
  using a_subid' mult_isor by fastforce

lemma a_mul_d' [simp]: "ad x  d x = 0"
proof -
  have "1 = ad (ad x  x)"
    using a_very_costrict'' by force
  thus ?thesis
    by (metis a_subid' a_very_costrict'' apd_d_def order.antisym local.apd2)
qed

lemma a_d_closed [simp]: "d (ad x) = ad x"
proof (rule order.antisym)
  have "d (ad x) = (d x + ad x)  d (ad x)"
    by (simp add: apd_d_def)
  also have "... = ad (ad x)  ad (d x) + ad x  d (ad x)"
    using apd_d_def local.distrib_right' by presburger
  also have "... = ad x  d (ad x)"
    using a_mul_d' apd_d_def by auto
      finally show "d (ad x)  ad x"
    by (metis a_subid' mult_1_right mult_isol apd_d_def)
next
  have "ad x = ad (1  x)"
    by simp
  also have "...  ad (1  d x)"
    using apd_d_def local.apd2 by presburger
  also have "... = ad (d x)"
    by simp
  finally show "ad x  d (ad x)"
   by (simp add: apd_d_def)
qed

lemma meet_ord_def: "ad x  ad y  ad x  ad y = ad x"
  by (metis a_d_closed a_subid_aux1' d1_a' order.eq_iff mult_1_right mult_isol)

lemma d_weak_loc: "x  y = 0  x  d y = 0"
proof -
  have "x  y = 0  ad (x  y) = 1"
    by (simp add: a_very_costrict'')
  also have "...  ad (x  d y) = 1"
    by (metis apd1 apd2 a_subid' apd_d_def d1_a' order.eq_iff mult_1_left mult_assoc)
  finally show ?thesis
    by (simp add: a_very_costrict'')
qed

lemma gla_1: "ad x  y = 0  ad x  ad y"
proof -
  assume "ad x  y = 0"
  hence a: "ad x  d y = 0"
    using d_weak_loc by force
  hence "d y = ad x  d y + d y"
    by simp
  also have "... = (1 + ad x)  d y"
    using join.sup_commute by auto
  also have "... = (d x + ad x)  d y"
    using apd_d_def calculation by auto
  also have "... = d x  d y"
    by (simp add: a join.sup_commute)
  finally have "d y  d x"
    by (metis apd_d_def a_subid' mult_1_right mult_isol)
  hence "d y  ad x = 0"
    by (metis apd_d_def a_d_closed a_mul_d' distrib_right' less_eq_def no_trivial_inverse)
  hence "ad x = ad y  ad x"
    by (metis apd_d_def apd3 add_0_left distrib_right' mult_1_left)
  thus "ad x  ad y"
    by (metis add_commute apd3 mult_oner subdistl)
qed

lemma a2_eq' [simp]: "ad (x  d y) = ad (x  y)"
proof (rule order.antisym)
  show "ad (x  y)  ad (x  d y)"
    by (simp add: apd_d_def)
next
  show "ad (x  d y)  ad (x  y)"
    by (metis gla_1 apd1 a_mul_d' d1_a' mult_assoc)
qed

lemma a_supdist_var: "ad (x + y)  ad x"
  by (metis gla_1 apd1 join.le_bot subdistl)

lemma a_antitone': "x  y  ad y  ad x"
  using a_supdist_var local.order_prop by auto

lemma a_comm_var: "ad x  ad y  ad y  ad x"
proof -
  have "ad x  ad y = d (ad x  ad y)  ad x  ad y"
    by (simp add: mult_assoc)
  also have "...  d (ad x  ad y)  ad x"
    using a_subid' mult_isol by fastforce
  also have "...  d (ad y)  ad x"
    by (simp add: a_antitone' a_subid_aux1' apd_d_def local.mult_isor)
  finally show ?thesis
    by simp
qed

lemma a_comm': "ad x  ad y = ad y  ad x"
  by (simp add: a_comm_var order.eq_iff)

lemma a_closed [simp]: "d (ad x  ad y) = ad x  ad y"
proof -
  have f1: "x y. ad x  ad (ad y  x)"
    by (simp add: a_antitone' a_subid_aux1')
  have "x y. d (ad x  y)  ad x"
    by (metis a2_eq' a_antitone' a_comm' a_d_closed apd_d_def f1)
  hence "x y. d (ad x  y)  y = ad x  y"
    by (metis d1_a' meet_ord_def mult_assoc apd_d_def)
  thus ?thesis
    by (metis f1 a_comm' apd_d_def meet_ord_def)
qed

lemma a_export'' [simp]: "ad (ad x  y) = d x + ad y"
proof (rule order.antisym)
  have "ad (ad x  y)  ad x  d y = 0"
    using d_weak_loc mult_assoc by fastforce
  hence a: "ad (ad x  y)  d y  d x"
    by (metis a_closed a_comm' apd_d_def gla_1 mult_assoc)
  have "ad (ad x  y) = ad (ad x  y)  d y + ad (ad x  y)  ad y"
    by (metis apd3 a_comm' d1_a' distrib_right' mult_1_right apd_d_def)
  thus "ad (ad x  y)  d x + ad y"
    by (metis a_subid_aux1' a join.sup_mono)
next
  have "ad y  ad (ad x  y)"
    by (simp add: a_antitone' a_subid_aux1')
  thus "d x + ad y  ad (ad x  y)"
    by (metis apd_d_def a_mul_d' d1_a' gla_1 apd1 join.sup_least mult_assoc)
qed

lemma d1_sum_var: "x + y  (d x + d y)  (x + y)"
proof -
  have "x + y = d x  x + d y  y"
    by simp
  also have "...  (d x + d y)  x + (d x + d y)  y"
    using local.distrib_right' local.join.sup_ge1 local.join.sup_ge2 local.join.sup_mono by presburger
  finally show ?thesis
    using order_trans subdistl_var by blast
qed

lemma a4': "ad (x + y) = ad x  ad y"
proof (rule order.antisym)
  show "ad (x + y)  ad x  ad y"
    by (metis a_d_closed a_supdist_var add_commute d1_a' local.mult_isol_var)
  hence "ad x  ad y = ad x  ad y + ad (x + y)"
    using less_eq_def add_commute by simp
  also have "... = ad (ad (ad x  ad y)  (x + y))"
    by (metis a_closed a_export'')
  finally show "ad x  ad y  ad (x + y)"
    using a_antitone' apd_d_def d1_sum_var by auto
qed

text ‹Antidomain pre-dioids are domain pre-dioids and antidomain near-semirings, but still not antidomain monoids.›

sublocale dpdz: domain_pre_dioid_one_zerol "(+)" "(⋅)" 1 0 "(≤)" "(<)" "λx. ad (ad x)"
  apply (unfold_locales)
  using apd_d_def d1_a' apply auto[1]
  using a2_eq' apd_d_def apply auto[1]
  apply (simp add: a_subid')
  apply (simp add: a4' apd_d_def)
  by (metis a_mul_d' a_very_costrict'' apd_d_def local.mult_onel)

subclass antidomain_near_semiring
  apply (unfold_locales)
  apply simp
  using local.apd2 local.less_eq_def apply blast
  apply simp
  by (simp add: a4')

lemma a_supdist: "ad (x + y)  ad x + ad y"
  using a_supdist_var local.join.le_supI1 by auto

lemma a_gla: "ad x  y = 0  ad x  ad y"
  using gla_1 a_gla2 by blast

lemma a_subid_aux2: "x  ad y  x"
  using a_subid' mult_isol by fastforce

lemma a42_var: "d x  d y  ad (ad x + ad y)"
  by (simp add: apd_d_def)

lemma d1_weak [simp]: "(d x + d y)  x = x"
proof -
  have "(d x + d y)  x = (1 + d y)  x"
    by simp
  thus ?thesis
   by (metis add_commute apd_d_def dpdz.dnso3 local.mult_1_left)
qed

lemma "x  ad 1 = ad 1"
(*nitpick [expect=genuine]*)
oops

lemma "ad x  (y + z) = ad x  y + ad x  z"
(*nitpick [expect=genuine]*)
oops

lemma "ad (x  y)  ad (x  ad y) = ad x"
(*nitpick [expect=genuine]*)
oops

lemma "ad (x  y)  ad (x  ad y) = ad x"
(*nitpick [expect=genuine]*)
oops

no_notation apd_d ("d")

end

subsection ‹Antidomain Semirings›

text ‹Antidomain semirings are direct expansions of antidomain pre-dioids, but do not require idempotency of addition. Hence we give a slightly different axiomatisation, following~cite"DesharnaisStruthSCP".›

class antidomain_semiringl = semiring_one_zerol + plus_ord + antidomain_op +
  assumes as1 [simp]: "ad x  x = 0"
  and as2 [simp]: "ad (x  y) + ad (x  ad (ad y)) = ad (x  ad (ad y))"
  and as3 [simp]: "ad (ad x) + ad x = 1"

begin

definition ads_d :: "'a  'a" ("d") where
  "d x = ad (ad x)"

lemma one_idem': "1 + 1 = 1"
  by (metis as1 as2 as3 add_zeror mult.right_neutral)

text ‹Every antidomain semiring is a dioid and an antidomain pre-dioid.›

subclass dioid
  by (standard, metis distrib_left mult.right_neutral one_idem')

subclass antidomain_pre_dioid
  by (unfold_locales, auto simp: local.less_eq_def)

lemma am5_lem [simp]: "ad (x  y)  ad (x  ad y) = ad x"
proof -
  have "ad (x  y )  ad (x  ad y) = ad (x  d y)  ad (x  ad y)"
    using ads_d_def local.a2_eq' local.apd_d_def by auto
  also have "... = ad (x  d y + x  ad y)"
    using ans4 by presburger
  also have "... = ad (x  (d y + ad y))"
    using distrib_left by presburger
  finally show ?thesis
    by (simp add: ads_d_def)
qed

lemma am6_lem [simp]: "ad (x  y)  x  ad y = ad (x  y)  x"
proof -
  fix x y
  have "ad (x  y)  x  ad y = ad (x  y)  x  ad y + 0"
    by simp
  also have "... = ad (x  y)  x  ad y + ad (x  d y)  x  d y"
    using ans1 mult_assoc by presburger
  also have "... = ad (x  y)  x  (ad y + d y)"
    using ads_d_def local.a2_eq' local.apd_d_def local.distrib_left by auto
  finally show "ad (x  y)  x  ad y = ad (x  y)  x"
    using add_commute ads_d_def local.as3 by auto
qed

lemma a_zero [simp]: "ad 0 = 1"
  by (simp add: local.a_very_costrict'')

lemma a_one [simp]: "ad 1 = 0"
  using a_zero local.dpdz.dpd5 by blast

subclass antidomain_left_monoid
  by (unfold_locales, auto simp:  local.a_comm')

text ‹Every antidomain left semiring is a domain left semiring.›

no_notation domain_semiringl_class.fd ("( |_ _)" [61,81] 82)

definition fdia :: "'a  'a  'a" ("( |_ _)" [61,81] 82) where
  "|x y = ad (ad (x  y))"

sublocale ds: domain_semiringl "(+)" "(⋅)" 1 0 "λx. ad (ad x)" "(≤)" "(<)"
  rewrites "ds.fd x y  fdia x y"
proof -
  show "class.domain_semiringl (+) (⋅) 1 0 (λx. ad (ad x)) (≤) (<) "
    by (unfold_locales, auto simp: local.dpdz.dpd4 ans_d_def)
  then interpret ds: domain_semiringl "(+)" "(⋅)" 1 0 "λx. ad (ad x)" "(≤)" "(<)" .
  show "ds.fd x y  fdia x y"
    by (auto simp: fdia_def ds.fd_def)
qed

lemma fd_eq_fdia [simp]: "domain_semiringl.fd (⋅) d x y  fdia x y"
proof -
  have "class.domain_semiringl (+) (⋅) 1 0 d (≤) (<)"
    by (unfold_locales, auto simp: ads_d_def local.ans_d_def)
  hence "domain_semiringl.fd (⋅) d x y = d ((⋅) x y)"
    by (rule domain_semiringl.fd_def)
  also have "... = ds.fd x y"
    by (simp add: ds.fd_def ads_d_def)
  finally show "domain_semiringl.fd (⋅) d x y  |x y"
    by auto
qed

end

class antidomain_semiring = antidomain_semiringl + semiring_one_zero

begin

text ‹Every antidomain semiring is an antidomain monoid.›

subclass antidomain_monoid
  by (standard, metis ans1 mult_1_right annir)

lemma "a_zero = 0"
  by (simp add: local.a_zero_def)

sublocale ds: domain_semiring "(+)" "(⋅)" 1 0 "λx. ad (ad x)" "(≤)" "(<)"
  rewrites "ds.fd x y  fdia x y"
  by unfold_locales

end

subsection ‹The Boolean Algebra of Domain Elements›

typedef (overloaded) 'a a2_element = "{x :: 'a :: antidomain_semiring. x = d x}"
  by (rule_tac x=1 in exI, auto simp: ads_d_def)

setup_lifting type_definition_a2_element

instantiation a2_element :: (antidomain_semiring) boolean_algebra

begin

lift_definition less_eq_a2_element :: "'a a2_element  'a a2_element  bool" is "(≤)" .

lift_definition less_a2_element :: "'a a2_element  'a a2_element  bool" is "(<)" .

lift_definition bot_a2_element :: "'a a2_element" is 0
  by (simp add: ads_d_def)

lift_definition top_a2_element :: "'a a2_element" is 1
  by (simp add: ads_d_def)

lift_definition inf_a2_element :: "'a a2_element  'a a2_element  'a a2_element" is "(⋅)"
  by (metis (no_types, lifting) ads_d_def dpdz.dom_mult_closed)

lift_definition sup_a2_element :: "'a a2_element  'a a2_element  'a a2_element" is "(+)"
  by (metis ads_d_def ds.dsr5)

lift_definition minus_a2_element :: "'a a2_element  'a a2_element  'a a2_element" is "λx y. x  ad y"
  by (metis (no_types, lifting) ads_d_def dpdz.domain_export'')

lift_definition uminus_a2_element :: "'a a2_element  'a a2_element" is antidomain_op
  by (simp add: ads_d_def)

instance
  apply (standard; transfer)
  apply (simp add: less_le_not_le)
  apply simp
  apply auto[1]
  apply simp
  apply (metis a_subid_aux2 ads_d_def)
  apply (metis a_subid_aux1' ads_d_def)
  apply (metis (no_types, lifting) ads_d_def dpdz.dom_glb)
  apply simp
  apply simp
  apply simp
  apply simp
  apply (metis a_subid' ads_d_def)
  apply (metis (no_types, lifting) ads_d_def dpdz.dom_distrib)
  apply (metis ads_d_def ans1)
  apply (metis ads_d_def ans3)
  by simp

end

subsection ‹Further Properties›

context antidomain_semiringl

begin

lemma a_2_var: "ad x  d y = 0  ad x  ad y"
  using local.a_gla local.ads_d_def local.dpdz.dom_weakly_local by auto

text ‹The following two lemmas give the Galois connection of Heyting algebras.›

lemma da_shunt1: "x  d y + z  x  ad y  z"
proof -
  assume "x  d y + z"
  hence "x  ad y  (d y + z)  ad y"
    using mult_isor by blast
  also have "... = d y  ad y + z  ad y"
    by simp
  also have "...  z"
    by (simp add: a_subid_aux2 ads_d_def)
  finally show "x  ad y  z"
    by simp
qed

lemma da_shunt2: "x  ad y + z  x  d y  z"
  using da_shunt1 local.a_add_idem local.ads_d_def am_add_op_def by auto

lemma d_a_galois1: "d x  ad y  d z  d x  d z + d y"
  by (metis add_assoc local.a_gla local.ads_d_def local.am2 local.ans4 local.ans_d_def local.dnsz.dnso4)

lemma d_a_galois2: "d x  d y  d z  d x  d z + ad y"
proof -
  have "a aa. ad ((a::'a)  ad (ad aa)) = ad (a  aa)"
    using local.a2_eq' local.apd_d_def by force
  then show ?thesis
    by (metis d_a_galois1 local.a_export' local.ads_d_def local.ans_d_def)
qed

lemma d_cancellation_1: "d x  d y + d x  ad y"
proof -
  have a: "d (d x  ad y) = ad y  d x"
    using local.a_closure' local.ads_d_def local.am2 local.ans_d_def by auto
  hence "d x  d (d x  ad y) + d y"
    using d_a_galois1 local.a_comm_var local.ads_d_def by fastforce
  thus ?thesis
    using a add_commute local.ads_d_def local.am2 by auto
qed

lemma d_cancellation_2: "(d z + d y)  ad y  d z"
  by (simp add: da_shunt1)

lemma a_de_morgan: "ad (ad x  ad y) = d (x + y)"
  by (simp add: local.ads_d_def)

lemma a_de_morgan_var_3: "ad (d x + d y) = ad x  ad y"
  using local.a_add_idem local.ads_d_def am_add_op_def by auto

lemma a_de_morgan_var_4: "ad (d x  d y) = ad x + ad y"
  using local.a_add_idem local.ads_d_def am_add_op_def by auto

lemma a_4: "ad x  ad (x  y)"
  using local.a_add_idem local.a_antitone' local.dpdz.domain_1'' am_add_op_def by fastforce

lemma a_6: "ad (d x  y) = ad x + ad y"
  using a_de_morgan_var_4 local.ads_d_def by auto

lemma a_7: "d x  ad (d y + d z) = d x  ad y  ad z"
  using a_de_morgan_var_3 local.mult.semigroup_axioms semigroup.assoc by fastforce

lemma a_d_add_closure [simp]: "d (ad x + ad y) = ad x + ad y"
  using local.a_add_idem local.ads_d_def am_add_op_def by auto

lemma d_6 [simp]: "d x + ad x  d y = d x + d y"
proof -
  have "ad (ad x  (x + ad y)) = d (x + y)"
    by (simp add: distrib_left ads_d_def)
  thus ?thesis
    by (simp add: local.ads_d_def local.ans_d_def)
qed

lemma d_7 [simp]: "ad x + d x  ad y = ad x + ad y"
  by (metis a_d_add_closure local.ads_d_def local.ans4 local.s4)

lemma a_mult_add: "ad x  (y + x) = ad x  y"
  by (simp add: distrib_left)

lemma kat_2: "y  ad z  ad x  y  d x  y  ad z = 0"
proof -
  assume a: "y  ad z  ad x  y"
  hence "d x  y  ad z  d x  ad x  y"
    using local.mult_isol mult_assoc by presburger
  thus ?thesis
    using local.join.le_bot ads_d_def by auto
qed

lemma kat_3: "d x  y  ad z = 0  d x  y = d x  y  d z"
  using local.a_zero_def local.ads_d_def local.am_d_def local.kat_3' by auto

lemma kat_4: "d x  y = d x  y  d z  d x  y  y  d z"
  using a_subid_aux1 mult_assoc ads_d_def by auto

lemma kat_2_equiv: "y  ad z  ad x  y  d x  y  ad z = 0"
proof
  assume "y  ad z  ad x  y"
  thus "d x  y  ad z = 0"
    by (simp add: kat_2)
next
  assume 1: "d x  y  ad z = 0"
  have "y  ad z = (d x + ad x)  y  ad z"
    by (simp add: local.ads_d_def)
  also have "... = d x  y  ad z + ad x  y  ad z"
    using local.distrib_right by presburger
  also have "... = ad x  y  ad z"
    using "1" by auto
  also have "...  ad x  y"
    by (simp add: local.a_subid_aux2)
  finally show "y  ad z  ad x  y" .
qed

lemma kat_4_equiv: "d x  y = d x  y  d z  d x  y  y  d z"
  using local.ads_d_def local.dpdz.d_preserves_equation by auto

lemma kat_3_equiv_opp: "ad z  y  d x = 0  y  d x = d z  y  d x"
proof -
  have "ad z  (y  d x) = 0  (ad z  y  d x = 0) = (y  d x = d z  y  d x)"
    by (metis (no_types, opaque_lifting) add_commute local.add_zerol local.ads_d_def local.as3 local.distrib_right' local.mult_1_left mult_assoc)
  thus ?thesis
    by (metis a_4 local.a_add_idem local.a_gla2 local.ads_d_def mult_assoc am_add_op_def)
qed

lemma kat_4_equiv_opp: "y  d x = d z  y  d x  y  d x  d z  y"
  using kat_2_equiv kat_3_equiv_opp local.ads_d_def by auto

subsection ‹Forward Box and Diamond Operators›

lemma fdemodalisation22: "|x y  d z  ad z  x  d y = 0"
proof -
  have "|x y  d z  d (x  y)  d z"
    by (simp add: fdia_def ads_d_def)
  also have "...  ad z  d (x  y) = 0"
    by (metis add_commute local.a_gla local.ads_d_def local.ans4)
  also have "...  ad z  x  y = 0"
    using dpdz.dom_weakly_local mult_assoc ads_d_def by auto
  finally show ?thesis
    using dpdz.dom_weakly_local ads_d_def by auto
qed

lemma dia_diff_var: "|x y  |x (d y  ad z) + |x z"
proof -
  have 1: "|x (d y  d z)  |x (1  d z)"
    using dpdz.dom_glb_eq ds.fd_subdist fdia_def ads_d_def by force
  have "|x y = |x (d y  (ad z + d z))"
    by (metis as3 add_comm ds.fdia_d_simp mult_1_right ads_d_def)
  also have "... = |x (d y  ad z) + |x (d y  d z)"
    by (simp add: local.distrib_left local.ds.fdia_add1)
  also have "...  |x (d y  ad z) + |x (1  d z)"
    using "1" local.join.sup.mono by blast
  finally show ?thesis
    by (simp add: fdia_def ads_d_def)
qed

lemma dia_diff: "|x y  ad ( |x z )  |x (d y  ad z)"
  using fdia_def dia_diff_var d_a_galois2 ads_d_def by metis

lemma fdia_export_2: "ad y  |x z = |ad y  x z"
  using local.am_d_def local.d_a_export local.fdia_def mult_assoc by auto

lemma fdia_split: "|x y = d z  |x y + ad z  |x y"
  by (metis mult_onel ans3 distrib_right ads_d_def)

definition fbox :: "'a  'a  'a" ("( |_] _)" [61,81] 82) where
  "|x] y = ad (x  ad y)"

text ‹The next lemmas establish the De Morgan duality between boxes and diamonds.›

lemma fdia_fbox_de_morgan_2: "ad ( |x y) = |x] ad y"
  using fbox_def local.a_closure local.a_loc local.am_d_def local.fdia_def by auto

lemma fbox_simp: "|x] y = |x] d y"
  using fbox_def local.a_add_idem local.ads_d_def am_add_op_def by auto

lemma fbox_dom [simp]: "|x] 0 = ad x"
  by (simp add: fbox_def)

lemma fbox_add1: "|x] (d y  d z) = |x] y  |x] z"
  using a_de_morgan_var_4 fbox_def local.distrib_left by auto

lemma fbox_add2: "|x + y] z = |x] z  |y] z"
  by (simp add: fbox_def)

lemma fbox_mult: "|x  y] z = |x] |y] z"
  using fbox_def local.a2_eq' local.apd_d_def mult_assoc by auto

lemma fbox_zero [simp]: "|0] x = 1"
  by (simp add: fbox_def)

lemma fbox_one [simp]: "|1] x = d x"
  by (simp add: fbox_def ads_d_def)

lemma fbox_iso: "d x  d y  |z] x  |z] y"
proof -
  assume "d x  d y"
  hence "ad y  ad x"
    using local.a_add_idem local.a_antitone' local.ads_d_def am_add_op_def by fastforce
  hence "z  ad y  z  ad x"
    by (simp add: mult_isol)
  thus "|z] x  |z] y"
    by (simp add: fbox_def a_antitone')
qed

lemma fbox_antitone_var: "x  y  |y] z  |x] z"
  by (simp add: fbox_def a_antitone mult_isor)

lemma fbox_subdist_1: "|x] (d y  d z)  |x] y"
  using a_de_morgan_var_4 fbox_def local.a_supdist_var local.distrib_left by force

lemma fbox_subdist_2: "|x] y |x] (d y + d z)"
  by (simp add: fbox_iso ads_d_def)

lemma fbox_subdist: "|x] d y + |x] d z  |x] (d y + d z)"
  by (simp add: fbox_iso sup_least ads_d_def)

lemma fbox_diff_var: "|x] (d y + ad z)  |x] z  |x] y"
proof -
  have "ad (ad y)  ad (ad z) = ad (ad z + ad y)"
    using local.dpdz.dsg4 by auto
  then have "d (d (d y + ad z)  d z)  d y"
    by (simp add: local.a_subid_aux1' local.ads_d_def)
  then show ?thesis
    by (metis fbox_add1 fbox_iso)
qed

lemma fbox_diff: "|x] (d y + ad z)  |x] y + ad ( |x] z )"
proof -
  have f1: "a. ad (ad (ad (a::'a))) = ad a"
    using local.a_closure' local.ans_d_def by force
  have f2: "a aa. ad (ad (a::'a)) + ad aa = ad (ad a  aa)"
    using local.ans_d_def by auto
  have f3: "a aa. ad ((a::'a) + aa) = ad (aa + a)"
    by (simp add: local.am2)
  then have f4: "a aa. ad (ad (ad (a::'a)  aa)) = ad (ad aa + a)"
    using f2 f1 by (metis (no_types) local.ans4)
  have f5: "a aa ab. ad ((a::'a)  (aa + ab)) = ad (a  (ab + aa))"
    using f3 local.distrib_left by presburger
  have f6: "a aa. ad (ad (ad (a::'a) + aa)) = ad (ad aa  a)"
    using f3 f1 by fastforce
  have "ad (x  ad (y + ad z))  ad (ad (x  ad z)  (x  ad y))"
    using f5 f2 f1 by (metis (no_types) a_mult_add fbox_def fbox_subdist_1 local.a_gla2 local.ads_d_def local.ans4 local.distrib_left local.gla_1 mult_assoc)
  then show ?thesis
    using f6 f4 f3 f1 by (simp add: fbox_def local.ads_d_def)
qed

end

context antidomain_semiring

begin

lemma kat_1: "d x  y  y  d z  y  ad z  ad x  y"
proof -
  assume a: "d x  y  y  d z"
  have "y  ad z = d x  y  ad z + ad x  y  ad z"
    by (metis local.ads_d_def local.as3 local.distrib_right local.mult_1_left)
  also have "...  y  (d z  ad z) + ad x  y  ad z"
    by (metis a add_iso mult_isor mult_assoc)
  also have "... = ad x  y  ad z"
    by (simp add: ads_d_def)
  finally show "y  ad z  ad x  y"
    using local.a_subid_aux2 local.dual_order.trans by blast
qed

lemma kat_1_equiv: "d x  y  y  d z  y  ad z  ad x  y"
  using kat_1 kat_2 kat_3 kat_4 by blast

lemma kat_3_equiv': "d x  y  ad z = 0  d x  y = d x  y  d z"
  by (simp add: kat_1_equiv local.kat_2_equiv local.kat_4_equiv)

lemma kat_1_equiv_opp: "y  d x  d z  y  ad z  y  y  ad x"
  by (metis kat_1_equiv local.a_closure' local.ads_d_def local.ans_d_def)

lemma kat_2_equiv_opp: "ad z  y  y  ad x  ad z  y  d x = 0"
  by (simp add: kat_1_equiv_opp local.kat_3_equiv_opp local.kat_4_equiv_opp)

lemma fbox_one_1 [simp]: "|x] 1 = 1"
  by (simp add: fbox_def)

lemma fbox_demodalisation3: "d y  |x] d z  d y  x  x  d z"
  by (simp add: fbox_def a_gla kat_2_equiv_opp mult_assoc ads_d_def)

end

subsection ‹Antidomain Kleene Algebras›

class antidomain_left_kleene_algebra = antidomain_semiringl + left_kleene_algebra_zerol

begin

sublocale dka: domain_left_kleene_algebra "(+)" "(⋅)" 1 0 d "(≤)" "(<)" star
  rewrites "domain_semiringl.fd (⋅) d x y  |x y"
  by (unfold_locales, auto simp add: local.ads_d_def ans_d_def)

lemma a_star [simp]: "ad (x) = 0"
  using dka.dom_star local.a_very_costrict'' local.ads_d_def by force

lemma fbox_star_unfold [simp]: "|1] z  |x] |x] z = |x] z"
proof -
  have "ad (ad z + x  (x  ad z)) = ad (x  ad z)"
    using local.conway.dagger_unfoldl_distr mult_assoc by auto
  then show ?thesis
    using local.a_closure' local.ans_d_def local.fbox_def local.fdia_def local.fdia_fbox_de_morgan_2 by fastforce
qed

lemma fbox_star_unfold_var [simp]: "d z  |x] |x] z = |x] z"
  using fbox_star_unfold by auto

lemma fbox_star_unfoldr [simp]: "|1] z  |x] |x] z = |x] z"
  by (metis fbox_star_unfold fbox_mult star_slide_var)

lemma fbox_star_unfoldr_var [simp]: "d z  |x] |x] z = |x] z"
  using fbox_star_unfoldr by auto

lemma fbox_star_induct_var: "d y  |x] y  d y  |x] y"
proof -
  assume a1: "d y  |x] y"
  have "a. ad (ad (ad (a::'a))) = ad a"
    using local.a_closure' local.ans_d_def by auto
  then have "ad (ad (x  ad y))  ad y"
    using a1 by (metis dka.fdia_star_induct local.a_export' local.ads_d_def local.ans4 local.ans_d_def local.eq_refl local.fbox_def local.fdia_def local.meet_ord_def)
  then have "ad (ad y + ad (x  ad y)) = zero_class.zero"
    by (metis (no_types) add_commute local.a_2_var local.ads_d_def local.ans4)
  then show ?thesis
    using local.a_2_var local.ads_d_def local.fbox_def by auto
qed

lemma fbox_star_induct: "d y  d z  |x] y  d y  |x] z"
proof -
  assume a1: "d y  d z  |x] y"
  hence a: "d y  d z" and "d y  |x] y"
    apply (metis local.a_subid_aux2 local.dual_order.trans local.fbox_def)
    using a1 dka.dom_subid_aux2 local.dual_order.trans by blast
  hence "d y  |x] y"
    using fbox_star_induct_var by blast
  thus ?thesis
    using a local.fbox_iso local.order.trans by blast
qed

lemma fbox_star_induct_eq: "d z  |x] y = d y  d y  |x] z"
  by (simp add: fbox_star_induct)

lemma fbox_export_1: "ad y + |x] y = |d y  x] y"
  by (simp add: local.a_6 local.fbox_def mult_assoc)

lemma fbox_export_2: "d y + |x] y = |ad y  x] y"
  by (simp add: local.ads_d_def local.ans_d_def local.fbox_def mult_assoc)

end

class antidomain_kleene_algebra = antidomain_semiring + kleene_algebra

begin

subclass antidomain_left_kleene_algebra ..

lemma "d p  |(d t  x)  ad t] (d q  ad t)  d p  |d t  x] d q"
(*nitpick [expect=genuine]*)
oops

end

end