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 add: sup_assoc)
  apply (simp add: sup_commute)
  apply simp
  apply simp
  apply (simp add: mult_assoc)
  apply (simp add: mult_right_dist_sup)
  apply simp
  apply simp
  apply simp
  apply (simp add: mult_right_isotone)
  apply (simp add: le_iff_sup)
  by (simp add: less_le_not_le)

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"
  by (simp add: d_plus_one le_iff_sup)

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)"
  by (simp add: d_isotone)

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)"
  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_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
  apply (simp add: a_restrict)
  using a_complement sup_commute apply fastforce
  apply (simp add: a_plus_mult_d le_iff_sup)
  by simp

subclass left_zero_domain_semiring
  apply unfold_locales
  apply (simp add: d_def aa.double_complement_above)
  apply (simp add: aa.a_d.d3_eq d_def)
  apply (simp add: d_def)
  apply (simp add: d_def)
  by (simp add: d_def aa.l15)

subclass tests
  apply unfold_locales
  apply (simp add: mult_assoc)
  apply (simp add: aa.sba_dual.sub_commutative)
  apply (simp add: aa.sba_dual.sub_complement)
  using aa.sba_dual.sub_sup_closed apply simp
  apply simp
  apply simp
  apply (simp add: aa.sba_dual.sub_inf_def)
  apply (simp add: aa.less_eq_inf)
  by (simp add: less_le_not_le)

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)"
  by (simp add: aa.l10_iff)

lemma a_mult_d:
  "a(x * y) = a(x * d(y))"
  by (simp add: d_def aa.sba3_complement_inf_double_complement)

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

lemma a_plus_left_lower_bound:
  "a(x  y)  a(x)"
  by (simp add: aa.l9)

lemma a_mult_sup:
  "a(x) * (y  x) = a(x) * y"
  by (simp add: aa.sba3_inf_complement_bot semiring.distrib_left)

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"
  by (simp add: aa.sba3_inf_complement_bot d_def)

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: aa.less_eq_inf_bot d_def)

lemma a_antitone:
  "x  y  a(y)  a(x)"
  by (simp add: aa.l9)

lemma a_mult_deMorgan:
  "a(a(x) * a(y)) = d(x  y)"
  by (simp add: aa.sup_demorgan d_def)

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

lemma a_mult_deMorgan_2:
  "a(d(x) * d(y)) = a(x)  a(y)"
  by (simp add: d_def sup_def)

lemma a_plus_deMorgan:
  "a(a(x)  a(y)) = d(x) * d(y)"
  by (simp add: aa.sub_sup_demorgan d_def)

lemma a_plus_deMorgan_1:
  "a(d(x)  d(y)) = a(x) * a(y)"
  by (simp add: aa.sup_demorgan d_def)

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)"
  by (simp add: d_def)

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)"
  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)"
  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)"
  by (simp add: aa.l10_iff d_def)

lemma d_d_shunting_zero:
  "d(x) * d(y) = bot  d(x)  a(y)"
  by (simp add: aa.l10_iff d_def)

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

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

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)
  apply (simp add: kat_2)
  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 (simp add: kat_4)
  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