Theory Relative_Domain

(* Title:      Relative Domain
   Author:     Walter Guttmann
   Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

section ‹Relative Domain›

theory Relative_Domain

imports Tests

begin

class Z =
  fixes Z :: "'a"

class relative_domain_semiring = idempotent_left_semiring + dom + Z +
  assumes d_restrict : "x ≤ d(x) * x ⊔ Z"
  assumes d_mult_d   : "d(x * y) = d(x * d(y))"
  assumes d_below_one: "d(x) ≤ 1"
  assumes d_Z        : "d(Z) = bot"
  assumes d_dist_sup : "d(x ⊔ y) = d(x) ⊔ d(y)"
  assumes d_export   : "d(d(x) * y) = d(x) * d(y)"
begin

lemma d_plus_one: 
  "d(x) ⊔ 1 = 1"
  by (simp add: d_below_one sup_absorb2)

text ‹Theorem 44.2›

lemma d_zero:
  "d(bot) = bot"
  by (metis d_Z d_export mult_left_zero)

text ‹Theorem 44.3›

lemma d_involutive:
  "d(d(x)) = d(x)"
  by (metis d_mult_d mult_left_one)

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

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

text ‹Theorem 44.4›

lemma d_mult_sub:
  "d(x * y) ≤ d(x)"
  by (smt (verit, ccfv_threshold) d_plus_one d_dist_sup d_mult_d le_iff_sup mult.right_neutral mult_left_sub_dist_sup_right sup_commute)

lemma d_sub_one:
  "x ≤ 1 ⟹ x ≤ d(x) ⊔ Z"
  by (metis sup_left_isotone d_restrict mult_right_isotone mult_1_right order_trans)

lemma d_one:
  "d(1) ⊔ Z = 1 ⊔ Z"
  by (meson d_sub_one d_below_one order.trans preorder_one_closed sup.cobounded1 sup_same_context)

text ‹Theorem 44.8›

lemma d_strict:
  "d(x) = bot ⟷ x ≤ Z"
  by (metis sup_commute sup_bot_right d_Z d_dist_sup d_restrict le_iff_sup mult_left_zero)

text ‹Theorem 44.1›

lemma d_isotone:
  "x ≤ y ⟹ d(x) ≤ d(y)"
  using d_dist_sup sup_right_divisibility by force

lemma d_plus_left_upper_bound:
  "d(x) ≤ d(x ⊔ y)"
  by (simp add: d_isotone)

lemma d_idempotent:
  "d(x) * d(x) = d(x)"
  by (smt (verit, ccfv_threshold) d_involutive d_mult_sub d_Z d_dist_sup d_export d_restrict le_iff_sup sup_bot_left sup_commute)

text ‹Theorem 44.12›

lemma d_least_left_preserver:
  "x ≤ d(y) * x ⊔ Z ⟷ d(x) ≤ d(y)"
  apply (rule iffI)
  apply (smt (z3) comm_monoid.comm_neutral d_involutive d_mult_sub d_plus_left_upper_bound d_Z d_dist_sup order_trans sup_absorb2 sup_bot.comm_monoid_axioms)
  by (smt (verit, del_insts) d_restrict mult_right_dist_sup sup.cobounded1 sup.orderE sup_assoc sup_commute)

text ‹Theorem 44.9›

lemma d_weak_locality:
  "x * y ≤ Z ⟷ x * d(y) ≤ Z"
  by (metis d_mult_d d_strict)

lemma d_sup_closed:
  "d(d(x) ⊔ d(y)) = d(x) ⊔ d(y)"
  by (simp add: d_involutive d_dist_sup)

lemma d_mult_closed:
  "d(d(x) * d(y)) = d(x) * d(y)"
  using d_export d_mult_d by auto

lemma d_mult_left_lower_bound:
  "d(x) * d(y) ≤ d(x)"
  by (metis d_export d_involutive d_mult_sub)

lemma d_mult_left_absorb_sup:
  "d(x) * (d(x) ⊔ d(y)) = d(x)"
  by (smt d_sup_closed d_export d_idempotent d_involutive d_mult_sub order.eq_iff mult_left_sub_dist_sup_left)

lemma d_sup_left_absorb_mult:
  "d(x) ⊔ d(x) * d(y) = d(x)"
  using d_mult_left_lower_bound sup.absorb_iff1 by auto

lemma d_commutative:
  "d(x) * d(y) = d(y) * d(x)"
  by (metis sup_commute order.antisym d_sup_left_absorb_mult d_below_one d_export d_mult_left_absorb_sup mult_assoc mult_left_isotone mult_left_one)

lemma d_mult_greatest_lower_bound:
  "d(x) ≤ d(y) * d(z) ⟷ d(x) ≤ d(y) ∧ d(x) ≤ d(z)"
  by (metis d_commutative d_idempotent d_mult_left_lower_bound mult_isotone order_trans)

lemma d_sup_left_dist_mult:
  "d(x) ⊔ d(y) * d(z) = (d(x) ⊔ d(y)) * (d(x) ⊔ d(z))"
  by (metis sup_assoc d_commutative d_dist_sup d_idempotent d_mult_left_absorb_sup mult_right_dist_sup)

lemma d_order:
  "d(x) ≤ d(y) ⟷ d(x) = d(x) * d(y)"
  by (metis d_mult_greatest_lower_bound d_mult_left_absorb_sup le_iff_sup order_refl)

text ‹Theorem 44.6›

lemma Z_mult_decreasing:
  "Z * x ≤ Z"
  by (metis d_mult_sub bot.extremum d_strict order.eq_iff)

text ‹Theorem 44.5›

lemma d_below_d_one:
  "d(x) ≤ d(1)"
  by (metis d_mult_sub mult_left_one)

text ‹Theorem 44.7›

lemma d_relative_Z:
  "d(x) * x ⊔ Z = x ⊔ Z"
  by (metis sup_ge1 sup_same_context d_below_one d_restrict mult_isotone mult_left_one)

lemma Z_left_zero_above_one:
  "1 ≤ x ⟹ Z * x = Z"
  by (metis Z_mult_decreasing order.eq_iff mult_right_isotone mult_1_right)

text ‹Theorem 44.11›

lemma kat_4:
  "d(x) * y = d(x) * y * d(z) ⟹ d(x) * y ≤ y * d(z)"
  by (metis d_below_one mult_left_isotone mult_left_one)

lemma kat_4_equiv:
  "d(x) * y = d(x) * y * d(z) ⟷ d(x) * y ≤ y * d(z)"
  apply (rule iffI)
  apply (simp add: kat_4)
  apply (rule order.antisym)
  apply (metis d_idempotent mult_assoc mult_right_isotone)
  by (metis d_below_one mult_right_isotone mult_1_right)

lemma kat_4_equiv_opp:
  "y * d(x) = d(z) * y * d(x) ⟷ y * d(x) ≤ d(z) * y"
  apply (rule iffI)
  using d_below_one mult_right_isotone apply fastforce
  apply (rule order.antisym)
  apply (metis d_idempotent mult_assoc mult_left_isotone)
  by (metis d_below_one mult_left_isotone mult_left_one)

text ‹Theorem 44.10›

lemma d_restrict_iff_1:
  "d(x) * y ≤ z ⟷ d(x) * y ≤ d(x) * z"
  by (smt (verit, del_insts) d_below_one d_idempotent mult_assoc mult_left_isotone mult_left_one mult_right_isotone order_trans)

(* independence of axioms, checked in relative_domain_semiring without the respective axiom: *)
proposition d_restrict : "x ≤ d(x) * x ⊔ Z" (* nitpick [expect=genuine,card=2] *) oops
proposition d_mult_d   : "d(x * y) = d(x * d(y))" (* nitpick [expect=genuine,card=3] *) oops
proposition d_below_one: "d(x) ≤ 1" (* nitpick [expect=genuine,card=3] *) oops
proposition d_Z        : "d(Z) = bot" (* nitpick [expect=genuine,card=2] *) oops
proposition d_dist_sup : "d(x ⊔ y) = d(x) ⊔ d(y)" (* nitpick [expect=genuine,card=3] *) oops
proposition d_export   : "d(d(x) * y) = d(x) * d(y)" (* nitpick [expect=genuine,card=5] *) oops

end

typedef (overloaded) 'a dImage = "{ x::'a::relative_domain_semiring . (∃y::'a . x = d(y)) }"
  by auto

lemma simp_dImage[simp]:
  "∃y . Rep_dImage x = d(y)"
  using Rep_dImage by simp

setup_lifting type_definition_dImage

text ‹Theorem 44›

instantiation dImage :: (relative_domain_semiring) bounded_distrib_lattice
begin

lift_definition sup_dImage :: "'a dImage ⇒ 'a dImage ⇒ 'a dImage" is sup
  by (metis d_dist_sup)

lift_definition inf_dImage :: "'a dImage ⇒ 'a dImage ⇒ 'a dImage" is times
  by (metis d_export)

lift_definition bot_dImage :: "'a dImage" is bot
  by (metis d_zero)

lift_definition top_dImage :: "'a dImage" is "d(1)"
  by auto

lift_definition less_eq_dImage :: "'a dImage ⇒ 'a dImage ⇒ bool" is less_eq .

lift_definition less_dImage :: "'a dImage ⇒ 'a dImage ⇒ bool" is less .

instance
  apply intro_classes
  apply (simp add: less_dImage.rep_eq less_eq_dImage.rep_eq less_le_not_le)
  apply (simp add: less_eq_dImage.rep_eq)
  using less_eq_dImage.rep_eq apply simp
  apply (simp add: Rep_dImage_inject less_eq_dImage.rep_eq)
  apply (metis (mono_tags) d_involutive d_mult_sub inf_dImage.rep_eq less_eq_dImage.rep_eq simp_dImage)
  apply (metis (mono_tags) d_mult_greatest_lower_bound inf_dImage.rep_eq less_eq_dImage.rep_eq order_refl simp_dImage)
  apply (metis (mono_tags) d_mult_greatest_lower_bound inf_dImage.rep_eq less_eq_dImage.rep_eq simp_dImage)
  apply (simp add: less_eq_dImage.rep_eq sup_dImage.rep_eq)
  apply (simp add: less_eq_dImage.rep_eq sup_dImage.rep_eq)
  apply (simp add: less_eq_dImage.rep_eq sup_dImage.rep_eq)
  apply (simp add: bot_dImage.rep_eq less_eq_dImage.rep_eq)
  apply (smt (z3) d_below_d_one less_eq_dImage.rep_eq simp_dImage top_dImage.rep_eq)
  by (smt (z3) inf_dImage.rep_eq sup_dImage.rep_eq simp_dImage Rep_dImage_inject d_sup_left_dist_mult)

end

class bounded_relative_domain_semiring = relative_domain_semiring + bounded_idempotent_left_semiring
begin

lemma Z_top:
  "Z * top = Z"
  by (simp add: Z_left_zero_above_one)

lemma d_restrict_top:
  "x ≤ d(x) * top ⊔ Z"
  by (metis sup_left_isotone d_restrict mult_right_isotone order_trans top_greatest)

proposition d_one_one: "d(1) = 1" nitpick [expect=genuine,card=2] oops

end

class relative_domain_semiring_split = relative_domain_semiring +
  assumes split_Z: "x * (y ⊔ Z) ≤ x * y ⊔ Z"
begin

lemma d_restrict_iff:
  "(x ≤ y ⊔ Z) ⟷ (x ≤ d(x) * y ⊔ Z)"
proof -
  have "x ≤ y ⊔ Z ⟶ x ≤ d(x) * (y ⊔ Z) ⊔ Z"
    by (smt sup_left_isotone d_restrict le_iff_sup mult_left_sub_dist_sup_left order_trans)
  hence "x ≤ y ⊔ Z ⟶ x ≤ d(x) * y ⊔ Z"
    by (meson le_supI order_lesseq_imp split_Z sup.cobounded2)
  thus ?thesis
    by (meson d_restrict_iff_1 le_supI mult_left_sub_dist_sup_left order_lesseq_imp sup.cobounded2)
qed

end

class relative_antidomain_semiring = idempotent_left_semiring + dom + Z + uminus +
  assumes a_restrict  : "-x * x ≤ Z"
  assumes a_mult_d    : "-(x * y) = -(x * --y)"
  assumes a_complement: "-x * --x = bot"
  assumes a_Z         : "-Z = 1"
  assumes a_export    : "-(--x * y) = -x ⊔ -y"
  assumes a_dist_sup  : "-(x ⊔ y) = -x * -y"
  assumes d_def       : "d(x) = --x"
begin

notation
  uminus ("a")

text ‹Theorem 45.7›

lemma a_complement_one:
  "--x ⊔ -x = 1"
  by (metis a_Z a_complement a_export a_mult_d mult_left_one)

text ‹Theorem 45.5 and Theorem 45.6›

lemma a_d_closed:
  "d(a(x)) = a(x)"
  by (metis a_mult_d d_def mult_left_one)

lemma a_below_one:
  "a(x) ≤ 1"
  using a_complement_one sup_right_divisibility by auto

lemma a_export_a:
  "a(a(x) * y) = d(x) ⊔ a(y)"
  by (metis a_d_closed a_export d_def)

lemma a_sup_absorb:
  "(x ⊔ a(y)) * a(a(y)) = x * a(a(y))"
  by (simp add: a_complement mult_right_dist_sup)

text ‹Theorem 45.10›

lemma a_greatest_left_absorber:
  "a(x) * y ≤ Z ⟷ a(x) ≤ a(y)"
  apply (rule iffI)
  apply (smt a_Z a_sup_absorb a_dist_sup a_export_a a_mult_d sup_commute d_def le_iff_sup mult_left_one)
  by (meson a_restrict mult_isotone order.refl order_trans)

lemma a_plus_left_lower_bound:
  "a(x ⊔ y) ≤ a(x)"
  by (metis a_greatest_left_absorber a_restrict sup_commute mult_left_sub_dist_sup_right order_trans)

text ‹Theorem 45.2›

subclass relative_domain_semiring
  apply unfold_locales
  apply (smt (verit) a_Z a_complement_one a_restrict sup_commute sup_ge1 case_split_left d_def order_trans)
  using a_mult_d d_def apply force
  apply (simp add: a_below_one d_def)
  apply (metis a_Z a_complement d_def mult_left_one)
  apply (simp add: a_export_a a_dist_sup d_def)
  using a_dist_sup a_export d_def by auto

text ‹Theorem 45.1›

subclass tests
  apply unfold_locales
  apply (simp add: mult_assoc)
  apply (metis a_dist_sup sup_commute)
  apply (smt a_complement a_d_closed a_export_a sup_bot_right d_sup_left_dist_mult)
  apply (metis a_d_closed a_dist_sup d_def)
  apply (rule the_equality[THEN sym])
  apply (simp add: a_complement)
  apply (simp add: a_complement)
  using a_d_closed a_Z d_Z d_def apply force
  using a_export a_mult_d apply fastforce
  apply (metis a_d_closed d_order)
  by (simp add: less_le_not_le)

lemma a_plus_mult_d:
  "-(x * y) ⊔ -(x * --y) = -(x * --y)"
  using a_mult_d by auto

lemma a_mult_d_2:
  "a(x * y) = a(x * d(y))"
  using a_mult_d d_def by auto

lemma a_3:
  "a(x) * a(y) * d(x ⊔ y) = bot"
  by (metis a_complement a_dist_sup d_def)

lemma a_fixpoint:
  "∀x . (a(x) = x ⟶ (∀y . y = bot))"
  by (metis a_complement_one mult_1_left mult_left_zero order.refl sup.order_iff tests_dual.one_def)

text ‹Theorem 45.9›

lemma a_strict:
  "a(x) = 1 ⟷ x ≤ Z"
  by (metis a_Z d_def d_strict order.refl tests_dual.sba_dual.double_negation)

lemma d_complement_zero:
  "d(x) * a(x) = bot"
  by (simp add: d_def tests_dual.sub_commutative)

lemma a_complement_zero:
  "a(x) * d(x) = bot"
  by (simp add: d_def)

lemma a_shunting_zero:
  "a(x) * d(y) = bot ⟷ a(x) ≤ a(y)"
  by (simp add: d_def tests_dual.sba_dual.less_eq_inf_bot)

lemma a_antitone:
  "x ≤ y ⟹ a(y) ≤ a(x)"
  using a_plus_left_lower_bound sup_commute sup_right_divisibility by fastforce

lemma a_mult_deMorgan:
  "a(a(x) * a(y)) = d(x ⊔ y)"
  by (simp add: a_dist_sup d_def)

lemma a_mult_deMorgan_1:
  "a(a(x) * a(y)) = d(x) ⊔ d(y)"
  by (simp add: a_mult_deMorgan d_dist_sup)

lemma a_mult_deMorgan_2:
  "a(d(x) * d(y)) = a(x) ⊔ a(y)"
  using a_export d_def by auto

lemma a_plus_deMorgan:
  "a(a(x) ⊔ a(y)) = d(x) * d(y)"
  by (simp add: a_dist_sup d_def)

lemma a_plus_deMorgan_1:
  "a(d(x) ⊔ d(y)) = a(x) * a(y)"
  by (simp add: a_dist_sup d_def)

text ‹Theorem 45.8›

lemma a_mult_left_upper_bound:
  "a(x) ≤ a(x * y)"
  using a_shunting_zero d_def d_mult_sub tests_dual.less_eq_sup_top by auto

text ‹Theorem 45.6›

lemma d_a_closed:
  "a(d(x)) = a(x)"
  by (simp add: d_def)

lemma a_export_d:
  "a(d(x) * y) = a(x) ⊔ a(y)"
  by (simp add: a_export d_def)

lemma a_7:
  "d(x) * a(d(y) ⊔ d(z)) = d(x) * a(y) * a(z)"
  by (simp add: a_plus_deMorgan_1 mult_assoc)

lemma d_a_shunting:
  "d(x) * a(y) ≤ d(z) ⟷ d(x) ≤ d(z) ⊔ d(y)"
  by (simp add: d_def tests_dual.sba_dual.shunting_right)

lemma d_d_shunting:
  "d(x) * d(y) ≤ d(z) ⟷ d(x) ≤ d(z) ⊔ a(y)"
  by (simp add: d_def tests_dual.sba_dual.shunting_right)

lemma d_cancellation_1:
  "d(x) ≤ d(y) ⊔ (d(x) * a(y))"
  by (smt (z3) a_d_closed d_a_shunting d_export eq_refl sup_commute)

lemma d_cancellation_2:
  "(d(z) ⊔ d(y)) * a(y) ≤ d(z)"
  by (metis d_a_shunting d_dist_sup eq_refl)

lemma a_sup_closed:
  "d(a(x) ⊔ a(y)) = a(x) ⊔ a(y)"
  using a_mult_deMorgan tests_dual.sub_inf_def by auto

lemma a_mult_closed:
  "d(a(x) * a(y)) = a(x) * a(y)"
  using d_def tests_dual.sub_sup_closed by auto

lemma d_a_shunting_zero:
  "d(x) * a(y) = bot ⟷ d(x) ≤ d(y)"
  using a_shunting_zero d_def by force

lemma d_d_shunting_zero:
  "d(x) * d(y) = bot ⟷ d(x) ≤ a(y)"
  using d_a_shunting_zero d_def by auto

lemma d_compl_intro:
  "d(x) ⊔ d(y) = d(x) ⊔ a(x) * d(y)"
  by (simp add: d_def tests_dual.sba_dual.sup_complement_intro)

lemma a_compl_intro:
  "a(x) ⊔ a(y) = a(x) ⊔ d(x) * a(y)"
  by (simp add: d_def tests_dual.sba_dual.sup_complement_intro)

lemma kat_2:
  "y * a(z) ≤ a(x) * y ⟹ d(x) * y * a(z) = bot"
  by (metis d_complement_zero order.eq_iff mult_assoc mult_left_zero mult_right_isotone bot_least)

text ‹Theorem 45.4›

lemma kat_2_equiv:
  "y * a(z) ≤ a(x) * y ⟷ d(x) * y * a(z) = bot"
  apply (rule iffI)
  apply (simp add: kat_2)
  by (smt (verit, best) a_Z a_below_one a_complement_one case_split_left d_def mult_assoc mult_right_isotone mult_1_right bot_least)

lemma kat_3_equiv_opp:
  "a(z) * y * d(x) = bot ⟷ y * d(x) = d(z) * y * d(x)"
  using kat_2_equiv d_def kat_4_equiv_opp by auto

text ‹Theorem 45.4›

lemma kat_3_equiv_opp_2:
  "d(z) * y * a(x) = bot ⟷ y * a(x) = a(z) * y * a(x)"
  by (metis a_d_closed kat_3_equiv_opp d_def)

lemma kat_equiv_6:
  "d(x) * y * a(z) = d(x) * y * bot ⟷ d(x) * y * a(z) ≤ y * bot"
  by (metis d_restrict_iff_1 order.eq_iff mult_left_sub_dist_sup_right tests_dual.sba_dual.sup_right_unit mult_assoc)

lemma d_one_one:
  "d(1) = 1"
  by (simp add: d_def)

lemma case_split_left_sup:
  "-p * x ≤ y ∧ --p * x ≤ z ⟹ x ≤ y ⊔ z"
  by (smt (z3) a_complement_one case_split_left order_lesseq_imp sup.cobounded2 sup_ge1)

lemma test_mult_left_sub_dist_shunt:
  "-p * (--p * x ⊔ Z) ≤ Z"
  by (simp add: a_greatest_left_absorber a_Z a_dist_sup a_export)

lemma test_mult_left_dist_shunt:
  "-p * (--p * x ⊔ Z) = -p * Z"
  by (smt (verit, ccfv_SIG) order.antisym mult_left_sub_dist_sup_right sup.orderE tests_dual.sba_dual.sup_idempotent mult_assoc test_mult_left_sub_dist_shunt tests_dual.sup_absorb)

(* independence of axioms, checked in relative_antidomain_semiring without the respective axiom: *)
proposition a_restrict  : "-x * x ≤ Z" (* nitpick [expect=genuine,card=3] *) oops
proposition a_mult_d    : "-(x * y) = -(x * --y)" (* nitpick [expect=genuine,card=3] *) oops
proposition a_complement: "-x * --x = bot" (* nitpick [expect=genuine,card=2] *) oops
proposition a_Z         : "-Z = 1" (* nitpick [expect=genuine,card=2] *) oops
proposition a_export    : "-(--x * y) = -x ⊔ -y" (* nitpick [expect=genuine,card=5] *) oops
proposition a_dist_sup  : "-(x ⊔ y) = -x * -y" (* nitpick [expect=genuine,card=3] *) oops
proposition d_def       : "d(x) = --x" (* nitpick [expect=genuine,card=2] *) oops

end

typedef (overloaded) 'a aImage = "{ x::'a::relative_antidomain_semiring . (∃y::'a . x = a(y)) }"
  by auto

lemma simp_aImage[simp]:
  "∃y . Rep_aImage x = a(y)"
  using Rep_aImage by simp

setup_lifting type_definition_aImage

text ‹Theorem 45.3›

instantiation aImage :: (relative_antidomain_semiring) boolean_algebra
begin

lift_definition sup_aImage :: "'a aImage ⇒ 'a aImage ⇒ 'a aImage" is sup
  using tests_dual.sba_dual.sba_dual.inf_closed by auto

lift_definition inf_aImage :: "'a aImage ⇒ 'a aImage ⇒ 'a aImage" is times
  using tests_dual.sba_dual.inf_closed by auto

lift_definition minus_aImage :: "'a aImage ⇒ 'a aImage ⇒ 'a aImage" is "λx y . x * a(y)"
  using tests_dual.sba_dual.inf_closed by blast

lift_definition uminus_aImage :: "'a aImage ⇒ 'a aImage" is a
  by auto

lift_definition bot_aImage :: "'a aImage" is bot
  by (metis tests_dual.sba_dual.sba_dual.complement_bot)

lift_definition top_aImage :: "'a aImage" is 1
  using a_Z by auto

lift_definition less_eq_aImage :: "'a aImage ⇒ 'a aImage ⇒ bool" is less_eq .

lift_definition less_aImage :: "'a aImage ⇒ 'a aImage ⇒ bool" is less .

instance
  apply intro_classes
  apply (simp add: less_aImage.rep_eq less_eq_aImage.rep_eq less_le_not_le)
  apply (simp add: less_eq_aImage.rep_eq)
  using less_eq_aImage.rep_eq apply simp
  apply (simp add: Rep_aImage_inject less_eq_aImage.rep_eq)
  apply (metis (mono_tags) a_below_one inf_aImage.rep_eq less_eq_aImage.rep_eq mult.right_neutral mult_right_isotone simp_aImage)
  apply (metis (mono_tags, lifting) less_eq_aImage.rep_eq a_d_closed a_export bot.extremum_unique inf_aImage.rep_eq kat_equiv_6 mult.assoc mult.left_neutral mult_left_isotone mult_left_zero simp_aImage sup.cobounded1 tests_dual.sba_dual.sba_dual.complement_top)
  apply (smt (z3) less_eq_aImage.rep_eq inf_aImage.rep_eq mult_isotone simp_aImage tests_dual.sba_dual.inf_idempotent)
  apply (simp add: less_eq_aImage.rep_eq sup_aImage.rep_eq)
  apply (simp add: less_eq_aImage.rep_eq sup_aImage.rep_eq)
  using less_eq_aImage.rep_eq sup_aImage.rep_eq apply force
  apply (simp add: less_eq_aImage.rep_eq bot_aImage.rep_eq)
  apply (smt (z3) less_eq_aImage.rep_eq a_below_one simp_aImage top_aImage.rep_eq)
  apply (metis (mono_tags, lifting) tests_dual.sba_dual.sba_dual.inf_left_dist_sup Rep_aImage_inject inf_aImage.rep_eq sup_aImage.rep_eq simp_aImage)
  apply (smt (z3) inf_aImage.rep_eq uminus_aImage.rep_eq Rep_aImage_inject a_complement bot_aImage.rep_eq simp_aImage)
  apply (smt (z3) top_aImage.rep_eq Rep_aImage_inject a_complement_one simp_aImage sup_aImage.rep_eq sup_commute uminus_aImage.rep_eq)
  by (metis (mono_tags) inf_aImage.rep_eq Rep_aImage_inject minus_aImage.rep_eq uminus_aImage.rep_eq)

end

class bounded_relative_antidomain_semiring = relative_antidomain_semiring + bounded_idempotent_left_semiring
begin

subclass bounded_relative_domain_semiring ..

lemma a_top:
  "a(top) = bot"
  by (metis a_plus_left_lower_bound bot_unique sup_right_top tests_dual.sba_dual.complement_top)

lemma d_top:
  "d(top) = 1"
  using a_top d_def by auto

lemma shunting_top_1:
  "-p * x ≤ y ⟹ x ≤ --p * top ⊔ y"
  by (metis sup_commute case_split_left_sup mult_right_isotone top_greatest)

lemma shunting_Z:
  "-p * x ≤ Z ⟷ x ≤ --p * top ⊔ Z"
  apply (rule iffI)
  apply (simp add: shunting_top_1)
  by (smt a_top a_Z a_antitone a_dist_sup a_export a_greatest_left_absorber sup_commute sup_bot_right mult_left_one)

proposition a_left_dist_sup: "-p * (y ⊔ z) = -p * y ⊔ -p * z" nitpick [expect=genuine,card=7] oops
proposition shunting_top: "-p * x ≤ y ⟷ x ≤ --p * top ⊔ y" nitpick [expect=genuine,card=7] oops

end

class relative_left_zero_antidomain_semiring = relative_antidomain_semiring + idempotent_left_zero_semiring
begin

lemma kat_3:
  "d(x) * y * a(z) = bot ⟹ d(x) * y = d(x) * y * d(z)"
  by (metis d_def mult_1_right mult_left_dist_sup sup_monoid.add_0_left tests_dual.inf_complement)

lemma a_a_below:
  "a(a(x)) * y ≤ y"
  using d_def d_restrict_iff_1 by auto

lemma kat_equiv_5:
  "d(x) * y ≤ y * d(z) ⟷ d(x) * y * a(z) = d(x) * y * bot"
proof
  assume "d(x) * y ≤ y * d(z)"
  thus "d(x) * y * a(z) = d(x) * y * bot"
    by (metis d_complement_zero kat_4_equiv mult_assoc)
next
  assume "d(x) * y * a(z) = d(x) * y * bot"
  hence "a(a(x)) * y * a(z) ≤ y * a(a(z))"
    by (simp add: a_a_below d_def mult_isotone)
  thus "d(x) * y ≤ y * d(z)"
    by (metis a_a_below a_complement_one case_split_right d_def mult_isotone order_refl)
qed

lemma case_split_right_sup:
  "x * -p ≤ y ⟹ x * --p ≤ z ⟹ x ≤ y ⊔ z"
  by (smt (verit, ccfv_SIG) a_complement_one order.trans mult_1_right mult_left_dist_sup sup_commute sup_right_isotone)

end

class bounded_relative_left_zero_antidomain_semiring = relative_left_zero_antidomain_semiring + bounded_idempotent_left_zero_semiring
begin

lemma shunting_top:
  "-p * x ≤ y ⟷ x ≤ --p * top ⊔ y"
  apply (rule iffI)
  apply (metis sup_commute case_split_left_sup mult_right_isotone top_greatest)
  by (metis a_complement sup_bot_left sup_right_divisibility mult_assoc mult_left_dist_sup mult_left_one mult_left_zero mult_right_dist_sup mult_right_isotone order_trans tests_dual.inf_left_unit)

end

end