# Theory N_Algebras

```(* Title:      N-Algebras
Author:     Walter Guttmann
Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

section ‹N-Algebras›

theory N_Algebras

imports Stone_Kleene_Relation_Algebras.Iterings Base Lattice_Ordered_Semirings

begin

class C_left_n_algebra = bounded_idempotent_left_semiring + bounded_distrib_lattice + n + L
begin

abbreviation C :: "'a ⇒ 'a" where "C x ≡ n(L) * top ⊓ x"

text ‹AACP Theorem 3.38›

lemma C_isotone:
"x ≤ y ⟶ C x ≤ C y"
using inf.sup_right_isotone by auto

text ‹AACP Theorem 3.40›

lemma C_decreasing:
"C x ≤ x"
by simp

end

class left_n_algebra = C_left_n_algebra +
assumes n_dist_n_add            : "n(x) ⊔ n(y) = n(n(x) * top ⊔ y)"
assumes n_export                : "n(x) * n(y) = n(n(x) * y)"
assumes n_left_upper_bound      : "n(x) ≤ n(x ⊔ y)"
assumes n_nL_meet_L_nL0         : "n(L) * x = (x ⊓ L) ⊔ n(L * bot) * x"
assumes n_n_L_split_n_n_L_L     : "x * n(y) * L = x * bot ⊔ n(x * n(y) * L) * L"
assumes n_sub_nL                : "n(x) ≤ n(L)"
assumes n_L_decreasing          : "n(x) * L ≤ x"
assumes n_L_T_meet_mult_combined: "C (x * y) * z ≤ C x * y * C z"
assumes n_n_top_split_n_top     : "x * n(y) * top ≤ x * bot ⊔ n(x * y) * top"
assumes n_top_meet_L_below_L    : "x * top * y ⊓ L ≤ x * L * y"
begin

subclass lattice_ordered_pre_left_semiring ..

lemma n_L_T_meet_mult_below:
"C (x * y) ≤ C x * y"
proof -
have "C (x * y) ≤ C x * y * C 1"
by (meson order.trans mult_sub_right_one n_L_T_meet_mult_combined)
also have "... ≤ C x * y"
by (metis mult_1_right mult_left_sub_dist_inf_right)
finally show ?thesis
.
qed

text ‹AACP Theorem 3.41›

lemma n_L_T_meet_mult_propagate:
"C x * y ≤ x * C y"
proof -
have "C x * y ≤ C x * 1 * C y"
by (metis mult_1_right mult_assoc n_L_T_meet_mult_combined mult_1_right)
also have "... ≤ x * C y"
finally show ?thesis
.
qed

text ‹AACP Theorem 3.43›

lemma C_n_mult_closed:
"C (n(x) * y) = n(x) * y"
by (simp add: inf.absorb2 mult_isotone n_sub_nL)

text ‹AACP Theorem 3.40›

lemma meet_L_below_C:
"x ⊓ L ≤ C x"

text ‹AACP Theorem 3.42›

lemma n_L_T_meet_mult:
"C (x * y) = C x * y"
apply (rule order.antisym)
apply (rule n_L_T_meet_mult_below)

text ‹AACP Theorem 3.42›

lemma C_mult_propagate:
"C x * y = C x * C y"
by (smt (z3) C_n_mult_closed order.eq_iff inf.left_commute inf.sup_monoid.add_commute mult_left_sub_dist_inf_right n_L_T_meet_mult_propagate)

text ‹AACP Theorem 3.32›

lemma meet_L_below_n_L:
"x ⊓ L ≤ n(L) * x"

text ‹AACP Theorem 3.27›

lemma n_vector_meet_L:
"x * top ⊓ L ≤ x * L"
by (metis mult_1_right n_top_meet_L_below_L)

lemma n_right_upper_bound:
"n(x) ≤ n(y ⊔ x)"

text ‹AACP Theorem 3.1›

lemma n_isotone:
"x ≤ y ⟹ n(x) ≤ n(y)"
by (metis le_iff_sup n_left_upper_bound)

"n(bot) ⊔ n(x) = n(x)"
using le_iff_sup sup_bot_right sup_right_divisibility n_isotone by auto

text ‹AACP Theorem 3.13›

lemma n_mult_right_zero_L:
"n(x) * bot ≤ L"
by (meson bot_least mult_isotone n_L_decreasing n_sub_nL order_trans)

"n(top) ⊔ n(x) = n(top)"

text ‹AACP Theorem 3.18›

lemma n_n_L:
"n(n(x) * L) = n(x)"

lemma n_mult_transitive:
"n(x) * n(x) ≤ n(x)"
by (metis mult_right_isotone n_export n_sub_nL n_n_L)

"n(x) * (n(x) ⊔ n(y)) ≤ n(x)"
by (metis mult_right_isotone n_dist_n_add n_export n_sub_nL n_n_L)

text ‹AACP Theorem 3.21›

lemma n_mult_left_lower_bound:
"n(x) * n(y) ≤ n(x)"
by (metis mult_right_isotone n_export n_sub_nL n_n_L)

text ‹AACP Theorem 3.20›

lemma n_mult_left_zero:
"n(bot) * n(x) = n(bot)"
by (metis n_export sup_absorb1 n_add_left_zero n_mult_left_lower_bound)

lemma n_mult_right_one:
"n(x) * n(top) = n(x)"

lemma n_L_increasing:
"n(x) ≤ n(n(x) * L)"

text ‹AACP Theorem 3.2›

lemma n_galois:
"n(x) ≤ n(y) ⟷ n(x) * L ≤ y"
by (metis mult_left_isotone n_L_decreasing n_L_increasing n_isotone order_trans)

"n(x ⊔ n(x) * top) = n(x)"

text ‹AACP Theorem 3.6›

lemma n_L_below_nL_top:
"L ≤ n(L) * top"
by (metis inf_top.left_neutral meet_L_below_n_L)

text ‹AACP Theorem 3.4›

lemma n_less_eq_char_n:
"x ≤ y ⟷ x ≤ y ⊔ L ∧ C x ≤ y ⊔ n(y) * top"
proof
assume "x ≤ y"
thus "x ≤ y ⊔ L ∧ C x ≤ y ⊔ n(y) * top"
next
assume 1: "x ≤ y ⊔ L ∧ C x ≤ y ⊔ n(y) * top"
hence "x ≤ y ⊔ (x ⊓ L)"
using sup_commute sup_inf_distrib2 by force
also have "... ≤ y ⊔ C x"
using sup_right_isotone meet_L_below_C by blast
also have "... ≤ y ⊔ n(y) * top"
using 1 by simp
finally have "x ≤ y ⊔ (L ⊓ n(y) * top)"
using 1 by (simp add: sup_inf_distrib1)
thus "x ≤ y"
by (metis inf_commute n_L_decreasing order_trans sup_absorb1 n_vector_meet_L)
qed

text ‹AACP Theorem 3.31›

lemma n_L_decreasing_meet_L:
"n(x) * L ≤ x ⊓ L"
using n_sub_nL n_galois by auto

text ‹AACP Theorem 3.5›

lemma n_zero_L_zero:
"n(bot) * L = bot"

lemma n_L_top_below_L:
"L * top ≤ L"
proof -
have "n(L * bot) * L * top ≤ L * bot"
by (metis dense_top_closed mult_isotone n_L_decreasing zero_vector mult_assoc)
hence "n(L * bot) * L * top ≤ L"
using order_lesseq_imp zero_right_mult_decreasing by blast
hence "n(L) * L * top ≤ L"
by (metis inf.absorb2 n_nL_meet_L_nL0 order.refl sup.absorb_iff1 top_right_mult_increasing mult_assoc)
thus "L * top ≤ L"
by (metis inf.absorb2 inf.sup_monoid.add_commute n_L_decreasing n_L_below_nL_top n_vector_meet_L)
qed

text ‹AACP Theorem 3.9›

lemma n_L_top_L:
"L * top = L"
by (simp add: order.antisym top_right_mult_increasing n_L_top_below_L)

text ‹AACP Theorem 3.10›

lemma n_L_below_L:
"L * x ≤ L"
by (metis mult_right_isotone top.extremum n_L_top_L)

text ‹AACP Theorem 3.7›

lemma n_nL_nT:
"n(L) = n(top)"
using order.eq_iff n_sub_nL n_add_left_top by auto

text ‹AACP Theorem 3.8›

lemma n_L_L:
"n(L) * L = L"
using order.antisym meet_L_below_n_L n_L_decreasing_meet_L by fastforce

lemma n_top_L:
"n(top) * L = L"
using n_L_L n_nL_nT by auto

text ‹AACP Theorem 3.23›

lemma n_n_L_split_n_L:
"x * n(y) * L ≤ x * bot ⊔ n(x * y) * L"
by (metis n_n_L_split_n_n_L_L n_L_decreasing mult_assoc mult_left_isotone mult_right_isotone n_isotone sup_right_isotone)

text ‹AACP Theorem 3.12›

lemma n_L_split_n_L_L:
"x * L = x * bot ⊔ n(x * L) * L"
apply (rule order.antisym)
apply (metis mult_assoc n_n_L_split_n_L n_L_L)

text ‹AACP Theorem 3.11›

lemma n_L_split_L:
"x * L ≤ x * bot ⊔ L"
by (metis n_n_L_split_n_n_L_L n_sub_nL sup_right_isotone mult_assoc n_L_L n_galois)

text ‹AACP Theorem 3.24›

lemma n_split_top:
"x * n(y) * top ≤ x * y ⊔ n(x * y) * top"
proof -
have "x * bot ⊔ n(x * y) * top ≤ x * y ⊔ n(x * y) * top"
by (meson bot_least mult_isotone order.refl sup_left_isotone)
thus ?thesis
using order.trans n_n_top_split_n_top by blast
qed

text ‹AACP Theorem 3.9›

lemma n_L_L_L:
"L * L = L"
by (metis inf.sup_monoid.add_commute inf_absorb1 n_L_below_L n_L_top_L n_vector_meet_L)

text ‹AACP Theorem 3.9›

lemma n_L_top_L_L:
"L * top * L = L"

text ‹AACP Theorem 3.19›

lemma n_n_nL:
"n(x) = n(x) * n(L)"

lemma n_L_mult_idempotent:
"n(L) * n(L) = n(L)"
using n_n_nL by auto

text ‹AACP Theorem 3.22›

lemma n_n_L_n:
"n(x * n(y) * L) ≤ n(x * y)"
by (simp add: mult_right_isotone n_L_decreasing mult_assoc n_isotone)

text ‹AACP Theorem 3.3›

lemma n_less_eq_char:
"x ≤ y ⟷ x ≤ y ⊔ L ∧ x ≤ y ⊔ n(y) * top"
by (meson inf.coboundedI2 le_supI1 n_less_eq_char_n)

text ‹AACP Theorem 3.28›

lemma n_top_meet_L_split_L:
"x * top * y ⊓ L ≤ x * bot ⊔ L * y"
proof -
have "x * top * y ⊓ L ≤ x * bot ⊔ n(x * L) * L * y"
by (smt n_top_meet_L_below_L mult_assoc n_L_L_L n_L_split_n_L_L mult_right_dist_sup mult_left_zero)
also have "... ≤ x * bot ⊔ x * L * y"
using mult_left_isotone n_L_decreasing sup_right_isotone by force
also have "... ≤ x * bot ⊔ (x * bot ⊔ L) * y"
using mult_left_isotone sup_right_isotone n_L_split_L by blast
also have "... = x * bot ⊔ x * bot * y ⊔ L * y"
also have "... = x * bot ⊔ L * y"
finally show ?thesis
.
qed

text ‹AACP Theorem 3.29›

lemma n_top_meet_L_L_meet_L:
"x * top * y ⊓ L = x * L * y ⊓ L"
apply (rule order.antisym)
by (metis inf.sup_monoid.add_commute inf.sup_right_isotone mult_isotone order.refl top.extremum)

lemma n_n_top_below_n_L:
"n(x * top) ≤ n(x * L)"
by (meson order.trans n_L_decreasing_meet_L n_galois n_vector_meet_L)

text ‹AACP Theorem 3.14›

lemma n_n_top_n_L:
"n(x * top) = n(x * L)"
by (metis order.antisym mult_right_isotone n_isotone n_n_top_below_n_L top_greatest)

text ‹AACP Theorem 3.30›

lemma n_meet_L_0_below_0_meet_L:
"(x ⊓ L) * bot ≤ x * bot ⊓ L"
by (meson inf.boundedE inf.boundedI mult_right_sub_dist_inf_left zero_right_mult_decreasing)

text ‹AACP Theorem 3.15›

lemma n_n_L_below_L:
"n(x) * L ≤ x * L"
by (metis mult_assoc mult_left_isotone n_L_L_L n_L_decreasing)

lemma n_n_L_below_n_L_L:
"n(x) * L ≤ n(x * L) * L"
by (simp add: mult_left_isotone n_galois n_n_L_below_L)

text ‹AACP Theorem 3.16›

lemma n_below_n_L:
"n(x) ≤ n(x * L)"

text ‹AACP Theorem 3.17›

lemma n_below_n_L_mult:
"n(x) ≤ n(L) * n(x)"
by (metis n_export order_trans meet_L_below_n_L n_L_decreasing_meet_L n_isotone n_n_L)

text ‹AACP Theorem 3.33›

lemma n_meet_L_below:
"n(x) ⊓ L ≤ x"
by (meson inf.coboundedI1 inf.coboundedI2 le_supI2 sup.cobounded1 top_right_mult_increasing n_less_eq_char)

text ‹AACP Theorem 3.35›

lemma n_meet_L_top_below_n_L:
"(n(x) ⊓ L) * top ≤ n(x) * L"
proof -
have "(n(x) ⊓ L) * top ≤ n(x) * top ⊓ L * top"
by (meson mult_right_sub_dist_inf)
thus ?thesis
by (metis n_L_top_L n_vector_meet_L order_trans)
qed

text ‹AACP Theorem 3.34›

lemma n_meet_L_top_below:
"(n(x) ⊓ L) * top ≤ x"
using order.trans n_L_decreasing n_meet_L_top_below_n_L by blast

text ‹AACP Theorem 3.36›

lemma n_n_meet_L:
"n(x) = n(x ⊓ L)"
by (meson order.antisym inf.cobounded1 n_L_decreasing_meet_L n_galois n_isotone)

lemma n_T_below_n_meet:
"n(x) * top = n(C x) * top"
by (metis inf.absorb2 inf.sup_monoid.add_assoc meet_L_below_C n_n_meet_L)

text ‹AACP Theorem 3.44›

lemma n_C:
"n(C x) = n(x)"
by (metis n_T_below_n_meet n_export n_mult_right_one)

text ‹AACP Theorem 3.37›

lemma n_T_meet_L:
"n(x) * top ⊓ L = n(x) * L"
by (metis antisym_conv n_L_decreasing_meet_L n_n_L n_n_top_n_L n_vector_meet_L)

text ‹AACP Theorem 3.39›

lemma n_L_top_meet_L:
"C L = L"

end

class n_algebra = left_n_algebra + idempotent_left_zero_semiring
begin

(* independence of axioms, checked in n_algebra without the respective axiom: *)
proposition n_dist_n_add            : "n(x) ⊔ n(y) = n(n(x) * top ⊔ y)" (* nitpick [expect=genuine,card=5] *) oops
proposition n_export                : "n(x) * n(y) = n(n(x) * y)" (* nitpick [expect=genuine,card=4] *) oops
proposition n_left_upper_bound      : "n(x) ≤ n(x ⊔ y)" (* nitpick [expect=genuine,card=5] *) oops
proposition n_nL_meet_L_nL0         : "n(L) * x = (x ⊓ L) ⊔ n(L * bot) * x" (* nitpick [expect=genuine,card=2] *) oops
proposition n_n_L_split_n_n_L_L     : "x * n(y) * L = x * bot ⊔ n(x * n(y) * L) * L" (* nitpick [expect=genuine,card=6] *) oops
proposition n_sub_nL                : "n(x) ≤ n(L)" (* nitpick [expect=genuine,card=2] *) oops
proposition n_L_decreasing          : "n(x) * L ≤ x" (* nitpick [expect=genuine,card=3] *) oops
proposition n_L_T_meet_mult_combined: "C (x * y) * z ≤ C x * y * C z" (* nitpick [expect=genuine,card=4] *) oops
proposition n_n_top_split_n_top     : "x * n(y) * top ≤ x * bot ⊔ n(x * y) * top" (* nitpick [expect=genuine,card=4] *) oops
proposition n_top_meet_L_below_L    : "x * top * y ⊓ L ≤ x * L * y" (* nitpick [expect=genuine,card=5] *) oops

text ‹AACP Theorem 3.25›

lemma n_top_split_0:
"n(x) * top * y ≤ x * y ⊔ n(x * bot) * top"
proof -
have 1: "n(x) * top * y ⊓ L ≤ x * y"
using inf.coboundedI1 mult_left_isotone n_L_decreasing_meet_L n_top_meet_L_L_meet_L by force
have "n(x) * top * y = n(x) * n(L) * top * y"
using n_n_nL by auto
also have "... = n(x) * ((top * y ⊓ L) ⊔ n(L * bot) * top * y)"
by (metis mult_assoc n_nL_meet_L_nL0)
also have "... ≤ n(x) * (top * y ⊓ L) ⊔ n(x) * n(L * bot) * top"
by (metis sup_right_isotone mult_assoc mult_left_dist_sup mult_right_isotone top_greatest)
also have "... ≤ (n(x) * top * y ⊓ L) ⊔ n(n(x) * L * bot) * top"
by (smt sup_left_isotone order.trans inf_greatest mult_assoc mult_left_sub_dist_inf_left mult_left_sub_dist_inf_right n_export n_galois n_sub_nL)
also have "... ≤ x * y ⊔ n(n(x) * L * bot) * top"
using 1 sup_left_isotone by blast
also have "... ≤ x * y ⊔ n(x * bot) * top"
using mult_left_isotone n_galois n_isotone order.refl sup_right_isotone by auto
finally show ?thesis
.
qed

text ‹AACP Theorem 3.26›

lemma n_top_split:
"n(x) * top * y ≤ x * y ⊔ n(x * y) * top"
by (metis order.trans sup_bot_right mult_assoc sup_right_isotone mult_left_isotone mult_left_sub_dist_sup_right n_isotone n_top_split_0)

proposition n_zero: "n(bot) = bot" nitpick [expect=genuine,card=2] oops
proposition n_one: "n(1) = bot" nitpick [expect=genuine,card=2] oops
proposition n_nL_one: "n(L) = 1" nitpick [expect=genuine,card=2] oops
proposition n_nT_one: "n(top) = 1" nitpick [expect=genuine,card=2] oops
proposition n_n_zero: "n(x) = n(x * bot)" nitpick [expect=genuine,card=2] oops
proposition n_dist_add: "n(x) ⊔ n(y) = n(x ⊔ y)" nitpick [expect=genuine,card=4] oops
proposition n_L_split: "x * n(y) * L = x * bot ⊔ n(x * y) * L" nitpick [expect=genuine,card=3] oops
proposition n_split: "x ≤ x * bot ⊔ n(x * L) * top" nitpick [expect=genuine,card=2] oops
proposition n_mult_top_1: "n(x * y) ≤ n(x * n(y) * top)" nitpick [expect=genuine,card=3] oops
proposition l91_1: "n(L) * x ≤ n(x * top) * top" nitpick [expect=genuine,card=3] oops
proposition meet_domain_top: "x ⊓ n(y) * top = n(y) * x" nitpick [expect=genuine,card=3] oops
proposition meet_domain_2: "x ⊓ n(y) * top ≤ n(L) * x" nitpick [expect=genuine,card=4] oops
proposition n_nL_top_n_top_meet_L_top_2: "n(L) * x * top ≤ n(x * top ⊓ L) * top" nitpick [expect=genuine,card=3] oops
proposition n_nL_top_n_top_meet_L_top_1: "n(x * top ⊓ L) * top ≤ n(L) * x * top" nitpick [expect=genuine,card=2] oops
proposition l9: "x * bot ⊓ L ≤ n(x * L) * L" nitpick [expect=genuine,card=4] oops
proposition l18_2: "n(x * L) * L ≤ n(x) * L" nitpick [expect=genuine,card=3] oops
proposition l51_1: "n(x) * L ≤ (x ⊓ L) * bot" nitpick [expect=genuine,card=2] oops
proposition l51_2: "(x ⊓ L) * bot ≤ n(x) * L" nitpick [expect=genuine,card=4] oops

proposition n_split_equal: "x ⊔ n(x * L) * top = x * bot ⊔ n(x * L) * top" nitpick [expect=genuine,card=2] oops
proposition n_split_top: "x * top ≤ x * bot ⊔ n(x * L) * top" nitpick [expect=genuine,card=2] oops
proposition n_mult: "n(x * n(y) * L) = n(x * y)" nitpick [expect=genuine,card=3] oops
proposition n_mult_1: "n(x * y) ≤ n(x * n(y) * L)" nitpick [expect=genuine,card=3] oops
proposition n_mult_top: "n(x * n(y) * top) = n(x * y)" nitpick [expect=genuine,card=3] oops
proposition n_mult_right_upper_bound: "n(x * y) ≤ n(z) ⟷ n(x) ≤ n(z) ∧ x * n(y) * L ≤ x * bot ⊔ n(z) * L" nitpick [expect=genuine,card=2] oops
proposition meet_domain: "x ⊓ n(y) * z = n(y) * (x ⊓ z)" nitpick [expect=genuine,card=3] oops
proposition meet_domain_1: "x ⊓ n(y) * z ≤ n(y) * x" nitpick [expect=genuine,card=3] oops
proposition meet_domain_top_3: "x ⊓ n(y) * top ≤ n(y) * x" nitpick [expect=genuine,card=3] oops
proposition n_n_top_n_top_split_n_n_top_top: "n(x) * top ⊔ x * n(y) * top = x * bot ⊔ n(x * n(y) * top) * top" nitpick [expect=genuine,card=2] oops
proposition n_n_top_n_top_split_n_n_top_top_1: "x * bot ⊔ n(x * n(y) * top) * top ≤ n(x) * top ⊔ x * n(y) * top" nitpick [expect=genuine,card=5] oops
proposition n_n_top_n_top_split_n_n_top_top_2: "n(x) * top ⊔ x * n(y) * top ≤ x * bot ⊔ n(x * n(y) * top) * top" nitpick [expect=genuine,card=2] oops
proposition n_nL_top_n_top_meet_L_top: "n(L) * x * top = n(x * top ⊓ L) * top" nitpick [expect=genuine,card=2] oops
proposition l18: "n(x) * L = n(x * L) * L" nitpick [expect=genuine,card=3] oops
proposition l22: "x * bot ⊓ L = n(x) * L" nitpick [expect=genuine,card=2] oops
proposition l22_1: "x * bot ⊓ L = n(x * L) * L" nitpick [expect=genuine,card=2] oops
proposition l22_2: "x ⊓ L = n(x) * L" nitpick [expect=genuine,card=3] oops
proposition l22_3: "x ⊓ L = n(x * L) * L" nitpick [expect=genuine,card=3] oops
proposition l22_4: "x ⊓ L ≤ n(x) * L" nitpick [expect=genuine,card=3] oops
proposition l22_5: "x * bot ⊓ L ≤ n(x) * L" nitpick [expect=genuine,card=4] oops
proposition l23: "x * top ⊓ L = n(x) * L" nitpick [expect=genuine,card=3] oops
proposition l51: "n(x) * L = (x ⊓ L) * bot" nitpick [expect=genuine,card=2] oops
proposition l91: "x = x * top ⟶ n(L) * x ≤ n(x) * top" nitpick [expect=genuine,card=3] oops
proposition l92: "x = x * top ⟶ n(L) * x ≤ n(x ⊓ L) * top" nitpick [expect=genuine,card=3] oops
proposition "x ⊓ L ≤ n(x) * top" nitpick [expect=genuine,card=3] oops
proposition n_meet_comp: "n(x) ⊓ n(y) ≤ n(x) * n(y)" nitpick [expect=genuine,card=3] oops

proposition n_n_meet_L_n_zero: "n(x) = (n(x) ⊓ L) ⊔ n(x * bot)" oops
proposition n_below_n_zero: "n(x) ≤ x ⊔ n(x * bot)" oops
proposition n_n_top_split_n_L_n_zero_top: "n(x) * top = n(x) * L ⊔ n(x * bot) * top" oops
proposition n_meet_L_0_0_meet_L: "(x ⊓ L) * bot = x * bot ⊓ L" oops

end

end

```