# 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
by simp

end

text ‹M0-algebra›

context lattice_ordered_pre_left_semiring
begin

text ‹Section 7›

lemma vector_1:
"vector x ⟷ x * top ≤ x"

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
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"

text ‹Theorem 10 / Figure 3: closure properties›

text ‹zero-vector›

lemma zero_zero_vector:
"zero_vector bot"

lemma sup_zero_vector:
"zero_vector x ⟹ zero_vector y ⟹ zero_vector (x ⊔ y)"

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"

lemma one_one_vector:
"one_vector 1"

lemma top_one_vector:
"one_vector top"

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"

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"

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"

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"

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"

lemma top_down_closed:
"down_closed top"

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)"

lemma inf_down_closed:
"down_closed x ⟹ down_closed y ⟹ down_closed (x ⊓ y)"

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
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)"

lemma transitive_sup_distributive_complement:
"transitive x ⟹ sup_distributive (-x)"

lemma transitive_inf_distributive_complement:
"transitive x ⟹ inf_distributive (-x)"

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)"

lemma up_closed_sup_distributive_complement:
"up_closed x ⟹ sup_distributive (-x)"

lemma up_closed_inf_distributive_complement:
"up_closed x ⟹ inf_distributive (-x)"

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"

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
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"
also have "... = x * top ⊓ ((x * top ⊓ y) * z ⊔ (-(x * top) ⊓ y) * z)"
also have "... = (x * top ⊓ (x * top ⊓ y) * z) ⊔ (x * top ⊓ (-(x * top) ⊓ y) * z)"
also have "... ≤ (x * top ⊓ y) * z ⊔ (x * top ⊓ (-(x * top) ⊓ y) * z)"
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"
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"

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"

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"

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"

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"

lemma zero_vector_b:
"zero_vector x ⟷ -x * bot ≤ -x"

lemma one_vector_b1:
"one_vector x ⟷ -x ≤ -x * bot"

lemma one_vector_b0:
"one_vector x ⟷ (∀y z . -x * y = -x * z)"

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)"

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
using mult_right_dist_inf vector_zero_inf_comp by auto

lemma complement_zero_vector:
"zero_vector x ⟷ zero_vector (-x)"

lemma down_closed:
"down_closed x"