# Theory Recursion

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

section ‹Recursion›

theory Recursion

imports Approximation N_Algebras

begin

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

lemma apx_transitive_2:
assumes "x ⊑ y"
and "y ⊑ z"
shows "x ⊑ z"
proof -
have "C z ≤ C (y ⊔ n(y) * top)"
using assms(2) apx_def le_inf_iff by blast
also have "... = C y ⊔ n(y) * top"
also have "... ≤ x ⊔ n(x) * top ⊔ n(y) * top"
using assms(1) apx_def sup_left_isotone by blast
also have "... = x ⊔ n(x) * top ⊔ n(C y) * top"
also have "... ≤ x ⊔ n(x) * top"
by (metis assms(1) sup_assoc sup_idem sup_right_isotone apx_def mult_left_isotone n_add_n_top n_isotone)
finally show ?thesis
by (smt assms sup_assoc sup_commute apx_def le_iff_sup)
qed

lemma apx_meet_L:
assumes "y ⊑ x"
shows "x ⊓ L ≤ y ⊓ L"
proof -
have "x ⊓ L = C x ⊓ L"
also have "... ≤ (y ⊔ n(y) * top) ⊓ L"
using assms apx_def inf.sup_left_isotone by blast
also have "... = (y ⊓ L) ⊔ (n(y) * top ⊓ L)"
also have "... ≤ (y ⊓ L) ⊔ n(y ⊓ L) * top"
using n_n_meet_L sup_right_isotone by force
finally show ?thesis
by (metis le_iff_sup inf_le2 n_less_eq_char)
qed

text ‹AACP Theorem 4.1›

subclass apx_biorder
apply unfold_locales
apply (metis sup_same_context order.antisym apx_def apx_meet_L relative_equality)
using apx_transitive_2 by blast

lemma sup_apx_left_isotone_2:
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 "C (y ⊔ z) ≤ x ⊔ n(x) * top ⊔ C z"
using assms apx_def inf_sup_distrib1 sup_left_isotone by auto
also have "... ≤ x ⊔ z ⊔ n(x) * top"
using inf.coboundedI1 inf.sup_monoid.add_commute sup.cobounded1 sup.cobounded2 sup_assoc sup_least sup_right_isotone by auto
also have "... ≤ x ⊔ z ⊔ n(x ⊔ z) * top"
using mult_isotone n_left_upper_bound semiring.add_left_mono by force
finally show ?thesis
using 1 apx_def by blast
qed

lemma mult_apx_left_isotone_2:
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 n_L_below_L order_lesseq_imp semiring.add_left_mono by blast
have "C (y * z) = C y * z"
also have "... ≤ x * z ⊔ n(x) * top * z"
by (metis assms apx_def mult_left_isotone mult_right_dist_sup)
also have "... ≤ x * z ⊔ n(x * z) * top"
finally show ?thesis
using 1 by (simp add: apx_def)
qed

lemma mult_apx_right_isotone_2:
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 n_L_split_L semiring.add_left_mono sup_assoc by presburger
finally have 1: "z * x ≤ z * y ⊔ L"
using mult_right_isotone sup.absorb_iff1 by auto
have "C (z * y) ≤ z * C y"
also have "... ≤ z * (x ⊔ n(x) * top)"
using assms apx_def mult_right_isotone by blast
also have "... = z * x ⊔ z * n(x) * top"
also have "... ≤ z * x ⊔ n(z * x) * top"
finally show ?thesis
using 1 apx_def by blast
qed

text ‹AACP Theorem 4.1 and Theorem 4.2›

subclass apx_semiring
apply unfold_locales
apply (simp add: apx_def n_L_below_nL_top sup.absorb2)
using sup_apx_left_isotone_2 apply blast
using mult_apx_left_isotone_2 apply blast

text ‹AACP Theorem 4.2›

lemma meet_L_apx_isotone:
"x ⊑ y ⟹ x ⊓ L ⊑ y ⊓ L"
by (smt (verit) apx_meet_L apx_def inf.cobounded2 inf.left_commute n_L_top_meet_L n_less_eq_char sup.absorb2)

text ‹AACP Theorem 4.2›

lemma n_L_apx_isotone:
assumes "x ⊑ y"
shows "n(x) * L ⊑ n(y) * L"
proof -
have "C (n(y) * L) ≤ n(C y) * L"
also have "... ≤ n(x) * L ⊔ n(n(x) * L) * top"
by (metis assms apx_def n_add_n_top n_galois n_isotone n_n_L)
finally show ?thesis
using apx_def le_inf_iff n_L_decreasing_meet_L sup.absorb2 by auto
qed

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 ≡ C (ν f) ≤ μ f ⊔ (ν f ⊓ L) ⊔ n(ν f) * top"

definition nu_below_mu_nu_2 :: "('a ⇒ 'a) ⇒ bool"
where "nu_below_mu_nu_2 f ≡ C (ν f) ≤ μ f ⊔ (ν f ⊓ L) ⊔ n(μ f ⊔ (ν f ⊓ L)) * 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"

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

lemma l_apx_mu:
"μ f ⊔ (ν f ⊓ L) ⊑ μ f"
proof -
have 1: "μ f ⊔ (ν f ⊓ L) ≤ μ f ⊔ L"
using sup_right_isotone by auto
have "C (μ f) ≤ μ f ⊔ (ν f ⊓ L) ⊔ n(μ f ⊔ (ν f ⊓ L)) * top"
thus ?thesis
using 1 apx_def by blast
qed

text ‹AACP Theorem 4.8 implies Theorem 4.9›

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 "C (ν f) = C (C (ν f))"
by auto
also have "... ≤ C (μ f ⊔ (ν f ⊓ L) ⊔ n(ν f) * top)"
using assms nu_below_mu_nu_def by auto
also have "... = C (μ f ⊔ (ν f ⊓ L)) ⊔ C (n(ν f) * top)"
using inf_sup_distrib1 by auto
also have "... = C (μ f ⊔ (ν f ⊓ L)) ⊔ n(ν f) * top"
also have "... ≤ μ f ⊔ (ν f ⊓ L) ⊔ n(ν f) * top"
using inf_le2 sup_left_isotone by blast
also have "... = μ f ⊔ (ν f ⊓ L) ⊔ n(ν f ⊓ L) * top"
using n_n_meet_L by auto
also have "... ≤ μ f ⊔ (ν f ⊓ L) ⊔ n(μ f ⊔ (ν f ⊓ L)) * top"
using mult_isotone n_right_upper_bound semiring.add_left_mono by auto
finally show ?thesis
qed

text ‹AACP Theorem 4.9 implies Theorem 4.8›

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 "C (ν f) ≤ μ f ⊔ (ν f ⊓ L) ⊔ n(μ f ⊔ (ν f ⊓ L)) * top"
using assms(3) nu_below_mu_nu_2_def by blast
also have "... ≤ μ f ⊔ (ν f ⊓ L) ⊔ n(ν f) * top"
by (metis assms(1,2) order.eq_iff n_n_meet_L n_l_nu)
finally show ?thesis
using nu_below_mu_nu_def by blast
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

text ‹AACP Theorem 4.9 implies Theorem 4.10›

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

text ‹AACP Theorem 4.10 implies Theorem 4.11›

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"
proof (unfold is_apx_meet_def, intro conjI)
show "?l ⊑ μ f"
show "?l ⊑ ν f"
using assms mu_nu_apx_nu_def by blast
show "∀w. w ⊑ μ f ∧ w ⊑ ν f ⟶ w ⊑ ?l"
by (metis apx_meet_L le_inf_iff sup.absorb1 sup_apx_left_isotone)
qed
thus ?thesis
qed

text ‹AACP Theorem 4.11 implies Theorem 4.12›

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 ‹AACP Theorem 4.12 implies Theorem 4.9›

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 ⟶ C (ν f) ≤ ?l ⊔ n(?l) * top"
proof
fix m
show "m ⊑ μ f ∧ m ⊑ ν f ∧ m ≤ ν f ⟶ C (ν f) ≤ ?l ⊔ n(?l) * top"
proof
assume 1: "m ⊑ μ f ∧ m ⊑ ν f ∧ m ≤ ν f"
hence "m ≤ ?l"
by (smt (z3) apx_def sup.left_commute sup_inf_distrib1 sup_left_divisibility)
hence "m ⊔ n(m) * top ≤ ?l ⊔ n(?l) * top"
by (metis sup_mono mult_left_isotone n_isotone)
thus "C (ν f) ≤ ?l ⊔ n(?l) * top"
using 1 apx_def order.trans by blast
qed
qed
thus ?thesis
by (smt (verit, ccfv_threshold) assms apx_meet_below_nu_def apx_meet_same apx_meet_unique is_apx_meet_def nu_below_mu_nu_2_def)
qed

text ‹AACP Theorem 4.5 implies Theorem 4.6›

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 ⟶ C (κ f) ≤ w ⊔ n(w) * top"
by (metis assms(2,3) apx_def inf.sup_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)"
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 ‹AACP Theorem 4.6 implies Theorem 4.12›

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 ‹AACP Theorem 4.12 implies Theorem 4.7›

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"
also have "... ≤ f(?l) ⊔ L"
using assms(3) isotone_def sup_ge1 sup_left_isotone by blast
finally show "?l ≤ f(?l) ⊔ L"
.
qed
have "C (f(?l)) ≤ ?l ⊔ n(?l) * top"
proof -
have "C (f(?l)) ≤ C (f(ν f))"
using assms(1-3) l_below_nu inf.sup_right_isotone isotone_def by blast
also have "... = C (ν f)"
by (metis assms(2) nu_unfold)
also have "... ≤ ?l ⊔ n(?l) * top"
by (metis assms(5) apx_meet_below_nu_nu_below_mu_nu_2 nu_below_mu_nu_2_def)
finally show "C (f(?l)) ≤ ?l ⊔ n(?l) * top"
.
qed
hence 3: "?l ⊑ f(?l)"
using 2 apx_def by blast
have 4: "f(?l) ⊑ μ f"
proof -
have "?l ⊑ μ f"
thus "f(?l) ⊑ μ f"
by (metis assms(1,4) mu_unfold ord.isotone_def)
qed
have "f(?l) ⊑ ν f"
proof -
have "?l ⊑ ν f"
using 1
by (metis apx_meet_below_nu_def assms(5) apx_meet is_apx_meet_def)
thus "f(?l) ⊑ ν f"
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_meet is_apx_meet_def by fastforce
hence 5: "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 6: "f(y) = y"
hence 7: "?l ≤ y ⊔ L"
using assms(1) inf.cobounded2 is_least_fixpoint_def least_fixpoint semiring.add_mono by blast
have "y ≤ ν f"
using 6 assms(2) greatest_fixpoint is_greatest_fixpoint_def by auto
hence "C y ≤ ?l ⊔ n(?l) * top"
using assms(5) apx_meet_below_nu_nu_below_mu_nu_2 inf.sup_right_isotone nu_below_mu_nu_2_def order_trans by blast
thus "?l ⊑ y"
using 7 apx_def by blast
qed
qed
thus ?thesis
using 5 apx.least_fixpoint_same apx.has_least_fixpoint_def apx.is_least_fixpoint_def kappa_mu_nu_def by auto
qed

text ‹AACP Theorem 4.7 implies Theorem 4.5›

lemma kappa_mu_nu_has_apx_least_fixpoint:
"kappa_mu_nu f ⟹ apx.has_least_fixpoint f"

text ‹AACP Theorem 4.8 implies Theorem 4.7›

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

text ‹AACP Theorem 4.7 implies Theorem 4.8›

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_has_apx_least_fixpoint 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 ⊔ n(ν f) * L"

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

definition mu_nu_apx_nu_L :: "('a ⇒ 'a) ⇒ bool"
where "mu_nu_apx_nu_L f ≡ μ f ⊔ n(ν f) * 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 ⊔ n(ν f) * L"

lemma n_below_l:
"x ⊔ n(y) * L ≤ x ⊔ (y ⊓ L)"

lemma n_equal_l:
assumes "nu_below_mu_nu_L f"
shows "μ f ⊔ n(ν f) * L = μ f ⊔ (ν f ⊓ L)"
proof -
have "ν f ⊓ L ≤ (μ f ⊔ n(ν f) * top) ⊓ L"
by (meson assms order.trans inf.boundedI inf.cobounded2 meet_L_below_C nu_below_mu_nu_L_def)
also have "... ≤ μ f ⊔ (n(ν f) * top ⊓ L)"
also have "... ≤ μ f ⊔ n(ν f) * L"
finally have "μ f ⊔ (ν f ⊓ L) ≤ μ f ⊔ n(ν f) * L"
by simp
thus "μ f ⊔ n(ν f) * L = μ f ⊔ (ν f ⊓ L)"
by (meson order.antisym n_below_l)
qed

text ‹AACP Theorem 4.14 implies Theorem 4.8›

lemma nu_below_mu_nu_L_nu_below_mu_nu:
"nu_below_mu_nu_L f ⟹ nu_below_mu_nu f"
by (metis sup_assoc sup_right_top mult_left_dist_sup n_equal_l nu_below_mu_nu_L_def nu_below_mu_nu_def)

text ‹AACP Theorem 4.14 implies Theorem 4.13›

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 force

text ‹AACP Theorem 4.14 implies Theorem 4.15›

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

text ‹AACP Theorem 4.14 implies Theorem 4.16›

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

text ‹AACP Theorem 4.15 implies Theorem 4.14›

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 ⊔ n(ν f) * L"
let ?l = "μ f ⊔ (ν f ⊓ L)"
have "C (ν f) ≤ ?n ⊔ n(?n) * top"
using assms(3) apx_def mu_nu_apx_nu_L_def by blast
also have "... ≤ ?n ⊔ n(?l) * top"
using mult_left_isotone n_L_decreasing_meet_L n_isotone semiring.add_left_mono by auto
also have "... ≤ ?n ⊔ n(ν f) * top"
using assms(1,2) l_below_nu mult_left_isotone n_isotone sup_right_isotone by auto
finally show ?thesis
by (metis sup_assoc sup_right_top mult_left_dist_sup nu_below_mu_nu_L_def)
qed

text ‹AACP Theorem 4.13 implies Theorem 4.15›

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 fastforce

text ‹AACP Theorem 4.16 implies Theorem 4.15›

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_meet_char is_apx_meet_def mu_nu_apx_meet_L_def mu_nu_apx_nu_L_def by fastforce

text ‹AACP Theorem 4.13 implies Theorem 4.14›

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"

proposition nu_below_mu_nu_nu_below_mu_nu_L: "nu_below_mu_nu f ⟶ nu_below_mu_nu_L f" nitpick [expect=genuine,card=3] oops

lemma unfold_fold_1:
"isotone f ⟹ has_least_prefixpoint f ⟹ apx.has_least_fixpoint f ⟹ f(x) ≤ x ⟹ κ f ≤ x ⊔ L"
by (metis sup_left_isotone apx_def has_least_fixpoint_def is_least_prefixpoint_def least_prefixpoint_char least_prefixpoint_fixpoint order_trans pmu_mu kappa_apx_below_mu)

lemma unfold_fold_2:
assumes "isotone f"
and "apx.isotone f"
and "has_least_prefixpoint f"
and "has_greatest_fixpoint f"
and "apx.has_least_fixpoint f"
and "f(x) ≤ x"
and "κ f ⊓ L ≤ x ⊓ L"
shows "κ f ≤ x"
proof -
have "κ f ⊓ L = ν f ⊓ L"
by (smt (z3) apx_meet_L assms(4,5) order.eq_iff inf.cobounded1 kappa_apx_below_nu kappa_below_nu le_inf_iff)
hence "κ f = (κ f ⊓ L) ⊔ μ f"
by (metis assms(1-5) apx_meet_below_nu_kappa_mu_nu has_apx_least_fixpoint_kappa_apx_meet sup_commute least_fixpoint_char least_prefixpoint_fixpoint kappa_apx_meet_apx_meet_below_nu kappa_mu_nu_def)
thus ?thesis
by (metis assms(1,3,6,7) sup_least is_least_prefixpoint_def least_prefixpoint le_inf_iff pmu_mu)
qed

end

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

lemma apx_transitive_2:
assumes "x ⊑ y"
and "y ⊑ z"
shows "x ⊑ z"
proof -
have "z ≤ y ⊔ n(y) * top"
using assms(2) apx_def by auto
also have "... ≤ x ⊔ n(x) * top ⊔ n(y) * top"
using assms(1) apx_def sup_left_isotone by blast
also have "... ≤ x ⊔ n(x) * top"
by (metis assms(1) sup_assoc sup_idem sup_right_isotone apx_def mult_left_isotone n_add_n_top n_isotone)
finally show ?thesis
by (smt assms sup_assoc sup_commute apx_def le_iff_sup)
qed

lemma apx_meet_L:
assumes "y ⊑ x"
shows "x ⊓ L ≤ y ⊓ L"
proof -
have "x ⊓ L ≤ (y ⊓ L) ⊔ (n(y) * top ⊓ L)"
by (metis assms apx_def inf.sup_left_isotone inf_sup_distrib2)
also have "... ≤ (y ⊓ L) ⊔ n(y ⊓ L) * top"
using n_n_meet_L sup_right_isotone by force
finally show ?thesis
by (metis le_iff_sup inf_le2 n_less_eq_char)
qed

text ‹AACP Theorem 4.1›

subclass apx_biorder
apply unfold_locales
using apx_def order.eq_iff n_less_eq_char apply blast
using apx_transitive_2 by blast

lemma sup_apx_left_isotone_2:
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 "y ⊔ z ≤ x ⊔ n(x) * top ⊔ z"
using assms apx_def sup_left_isotone by blast
also have "... ≤ x ⊔ z ⊔ n(x ⊔ z) * top"
by (metis sup_assoc sup_commute sup_right_isotone mult_left_isotone n_right_upper_bound)
finally show ?thesis
using 1 apx_def by auto
qed

lemma mult_apx_left_isotone_2:
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 n_L_below_L order_lesseq_imp semiring.add_left_mono by blast
have "y * z ≤ x * z ⊔ n(x) * top * z"
by (metis assms apx_def mult_left_isotone mult_right_dist_sup)
also have "... ≤ x * z ⊔ n(x * z) * top"
finally show ?thesis
using 1 by (simp add: apx_def)
qed

lemma mult_apx_right_isotone_2:
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 n_L_split_L semiring.add_left_mono sup_assoc by auto
finally have 1: "z * x ≤ z * y ⊔ L"
using mult_right_isotone sup.absorb_iff1 by force
have "z * y ≤ z * (x ⊔ n(x) * top)"
using assms apx_def mult_right_isotone by blast
also have "... = z * x ⊔ z * n(x) * top"