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