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