Theory Boolean_Semirings

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

section ‹Boolean Semirings›

theory Boolean_Semirings

imports Stone_Algebras.P_Algebras Lattice_Ordered_Semirings


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

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


text ‹M0-algebra›

context lattice_ordered_pre_left_semiring

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)

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


context multirelation_algebra_1

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)


text ‹M1-algebra›

context multirelation_algebra_2

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


text ‹M3-algebra›

context up_closed_multirelation_algebra

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 (xd)"
  using up_closed_zero_vector_vector vector_dual vector_zero_vector up_closed by blast


text ‹complemented M0-algebra›

class lattice_ordered_pre_left_semiring_b = lattice_ordered_pre_left_semiring + complemented_distributive_lattice

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)


class multirelation_algebra_1b = multirelation_algebra_1 + complemented_distributive_lattice

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)

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


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"

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)

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

(* 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


class multirelation_algebra_2b = multirelation_algebra_2 + complemented_distributive_lattice

subclass multirelation_algebra_1b ..

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


text ‹complemented M1-algebra›

class multirelation_algebra_2c = multirelation_algebra_2b + multirelation_algebra_1c

class multirelation_algebra_3b = multirelation_algebra_3 + complemented_distributive_lattice

subclass lattice_ordered_pre_left_semiring_b ..

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


text ‹complemented M2-algebra›

class multirelation_algebra_5b = multirelation_algebra_5 + complemented_distributive_lattice

subclass multirelation_algebra_2b ..

subclass multirelation_algebra_3b ..

lemma dual_down_closed:
  "down_closed x  down_closed (xd)"
  using complement_down_closed_up_closed dual_complement_commute dual_up_closed by auto


class multirelation_algebra_5c = multirelation_algebra_5b + multirelation_algebra_1c

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


class up_closed_multirelation_algebra_b = up_closed_multirelation_algebra + complemented_distributive_lattice

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)