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