Theory Boolean_Semirings

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

section ‹Boolean Semirings›

theory Boolean_Semirings

imports Stone_Algebras.P_Algebras Lattice_Ordered_Semirings

begin

class complemented_distributive_lattice = bounded_distrib_lattice + uminus +
  assumes inf_complement: "x ⊓ (-x) = bot"
  assumes sup_complement: "x ⊔ (-x) = top"
begin

sublocale boolean_algebra where minus = "λx y . x ⊓ (-y)" and inf = inf and sup = sup and bot = bot and top = top
  apply unfold_locales
  apply (simp add: inf_complement)
  apply (simp add: sup_complement)
  by simp

end

text ‹M0-algebra›

context lattice_ordered_pre_left_semiring
begin

text ‹Section 7›

lemma vector_1:
  "vector x ⟷ x * top ≤ x"
  by (simp add: antisym_conv top_right_mult_increasing)

definition zero_vector :: "'a ⇒ bool" where "zero_vector x ≡ x ≤ x * bot"
definition one_vector :: "'a ⇒ bool" where "one_vector x ≡ x * bot ≤ x"

lemma zero_vector_left_zero:
  assumes "zero_vector x"
    shows "x * y = x * bot"
proof -
  have "x * y ≤ x * bot"
    by (metis assms mult_isotone top.extremum vector_mult_closed zero_vector zero_vector_def)
  thus ?thesis
    by (simp add: order.antisym mult_right_isotone)
qed

lemma zero_vector_1:
  "zero_vector x ⟷ (∀y . x * y = x * bot)"
  by (metis top_right_mult_increasing zero_vector_def zero_vector_left_zero)

lemma zero_vector_2:
  "zero_vector x ⟷ (∀y . x * y ≤ x * bot)"
  by (metis eq_refl order_trans top_right_mult_increasing zero_vector_def zero_vector_left_zero)

lemma zero_vector_3:
  "zero_vector x ⟷ x * 1 = x * bot"
  by (metis mult_sub_right_one zero_vector_def zero_vector_left_zero)

lemma zero_vector_4:
  "zero_vector x ⟷ x * 1 ≤ x * bot"
  using order.antisym mult_right_isotone zero_vector_3 by auto

lemma zero_vector_5:
  "zero_vector x ⟷ x * top = x * bot"
  by (metis top_right_mult_increasing zero_vector_def zero_vector_left_zero)

lemma zero_vector_6:
  "zero_vector x ⟷ x * top ≤ x * bot"
  by (meson mult_right_isotone order_trans top.extremum zero_vector_2)

lemma zero_vector_7:
  "zero_vector x ⟷ (∀y . x * top = x * y)"
  by (metis zero_vector_1)

lemma zero_vector_8:
  "zero_vector x ⟷ (∀y . x * top ≤ x * y)"
  by (metis zero_vector_6 zero_vector_left_zero)

lemma zero_vector_9:
  "zero_vector x ⟷ (∀y . x * 1 = x * y)"
  by (metis zero_vector_1)

lemma zero_vector_0:
  "zero_vector x ⟷ (∀y z . x * y = x * z)"
  by (metis zero_vector_5 zero_vector_left_zero)

text ‹Theorem 6 / Figure 2: relations between properties›

lemma co_vector_zero_vector_one_vector:
  "co_vector x ⟷ zero_vector x ∧ one_vector x"
  using co_vector_def one_vector_def zero_vector_def by auto

lemma up_closed_one_vector:
  "up_closed x ⟹ one_vector x"
  by (metis bot_least mult_right_isotone up_closed_def one_vector_def)

lemma zero_vector_dense:
  "zero_vector x ⟹ dense_rel x"
  by (metis zero_vector_0 zero_vector_def)

lemma zero_vector_sup_distributive:
  "zero_vector x ⟹ sup_distributive x"
  by (metis sup_distributive_def sup_idem zero_vector_0)

lemma zero_vector_inf_distributive:
  "zero_vector x ⟹ inf_distributive x"
  by (metis inf_idem inf_distributive_def zero_vector_0)

lemma up_closed_zero_vector_vector:
  "up_closed x ⟹ zero_vector x ⟹ vector x"
  by (metis up_closed_def zero_vector_0)

lemma zero_vector_one_vector_vector:
  "zero_vector x ⟹ one_vector x ⟹ vector x"
  by (metis one_vector_def vector_1 zero_vector_0)

lemma co_vector_vector:
  "co_vector x ⟹ vector x"
  by (simp add: co_vector_zero_vector_one_vector zero_vector_one_vector_vector)

text ‹Theorem 10 / Figure 3: closure properties›

text ‹zero-vector›

lemma zero_zero_vector:
  "zero_vector bot"
  by (simp add: zero_vector_def)

lemma sup_zero_vector:
  "zero_vector x ⟹ zero_vector y ⟹ zero_vector (x ⊔ y)"
  by (simp add: mult_right_dist_sup zero_vector_3)

lemma comp_zero_vector:
  "zero_vector x ⟹ zero_vector y ⟹ zero_vector (x * y)"
  by (metis mult_one_associative zero_vector_0)

text ‹one-vector›

lemma zero_one_vector:
  "one_vector bot"
  by (simp add: one_vector_def)

lemma one_one_vector:
  "one_vector 1"
  by (simp add: one_up_closed up_closed_one_vector)

lemma top_one_vector:
  "one_vector top"
  by (simp add: one_vector_def)

lemma sup_one_vector:
  "one_vector x ⟹ one_vector y ⟹ one_vector (x ⊔ y)"
  by (simp add: mult_right_dist_sup order_trans one_vector_def)

lemma inf_one_vector:
  "one_vector x ⟹ one_vector y ⟹ one_vector (x ⊓ y)"
  by (meson order.trans inf.boundedI mult_right_sub_dist_inf_left mult_right_sub_dist_inf_right one_vector_def)

lemma comp_one_vector:
  "one_vector x ⟹ one_vector y ⟹ one_vector (x * y)"
  using mult_isotone mult_semi_associative order_lesseq_imp one_vector_def by blast

end

context multirelation_algebra_1
begin

text ‹Theorem 10 / Figure 3: closure properties›

text ‹zero-vector›

lemma top_zero_vector:
   "zero_vector top"
  by (simp add: mult_left_top zero_vector_def)

end

text ‹M1-algebra›

context multirelation_algebra_2
begin

text ‹Section 7›

lemma zero_vector_10:
  "zero_vector x ⟷ x * top = x * 1"
  by (metis mult_one_associative mult_top_associative zero_vector_7)

lemma zero_vector_11:
  "zero_vector x ⟷ x * top ≤ x * 1"
  using order.antisym mult_right_isotone zero_vector_10 by fastforce

text ‹Theorem 6 / Figure 2: relations between properties›

lemma vector_zero_vector:
  "vector x ⟹ zero_vector x"
  by (simp add: zero_vector_def vector_left_annihilator)

lemma vector_up_closed_zero_vector:
  "vector x ⟷ up_closed x ∧ zero_vector x"
  using up_closed_zero_vector_vector vector_up_closed vector_zero_vector by blast

lemma vector_zero_vector_one_vector:
  "vector x ⟷ zero_vector x ∧ one_vector x"
  by (simp add: co_vector_zero_vector_one_vector vector_co_vector)

proposition "(x * bot ⊓ y) * 1 = x * bot ⊓ y * 1" nitpick [expect=genuine,card=7] oops

end

text ‹M3-algebra›

context up_closed_multirelation_algebra
begin

lemma up_closed:
  "up_closed x"
  by (simp add: up_closed_def)

lemma dedekind_1_left:
  "x * 1 ⊓ y ≤ (x ⊓ y * 1) * 1"
  by simp

text ‹Theorem 10 / Figure 3: closure properties›

text ‹zero-vector›

lemma zero_vector_dual:
  "zero_vector x ⟷ zero_vector (x⇧^d)"
  using up_closed_zero_vector_vector vector_dual vector_zero_vector up_closed by blast

end

text ‹complemented M0-algebra›

class lattice_ordered_pre_left_semiring_b = lattice_ordered_pre_left_semiring + complemented_distributive_lattice
begin

definition down_closed :: "'a ⇒ bool" where "down_closed x ≡ -x * 1 ≤ -x"

text ‹Theorem 10 / Figure 3: closure properties›

text ‹down-closed›

lemma zero_down_closed:
  "down_closed bot"
  by (simp add: down_closed_def)

lemma top_down_closed:
  "down_closed top"
  by (simp add: down_closed_def)

lemma complement_down_closed_up_closed:
  "down_closed x ⟷ up_closed (-x)"
  using down_closed_def order.antisym mult_sub_right_one up_closed_def by auto

lemma sup_down_closed:
  "down_closed x ⟹ down_closed y ⟹ down_closed (x ⊔ y)"
  by (simp add: complement_down_closed_up_closed inf_up_closed)

lemma inf_down_closed:
  "down_closed x ⟹ down_closed y ⟹ down_closed (x ⊓ y)"
  by (simp add: complement_down_closed_up_closed sup_up_closed)

end

class multirelation_algebra_1b = multirelation_algebra_1 + complemented_distributive_lattice
begin

subclass lattice_ordered_pre_left_semiring_b ..

text ‹Theorem 7.1›

lemma complement_mult_zero_sub:
  "-(x * bot) ≤ -x * bot"
proof -
  have "top = -x * bot ⊔ x * bot"
    by (metis compl_sup_top mult_left_top mult_right_dist_sup)
  thus ?thesis
    by (simp add: heyting.implies_order sup.commute)
qed

text ‹Theorem 7.2›

lemma transitive_zero_vector_complement:
  "transitive x ⟹ zero_vector (-x)"
  by (meson complement_mult_zero_sub compl_mono mult_right_isotone order_trans zero_vector_def bot_least)

lemma transitive_dense_complement:
  "transitive x ⟹ dense_rel (-x)"
  by (simp add: zero_vector_dense transitive_zero_vector_complement)

lemma transitive_sup_distributive_complement:
  "transitive x ⟹ sup_distributive (-x)"
  by (simp add: zero_vector_sup_distributive transitive_zero_vector_complement)

lemma transitive_inf_distributive_complement:
  "transitive x ⟹ inf_distributive (-x)"
  by (simp add: zero_vector_inf_distributive transitive_zero_vector_complement)

lemma up_closed_zero_vector_complement:
  "up_closed x ⟹ zero_vector (-x)"
  by (meson complement_mult_zero_sub compl_le_swap2 one_vector_def order_trans up_closed_one_vector zero_vector_def)

lemma up_closed_dense_complement:
  "up_closed x ⟹ dense_rel (-x)"
  by (simp add: zero_vector_dense up_closed_zero_vector_complement)

lemma up_closed_sup_distributive_complement:
  "up_closed x ⟹ sup_distributive (-x)"
  by (simp add: zero_vector_sup_distributive up_closed_zero_vector_complement)

lemma up_closed_inf_distributive_complement:
  "up_closed x ⟹ inf_distributive (-x)"
  by (simp add: zero_vector_inf_distributive up_closed_zero_vector_complement)

text ‹Theorem 10 / Figure 3: closure properties›

text ‹closure under complement›

lemma co_total_total:
  "co_total x ⟹ total (-x)"
  by (metis complement_mult_zero_sub co_total_def compl_bot_eq mult_left_sub_dist_sup_right sup_bot_right top_le)

lemma complement_one_vector_zero_vector:
  "one_vector x ⟹ zero_vector (-x)"
  using compl_mono complement_mult_zero_sub one_vector_def order_trans zero_vector_def by blast

text ‹Theorem 6 / Figure 2: relations between properties›

lemma down_closed_zero_vector:
  "down_closed x ⟹ zero_vector x"
  using complement_down_closed_up_closed up_closed_zero_vector_complement by force

lemma down_closed_one_vector_vector:
  "down_closed x ⟹ one_vector x ⟹ vector x"
  by (simp add: down_closed_zero_vector zero_vector_one_vector_vector)

proposition complement_vector: "vector x ⟶ vector (-x)" nitpick [expect=genuine,card=8] oops

end

class multirelation_algebra_1c = multirelation_algebra_1b +
  assumes dedekind_top_left: "x * top ⊓ y ≤ (x ⊓ y * top) * top"
  assumes comp_zero_inf: "(x * bot ⊓ y) * bot ≤ (x ⊓ y) * bot"
begin

text ‹Theorem 7.3›

lemma schroeder_top_sub:
  "-(x * top) * top ≤ -x"
proof -
  have "-(x * top) * top ⊓ x ≤ bot"
    by (metis dedekind_top_left p_inf zero_vector)
  thus ?thesis
    by (simp add: shunting_1)
qed

text ‹Theorem 7.4›

lemma schroeder_top:
  "x * top ≤ y ⟷ -y * top ≤ -x"
  apply (rule iffI)
  using compl_mono inf.order_trans mult_left_isotone schroeder_top_sub apply blast
  by (metis compl_mono double_compl mult_left_isotone order_trans schroeder_top_sub)

text ‹Theorem 7.5›

lemma schroeder_top_eq:
  "-(x * top) * top = -(x * top)"
  using vector_1 vector_mult_closed vector_top_closed schroeder_top by auto

lemma schroeder_one_eq:
  "-(x * top) * 1 = -(x * top)"
  by (metis top_mult_right_one schroeder_top_eq)

text ‹Theorem 7.6›

lemma vector_inf_comp:
  "x * top ⊓ y * z = (x * top ⊓ y) * z"
proof (rule order.antisym)
  have "x * top ⊓ y * z = x * top ⊓ ((x * top ⊓ y) ⊔ (-(x * top) ⊓ y)) * z"
    by (simp add: inf_commute)
  also have "... = x * top ⊓ ((x * top ⊓ y) * z ⊔ (-(x * top) ⊓ y) * z)"
    by (simp add: inf_sup_distrib2 mult_right_dist_sup)
  also have "... = (x * top ⊓ (x * top ⊓ y) * z) ⊔ (x * top ⊓ (-(x * top) ⊓ y) * z)"
    by (simp add: inf_sup_distrib1)
  also have "... ≤ (x * top ⊓ y) * z ⊔ (x * top ⊓ (-(x * top) ⊓ y) * z)"
    by (simp add: le_infI2)
  also have "... ≤ (x * top ⊓ y) * z ⊔ (x * top ⊓ -(x * top) * z)"
    by (metis inf.sup_left_isotone inf_commute mult_right_sub_dist_inf_left sup_right_isotone)
  also have "... ≤ (x * top ⊓ y) * z ⊔ (x * top ⊓ -(x * top) * top)"
    using inf.sup_right_isotone mult_right_isotone sup_right_isotone by auto
  also have "... = (x * top ⊓ y) * z"
    by (simp add: schroeder_top_eq)
  finally show "x * top ⊓ y * z ≤ (x * top ⊓ y) * z"
    .
next
  show "(x * top ⊓ y) * z ≤ x * top ⊓ y * z"
    by (metis inf.bounded_iff mult_left_top mult_right_sub_dist_inf_left mult_right_sub_dist_inf_right mult_semi_associative order_lesseq_imp)
qed

(* The following proof is based on ‹vector_inf_comp›, so the latter could serve as axiom instead. *)
lemma dedekind_top_left_var:
  "x * top ⊓ y ≤ (x ⊓ y * top) * top"
  by (metis inf.commute top_right_mult_increasing vector_inf_comp)

text ‹Theorem 7.7›

lemma vector_zero_inf_comp:
  "(x * bot ⊓ y) * z = x * bot ⊓ y * z"
  by (metis vector_inf_comp vector_mult_closed zero_vector)

lemma vector_zero_inf_comp_2:
  "(x * bot ⊓ y) * z = (x * bot ⊓ y * 1) * z"
  by (simp add: vector_zero_inf_comp)

text ‹Theorem 7.8›

lemma comp_zero_inf_2:
  "x * bot ⊓ y * bot = (x ⊓ y) * bot"
  using order.antisym mult_right_sub_dist_inf comp_zero_inf vector_zero_inf_comp by auto

lemma comp_zero_inf_3:
  "x * bot ⊓ y * bot = (x * bot ⊓ y) * bot"
  by (simp add: vector_zero_inf_comp)

lemma comp_zero_inf_4:
  "x * bot ⊓ y * bot = (x * bot ⊓ y * bot) * bot"
  by (metis comp_zero_inf_2 inf.commute vector_zero_inf_comp)

lemma comp_zero_inf_5:
  "x * bot ⊓ y * bot = (x * 1 ⊓ y * 1) * bot"
  by (metis comp_zero_inf_2 mult_one_associative)

lemma comp_zero_inf_6:
  "x * bot ⊓ y * bot = (x * 1 ⊓ y * bot) * bot"
  using inf.sup_monoid.add_commute vector_zero_inf_comp by fastforce

lemma comp_zero_inf_7:
  "x * bot ⊓ y * bot = (x * 1 ⊓ y) * bot"
  by (metis comp_zero_inf_2 mult_one_associative)

text ‹Theorem 10 / Figure 3: closure properties›

text ‹zero-vector›

lemma inf_zero_vector:
  "zero_vector x ⟹ zero_vector y ⟹ zero_vector (x ⊓ y)"
  by (metis comp_zero_inf_2 inf.sup_mono zero_vector_def)

text ‹down-closed›

lemma comp_down_closed:
  "down_closed x ⟹ down_closed y ⟹ down_closed (x * y)"
  by (metis complement_down_closed_up_closed down_closed_zero_vector up_closed_def zero_vector_0 schroeder_one_eq)

text ‹closure under complement›

lemma complement_vector:
  "vector x ⟷ vector (-x)"
  using vector_1 schroeder_top by blast

lemma complement_zero_vector_one_vector:
  "zero_vector x ⟹ one_vector (-x)"
  by (metis comp_zero_inf_2 order.antisym complement_mult_zero_sub double_compl inf.sup_monoid.add_commute mult_left_zero one_vector_def order.refl pseudo_complement top_right_mult_increasing zero_vector_0)

lemma complement_zero_vector_one_vector_iff:
  "zero_vector x ⟷ one_vector (-x)"
  using complement_zero_vector_one_vector complement_one_vector_zero_vector by force

lemma complement_one_vector_zero_vector_iff:
  "one_vector x ⟷ zero_vector (-x)"
  using complement_zero_vector_one_vector complement_one_vector_zero_vector by force

text ‹Theorem 6 / Figure 2: relations between properties›

lemma vector_down_closed:
  "vector x ⟹ down_closed x"
  using complement_vector complement_down_closed_up_closed vector_up_closed by blast

lemma co_vector_down_closed:
  "co_vector x ⟹ down_closed x"
  by (simp add: co_vector_vector vector_down_closed)

lemma vector_down_closed_one_vector:
  "vector x ⟷ down_closed x ∧ one_vector x"
  using down_closed_one_vector_vector up_closed_one_vector vector_up_closed vector_down_closed by blast

lemma vector_up_closed_down_closed:
  "vector x ⟷ up_closed x ∧ down_closed x"
  using down_closed_zero_vector up_closed_zero_vector_vector vector_up_closed vector_down_closed by blast

text ‹Section 7›

lemma vector_b1:
  "vector x ⟷ -x * top = -x"
  using complement_vector by auto

lemma vector_b2:
  "vector x ⟷ -x * bot = -x"
  by (metis down_closed_zero_vector vector_mult_closed zero_vector zero_vector_left_zero vector_b1 vector_down_closed)

lemma covector_b1:
  "co_vector x ⟷ -x * top = -x"
  using co_vector_def co_vector_vector vector_b1 vector_b2 by force

lemma covector_b2:
  "co_vector x ⟷ -x * bot = -x"
  using covector_b1 vector_b1 vector_b2 by auto

lemma vector_co_vector_iff:
  "vector x ⟷ co_vector x"
  by (simp add: covector_b2 vector_b2)

lemma zero_vector_b:
  "zero_vector x ⟷ -x * bot ≤ -x"
  by (simp add: complement_zero_vector_one_vector_iff one_vector_def)

lemma one_vector_b1:
  "one_vector x ⟷ -x ≤ -x * bot"
  by (simp add: complement_one_vector_zero_vector_iff zero_vector_def)

lemma one_vector_b0:
  "one_vector x ⟷ (∀y z . -x * y = -x * z)"
  by (simp add: complement_one_vector_zero_vector_iff zero_vector_0)

proposition schroeder_one: "x * -1 ≤ y ⟷ -y * -1 ≤ -x" nitpick [expect=genuine,card=8] oops

end

class multirelation_algebra_2b = multirelation_algebra_2 + complemented_distributive_lattice
begin

subclass multirelation_algebra_1b ..

proposition "-x * bot ≤ -(x * bot)" nitpick [expect=genuine,card=8] oops

end

text ‹complemented M1-algebra›

class multirelation_algebra_2c = multirelation_algebra_2b + multirelation_algebra_1c

class multirelation_algebra_3b = multirelation_algebra_3 + complemented_distributive_lattice
begin

subclass lattice_ordered_pre_left_semiring_b ..

lemma dual_complement_commute:
  "-(x⇧^d) = (-x)⇧^d"
  by (metis compl_unique dual_dist_sup dual_dist_inf dual_top dual_zero inf_complement sup_compl_top)

end

text ‹complemented M2-algebra›

class multirelation_algebra_5b = multirelation_algebra_5 + complemented_distributive_lattice
begin

subclass multirelation_algebra_2b ..

subclass multirelation_algebra_3b ..

lemma dual_down_closed:
  "down_closed x ⟷ down_closed (x⇧^d)"
  using complement_down_closed_up_closed dual_complement_commute dual_up_closed by auto

end

class multirelation_algebra_5c = multirelation_algebra_5b + multirelation_algebra_1c
begin

lemma complement_mult_zero_below:
  "-x * bot ≤ -(x * bot)"
  by (simp add: comp_zero_inf_2 shunting_1)

proposition "x * 1 ⊓ y * 1 ≤ (x ⊓ y) * 1" nitpick [expect=genuine,card=4] oops
proposition "x * 1 ⊓ (y * 1) ≤ (x * 1 ⊓ y) * 1" nitpick [expect=genuine,card=4] oops

end

class up_closed_multirelation_algebra_b = up_closed_multirelation_algebra + complemented_distributive_lattice
begin

subclass multirelation_algebra_5c
  apply unfold_locales
  apply (metis inf.sup_monoid.add_commute top_right_mult_increasing vector_inf_comp)
  using mult_right_dist_inf vector_zero_inf_comp by auto

lemma complement_zero_vector:
  "zero_vector x ⟷ zero_vector (-x)"
  by (simp add: zero_right_mult_decreasing zero_vector_b)

lemma down_closed:
  "down_closed x"
  by (simp add: down_closed_def)

lemma vector:
  "vector x"
  by (simp add: down_closed up_closed_def vector_up_closed_down_closed)

end

end