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

lemma mult_left_sub_dist_inf_right:
"x * (y ⊓ z) ≤ x * z"

lemma mult_right_sub_dist_inf_left:
"(x ⊓ y) * z ≤ x * z"

lemma mult_right_sub_dist_inf_right:
"(x ⊓ y) * z ≤ y * z"

lemma mult_right_sub_dist_inf:
"(x ⊓ y) * z ≤ x * z ⊓ y * z"

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"

lemma idempotent_transitive_dense:
"idempotent x ⟷ transitive x ∧ dense_rel x"

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"

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"

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

text ‹co-total›

lemma zero_co_total:
"co_total bot"

lemma one_co_total:
"co_total 1"

lemma sup_co_total:
"co_total x ⟹ co_total y ⟹ co_total (x ⊔ y)"

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"

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

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

lemma comp_coreflexive:
"coreflexive x ⟹ coreflexive y ⟹ coreflexive (x * y)"

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"

lemma one_up_closed:
"up_closed 1"

lemma top_up_closed:
"up_closed top"

lemma sup_up_closed:
"up_closed x ⟹ up_closed y ⟹ up_closed (x ⊔ y)"

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)

lemma zero_sup_distributive:
"sup_distributive bot"

lemma one_sup_distributive:
"sup_distributive 1"

lemma sup_sup_distributive:
"sup_distributive x ⟹ sup_distributive y ⟹ sup_distributive (x ⊔ y)"

text ‹inf-distributive›

lemma zero_inf_distributive:
"inf_distributive bot"

lemma one_inf_distributive:
"inf_distributive 1"

text ‹contact›

lemma one_contact:
"contact 1"

lemma top_contact:
"contact top"

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"

lemma one_kernel:
"kernel 1"

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

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"

lemma one_test:
"test 1"

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"

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

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

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"

lemma mult_zero_sup_dist:
"(x * bot ⊔ y) * z = x * bot ⊔ y * z"

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"

lemma top_inf_distributive:
"inf_distributive 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"

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"

lemma vector_inf_distributive:
"vector x ⟹ inf_distributive x"

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

end

class dual =
fixes dual :: "'a ⇒ 'a" ("_⇧d" [100] 100)

class multirelation_algebra_3 = lattice_ordered_pre_left_semiring + dual +
assumes dual_involutive: "x⇧d⇧d = x"
assumes dual_dist_sup: "(x ⊔ y)⇧d = x⇧d ⊓ y⇧d"
assumes dual_one: "1⇧d = 1"
begin

lemma dual_dist_inf:
"(x ⊓ y)⇧d = x⇧d ⊔ y⇧d"
by (metis dual_dist_sup dual_involutive)

lemma dual_antitone:
"x ≤ y ⟹ y⇧d ≤ x⇧d"
using dual_dist_sup sup_right_divisibility by fastforce

lemma dual_zero:
"bot⇧d = top"
by (metis dual_antitone bot_least dual_involutive top_le)

lemma dual_top:
"top⇧d = bot"
using dual_zero dual_involutive by auto

text ‹AAMP Theorem 10 / Figure 3: closure properties›

lemma reflexive_coreflexive_dual:
"reflexive x ⟷ coreflexive (x⇧d)"
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 ≤ x⇧d * y⇧d"
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 * y⇧d"
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 (x⇧d)"
by (metis co_total_def dual_sub_dist_comp dual_zero top_le)

lemma transitive_dense_dual:
"transitive x ⟹ dense_rel (x⇧d)"
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 * y⇧d"
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 ⟹ x⇧d * y⇧d ≤ (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 = x⇧d * y⇧d"

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 (x⇧d)"
by (metis dual_involutive dual_one up_closed_def strong_up_closed_2)

text ‹contact›

lemma contact_kernel_dual:
"contact x ⟷ kernel (x⇧d)"
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)

lemma sup_dist_contact_inf_dist_kernel_dual:
"sup_dist_contact x ⟷ inf_dist_kernel (x⇧d)"
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 (x⇧d)"
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 (x⇧d)"
using 1 contact_kernel_dual sup_dist_contact_def inf_dist_kernel_def by blast
next
assume 3: "inf_dist_kernel (x⇧d)"
hence 4: "up_closed (x⇧d)"
using kernel_up_closed inf_dist_kernel_def by auto
have "inf_distributive (x⇧d)"
using 3 inf_dist_kernel_def by auto
hence "sup_distributive (x⇧d⇧d)"
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 (x⇧d)"
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 (x⇧d)"
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 * y⇧d ≤ (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 = x⇧d * y⇧d"
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

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"

text ‹AAMP Theorem 10 / Figure 3: closure properties›

text ‹total›

lemma inf_total:
"total x ⟹ total y ⟹ total (x ⊓ y)"

lemma comp_total:
"total x ⟹ total y ⟹ total (x * y)"

lemma total_co_total_dual:
"total x ⟷ co_total (x⇧d)"
by (metis co_total_def dual_dist_comp dual_involutive dual_top)

text ‹dense›

lemma transitive_iff_dense_dual:
"transitive x ⟷ dense_rel (x⇧d)"
by (metis dual_antitone dual_dist_comp dual_involutive)

text ‹idempotent›

lemma idempotent_dual:
"idempotent x ⟷ idempotent (x⇧d)"
using dual_involutive idempotent_transitive_dense transitive_iff_dense_dual by auto

lemma comp_sup_distributive:
"sup_distributive x ⟹ sup_distributive y ⟹ sup_distributive (x * y)"

lemma sup_inf_distributive_dual:
"sup_distributive x ⟷ inf_distributive (x⇧d)"
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)"

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 ⊓ x⇧d * 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"

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