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)"
  by (simp add: apx_n_order_reverse order.antisym)

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 (simp add: apx_def)
  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
    by (simp add: apx_def sup_commute)
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)
  apply (simp add: sup_apx_left_isotone)
  apply (simp add: mult_apx_left_isotone)
  by (simp add: mult_apx_right_isotone)

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"
  by (simp add: mu_below_nu n_L_decreasing)

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)
    apply (simp add: assms(1,2) l_apx_mu)
    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
    by (simp add: apx_meet_char mu_nu_apx_meet_def)
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"
  by (simp add: kappa_mu_nu_ni_kappa_mu_nu nu_below_mu_nu_kappa_mu_nu)

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"
    by (simp add: circ_plus_same n_circ_left_unfold)
  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"
    by (simp add: mult_left_isotone n_star_below_n_omega)
  have "...  x * n(xω) * top"
    by (simp add: star_n_omega_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