# Theory Domain

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

section ‹Domain›

theory Domain

imports Stone_Relation_Algebras.Semirings Tests

begin

context idempotent_left_semiring
begin

sublocale ils: il_semiring where inf = times and sup = sup and bot = bot and less_eq = less_eq and less = less and top = 1
apply unfold_locales
apply simp
apply simp
apply simp
apply simp
apply simp

end

class left_zero_domain_semiring = idempotent_left_zero_semiring + dom +
assumes d_restrict: "x ⊔ d(x) * x = d(x) * x"
assumes d_mult_d  : "d(x * y) = d(x * d(y))"
assumes d_plus_one: "d(x) ⊔ 1 = 1"
assumes d_zero    : "d(bot) = bot"
assumes d_dist_sup: "d(x ⊔ y) = d(x) ⊔ d(y)"
begin

text ‹Many lemmas in this class are taken from Georg Struth's theories.›

lemma d_restrict_equals:
"x = d(x) * x"
by (metis sup_commute d_plus_one d_restrict mult_left_one mult_right_dist_sup)

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)

lemma d_mult_sub:
"d(x * y) ≤ d(x)"
by (metis d_dist_sup d_mult_d d_plus_one le_iff_sup mult_left_sub_dist_sup_left mult_1_right)

lemma d_sub_one:
"x ≤ 1 ⟹ x ≤ d(x)"
by (metis d_restrict_equals mult_right_isotone mult_1_right)

lemma d_strict:
"d(x) = bot ⟷ x = bot"
by (metis d_restrict_equals d_zero mult_left_zero)

lemma d_one:
"d(1) = 1"
by (metis d_restrict_equals mult_1_right)

lemma d_below_one:
"d(x) ≤ 1"

lemma d_isotone:
"x ≤ y ⟹ d(x) ≤ d(y)"
by (metis d_dist_sup le_iff_sup)

lemma d_plus_left_upper_bound:
"d(x) ≤ d(x ⊔ y)"

lemma d_export:
"d(d(x) * y) = d(x) * d(y)"
apply (rule order.antisym)
apply (metis d_below_one d_involutive d_mult_sub d_restrict_equals d_isotone d_mult_d mult_isotone mult_left_one)
by (metis d_below_one d_sub_one coreflexive_mult_closed d_mult_d)

lemma d_idempotent:
"d(x) * d(x) = d(x)"
by (metis d_export d_restrict_equals)

lemma d_commutative:
"d(x) * d(y) = d(y) * d(x)"
by (metis ils.il_inf_associative order.antisym d_export d_mult_d d_mult_sub d_one d_restrict_equals mult_isotone mult_left_one)

lemma d_least_left_preserver:
"x ≤ d(y) * x ⟷ d(x) ≤ d(y)"
by (metis d_below_one d_involutive d_mult_sub d_restrict_equals order.eq_iff mult_left_isotone mult_left_one)

lemma d_weak_locality:
"x * y = bot ⟷ x * d(y) = bot"
by (metis d_mult_d d_strict)

lemma d_sup_closed:
"d(d(x) ⊔ d(y)) = d(x) ⊔ d(y)"

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_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_mult_left_absorb_sup:
"d(x) * (d(x) ⊔ d(y)) = d(x)"
by (metis sup_commute d_idempotent d_plus_one mult_left_dist_sup mult_1_right)

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_sup_left_dist_mult:
"d(x) ⊔ d(y) * d(z) = (d(x) ⊔ d(y)) * (d(x) ⊔ d(z))"
by (smt sup_assoc d_commutative d_idempotent d_mult_left_absorb_sup mult_left_dist_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)

lemma d_mult_below:
"d(x) * y ≤ y"
by (metis sup_left_divisibility d_plus_one mult_left_one mult_right_dist_sup)

lemma d_preserves_equation:
"d(y) * x ≤ x * d(y) ⟷ d(y) * x = d(y) * x * d(y)"
by (simp add: d_below_one d_idempotent test_preserves_equation)

end

class left_zero_antidomain_semiring = idempotent_left_zero_semiring + dom + uminus +
assumes a_restrict   : "-x * x = bot"
assumes a_plus_mult_d: "-(x * y) ⊔ -(x * --y) = -(x * --y)"
assumes a_complement : "--x ⊔ -x = 1"
assumes d_def        : "d(x) = --x"
begin

sublocale aa: a_algebra where minus = "λx y . -(-x ⊔ y)" and uminus = uminus and inf = times and sup = sup and bot = bot and less_eq = less_eq and less = less and top = 1
apply unfold_locales
using a_complement sup_commute apply fastforce
by simp

subclass left_zero_domain_semiring
apply unfold_locales

subclass tests
apply unfold_locales
using aa.sba_dual.sub_sup_closed apply simp
apply simp
apply simp

text ‹Many lemmas in this class are taken from Georg Struth's theories.›

notation
uminus ("a")

lemma a_greatest_left_absorber:
"a(x) * y = bot ⟷ a(x) ≤ a(y)"

lemma a_mult_d:
"a(x * y) = a(x * d(y))"

lemma a_d_closed:
"d(a(x)) = a(x)"

lemma a_plus_left_lower_bound:
"a(x ⊔ y) ≤ a(x)"

lemma a_mult_sup:
"a(x) * (y ⊔ x) = a(x) * y"

lemma a_3:
"a(x) * a(y) * d(x ⊔ y) = bot"
using d_weak_locality aa.l12 aa.sba3_inf_complement_bot by force

lemma a_export:
"a(a(x) * y) = d(x) ⊔ a(y)"
using a_mult_d d_def aa.sba_dual.sub_inf_def by auto

lemma a_fixpoint:
"∀x . (a(x) = x ⟶ (∀y . y = bot))"
by (metis aa.a_d.d_fully_strict aa.sba2_bot_unit aa.sup_idempotent aa.sup_right_zero_var)

lemma a_strict:
"a(x) = 1 ⟷ x = bot"
using aa.a_d.d_fully_strict one_def by fastforce

lemma d_complement_zero:
"d(x) * a(x) = bot"

lemma a_complement_zero:
"a(x) * d(x) = bot"

lemma a_shunting_zero:
"a(x) * d(y) = bot ⟷ a(x) ≤ a(y)"

lemma a_antitone:
"x ≤ y ⟹ a(y) ≤ a(x)"

lemma a_mult_deMorgan:
"a(a(x) * a(y)) = d(x ⊔ y)"

lemma a_mult_deMorgan_1:
"a(a(x) * a(y)) = d(x) ⊔ d(y)"

lemma a_mult_deMorgan_2:
"a(d(x) * d(y)) = a(x) ⊔ a(y)"

lemma a_plus_deMorgan:
"a(a(x) ⊔ a(y)) = d(x) * d(y)"

lemma a_plus_deMorgan_1:
"a(d(x) ⊔ d(y)) = a(x) * a(y)"

lemma a_mult_left_upper_bound:
"a(x) ≤ a(x * y)"
using aa.l5 d_def d_mult_sub by auto

lemma d_a_closed:
"a(d(x)) = a(x)"

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

lemma a_7:
"d(x) * a(d(y) ⊔ d(z)) = d(x) * a(y) * a(z)"

lemma d_a_shunting:
"d(x) * a(y) ≤ d(z) ⟷ d(x) ≤ d(z) ⊔ d(y)"
using aa.sba_dual.shunting_right d_def by auto

lemma d_d_shunting:
"d(x) * d(y) ≤ d(z) ⟷ d(x) ≤ d(z) ⊔ a(y)"
using d_a_shunting d_def by auto

lemma d_cancellation_1:
"d(x) ≤ d(y) ⊔ (d(x) * a(y))"
by (metis a_d_closed aa.sba2_export aa.sup_demorgan d_def eq_refl le_supE 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 aa.sub_sup_closed d_def by auto

lemma a_mult_closed:
"d(a(x) * a(y)) = a(x) * a(y)"
using a_d_closed aa.l12 by auto

lemma d_a_shunting_zero:
"d(x) * a(y) = bot ⟷ d(x) ≤ d(y)"

lemma d_d_shunting_zero:
"d(x) * d(y) = bot ⟷ d(x) ≤ a(y)"

lemma d_compl_intro:
"d(x) ⊔ d(y) = d(x) ⊔ a(x) * d(y)"

lemma a_compl_intro:
"a(x) ⊔ a(y) = a(x) ⊔ d(x) * a(y)"

lemma kat_2:
"y * a(z) ≤ a(x) * y ⟹ d(x) * y * a(z) = bot"
by (smt a_export a_plus_left_lower_bound le_sup_iff d_d_shunting_zero d_export d_strict le_iff_sup mult_assoc)

lemma kat_3:
"d(x) * y * a(z) = bot ⟹ d(x) * y = d(x) * y * d(z)"
by (metis a_export_d aa.complement_bot d_complement_zero d_def mult_1_right mult_left_dist_sup sup_bot_left)

lemma kat_4:
"d(x) * y = d(x) * y * d(z) ⟹ d(x) * y ≤ y * d(z)"
using d_mult_below mult_assoc by auto

lemma kat_2_equiv:
"y * a(z) ≤ a(x) * y ⟷ d(x) * y * a(z) = bot"
apply (rule iffI)
by (metis aa.top_greatest a_complement sup_bot_left d_def mult_left_one mult_right_dist_sup mult_right_isotone mult_1_right)

lemma kat_4_equiv:
"d(x) * y = d(x) * y * d(z) ⟷ d(x) * y ≤ y * d(z)"
apply (rule iffI)
apply (rule order.antisym)
apply (metis d_idempotent le_iff_sup mult_assoc mult_left_dist_sup)
by (metis d_plus_one le_iff_sup mult_left_dist_sup mult_1_right)

lemma kat_3_equiv_opp:
"a(z) * y * d(x) = bot ⟷ y * d(x) = d(z) * y * d(x)"
by (metis a_complement a_restrict sup_bot_left d_a_closed d_def mult_assoc mult_left_one mult_left_zero mult_right_dist_sup)

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 d_def by auto

lemma d_restrict_iff:
"(x ≤ y) ⟷ (x ≤ d(x) * y)"
by (metis d_mult_below d_restrict_equals mult_isotone order_lesseq_imp)

lemma d_restrict_iff_1:
"(d(x) * y ≤ z) ⟷ (d(x) * y ≤ d(x) * z)"
by (metis sup_commute d_export d_mult_left_lower_bound d_plus_one d_restrict_iff mult_left_isotone mult_left_one mult_right_sub_dist_sup_right order_trans)

end

end

```