# 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_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"
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_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"
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

```