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