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

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

lemma n_mult_right_lower_bound:
"n(x) * n(y) ≤ n(y)"

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

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

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"

lemma ni_one:
"ni(1) = bot"

lemma ni_L:
"ni(L) = L"

lemma ni_top:
"ni(top) = L"

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"

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

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

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

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"

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

lemma ni_export:
"ni(n(x) * y) = n(x) * ni(y)"

lemma ni_mult_top:
"ni(x * n(y) * top) = ni(x * y)"

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)
using less_eq_nImage.rep_eq apply force
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)"

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

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

lemma circ_circ_2:
"x⇧∘⇧∘ = L ⊔ x⇧∘"

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⇧Ω"
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)"
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"
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⇧ω)"
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 (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)
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⇧⋆)"

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
qed

lemma star_L_split_same:
"x * y * L ≤ x * bot ⊔ y * L ⟹ x⇧⋆ * y * L = x⇧⋆ * bot ⊔ y * L"
apply (rule order.antisym)
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"

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

lemma ni_below_ni_omega:
"ni(x) ≤ ni(x⇧ω)"

lemma ni_star:
"ni(x)⇧⋆ = 1 ⊔ ni(x)"

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

lemma ni_star_left_unfold:
"ni(x⇧⋆) = ni(x * x⇧⋆)"

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

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

```