Theory Domain_Recursion

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

section ‹Domain Recursion›

theory Domain_Recursion

imports Domain_Iterings Approximation

begin

class domain_semiring_lattice_apx = domain_semiring_lattice_L + apx +
  assumes apx_def: "x ⊑ y ⟷ x ≤ y ⊔ L ∧ d(L) * y ≤ x ⊔ d(x * bot) * top"
begin

lemma apx_transitive:
  assumes "x ⊑ y"
      and "y ⊑ z"
    shows "x ⊑ z"
proof -
  have 1: "x ≤ z ⊔ L"
    by (smt assms sup_assoc sup_commute apx_def le_iff_sup)
  have "d(d(L) * y * bot) * top ≤ d((x ⊔ d(x * bot) * top) * bot) * top"
    by (metis assms(1) apx_def d_isotone mult_left_isotone)
  also have "... ≤ d(x * bot) * top"
    by (metis le_sup_iff d_galois mult_left_isotone mult_right_dist_sup order_refl zero_right_mult_decreasing)
  finally have 2: "d(d(L) * y * bot) * top ≤ d(x * bot) * top"
    .
  have "d(L) * z = d(L) * (d(L) * z)"
    by (simp add: d_mult_idempotent ils.il_inf_associative)
  also have "... ≤ d(L) * y ⊔ d(d(L) * y * bot) * top"
    by (metis assms(2) apx_def d_export mult_assoc mult_left_dist_sup mult_right_isotone)
  also have "... ≤ x ⊔ d(x * bot) * top"
    using 2 by (meson assms(1) apx_def le_supI2 sup_least)
  finally show ?thesis
    using 1 by (simp add: apx_def)
qed

lemma apx_meet_L:
  assumes "y ⊑ x"
    shows "x ⊓ L ≤ y ⊓ L"
proof -
  have "x ⊓ L = d(L) * x ⊓ L"
    using meet_intro_domain by auto
  also have "... ≤ (y ⊔ d(y * bot) * top) ⊓ L"
    using assms apx_def inf.sup_left_isotone by blast
  also have "... ≤ y"
    by (simp add: inf.sup_monoid.add_commute inf_sup_distrib1 l13 meet_domain_top)
  finally show ?thesis
    by simp
qed

lemma sup_apx_left_isotone:
  assumes "x ⊑ y"
    shows "x ⊔ z ⊑ y ⊔ z"
proof -
  have 1: "x ⊔ z ≤ y ⊔ z ⊔ L"
    by (smt assms sup_assoc sup_commute sup_left_isotone apx_def)
  have "d(L) * (y ⊔ z) = d(L) * y ⊔ d(L) * z"
    by (simp add: mult_left_dist_sup)
  also have "... ≤ d(L) * y ⊔ z"
    by (simp add: d_mult_below le_supI1 sup_commute)
  also have "... ≤ x ⊔ d(x * bot) * top ⊔ z"
    using assms apx_def sup_left_isotone by blast
  also have "... ≤ x ⊔ z ⊔ d((x ⊔ z) * bot) * top"
    by (simp add: d_dist_sup le_iff_sup semiring.distrib_right sup.left_commute sup_monoid.add_assoc)
  finally show ?thesis
    using 1 by (simp add: apx_def)
qed

subclass apx_biorder
  apply unfold_locales
  apply (metis le_sup_iff sup_ge1 apx_def d_plus_one mult_left_one mult_right_dist_sup)
  apply (meson apx_meet_L order.antisym apx_def relative_equality sup_same_context)
  using apx_transitive by blast

lemma mult_apx_left_isotone:
  assumes "x ⊑ y"
    shows "x * z ⊑ y * z"
proof -
  have "x * z ≤ y * z ⊔ L * z"
    by (metis assms apx_def mult_left_isotone mult_right_dist_sup)
  hence 1: "x * z ≤ y * z ⊔ L"
    using l40 order_lesseq_imp semiring.add_left_mono by blast
  have "d(L) * y * z ≤ x * z ⊔ d(x * bot) * top * z"
    by (metis assms apx_def mult_left_isotone mult_right_dist_sup)
  also have "... ≤ x * z ⊔ d(x * z * bot) * top"
    by (metis sup_right_isotone d_isotone mult_assoc mult_isotone mult_right_isotone top_greatest bot_least)
  finally show ?thesis
    using 1 by (simp add: apx_def mult_assoc)
qed

lemma mult_apx_right_isotone:
  assumes "x ⊑ y"
    shows "z * x ⊑ z * y"
proof -
  have "z * x ≤ z * y ⊔ z * L"
    by (metis assms apx_def mult_left_dist_sup mult_right_isotone)
  also have "... ≤ z * y ⊔ z * bot ⊔ L"
    using l14 semiring.add_left_mono sup_monoid.add_assoc by auto
  finally have 1: "z * x ≤ z * y ⊔ L"
    using mult_right_isotone sup.order_iff by auto
  have "d(L) * z * y ≤ z * d(L) * y"
    by (simp add: l2 mult_left_isotone)
  also have "... ≤ z * (x ⊔ d(x * bot) * top)"
    by (metis assms apx_def mult_assoc mult_right_isotone)
  also have "... = z * x ⊔ z * d(x * bot) * top"
    by (simp add: mult_left_dist_sup mult_assoc)
  also have "... ≤ z * x ⊔ d(z * x * bot) * top"
    by (metis sup_right_isotone mult_assoc mult_domain_top)
  finally show ?thesis
    using 1 by (simp add: apx_def mult_assoc)
qed

subclass apx_semiring
  apply unfold_locales
  apply (metis sup_ge2 apx_def l3 mult_right_isotone order_trans top_greatest)
  apply (simp add: sup_apx_left_isotone)
  apply (simp add: mult_apx_left_isotone)
  by (simp add: mult_apx_right_isotone)

lemma meet_L_apx_isotone:
  "x ⊑ y ⟹ x ⊓ L ⊑ y ⊓ L"
  by (smt (z3) inf.cobounded2 sup.coboundedI1 sup_absorb sup_commute apx_def apx_meet_L d_restrict_equals l20 inf_commute meet_domain)

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 ⊔ (ν f ⊓ L)"

definition nu_below_mu_nu :: "('a ⇒ 'a) ⇒ bool"
  where "nu_below_mu_nu f ≡ d(L) * ν f ≤ μ f ⊔ (ν f ⊓ L) ⊔ d(ν f * bot) * top"

definition nu_below_mu_nu_2 :: "('a ⇒ 'a) ⇒ bool"
  where "nu_below_mu_nu_2 f ≡ d(L) * ν f ≤ μ f ⊔ (ν f ⊓ L) ⊔ d((μ f ⊔ (ν f ⊓ L)) * bot) * top"

definition mu_nu_apx_nu :: "('a ⇒ 'a) ⇒ bool"
  where "mu_nu_apx_nu f ≡ μ f ⊔ (ν 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 ⊔ (ν 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 ⊔ (ν f ⊓ L)"
  by simp

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

lemma n_l_nu:
  "has_least_fixpoint f ⟹ has_greatest_fixpoint f ⟹ (μ f ⊔ (ν f ⊓ L)) ⊓ L = ν f ⊓ L"
  by (meson l_below_nu inf.sup_same_context inf_le1 order_trans sup.cobounded2)

lemma l_apx_mu:
  "μ f ⊔ (ν f ⊓ L) ⊑ μ f"
  by (simp add: apx_def d_mult_below le_supI1 sup_inf_distrib1)

lemma nu_below_mu_nu_nu_below_mu_nu_2:
  assumes "nu_below_mu_nu f"
    shows "nu_below_mu_nu_2 f"
proof -
  have "d(L) * ν f = d(L) * (d(L) * ν f)"
    by (simp add: d_mult_idempotent ils.il_inf_associative)
  also have "... ≤ d(L) * (μ f ⊔ (ν f ⊓ L) ⊔ d(ν f * bot) * top)"
    using assms mult_isotone nu_below_mu_nu_def by blast
  also have "... = d(L) * (μ f ⊔ (ν f ⊓ L)) ⊔ d(L) * d(ν f * bot) * top"
    by (simp add: ils.il_inf_associative mult_left_dist_sup)
  also have "... ≤ μ f ⊔ (ν f ⊓ L) ⊔ d(L) * d(ν f * bot) * top"
    using d_mult_below sup_left_isotone by auto
  also have "... = μ f ⊔ (ν f ⊓ L) ⊔ d(d(ν f * bot) * L) * top"
    by (simp add: d_commutative d_export)
  also have "... = μ f ⊔ (ν f ⊓ L) ⊔ d((ν f ⊓ L) * bot) * top"
    using l51 by auto
  also have "... ≤ μ f ⊔ (ν f ⊓ L) ⊔ d((μ f ⊔ (ν f ⊓ L)) * bot) * top"
    by (meson d_isotone inf.eq_refl mult_isotone semiring.add_left_mono sup.cobounded2)
  finally show ?thesis
    using nu_below_mu_nu_2_def by auto
qed

lemma nu_below_mu_nu_2_nu_below_mu_nu:
  assumes "has_least_fixpoint f"
      and "has_greatest_fixpoint f"
      and "nu_below_mu_nu_2 f"
    shows "nu_below_mu_nu f"
proof -
  have "d(L) * ν f ≤ μ f ⊔ (ν f ⊓ L) ⊔ d((μ f ⊔ (ν f ⊓ L)) * bot) * top"
    using assms(3) nu_below_mu_nu_2_def by blast
  also have "... ≤ μ f ⊔ (ν f ⊓ L) ⊔ d(ν f * bot) * top"
    by (metis assms(1,2) d_isotone inf.sup_monoid.add_commute inf.sup_right_divisibility le_supI le_supI2 mu_below_nu mult_left_isotone sup_left_divisibility)
  finally show ?thesis
    by (simp add: nu_below_mu_nu_def)
qed

lemma nu_below_mu_nu_equivalent:
  "has_least_fixpoint f ⟹ has_greatest_fixpoint f ⟹ (nu_below_mu_nu f ⟷ nu_below_mu_nu_2 f)"
  using nu_below_mu_nu_2_nu_below_mu_nu nu_below_mu_nu_nu_below_mu_nu_2 by blast

lemma nu_below_mu_nu_2_mu_nu_apx_nu:
  assumes "has_least_fixpoint f"
      and "has_greatest_fixpoint f"
      and "nu_below_mu_nu_2 f"
    shows "mu_nu_apx_nu f"
proof -
  have "μ f ⊔ (ν f ⊓ L) ≤ ν f ⊔ L"
    using assms(1,2) l_below_nu le_supI1 by blast
  thus ?thesis
    using assms(3) apx_def mu_nu_apx_nu_def nu_below_mu_nu_2_def by blast
qed

lemma mu_nu_apx_nu_mu_nu_apx_meet:
  assumes "mu_nu_apx_nu f"
    shows "mu_nu_apx_meet f"
proof -
  let ?l = "μ f ⊔ (ν f ⊓ L)"
  have "is_apx_meet (μ f) (ν f) ?l"
    apply (unfold is_apx_meet_def, intro conjI)
    apply (simp add: l_apx_mu)
    using assms mu_nu_apx_nu_def apply blast
    by (metis apx_meet_L le_supI2 sup.order_iff sup_apx_left_isotone sup_inf_absorb)
  thus ?thesis
    by (smt apx_meet_char mu_nu_apx_meet_def)
qed

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

lemma apx_meet_below_nu_nu_below_mu_nu_2:
  assumes "apx_meet_below_nu f"
    shows "nu_below_mu_nu_2 f"
proof -
  let ?l = "μ f ⊔ (ν f ⊓ L)"
  have "∀m . m ⊑ μ f ∧ m ⊑ ν f ∧ m ≤ ν f ⟶ d(L) * ν f ≤ ?l ⊔ d(?l * bot) * top"
  proof
    fix m
    show "m ⊑ μ f ∧ m ⊑ ν f ∧ m ≤ ν f ⟶ d(L) * ν f ≤ ?l ⊔ d(?l * bot) * top"
    proof
      assume 1: "m ⊑ μ f ∧ m ⊑ ν f ∧ m ≤ ν f"
      hence "m ≤ ?l"
        by (metis apx_def ils.il_associative sup.orderE sup.orderI sup_inf_distrib1 sup_inf_distrib2)
      hence "m ⊔ d(m * bot) * top ≤ ?l ⊔ d(?l * bot) * top"
        by (meson d_isotone order.trans le_supI le_supI2 mult_left_isotone sup.cobounded1)
      thus "d(L) * ν f ≤ ?l ⊔ d(?l * bot) * top"
        using 1 apx_def order_lesseq_imp by blast
    qed
  qed
  thus ?thesis
    by (smt (verit) assms apx_meet_below_nu_def apx_meet_same apx_meet_unique is_apx_meet_def nu_below_mu_nu_2_def)
qed

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 1: "∀w . w ⊑ μ f ∧ w ⊑ ν f ⟶ d(L) * κ f ≤ w ⊔ d(w * bot) * top"
    by (metis assms(2,3) apx_def mult_right_isotone order_trans kappa_below_nu)
  have "∀w . w ⊑ μ f ∧ w ⊑ ν f ⟶ w ≤ κ f ⊔ L"
    by (metis assms(1,3) sup_left_isotone apx_def mu_below_kappa order_trans)
  hence "∀w . w ⊑ μ f ∧ w ⊑ ν f ⟶ w ⊑ κ f"
    using 1 apx_def by blast
  hence "is_apx_meet (μ f) (ν f) (κ f)"
    using assms apx_meet_char is_apx_meet_def kappa_apx_below_mu kappa_apx_below_nu kappa_apx_meet_def by presburger
  thus ?thesis
    by (simp add: assms(3) kappa_apx_meet_def apx_meet_char)
qed

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

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 ⊔ (ν f ⊓ L)"
  let ?m = "μ f △ ν f"
  have 1: "?m = ?l"
    by (metis assms(1,2,5) apx_meet_below_nu_nu_below_mu_nu_2 mu_nu_apx_meet_def mu_nu_apx_nu_mu_nu_apx_meet nu_below_mu_nu_2_mu_nu_apx_nu)
  have 2: "?l ≤ f(?l) ⊔ L"
  proof -
    have "?l ≤ μ f ⊔ L"
      using sup_right_isotone by auto
    also have "... = f(μ f) ⊔ L"
      by (simp add: assms(1) mu_unfold)
    also have "... ≤ f(?l) ⊔ L"
      by (metis assms(3) sup_left_isotone sup_ge1 isotone_def)
    finally show ?thesis
      .
  qed
  have "d(L) * f(?l) ≤ ?l ⊔ d(?l * bot) * top"
  proof -
    have "d(L) * f(?l) ≤ d(L) * f(ν f)"
      by (metis assms(1-3) l_below_nu mult_right_isotone ord.isotone_def)
    also have "... = d(L) * ν f"
      by (metis assms(2) nu_unfold)
    also have "... ≤ ?l ⊔ d(?l * bot) * top"
      using apx_meet_below_nu_nu_below_mu_nu_2 assms(5) nu_below_mu_nu_2_def by blast
    finally show ?thesis
      .
  qed
  hence 3: "?l ⊑ f(?l)"
    using 2 by (simp add: apx_def)
  have 4: "f(?l) ⊑ μ f"
  proof -
    have "?l ⊑ μ f"
      by (simp add: l_apx_mu)
    thus ?thesis
      by (metis assms(1,4) mu_unfold ord.isotone_def)
  qed
  have 5: "f(?l) ⊑ ν f"
  proof -
    have "?l ⊑ ν f"
      by (meson apx_meet_below_nu_nu_below_mu_nu_2 assms(1,2,5) l_below_nu apx_def le_supI1 nu_below_mu_nu_2_def)
    thus ?thesis
      by (metis assms(2,4) nu_unfold ord.isotone_def)
  qed
  hence "f(?l) ⊑ ?l"
    using 1 4 apx_meet_below_nu_def assms(5) apx_greatest_lower_bound by fastforce
  hence 6: "f(?l) = ?l"
    using 3 apx.order.antisym by blast
  have "∀y . f(y) = y ⟶ ?l ⊑ y"
  proof
    fix y
    show "f(y) = y ⟶ ?l ⊑ y"
    proof
      assume 7: "f(y) = y"
      hence 8: "?l ≤ y ⊔ L"
        using assms(1) inf.cobounded2 is_least_fixpoint_def least_fixpoint semiring.add_mono by blast
      have "y ≤ ν f"
        using 7 assms(2) greatest_fixpoint is_greatest_fixpoint_def by auto
      hence "d(L) * y ≤ ?l ⊔ d(?l * bot) * top"
        using 3 5 by (smt (z3) apx.order.trans apx_def semiring.distrib_left sup.absorb_iff2 sup_assoc)
      thus "?l ⊑ y"
        using 8 by (simp add: apx_def)
    qed
  qed
  thus ?thesis
    using 1 6 by (smt (verit) kappa_mu_nu_def apx.is_least_fixpoint_def apx.least_fixpoint_char)
qed

lemma kappa_mu_nu_has_apx_least_fixpoint:
  "kappa_mu_nu f ⟹ apx.has_least_fixpoint f"
  by (simp add: kappa_mu_nu_def)

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_2_mu_nu_apx_nu nu_below_mu_nu_nu_below_mu_nu_2 by blast

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_2 has_apx_least_fixpoint_kappa_apx_meet kappa_apx_meet_apx_meet_below_nu kappa_mu_nu_def nu_below_mu_nu_2_nu_below_mu_nu)

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

definition nu_below_mu_nu_L :: "('a ⇒ 'a) ⇒ bool"
  where "nu_below_mu_nu_L f ≡ d(L) * ν f ≤ μ f ⊔ d(ν f * bot) * top"

definition mu_nu_apx_nu_L :: "('a ⇒ 'a) ⇒ bool"
  where "mu_nu_apx_nu_L f ≡ μ f ⊔ d(ν f * bot) * L ⊑ ν f"

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

lemma n_below_l:
  "x ⊔ d(y * bot) * L ≤ x ⊔ (y ⊓ L)"
  using d_mult_below l13 sup_right_isotone by auto

lemma n_equal_l:
  assumes "nu_below_mu_nu_L f"
    shows"μ f ⊔ d(ν f * bot) * L = μ f ⊔ (ν f ⊓ L)"
proof -
  have "ν f ⊓ L ≤ (μ f ⊔ d(ν f * bot) * top) ⊓ L"
    using assms l31 nu_below_mu_nu_L_def by force
  also have "... ≤ μ f ⊔ d(ν f * bot) * L"
    using distrib(4) inf.sup_monoid.add_commute meet_domain_top sup_left_isotone by force
  finally have "μ f ⊔ (ν f ⊓ L) ≤ μ f ⊔ d(ν f * bot) * L"
    by auto
  thus ?thesis
    by (meson order.antisym n_below_l)
qed

lemma nu_below_mu_nu_L_nu_below_mu_nu:
  "nu_below_mu_nu_L f ⟹ nu_below_mu_nu f"
  using order_lesseq_imp sup.cobounded1 sup_left_isotone nu_below_mu_nu_L_def nu_below_mu_nu_def by blast

lemma nu_below_mu_nu_L_kappa_mu_nu_L:
  "has_least_fixpoint f ⟹ has_greatest_fixpoint f ⟹ isotone f ⟹ apx.isotone f ⟹ nu_below_mu_nu_L f ⟹ kappa_mu_nu_L f"
  using kappa_mu_nu_L_def kappa_mu_nu_def n_equal_l nu_below_mu_nu_L_nu_below_mu_nu nu_below_mu_nu_kappa_mu_nu by auto

lemma nu_below_mu_nu_L_mu_nu_apx_nu_L:
  "has_least_fixpoint f ⟹ has_greatest_fixpoint f ⟹ nu_below_mu_nu_L f ⟹ mu_nu_apx_nu_L f"
  using mu_nu_apx_nu_L_def mu_nu_apx_nu_def n_equal_l nu_below_mu_nu_2_mu_nu_apx_nu nu_below_mu_nu_L_nu_below_mu_nu nu_below_mu_nu_nu_below_mu_nu_2 by auto

lemma nu_below_mu_nu_L_mu_nu_apx_meet_L:
  "has_least_fixpoint f ⟹ has_greatest_fixpoint f ⟹ nu_below_mu_nu_L f ⟹ mu_nu_apx_meet_L f"
  using mu_nu_apx_meet_L_def mu_nu_apx_meet_def mu_nu_apx_nu_mu_nu_apx_meet n_equal_l nu_below_mu_nu_2_mu_nu_apx_nu nu_below_mu_nu_L_nu_below_mu_nu nu_below_mu_nu_nu_below_mu_nu_2 by auto

lemma mu_nu_apx_nu_L_nu_below_mu_nu_L:
  assumes "has_least_fixpoint f"
      and "has_greatest_fixpoint f"
      and "mu_nu_apx_nu_L f"
    shows "nu_below_mu_nu_L f"
proof -
  let ?n = "μ f ⊔ d(ν f * bot) * L"
  let ?l = "μ f ⊔ (ν f ⊓ L)"
  have "d(L) * ν f ≤ ?n ⊔ d(?n * bot) * top"
    using assms(3) apx_def mu_nu_apx_nu_L_def by blast
  also have "... ≤ ?n ⊔ d(?l * bot) * top"
    using d_isotone mult_left_isotone semiring.add_left_mono n_below_l by auto
  also have "... ≤ ?n ⊔ d(ν f * bot) * top"
    by (meson assms(1,2) l_below_nu d_isotone mult_left_isotone sup_right_isotone)
  finally show ?thesis
    by (metis sup_assoc sup_right_top mult_left_dist_sup nu_below_mu_nu_L_def)
qed

lemma kappa_mu_nu_L_mu_nu_apx_nu_L:
  "has_greatest_fixpoint f ⟹ kappa_mu_nu_L f ⟹ mu_nu_apx_nu_L f"
  using kappa_mu_nu_L_def kappa_apx_below_nu mu_nu_apx_nu_L_def by force

lemma mu_nu_apx_meet_L_mu_nu_apx_nu_L:
  "mu_nu_apx_meet_L f ⟹ mu_nu_apx_nu_L f"
  using apx_greatest_lower_bound mu_nu_apx_meet_L_def mu_nu_apx_nu_L_def by fastforce

lemma kappa_mu_nu_L_nu_below_mu_nu_L:
  "has_least_fixpoint f ⟹ has_greatest_fixpoint f ⟹ kappa_mu_nu_L f ⟹ nu_below_mu_nu_L f"
  using kappa_mu_nu_L_mu_nu_apx_nu_L mu_nu_apx_nu_L_nu_below_mu_nu_L by auto

end

class itering_apx = domain_itering_lattice_L + domain_semiring_lattice_apx
begin

lemma circ_apx_isotone:
  assumes "x ⊑ y"
    shows "x⇧∘ ⊑ y⇧∘"
proof -
  have 1: "x ≤ y ⊔ L ∧ d(L) * y ≤ x ⊔ d(x * bot) * top"
    using assms apx_def by auto
  have "d(L) * y⇧∘ ≤ (d(L) * y)⇧∘"
    by (metis d_circ_import d_mult_below l2)
  also have "... ≤ x⇧∘ * (d(x * bot) * top * x⇧∘)⇧∘"
    using 1 by (metis circ_sup_1 circ_isotone)
  also have "... = x⇧∘ ⊔ x⇧∘ * d(x * bot) * top"
    by (metis circ_left_top mult_assoc mult_left_dist_sup mult_1_right mult_top_circ)
  also have "... ≤ x⇧∘ ⊔ d(x⇧∘ * x * bot) * top"
    by (metis sup_right_isotone mult_assoc mult_domain_top)
  finally have 2: "d(L) * y⇧∘ ≤ x⇧∘ ⊔ d(x⇧∘ * bot) * top"
    using circ_plus_same d0_circ_left_unfold by auto
  have "x⇧∘ ≤ y⇧∘ * L⇧∘"
    using 1 by (metis circ_sup_1 circ_back_loop_fixpoint circ_isotone l40 le_iff_sup mult_assoc)
  also have "... = y⇧∘ ⊔ y⇧∘ * L"
    by (simp add: circ_L mult_left_dist_sup sup_commute)
  also have "... ≤ y⇧∘ ⊔ y⇧∘ * bot ⊔ L"
    using l14 semiring.add_left_mono sup_monoid.add_assoc by auto
  finally have "x⇧∘ ≤ y⇧∘ ⊔ L"
    using sup.absorb_iff1 zero_right_mult_decreasing by auto
  thus ?thesis
    using 2 by (simp add: apx_def)
qed

end

class omega_algebra_apx = domain_omega_algebra_lattice_L + domain_semiring_lattice_apx

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

context omega_algebra_apx
begin

lemma omega_apx_isotone:
  assumes "x ⊑ y"
    shows "x⇧ω ⊑ y⇧ω"
proof -
  have 1: "x ≤ y ⊔ L ∧ d(L) * y ≤ x ⊔ d(x * bot) * top"
    using assms apx_def by auto
  have "d(L) * y⇧ω = (d(L) * y)⇧ω"
    by (simp add: d_omega_export l2)
  also have "... ≤ (x ⊔ d(x * bot) * top)⇧ω"
    using 1 by (simp add: omega_isotone)
  also have "... = (x⇧⋆ * d(x * bot) * top)⇧ω ⊔ (x⇧⋆ * d(x * bot) * top)⇧⋆ * x⇧ω"
    by (simp add: ils.il_inf_associative omega_decompose)
  also have "... ≤ x⇧⋆ * d(x * bot) * top ⊔ (x⇧⋆ * d(x * bot) * top)⇧⋆ * x⇧ω"
    using mult_top_omega sup_left_isotone by blast
  also have "... = x⇧⋆ * d(x * bot) * top ⊔ (1 ⊔ x⇧⋆ * d(x * bot) * top * (x⇧⋆ * d(x * bot) * top)⇧⋆) * x⇧ω"
    by (simp add: star_left_unfold_equal)
  also have "... ≤ x⇧ω ⊔ x⇧⋆ * d(x * bot) * top"
    by (smt (verit, ccfv_threshold) sup_mono le_sup_iff mult_assoc mult_left_one mult_right_dist_sup mult_right_isotone order_refl top_greatest)
  also have "... ≤ x⇧ω ⊔ d(x⇧⋆ * x * bot) * top"
    by (metis sup_right_isotone mult_assoc mult_domain_top)
  also have "... ≤ x⇧ω ⊔ d(x⇧⋆ * bot) * top"
    by (simp add: dL_star.d0_circ_left_unfold star_plus)
  finally have 2: "d(L) * y⇧ω ≤ x⇧ω ⊔ d(x⇧ω * bot) * top"
    by (meson sup_right_isotone d0_star_below_d0_omega mult_left_isotone order_trans)
  have "x⇧ω ≤ (y ⊔ L)⇧ω"
    using 1 by (simp add: omega_isotone)
  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⇧ω"
    using mult_L_omega omega_unfold sup_left_isotone by auto
  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: dL_star.mult_L_circ_mult_below star_left_unfold_equal sup_commute)
  also have "... ≤ y⇧⋆ * bot ⊔ L ⊔ y⇧ω"
    by (simp add: l14 le_supI1)
  finally have "x⇧ω ≤ y⇧ω ⊔ L"
    using star_bot_below_omega sup.left_commute sup.order_iff sup_commute by auto
  thus ?thesis
    using 2 by (simp add: apx_def)
qed

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

lemma d_split_nu_mu:
  "d(L) * (y⇧ω ⊔ y⇧⋆ * z) ≤ y⇧⋆ * z ⊔ ((y⇧ω ⊔ y⇧⋆ * z) ⊓ L) ⊔ d((y⇧ω ⊔ y⇧⋆ * z) * bot) * top"
proof -
  have "d(L) * y⇧ω ≤ (y⇧ω ⊓ L) ⊔ d(y⇧ω * bot) * top"
    using l31 l91 omega_vector sup_right_isotone by auto
  hence "d(L) * (y⇧ω ⊔ y⇧⋆ * z) ≤ y⇧⋆ * z ⊔ (y⇧ω ⊓ L) ⊔ d(y⇧ω * bot) * top"
    by (smt sup_assoc sup_commute sup_mono d_mult_below mult_left_dist_sup)
  also have "... ≤ y⇧⋆ * z ⊔ ((y⇧ω ⊔ y⇧⋆ * z) ⊓ L) ⊔ d(y⇧ω * bot) * top"
    by (simp add: le_supI1 le_supI2)
  also have "... ≤ y⇧⋆ * z ⊔ ((y⇧ω ⊔ y⇧⋆ * z) ⊓ L) ⊔ d((y⇧ω ⊔ y⇧⋆ * z) * bot) * top"
    by (meson d_isotone mult_left_isotone sup.cobounded1 sup_right_isotone)
  finally show ?thesis
    .
qed

lemma loop_exists:
  "d(L) * ν (λx . y * x ⊔ z) ≤ μ (λx . y * x ⊔ z) ⊔ (ν (λx . y * x ⊔ z) ⊓ L) ⊔ d(ν (λx . y * x ⊔ z) * bot) * top"
  by (simp add: d_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) ⊔ (ν (λx . y * x ⊔ z) ⊓ L))"
  using apx.least_fixpoint_char affine_apx_isotone loop_exists affine_has_greatest_fixpoint affine_has_least_fixpoint affine_isotone nu_below_mu_nu_def nu_below_mu_nu_kappa_mu_nu kappa_mu_nu_def by auto

lemma loop_has_apx_least_fixpoint:
  "apx.has_least_fixpoint (λx . y * x ⊔ z)"
  by (metis apx.has_least_fixpoint_def loop_apx_least_fixpoint)

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

lemma loop_semantics_kappa_mu_nu:
  "κ (λx . y * x ⊔ z) = (y⇧ω ⊓ L) ⊔ y⇧⋆ * z"
proof -
  have "κ (λx . y * x ⊔ z) = y⇧⋆ * z ⊔ ((y⇧ω ⊔ y⇧⋆ * z) ⊓ L)"
    by (metis loop_semantics omega_loop_nu star_loop_mu)
  thus ?thesis
    by (metis sup.absorb2 sup_commute sup_ge2 sup_inf_distrib1)
qed

lemma loop_semantics_kappa_mu_nu_domain:
  "κ (λx . y * x ⊔ z) = d(y⇧ω) * L ⊔ y⇧⋆ * z"
  by (simp add: omega_meet_L loop_semantics_kappa_mu_nu)

lemma loop_semantics_apx_isotone:
  "w ⊑ y ⟹ κ (λx . w * x ⊔ z) ⊑ κ (λx . y * x ⊔ z)"
  by (metis loop_semantics_kappa_mu_nu combined_apx_isotone)

end

end