# Theory Recursion_Strict

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

section ‹Strict Recursion›

theory Recursion_Strict

imports N_Semirings Approximation

begin

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

lemma apx_n_order_reverse:
"y ⊑ x ⟹ n(x) ≤ n(y)"
by (metis apx_def le_iff_sup n_sup_left_absorb_mult n_dist_sup n_export)

lemma apx_n_order:
"x ⊑ y ⟹ y ⊑ x ⟹ n(x) = n(y)"

lemma apx_transitive:
assumes "x ⊑ y"
and "y ⊑ z"
shows "x ⊑ z"
proof -
have "n(y) * L ≤ n(x) * L"
by (simp add: apx_n_order_reverse assms(1) mult_left_isotone)
hence 1: "x ≤ z ⊔ n(x) * L"
by (smt assms sup_assoc sup_right_divisibility apx_def le_iff_sup)
have "z ≤ x ⊔ n(x) * top ⊔ n(x ⊔ n(x) * top) * top"
by (smt (verit) assms sup_left_isotone order_refl sup_assoc sup_mono apx_def mult_left_isotone n_isotone order_trans)
also have "... = x ⊔ n(x) * top"
by (simp add: n_dist_sup n_export n_sup_left_absorb_mult)
finally show ?thesis
using 1 by (simp add: apx_def)
qed

text ‹Theorem 16.1›

subclass apx_biorder
apply unfold_locales
apply (smt (verit) order.antisym le_sup_iff apx_def eq_refl le_iff_sup n_galois apx_n_order)
using apx_transitive by blast

lemma sup_apx_left_isotone:
assumes "x ⊑ y"
shows "x ⊔ z ⊑ y ⊔ z"
proof -
have "x ≤ y ⊔ n(x) * L ∧ y ≤ x ⊔ n(x) * top"
using assms apx_def by auto
hence "z ⊔ x ≤ z ⊔ y ⊔ n(z ⊔ x) * L ∧ z ⊔ y ≤ z ⊔ x ⊔ n(z ⊔ x) * top"
by (metis sup_assoc sup_right_isotone mult_right_sub_dist_sup_right n_dist_sup order_trans)
thus ?thesis
qed

lemma mult_apx_left_isotone:
assumes "x ⊑ y"
shows "x * z ⊑ y * z"
proof -
have "x ≤ y ⊔ n(x) * L"
using assms apx_def by auto
hence "x * z ≤ y * z ⊔ n(x) * L"
by (smt (verit, ccfv_threshold) L_left_zero mult_left_isotone semiring.distrib_right mult_assoc)
hence 1: "x * z ≤ y * z ⊔ n(x * z) * L"
by (meson mult_left_isotone n_mult_left_upper_bound order_lesseq_imp sup_mono)
have "y * z ≤ x * z ⊔ n(x) * top * z"
by (metis assms apx_def mult_left_isotone mult_right_dist_sup)
hence "y * z ≤ x * z ⊔ n(x * z) * top"
using mult_isotone n_mult_left_upper_bound order.trans sup_right_isotone top_greatest mult_assoc by presburger
thus ?thesis
using 1 by (simp add: apx_def)
qed

lemma mult_apx_right_isotone:
assumes "x ⊑ y"
shows "z * x ⊑ z * y"
proof -
have "x ≤ y ⊔ n(x) * L"
using assms apx_def by auto
hence 1: "z * x ≤ z * y ⊔ n(z * x) * L"
by (smt sup_assoc sup_ge1 sup_bot_right mult_assoc mult_left_dist_sup mult_right_isotone n_L_split)
have "y ≤ x ⊔ n(x) * top"
using assms apx_def by auto
hence "z * y ≤ z * x ⊔ z * n(x) * top"
by (smt mult_assoc mult_left_dist_sup mult_right_isotone)
also have "... ≤ z * x ⊔ n(z * x) * top"
by (smt (verit) sup_assoc le_supI le_sup_iff sup_ge1 sup_bot_right mult_left_dist_sup n_L_split n_top_split order_trans)
finally show ?thesis
using 1 by (simp add: apx_def)
qed

text ‹Theorem 16.1 and Theorem 16.2›

subclass apx_semiring
apply unfold_locales
apply (metis sup_right_top sup_ge2 apx_def mult_left_one n_L top_greatest)

text ‹Theorem 16.2›

lemma ni_apx_isotone:
"x ⊑ y ⟹ ni(x) ⊑ ni(y)"
using apx_n_order_reverse apx_def le_supI1 n_ni ni_def ni_n_order by force

text ‹Theorem 17›

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

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

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

lemma l_below_nu:
"has_least_fixpoint f ⟹ has_greatest_fixpoint f ⟹ μ f ⊔ n(ν f) * L ≤ ν f"

lemma n_l_nu:
"has_least_fixpoint f ⟹ has_greatest_fixpoint f ⟹ n(μ f ⊔ n(ν f) * L) = n(ν f)"
by (metis le_iff_sup mu_below_nu n_dist_sup n_n_L)

lemma l_apx_mu:
"has_least_fixpoint f ⟹ has_greatest_fixpoint f ⟹ μ f ⊔ n(ν f) * L ⊑ μ f"
by (simp add: apx_def le_supI1 n_l_nu)

text ‹Theorem 17.4 implies Theorem 17.5›

lemma nu_below_mu_nu_mu_nu_apx_nu:
"has_least_fixpoint f ⟹ has_greatest_fixpoint f ⟹ nu_below_mu_nu f ⟹ mu_nu_apx_nu f"
by (smt (z3) l_below_nu apx_def le_sup_iff sup.absorb2 sup_commute sup_monoid.add_assoc mu_nu_apx_nu_def n_l_nu nu_below_mu_nu_def)

text ‹Theorem 17.5 implies Theorem 17.6›

lemma mu_nu_apx_nu_mu_nu_apx_meet:
assumes "has_least_fixpoint f"
and "has_greatest_fixpoint f"
and "mu_nu_apx_nu f"
shows "mu_nu_apx_meet f"
proof -
let ?l = "μ f ⊔ n(ν f) * L"
have "is_apx_meet (μ f) (ν f) ?l"
apply (unfold is_apx_meet_def, intro conjI)
using assms(3) mu_nu_apx_nu_def apply blast
by (meson assms(1,2) l_below_nu apx_def order_trans sup_ge1 sup_left_isotone)
thus ?thesis
qed

text ‹Theorem 17.6 implies Theorem 17.7›

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 ‹Theorem 17.7 implies Theorem 17.4›

lemma apx_meet_below_nu_nu_below_mu_nu:
assumes "apx_meet_below_nu f"
shows "nu_below_mu_nu f"
proof -
have "∀m . m ⊑ μ f ∧ m ⊑ ν f ∧ m ≤ ν f ⟶ ν f ≤ μ f ⊔ n(m) * top"
by (smt (verit) sup_assoc sup_left_isotone sup_right_top apx_def mult_left_dist_sup order_trans)
thus ?thesis
by (smt (verit) assms sup_right_isotone apx_greatest_lower_bound apx_meet_below_nu_def apx_reflexive mult_left_isotone n_isotone nu_below_mu_nu_def order_trans)
qed

text ‹Theorem 17.1 implies Theorem 17.2›

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 "∀w . w ⊑ μ f ∧ w ⊑ ν f ⟶ w ⊑ κ f"
by (meson assms apx_def order.trans kappa_below_nu mu_below_kappa semiring.add_right_mono)
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 ‹Theorem 17.2 implies Theorem 17.7›

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 ‹Theorem 17.7 implies Theorem 17.3›

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 ⊔ n(ν f) * L"
let ?m = "μ f △ ν f"
have 1: "?l ⊑ ν f"
using apx_meet_below_nu_nu_below_mu_nu assms(1,2,5) mu_nu_apx_nu_def nu_below_mu_nu_mu_nu_apx_nu by blast
hence 2: "?m = ?l"
using assms(1,2) mu_nu_apx_meet_def mu_nu_apx_nu_def mu_nu_apx_nu_mu_nu_apx_meet by blast
have "μ f ≤ f(?l)"
by (metis assms(1,3) isotone_def mu_unfold sup_ge1)
hence 3: "?l ≤ f(?l) ⊔ n(?l) * L"
using assms(1,2) semiring.add_right_mono n_l_nu by auto
have "f(?l) ≤ f(ν f)"
using assms(1-3) l_below_nu isotone_def by blast
also have "... ≤ ?l ⊔ n(?l) * top"
using 1 by (metis assms(2) apx_def nu_unfold)
finally have 4: "?l ⊑ f(?l)"
using 3 apx_def by blast
have 5: "f(?l) ⊑ μ f"
by (metis assms(1,2,4) apx.isotone_def is_least_fixpoint_def least_fixpoint l_apx_mu)
have "f(?l) ⊑ ν f"
using 1 by (metis assms(2,4) apx.isotone_def greatest_fixpoint is_greatest_fixpoint_def)
hence "f(?l) ⊑ ?l"
using 2 5 apx_meet_below_nu_def assms(5) apx_greatest_lower_bound by fastforce
hence "f(?l) = ?l"
using 4 by (simp add: apx.order.antisym)
thus ?thesis
using 1 by (smt (verit, del_insts) assms(1,2) sup_left_isotone apx_antisymmetric apx_def apx.least_fixpoint_char greatest_fixpoint apx.is_least_fixpoint_def is_greatest_fixpoint_def is_least_fixpoint_def least_fixpoint n_l_nu order_trans kappa_mu_nu_def)
qed

text ‹Theorem 17.3 implies Theorem 17.1›

lemma kappa_mu_nu_has_apx_least_fixpoint:
"kappa_mu_nu f ⟹ apx.has_least_fixpoint f"
using kappa_mu_nu_def by auto

text ‹Theorem 17.4 implies Theorem 17.3›

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_mu_nu_apx_nu by blast

text ‹Theorem 17.3 implies Theorem 17.4›

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

definition kappa_mu_nu_ni :: "('a ⇒ 'a) ⇒ bool"
where "kappa_mu_nu_ni f ≡ apx.has_least_fixpoint f ∧ κ f = μ f ⊔ ni(ν f)"

lemma kappa_mu_nu_ni_kappa_mu_nu:
"kappa_mu_nu_ni f ⟷ kappa_mu_nu f"
by (simp add: kappa_mu_nu_def kappa_mu_nu_ni_def ni_def)

lemma nu_below_mu_nu_kappa_mu_nu_ni:
"has_least_fixpoint f ⟹ has_greatest_fixpoint f ⟹ isotone f ⟹ apx.isotone f ⟹ nu_below_mu_nu f ⟹ kappa_mu_nu_ni f"

lemma kappa_mu_nu_ni_nu_below_mu_nu:
"has_least_fixpoint f ⟹ has_greatest_fixpoint f ⟹ kappa_mu_nu_ni f ⟹ nu_below_mu_nu f"
using kappa_mu_nu_ni_kappa_mu_nu kappa_mu_nu_nu_below_mu_nu by blast

end

class itering_apx = n_itering + semiring_apx
begin

text ‹Theorem 16.3›

lemma circ_apx_isotone:
assumes "x ⊑ y"
shows "x⇧∘ ⊑ y⇧∘"
proof -
have 1: "x ≤ y ⊔ n(x) * L ∧ y ≤ x ⊔ n(x) * top"
using assms apx_def by auto
hence "y⇧∘ ≤ x⇧∘ ⊔ x⇧∘ * n(x) * top"
by (metis circ_isotone circ_left_top circ_unfold_sum mult_assoc)
also have "... ≤ x⇧∘ ⊔ n(x⇧∘ * x) * top"
by (smt le_sup_iff n_isotone n_top_split order_refl order_trans right_plus_below_circ zero_right_mult_decreasing)
also have "... ≤ x⇧∘ ⊔ n(x⇧∘) * top"
finally have 2: "y⇧∘ ≤ x⇧∘ ⊔ n(x⇧∘) * top"
.
have "x⇧∘ ≤ y⇧∘ ⊔ y⇧∘ * n(x) * L"
using 1 by (metis L_left_zero circ_isotone circ_unfold_sum mult_assoc)
also have "... = y⇧∘ ⊔ n(y⇧∘ * x) * L"
by (metis sup_assoc sup_bot_right mult_assoc mult_zero_sup_circ_2 n_L_split n_mult_right_bot)
also have "... ≤ y⇧∘ ⊔ n(x⇧∘ * x) * L ⊔ n(x⇧∘) * n(top * x) * L"
using 2 by (metis sup_assoc sup_right_isotone mult_assoc mult_left_isotone mult_right_dist_sup n_dist_sup n_export n_isotone)
finally have "x⇧∘ ≤ y⇧∘ ⊔ n(x⇧∘) * L"
by (metis sup_assoc circ_plus_same n_sup_left_absorb_mult n_circ_left_unfold n_dist_sup n_export ni_def ni_dist_sup)
thus ?thesis
using 2 by (simp add: apx_def)
qed

end

class omega_algebra_apx = n_omega_algebra_2 + semiring_apx

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

sublocale omega_algebra_apx < nL_omega: itering_apx where circ = Omega ..

context omega_algebra_apx
begin

text ‹Theorem 16.4›

lemma omega_apx_isotone:
assumes "x ⊑ y"
shows "x⇧ω ⊑ y⇧ω"
proof -
have 1: "x ≤ y ⊔ n(x) * L ∧ y ≤ x ⊔ n(x) * top"
using assms apx_def by auto
hence "y⇧ω ≤ x⇧⋆ * n(x) * top * (x⇧⋆ * n(x) * top)⇧ω ⊔ x⇧ω ⊔ x⇧⋆ * n(x) * top * (x⇧⋆ * n(x) * top)⇧⋆ * x⇧ω"
by (smt sup_assoc mult_assoc mult_left_one mult_right_dist_sup omega_decompose omega_isotone omega_unfold star_left_unfold_equal)
also have "... ≤ x⇧⋆ * n(x) * top ⊔ x⇧ω ⊔ x⇧⋆ * n(x) * top * (x⇧⋆ * n(x) * top)⇧⋆ * x⇧ω"
using mult_top_omega omega_unfold sup_left_isotone by auto
also have "... = x⇧⋆ * n(x) * top ⊔ x⇧ω"
by (smt (z3) mult_left_dist_sup sup_assoc sup_commute sup_left_top mult_assoc)
also have "... ≤ n(x⇧⋆ * x) * top ⊔ x⇧⋆ * bot ⊔ x⇧ω"
using n_top_split semiring.add_left_mono sup_commute by fastforce
also have "... ≤ n(x⇧⋆ * x) * top ⊔ x⇧ω"
using semiring.add_right_mono star_bot_below_omega sup_commute by fastforce
finally have 2: "y⇧ω ≤ x⇧ω ⊔ n(x⇧ω) * top"
by (metis sup_commute sup_right_isotone mult_left_isotone n_star_below_n_omega n_star_left_unfold order_trans star.circ_plus_same)
have "x⇧ω ≤ (y ⊔ n(x) * L)⇧ω"
using 1 by (simp add: omega_isotone)
also have "... = y⇧⋆ * n(x) * L * (y⇧⋆ * n(x) * L)⇧ω ⊔ y⇧ω ⊔ y⇧⋆ * n(x) * L * (y⇧⋆ * n(x) * L)⇧⋆ * y⇧ω"
by (smt sup_assoc mult_assoc mult_left_one mult_right_dist_sup omega_decompose omega_isotone omega_unfold star_left_unfold_equal)
also have "... = y⇧⋆ * n(x) * L ⊔ y⇧ω"
using L_left_zero sup_assoc sup_monoid.add_commute mult_assoc by force
also have "... ≤ y⇧ω ⊔ y⇧⋆ * bot ⊔ n(y⇧⋆ * x) * L"
by (simp add: n_L_split sup_assoc sup_commute)
also have "... ≤ y⇧ω ⊔ n(x⇧⋆ * x) * L ⊔ n(x⇧⋆) * n(top * x) * L"
using 1 by (metis sup_right_isotone sup_bot_right apx_def mult_assoc mult_left_dist_sup mult_left_isotone mult_right_dist_sup n_dist_sup n_export n_isotone star.circ_apx_isotone star_mult_omega sup_assoc)
finally have "x⇧ω ≤ y⇧ω ⊔ n(x⇧ω) * L"
by (smt (verit, best) le_supE sup.orderE sup_commute sup_assoc sup_isotone mult_right_dist_sup n_sup_left_absorb_mult n_star_left_unfold ni_def ni_star_below_ni_omega order_refl order_trans star.circ_plus_same)
thus ?thesis
using 2 by (simp add: apx_def)
qed

end

class omega_algebra_apx_extra = omega_algebra_apx +
assumes n_split_omega: "x⇧ω ≤ x⇧⋆ * bot ⊔ n(x⇧ω) * top"
begin

lemma omega_n_star:
"x⇧ω ⊔ n(x⇧⋆) * top ≤ x⇧⋆ * n(x⇧ω) * top"
proof -
have 1: "n(x⇧⋆) * top ≤ n(x⇧ω) * top"
have "... ≤ x⇧⋆ * n(x⇧ω) * top"
thus ?thesis
using 1 by (metis le_sup_iff n_split_omega order_trans star_n_omega_top)
qed

lemma n_omega_zero:
"n(x⇧ω) = bot ⟷ n(x⇧⋆) = bot ∧ x⇧ω ≤ x⇧⋆ * bot"
by (metis sup_bot_right order.eq_iff mult_left_zero n_mult_bot n_split_omega star_bot_below_omega)

lemma n_split_nu_mu:
"y⇧ω ⊔ y⇧⋆ * z ≤ y⇧⋆ * z ⊔ n(y⇧ω ⊔ y⇧⋆ * z) * top"
proof -
have "y⇧ω ≤ y⇧⋆ * bot ⊔ n(y⇧ω ⊔ y⇧⋆ * z) * top"
by (smt sup_ge1 sup_right_isotone mult_left_isotone n_isotone n_split_omega order_trans)
also have "... ≤ y⇧⋆ * z ⊔ n(y⇧ω ⊔ y⇧⋆ * z) * top"
using nL_star.star_zero_below_circ_mult sup_left_isotone by auto
finally show ?thesis
by simp
qed

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

lemma loop_has_apx_least_fixpoint:
"apx.has_least_fixpoint (λx . y * x ⊔ z)"
using affine_apx_isotone affine_has_greatest_fixpoint affine_has_least_fixpoint affine_isotone kappa_mu_nu_def nu_below_mu_nu_def nu_below_mu_nu_kappa_mu_nu loop_exists by auto

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

lemma loop_apx_least_fixpoint_ni:
"apx.is_least_fixpoint (λx . y * x ⊔ z) (μ (λx . y * x ⊔ z) ⊔ ni(ν (λx . y * x ⊔ z)))"
using ni_def loop_apx_least_fixpoint by auto

lemma loop_semantics_ni:
"κ (λx . y * x ⊔ z) = μ (λx . y * x ⊔ z) ⊔ ni(ν (λx . y * x ⊔ z))"
using ni_def loop_semantics by auto

text ‹Theorem 18›

lemma loop_semantics_kappa_mu_nu:
"κ (λx . y * x ⊔ z) = n(y⇧ω) * L ⊔ y⇧⋆ * z"
proof -
have "κ (λx . y * x ⊔ z) = y⇧⋆ * z ⊔ n(y⇧ω ⊔ y⇧⋆ * z) * L"
by (metis loop_semantics omega_loop_nu star_loop_mu)
thus ?thesis
by (smt sup_assoc sup_commute le_iff_sup mult_right_dist_sup n_L_decreasing n_dist_sup)
qed

end

class omega_algebra_apx_extra_2 = omega_algebra_apx +
assumes omega_n_star: "x⇧ω ≤ x⇧⋆ * n(x⇧ω) * top"
begin

subclass omega_algebra_apx_extra
apply unfold_locales
using omega_n_star star_n_omega_top by auto

end

end

```