# Theory Omega_Algebras

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

section ‹Omega Algebras›

theory Omega_Algebras

imports Stone_Kleene_Relation_Algebras.Kleene_Algebras

begin

nitpick_params [timeout = 600]

class omega =
fixes omega :: "'a ⇒ 'a" ("_⇧ω" [100] 100)

class left_omega_algebra = left_kleene_algebra + omega +
assumes omega_unfold: "y⇧ω = y * y⇧ω"
assumes omega_induct: "x ≤ z ⊔ y * x ⟶ x ≤ y⇧ω ⊔ y⇧⋆ * z"
begin

text ‹Many lemmas in this class are taken from Georg Struth's Isabelle theories.›

lemma star_bot_below_omega:
"x⇧⋆ * bot ≤ x⇧ω"
using omega_unfold star_left_induct_equal by auto

lemma star_bot_below_omega_bot:
"x⇧⋆ * bot ≤ x⇧ω * bot"
by (metis omega_unfold star_left_induct_equal sup_monoid.add_0_left mult_assoc)

lemma omega_induct_mult:
"y ≤ x * y ⟹ y ≤ x⇧ω"
by (metis bot_least omega_induct sup.absorb1 sup.absorb2 star_bot_below_omega)

lemma omega_sub_dist:
"x⇧ω ≤ (x ⊔ y)⇧ω"
by (metis eq_refl mult_isotone omega_unfold sup.cobounded1 omega_induct_mult)

lemma omega_isotone:
"x ≤ y ⟹ x⇧ω ≤ y⇧ω"
using sup_left_divisibility omega_sub_dist by fastforce

lemma omega_induct_equal:
"y = z ⊔ x * y ⟹ y ≤ x⇧ω ⊔ x⇧⋆ * z"
by (simp add: omega_induct)

lemma omega_bot:
"bot⇧ω = bot"
by (metis mult_left_zero omega_unfold)

lemma omega_one_greatest:
"x ≤ 1⇧ω"
by (simp add: omega_induct_mult)

lemma star_mult_omega:
"x⇧⋆ * x⇧ω = x⇧ω"
by (metis order.antisym omega_unfold star.circ_loop_fixpoint star_left_induct_mult_equal sup.cobounded2)

lemma omega_sub_vector:
"x⇧ω * y ≤ x⇧ω"
by (metis mult_semi_associative omega_unfold omega_induct_mult)

lemma omega_simulation:
"z * x ≤ y * z ⟹ z * x⇧ω ≤ y⇧ω"
by (smt (verit, ccfv_threshold) mult_isotone omega_unfold order_lesseq_imp mult_assoc omega_induct_mult)

lemma omega_omega:
"x⇧ω⇧ω ≤ x⇧ω"
by (metis omega_unfold omega_sub_vector)

lemma left_plus_omega:
"(x * x⇧⋆)⇧ω = x⇧ω"
by (metis order.antisym mult_assoc omega_induct_mult omega_unfold order_refl star.left_plus_circ star_mult_omega)

lemma omega_slide:
"x * (y * x)⇧ω = (x * y)⇧ω"
by (metis order.antisym mult_assoc mult_right_isotone omega_simulation omega_unfold order_refl)

lemma omega_simulation_2:
"y * x ≤ x * y ⟹ (x * y)⇧ω ≤ x⇧ω"
by (metis mult_right_isotone sup.absorb2 omega_induct_mult omega_slide omega_sub_dist)

lemma wagner:
"(x ⊔ y)⇧ω = x * (x ⊔ y)⇧ω ⊔ z ⟹ (x ⊔ y)⇧ω = x⇧ω ⊔ x⇧⋆ * z"
by (smt (verit, ccfv_SIG) order.refl star_left_induct sup.absorb2 sup_assoc sup_commute omega_induct_equal omega_sub_dist)

lemma right_plus_omega:
"(x⇧⋆ * x)⇧ω = x⇧ω"
by (metis left_plus_omega omega_slide star_mult_omega)

lemma omega_sub_dist_1:
"(x * y⇧⋆)⇧ω ≤ (x ⊔ y)⇧ω"
by (metis left_plus_omega mult_isotone star.circ_sub_dist sup.cobounded1 sup_monoid.add_commute omega_isotone)

lemma omega_sub_dist_2:
"(x⇧⋆ * y)⇧ω ≤ (x ⊔ y)⇧ω"
by (metis mult_isotone star.circ_sub_dist sup.cobounded2 omega_isotone right_plus_omega)

lemma omega_star:
"(x⇧ω)⇧⋆ = 1 ⊔ x⇧ω"
by (metis antisym_conv star.circ_mult_increasing star_left_unfold_equal omega_sub_vector)

lemma omega_mult_omega_star:
"x⇧ω * x⇧ω⇧⋆ = x⇧ω"
by (simp add: order.antisym star.circ_mult_increasing omega_sub_vector)

lemma omega_sum_unfold_1:
"(x ⊔ y)⇧ω = x⇧ω ⊔ x⇧⋆ * y * (x ⊔ y)⇧ω"
by (metis mult_right_dist_sup omega_unfold mult_assoc wagner)

lemma omega_sum_unfold_2:
"(x ⊔ y)⇧ω ≤ (x⇧⋆ * y)⇧ω ⊔ (x⇧⋆ * y)⇧⋆ * x⇧ω"
using omega_induct_equal omega_sum_unfold_1 by auto

lemma omega_sum_unfold_3:
"(x⇧⋆ * y)⇧⋆ * x⇧ω ≤ (x ⊔ y)⇧ω"
using star_left_induct_equal omega_sum_unfold_1 by auto

lemma omega_decompose:
"(x ⊔ y)⇧ω = (x⇧⋆ * y)⇧ω ⊔ (x⇧⋆ * y)⇧⋆ * x⇧ω"
by (metis sup.absorb1 sup_same_context omega_sub_dist_2 omega_sum_unfold_2 omega_sum_unfold_3)

lemma omega_loop_fixpoint:
"y * (y⇧ω ⊔ y⇧⋆ * z) ⊔ z = y⇧ω ⊔ y⇧⋆ * z"
apply (rule order.antisym)
apply (smt (verit, ccfv_threshold) eq_refl mult_isotone mult_left_sub_dist_sup omega_induct omega_unfold star.circ_loop_fixpoint sup_assoc sup_commute sup_right_isotone)
by (smt (z3) mult_left_sub_dist_sup omega_unfold star.circ_loop_fixpoint sup.left_commute sup_commute sup_right_isotone)

lemma omega_loop_greatest_fixpoint:
"y * x ⊔ z = x ⟹ x ≤ y⇧ω ⊔ y⇧⋆ * z"
by (simp add: sup_commute omega_induct_equal)

lemma omega_square:
"x⇧ω = (x * x)⇧ω"
using order.antisym omega_unfold order_refl mult_assoc omega_induct_mult omega_simulation_2 by auto

lemma mult_bot_omega:
"(x * bot)⇧ω = x * bot"
by (metis mult_left_zero omega_slide)

lemma mult_bot_add_omega:
"(x ⊔ y * bot)⇧ω = x⇧ω ⊔ x⇧⋆ * y * bot"
by (metis mult_left_zero sup_commute mult_assoc mult_bot_omega omega_decompose omega_loop_fixpoint)

lemma omega_mult_star:
"x⇧ω * x⇧⋆ = x⇧ω"
by (meson antisym_conv star.circ_back_loop_prefixpoint sup.boundedE omega_sub_vector)

lemma omega_loop_is_greatest_fixpoint:
"is_greatest_fixpoint (λx . y * x ⊔ z) (y⇧ω ⊔ y⇧⋆ * z)"
by (simp add: is_greatest_fixpoint_def omega_loop_fixpoint omega_loop_greatest_fixpoint)

lemma omega_loop_nu:
"ν (λx . y * x ⊔ z) = y⇧ω ⊔ y⇧⋆ * z"
by (metis greatest_fixpoint_same omega_loop_is_greatest_fixpoint)

lemma omega_loop_bot_is_greatest_fixpoint:
"is_greatest_fixpoint (λx . y * x) (y⇧ω)"
using is_greatest_fixpoint_def omega_unfold omega_induct_mult by auto

lemma omega_loop_bot_nu:
"ν (λx . y * x) = y⇧ω"
by (metis greatest_fixpoint_same omega_loop_bot_is_greatest_fixpoint)

lemma affine_has_greatest_fixpoint:
"has_greatest_fixpoint (λx . y * x ⊔ z)"
using has_greatest_fixpoint_def omega_loop_is_greatest_fixpoint by blast

lemma omega_separate_unfold:
"(x⇧⋆ * y)⇧ω = y⇧ω ⊔ y⇧⋆ * x * (x⇧⋆ * y)⇧ω"
by (metis star.circ_loop_fixpoint sup_commute mult_assoc omega_slide omega_sum_unfold_1)

lemma omega_bot_left_slide:
"(x * y)⇧⋆ * ((x * y)⇧ω * bot ⊔ 1) * x ≤ x * (y * x)⇧⋆ * ((y * x)⇧ω * bot ⊔ 1)"
proof -
have "x ⊔ x * (y * x) * (y * x)⇧⋆ * ((y * x)⇧ω * bot ⊔ 1) ≤ x * (y * x)⇧⋆ * ((y * x)⇧ω * bot ⊔ 1)"
by (metis sup_commute mult_assoc mult_right_isotone star.circ_back_loop_prefixpoint star.mult_zero_sup_circ star.mult_zero_circ le_supE le_supI order.refl star.circ_increasing star.circ_mult_upper_bound)
hence "((x * y)⇧ω * bot ⊔ 1) * x ⊔ x * y * (x * (y * x)⇧⋆ * ((y * x)⇧ω * bot ⊔ 1)) ≤ x * (y * x)⇧⋆ * ((y * x)⇧ω * bot ⊔ 1)"
by (smt (z3) sup.absorb_iff2 sup_assoc mult_assoc mult_left_one mult_left_sub_dist_sup_left mult_left_zero mult_right_dist_sup omega_slide star_mult_omega)
thus ?thesis
by (simp add: star_left_induct mult_assoc)
qed

lemma omega_bot_add_1:
"(x ⊔ y)⇧⋆ * ((x ⊔ y)⇧ω * bot ⊔ 1) = x⇧⋆ * (x⇧ω * bot ⊔ 1) * (y * x⇧⋆ * (x⇧ω * bot ⊔ 1))⇧⋆ * ((y * x⇧⋆ * (x⇧ω * bot ⊔ 1))⇧ω * bot ⊔ 1)"
proof (rule order.antisym)
have 1: "(x ⊔ y) * x⇧⋆ * (x⇧ω * bot ⊔ 1) * (y * x⇧⋆ * (x⇧ω * bot ⊔ 1))⇧⋆ * ((y * x⇧⋆ * (x⇧ω * bot ⊔ 1))⇧ω * bot ⊔ 1) ≤ x⇧⋆ * (x⇧ω * bot ⊔ 1) * (y * x⇧⋆ * (x⇧ω * bot ⊔ 1))⇧⋆ * ((y * x⇧⋆ * (x⇧ω * bot ⊔ 1))⇧ω * bot ⊔ 1)"
by (smt (z3) eq_refl star.circ_mult_upper_bound star.circ_sub_dist_1 star.mult_zero_circ star.mult_zero_sup_circ star_sup_1 sup_assoc sup_commute mult_assoc)
have 2: "1 ≤ x⇧⋆ * (x⇧ω * bot ⊔ 1) * (y * x⇧⋆ * (x⇧ω * bot ⊔ 1))⇧⋆ * ((y * x⇧⋆ * (x⇧ω * bot ⊔ 1))⇧ω * bot ⊔ 1)"
using reflexive_mult_closed star.circ_reflexive sup_ge2 by auto
have "(y * x⇧⋆)⇧ω * bot ≤ (y * x⇧⋆ * (x⇧ω * bot ⊔ 1))⇧ω * bot"
by (metis mult_1_right mult_left_isotone mult_left_sub_dist_sup_right omega_isotone)
also have 3: "... ≤ (x⇧ω * bot ⊔ 1) * (y * x⇧⋆ * (x⇧ω * bot ⊔ 1))⇧⋆ * ((y * x⇧⋆ * (x⇧ω * bot ⊔ 1))⇧ω * bot ⊔ 1)"
by (metis mult_isotone mult_left_one star.circ_reflexive sup_commute sup_ge2)
finally have 4: "(x⇧⋆ * y)⇧ω * bot ≤ x⇧⋆ * (x⇧ω * bot ⊔ 1) * (y * x⇧⋆ * (x⇧ω * bot ⊔ 1))⇧⋆ * ((y * x⇧⋆ * (x⇧ω * bot ⊔ 1))⇧ω * bot ⊔ 1)"
by (smt mult_assoc mult_right_isotone omega_slide)
have "y * (x⇧⋆ * y)⇧⋆ * x⇧ω * bot ≤ y * (x⇧⋆ * (x⇧ω * bot ⊔ y))⇧⋆ * x⇧⋆ * x⇧ω * bot * (y * x⇧⋆ * (x⇧ω * bot ⊔ 1))⇧ω * bot"
using mult_isotone mult_left_sub_dist_sup_left mult_left_zero order.refl star_isotone sup_commute mult_assoc star_mult_omega by auto
also have "... ≤ y * (x⇧⋆ * (x⇧ω * bot ⊔ y))⇧⋆ * (x⇧⋆ * (x⇧ω * bot ⊔ 1) * y)⇧ω * bot"
by (smt mult_assoc mult_left_isotone mult_left_sub_dist_sup_left omega_slide)
also have "... = y * (x⇧⋆ * (x⇧ω * bot ⊔ 1) * y)⇧ω * bot"
using mult_left_one mult_left_zero mult_right_dist_sup mult_assoc star_mult_omega by auto
finally have "x⇧⋆ * y * (x⇧⋆ * y)⇧⋆ * x⇧ω * bot ≤ x⇧⋆ * (x⇧ω * bot ⊔ 1) * (y * x⇧⋆ * (x⇧ω * bot ⊔ 1))⇧⋆ * ((y * x⇧⋆ * (x⇧ω * bot ⊔ 1))⇧ω * bot ⊔ 1)"
using 3 by (smt mult_assoc mult_right_isotone omega_slide order_trans)
hence "(x⇧⋆ * y)⇧⋆ * x⇧ω * bot ≤ x⇧⋆ * (x⇧ω * bot ⊔ 1) * (y * x⇧⋆ * (x⇧ω * bot ⊔ 1))⇧⋆ * ((y * x⇧⋆ * (x⇧ω * bot ⊔ 1))⇧ω * bot ⊔ 1)"
by (smt (verit, ccfv_threshold) sup_assoc sup_commute le_iff_sup mult_assoc mult_isotone mult_left_one mult_1_right mult_right_sub_dist_sup_left order_trans star.circ_loop_fixpoint star.circ_reflexive star.mult_zero_circ)
hence "(x ⊔ y)⇧ω * bot ≤ x⇧⋆ * (x⇧ω * bot ⊔ 1) * (y * x⇧⋆ * (x⇧ω * bot ⊔ 1))⇧⋆ * ((y * x⇧⋆ * (x⇧ω * bot ⊔ 1))⇧ω * bot ⊔ 1)"
using 4 by (smt (z3) mult_right_dist_sup sup.orderE sup_assoc sup_right_divisibility omega_decompose)
thus "(x ⊔ y)⇧⋆ * ((x ⊔ y)⇧ω * bot ⊔ 1) ≤ x⇧⋆ * (x⇧ω * bot ⊔ 1) * (y * x⇧⋆ * (x⇧ω * bot ⊔ 1))⇧⋆ * ((y * x⇧⋆ * (x⇧ω * bot ⊔ 1))⇧ω * bot ⊔ 1)"
using 1 2 star_left_induct mult_assoc by force
next
have 5: "x⇧ω * bot ≤ (x ⊔ y)⇧⋆ * ((x ⊔ y)⇧ω * bot ⊔ 1)"
by (metis bot_least le_supI1 le_supI2 mult_isotone star.circ_loop_fixpoint sup.cobounded1 omega_isotone)
have 6: "(y * x⇧⋆)⇧ω * bot ≤ (x ⊔ y)⇧⋆ * ((x ⊔ y)⇧ω * bot ⊔ 1)"
by (metis sup_commute mult_left_isotone omega_sub_dist_1 mult_assoc mult_left_sub_dist_sup_left order_trans star_mult_omega)
have 7: "(y * x⇧⋆)⇧⋆ ≤ (x ⊔ y)⇧⋆"
by (metis mult_left_one mult_right_sub_dist_sup_left star.circ_sup_1 star.circ_plus_one)
hence "(y * x⇧⋆)⇧⋆ * x⇧ω * bot ≤ (x ⊔ y)⇧⋆ * ((x ⊔ y)⇧ω * bot ⊔ 1)"
by (smt sup_assoc le_iff_sup mult_assoc mult_isotone mult_right_dist_sup omega_sub_dist)
hence "(x⇧ω * bot ⊔ y * x⇧⋆)⇧ω * bot ≤ (x ⊔ y)⇧⋆ * ((x ⊔ y)⇧ω * bot ⊔ 1)"
using 6 by (smt sup_commute sup.bounded_iff mult_assoc mult_right_dist_sup mult_bot_add_omega omega_unfold omega_bot)
hence "(y * x⇧⋆ * (x⇧ω * bot ⊔ 1))⇧ω * bot ≤ y * x⇧⋆ * (x ⊔ y)⇧⋆ * ((x ⊔ y)⇧ω * bot ⊔ 1)"
by (smt mult_assoc mult_left_one mult_left_zero mult_right_dist_sup mult_right_isotone omega_slide)
also have "... ≤ (x ⊔ y)⇧⋆ * ((x ⊔ y)⇧ω * bot ⊔ 1)"
using 7 by (metis mult_left_isotone order_refl star.circ_mult_upper_bound star_left_induct_mult_iff)
finally have "(y * x⇧⋆ * (x⇧ω * bot ⊔ 1))⇧⋆ * ((y * x⇧⋆ * (x⇧ω * bot ⊔ 1))⇧ω * bot ⊔ 1) ≤ (x ⊔ y)⇧⋆ * ((x ⊔ y)⇧ω * bot ⊔ 1)"
using 5 by (smt (z3) le_supE star.circ_mult_upper_bound star.circ_sub_dist_1 star.mult_zero_circ star.mult_zero_sup_circ star_involutive star_isotone sup_commute)
hence "(x⇧ω * bot ⊔ 1) * (y * x⇧⋆ * (x⇧ω * bot ⊔ 1))⇧⋆ * ((y * x⇧⋆ * (x⇧ω * bot ⊔ 1))⇧ω * bot ⊔ 1) ≤ (x ⊔ y)⇧⋆ * ((x ⊔ y)⇧ω * bot ⊔ 1)"
using 5 by (metis sup_commute mult_assoc star.circ_isotone star.circ_mult_upper_bound star.mult_zero_sup_circ star.mult_zero_circ star_involutive)
thus "x⇧⋆ * (x⇧ω * bot ⊔ 1) * (y * x⇧⋆ * (x⇧ω * bot ⊔ 1))⇧⋆ * ((y * x⇧⋆ * (x⇧ω * bot ⊔ 1))⇧ω * bot ⊔ 1) ≤ (x ⊔ y)⇧⋆ * ((x ⊔ y)⇧ω * bot ⊔ 1)"
by (smt sup_assoc sup_commute mult_assoc star.circ_mult_upper_bound star.circ_sub_dist star.mult_zero_sup_circ star.mult_zero_circ)
qed

lemma star_omega_greatest:
"x⇧⋆⇧ω = 1⇧ω"
by (metis sup_commute le_iff_sup omega_one_greatest omega_sub_dist star.circ_plus_one)

lemma omega_vector_greatest:
"x⇧ω * 1⇧ω = x⇧ω"
by (metis order.antisym mult_isotone omega_mult_omega_star omega_one_greatest omega_sub_vector)

lemma mult_greatest_omega:
"(x * 1⇧ω)⇧ω ≤ x * 1⇧ω"
by (metis mult_right_isotone omega_slide omega_sub_vector)

lemma omega_mult_star_2:
"x⇧ω * y⇧⋆ = x⇧ω"
by (meson order.antisym le_supE star.circ_back_loop_prefixpoint omega_sub_vector)

lemma omega_import:
assumes "p ≤ p * p"
and "p * x ≤ x * p"
shows "p * x⇧ω = p * (p * x)⇧ω"
proof -
have "p * x⇧ω ≤ p * (p * x) * x⇧ω"
by (metis assms(1) mult_assoc mult_left_isotone omega_unfold)
also have "... ≤ p * x * p * x⇧ω"
by (metis assms(2) mult_assoc mult_left_isotone mult_right_isotone)
finally have "p * x⇧ω ≤ (p * x)⇧ω"
by (simp add: mult_assoc omega_induct_mult)
hence "p * x⇧ω ≤ p * (p * x)⇧ω"
by (metis assms(1) mult_assoc mult_left_isotone mult_right_isotone order_trans)
thus "p * x⇧ω = p * (p * x)⇧ω"
by (metis assms(2) sup_left_divisibility order.antisym mult_right_isotone omega_induct_mult omega_slide omega_sub_dist)
qed

proposition omega_circ_simulate_right_plus: "z * x ≤ y * (y⇧ω * bot ⊔ y⇧⋆) * z ⊔ w ⟶ z * (x⇧ω * bot ⊔ x⇧⋆) ≤ (y⇧ω * bot ⊔ y⇧⋆) * (z ⊔ w * (x⇧ω * bot ⊔ x⇧⋆))" nitpick [expect=genuine,card=4] oops
proposition omega_circ_simulate_left_plus: "x * z ≤ z * (y⇧ω * bot ⊔ y⇧⋆) ⊔ w ⟶ (x⇧ω * bot ⊔ x⇧⋆) * z ≤ (z ⊔ (x⇧ω * bot ⊔ x⇧⋆) * w) * (y⇧ω * bot ⊔ y⇧⋆)" nitpick [expect=genuine,card=5] oops

end

text ‹Theorem 50.2›

sublocale left_omega_algebra < comb0: left_conway_semiring where circ = "(λx . x⇧⋆ * (x⇧ω * bot ⊔ 1))"
apply unfold_locales
apply (smt sup_assoc sup_commute le_iff_sup mult_assoc mult_left_sub_dist_sup_left omega_unfold star.circ_loop_fixpoint star_mult_omega)
using omega_bot_left_slide mult_assoc apply fastforce
using omega_bot_add_1 mult_assoc by simp

class left_zero_omega_algebra = left_zero_kleene_algebra + left_omega_algebra
begin

lemma star_omega_absorb:
"y⇧⋆ * (y⇧⋆ * x)⇧⋆ * y⇧ω = (y⇧⋆ * x)⇧⋆ * y⇧ω"
proof -
have "y⇧⋆ * (y⇧⋆ * x)⇧⋆ * y⇧ω = y⇧⋆ * y⇧⋆ * x * (y⇧⋆ * x)⇧⋆ * y⇧ω ⊔ y⇧⋆ * y⇧ω"
by (metis sup_commute mult_assoc mult_right_dist_sup star.circ_back_loop_fixpoint star.circ_plus_same)
thus ?thesis
by (metis mult_assoc star.circ_loop_fixpoint star.circ_transitive_equal star_mult_omega)
qed

lemma omega_circ_simulate_right_plus:
assumes "z * x ≤ y * (y⇧ω * bot ⊔ y⇧⋆) * z ⊔ w"
shows "z * (x⇧ω * bot ⊔ x⇧⋆) ≤ (y⇧ω * bot ⊔ y⇧⋆) * (z ⊔ w * (x⇧ω * bot ⊔ x⇧⋆))"
proof -
have 1: "z * x ≤ y⇧ω * bot ⊔ y * y⇧⋆ * z ⊔ w"
by (metis assms mult_assoc mult_left_dist_sup mult_left_zero mult_right_dist_sup omega_unfold)
hence "(y⇧ω * bot ⊔ y⇧⋆ * z ⊔ y⇧⋆ * w * x⇧ω * bot ⊔ y⇧⋆ * w * x⇧⋆) * x ≤ y⇧ω * bot ⊔ y⇧⋆ * (y⇧ω * bot ⊔ y * y⇧⋆ * z ⊔ w) ⊔ y⇧⋆ * w * x⇧ω * bot ⊔ y⇧⋆ * w * x⇧⋆"
by (smt sup_assoc sup_ge1 sup_ge2 le_iff_sup mult_assoc mult_left_dist_sup mult_left_zero mult_right_dist_sup star.circ_back_loop_fixpoint)
also have "... = y⇧ω * bot ⊔ y⇧⋆ * y * y⇧⋆ * z ⊔ y⇧⋆ * w * x⇧ω * bot ⊔ y⇧⋆ * w * x⇧⋆"
by (smt sup_assoc sup_ge2 le_iff_sup mult_assoc mult_left_dist_sup star.circ_back_loop_fixpoint star_mult_omega)
also have "... ≤ y⇧ω * bot ⊔ y⇧⋆ * z ⊔ y⇧⋆ * w * x⇧ω * bot ⊔ y⇧⋆ * w * x⇧⋆"
by (smt sup_commute sup_left_isotone mult_left_isotone star.circ_increasing star.circ_plus_same star.circ_transitive_equal)
finally have "z ⊔ (y⇧ω * bot ⊔ y⇧⋆ * z ⊔ y⇧⋆ * w * x⇧ω * bot ⊔ y⇧⋆ * w * x⇧⋆) * x ≤ y⇧ω * bot ⊔ y⇧⋆ * z ⊔ y⇧⋆ * w * x⇧ω * bot ⊔ y⇧⋆ * w * x⇧⋆"
by (metis (no_types, lifting) le_supE le_supI star.circ_loop_fixpoint sup.cobounded1)
hence 2: "z * x⇧⋆ ≤ y⇧ω * bot ⊔ y⇧⋆ * z ⊔ y⇧⋆ * w * x⇧ω * bot ⊔ y⇧⋆ * w * x⇧⋆"
by (simp add: star_right_induct)
have "z * x⇧ω * bot ≤ (y⇧ω * bot ⊔ y * y⇧⋆ * z ⊔ w) * x⇧ω * bot"
using 1 by (smt sup_left_divisibility mult_assoc mult_right_sub_dist_sup_left omega_unfold)
hence "z * x⇧ω * bot ≤ y⇧ω ⊔ y⇧⋆ * (y⇧ω * bot ⊔ w * x⇧ω * bot)"
by (smt sup_assoc sup_commute left_plus_omega mult_assoc mult_left_zero mult_right_dist_sup omega_induct star.left_plus_circ)
thus "z * (x⇧ω * bot ⊔ x⇧⋆) ≤ (y⇧ω * bot ⊔ y⇧⋆) * (z ⊔ w * (x⇧ω * bot ⊔ x⇧⋆))"
using 2 by (smt sup_assoc sup_commute le_iff_sup mult_assoc mult_left_dist_sup mult_left_zero mult_right_dist_sup omega_unfold omega_bot star_mult_omega zero_right_mult_decreasing)
qed

lemma omega_circ_simulate_left_plus:
assumes "x * z ≤ z * (y⇧ω * bot ⊔ y⇧⋆) ⊔ w"
shows "(x⇧ω * bot ⊔ x⇧⋆) * z ≤ (z ⊔ (x⇧ω * bot ⊔ x⇧⋆) * w) * (y⇧ω * bot ⊔ y⇧⋆)"
proof -
have "x * (z * y⇧ω * bot ⊔ z * y⇧⋆ ⊔ x⇧ω * bot ⊔ x⇧⋆ * w * y⇧ω * bot ⊔ x⇧⋆ * w * y⇧⋆) = x * z * y⇧ω * bot ⊔ x * z * y⇧⋆ ⊔ x⇧ω * bot ⊔ x * x⇧⋆ * w * y⇧ω * bot ⊔ x * x⇧⋆ * w * y⇧⋆"
by (smt mult_assoc mult_left_dist_sup omega_unfold)
also have "... ≤ x * z * y⇧ω * bot ⊔ x * z * y⇧⋆ ⊔ x⇧ω * bot ⊔ x⇧⋆ * w * y⇧ω * bot ⊔ x⇧⋆ * w * y⇧⋆"
by (metis sup_mono sup_right_isotone mult_left_isotone star.left_plus_below_circ)
also have "... ≤ (z * y⇧ω * bot ⊔ z * y⇧⋆ ⊔ w) * y⇧ω * bot ⊔ (z * y⇧ω * bot ⊔ z * y⇧⋆ ⊔ w) * y⇧⋆ ⊔ x⇧ω * bot ⊔ x⇧⋆ * w * y⇧ω * bot ⊔ x⇧⋆ * w * y⇧⋆"
by (metis assms sup_left_isotone mult_assoc mult_left_dist_sup mult_left_isotone)
also have "... = z * y⇧ω * bot ⊔ z * y⇧⋆ * y⇧ω * bot ⊔ w * y⇧ω * bot ⊔ z * y⇧ω * bot ⊔ z * y⇧⋆ * y⇧⋆ ⊔ w * y⇧⋆ ⊔ x⇧ω * bot ⊔ x⇧⋆ * w * y⇧ω * bot ⊔ x⇧⋆ * w * y⇧⋆"
by (smt sup_assoc mult_assoc mult_left_zero mult_right_dist_sup)
also have "... = z * y⇧ω * bot ⊔ z * y⇧⋆ ⊔ x⇧ω * bot ⊔ x⇧⋆ * w * y⇧ω * bot ⊔ x⇧⋆ * w * y⇧⋆"
by (smt (verit, ccfv_threshold) sup_assoc sup_commute sup_idem mult_assoc mult_right_dist_sup star.circ_loop_fixpoint star.circ_transitive_equal star_mult_omega)
finally have "x⇧⋆ * z ≤ z * y⇧ω * bot ⊔ z * y⇧⋆ ⊔ x⇧ω * bot ⊔ x⇧⋆ * w * y⇧ω * bot ⊔ x⇧⋆ * w * y⇧⋆"
by (smt (z3) le_supE sup_least sup_ge1 star.circ_back_loop_fixpoint star_left_induct)
hence "(x⇧ω * bot ⊔ x⇧⋆) * z ≤ z * y⇧ω * bot ⊔ z * y⇧⋆ ⊔ x⇧ω * bot ⊔ x⇧⋆ * w * y⇧ω * bot ⊔ x⇧⋆ * w * y⇧⋆"
by (smt (z3) sup.left_commute sup_commute sup_least sup_ge1 mult_assoc mult_left_zero mult_right_dist_sup)
thus "(x⇧ω * bot ⊔ x⇧⋆) * z ≤ (z ⊔ (x⇧ω * bot ⊔ x⇧⋆) * w) * (y⇧ω * bot ⊔ y⇧⋆)"
by (smt sup_assoc mult_assoc mult_left_dist_sup mult_left_zero mult_right_dist_sup)
qed

lemma omega_translate:
"x⇧⋆ * (x⇧ω * bot ⊔ 1) = x⇧ω * bot ⊔ x⇧⋆"
by (metis mult_assoc mult_left_dist_sup mult_1_right star_mult_omega)

lemma omega_circ_simulate_right:
assumes "z * x ≤ y * z ⊔ w"
shows "z * (x⇧ω * bot ⊔ x⇧⋆) ≤ (y⇧ω * bot ⊔ y⇧⋆) * (z ⊔ w * (x⇧ω * bot ⊔ x⇧⋆))"
proof -
have "... ≤ y * (y⇧ω * bot ⊔ y⇧⋆) * z ⊔ w"
using comb0.circ_mult_increasing mult_isotone sup_left_isotone omega_translate by auto
thus "z * (x⇧ω * bot ⊔ x⇧⋆) ≤ (y⇧ω * bot ⊔ y⇧⋆) * (z ⊔ w * (x⇧ω * bot ⊔ x⇧⋆))"
using assms order_trans omega_circ_simulate_right_plus by blast
qed

end

sublocale left_zero_omega_algebra < comb1: left_conway_semiring_1 where circ = "(λx . x⇧⋆ * (x⇧ω * bot ⊔ 1))"
apply unfold_locales
by (smt order.eq_iff mult_assoc mult_left_dist_sup mult_left_zero mult_right_dist_sup mult_1_right omega_slide star_slide)

sublocale left_zero_omega_algebra < comb0: itering where circ = "(λx . x⇧⋆ * (x⇧ω * bot ⊔ 1))"
apply unfold_locales
using comb1.circ_sup_9 apply blast
using comb1.circ_mult_1 apply blast
apply (metis omega_circ_simulate_right_plus omega_translate)
using omega_circ_simulate_left_plus omega_translate by auto

text ‹Theorem 2.2›

sublocale left_zero_omega_algebra < comb2: itering where circ = "(λx . x⇧ω * bot ⊔ x⇧⋆)"
apply unfold_locales
using comb1.circ_sup_9 omega_translate apply force
apply (metis comb1.circ_mult_1 omega_translate)
using omega_circ_simulate_right_plus apply blast
by (simp add: omega_circ_simulate_left_plus)

class omega_algebra = kleene_algebra + left_zero_omega_algebra

class left_omega_conway_semiring = left_omega_algebra + left_conway_semiring
begin

subclass left_kleene_conway_semiring ..

lemma circ_below_omega_star:
"x⇧∘ ≤ x⇧ω ⊔ x⇧⋆"
by (metis circ_left_unfold mult_1_right omega_induct order_refl)

lemma omega_mult_circ:
"x⇧ω * x⇧∘ = x⇧ω"
by (metis circ_star omega_mult_star_2)

lemma circ_mult_omega:
"x⇧∘ * x⇧ω = x⇧ω"
by (metis order.antisym sup_right_divisibility circ_loop_fixpoint circ_plus_sub omega_simulation)

lemma circ_omega_greatest:
"x⇧∘⇧ω = 1⇧ω"
by (metis circ_star star_omega_greatest)

lemma omega_circ:
"x⇧ω⇧∘ = 1 ⊔ x⇧ω"
by (metis order.antisym circ_left_unfold mult_left_sub_dist_sup_left mult_1_right omega_sub_vector)

end

class bounded_left_omega_algebra = bounded_left_kleene_algebra + left_omega_algebra
begin

lemma omega_one:
"1⇧ω = top"
by (simp add: order.antisym omega_one_greatest)

lemma star_omega_top:
"x⇧⋆⇧ω = top"
by (simp add: star_omega_greatest omega_one)

lemma omega_vector:
"x⇧ω * top = x⇧ω"
by (simp add: order.antisym omega_sub_vector top_right_mult_increasing)

lemma mult_top_omega:
"(x * top)⇧ω ≤ x * top"
using mult_greatest_omega omega_one by auto

end

sublocale bounded_left_omega_algebra < comb0: bounded_left_conway_semiring where circ = "(λx . x⇧⋆ * (x⇧ω * bot ⊔ 1))" ..

class bounded_left_zero_omega_algebra = bounded_left_zero_kleene_algebra + left_zero_omega_algebra
begin

subclass bounded_left_omega_algebra ..

end

sublocale bounded_left_zero_omega_algebra < comb0: bounded_itering where circ = "(λx . x⇧⋆ * (x⇧ω * bot ⊔ 1))" ..

class bounded_omega_algebra = bounded_kleene_algebra + omega_algebra
begin

subclass bounded_left_zero_omega_algebra ..

end

class bounded_left_omega_conway_semiring = bounded_left_omega_algebra + left_omega_conway_semiring
begin

subclass left_kleene_conway_semiring ..

subclass bounded_left_conway_semiring ..

lemma circ_omega:
"x⇧∘⇧ω = top"
by (simp add: circ_omega_greatest omega_one)

end

class top_left_omega_algebra = bounded_left_omega_algebra +
assumes top_left_bot: "top * x = top"
begin

lemma omega_translate_3:
"x⇧⋆ * (x⇧ω * bot ⊔ 1) = x⇧⋆ * (x⇧ω ⊔ 1)"
by (metis omega_one omega_vector_greatest top_left_bot mult_assoc)

end

text ‹Theorem 50.2›

sublocale top_left_omega_algebra < comb4: left_conway_semiring where circ = "(λx . x⇧⋆ * (x⇧ω ⊔ 1))"
apply unfold_locales
using comb0.circ_left_unfold omega_translate_3 apply force
using omega_bot_left_slide omega_translate_3 mult_assoc apply force
using comb0.circ_sup_1 omega_translate_3 by auto

class top_left_bot_omega_algebra = bounded_left_zero_omega_algebra +
assumes top_left_bot: "top * x = top"
begin

lemma omega_translate_2:
"x⇧ω * bot ⊔ x⇧⋆ = x⇧ω ⊔ x⇧⋆"
by (metis mult_assoc omega_mult_star_2 star.circ_top top_left_bot)

end

text ‹Theorem 2.3›

sublocale top_left_bot_omega_algebra < comb3: itering where circ = "(λx . x⇧ω ⊔ x⇧⋆)"
apply unfold_locales
using comb2.circ_slide_1 comb2.circ_sup_1 omega_translate_2 apply force
apply (metis comb2.circ_mult_1 omega_translate_2)
using omega_circ_simulate_right_plus omega_translate_2 apply force
using omega_circ_simulate_left_plus omega_translate_2 by auto

class Omega =
fixes Omega :: "'a ⇒ 'a" ("_⇧Ω" [100] 100)

end

```