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"
    by (simp add: mult_right_sub_dist_inf_right)
  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"
  by (simp add: le_supI1 n_nL_meet_L_nL0)

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)
  by (smt (z3) C_n_mult_closed inf.boundedE inf.sup_monoid.add_assoc inf.sup_monoid.add_commute mult_right_sub_dist_inf mult_assoc)

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"
  by (simp add: n_nL_meet_L_nL0)

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)"
  by (simp add: n_left_upper_bound sup_commute)

text AACP Theorem 3.1

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

lemma n_add_left_zero:
  "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)

lemma n_add_left_top:
  "n(top)  n(x) = n(top)"
  by (simp add: sup_absorb1 n_isotone)

text AACP Theorem 3.18

lemma n_n_L:
  "n(n(x) * L) = n(x)"
  by (metis order.antisym n_dist_n_add n_export n_sub_nL sup_bot_right sup_commute sup_top_left n_add_left_zero n_right_upper_bound)

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

lemma n_mult_left_absorb_add_sub:
  "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)"
  using n_dist_n_add n_export sup_commute n_add_left_zero by fastforce

lemma n_L_increasing:
  "n(x)  n(n(x) * L)"
  by (simp add: n_n_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)

lemma n_add_n_top:
  "n(x  n(x) * top) = n(x)"
  by (metis n_dist_n_add sup.idem sup_commute)

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"
    by (simp add: inf.coboundedI2 le_supI1)
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"
  by (simp add: le_bot n_L_decreasing)

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)
  by (simp add: mult_right_isotone n_L_decreasing)

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"
  by (simp add: n_L_L_L n_L_top_L)

text AACP Theorem 3.19

lemma n_n_nL:
  "n(x) = n(x) * n(L)"
  by (simp add: n_export n_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"
    by (simp add: mult_right_dist_sup sup_assoc)
  also have "... = x * bot  L * y"
    by (simp add: mult_assoc)
  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)
  apply (simp add: n_top_meet_L_below_L)
  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)"
  by (simp add: n_galois n_n_L_below_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"
  by (simp add: n_L_L n_T_meet_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