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