Theory N_Semirings

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

section N-Semirings

theory N_Semirings

imports Test_Iterings Omega_Algebras

begin

class n_semiring = bounded_idempotent_left_zero_semiring + n + L +
  assumes n_bot         : "n(bot) = bot"
  assumes n_top         : "n(top) = 1"
  assumes n_dist_sup    : "n(x  y) = n(x)  n(y)"
  assumes n_export      : "n(n(x) * y) = n(x) * n(y)"
  assumes n_sub_mult_bot: "n(x) = n(x * bot) * n(x)"
  assumes n_L_split     : "x * n(y) * L = x * bot  n(x * y) * L"
  assumes n_split       : "x  x * bot  n(x * L) * top"
begin

lemma n_sub_one:
  "n(x)  1"
  by (metis sup_left_top sup_ge2 n_dist_sup n_top)

text Theorem 15

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

lemma n_mult_idempotent:
  "n(x) * n(x) = n(x)"
  by (metis mult_assoc mult_1_right n_export n_sub_mult_bot n_top)

text Theorem 15.3

lemma n_mult_bot:
  "n(x) = n(x * bot)"
  by (metis sup_commute sup_left_top sup_bot_right mult_left_dist_sup mult_1_right n_dist_sup n_sub_mult_bot n_top)

lemma n_mult_left_upper_bound:
  "n(x)  n(x * y)"
  by (metis mult_right_isotone n_isotone n_mult_bot bot_least)

lemma n_mult_right_bot:
  "n(x) * bot = bot"
  by (metis sup_left_top sup_bot_left mult_left_one mult_1_right n_export n_dist_sup n_sub_mult_bot n_top n_bot)

text Theorem 15.9

lemma n_mult_n:
  "n(x * n(y)) = n(x)"
  by (metis mult_assoc n_mult_right_bot n_mult_bot)

lemma n_mult_left_absorb_sup:
  "n(x) * (n(x)  n(y)) = n(x)"
  by (metis sup_left_top mult_left_dist_sup mult_1_right n_dist_sup n_mult_idempotent n_top)

lemma n_mult_right_absorb_sup:
  "(n(x)  n(y)) * n(y) = n(y)"
  by (metis sup_commute sup_left_top mult_left_one mult_right_dist_sup n_dist_sup n_mult_idempotent n_top)

lemma n_sup_left_absorb_mult:
  "n(x)  n(x) * n(y) = n(x)"
  using mult_left_dist_sup n_mult_idempotent n_mult_left_absorb_sup by auto

lemma n_sup_right_absorb_mult:
  "n(x) * n(y)  n(y) = n(y)"
  using mult_right_dist_sup n_mult_idempotent n_mult_right_absorb_sup by auto

lemma n_mult_commutative:
  "n(x) * n(y) = n(y) * n(x)"
  by (smt sup_commute mult_left_dist_sup mult_right_dist_sup n_sup_left_absorb_mult n_sup_right_absorb_mult n_export n_mult_idempotent)

lemma n_sup_left_dist_mult:
  "n(x)  n(y) * n(z) = (n(x)  n(y)) * (n(x)  n(z))"
  by (metis sup_assoc mult_left_dist_sup mult_right_dist_sup n_sup_right_absorb_mult n_mult_commutative n_mult_left_absorb_sup)

lemma n_sup_right_dist_mult:
  "n(x) * n(y)  n(z) = (n(x)  n(z)) * (n(y)  n(z))"
  by (simp add: sup_commute n_sup_left_dist_mult)

lemma n_order:
  "n(x)  n(y)  n(x) * n(y) = n(x)"
  by (metis le_iff_sup n_sup_right_absorb_mult n_mult_left_absorb_sup)

lemma n_mult_left_lower_bound:
  "n(x) * n(y)  n(x)"
  by (simp add: sup.orderI n_sup_left_absorb_mult)

lemma n_mult_right_lower_bound:
  "n(x) * n(y)  n(y)"
  by (simp add: le_iff_sup n_sup_right_absorb_mult)

lemma n_mult_least_upper_bound:
  "n(x)  n(y)  n(x)  n(z)  n(x)  n(y) * n(z)"
  by (metis order.trans mult_left_isotone n_mult_commutative n_mult_right_lower_bound n_order)

lemma n_mult_left_divisibility:
  "n(x)  n(y)  (z . n(x) = n(y) * n(z))"
  by (metis n_mult_commutative n_mult_left_lower_bound n_order)

lemma n_mult_right_divisibility:
  "n(x)  n(y)  (z . n(x) = n(z) * n(y))"
  by (simp add: n_mult_commutative n_mult_left_divisibility)

text Theorem 15.1

lemma n_one:
  "n(1) = bot"
  by (metis mult_left_one n_mult_bot n_bot)

lemma n_split_equal:
  "x  n(x * L) * top = x * bot  n(x * L) * top"
  using n_split order_trans sup.cobounded1 sup_same_context zero_right_mult_decreasing by blast

lemma n_split_top:
  "x * top  x * bot  n(x * L) * top"
  by (metis mult_left_isotone n_split vector_bot_closed vector_mult_closed vector_sup_closed vector_top_closed)

text Theorem 15.2

lemma n_L:
  "n(L) = 1"
  by (metis sup_bot_left order.antisym mult_left_one n_export n_isotone n_mult_commutative n_split_top n_sub_one n_top)

text Theorem 15.5

lemma n_split_L:
  "x * L = x * bot  n(x * L) * L"
  by (metis mult_1_right n_L n_L_split)

lemma n_n_L:
  "n(n(x) * L) = n(x)"
  by (simp add: n_export n_L)

lemma n_L_decreasing:
  "n(x) * L  x"
  by (metis mult_left_zero n_L_split order_trans sup.orderI zero_right_mult_decreasing mult_assoc n_mult_bot)

text Theorem 15.10

lemma n_galois:
  "n(x)  n(y)  n(x) * L  y"
  by (metis order.trans mult_left_isotone n_L_decreasing n_isotone n_n_L)

text Theorem 15.6

lemma split_L:
  "x * L  x * bot  L"
  by (metis sup_commute sup_left_isotone n_galois n_L n_split_L n_sub_one)

text Theorem 15.7

lemma L_left_zero:
  "L * x = L"
  by (metis order.antisym mult.left_neutral mult_left_zero zero_right_mult_decreasing n_L n_L_decreasing n_mult_bot mult.assoc)

text Theorem 15.8

lemma n_mult:
  "n(x * n(y) * L) = n(x * y)"
  using n_L_split n_dist_sup sup.absorb2 n_mult_left_upper_bound n_mult_bot n_n_L by auto

lemma n_mult_top:
  "n(x * n(y) * top) = n(x * y)"
  by (metis mult_1_right n_mult n_top)

text Theorem 15.4

lemma n_top_L:
  "n(x * top) = n(x * L)"
  by (metis mult_1_right n_L n_mult_top)

lemma n_top_split:
  "x * n(y) * top  x * bot  n(x * y) * top"
  by (metis mult_assoc n_mult n_mult_right_bot n_split_top)

lemma n_mult_right_upper_bound:
  "n(x * y)  n(z)  n(x)  n(z)  x * n(y) * L  x * bot  n(z) * L"
  apply (rule iffI)
  apply (metis sup_right_isotone order.eq_iff mult_isotone n_L_split n_mult_left_upper_bound order_trans)
  by (smt (verit, ccfv_threshold) n_dist_sup n_export sup.absorb_iff2 n_mult n_mult_commutative n_mult_bot n_n_L)

lemma n_preserves_equation:
  "n(y) * x  x * n(y)  n(y) * x = n(y) * x * n(y)"
  using eq_refl test_preserves_equation n_mult_idempotent n_sub_one by auto

definition ni :: "'a  'a"
  where "ni x = n(x) * L"

lemma ni_bot:
  "ni(bot) = bot"
  by (simp add: n_bot ni_def)

lemma ni_one:
  "ni(1) = bot"
  by (simp add: n_one ni_def)

lemma ni_L:
  "ni(L) = L"
  by (simp add: n_L ni_def)

lemma ni_top:
  "ni(top) = L"
  by (simp add: n_top ni_def)

lemma ni_dist_sup:
  "ni(x  y) = ni(x)  ni(y)"
  by (simp add: mult_right_dist_sup n_dist_sup ni_def)

lemma ni_mult_bot:
  "ni(x) = ni(x * bot)"
  using n_mult_bot ni_def by auto

lemma ni_split:
  "x * ni(y) = x * bot  ni(x * y)"
  using n_L_split mult_assoc ni_def by auto

lemma ni_decreasing:
  "ni(x)  x"
  by (simp add: n_L_decreasing ni_def)

lemma ni_isotone:
  "x  y  ni(x)  ni(y)"
  using mult_left_isotone n_isotone ni_def by auto

lemma ni_mult_left_upper_bound:
  "ni(x)  ni(x * y)"
  using mult_left_isotone n_mult_left_upper_bound ni_def by force

lemma ni_idempotent:
  "ni(ni(x)) = ni(x)"
  by (simp add: n_n_L ni_def)

lemma ni_below_L:
  "ni(x)  L"
  using n_L n_galois n_sub_one ni_def by auto

lemma ni_left_zero:
  "ni(x) * y = ni(x)"
  by (simp add: L_left_zero mult_assoc ni_def)

lemma ni_split_L:
  "x * L = x * bot  ni(x * L)"
  using n_split_L ni_def by auto

lemma ni_top_L:
  "ni(x * top) = ni(x * L)"
  by (simp add: n_top_L ni_def)

lemma ni_galois:
  "ni(x)  ni(y)  ni(x)  y"
  by (metis n_galois n_n_L ni_def)

lemma ni_mult:
  "ni(x * ni(y)) = ni(x * y)"
  using mult_assoc n_mult ni_def by auto

lemma ni_n_order:
  "ni(x)  ni(y)  n(x)  n(y)"
  using n_galois ni_def ni_galois by auto

lemma ni_n_equal:
  "ni(x) = ni(y)  n(x) = n(y)"
  by (metis n_n_L ni_def)

lemma ni_mult_right_upper_bound:
  "ni(x * y)  ni(z)  ni(x)  ni(z)  x * ni(y)  x * bot  ni(z)"
  using mult_assoc n_mult_right_upper_bound ni_def ni_n_order by auto

lemma n_ni:
  "n(ni(x)) = n(x)"
  by (simp add: n_n_L ni_def)

lemma ni_n:
  "ni(n(x)) = bot"
  by (metis n_mult_right_bot ni_mult_bot ni_bot)

lemma ni_n_galois:
  "n(x)  n(y)  ni(x)  y"
  by (simp add: n_galois ni_def)

lemma n_mult_ni:
  "n(x * ni(y)) = n(x * y)"
  using ni_mult ni_n_equal by auto

lemma ni_mult_n:
  "ni(x * n(y)) = ni(x)"
  by (simp add: n_mult_n ni_def)

lemma ni_export:
  "ni(n(x) * y) = n(x) * ni(y)"
  by (simp add: n_mult_right_bot ni_split)

lemma ni_mult_top:
  "ni(x * n(y) * top) = ni(x * y)"
  by (simp add: n_mult_top ni_def)

lemma ni_n_bot:
  "ni(x) = bot  n(x) = bot"
  using n_bot ni_n_equal ni_bot by force

lemma ni_n_L:
  "ni(x) = L  n(x) = 1"
  using n_L ni_L ni_n_equal by force

(* independence of axioms, checked in n_semiring without the respective axiom: *)
proposition n_bot         : "n(bot) = bot" (* nitpick [expect=genuine,card=2] *) oops
proposition n_top         : "n(top) = 1" (* nitpick [expect=genuine,card=3] *) oops
proposition n_dist_sup    : "n(x  y) = n(x)  n(y)" (* nitpick [expect=genuine,card=5] *) oops
proposition n_export      : "n(n(x) * y) = n(x) * n(y)" (* nitpick [expect=genuine,card=6] *) oops
proposition n_sub_mult_bot: "n(x) = n(x * bot) * n(x)" (* nitpick [expect=genuine,card=2] *) oops
proposition n_L_split     : "x * n(y) * L = x * bot  n(x * y) * L" (* nitpick [expect=genuine,card=4] *) oops
proposition n_split       : "x  x * bot  n(x * L) * top" (* nitpick [expect=genuine,card=3] *) oops

end

typedef (overloaded) 'a nImage = "{ x::'a::n_semiring . (y::'a . x = n(y)) }"
  by auto

lemma simp_nImage[simp]:
  "y . Rep_nImage x = n(y)"
  using Rep_nImage by simp

setup_lifting type_definition_nImage

text Theorem 15

instantiation nImage :: (n_semiring) bounded_idempotent_semiring
begin

lift_definition sup_nImage :: "'a nImage  'a nImage  'a nImage" is sup
  by (metis n_dist_sup)

lift_definition times_nImage :: "'a nImage  'a nImage  'a nImage" is times
  by (metis n_export)

lift_definition bot_nImage :: "'a nImage" is bot
  by (metis n_bot)

lift_definition one_nImage :: "'a nImage" is 1
  using n_L by auto

lift_definition top_nImage :: "'a nImage" is 1
  using n_L by auto

lift_definition less_eq_nImage :: "'a nImage  'a nImage  bool" is less_eq .

lift_definition less_nImage :: "'a nImage  'a nImage  bool" is less .

instance
  apply intro_classes
  apply (simp add: less_eq_nImage.rep_eq less_le_not_le less_nImage.rep_eq)
  apply (simp add: less_eq_nImage.rep_eq)
  using less_eq_nImage.rep_eq apply force
  apply (simp add: less_eq_nImage.rep_eq Rep_nImage_inject)
  apply (simp add: sup_nImage.rep_eq less_eq_nImage.rep_eq)
  apply (simp add: less_eq_nImage.rep_eq sup_nImage.rep_eq)
  apply (simp add: sup_nImage.rep_eq less_eq_nImage.rep_eq)
  apply (simp add: bot_nImage.rep_eq less_eq_nImage.rep_eq)
  apply (simp add: sup_nImage.rep_eq times_nImage.rep_eq less_eq_nImage.rep_eq mult_left_dist_sup)
  apply (metis (mono_tags, lifting) sup_nImage.rep_eq times_nImage.rep_eq Rep_nImage_inverse mult_right_dist_sup)
  apply (smt (z3) times_nImage.rep_eq Rep_nImage_inverse bot_nImage.rep_eq mult_left_zero)
  using Rep_nImage_inject one_nImage.rep_eq times_nImage.rep_eq apply fastforce
  apply (simp add: one_nImage.rep_eq times_nImage.rep_eq less_eq_nImage.rep_eq)
  apply (smt (verit, del_insts) sup_nImage.rep_eq Rep_nImage Rep_nImage_inject mem_Collect_eq n_sub_one sup.absorb2 top_nImage.rep_eq)
  apply (simp add: less_eq_nImage.rep_eq mult.assoc times_nImage.rep_eq)
  using Rep_nImage_inject mult.assoc times_nImage.rep_eq apply fastforce
  using Rep_nImage_inject one_nImage.rep_eq times_nImage.rep_eq apply fastforce
  apply (metis (mono_tags, lifting) sup_nImage.rep_eq times_nImage.rep_eq Rep_nImage_inject mult_left_dist_sup)
  by (smt (z3) Rep_nImage_inject bot_nImage.rep_eq n_mult_right_bot simp_nImage times_nImage.rep_eq)

end

text Theorem 15

instantiation nImage :: (n_semiring) bounded_distrib_lattice
begin

lift_definition inf_nImage :: "'a nImage  'a nImage  'a nImage" is times
  by (metis n_export)

instance
  apply intro_classes
  apply (metis (mono_tags) inf_nImage.rep_eq less_eq_nImage.rep_eq n_mult_left_lower_bound simp_nImage)
  apply (metis (mono_tags) inf_nImage.rep_eq less_eq_nImage.rep_eq n_mult_right_lower_bound simp_nImage)
  apply (smt (z3) inf_nImage_def le_iff_sup less_eq_nImage.rep_eq mult_right_dist_sup n_mult_left_absorb_sup simp_nImage times_nImage.rep_eq times_nImage_def)
  apply simp
  by (smt (z3) Rep_nImage_inject inf_nImage.rep_eq n_sup_right_dist_mult simp_nImage sup.commute sup_nImage.rep_eq)

end

class n_itering = bounded_itering + n_semiring
begin

lemma mult_L_circ:
  "(x * L) = 1  x * L"
  by (metis L_left_zero circ_mult mult_assoc)

lemma mult_L_circ_mult:
  "(x * L) * y = y  x * L"
  by (metis L_left_zero mult_L_circ mult_assoc mult_left_one mult_right_dist_sup)

lemma circ_L:
  "L = L  1"
  by (metis L_left_zero sup_commute circ_left_unfold)

lemma circ_n_L:
  "x * n(x) * L = x * bot"
  by (metis sup_bot_left circ_left_unfold circ_plus_same mult_left_zero n_L_split n_dist_sup n_mult_bot n_one ni_def ni_split)

lemma n_circ_left_unfold:
  "n(x) = n(x * x)"
  by (metis circ_n_L circ_plus_same n_mult n_mult_bot)

lemma ni_circ:
  "ni(x) = 1  ni(x)"
  by (simp add: mult_L_circ ni_def)

lemma circ_ni:
  "x * ni(x) = x * bot"
  using circ_n_L ni_def mult_assoc by auto

lemma ni_circ_left_unfold:
  "ni(x) = ni(x * x)"
  by (simp add: ni_def n_circ_left_unfold)

lemma n_circ_import:
  "n(y) * x  x * n(y)  n(y) * x = n(y) * (n(y) * x)"
  by (simp add: circ_import n_mult_idempotent n_sub_one)

end

class n_omega_itering = left_omega_conway_semiring + n_itering +
  assumes circ_circ: "x = L  x"
begin

lemma L_below_one_circ:
  "L  1"
  by (metis sup_left_divisibility circ_circ circ_one)

lemma circ_below_L_sup_star:
  "x  L  x"
  by (metis circ_circ circ_increasing)

lemma L_sup_circ_sup_star:
  "L  x = L  x"
  by (metis circ_circ circ_star star_circ)

lemma circ_one_L:
  "1 = L  1"
  using circ_circ circ_one star_one by auto

lemma one_circ_zero:
  "L = 1 * bot"
  by (metis L_left_zero circ_L circ_ni circ_one_L circ_plus_same ni_L)

lemma circ_not_simulate:
  "(x y z . x * z  z * y  x * z  z * y)  1 = bot"
  by (metis L_left_zero circ_one_L order.eq_iff mult_left_one mult_left_zero mult_right_sub_dist_sup_left n_L n_bot bot_least)

lemma star_circ_L:
  "x = L  x"
  by (simp add: circ_circ star_circ)

lemma circ_circ_2:
  "x = L  x"
  by (simp add: L_sup_circ_sup_star circ_circ)

lemma circ_sup_6:
  "L  (x  y) = (x * y)"
  by (metis circ_circ_2 sup_assoc sup_commute circ_sup_1 circ_circ_sup circ_decompose_4)

lemma circ_sup_7:
  "(x * y) = L  (x  y)"
  using L_sup_circ_sup_star circ_sup_6 by auto

end

class n_omega_algebra_2 = bounded_left_zero_omega_algebra + n_semiring + Omega +
  assumes Omega_def: "xΩ = n(xω) * L  x"
begin

lemma mult_L_star:
  "(x * L) = 1  x * L"
  by (simp add: L_left_zero transitive_star mult_assoc)

lemma mult_L_omega:
  "(x * L)ω = x * L"
  by (metis L_left_zero omega_slide)

lemma mult_L_sup_star:
  "(x * L  y) = y  y * x * L"
  by (metis L_left_zero star.mult_zero_sup_circ_2 sup_commute mult_assoc)

lemma mult_L_sup_omega:
  "(x * L  y)ω = yω  y * x * L"
  by (metis L_left_zero mult_bot_add_omega sup_commute mult_assoc)

lemma mult_L_sup_circ:
  "(x * L  y)Ω = n(yω) * L  y  y * x * L"
  by (smt sup_assoc sup_commute Omega_def le_iff_sup mult_L_sup_omega mult_L_sup_star mult_right_dist_sup n_L_decreasing n_dist_sup)

lemma circ_sup_n:
  "(xΩ * y)Ω * xΩ = n((x * y)ω) * L  ((x * y) * x  (x * y) * n(xω) * L)"
  by (smt L_left_zero sup_assoc sup_commute Omega_def mult_L_sup_circ mult_assoc mult_left_dist_sup mult_right_dist_sup)

text Theorem 20.6

lemma n_omega_induct:
  "n(y)  n(x * y  z)  n(y)  n(xω  x * z)"
  by (smt sup_commute mult_assoc n_dist_sup n_galois n_mult omega_induct)

lemma n_Omega_left_unfold:
  "1  x * xΩ = xΩ"
proof -
  have "1  x * xΩ = 1  x * n(xω) * L  x * x"
    by (simp add: Omega_def semiring.distrib_left sup_assoc mult_assoc)
  also have "... = n(x * xω) * L  (1  x * x)"
    by (metis sup_assoc sup_commute sup_bot_left mult_left_dist_sup n_L_split)
  also have "... = n(xω) * L  x"
    using omega_unfold star_left_unfold_equal by auto
  also have "... = xΩ"
    by (simp add: Omega_def)
  finally show ?thesis
    .
qed

lemma n_Omega_circ_sup:
  "(x  y)Ω = (xΩ * y)Ω * xΩ"
proof -
  have "(xΩ * y)Ω * xΩ = n((x * y)ω) * L  ((x * y) * x  (x * y) * n(xω) * L)"
    by (simp add: circ_sup_n)
  also have "... = n((x * y)ω) * L  n((x * y) * xω) * L  (x * y) * bot  (x * y) * x"
    using n_L_split sup.left_commute sup_commute by auto
  also have "... = n((x * y)ω  (x * y) * xω) * L  (x * y) * x"
    by (smt sup_assoc sup_bot_left mult_left_dist_sup mult_right_dist_sup n_dist_sup)
  also have "... = (x  y)Ω"
    by (simp add: Omega_def omega_decompose star.circ_sup_9)
  finally show ?thesis
    ..
qed

lemma n_Omega_circ_simulate_right_sup:
  assumes "z * x  y * yΩ * z  w"
    shows "z * xΩ  yΩ * (z  w * xΩ)"
proof -
  have "z * x  y * yΩ * z  w"
    by (simp add: assms)
  also have "... = y * n(yω) * L  y * y * z  w"
    using L_left_zero Omega_def mult_right_dist_sup semiring.distrib_left mult_assoc by auto
  finally have 1: "z * x  n(yω) * L  y * y * z  w"
    by (metis sup_assoc sup_commute sup_bot_left mult_assoc mult_left_dist_sup n_L_split omega_unfold)
  hence "(n(yω) * L  y * z  y * w * n(xω) * L  y * w * x) * x  n(yω) * L  y * (n(yω) * L  y * y * z  w)  y * w * n(xω) * L  y * w * x"
    by (smt L_left_zero sup_assoc sup_ge1 sup_ge2 le_iff_sup mult_assoc mult_left_dist_sup mult_right_dist_sup star.circ_back_loop_fixpoint)
  also have "... = n(yω) * L  y * n(yω) * L  y * y * y * z  y * w  y * w * n(xω) * L  y * w * x"
    using semiring.distrib_left sup_assoc mult_assoc by auto
  also have "... = n(yω) * L  y * n(yω) * L  y * y * y * z  y * w * n(xω) * L  y * w * x"
    by (smt (verit, ccfv_SIG) le_supI1 order.refl semiring.add_mono star.circ_back_loop_prefixpoint sup.bounded_iff sup.coboundedI1 sup.mono sup_left_divisibility sup_right_divisibility sup_same_context)
  also have "... = n(yω) * L  y * y * y * z  y * w * n(xω) * L  y * w * x"
    by (smt sup_assoc sup_commute sup_idem mult_assoc mult_left_dist_sup n_L_split star_mult_omega)
  also have "...  n(yω) * L  y * z  y * w * n(xω) * L  y * w * x"
    by (meson mult_left_isotone order_refl semiring.add_left_mono star.circ_mult_upper_bound star.right_plus_below_circ sup_left_isotone)
  finally have 2: "z * x  n(yω) * L  y * z  y * w * n(xω) * L  y * w * x"
    by (smt le_supI1 le_sup_iff sup_ge1 star.circ_loop_fixpoint star_right_induct)
  have "z * x * xω  n(yω) * L  y * y * z * xω  w * xω"
    using 1 by (smt (verit, del_insts) L_left_zero mult_assoc mult_left_isotone mult_right_dist_sup)
  hence "n(z * x * xω)  n(y * y * z * xω  n(yω) * L  w * xω)"
    by (simp add: n_isotone sup_commute)
  hence "n(z * xω)  n(yω  y * w * xω)"
    by (smt (verit, del_insts) sup_assoc sup_commute left_plus_omega le_iff_sup mult_assoc mult_left_dist_sup n_L_decreasing n_omega_induct omega_unfold star.left_plus_circ star_mult_omega)
  hence "n(z * xω) * L  n(yω) * L  y * w * n(xω) * L"
    by (metis n_dist_sup n_galois n_mult n_n_L)
  hence "z * n(xω) * L  z * bot  n(yω) * L  y * w * n(xω) * L"
    using n_L_split semiring.add_left_mono sup_assoc by auto
  also have "...  n(yω) * L  y * z  y * w * n(xω) * L"
    by (smt (z3) order.trans mult_1_left mult_right_sub_dist_sup_left semiring.add_right_mono star_left_unfold_equal sup_commute zero_right_mult_decreasing)
  finally have "z * n(xω) * L  n(yω) * L  y * z  y * w * n(xω) * L  y * w * x"
    using le_supI1 by blast
  thus ?thesis
    using 2 by (smt L_left_zero Omega_def sup_assoc le_iff_sup mult_assoc mult_left_dist_sup mult_right_dist_sup)
qed

lemma n_Omega_circ_simulate_left_sup:
  assumes "x * z  z * yΩ  w"
    shows "xΩ * z  (z  xΩ * w) * yΩ"
proof -
  have "x * (z * n(yω) * L  z * y  n(xω) * L  x * w * n(yω) * L  x * w * y) = x * z * n(yω) * L  x * z * y  n(xω) * L  x * x * w * n(yω) * L  x * x * w * y"
    by (smt sup_assoc sup_commute mult_assoc mult_left_dist_sup n_L_split omega_unfold)
  also have "...  (z * n(yω) * L  z * y  w) * n(yω) * L  (z * n(yω) * L  z * y  w) * y  n(xω) * L  x * w * n(yω) * L  x * w * y"
    by (smt assms Omega_def sup_assoc sup_ge2 le_iff_sup mult_assoc mult_left_dist_sup mult_right_dist_sup star.circ_loop_fixpoint)
  also have "... = z * n(yω) * L  z * y * n(yω) * L  w * n(yω) * L  z * y  w * y  n(xω) * L  x * w * n(yω) * L  x * w * y"
    by (smt L_left_zero sup_assoc sup_commute sup_idem mult_assoc mult_right_dist_sup star.circ_transitive_equal)
  also have "... = z * n(yω) * L  w * n(yω) * L  z * y  w * y  n(xω) * L  x * w * n(yω) * L  x * w * y"
    by (smt sup_assoc sup_commute sup_idem le_iff_sup mult_assoc n_L_split star_mult_omega zero_right_mult_decreasing)
  finally have "x * (z * n(yω) * L  z * y  n(xω) * L  x * w * n(yω) * L  x * w * y)  z * n(yω) * L  z * y  n(xω) * L  x * w * n(yω) * L  x * w * y"
    by (smt sup_assoc sup_commute sup_idem mult_assoc star.circ_loop_fixpoint)
  thus "xΩ * z  (z  xΩ * w) * yΩ"
    by (smt (verit, del_insts) L_left_zero Omega_def sup_assoc le_supI1 le_sup_iff sup_ge1 mult_assoc mult_left_dist_sup mult_right_dist_sup star.circ_back_loop_fixpoint star_left_induct)
qed

end

text Theorem 2.6 and Theorem 19

sublocale n_omega_algebra_2 < nL_omega: itering where circ = Omega
  apply unfold_locales
  apply (simp add: n_Omega_circ_sup)
  apply (smt L_left_zero sup_assoc sup_commute sup_bot_left Omega_def mult_assoc mult_left_dist_sup mult_right_dist_sup n_L_split omega_slide star.circ_mult)
  apply (simp add: n_Omega_circ_simulate_right_sup)
  using n_Omega_circ_simulate_left_sup by auto

sublocale n_omega_algebra_2 < nL_omega: n_omega_itering where circ = Omega
  apply unfold_locales
  by (smt Omega_def sup_assoc sup_commute le_iff_sup mult_L_sup_star mult_left_one n_L_split n_top ni_below_L ni_def star_involutive star_mult_omega star_omega_top zero_right_mult_decreasing)

sublocale n_omega_algebra_2 < nL_omega: left_zero_kleene_conway_semiring where circ = Omega ..

sublocale n_omega_algebra_2 < nL_star: left_omega_conway_semiring where circ = star ..

context n_omega_algebra_2
begin

lemma circ_sup_8:
  "n((x * y) * xω) * L  (x * y)Ω * xΩ"
  by (metis sup_ge1 nL_omega.circ_sup_4 Omega_def mult_left_isotone n_isotone omega_sum_unfold_3 order_trans)

lemma n_split_omega_omega:
  "xω  xω * bot  n(xω) * top"
  by (metis n_split n_top_L omega_vector)

text Theorem 20.1

lemma n_below_n_star:
  "n(x)  n(x)"
  by (simp add: n_isotone star.circ_increasing)

text Theorem 20.2

lemma n_star_below_n_omega:
  "n(x)  n(xω)"
  by (metis n_mult_left_upper_bound star_mult_omega)

lemma n_below_n_omega:
  "n(x)  n(xω)"
  using order.trans n_below_n_star n_star_below_n_omega by blast

text Theorem 20.4

lemma star_n_L:
  "x * n(x) * L = x * bot"
  by (metis sup_bot_left mult_left_zero n_L_split n_dist_sup n_mult_bot n_one ni_def ni_split star_left_unfold_equal star_plus)

lemma star_L_split:
  assumes "y  z"
      and "x * z * L  x * bot  z * L"
    shows "x * y * L  x * bot  z * L"
proof -
  have "x * (x * bot  z * L)  x * bot  x * z * L"
    by (metis sup_bot_right order.eq_iff mult_assoc mult_left_dist_sup star.circ_loop_fixpoint)
  also have "...  x * bot  x * bot  z * L"
    using assms(2) semiring.add_left_mono sup_assoc by auto
  also have "... = x * bot  z * L"
    using mult_left_isotone star.circ_increasing sup.absorb_iff2 sup_commute by auto
  finally have "y * L  x * (x * bot  z * L)  x * bot  z * L"
    by (metis assms(1) le_sup_iff sup_ge2 mult_left_isotone order_trans)
  thus ?thesis
    by (simp add: star_left_induct mult_assoc)
qed

lemma star_L_split_same:
  "x * y * L  x * bot  y * L  x * y * L = x * bot  y * L"
  apply (rule order.antisym)
  apply (simp add: star_L_split)
  by (metis bot_least le_supI mult_isotone nL_star.star_below_circ star.circ_loop_fixpoint sup.cobounded2 mult_assoc)

lemma star_n_L_split_equal:
  "n(x * y)  n(y)  x * n(y) * L = x * bot  n(y) * L"
  by (simp add: n_mult_right_upper_bound star_L_split_same)

lemma n_star_mult:
  "n(x * y)  n(y)  n(x * y) = n(x)  n(y)"
  by (metis n_dist_sup n_mult n_mult_bot n_n_L star_n_L_split_equal)

text Theorem 20.3

lemma n_omega_mult:
  "n(xω * y) = n(xω)"
  by (simp add: n_isotone n_mult_left_upper_bound omega_sub_vector order.eq_iff)

lemma n_star_left_unfold:
  "n(x) = n(x * x)"
  by (metis n_mult n_mult_bot star.circ_plus_same star_n_L)

lemma ni_star_below_ni_omega:
  "ni(x)  ni(xω)"
  by (simp add: ni_n_order n_star_below_n_omega)

lemma ni_below_ni_omega:
  "ni(x)  ni(xω)"
  by (simp add: ni_n_order n_below_n_omega)

lemma ni_star:
  "ni(x) = 1  ni(x)"
  by (simp add: mult_L_star ni_def)

lemma ni_omega:
  "ni(x)ω = ni(x)"
  using mult_L_omega ni_def by auto

lemma ni_omega_induct:
  "ni(y)  ni(x * y  z)  ni(y)  ni(xω  x * z)"
  using n_omega_induct ni_n_order by blast

lemma star_ni:
  "x * ni(x) = x * bot"
  using ni_def mult_assoc star_n_L by auto

lemma star_ni_split_equal:
  "ni(x * y)  ni(y)  x * ni(y) = x * bot  ni(y)"
  using ni_def ni_mult_right_upper_bound mult_assoc star_L_split_same by auto

lemma ni_star_mult:
  "ni(x * y)  ni(y)  ni(x * y) = ni(x)  ni(y)"
  using mult_right_dist_sup ni_def ni_n_order n_star_mult by auto

lemma ni_omega_mult:
  "ni(xω * y) = ni(xω)"
  by (simp add: ni_def n_omega_mult)

lemma ni_star_left_unfold:
  "ni(x) = ni(x * x)"
  by (simp add: ni_def n_star_left_unfold)

lemma n_star_import:
  assumes "n(y) * x  x * n(y)"
    shows "n(y) * x = n(y) * (n(y) * x)"
proof (rule order.antisym)
  have "n(y) * (n(y) * x) * x  n(y) * (n(y) * x)"
    by (smt assms mult_assoc mult_right_dist_sup mult_right_sub_dist_sup_left n_mult_idempotent n_preserves_equation star.circ_back_loop_fixpoint)
  thus "n(y) * x  n(y) * (n(y) * x)"
    using assms eq_refl n_mult_idempotent n_sub_one star.circ_import by auto
next
  show "n(y) * (n(y) * x)  n(y) * x"
    by (simp add: assms n_mult_idempotent n_sub_one star.circ_import)
qed

lemma n_omega_export:
  "n(y) * x  x * n(y)  n(y) * xω = (n(y) * x)ω"
  apply (rule order.antisym)
  apply (simp add: n_preserves_equation omega_simulation)
  by (metis mult_right_isotone mult_1_right n_sub_one omega_isotone omega_slide)

lemma n_omega_import:
  "n(y) * x  x * n(y)  n(y) * xω = n(y) * (n(y) * x)ω"
  by (simp add: n_mult_idempotent omega_import)

text Theorem 20.5

lemma star_n_omega_top:
  "x * n(xω) * top = x * bot  n(xω) * top"
  by (smt (verit, del_insts) le_supI le_sup_iff sup_right_divisibility order.antisym mult_assoc nL_star.circ_mult_omega nL_star.star_zero_below_circ_mult n_top_split star.circ_loop_fixpoint)

proposition n_star_induct_sup: "n(z  x * y)  n(y)  n(x * z)  n(y)" oops

end

end