Theory Recursion_Strict

(* Title:      Strict Recursion
   Author:     Walter Guttmann
   Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

section ‹Strict Recursion›

theory Recursion_Strict

imports N_Semirings Approximation

begin

class semiring_apx = n_semiring + apx +
  assumes apx_def: "x ⊑ y ⟷ x ≤ y ⊔ n(x) * L ∧ y ≤ x ⊔ n(x) * top"
begin

lemma apx_n_order_reverse:
  "y ⊑ x ⟹ n(x) ≤ n(y)"
  by (metis apx_def le_iff_sup n_sup_left_absorb_mult n_dist_sup n_export)

lemma apx_n_order:
  "x ⊑ y ⟹ y ⊑ x ⟹ n(x) = n(y)"
  by (simp add: apx_n_order_reverse order.antisym)

lemma apx_transitive:
  assumes "x ⊑ y"
      and "y ⊑ z"
    shows "x ⊑ z"
proof -
  have "n(y) * L ≤ n(x) * L"
    by (simp add: apx_n_order_reverse assms(1) mult_left_isotone)
  hence 1: "x ≤ z ⊔ n(x) * L"
    by (smt assms sup_assoc sup_right_divisibility apx_def le_iff_sup)
  have "z ≤ x ⊔ n(x) * top ⊔ n(x ⊔ n(x) * top) * top"
    by (smt (verit) assms sup_left_isotone order_refl sup_assoc sup_mono apx_def mult_left_isotone n_isotone order_trans)
  also have "... = x ⊔ n(x) * top"
    by (simp add: n_dist_sup n_export n_sup_left_absorb_mult)
  finally show ?thesis
    using 1 by (simp add: apx_def)
qed

text ‹Theorem 16.1›

subclass apx_biorder
  apply unfold_locales
  apply (simp add: apx_def)
  apply (smt (verit) order.antisym le_sup_iff apx_def eq_refl le_iff_sup n_galois apx_n_order)
  using apx_transitive by blast

lemma sup_apx_left_isotone:
  assumes "x ⊑ y"
    shows "x ⊔ z ⊑ y ⊔ z"
proof -
  have "x ≤ y ⊔ n(x) * L ∧ y ≤ x ⊔ n(x) * top"
    using assms apx_def by auto
  hence "z ⊔ x ≤ z ⊔ y ⊔ n(z ⊔ x) * L ∧ z ⊔ y ≤ z ⊔ x ⊔ n(z ⊔ x) * top"
    by (metis sup_assoc sup_right_isotone mult_right_sub_dist_sup_right n_dist_sup order_trans)
  thus ?thesis
    by (simp add: apx_def sup_commute)
qed

lemma mult_apx_left_isotone:
  assumes "x ⊑ y"
    shows "x * z ⊑ y * z"
proof -
  have "x ≤ y ⊔ n(x) * L"
    using assms apx_def by auto
  hence "x * z ≤ y * z ⊔ n(x) * L"
    by (smt (verit, ccfv_threshold) L_left_zero mult_left_isotone semiring.distrib_right mult_assoc)
  hence 1: "x * z ≤ y * z ⊔ n(x * z) * L"
    by (meson mult_left_isotone n_mult_left_upper_bound order_lesseq_imp sup_mono)
  have "y * z ≤ x * z ⊔ n(x) * top * z"
    by (metis assms apx_def mult_left_isotone mult_right_dist_sup)
  hence "y * z ≤ x * z ⊔ n(x * z) * top"
    using mult_isotone n_mult_left_upper_bound order.trans sup_right_isotone top_greatest mult_assoc by presburger
  thus ?thesis
    using 1 by (simp add: apx_def)
qed

lemma mult_apx_right_isotone:
  assumes "x ⊑ y"
    shows "z * x ⊑ z * y"
proof -
  have "x ≤ y ⊔ n(x) * L"
    using assms apx_def by auto
  hence 1: "z * x ≤ z * y ⊔ n(z * x) * L"
    by (smt sup_assoc sup_ge1 sup_bot_right mult_assoc mult_left_dist_sup mult_right_isotone n_L_split)
  have "y ≤ x ⊔ n(x) * top"
    using assms apx_def by auto
  hence "z * y ≤ z * x ⊔ z * n(x) * top"
    by (smt mult_assoc mult_left_dist_sup mult_right_isotone)
  also have "... ≤ z * x ⊔ n(z * x) * top"
    by (smt (verit) sup_assoc le_supI le_sup_iff sup_ge1 sup_bot_right mult_left_dist_sup n_L_split n_top_split order_trans)
  finally show ?thesis
    using 1 by (simp add: apx_def)
qed

text ‹Theorem 16.1 and Theorem 16.2›

subclass apx_semiring
  apply unfold_locales
  apply (metis sup_right_top sup_ge2 apx_def mult_left_one n_L top_greatest)
  apply (simp add: sup_apx_left_isotone)
  apply (simp add: mult_apx_left_isotone)
  by (simp add: mult_apx_right_isotone)

text ‹Theorem 16.2›

lemma ni_apx_isotone:
  "x ⊑ y ⟹ ni(x) ⊑ ni(y)"
  using apx_n_order_reverse apx_def le_supI1 n_ni ni_def ni_n_order by force

text ‹Theorem 17›

definition kappa_apx_meet :: "('a ⇒ 'a) ⇒ bool"
  where "kappa_apx_meet f ≡ apx.has_least_fixpoint f ∧ has_apx_meet (μ f) (ν f) ∧ κ f = μ f △ ν f"

definition kappa_mu_nu :: "('a ⇒ 'a) ⇒ bool"
  where "kappa_mu_nu f ≡ apx.has_least_fixpoint f ∧ κ f = μ f ⊔ n(ν f) * L"

definition nu_below_mu_nu :: "('a ⇒ 'a) ⇒ bool"
  where "nu_below_mu_nu f ≡ ν f ≤ μ f ⊔ n(ν f) * top"

definition mu_nu_apx_nu :: "('a ⇒ 'a) ⇒ bool"
  where "mu_nu_apx_nu f ≡ μ f ⊔ n(ν f) * L ⊑ ν f"

definition mu_nu_apx_meet :: "('a ⇒ 'a) ⇒ bool"
  where "mu_nu_apx_meet f ≡ has_apx_meet (μ f) (ν f) ∧ μ f △ ν f = μ f ⊔ n(ν f) * L"

definition apx_meet_below_nu :: "('a ⇒ 'a) ⇒ bool"
  where "apx_meet_below_nu f ≡ has_apx_meet (μ f) (ν f) ∧ μ f △ ν f ≤ ν f"

lemma mu_below_l:
  "μ f ≤ μ f ⊔ n(ν f) * L"
  by simp

lemma l_below_nu:
  "has_least_fixpoint f ⟹ has_greatest_fixpoint f ⟹ μ f ⊔ n(ν f) * L ≤ ν f"
  by (simp add: mu_below_nu n_L_decreasing)

lemma n_l_nu:
  "has_least_fixpoint f ⟹ has_greatest_fixpoint f ⟹ n(μ f ⊔ n(ν f) * L) = n(ν f)"
  by (metis le_iff_sup mu_below_nu n_dist_sup n_n_L)

lemma l_apx_mu:
  "has_least_fixpoint f ⟹ has_greatest_fixpoint f ⟹ μ f ⊔ n(ν f) * L ⊑ μ f"
  by (simp add: apx_def le_supI1 n_l_nu)

text ‹Theorem 17.4 implies Theorem 17.5›

lemma nu_below_mu_nu_mu_nu_apx_nu:
  "has_least_fixpoint f ⟹ has_greatest_fixpoint f ⟹ nu_below_mu_nu f ⟹ mu_nu_apx_nu f"
  by (smt (z3) l_below_nu apx_def le_sup_iff sup.absorb2 sup_commute sup_monoid.add_assoc mu_nu_apx_nu_def n_l_nu nu_below_mu_nu_def)

text ‹Theorem 17.5 implies Theorem 17.6›

lemma mu_nu_apx_nu_mu_nu_apx_meet:
  assumes "has_least_fixpoint f"
      and "has_greatest_fixpoint f"
      and "mu_nu_apx_nu f"
    shows "mu_nu_apx_meet f"
proof -
  let ?l = "μ f ⊔ n(ν f) * L"
  have "is_apx_meet (μ f) (ν f) ?l"
    apply (unfold is_apx_meet_def, intro conjI)
    apply (simp add: assms(1,2) l_apx_mu)
    using assms(3) mu_nu_apx_nu_def apply blast
    by (meson assms(1,2) l_below_nu apx_def order_trans sup_ge1 sup_left_isotone)
  thus ?thesis
    by (simp add: apx_meet_char mu_nu_apx_meet_def)
qed

text ‹Theorem 17.6 implies Theorem 17.7›

lemma mu_nu_apx_meet_apx_meet_below_nu:
  "has_least_fixpoint f ⟹ has_greatest_fixpoint f ⟹ mu_nu_apx_meet f ⟹ apx_meet_below_nu f"
  using apx_meet_below_nu_def l_below_nu mu_nu_apx_meet_def by auto

text ‹Theorem 17.7 implies Theorem 17.4›

lemma apx_meet_below_nu_nu_below_mu_nu:
  assumes "apx_meet_below_nu f"
    shows "nu_below_mu_nu f"
proof -
  have "∀m . m ⊑ μ f ∧ m ⊑ ν f ∧ m ≤ ν f ⟶ ν f ≤ μ f ⊔ n(m) * top"
    by (smt (verit) sup_assoc sup_left_isotone sup_right_top apx_def mult_left_dist_sup order_trans)
  thus ?thesis
    by (smt (verit) assms sup_right_isotone apx_greatest_lower_bound apx_meet_below_nu_def apx_reflexive mult_left_isotone n_isotone nu_below_mu_nu_def order_trans)
qed

text ‹Theorem 17.1 implies Theorem 17.2›

lemma has_apx_least_fixpoint_kappa_apx_meet:
  assumes "has_least_fixpoint f"
      and "has_greatest_fixpoint f"
      and "apx.has_least_fixpoint f"
    shows "kappa_apx_meet f"
proof -
  have "∀w . w ⊑ μ f ∧ w ⊑ ν f ⟶ w ⊑ κ f"
    by (meson assms apx_def order.trans kappa_below_nu mu_below_kappa semiring.add_right_mono)
  hence "is_apx_meet (μ f) (ν f) (κ f)"
    by (simp add: assms is_apx_meet_def kappa_apx_below_mu kappa_apx_below_nu)
  thus ?thesis
    by (simp add: assms(3) kappa_apx_meet_def apx_meet_char)
qed

text ‹Theorem 17.2 implies Theorem 17.7›

lemma kappa_apx_meet_apx_meet_below_nu:
  "has_greatest_fixpoint f ⟹ kappa_apx_meet f ⟹ apx_meet_below_nu f"
  using apx_meet_below_nu_def kappa_apx_meet_def kappa_below_nu by force

text ‹Theorem 17.7 implies Theorem 17.3›

lemma apx_meet_below_nu_kappa_mu_nu:
  assumes "has_least_fixpoint f"
      and "has_greatest_fixpoint f"
      and "isotone f"
      and "apx.isotone f"
      and "apx_meet_below_nu f"
    shows "kappa_mu_nu f"
proof -
  let ?l = "μ f ⊔ n(ν f) * L"
  let ?m = "μ f △ ν f"
  have 1: "?l ⊑ ν f"
    using apx_meet_below_nu_nu_below_mu_nu assms(1,2,5) mu_nu_apx_nu_def nu_below_mu_nu_mu_nu_apx_nu by blast
  hence 2: "?m = ?l"
    using assms(1,2) mu_nu_apx_meet_def mu_nu_apx_nu_def mu_nu_apx_nu_mu_nu_apx_meet by blast
  have "μ f ≤ f(?l)"
    by (metis assms(1,3) isotone_def mu_unfold sup_ge1)
  hence 3: "?l ≤ f(?l) ⊔ n(?l) * L"
    using assms(1,2) semiring.add_right_mono n_l_nu by auto
  have "f(?l) ≤ f(ν f)"
    using assms(1-3) l_below_nu isotone_def by blast
  also have "... ≤ ?l ⊔ n(?l) * top"
    using 1 by (metis assms(2) apx_def nu_unfold)
  finally have 4: "?l ⊑ f(?l)"
    using 3 apx_def by blast
  have 5: "f(?l) ⊑ μ f"
    by (metis assms(1,2,4) apx.isotone_def is_least_fixpoint_def least_fixpoint l_apx_mu)
  have "f(?l) ⊑ ν f"
    using 1 by (metis assms(2,4) apx.isotone_def greatest_fixpoint is_greatest_fixpoint_def)
  hence "f(?l) ⊑ ?l"
    using 2 5 apx_meet_below_nu_def assms(5) apx_greatest_lower_bound by fastforce
  hence "f(?l) = ?l"
    using 4 by (simp add: apx.order.antisym)
  thus ?thesis
    using 1 by (smt (verit, del_insts) assms(1,2) sup_left_isotone apx_antisymmetric apx_def apx.least_fixpoint_char greatest_fixpoint apx.is_least_fixpoint_def is_greatest_fixpoint_def is_least_fixpoint_def least_fixpoint n_l_nu order_trans kappa_mu_nu_def)
qed

text ‹Theorem 17.3 implies Theorem 17.1›

lemma kappa_mu_nu_has_apx_least_fixpoint:
  "kappa_mu_nu f ⟹ apx.has_least_fixpoint f"
  using kappa_mu_nu_def by auto

text ‹Theorem 17.4 implies Theorem 17.3›

lemma nu_below_mu_nu_kappa_mu_nu:
  "has_least_fixpoint f ⟹ has_greatest_fixpoint f ⟹ isotone f ⟹ apx.isotone f ⟹ nu_below_mu_nu f ⟹ kappa_mu_nu f"
  using apx_meet_below_nu_kappa_mu_nu mu_nu_apx_meet_apx_meet_below_nu mu_nu_apx_nu_mu_nu_apx_meet nu_below_mu_nu_mu_nu_apx_nu by blast

text ‹Theorem 17.3 implies Theorem 17.4›

lemma kappa_mu_nu_nu_below_mu_nu:
  "has_least_fixpoint f ⟹ has_greatest_fixpoint f ⟹ kappa_mu_nu f ⟹ nu_below_mu_nu f"
  by (simp add: apx_meet_below_nu_nu_below_mu_nu has_apx_least_fixpoint_kappa_apx_meet kappa_apx_meet_apx_meet_below_nu kappa_mu_nu_def)

definition kappa_mu_nu_ni :: "('a ⇒ 'a) ⇒ bool"
  where "kappa_mu_nu_ni f ≡ apx.has_least_fixpoint f ∧ κ f = μ f ⊔ ni(ν f)"

lemma kappa_mu_nu_ni_kappa_mu_nu:
  "kappa_mu_nu_ni f ⟷ kappa_mu_nu f"
  by (simp add: kappa_mu_nu_def kappa_mu_nu_ni_def ni_def)

lemma nu_below_mu_nu_kappa_mu_nu_ni:
  "has_least_fixpoint f ⟹ has_greatest_fixpoint f ⟹ isotone f ⟹ apx.isotone f ⟹ nu_below_mu_nu f ⟹ kappa_mu_nu_ni f"
  by (simp add: kappa_mu_nu_ni_kappa_mu_nu nu_below_mu_nu_kappa_mu_nu)

lemma kappa_mu_nu_ni_nu_below_mu_nu:
  "has_least_fixpoint f ⟹ has_greatest_fixpoint f ⟹ kappa_mu_nu_ni f ⟹ nu_below_mu_nu f"
  using kappa_mu_nu_ni_kappa_mu_nu kappa_mu_nu_nu_below_mu_nu by blast

end

class itering_apx = n_itering + semiring_apx
begin

text ‹Theorem 16.3›

lemma circ_apx_isotone:
  assumes "x ⊑ y"
    shows "x⇧∘ ⊑ y⇧∘"
proof -
  have 1: "x ≤ y ⊔ n(x) * L ∧ y ≤ x ⊔ n(x) * top"
    using assms apx_def by auto
  hence "y⇧∘ ≤ x⇧∘ ⊔ x⇧∘ * n(x) * top"
    by (metis circ_isotone circ_left_top circ_unfold_sum mult_assoc)
  also have "... ≤ x⇧∘ ⊔ n(x⇧∘ * x) * top"
    by (smt le_sup_iff n_isotone n_top_split order_refl order_trans right_plus_below_circ zero_right_mult_decreasing)
  also have "... ≤ x⇧∘ ⊔ n(x⇧∘) * top"
    by (simp add: circ_plus_same n_circ_left_unfold)
  finally have 2: "y⇧∘ ≤ x⇧∘ ⊔ n(x⇧∘) * top"
    .
  have "x⇧∘ ≤ y⇧∘ ⊔ y⇧∘ * n(x) * L"
    using 1 by (metis L_left_zero circ_isotone circ_unfold_sum mult_assoc)
  also have "... = y⇧∘ ⊔ n(y⇧∘ * x) * L"
    by (metis sup_assoc sup_bot_right mult_assoc mult_zero_sup_circ_2 n_L_split n_mult_right_bot)
  also have "... ≤ y⇧∘ ⊔ n(x⇧∘ * x) * L ⊔ n(x⇧∘) * n(top * x) * L"
    using 2 by (metis sup_assoc sup_right_isotone mult_assoc mult_left_isotone mult_right_dist_sup n_dist_sup n_export n_isotone)
  finally have "x⇧∘ ≤ y⇧∘ ⊔ n(x⇧∘) * L"
    by (metis sup_assoc circ_plus_same n_sup_left_absorb_mult n_circ_left_unfold n_dist_sup n_export ni_def ni_dist_sup)
  thus ?thesis
    using 2 by (simp add: apx_def)
qed

end

class omega_algebra_apx = n_omega_algebra_2 + semiring_apx

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

sublocale omega_algebra_apx < nL_omega: itering_apx where circ = Omega ..

context omega_algebra_apx
begin

text ‹Theorem 16.4›

lemma omega_apx_isotone:
  assumes "x ⊑ y"
    shows "x⇧ω ⊑ y⇧ω"
proof -
  have 1: "x ≤ y ⊔ n(x) * L ∧ y ≤ x ⊔ n(x) * top"
    using assms apx_def by auto
  hence "y⇧ω ≤ x⇧⋆ * n(x) * top * (x⇧⋆ * n(x) * top)⇧ω ⊔ x⇧ω ⊔ x⇧⋆ * n(x) * top * (x⇧⋆ * n(x) * top)⇧⋆ * x⇧ω"
    by (smt sup_assoc mult_assoc mult_left_one mult_right_dist_sup omega_decompose omega_isotone omega_unfold star_left_unfold_equal)
  also have "... ≤ x⇧⋆ * n(x) * top ⊔ x⇧ω ⊔ x⇧⋆ * n(x) * top * (x⇧⋆ * n(x) * top)⇧⋆ * x⇧ω"
    using mult_top_omega omega_unfold sup_left_isotone by auto
  also have "... = x⇧⋆ * n(x) * top ⊔ x⇧ω"
    by (smt (z3) mult_left_dist_sup sup_assoc sup_commute sup_left_top mult_assoc)
  also have "... ≤ n(x⇧⋆ * x) * top ⊔ x⇧⋆ * bot ⊔ x⇧ω"
    using n_top_split semiring.add_left_mono sup_commute by fastforce
  also have "... ≤ n(x⇧⋆ * x) * top ⊔ x⇧ω"
    using semiring.add_right_mono star_bot_below_omega sup_commute by fastforce
  finally have 2: "y⇧ω ≤ x⇧ω ⊔ n(x⇧ω) * top"
    by (metis sup_commute sup_right_isotone mult_left_isotone n_star_below_n_omega n_star_left_unfold order_trans star.circ_plus_same)
  have "x⇧ω ≤ (y ⊔ n(x) * L)⇧ω"
    using 1 by (simp add: omega_isotone)
  also have "... = y⇧⋆ * n(x) * L * (y⇧⋆ * n(x) * L)⇧ω ⊔ y⇧ω ⊔ y⇧⋆ * n(x) * L * (y⇧⋆ * n(x) * L)⇧⋆ * y⇧ω"
    by (smt sup_assoc mult_assoc mult_left_one mult_right_dist_sup omega_decompose omega_isotone omega_unfold star_left_unfold_equal)
  also have "... = y⇧⋆ * n(x) * L ⊔ y⇧ω"
    using L_left_zero sup_assoc sup_monoid.add_commute mult_assoc by force
  also have "... ≤ y⇧ω ⊔ y⇧⋆ * bot ⊔ n(y⇧⋆ * x) * L"
    by (simp add: n_L_split sup_assoc sup_commute)
  also have "... ≤ y⇧ω ⊔ n(x⇧⋆ * x) * L ⊔ n(x⇧⋆) * n(top * x) * L"
    using 1 by (metis sup_right_isotone sup_bot_right apx_def mult_assoc mult_left_dist_sup mult_left_isotone mult_right_dist_sup n_dist_sup n_export n_isotone star.circ_apx_isotone star_mult_omega sup_assoc)
  finally have "x⇧ω ≤ y⇧ω ⊔ n(x⇧ω) * L"
    by (smt (verit, best) le_supE sup.orderE sup_commute sup_assoc sup_isotone mult_right_dist_sup n_sup_left_absorb_mult n_star_left_unfold ni_def ni_star_below_ni_omega order_refl order_trans star.circ_plus_same)
  thus ?thesis
    using 2 by (simp add: apx_def)
qed

end

class omega_algebra_apx_extra = omega_algebra_apx +
  assumes n_split_omega: "x⇧ω ≤ x⇧⋆ * bot ⊔ n(x⇧ω) * top"
begin

lemma omega_n_star:
  "x⇧ω ⊔ n(x⇧⋆) * top ≤ x⇧⋆ * n(x⇧ω) * top"
proof -
  have 1: "n(x⇧⋆) * top ≤ n(x⇧ω) * top"
    by (simp add: mult_left_isotone n_star_below_n_omega)
  have "... ≤ x⇧⋆ * n(x⇧ω) * top"
    by (simp add: star_n_omega_top)
  thus ?thesis
    using 1 by (metis le_sup_iff n_split_omega order_trans star_n_omega_top)
qed

lemma n_omega_zero:
  "n(x⇧ω) = bot ⟷ n(x⇧⋆) = bot ∧ x⇧ω ≤ x⇧⋆ * bot"
  by (metis sup_bot_right order.eq_iff mult_left_zero n_mult_bot n_split_omega star_bot_below_omega)

lemma n_split_nu_mu:
  "y⇧ω ⊔ y⇧⋆ * z ≤ y⇧⋆ * z ⊔ n(y⇧ω ⊔ y⇧⋆ * z) * top"
proof -
  have "y⇧ω ≤ y⇧⋆ * bot ⊔ n(y⇧ω ⊔ y⇧⋆ * z) * top"
    by (smt sup_ge1 sup_right_isotone mult_left_isotone n_isotone n_split_omega order_trans)
  also have "... ≤ y⇧⋆ * z ⊔ n(y⇧ω ⊔ y⇧⋆ * z) * top"
    using nL_star.star_zero_below_circ_mult sup_left_isotone by auto
  finally show ?thesis
    by simp
qed

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

lemma loop_apx_least_fixpoint:
  "apx.is_least_fixpoint (λx . y * x ⊔ z) (μ (λx . y * x ⊔ z) ⊔ n(ν (λx . y * x ⊔ z)) * L)"
  using apx.least_fixpoint_char affine_apx_isotone affine_has_greatest_fixpoint affine_has_least_fixpoint affine_isotone kappa_mu_nu_def nu_below_mu_nu_def nu_below_mu_nu_kappa_mu_nu loop_exists by auto

lemma loop_has_apx_least_fixpoint:
  "apx.has_least_fixpoint (λx . y * x ⊔ z)"
  using affine_apx_isotone affine_has_greatest_fixpoint affine_has_least_fixpoint affine_isotone kappa_mu_nu_def nu_below_mu_nu_def nu_below_mu_nu_kappa_mu_nu loop_exists by auto

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 auto

lemma loop_apx_least_fixpoint_ni:
  "apx.is_least_fixpoint (λx . y * x ⊔ z) (μ (λx . y * x ⊔ z) ⊔ ni(ν (λx . y * x ⊔ z)))"
  using ni_def loop_apx_least_fixpoint by auto

lemma loop_semantics_ni:
  "κ (λx . y * x ⊔ z) = μ (λx . y * x ⊔ z) ⊔ ni(ν (λx . y * x ⊔ z))"
  using ni_def loop_semantics by auto

text ‹Theorem 18›

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"
    by (metis loop_semantics omega_loop_nu star_loop_mu)
  thus ?thesis
    by (smt sup_assoc sup_commute le_iff_sup mult_right_dist_sup n_L_decreasing n_dist_sup)
qed

end

class omega_algebra_apx_extra_2 = omega_algebra_apx +
  assumes omega_n_star: "x⇧ω ≤ x⇧⋆ * n(x⇧ω) * top"
begin

subclass omega_algebra_apx_extra
  apply unfold_locales
  using omega_n_star star_n_omega_top by auto

end

end