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"
    by (simp add: C_n_mult_closed inf_sup_distrib1)
  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"
    by (simp add: n_C)
  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"
    by (simp add: inf.left_commute inf.sup_monoid.add_assoc n_L_top_meet_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)"
    by (simp add: 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
  apply (simp add: apx_def inf.coboundedI2)
  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"
    by (simp add: n_L_T_meet_mult)
  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"
    by (simp add: n_top_split)
  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"
    by (simp add: n_L_T_meet_mult n_L_T_meet_mult_propagate)
  also have "... ≤ z * (x ⊔ n(x) * top)"
    using assms apx_def mult_right_isotone by blast
  also have "... = z * x ⊔ z * n(x) * top"
    by (simp add: mult_left_dist_sup mult_assoc)
  also have "... ≤ z * x ⊔ n(z * x) * top"
    by (simp add: n_split_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
  by (simp add: mult_apx_right_isotone_2)

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"
    by (simp add: n_C)
  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"
  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.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"
    by (simp add: le_supI1)
  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"
    by (simp add: C_n_mult_closed)
  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
    by (simp add: nu_below_mu_nu_2_def)
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"
      by (simp add: l_apx_mu)
    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
    by (simp add: apx_meet_char mu_nu_apx_meet_def)
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"
      by (simp add: assms(1) mu_unfold)
    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"
      by (simp add: l_apx_mu)
    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"
  by (simp add: kappa_mu_nu_def)

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)"
  using n_L_decreasing_meet_L semiring.add_left_mono by auto

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)"
    by (simp add: inf.coboundedI2 inf.sup_monoid.add_commute inf_sup_distrib1)
  also have "... ≤ μ f ⊔ n(ν f) * L"
    by (simp add: n_T_meet_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"
  by (simp add: kappa_mu_nu_L_mu_nu_apx_nu_L mu_nu_apx_nu_L_nu_below_mu_nu_L)

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
  apply (simp add: apx_def)
  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"
    by (simp add: n_top_split)
  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"
    by (simp add: mult_left_dist_sup mult_assoc)
  also have "... ≤ z * x ⊔ n(z * x) * top"
    by (simp add: n_split_top)
  finally show ?thesis
    using 1 by (simp add: apx_def)
qed

end

end