Theory Akra_Bazzi.Akra_Bazzi_Method

(*
  File:   Akra_Bazzi_Method.thy
  Author: Manuel Eberl <manuel@pruvisto.org>

  Provides the "master_theorem" and "akra_bazzi_termination" proof methods.
*)
section ‹The proof methods›
subsection ‹Master theorem and termination›
theory Akra_Bazzi_Method
imports 
  Complex_Main
  Akra_Bazzi
  Master_Theorem
  Eval_Numeral
begin

lemma landau_symbol_ge_3_cong:
  assumes "landau_symbol L L' Lr"
  assumes "⋀x::'a::linordered_semidom. x ≥ 3 ⟹ f x = g x"
  shows   "L at_top (f) = L at_top (g)"
apply (rule landau_symbol.cong[OF assms(1)])
apply (subst eventually_at_top_linorder, rule exI[of _ 3], simp add: assms(2))
done

lemma exp_1_lt_3: "exp (1::real) < 3"
proof-
  from Taylor_up[of 3 "λ_. exp" exp 0 1 0] 
    obtain t :: real where "t > 0" "t < 1" "exp 1 = 5/2 + exp t / 6" by (auto simp: eval_nat_numeral)
  note this(3)
  also from ‹t < 1› have "exp t < exp 1" by simp
  finally show "exp (1::real) < 3" by (simp add: field_simps)
qed

lemma ln_ln_pos:
  assumes "(x::real) ≥ 3"
  shows   "ln (ln x) > 0"
proof (subst ln_gt_zero_iff)
  from assms exp_1_lt_3 have "ln x > ln (exp 1)" by (intro ln_mono_strict) simp_all
  thus "ln x > 0" "ln x > 1" by simp_all
qed

definition akra_bazzi_terms where
  "akra_bazzi_terms x⇩0 x⇩1 bs ts = (∀i<length bs. akra_bazzi_term x⇩0 x⇩1 (bs!i) (ts!i))"

lemma akra_bazzi_termsI:
  "(⋀i. i < length bs ⟹ akra_bazzi_term x⇩0 x⇩1 (bs!i) (ts!i)) ⟹ akra_bazzi_terms x⇩0 x⇩1 bs ts"
  unfolding akra_bazzi_terms_def by blast

lemma master_theorem_functionI:
  assumes "∀x∈{x⇩0..<x⇩1}. f x ≥ 0"
  assumes "∀x≥x⇩1. f x = g x + (∑i<k. as ! i * f ((ts ! i) x))"
  assumes "∀x≥x⇩1. g x ≥ 0"
  assumes "∀a∈set as. a ≥ 0"
  assumes "list_ex (λa. a > 0) as"
  assumes "∀b∈set bs. b ∈ {0<..<1}"
  assumes "k ≠ 0"
  assumes "length as = k"
  assumes "length bs = k"
  assumes "length ts = k"
  assumes "akra_bazzi_terms x⇩0 x⇩1 bs ts"
  shows "master_theorem_function x⇩0 x⇩1 k as bs ts f g"
using assms unfolding akra_bazzi_terms_def by unfold_locales (auto simp: list_ex_iff)

lemma akra_bazzi_term_measure:
  " x ≥ x⇩1 ⟹ akra_bazzi_term 0 x⇩1 b t ⟹ (t x, x) ∈ Wellfounded.measure (λn::nat. n)"
  " x > x⇩1 ⟹ akra_bazzi_term 0 (Suc x⇩1) b t ⟹ (t x, x) ∈ Wellfounded.measure (λn::nat. n)"
  unfolding akra_bazzi_term_def by auto

lemma measure_prod_conv: 
  "((a, b), (c, d)) ∈ Wellfounded.measure (λx. t (fst x)) ⟷ (a, c) ∈ Wellfounded.measure t"
  "((e, f), (g, h)) ∈ Wellfounded.measure (λx. t (snd x)) ⟷ (f, h) ∈ Wellfounded.measure t"
by simp_all

lemmas measure_prod_conv' = measure_prod_conv[where t = "λx. x"]

lemma akra_bazzi_termination_simps:
  fixes x :: nat
  shows "a * real x / b = a/b * real x" "real x / b = 1/b * real x"
  by simp_all

lemma akra_bazzi_params_nonzeroI:
  "length as = length bs ⟹  
   (∀a∈set as. a ≥ 0) ⟹ (∀b∈set bs. b ∈ {0<..<1}) ⟹ (∃a∈set as. a > 0) ⟹
   akra_bazzi_params_nonzero (length as) as bs" by (unfold_locales, simp_all) []

lemmas akra_bazzi_p_rel_intros = 
  akra_bazzi_params_nonzero.p_lessI[rotated, OF _ akra_bazzi_params_nonzeroI]
  akra_bazzi_params_nonzero.p_greaterI[rotated, OF _ akra_bazzi_params_nonzeroI]
  akra_bazzi_params_nonzero.p_leI[rotated, OF _ akra_bazzi_params_nonzeroI]
  akra_bazzi_params_nonzero.p_geI[rotated, OF _ akra_bazzi_params_nonzeroI]
  akra_bazzi_params_nonzero.p_boundsI[rotated, OF _ akra_bazzi_params_nonzeroI]
  akra_bazzi_params_nonzero.p_boundsI'[rotated, OF _ akra_bazzi_params_nonzeroI]

lemma eval_length: "length [] = 0" "length (x # xs) = Suc (length xs)" by simp_all

lemma eval_akra_bazzi_sum:
  "(∑i<0. as!i * bs!i powr x) = 0"
  "(∑i<Suc 0. (a#as)!i * (b#bs)!i powr x) = a * b powr x"
  "(∑i<Suc k. (a#as)!i * (b#bs)!i powr x) = a * b powr x + (∑i<k. as!i * bs!i powr x)"
  apply simp
  apply simp
  apply (induction k arbitrary: a as b bs)
  apply simp_all
  done

lemma eval_akra_bazzi_sum':
  "(∑i<0. as!i * f ((ts!i) x)) = 0"
  "(∑i<Suc 0. (a#as)!i * f (((t#ts)!i) x)) = a * f (t x)"
  "(∑i<Suc k. (a#as)!i * f (((t#ts)!i) x)) = a * f (t x) + (∑i<k. as!i * f ((ts!i) x))"
  apply simp
  apply simp
  apply (induction k arbitrary: a as t ts)
  apply (simp_all add: algebra_simps)
  done

lemma akra_bazzi_termsI':
  "akra_bazzi_terms x⇩0 x⇩1 [] []"
  "akra_bazzi_term x⇩0 x⇩1 b t ⟹ akra_bazzi_terms x⇩0 x⇩1 bs ts ⟹ akra_bazzi_terms x⇩0 x⇩1 (b#bs) (t#ts)"
unfolding akra_bazzi_terms_def using less_Suc_eq_0_disj by auto

lemma ball_set_intros: "(∀x∈set []. P x)" "P x ⟹ (∀x∈set xs. P x) ⟹ (∀x∈set (x#xs). P x)"
  by auto

lemma ball_set_simps: "(∀x∈set []. P x) = True" "(∀x∈set (x#xs). P x) = (P x ∧ (∀x∈set xs. P x))"
  by auto

lemma bex_set_simps: "(∃x∈set []. P x) = False" "(∃x∈set (x#xs). P x) = (P x ∨ (∃x∈set xs. P x))"
  by auto

lemma eval_akra_bazzi_le_list_ex:
  "list_ex P (x#y#xs) ⟷ P x ∨ list_ex P (y#xs)"
  "list_ex P [x] ⟷ P x"
  "list_ex P [] ⟷ False"
  by (auto simp: list_ex_iff)

lemma eval_akra_bazzi_le_sum_list:
  "x ≤ sum_list [] ⟷ x ≤ 0" "x ≤ sum_list (y#ys) ⟷ x ≤ y + sum_list ys"
  "x ≤ z + sum_list [] ⟷ x ≤ z" "x ≤ z + sum_list (y#ys) ⟷ x ≤ z + y + sum_list ys"
  by (simp_all add: algebra_simps)

lemma atLeastLessThanE: "x ∈ {a..<b} ⟹ (x ≥ a ⟹ x < b ⟹ P) ⟹ P" by simp

lemma master_theorem_preprocess:
  "Θ(λn::nat. 1) = Θ(λn::nat. real n powr 0)"
  "Θ(λn::nat. real n) = Θ(λn::nat. real n powr 1)"
  "O(λn::nat. 1) = O(λn::nat. real n powr 0)"
  "O(λn::nat. real n) = O(λn::nat. real n powr 1)"

  "Θ(λn::nat. ln (ln (real n))) = Θ(λn::nat. real n powr 0 * ln (ln (real n)))"
  "Θ(λn::nat. real n * ln (ln (real n))) = Θ(λn::nat. real n powr 1 * ln (ln (real n)))"

  "Θ(λn::nat. ln (real n)) = Θ(λn::nat. real n powr 0 * ln (real n) powr 1)"
  "Θ(λn::nat. real n * ln (real n)) = Θ(λn::nat. real n powr 1 * ln (real n) powr 1)"
  "Θ(λn::nat. real n powr p * ln (real n)) = Θ(λn::nat. real n powr p * ln (real n) powr 1)"
  "Θ(λn::nat. ln (real n) powr p') = Θ(λn::nat. real n powr 0 * ln (real n) powr p')"
  "Θ(λn::nat. real n * ln (real n) powr p') = Θ(λn::nat. real n powr 1 * ln (real n) powr p')"
apply (simp_all)
apply (simp_all cong: landau_symbols[THEN landau_symbol_ge_3_cong])?
done

lemma akra_bazzi_term_imp_size_less:
  "x⇩1 ≤ x ⟹ akra_bazzi_term 0 x⇩1 b t ⟹ size (t x) < size x" 
  "x⇩1 < x ⟹ akra_bazzi_term 0 (Suc x⇩1) b t ⟹ size (t x) < size x" 
  by (simp_all add: akra_bazzi_term_imp_less)

definition "CLAMP (f :: nat ⇒ real) x = (if x < 3 then 0 else f x)"
definition "CLAMP' (f :: nat ⇒ real) x = (if x < 3 then 0 else f x)"
definition "MASTER_BOUND a b c x = real x powr a * ln (real x) powr b * ln (ln (real x)) powr c"
definition "MASTER_BOUND' a b x = real x powr a * ln (real x) powr b"
definition "MASTER_BOUND'' a x = real x powr a"

lemma ln_1_imp_less_3:
  "ln x = (1::real) ⟹ x < 3"
proof-
  assume "ln x = 1"
  also have "(1::real) ≤ ln (exp 1)" by simp
  finally have "ln x ≤ ln (exp 1)" by simp
  hence "x ≤ exp 1"
    by (cases "x > 0") (force simp del: ln_exp simp add: not_less intro: order.trans)+
  also have "... < 3" by (rule exp_1_lt_3)
  finally show ?thesis .
qed

lemma ln_1_imp_less_3': "ln (real (x::nat)) = 1 ⟹ x < 3" by (drule ln_1_imp_less_3) simp

lemma ln_ln_nonneg: "x ≥ (3::real) ⟹ ln (ln x) ≥ 0" using ln_ln_pos[of "x"] by simp
lemma ln_ln_nonneg': "x ≥ (3::nat) ⟹ ln (ln (real x)) ≥ 0" using ln_ln_pos[of "real x"] by simp

lemma MASTER_BOUND_postproc:
  "CLAMP (MASTER_BOUND' a 0) = CLAMP (MASTER_BOUND'' a)"
  "CLAMP (MASTER_BOUND' a 1) = CLAMP (λx. CLAMP (MASTER_BOUND'' a) x * CLAMP (λx. ln (real x)) x)"
  "CLAMP (MASTER_BOUND' a (numeral n)) = 
       CLAMP (λx. CLAMP (MASTER_BOUND'' a) x * CLAMP (λx. ln (real x) ^ numeral n) x)"
  "CLAMP (MASTER_BOUND' a (-1)) =
       CLAMP (λx. CLAMP (MASTER_BOUND'' a) x / CLAMP (λx. ln (real x)) x)"
  "CLAMP (MASTER_BOUND' a (-numeral n)) = 
       CLAMP (λx. CLAMP (MASTER_BOUND'' a) x / CLAMP (λx. ln (real x) ^ numeral n) x)"
  "CLAMP (MASTER_BOUND' a b) = 
       CLAMP (λx. CLAMP (MASTER_BOUND'' a) x * CLAMP (λx. ln (real x) powr b) x)"

  "CLAMP (MASTER_BOUND'' 0) = CLAMP (λx. 1)"
  "CLAMP (MASTER_BOUND'' 1) = CLAMP (λx. (real x))"
  "CLAMP (MASTER_BOUND'' (numeral n)) = CLAMP (λx. (real x) ^ numeral n)"
  "CLAMP (MASTER_BOUND'' (-1)) = CLAMP (λx. 1 / (real x))"
  "CLAMP (MASTER_BOUND'' (-numeral n)) = CLAMP (λx. 1 / (real x) ^ numeral n)"
  "CLAMP (MASTER_BOUND'' a) = CLAMP (λx. (real x) powr a)"

  and MASTER_BOUND_UNCLAMP:
  "CLAMP (λx. CLAMP f x * CLAMP g x) = CLAMP (λx. f x * g x)"
  "CLAMP (λx. CLAMP f x / CLAMP g x) = CLAMP (λx. f x / g x)"
  "CLAMP (CLAMP f) = CLAMP f"
  unfolding CLAMP_def[abs_def] MASTER_BOUND'_def[abs_def] MASTER_BOUND''_def[abs_def]
  by (simp_all add: powr_minus divide_inverse fun_eq_iff)

  
context
begin

private lemma CLAMP_: 
  "landau_symbol L L' Lr ⟹ L at_top (f::nat ⇒ real) ≡ L at_top (λx. CLAMP f x)"
  unfolding CLAMP_def[abs_def]
  by (intro landau_symbol.cong eq_reflection) 
     (auto intro: eventually_mono[OF eventually_ge_at_top[of "3::nat"]])

private lemma UNCLAMP'_: 
  "landau_symbol L L' Lr ⟹ L at_top (CLAMP' (MASTER_BOUND a b c)) ≡ L at_top (MASTER_BOUND a b c)"
  unfolding CLAMP'_def[abs_def] CLAMP_def[abs_def]
  by (intro landau_symbol.cong eq_reflection) 
     (auto intro: eventually_mono[OF eventually_ge_at_top[of "3::nat"]])

private lemma UNCLAMP_: 
  "landau_symbol L L' Lr ⟹ L at_top (CLAMP f) ≡ L at_top (f)"
  using eventually_ge_at_top[of "3::nat"] unfolding CLAMP'_def[abs_def] CLAMP_def[abs_def]
  by (intro landau_symbol.cong eq_reflection) 
     (auto intro: eventually_mono[OF eventually_ge_at_top[of "3::nat"]])

lemmas CLAMP = landau_symbols[THEN CLAMP_]
lemmas UNCLAMP' = landau_symbols[THEN UNCLAMP'_]
lemmas UNCLAMP = landau_symbols[THEN UNCLAMP_]
end

lemma propagate_CLAMP:
  "CLAMP (λx. f x * g x) = CLAMP' (λx. CLAMP f x * CLAMP g x)"
  "CLAMP (λx. f x / g x) = CLAMP' (λx. CLAMP f x / CLAMP g x)"
  "CLAMP (λx. inverse (f x)) = CLAMP' (λx. inverse (CLAMP f x))"
  "CLAMP (λx. real x) = CLAMP' (MASTER_BOUND 1 0 0)"
  "CLAMP (λx. real x powr a) = CLAMP' (MASTER_BOUND a 0 0)"
  "CLAMP (λx. real x ^ a') = CLAMP' (MASTER_BOUND (real a') 0 0)"
  "CLAMP (λx. ln (real x)) = CLAMP' (MASTER_BOUND 0 1 0)"
  "CLAMP (λx. ln (real x) powr b) = CLAMP' (MASTER_BOUND 0 b 0)"
  "CLAMP (λx. ln (real x) ^ b') = CLAMP' (MASTER_BOUND 0 (real b') 0)"
  "CLAMP (λx. ln (ln (real x))) = CLAMP' (MASTER_BOUND 0 0 1)"
  "CLAMP (λx. ln (ln (real x)) powr c) = CLAMP' (MASTER_BOUND 0 0 c)"
  "CLAMP (λx. ln (ln (real x)) ^ c') = CLAMP' (MASTER_BOUND 0 0 (real c'))"
  "CLAMP' (CLAMP f) = CLAMP' f"
  "CLAMP' (λx. CLAMP' (MASTER_BOUND a1 b1 c1) x * CLAMP' (MASTER_BOUND a2 b2 c2) x) = 
       CLAMP' (MASTER_BOUND (a1+a2) (b1+b2) (c1+c2))"
  "CLAMP' (λx. CLAMP' (MASTER_BOUND a1 b1 c1) x / CLAMP' (MASTER_BOUND a2 b2 c2) x) = 
       CLAMP' (MASTER_BOUND (a1-a2) (b1-b2) (c1-c2))"
  "CLAMP' (λx. inverse (MASTER_BOUND a1 b1 c1 x)) = CLAMP' (MASTER_BOUND (-a1) (-b1) (-c1))"
by (insert ln_1_imp_less_3')
   (rule ext, simp add: CLAMP_def CLAMP'_def MASTER_BOUND_def 
      powr_realpow powr_one[OF ln_ln_nonneg'] powr_realpow[OF ln_ln_pos] powr_add
      powr_diff powr_minus)+

lemma numeral_assoc_simps:
  "((a::real) + numeral b) + numeral c = a + numeral (b + c)"
  "(a + numeral b) - numeral c = a + neg_numeral_class.sub b c"
  "(a - numeral b) + numeral c = a + neg_numeral_class.sub c b"
  "(a - numeral b) - numeral c = a - numeral (b + c)" by simp_all

lemmas CLAMP_aux =
  arith_simps numeral_assoc_simps of_nat_power of_nat_mult of_nat_numeral
  one_add_one numeral_One [symmetric]

lemmas CLAMP_postproc = numeral_One

context master_theorem_function
begin

lemma master1_bigo_automation:
  assumes "g ∈ O(λx. real x powr p')" "1 < (∑i<k. as ! i * bs ! i powr p')" 
  shows   "f ∈ O(MASTER_BOUND p 0 0)"
proof-
  have "MASTER_BOUND p 0 0 ∈ Θ(λx::nat. x powr p)" unfolding MASTER_BOUND_def[abs_def]
    by (intro landau_real_nat_transfer bigthetaI_cong 
          eventually_mono[OF eventually_ge_at_top[of "3::real"]]) (auto dest!: ln_1_imp_less_3)
  from landau_o.big.cong_bigtheta[OF this] master1_bigo[OF assms] show ?thesis by simp
qed

lemma master1_automation:
  assumes "g ∈ O(MASTER_BOUND'' p')" "1 < (∑i<k. as ! i * bs ! i powr p')" 
          "eventually (λx. f x > 0) at_top"
  shows   "f ∈ Θ(MASTER_BOUND p 0 0)"
proof-
  have A: "MASTER_BOUND p 0 0 ∈ Θ(λx::nat. x powr p)" unfolding MASTER_BOUND_def[abs_def]
    by (intro landau_real_nat_transfer bigthetaI_cong 
      eventually_mono[OF eventually_ge_at_top[of "3::real"]]) (auto dest!: ln_1_imp_less_3)
  have B: "O(MASTER_BOUND'' p') = O(λx::nat. real x powr p')"
    using eventually_ge_at_top[of "2::nat"]
    by (intro landau_o.big.cong) (auto elim!: eventually_mono simp: MASTER_BOUND''_def)
  from landau_theta.cong_bigtheta[OF A] B assms(1) master1[OF _ assms(2-)] show ?thesis by simp
qed

lemma master2_1_automation:
  assumes "g ∈ Θ(MASTER_BOUND' p p')" "p' < -1"
  shows   "f ∈ Θ(MASTER_BOUND p 0 0)"
proof-
  have A: "MASTER_BOUND p 0 0 ∈ Θ(λx::nat. x powr p)" unfolding MASTER_BOUND_def[abs_def]
    by (intro landau_real_nat_transfer bigthetaI_cong 
          eventually_mono[OF eventually_ge_at_top[of "3::real"]]) (auto dest!: ln_1_imp_less_3)
  have B: "Θ(MASTER_BOUND' p p') = Θ(λx::nat. real x powr p * ln (real x) powr p')"
    by (subst CLAMP, (subst MASTER_BOUND_postproc MASTER_BOUND_UNCLAMP)+, simp only: UNCLAMP)
  from landau_theta.cong_bigtheta[OF A] B assms(1) master2_1[OF _ assms(2-)] show ?thesis by simp
qed

lemma master2_2_automation:
  assumes "g ∈ Θ(MASTER_BOUND' p (-1))"
  shows   "f ∈ Θ(MASTER_BOUND p 0 1)"
proof-
  have A: "MASTER_BOUND p 0 1 ∈ Θ(λx::nat. x powr p * ln (ln x))" unfolding MASTER_BOUND_def[abs_def]
    using eventually_ge_at_top[of "3::real"]
    apply (intro landau_real_nat_transfer, intro bigthetaI_cong)
    apply (elim eventually_mono, subst powr_one[OF ln_ln_nonneg])
    apply simp_all
    done
  have B: "Θ(MASTER_BOUND' p (-1)) = Θ(λx::nat. real x powr p / ln (real x))"
    by (subst CLAMP, (subst MASTER_BOUND_postproc MASTER_BOUND_UNCLAMP)+, simp only: UNCLAMP)
  from landau_theta.cong_bigtheta[OF A] B assms(1) master2_2 show ?thesis by simp
qed

lemma master2_3_automation:
  assumes "g ∈ Θ(MASTER_BOUND' p (p' - 1))" "p' > 0"
  shows   "f ∈ Θ(MASTER_BOUND p p' 0)"
proof-
  have A: "MASTER_BOUND p p' 0 ∈ Θ(λx::nat. x powr p * ln x powr p')" unfolding MASTER_BOUND_def[abs_def]
    using eventually_ge_at_top[of "3::real"]
    apply (intro landau_real_nat_transfer, intro bigthetaI_cong)
    apply (elim eventually_mono, auto dest: ln_1_imp_less_3)
    done
  have B: "Θ(MASTER_BOUND' p (p' - 1)) = Θ(λx::nat. real x powr p * ln x powr (p' - 1))"
    by (subst CLAMP, (subst MASTER_BOUND_postproc MASTER_BOUND_UNCLAMP)+, simp only: UNCLAMP)
  from landau_theta.cong_bigtheta[OF A] B assms(1) master2_3[OF _ assms(2-)] show ?thesis by simp
qed

lemma master3_automation:
  assumes "g ∈ Θ(MASTER_BOUND'' p')" "1 > (∑i<k. as ! i * bs ! i powr p')"
  shows   "f ∈ Θ(MASTER_BOUND p' 0 0)"
proof-
  have A: "MASTER_BOUND p' 0 0 ∈ Θ(λx::nat. x powr p')" unfolding MASTER_BOUND_def[abs_def]
    using eventually_ge_at_top[of "3::real"]
    apply (intro landau_real_nat_transfer, intro bigthetaI_cong)
    apply (elim eventually_mono, auto dest: ln_1_imp_less_3)
    done
  have B: "Θ(MASTER_BOUND'' p') = Θ(λx::nat. real x powr p')"
    by (subst CLAMP, (subst MASTER_BOUND_postproc)+, simp only: UNCLAMP)
  from landau_theta.cong_bigtheta[OF A] B assms(1) master3[OF _ assms(2-)] show ?thesis by simp
qed

lemmas master_automation = 
  master1_automation master2_1_automation master2_2_automation 
  master2_2_automation master3_automation


ML ‹

fun generalize_master_thm ctxt thm =
  let
    val ([p'], ctxt') = Variable.variant_fixes ["p''"] ctxt
    val p' = Free (p', HOLogic.realT)
    val a = @{term "nth as"} $ Bound 0
    val b = @{term "Transcendental.powr :: real => real => real"} $ 
              (@{term "nth bs"} $ Bound 0) $ p'
    val f = Abs ("i", HOLogic.natT, @{term "(*) :: real => real => real"} $ a $ b)
    val sum = @{term "sum :: (nat => real) => nat set => real"} $ f $ @{term "{..<k}"}
    val prop = HOLogic.mk_Trueprop (HOLogic.mk_eq (sum, @{term "1::real"}))
    val cprop = Thm.cterm_of ctxt' prop
  in
    thm
    |> Local_Defs.unfold ctxt' [Thm.assume cprop RS @{thm p_unique}]
    |> Thm.implies_intr cprop
    |> rotate_prems 1
    |> singleton (Variable.export ctxt' ctxt)
  end

fun generalize_master_thm' (binding, thm) ctxt =
  Local_Theory.note ((binding, []), [generalize_master_thm ctxt thm]) ctxt |> snd

›

local_setup ‹
  fold generalize_master_thm' 
    [(@{binding master1_automation'}, @{thm master1_automation}), 
     (@{binding master1_bigo_automation'}, @{thm master1_bigo_automation}), 
     (@{binding master2_1_automation'}, @{thm master2_1_automation}),
     (@{binding master2_2_automation'}, @{thm master2_2_automation}),
     (@{binding master2_3_automation'}, @{thm master2_3_automation}), 
     (@{binding master3_automation'}, @{thm master3_automation})]
›

end


definition "arith_consts (x :: real) (y :: nat) = 
  (if ¬ (-x) + 3 / x * 5 - 1 ≤ x ∧ True ∨ True ⟶ True then 
  x < inverse 3 powr 21 else x = real (Suc 0 ^ 2 + 
  (if 42 - x ≤ 1 ∧ 1 div y = y mod 2 ∨ y < Numeral1 then 0 else 0)) + Numeral1)"

ML_file ‹akra_bazzi.ML›

hide_const arith_consts

method_setup master_theorem = ‹
  Akra_Bazzi.setup_master_theorem
› "automatically apply the Master theorem for recursive functions"

method_setup akra_bazzi_termination = ‹
  Scan.succeed (fn ctxt => SIMPLE_METHOD' (Akra_Bazzi.akra_bazzi_termination_tac ctxt))
› "prove termination of Akra-Bazzi functions"

hide_const CLAMP CLAMP' MASTER_BOUND MASTER_BOUND' MASTER_BOUND''

end