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⇧^∘)"
    by (simp add: circ_left_unfold)
  also have "... = C 1 ⊔ C (x * x⇧^∘)"
    by (simp add: inf_sup_distrib1)
  also have "... ≤ 1 ⊔ C (x * x⇧^∘)"
    using sup_left_isotone by auto
  also have "... = 1 ⊔ C x * x⇧^∘"
    by (simp add: n_L_T_meet_mult)
  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)⇧^∘"
    by (simp add: C_circ_import)
  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⇧^Ω"
  by (simp add: Omega_def)

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"
    by (simp add: tarski)
  also have "... ≤ x * n(x) * L"
    by (simp add: mult_isotone n_L_decreasing)
  finally have "n(x) * L ≤ x⇧^ω"
    by (simp add: omega_induct_mult mult_assoc)
  thus ?thesis
    by (simp add: n_galois)
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
    by (simp add: order.antisym n_isotone)
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)⇧^⋆"
    by (simp add: Omega_def mult_L_sup_omega)
  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)
  apply (simp add: n_mult_omega_L_below_zero)
  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⇧^Ω)⇧^Ω"
    by (simp add: mult_left_isotone n_star_below_Omega)
  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⇧^Ω)⇧^Ω"
    by (simp add: Omega_def mult_isotone)
  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"
    by (simp add: n_n_L_split_n_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"
    by (simp add: n_mult_omega_L_star)
  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
  apply (simp add: n_Omega_left_unfold)
  apply (simp add: n_Omega_left_slide)
  by (simp add: n_Omega_sup_1)

(* 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)⇧^ω"
    by (simp add: C_omega_export)
  also have "... ≤ (x ⊔ n(x) * top)⇧^ω"
    using 1 omega_isotone by blast
  also have "... = (x⇧^⋆ * n(x) * top)⇧^ω ⊔ (x⇧^⋆ * n(x) * top)⇧^⋆ * x⇧^ω"
    by (simp add: omega_decompose mult_assoc)
  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⇧^ω"
    by (simp add: star_left_unfold_equal)
  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⇧^ω"
    by (simp add: omega_decompose)
  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⇧^ω"
    by (simp add: star_left_unfold_equal)
  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"
  by (simp add: mult_apx_right_isotone sup_apx_right_isotone)

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