Theory Lattice_Ordered_Semirings

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

section Lattice-Ordered Semirings

theory Lattice_Ordered_Semirings

imports Stone_Relation_Algebras.Semirings

begin

nitpick_params [timeout = 600]

text Many results in this theory are taken from a joint paper with Rudolf Berghammer.

text M0-algebra

class lattice_ordered_pre_left_semiring = pre_left_semiring + bounded_distrib_lattice
begin

subclass bounded_pre_left_semiring
  apply unfold_locales
  by simp

lemma top_mult_right_one:
  "x * top = x * top * 1"
  by (metis order.antisym mult_sub_right_one mult_sup_associative_one surjective_one_closed)

lemma mult_left_sub_dist_inf_left:
  "x * (y  z)  x * y"
  by (simp add: mult_right_isotone)

lemma mult_left_sub_dist_inf_right:
  "x * (y  z)  x * z"
  by (simp add: mult_right_isotone)

lemma mult_right_sub_dist_inf_left:
  "(x  y) * z  x * z"
  by (simp add: mult_left_isotone)

lemma mult_right_sub_dist_inf_right:
  "(x  y) * z  y * z"
  by (simp add: mult_left_isotone)

lemma mult_right_sub_dist_inf:
  "(x  y) * z  x * z  y * z"
  by (simp add: mult_right_sub_dist_inf_left mult_right_sub_dist_inf_right)

text Figure 1: fundamental properties

definition co_total          :: "'a  bool" where "co_total x  x * bot = bot"
definition up_closed         :: "'a  bool" where "up_closed x  x * 1 = x"
definition sup_distributive  :: "'a  bool" where "sup_distributive x  (y z . x * (y  z) = x * y  x * z)"
definition inf_distributive  :: "'a  bool" where "inf_distributive x  (y z . x * (y  z) = x * y  x * z)"
definition contact           :: "'a  bool" where "contact x  x * x  1 = x"
definition kernel            :: "'a  bool" where "kernel x  x * x  1 = x * 1"
definition sup_dist_contact  :: "'a  bool" where "sup_dist_contact x  sup_distributive x  contact x"
definition inf_dist_kernel   :: "'a  bool" where "inf_dist_kernel x  inf_distributive x  kernel x"
definition test              :: "'a  bool" where "test x  x * top  1 = x"
definition co_test           :: "'a  bool" where "co_test x  x * bot  1 = x"
definition co_vector         :: "'a  bool" where "co_vector x  x * bot = x"

text AAMP Theorem 6 / Figure 2: relations between properties

lemma reflexive_total:
  "reflexive x  total x"
  using sup_left_divisibility total_sup_closed by force

lemma reflexive_dense:
  "reflexive x  dense_rel x"
  using mult_left_isotone by fastforce

lemma reflexive_transitive_up_closed:
  "reflexive x  transitive x  up_closed x"
  by (metis antisym_conv mult_isotone mult_sub_right_one reflexive_dense up_closed_def)

lemma coreflexive_co_total:
  "coreflexive x  co_total x"
  by (metis co_total_def order.eq_iff mult_left_isotone mult_left_one bot_least)

lemma coreflexive_transitive:
  "coreflexive x  transitive x"
  by (simp add: coreflexive_transitive)

lemma idempotent_transitive_dense:
  "idempotent x  transitive x  dense_rel x"
  by (simp add: order.eq_iff)

lemma contact_reflexive:
  "contact x  reflexive x"
  using contact_def sup_right_divisibility by auto

lemma contact_transitive:
  "contact x  transitive x"
  using contact_def sup_left_divisibility by blast

lemma contact_dense:
  "contact x  dense_rel x"
  by (simp add: contact_reflexive reflexive_dense)

lemma contact_idempotent:
  "contact x  idempotent x"
  by (simp add: contact_dense contact_transitive idempotent_transitive_dense)

lemma contact_up_closed:
  "contact x  up_closed x"
  by (simp add: contact_reflexive contact_transitive reflexive_transitive_up_closed)

lemma contact_reflexive_idempotent_up_closed:
  "contact x  reflexive x  idempotent x  up_closed x"
  by (metis contact_def contact_idempotent contact_reflexive contact_up_closed sup_absorb2 sup_monoid.add_commute)

lemma kernel_coreflexive:
  "kernel x  coreflexive x"
  by (metis kernel_def inf.boundedE mult_sub_right_one)

lemma kernel_transitive:
  "kernel x  transitive x"
  by (simp add: coreflexive_transitive kernel_coreflexive)

lemma kernel_dense:
  "kernel x  dense_rel x"
  by (metis kernel_def inf.boundedE mult_sub_right_one)

lemma kernel_idempotent:
  "kernel x  idempotent x"
  by (simp add: idempotent_transitive_dense kernel_dense kernel_transitive)

lemma kernel_up_closed:
  "kernel x  up_closed x"
  by (metis kernel_coreflexive kernel_def kernel_idempotent inf.absorb1 up_closed_def)

lemma kernel_coreflexive_idempotent_up_closed:
  "kernel x  coreflexive x  idempotent x  up_closed x"
  by (metis kernel_coreflexive kernel_def kernel_idempotent inf.absorb1 up_closed_def)

lemma test_coreflexive:
  "test x  coreflexive x"
  using inf.sup_right_divisibility test_def by blast

lemma test_up_closed:
  "test x  up_closed x"
  by (metis order.eq_iff mult_left_one mult_sub_right_one mult_right_sub_dist_inf test_def top_mult_right_one up_closed_def)

lemma co_test_reflexive:
  "co_test x  reflexive x"
  using co_test_def sup_right_divisibility by blast

lemma co_test_transitive:
  "co_test x  transitive x"
  by (smt co_test_def sup_assoc le_iff_sup mult_left_one mult_left_zero mult_right_dist_sup mult_semi_associative)

lemma co_test_idempotent:
  "co_test x  idempotent x"
  by (simp add: co_test_reflexive co_test_transitive idempotent_transitive_dense reflexive_dense)

lemma co_test_up_closed:
  "co_test x  up_closed x"
  by (simp add: co_test_reflexive co_test_transitive reflexive_transitive_up_closed)

lemma co_test_contact:
  "co_test x  contact x"
  by (simp add: co_test_idempotent co_test_reflexive co_test_up_closed contact_reflexive_idempotent_up_closed)

lemma vector_transitive:
  "vector x  transitive x"
  by (metis mult_right_isotone top.extremum)

lemma vector_up_closed:
  "vector x  up_closed x"
  by (metis top_mult_right_one up_closed_def)

text AAMP Theorem 10 / Figure 3: closure properties

text total

lemma one_total:
  "total 1"
  by simp

lemma top_total:
  "total top"
  by simp

lemma sup_total:
  "total x  total y  total (x  y)"
  by (simp add: total_sup_closed)

text co-total

lemma zero_co_total:
  "co_total bot"
  by (simp add: co_total_def)

lemma one_co_total:
  "co_total 1"
  by (simp add: co_total_def)

lemma sup_co_total:
  "co_total x  co_total y  co_total (x  y)"
  by (simp add: co_total_def mult_right_dist_sup)

lemma inf_co_total:
  "co_total x  co_total y  co_total (x  y)"
  by (metis co_total_def order.antisym bot_least mult_right_sub_dist_inf_right)

lemma comp_co_total:
  "co_total x  co_total y  co_total (x * y)"
  by (metis co_total_def order.eq_iff mult_semi_associative bot_least)

text sub-transitive

lemma zero_transitive:
  "transitive bot"
  by (simp add: vector_transitive)

lemma one_transitive:
  "transitive 1"
  by simp

lemma top_transitive:
  "transitive top"
  by simp

lemma inf_transitive:
  "transitive x  transitive y  transitive (x  y)"
  by (meson inf_mono order_trans mult_left_sub_dist_inf_left mult_left_sub_dist_inf_right mult_right_sub_dist_inf)

text dense

lemma zero_dense:
  "dense_rel bot"
  by simp

lemma one_dense:
  "dense_rel 1"
  by simp

lemma top_dense:
  "dense_rel top"
  by simp

lemma sup_dense:
  assumes "dense_rel x"
      and "dense_rel y"
    shows "dense_rel (x  y)"
proof -
  have "x  x * x  y  y * y"
    using assms by auto
  hence "x  (x  y) * (x  y)  y  (x  y) * (x  y)"
    by (meson dense_sup_closed order_trans sup.cobounded1 sup.cobounded2)
  hence "x  y  (x  y) * (x  y)"
    by simp
  thus "dense_rel (x  y)"
    by simp
qed

text reflexive

lemma one_reflexive:
  "reflexive 1"
  by simp

lemma top_reflexive:
  "reflexive top"
  by simp

lemma sup_reflexive:
  "reflexive x  reflexive y  reflexive (x  y)"
  by (simp add: reflexive_sup_closed)

lemma inf_reflexive:
  "reflexive x  reflexive y  reflexive (x  y)"
  by simp

lemma comp_reflexive:
  "reflexive x  reflexive y  reflexive (x * y)"
  using reflexive_mult_closed by auto

text co-reflexive

lemma zero_coreflexive:
  "coreflexive bot"
  by simp

lemma one_coreflexive:
  "coreflexive 1"
  by simp

lemma sup_coreflexive:
  "coreflexive x  coreflexive y  coreflexive (x  y)"
  by simp

lemma inf_coreflexive:
  "coreflexive x  coreflexive y  coreflexive (x  y)"
  by (simp add: le_infI1)

lemma comp_coreflexive:
  "coreflexive x  coreflexive y  coreflexive (x * y)"
  by (simp add: coreflexive_mult_closed)

text idempotent

lemma zero_idempotent:
  "idempotent bot"
  by simp

lemma one_idempotent:
  "idempotent 1"
  by simp

lemma top_idempotent:
  "idempotent top"
  by simp

text up-closed

lemma zero_up_closed:
  "up_closed bot"
  by (simp add: up_closed_def)

lemma one_up_closed:
  "up_closed 1"
  by (simp add: up_closed_def)

lemma top_up_closed:
  "up_closed top"
  by (simp add: vector_up_closed)

lemma sup_up_closed:
  "up_closed x  up_closed y  up_closed (x  y)"
  by (simp add: mult_right_dist_sup up_closed_def)

lemma inf_up_closed:
  "up_closed x  up_closed y  up_closed (x  y)"
  by (metis order.antisym mult_sub_right_one mult_right_sub_dist_inf up_closed_def)

lemma comp_up_closed:
  "up_closed x  up_closed y  up_closed (x * y)"
  by (metis order.antisym mult_semi_associative mult_sub_right_one up_closed_def)

text add-distributive

lemma zero_sup_distributive:
  "sup_distributive bot"
  by (simp add: sup_distributive_def)

lemma one_sup_distributive:
  "sup_distributive 1"
  by (simp add: sup_distributive_def)

lemma sup_sup_distributive:
  "sup_distributive x  sup_distributive y  sup_distributive (x  y)"
  using sup_distributive_def mult_right_dist_sup sup_monoid.add_assoc sup_monoid.add_commute by auto

text inf-distributive

lemma zero_inf_distributive:
  "inf_distributive bot"
  by (simp add: inf_distributive_def)

lemma one_inf_distributive:
  "inf_distributive 1"
  by (simp add: inf_distributive_def)

text contact

lemma one_contact:
  "contact 1"
  by (simp add: contact_def)

lemma top_contact:
  "contact top"
  by (simp add: contact_def)

lemma inf_contact:
  "contact x  contact y  contact (x  y)"
  by (meson contact_reflexive_idempotent_up_closed contact_transitive inf_reflexive inf_transitive inf_up_closed preorder_idempotent)

text kernel

lemma zero_kernel:
  "kernel bot"
  by (simp add: kernel_def)

lemma one_kernel:
  "kernel 1"
  by (simp add: kernel_def)

lemma sup_kernel:
  "kernel x  kernel y  kernel (x  y)"
  using kernel_coreflexive_idempotent_up_closed order.antisym coreflexive_transitive sup_dense sup_up_closed by force

text add-distributive contact

lemma one_sup_dist_contact:
  "sup_dist_contact 1"
  by (simp add: sup_dist_contact_def one_sup_distributive one_contact)

text inf-distributive kernel

lemma zero_inf_dist_kernel:
  "inf_dist_kernel bot"
  by (simp add: inf_dist_kernel_def zero_kernel zero_inf_distributive)

lemma one_inf_dist_kernel:
  "inf_dist_kernel 1"
  by (simp add: inf_dist_kernel_def one_kernel one_inf_distributive)

text test

lemma zero_test:
  "test bot"
  by (simp add: test_def)

lemma one_test:
  "test 1"
  by (simp add: test_def)

lemma sup_test:
  "test x  test y  test (x  y)"
  by (simp add: inf_sup_distrib2 mult_right_dist_sup test_def)

lemma inf_test:
  "test x  test y  test (x  y)"
  by (smt (z3) inf.left_commute idempotent_one_closed inf.le_iff_sup inf_top.right_neutral mult_right_isotone mult_sub_right_one mult_right_sub_dist_inf test_def top_mult_right_one)

text co-test

lemma one_co_test:
  "co_test 1"
  by (simp add: co_test_def)

lemma sup_co_test:
  "co_test x  co_test y  co_test (x  y)"
  by (smt (z3) co_test_def mult_right_dist_sup sup.left_idem sup_assoc sup_commute)

text vector

lemma zero_vector:
  "vector bot"
  by simp

lemma top_vector:
  "vector top"
  by simp

lemma sup_vector:
  "vector x  vector y  vector (x  y)"
  by (simp add: vector_sup_closed)

lemma inf_vector:
  "vector x  vector y  vector (x  y)"
  by (metis order.antisym top_right_mult_increasing mult_right_sub_dist_inf)

lemma comp_vector:
  "vector y  vector (x * y)"
  by (simp add: vector_mult_closed)

end

class lattice_ordered_pre_left_semiring_1 = non_associative_left_semiring + bounded_distrib_lattice +
  assumes mult_associative_one: "x * (y * z) = (x * (y * 1)) * z"
  assumes mult_right_dist_inf_one: "(x * 1  y * 1) * z = x * z  y * z"
begin

subclass pre_left_semiring
  apply unfold_locales
  by (metis mult_associative_one mult_left_isotone mult_right_isotone mult_sub_right_one)

subclass lattice_ordered_pre_left_semiring ..

lemma mult_zero_associative:
  "x * bot * y = x * bot"
  by (metis mult_associative_one mult_left_zero)

lemma mult_zero_sup_one_dist:
  "(x * bot  1) * z = x * bot  z"
  by (simp add: mult_right_dist_sup mult_zero_associative)

lemma mult_zero_sup_dist:
  "(x * bot  y) * z = x * bot  y * z"
  by (simp add: mult_right_dist_sup mult_zero_associative)

lemma vector_zero_inf_one_comp:
  "(x * bot  1) * y = x * bot  y"
  by (metis mult_left_one mult_right_dist_inf_one mult_zero_associative)

text AAMP Theorem 6 / Figure 2: relations between properties

lemma co_test_inf_distributive:
  "co_test x  inf_distributive x"
  by (metis co_test_def distrib_imp1 inf_sup_distrib1 inf_distributive_def mult_zero_sup_one_dist)

lemma co_test_sup_distributive:
  "co_test x  sup_distributive x"
  by (metis sup_sup_distributive sup_distributive_def co_test_def one_sup_distributive sup.idem mult_zero_associative)

lemma co_test_sup_dist_contact:
  "co_test x  sup_dist_contact x"
  by (simp add: co_test_sup_distributive sup_dist_contact_def co_test_contact)

text AAMP Theorem 10 / Figure 3: closure properties

text co-test

lemma inf_co_test:
  "co_test x  co_test y  co_test (x  y)"
  by (smt (z3) co_test_def co_test_up_closed mult_right_dist_inf_one sup_commute sup_inf_distrib1 up_closed_def)

lemma comp_co_test:
  "co_test x  co_test y  co_test (x * y)"
  by (metis co_test_def mult_associative_one sup_assoc mult_zero_sup_one_dist)

end

class lattice_ordered_pre_left_semiring_2 = lattice_ordered_pre_left_semiring +
  assumes mult_sub_associative_one: "x * (y * z)  (x * (y * 1)) * z"
  assumes mult_right_dist_inf_one_sub: "x * z  y * z  (x * 1  y * 1) * z"
begin

subclass lattice_ordered_pre_left_semiring_1
  apply unfold_locales
  apply (simp add: order.antisym mult_sub_associative_one mult_sup_associative_one)
  by (metis order.eq_iff mult_one_associative mult_right_dist_inf_one_sub mult_right_sub_dist_inf)

end

class multirelation_algebra_1 = lattice_ordered_pre_left_semiring +
  assumes mult_left_top: "top * x = top"
begin

text AAMP Theorem 10 / Figure 3: closure properties

lemma top_sup_distributive:
  "sup_distributive top"
  by (simp add: sup_distributive_def mult_left_top)

lemma top_inf_distributive:
  "inf_distributive top"
  by (simp add: inf_distributive_def mult_left_top)

lemma top_sup_dist_contact:
  "sup_dist_contact top"
  by (simp add: sup_dist_contact_def top_contact top_sup_distributive)

lemma top_co_test:
  "co_test top"
  by (simp add: co_test_def mult_left_top)

end

text M1-algebra

class multirelation_algebra_2 = multirelation_algebra_1 + lattice_ordered_pre_left_semiring_2
begin

lemma mult_top_associative:
  "x * top * y = x * top"
  by (metis mult_left_top mult_associative_one)

lemma vector_inf_one_comp:
  "(x * top  1) * y = x * top  y"
  by (metis vector_zero_inf_one_comp mult_top_associative)

lemma vector_left_annihilator:
  "vector x  x * y = x"
  by (metis mult_top_associative)

text properties

lemma test_comp_inf:
  "test x  test y  x * y = x  y"
  by (metis inf.absorb1 inf.left_commute test_coreflexive test_def vector_inf_one_comp)

text AAMP Theorem 6 / Figure 2: relations between properties

lemma test_sup_distributive:
  "test x  sup_distributive x"
  by (metis sup_distributive_def inf_sup_distrib1 test_def vector_inf_one_comp)

lemma test_inf_distributive:
  "test x  inf_distributive x"
  by (smt (verit, ccfv_SIG) inf.commute inf.sup_monoid.add_assoc inf_distributive_def test_def inf.idem vector_inf_one_comp)

lemma test_inf_dist_kernel:
  "test x  inf_dist_kernel x"
  by (simp add: kernel_def inf_dist_kernel_def one_test test_comp_inf test_inf_distributive)

lemma vector_idempotent:
  "vector x  idempotent x"
  using vector_left_annihilator by blast

lemma vector_sup_distributive:
  "vector x  sup_distributive x"
  by (simp add: sup_distributive_def vector_left_annihilator)

lemma vector_inf_distributive:
  "vector x  inf_distributive x"
  by (simp add: inf_distributive_def vector_left_annihilator)

lemma vector_co_vector:
  "vector x  co_vector x"
  by (metis co_vector_def mult_zero_associative mult_top_associative)

text AAMP Theorem 10 / Figure 3: closure properties

text test

lemma comp_test:
  "test x  test y  test (x * y)"
  by (simp add: inf_test test_comp_inf)

end

class dual =
  fixes dual :: "'a  'a" ("_d" [100] 100)

class multirelation_algebra_3 = lattice_ordered_pre_left_semiring + dual +
  assumes dual_involutive: "xdd = x"
  assumes dual_dist_sup: "(x  y)d = xd  yd"
  assumes dual_one: "1d = 1"
begin

lemma dual_dist_inf:
  "(x  y)d = xd  yd"
  by (metis dual_dist_sup dual_involutive)

lemma dual_antitone:
  "x  y  yd  xd"
  using dual_dist_sup sup_right_divisibility by fastforce

lemma dual_zero:
  "botd = top"
  by (metis dual_antitone bot_least dual_involutive top_le)

lemma dual_top:
  "topd = bot"
  using dual_zero dual_involutive by auto

text AAMP Theorem 10 / Figure 3: closure properties

lemma reflexive_coreflexive_dual:
  "reflexive x  coreflexive (xd)"
  using dual_antitone dual_involutive dual_one by fastforce

end

class multirelation_algebra_4 = multirelation_algebra_3 +
  assumes dual_sub_dist_comp: "(x * y)d  xd * yd"
begin

subclass multirelation_algebra_1
  apply unfold_locales
  by (metis order.antisym top.extremum dual_zero dual_sub_dist_comp dual_involutive mult_left_zero)

lemma dual_sub_dist_comp_one:
  "(x * y)d  (x * 1)d * yd"
  by (metis dual_sub_dist_comp mult_one_associative)

text AAMP Theorem 10 / Figure 3: closure properties

lemma co_total_total_dual:
  "co_total x  total (xd)"
  by (metis co_total_def dual_sub_dist_comp dual_zero top_le)

lemma transitive_dense_dual:
  "transitive x  dense_rel (xd)"
  using dual_antitone dual_sub_dist_comp inf.order_lesseq_imp by blast

end

text M2-algebra

class multirelation_algebra_5 = multirelation_algebra_3 +
  assumes dual_dist_comp_one: "(x * y)d = (x * 1)d * yd"
begin

subclass multirelation_algebra_4
  apply unfold_locales
  by (metis dual_antitone mult_sub_right_one mult_left_isotone dual_dist_comp_one)

lemma strong_up_closed:
  "x * 1  x  xd * yd  (x * y)d"
  by (simp add: dual_dist_comp_one antisym_conv mult_sub_right_one)

lemma strong_up_closed_2:
  "up_closed x  (x * y)d = xd * yd"
  by (simp add: dual_dist_comp_one up_closed_def)

subclass lattice_ordered_pre_left_semiring_2
  apply unfold_locales
  apply (smt comp_up_closed dual_antitone dual_dist_comp_one dual_involutive dual_one mult_left_one mult_one_associative mult_semi_associative up_closed_def strong_up_closed_2)
  by (smt dual_dist_comp_one dual_dist_inf dual_involutive eq_refl mult_one_associative mult_right_dist_sup)

text AAMP Theorem 8

subclass multirelation_algebra_2 ..

text AAMP Theorem 10 / Figure 3: closure properties

text up-closed

lemma dual_up_closed:
  "up_closed x  up_closed (xd)"
  by (metis dual_involutive dual_one up_closed_def strong_up_closed_2)

text contact

lemma contact_kernel_dual:
  "contact x  kernel (xd)"
  by (metis contact_def contact_up_closed dual_dist_sup dual_involutive dual_one kernel_def kernel_up_closed up_closed_def strong_up_closed_2)

text add-distributive contact

lemma sup_dist_contact_inf_dist_kernel_dual:
  "sup_dist_contact x  inf_dist_kernel (xd)"
proof
  assume 1: "sup_dist_contact x"
  hence 2: "up_closed x"
    using sup_dist_contact_def contact_up_closed by auto
  have "sup_distributive x"
    using 1 sup_dist_contact_def by auto
  hence "inf_distributive (xd)"
    using 2 by (smt sup_distributive_def dual_dist_comp_one dual_dist_inf dual_involutive inf_distributive_def up_closed_def)
  thus "inf_dist_kernel (xd)"
    using 1 contact_kernel_dual sup_dist_contact_def inf_dist_kernel_def by blast
next
  assume 3: "inf_dist_kernel (xd)"
  hence 4: "up_closed (xd)"
    using kernel_up_closed inf_dist_kernel_def by auto
  have "inf_distributive (xd)"
    using 3 inf_dist_kernel_def by auto
  hence "sup_distributive (xdd)"
    using 4 by (smt inf_distributive_def sup_distributive_def dual_dist_sup dual_involutive strong_up_closed_2)
  thus "sup_dist_contact x"
    using 3 contact_kernel_dual sup_dist_contact_def dual_involutive inf_dist_kernel_def by auto
qed

text test

lemma test_co_test_dual:
  "test x  co_test (xd)"
  by (smt (z3) co_test_def co_test_up_closed dual_dist_comp_one dual_dist_inf dual_involutive dual_one dual_top test_def test_up_closed up_closed_def)

text vector

lemma vector_dual:
  "vector x  vector (xd)"
  by (metis dual_dist_comp_one dual_involutive mult_top_associative)

end

class multirelation_algebra_6 = multirelation_algebra_4 +
  assumes dual_sub_dist_comp_one: "(x * 1)d * yd  (x * y)d"
begin

subclass multirelation_algebra_5
  apply unfold_locales
  by (metis dual_sub_dist_comp dual_sub_dist_comp_one order.eq_iff mult_one_associative)

proposition "dense_rel x  coreflexive x  up_closed x" nitpick [expect=genuine,card=5] oops
proposition "x * top  y * z  (x * top  y) * z" nitpick [expect=genuine,card=8] oops

end

text M3-algebra

class up_closed_multirelation_algebra = multirelation_algebra_3 +
  assumes dual_dist_comp: "(x * y)d = xd * yd"
begin

lemma mult_right_dist_inf:
  "(x  y) * z = x * z  y * z"
  by (metis dual_dist_sup dual_dist_comp dual_involutive mult_right_dist_sup)

text AAMP Theorem 9

subclass idempotent_left_semiring
  apply unfold_locales
  apply (metis order.antisym dual_antitone dual_dist_comp dual_involutive mult_semi_associative)
  apply simp
  by (metis order.antisym dual_antitone dual_dist_comp dual_involutive dual_one mult_sub_right_one)

subclass multirelation_algebra_6
  apply unfold_locales
  by (simp_all add: dual_dist_comp)

lemma vector_inf_comp:
  "(x * top  y) * z = x * top  y * z"
  by (simp add: vector_left_annihilator mult_right_dist_inf mult.assoc)

lemma vector_zero_inf_comp:
  "(x * bot  y) * z = x * bot  y * z"
  by (simp add: mult_right_dist_inf mult.assoc)

text AAMP Theorem 10 / Figure 3: closure properties

text total

lemma inf_total:
  "total x  total y  total (x  y)"
  by (simp add: mult_right_dist_inf)

lemma comp_total:
  "total x  total y  total (x * y)"
  by (simp add: mult_assoc)

lemma total_co_total_dual:
  "total x  co_total (xd)"
  by (metis co_total_def dual_dist_comp dual_involutive dual_top)

text dense

lemma transitive_iff_dense_dual:
  "transitive x  dense_rel (xd)"
  by (metis dual_antitone dual_dist_comp dual_involutive)

text idempotent

lemma idempotent_dual:
  "idempotent x  idempotent (xd)"
  using dual_involutive idempotent_transitive_dense transitive_iff_dense_dual by auto

text add-distributive

lemma comp_sup_distributive:
  "sup_distributive x  sup_distributive y  sup_distributive (x * y)"
  by (simp add: sup_distributive_def mult.assoc)

lemma sup_inf_distributive_dual:
  "sup_distributive x  inf_distributive (xd)"
  by (smt (verit, ccfv_threshold) sup_distributive_def dual_dist_sup dual_dist_comp dual_dist_inf dual_involutive inf_distributive_def)

text inf-distributive

lemma inf_inf_distributive:
  "inf_distributive x  inf_distributive y  inf_distributive (x  y)"
  by (metis sup_inf_distributive_dual sup_sup_distributive dual_dist_inf dual_involutive)

lemma comp_inf_distributive:
  "inf_distributive x  inf_distributive y  inf_distributive (x * y)"
  by (simp add: inf_distributive_def mult.assoc)

proposition "co_total x  transitive x  up_closed x  coreflexive x" nitpick [expect=genuine,card=5] oops
proposition "total x  dense_rel x  up_closed x  reflexive x" nitpick [expect=genuine,card=5] oops
proposition "x * top  xd * bot = bot" nitpick [expect=genuine,card=6] oops

end

class multirelation_algebra_7 = multirelation_algebra_4 +
  assumes vector_inf_comp: "(x * top  y) * z = x * top  y * z"
begin

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

lemma test_sup_distributive:
  "test x  sup_distributive x"
  by (metis sup_distributive_def inf_sup_distrib1 mult_left_one test_def vector_inf_comp)

lemma test_inf_distributive:
  "test x  inf_distributive x"
  by (smt (z3) inf.right_idem inf.sup_monoid.add_assoc inf.sup_monoid.add_commute inf_distributive_def mult_left_one test_def vector_inf_comp)

lemma test_inf_dist_kernel:
  "test x  inf_dist_kernel x"
  by (metis inf.idem inf.sup_monoid.add_assoc kernel_def inf_dist_kernel_def mult_left_one test_def test_inf_distributive vector_inf_comp)

lemma co_test_inf_distributive:
  assumes "co_test x"
    shows "inf_distributive x"
proof -
  have "x = x * bot  1"
    using assms co_test_def by auto
  hence "y z . x * y  x * z = x * (y  z)"
    by (metis distrib_imp1 inf_sup_absorb inf_sup_distrib1 mult_left_one mult_left_top mult_right_dist_sup sup_top_right vector_zero_inf_comp)
  thus "inf_distributive x"
    by (simp add: inf_distributive_def)
qed

lemma co_test_sup_distributive:
  assumes "co_test x"
    shows "sup_distributive x"
proof -
  have "x = x * bot  1"
    using assms co_test_def by auto
  hence "y z . x * (y  z) = x * y  x * z"
    by (metis sup_sup_distributive sup_distributive_def inf_sup_absorb mult_left_top one_sup_distributive sup.idem sup_top_right vector_zero_inf_comp)
  thus "sup_distributive x"
    by (simp add: sup_distributive_def)
qed

lemma co_test_sup_dist_contact:
  "co_test x  sup_dist_contact x"
  by (simp add: sup_dist_contact_def co_test_sup_distributive co_test_contact)

end

end