# Theory N_Omega_Algebras

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

section ‹N-Omega-Algebras›

theory N_Omega_Algebras

imports Omega_Algebras Recursion

begin

class itering_apx = bounded_itering + n_algebra_apx
begin

lemma circ_L:
"L⇧∘ = L ⊔ 1"
by (metis sup_commute mult_top_circ n_L_top_L)

lemma C_circ_import:
"C (x⇧∘) ≤ (C x)⇧∘"
proof -
have 1: "C x * x⇧∘ ≤ (C x)⇧∘ * C x"
using C_mult_propagate circ_simulate order.eq_iff by blast
have "C (x⇧∘) = C (1 ⊔ x * x⇧∘)"
also have "... = C 1 ⊔ C (x * x⇧∘)"
also have "... ≤ 1 ⊔ C (x * x⇧∘)"
using sup_left_isotone by auto
also have "... = 1 ⊔ C x * x⇧∘"
also have "... ≤ (C x)⇧∘"
using 1 by (meson circ_reflexive order.trans le_supI right_plus_below_circ)
finally show ?thesis
.
qed

text ‹AACP Theorem 4.3 and Theorem 4.4›

lemma circ_apx_isotone:
assumes "x ⊑ y"
shows "x⇧∘ ⊑ y⇧∘"
proof -
have 1: "x ≤ y ⊔ L ∧ C y ≤ x ⊔ n(x) * top"
using assms apx_def by auto
have "C (y⇧∘) ≤ (C y)⇧∘"
also have "... ≤ x⇧∘ ⊔ x⇧∘ * n(x) * top"
using 1 by (metis circ_isotone circ_left_top circ_unfold_sum mult_assoc)
also have "... ≤ x⇧∘ ⊔ (x⇧∘ * bot ⊔ n(x⇧∘ * x) * top)"
using n_n_top_split_n_top sup_right_isotone by blast
also have "... ≤ x⇧∘ ⊔ (x⇧∘ * bot ⊔ n(x⇧∘) * top)"
using circ_plus_same left_plus_below_circ mult_left_isotone n_isotone sup_right_isotone by auto
also have "... = x⇧∘ ⊔ n(x⇧∘) * top"
by (meson sup.left_idem sup_relative_same_increasing zero_right_mult_decreasing)
finally have 2: "C (y⇧∘) ≤ x⇧∘ ⊔ n(x⇧∘) * top"
.
have "x⇧∘ ≤ y⇧∘ * L⇧∘"
using 1 by (metis circ_sup_1 circ_back_loop_fixpoint circ_isotone n_L_below_L le_iff_sup mult_assoc)
also have "... = y⇧∘ ⊔ y⇧∘ * L"
using circ_L mult_left_dist_sup sup_commute by auto
also have "... ≤ y⇧∘ ⊔ y⇧∘ * bot ⊔ L"
using n_L_split_L semiring.add_left_mono sup_assoc by auto
finally have "x⇧∘ ≤ y⇧∘ ⊔ L"
using sup.absorb1 zero_right_mult_decreasing by force
thus "x⇧∘ ⊑ y⇧∘"
using 2 by (simp add: apx_def)
qed

end

class n_omega_algebra_1 = bounded_left_zero_omega_algebra + n_algebra_apx + Omega +
assumes Omega_def: "x⇧Ω = n(x⇧ω) * L ⊔ x⇧⋆"
begin

text ‹AACP Theorem 8.13›

lemma C_omega_export:
"C (x⇧ω) = (C x)⇧ω"
proof -
have "C (x⇧ω) = C x * C (x⇧ω)"
by (metis C_mult_propagate n_L_T_meet_mult omega_unfold)
hence 1: "C (x⇧ω) ≤ (C x)⇧ω"
using eq_refl omega_induct_mult by auto
have "(C x)⇧ω = C (x * (C x)⇧ω)"
using n_L_T_meet_mult omega_unfold by auto
also have "... ≤ C (x⇧ω)"
by (metis calculation C_decreasing inf_le1 le_infI omega_induct_mult)
finally show ?thesis
using 1 order.antisym by blast
qed

text ‹AACP Theorem 8.2›

lemma L_mult_star:
"L * x⇧⋆ = L"
by (metis n_L_top_L star.circ_left_top mult_assoc)

text ‹AACP Theorem 8.3›

lemma mult_L_star:
"(x * L)⇧⋆ = 1 ⊔ x * L"
by (metis L_mult_star star.circ_mult_1 mult_assoc)

lemma mult_L_omega_below:
"(x * L)⇧ω ≤ x * L"
by (metis mult_right_isotone n_L_below_L omega_slide)

text ‹AACP Theorem 8.5›

lemma mult_L_sup_star:
"(x * L ⊔ y)⇧⋆ = y⇧⋆ ⊔ y⇧⋆ * x * L"
using L_mult_star mult_1_right mult_left_dist_sup star_sup_1 sup_commute mult_L_star mult_assoc by auto

lemma mult_L_sup_omega_below:
"(x * L ⊔ y)⇧ω ≤ y⇧ω ⊔ y⇧⋆ * x * L"
proof -
have "(x * L ⊔ y)⇧ω ≤ y⇧⋆ * x * L ⊔ (y⇧⋆ * x * L)⇧⋆ * y⇧ω"
by (metis sup_commute mult_assoc omega_decompose sup_left_isotone mult_L_omega_below)
also have "... ≤ y⇧ω ⊔ y⇧⋆ * x * L"
by (smt (z3) le_iff_sup le_supI mult_left_dist_sup n_L_below_L star_left_induct sup.cobounded2 sup.left_idem sup.orderE sup_assoc sup_commute mult_assoc)
finally show ?thesis
.
qed

lemma n_Omega_isotone:
"x ≤ y ⟹ x⇧Ω ≤ y⇧Ω"
by (metis Omega_def sup_mono mult_left_isotone n_isotone omega_isotone star_isotone)

lemma n_star_below_Omega:
"x⇧⋆ ≤ x⇧Ω"

lemma mult_L_star_mult_below:
"(x * L)⇧⋆ * y ≤ y ⊔ x * L"
by (metis sup_right_isotone mult_assoc mult_right_isotone n_L_below_L star_left_induct)

end

sublocale n_omega_algebra_1 < star: itering_apx where circ = star ..

class n_omega_algebra = n_omega_algebra_1 + n_algebra_apx +
assumes n_split_omega_mult: "C (x⇧ω) ≤ x⇧⋆ * n(x⇧ω) * top"
assumes tarski: "x * L ≤ x * L * x * L"
begin

text ‹AACP Theorem 8.4›

lemma mult_L_omega:
"(x * L)⇧ω = x * L"
apply (rule order.antisym)
apply (rule mult_L_omega_below)
using omega_induct_mult tarski mult_assoc by auto

text ‹AACP Theorem 8.6›

lemma mult_L_sup_omega:
"(x * L ⊔ y)⇧ω = y⇧ω ⊔ y⇧⋆ * x * L"
apply (rule order.antisym)
apply (rule mult_L_sup_omega_below)
by (metis le_supI omega_isotone omega_sub_dist_2 sup.cobounded2 sup_commute mult_L_omega mult_assoc)

text ‹AACP Theorem 8.1›

lemma tarski_mult_top_idempotent:
"x * L = x * L * x * L"
by (metis omega_unfold mult_L_omega mult_assoc)

text ‹AACP Theorem 8.7›

lemma n_below_n_omega:
"n(x) ≤ n(x⇧ω)"
proof -
have "n(x) * L ≤ n(x) * L * n(x) * L"
also have "... ≤ x * n(x) * L"
finally have "n(x) * L ≤ x⇧ω"
thus ?thesis
qed

text ‹AACP Theorem 8.14›

lemma n_split_omega_sup_zero:
"C (x⇧ω) ≤ x⇧⋆ * bot ⊔ n(x⇧ω) * top"
proof -
have "n(x⇧ω) * top ⊔ x * (x⇧⋆ * bot ⊔ n(x⇧ω) * top) = n(x⇧ω) * top ⊔ x * x⇧⋆ * bot ⊔ x * n(x⇧ω) * top"
by (simp add: mult_left_dist_sup sup_assoc mult_assoc)
also have "... ≤ n(x⇧ω) * top ⊔ x * x⇧⋆ * bot ⊔ x * bot ⊔ n(x⇧ω) * top"
by (metis sup_assoc sup_right_isotone n_n_top_split_n_top omega_unfold)
also have "... = x * x⇧⋆ * bot ⊔ n(x⇧ω) * top"
by (smt sup_assoc sup_commute sup_left_top sup_bot_right mult_assoc mult_left_dist_sup)
also have "... ≤ x⇧⋆ * bot ⊔ n(x⇧ω) * top"
by (metis sup_left_isotone mult_left_isotone star.left_plus_below_circ)
finally have "x⇧⋆ * n(x⇧ω) * top ≤ x⇧⋆ * bot ⊔ n(x⇧ω) * top"
using star_left_induct mult_assoc by auto
thus ?thesis
using n_split_omega_mult order_trans by blast
qed

lemma n_split_omega_sup:
"C (x⇧ω) ≤ x⇧⋆ ⊔ n(x⇧ω) * top"
by (metis sup_left_isotone n_split_omega_sup_zero order_trans zero_right_mult_decreasing)

text ‹AACP Theorem 8.12›

lemma n_dist_omega_star:
"n(y⇧ω ⊔ y⇧⋆ * z) = n(y⇧ω) ⊔ n(y⇧⋆ * z)"
proof -
have "n(y⇧ω ⊔ y⇧⋆ * z) = n(C (y⇧ω) ⊔ C (y⇧⋆ * z))"
by (metis inf_sup_distrib1 n_C)
also have "... ≤ n(C (y⇧ω) ⊔ y⇧⋆ * z)"
using n_isotone semiring.add_right_mono sup_commute by auto
also have "... ≤ n(y⇧⋆ * bot ⊔ n(y⇧ω) * top ⊔ y⇧⋆ * z)"
using n_isotone semiring.add_right_mono n_split_omega_sup_zero by blast
also have "... = n(y⇧ω) ⊔ n(y⇧⋆ * z)"
by (smt sup_assoc sup_commute sup_bot_right mult_left_dist_sup n_dist_n_add)
finally show ?thesis
qed

lemma mult_L_sup_circ_below:
"(x * L ⊔ y)⇧Ω ≤ n(y⇧ω) * L ⊔ y⇧⋆ ⊔ y⇧⋆ * x * L"
proof -
have "(x * L ⊔ y)⇧Ω ≤ n(y⇧ω ⊔ y⇧⋆ * x * L) * L ⊔ (x * L ⊔ y)⇧⋆"
also have "... = n(y⇧ω) * L ⊔ n(y⇧⋆ * x * L) * L ⊔ (x * L ⊔ y)⇧⋆"
by (simp add: semiring.distrib_right mult_assoc n_dist_omega_star)
also have "... ≤ n(y⇧ω) * L ⊔ y⇧⋆ ⊔ y⇧⋆ * x * L"
by (smt (z3) le_supI sup.cobounded1 sup_assoc sup_commute sup_idem sup_right_isotone mult_L_sup_star n_L_decreasing)
finally show ?thesis
.
qed

lemma n_mult_omega_L_below_zero:
"n(y * x⇧ω) * L ≤ y * x⇧⋆ * bot ⊔ y * n(x⇧ω) * L"
proof -
have "n(y * x⇧ω) * L ≤ C (y * x⇧ω) ⊓ L"
by (metis n_C n_L_decreasing_meet_L)
also have "... ≤ y * C (x⇧ω) ⊓ L"
using inf.sup_left_isotone n_L_T_meet_mult n_L_T_meet_mult_propagate by auto
also have "... ≤ y * (x⇧⋆ * bot ⊔ n(x⇧ω) * top) ⊓ L"
using inf.sup_left_isotone mult_right_isotone n_split_omega_sup_zero by auto
also have "... = (y * x⇧⋆ * bot ⊓ L) ⊔ (y * n(x⇧ω) * top ⊓ L)"
using inf_sup_distrib2 mult_left_dist_sup mult_assoc by auto
also have "... ≤ (y * x⇧⋆ * bot ⊓ L) ⊔ y * n(x⇧ω) * L"
using n_vector_meet_L sup_right_isotone by auto
also have "... ≤ y * x⇧⋆ * bot ⊔ y * n(x⇧ω) * L"
using sup_left_isotone by auto
finally show ?thesis
.
qed

text ‹AACP Theorem 8.10›

lemma n_mult_omega_L_star_zero:
"y * x⇧⋆ * bot ⊔ n(y * x⇧ω) * L = y * x⇧⋆ * bot ⊔ y * n(x⇧ω) * L"
apply (rule order.antisym)
by (smt sup_assoc sup_commute sup_bot_left sup_right_isotone mult_assoc mult_left_dist_sup n_n_L_split_n_L)

text ‹AACP Theorem 8.11›

lemma n_mult_omega_L_star:
"y * x⇧⋆ ⊔ n(y * x⇧ω) * L = y * x⇧⋆ ⊔ y * n(x⇧ω) * L"
by (metis zero_right_mult_decreasing n_mult_omega_L_star_zero sup_relative_same_increasing)

lemma n_mult_omega_L_below:
"n(y * x⇧ω) * L ≤ y * x⇧⋆ ⊔ y * n(x⇧ω) * L"
using sup_right_divisibility n_mult_omega_L_star by blast

lemma n_omega_L_below_zero:
"n(x⇧ω) * L ≤ x * x⇧⋆ * bot ⊔ x * n(x⇧ω) * L"
by (metis omega_unfold n_mult_omega_L_below_zero)

lemma n_omega_L_below:
"n(x⇧ω) * L ≤ x⇧⋆ ⊔ x * n(x⇧ω) * L"
by (metis omega_unfold n_mult_omega_L_below sup_left_isotone star.left_plus_below_circ order_trans)

lemma n_omega_L_star_zero:
"x * x⇧⋆ * bot ⊔ n(x⇧ω) * L = x * x⇧⋆ * bot ⊔ x * n(x⇧ω) * L"
by (metis n_mult_omega_L_star_zero omega_unfold)

text ‹AACP Theorem 8.8›

lemma n_omega_L_star:
"x⇧⋆ ⊔ n(x⇧ω) * L = x⇧⋆ ⊔ x * n(x⇧ω) * L"
by (metis star.circ_mult_upper_bound star.left_plus_below_circ bot_least n_omega_L_star_zero sup_relative_same_increasing)

text ‹AACP Theorem 8.9›

lemma n_omega_L_star_zero_star:
"x⇧⋆ * bot ⊔ n(x⇧ω) * L = x⇧⋆ * bot ⊔ x⇧⋆ * n(x⇧ω) * L"
by (metis n_mult_omega_L_star_zero star_mult_omega mult_assoc star.circ_transitive_equal)

text ‹AACP Theorem 8.8›

lemma n_omega_L_star_star:
"x⇧⋆ ⊔ n(x⇧ω) * L = x⇧⋆ ⊔ x⇧⋆ * n(x⇧ω) * L"
by (metis zero_right_mult_decreasing n_omega_L_star_zero_star sup_relative_same_increasing)

lemma n_Omega_left_unfold:
"1 ⊔ x * x⇧Ω = x⇧Ω"
by (smt Omega_def sup_assoc sup_commute mult_assoc mult_left_dist_sup n_omega_L_star star.circ_left_unfold)

lemma n_Omega_left_slide:
"(x * y)⇧Ω * x ≤ x * (y * x)⇧Ω"
proof -
have "(x * y)⇧Ω * x ≤ x * y * n((x * y)⇧ω) * L ⊔ (x * y)⇧⋆ * x"
by (smt Omega_def sup_commute sup_left_isotone mult_assoc mult_right_dist_sup mult_right_isotone n_L_below_L n_omega_L_star)
also have "... ≤ x * (y * bot ⊔ n(y * (x * y)⇧ω) * L) ⊔ (x * y)⇧⋆ * x"
by (metis mult_right_isotone n_n_L_split_n_L sup_commute sup_right_isotone mult_assoc)
also have "... = x * (y * x)⇧Ω"
by (smt (verit, del_insts) le_supI1 star_slide Omega_def sup_assoc sup_commute le_iff_sup mult_assoc mult_isotone mult_left_dist_sup omega_slide star.circ_increasing star.circ_slide bot_least)
finally show ?thesis
.
qed

lemma n_Omega_sup_1:
"(x ⊔ y)⇧Ω = x⇧Ω * (y * x⇧Ω)⇧Ω"
proof -
have 1: "(x ⊔ y)⇧Ω = n((x⇧⋆ * y)⇧ω) * L ⊔ n((x⇧⋆ * y)⇧⋆ * x⇧ω) * L ⊔ (x⇧⋆ * y)⇧⋆ * x⇧⋆"
by (simp add: Omega_def omega_decompose semiring.distrib_right star.circ_sup_9 n_dist_omega_star)
have "n((x⇧⋆ * y)⇧ω) * L ≤ (x⇧⋆ * y)⇧⋆ ⊔ x⇧⋆ * (y * n((x⇧⋆ * y)⇧ω) * L)"
by (metis n_omega_L_below mult_assoc)
also have "... ≤ (x⇧⋆ * y)⇧⋆ ⊔ x⇧⋆ * y * bot ⊔ x⇧⋆ * n((y * x⇧⋆)⇧ω) * L"
by (smt sup_assoc sup_right_isotone mult_assoc mult_left_dist_sup mult_right_isotone n_n_L_split_n_L omega_slide)
also have "... = (x⇧⋆ * y)⇧⋆ ⊔ x⇧⋆ * n((y * x⇧⋆)⇧ω) * L"
by (metis sup_commute le_iff_sup star.circ_sub_dist_1 zero_right_mult_decreasing)
also have "... ≤ x⇧⋆ * (y * x⇧⋆)⇧⋆ ⊔ x⇧⋆ * n((y * x⇧⋆)⇧ω) * L"
by (metis star_outer_increasing star_slide star_star_absorb sup_left_isotone)
also have "... ≤ x⇧⋆ * (y * x⇧Ω)⇧Ω"
by (metis Omega_def sup_commute mult_assoc mult_left_dist_sup mult_right_isotone n_Omega_isotone n_star_below_Omega)
also have "... ≤ x⇧Ω * (y * x⇧Ω)⇧Ω"
finally have 2: "n((x⇧⋆ * y)⇧ω) * L ≤ x⇧Ω * (y * x⇧Ω)⇧Ω"
.
have "n((x⇧⋆ * y)⇧⋆ * x⇧ω) * L ≤ n(x⇧ω) * L ⊔ x⇧⋆ * (y * x⇧⋆)⇧⋆ ⊔ x⇧⋆ * (y * x⇧⋆)⇧⋆ * y * n(x⇧ω) * L"
by (smt sup_assoc sup_commute mult_left_one mult_right_dist_sup n_mult_omega_L_below star.circ_mult star.circ_slide)
also have "... = n(x⇧ω) * L * (y * x⇧Ω)⇧⋆ ⊔ x⇧⋆ * (y * x⇧Ω)⇧⋆"
by (smt Omega_def sup_assoc mult_L_sup_star mult_assoc mult_left_dist_sup L_mult_star)
also have "... ≤ x⇧Ω * (y * x⇧Ω)⇧Ω"
finally have 3: "n((x⇧⋆ * y)⇧⋆ * x⇧ω) * L ≤ x⇧Ω * (y * x⇧Ω)⇧Ω"
.
have "(x⇧⋆ * y)⇧⋆ * x⇧⋆ ≤ x⇧Ω * (y * x⇧Ω)⇧Ω"
by (metis star_slide mult_isotone mult_right_isotone n_star_below_Omega order_trans star_isotone)
hence 4: "(x ⊔ y)⇧Ω ≤ x⇧Ω * (y * x⇧Ω)⇧Ω"
using 1 2 3 by simp
have 5: "x⇧Ω * (y * x⇧Ω)⇧Ω ≤ n(x⇧ω) * L ⊔ x⇧⋆ * n((y * x⇧Ω)⇧ω) * L ⊔ x⇧⋆ * (y * x⇧Ω)⇧⋆"
by (smt Omega_def sup_assoc sup_left_isotone mult_assoc mult_left_dist_sup mult_right_dist_sup mult_right_isotone n_L_below_L)
have "n(x⇧ω) * L ≤ n((x⇧⋆ * y)⇧⋆ * x⇧ω) * L"
by (metis sup_commute sup_ge1 mult_left_isotone n_isotone star.circ_loop_fixpoint)
hence 6: "n(x⇧ω) * L ≤ (x ⊔ y)⇧Ω"
using 1 order_lesseq_imp by fastforce
have "x⇧⋆ * n((y * x⇧Ω)⇧ω) * L ≤ x⇧⋆ * n((y * x⇧⋆)⇧ω ⊔ (y * x⇧⋆)⇧⋆ * y * n(x⇧ω) * L) * L"
by (metis Omega_def mult_L_sup_omega_below mult_assoc mult_left_dist_sup mult_left_isotone mult_right_isotone n_isotone)
also have "... ≤ x⇧⋆ * bot ⊔ n(x⇧⋆ * ((y * x⇧⋆)⇧ω ⊔ (y * x⇧⋆)⇧⋆ * y * n(x⇧ω) * L)) * L"
also have "... ≤ x⇧⋆ ⊔ n((x⇧⋆ * y)⇧ω ⊔ x⇧⋆ * (y * x⇧⋆)⇧⋆ * y * n(x⇧ω) * L) * L"
using omega_slide semiring.distrib_left sup_mono zero_right_mult_decreasing mult_assoc by fastforce
also have "... ≤ x⇧⋆ ⊔ n((x⇧⋆ * y)⇧ω ⊔ (x⇧⋆ * y)⇧⋆ * n(x⇧ω) * L) * L"
by (smt sup_right_divisibility sup_right_isotone mult_left_isotone n_isotone star.circ_mult)
also have "... ≤ x⇧⋆ ⊔ n((x ⊔ y)⇧ω) * L"
by (metis sup_right_isotone mult_assoc mult_left_isotone mult_right_isotone n_L_decreasing n_isotone omega_decompose)
also have "... ≤ (x ⊔ y)⇧Ω"
by (simp add: Omega_def le_supI1 star_isotone sup_commute)
finally have 7: "x⇧⋆ * n((y * x⇧Ω)⇧ω) * L ≤ (x ⊔ y)⇧Ω"
.
have "x⇧⋆ * (y * x⇧Ω)⇧⋆ ≤ (x⇧⋆ * y)⇧⋆ * x⇧⋆ ⊔ (x⇧⋆ * y)⇧⋆ * n(x⇧ω) * L"
by (smt Omega_def sup_right_isotone mult_L_sup_star mult_assoc mult_left_dist_sup mult_left_isotone star.left_plus_below_circ star_slide)
also have "... ≤ (x⇧⋆ * y)⇧⋆ * x⇧⋆ ⊔ n((x⇧⋆ * y)⇧⋆ * x⇧ω) * L"
also have "... ≤ (x ⊔ y)⇧Ω"
by (smt Omega_def sup_commute sup_right_isotone mult_left_isotone n_right_upper_bound omega_decompose star.circ_sup)
finally have "n(x⇧ω) * L ⊔ x⇧⋆ * n((y * x⇧Ω)⇧ω) * L ⊔ x⇧⋆ * (y * x⇧Ω)⇧⋆ ≤ (x ⊔ y)⇧Ω"
using 6 7 by simp
hence "x⇧Ω * (y * x⇧Ω)⇧Ω ≤ (x ⊔ y)⇧Ω"
using 5 order.trans by blast
thus ?thesis
using 4 order.antisym by blast
qed

end

sublocale n_omega_algebra < nL_omega: left_zero_conway_semiring where circ = Omega
apply unfold_locales

(* circ_plus_same does not hold in the non-strict model using Omega *)

context n_omega_algebra
begin

text ‹AACP Theorem 8.16›

lemma omega_apx_isotone:
assumes "x ⊑ y"
shows "x⇧ω ⊑ y⇧ω"
proof -
have 1: "x ≤ y ⊔ L ∧ C y ≤ x ⊔ n(x) * top"
using assms apx_def by auto
have "n(x) * top ⊔ x * (x⇧ω ⊔ n(x⇧ω) * top) ≤ n(x) * top ⊔ x⇧ω ⊔ n(x⇧ω) * top"
by (metis le_supI n_split_top sup.cobounded1 sup_assoc mult_assoc mult_left_dist_sup sup_right_isotone omega_unfold)
also have "... ≤ x⇧ω ⊔ n(x⇧ω) * top"
by (metis sup_commute sup_right_isotone mult_left_isotone n_below_n_omega sup_assoc sup_idem)
finally have 2: "x⇧⋆ * n(x) * top ≤ x⇧ω ⊔ n(x⇧ω) * top"
using star_left_induct mult_assoc by auto
have "C (y⇧ω) = (C y)⇧ω"
also have "... ≤ (x ⊔ n(x) * top)⇧ω"
using 1 omega_isotone by blast
also have "... = (x⇧⋆ * n(x) * top)⇧ω ⊔ (x⇧⋆ * n(x) * top)⇧⋆ * x⇧ω"
also have "... ≤ x⇧⋆ * n(x) * top ⊔ (x⇧⋆ * n(x) * top)⇧⋆ * x⇧ω"
using mult_top_omega sup_left_isotone by blast
also have "... = x⇧⋆ * n(x) * top ⊔ (1 ⊔ x⇧⋆ * n(x) * top * (x⇧⋆ * n(x) * top)⇧⋆) * x⇧ω"
also have "... ≤ x⇧ω ⊔ x⇧⋆ * n(x) * top"
by (smt sup_mono sup_least mult_assoc mult_left_one mult_right_dist_sup mult_right_isotone order_refl top_greatest sup.cobounded2)
also have "... ≤ x⇧ω ⊔ n(x⇧ω) * top"
using 2 by simp
finally have 3: "C (y⇧ω) ≤ x⇧ω ⊔ n(x⇧ω) * top"
.
have "x⇧ω ≤ (y ⊔ L)⇧ω"
using 1 omega_isotone by simp
also have "... = (y⇧⋆ * L)⇧ω ⊔ (y⇧⋆ * L)⇧⋆ * y⇧ω"
also have "... = y⇧⋆ * L * (y⇧⋆ * L)⇧ω ⊔ (y⇧⋆ * L)⇧⋆ * y⇧ω"
using omega_unfold by auto
also have "... ≤ y⇧⋆ * L ⊔ (y⇧⋆ * L)⇧⋆ * y⇧ω"
by (metis sup_left_isotone n_L_below_L mult_assoc mult_right_isotone)
also have "... = y⇧⋆ * L ⊔ (1 ⊔ y⇧⋆ * L * (y⇧⋆ * L)⇧⋆) * y⇧ω"
also have "... ≤ y⇧⋆ * L ⊔ y⇧ω"
by (simp add: mult_L_star_mult_below star_left_unfold_equal sup_commute)
also have "... ≤ y⇧⋆ * bot ⊔ L ⊔ y⇧ω"
using n_L_split_L sup_left_isotone by auto
finally have "x⇧ω ≤ y⇧ω ⊔ L"
by (simp add: star_bot_below_omega sup.absorb1 sup.left_commute sup_commute)
thus "x⇧ω ⊑ y⇧ω"
using 3 by (simp add: apx_def)
qed

lemma combined_apx_left_isotone:
"x ⊑ y ⟹ n(x⇧ω) * L ⊔ x⇧⋆ * z ⊑ n(y⇧ω) * L ⊔ y⇧⋆ * z"
by (simp add: mult_apx_isotone n_L_apx_isotone star.circ_apx_isotone sup_apx_isotone omega_apx_isotone)

lemma combined_apx_left_isotone_2:
"x ⊑ y ⟹ (x⇧ω ⊓ L) ⊔ x⇧⋆ * z ⊑ (y⇧ω ⊓ L) ⊔ y⇧⋆ * z"
by (metis sup_apx_isotone mult_apx_left_isotone omega_apx_isotone star.circ_apx_isotone meet_L_apx_isotone)

lemma combined_apx_right_isotone:
"y ⊑ z ⟹ n(x⇧ω) * L ⊔ x⇧⋆ * y ⊑ n(x⇧ω) * L ⊔ x⇧⋆ * z"
by (simp add: mult_apx_isotone sup_apx_left_isotone sup_commute)

lemma combined_apx_right_isotone_2:
"y ⊑ z ⟹ (x⇧ω ⊓ L) ⊔ x⇧⋆ * y ⊑ (x⇧ω ⊓ L) ⊔ x⇧⋆ * z"

lemma combined_apx_isotone:
"x ⊑ y ⟹ w ⊑ z ⟹ n(x⇧ω) * L ⊔ x⇧⋆ * w ⊑ n(y⇧ω) * L ⊔ y⇧⋆ * z"
by (simp add: mult_apx_isotone n_L_apx_isotone star.circ_apx_isotone sup_apx_isotone omega_apx_isotone)

lemma combined_apx_isotone_2:
"x ⊑ y ⟹ w ⊑ z ⟹ (x⇧ω ⊓ L) ⊔ x⇧⋆ * w ⊑ (y⇧ω ⊓ L) ⊔ y⇧⋆ * z"
by (meson combined_apx_left_isotone_2 combined_apx_right_isotone_2 apx.order.trans)

lemma n_split_nu_mu:
"C (y⇧ω ⊔ y⇧⋆ * z) ≤ y⇧⋆ * z ⊔ n(y⇧ω ⊔ y⇧⋆ * z) * top"
proof -
have "C (y⇧ω ⊔ y⇧⋆ * z) ≤ C (y⇧ω) ⊔ y⇧⋆ * z"
by (simp add: inf_sup_distrib1 le_supI1 sup_commute)
also have "... ≤ y⇧⋆ * bot ⊔ n(y⇧ω) * top ⊔ y⇧⋆ * z"
using n_split_omega_sup_zero sup_left_isotone by blast
also have "... ≤ y⇧⋆ * z ⊔ n(y⇧ω ⊔ y⇧⋆ * z) * top"
using le_supI1 mult_left_isotone mult_right_isotone n_left_upper_bound sup_right_isotone by force
finally show ?thesis
.
qed

lemma n_split_nu_mu_2:
"C (y⇧ω ⊔ y⇧⋆ * z) ≤ y⇧⋆ * z ⊔ ((y⇧ω ⊔ y⇧⋆ * z) ⊓ L) ⊔ n(y⇧ω ⊔ y⇧⋆ * z) * top"
proof -
have "C (y⇧ω ⊔ y⇧⋆ * z) ≤ C (y⇧ω) ⊔ y⇧⋆ * z"
using inf.sup_left_isotone sup_inf_distrib2 by auto
also have "... ≤ y⇧⋆ * bot ⊔ n(y⇧ω) * top ⊔ y⇧⋆ * z"
using n_split_omega_sup_zero sup_left_isotone by blast
also have "... ≤ y⇧⋆ * z ⊔ n(y⇧ω ⊔ y⇧⋆ * z) * top"
using le_supI1 mult_left_isotone mult_right_isotone n_left_upper_bound semiring.add_left_mono by auto
finally show ?thesis
using order_lesseq_imp semiring.add_right_mono sup.cobounded1 by blast
qed

lemma loop_exists:
"C (ν (λx . y * x ⊔ z)) ≤ μ (λx . y * x ⊔ z) ⊔ n(ν (λx . y * x ⊔ z)) * top"
using omega_loop_nu star_loop_mu n_split_nu_mu by auto

lemma loop_exists_2:
"C (ν (λx . y * x ⊔ z)) ≤ μ (λx . y * x ⊔ z) ⊔ (ν (λx . y * x ⊔ z) ⊓ L) ⊔ n(ν (λx . y * x ⊔ z)) * top"
by (simp add: omega_loop_nu star_loop_mu n_split_nu_mu_2)

lemma loop_apx_least_fixpoint:
"apx.is_least_fixpoint (λx . y * x ⊔ z) (μ (λx . y * x ⊔ z) ⊔ n(ν (λx . y * x ⊔ z)) * L)"
proof -
have "kappa_mu_nu_L (λx . y * x ⊔ z)"
by (metis affine_apx_isotone loop_exists affine_has_greatest_fixpoint affine_has_least_fixpoint affine_isotone nu_below_mu_nu_L_def nu_below_mu_nu_L_kappa_mu_nu_L)
thus ?thesis
using apx.least_fixpoint_char kappa_mu_nu_L_def by force
qed

lemma loop_apx_least_fixpoint_2:
"apx.is_least_fixpoint (λx . y * x ⊔ z) (μ (λx . y * x ⊔ z) ⊔ (ν (λx . y * x ⊔ z) ⊓ L))"
proof -
have "kappa_mu_nu (λx . y * x ⊔ z)"
by (metis affine_apx_isotone affine_has_greatest_fixpoint affine_has_least_fixpoint affine_isotone loop_exists_2 nu_below_mu_nu_def nu_below_mu_nu_kappa_mu_nu)
thus ?thesis
using apx.least_fixpoint_char kappa_mu_nu_def by force
qed

lemma loop_has_apx_least_fixpoint:
"apx.has_least_fixpoint (λx . y * x ⊔ z)"
using apx.least_fixpoint_char loop_apx_least_fixpoint by blast

lemma loop_semantics:
"κ (λx . y * x ⊔ z) = μ (λx . y * x ⊔ z) ⊔ n(ν (λx . y * x ⊔ z)) * L"
using apx.least_fixpoint_char loop_apx_least_fixpoint by force

lemma loop_semantics_2:
"κ (λx . y * x ⊔ z) = μ (λx . y * x ⊔ z) ⊔ (ν (λx . y * x ⊔ z) ⊓ L)"
using apx.least_fixpoint_char loop_apx_least_fixpoint_2 by force

text ‹AACP Theorem 8.15›

lemma loop_semantics_kappa_mu_nu:
"κ (λx . y * x ⊔ z) = n(y⇧ω) * L ⊔ y⇧⋆ * z"
proof -
have "κ (λx . y * x ⊔ z) = y⇧⋆ * z ⊔ n(y⇧ω ⊔ y⇧⋆ * z) * L"
using apx.least_fixpoint_char omega_loop_nu star_loop_mu loop_apx_least_fixpoint by auto
thus ?thesis
by (smt n_dist_omega_star sup_assoc mult_right_dist_sup sup_commute le_iff_sup n_L_decreasing)
qed

text ‹AACP Theorem 8.15›

lemma loop_semantics_kappa_mu_nu_2:
"κ (λx . y * x ⊔ z) = (y⇧ω ⊓ L) ⊔ y⇧⋆ * z"
proof -
have "κ (λx . y * x ⊔ z) = y⇧⋆ * z ⊔ ((y⇧ω ⊔ y⇧⋆ * z) ⊓ L)"
using apx.least_fixpoint_char omega_loop_nu star_loop_mu loop_apx_least_fixpoint_2 by auto
thus ?thesis
by (metis sup_absorb2 sup_ge2 sup_inf_distrib1 sup_monoid.add_commute)
qed

text ‹AACP Theorem 8.16›

lemma loop_semantics_apx_left_isotone:
"w ⊑ y ⟹ κ (λx . w * x ⊔ z) ⊑ κ (λx . y * x ⊔ z)"
by (metis loop_semantics_kappa_mu_nu_2 combined_apx_left_isotone_2)

text ‹AACP Theorem 8.16›

lemma loop_semantics_apx_right_isotone:
"w ⊑ z ⟹ κ (λx . y * x ⊔ w) ⊑ κ (λx . y * x ⊔ z)"
by (metis loop_semantics_kappa_mu_nu_2 combined_apx_right_isotone_2)

lemma loop_semantics_apx_isotone:
"v ⊑ y ⟹ w ⊑ z ⟹ κ (λx . v * x ⊔ w) ⊑ κ (λx . y * x ⊔ z)"
using apx_transitive_2 loop_semantics_apx_left_isotone loop_semantics_apx_right_isotone by blast

end

end

```