Theory Estimation_Method

section "The @{text estimation} tactic"

theory Estimation_Method
  imports Main "HOL-Eisbach.Eisbach_Tools"
begin

text "A few useful lemmas for working with inequalities."

lemma if_prop_cong:
  assumes "C = C'"
  assumes "C ⟹ P A A'"
  assumes "¬ C ⟹ P B B'"
  shows "P (if C then A else B) (if C' then A' else B')"
  using assms by simp

lemma if_leqI:
  assumes "C ⟹ A ≤ t"
  assumes "¬ C ⟹ B ≤ t"
  shows "(if C then A else B) ≤ t"
  using assms by simp

lemma if_le_max:
  "(if C then (t1 :: 'a :: linorder) else t2) ≤ max t1 t2"
  by simp

text "Prove some inequality by showing a chain of inequalities via an intermediate term."

method itrans for step :: "'a :: order" =
  (match conclusion in "s ≤ t" for s t :: 'a ⇒ ‹rule order.trans[of s step t]›)

text "A collection of monotonicity intro rules that will be automatically used by @{text estimation}."

lemmas mono_intros =
  order.refl add_mono diff_mono mult_le_mono max.mono min.mono power_increasing power_mono
  iffD2[OF Suc_le_mono] if_prop_cong[where P = "(≤)"] Nat.le0 one_le_numeral

text "Try to apply a given estimation rule @{text estimate} in a forward-manner."

method estimation uses estimate =
  (match estimate in "⋀a. f a ≤ h a" (multi) for f h ⇒ ‹
    match conclusion in "g f ≤ t" for g and t :: nat ⇒
    ‹rule order.trans[of "g f" "g h" t], intro mono_intros refl estimate››
    
  ¦ "x ≤ y" for x y ⇒ ‹
    match conclusion in "g x ≤ t" for g and t :: nat ⇒
    ‹rule order.trans[of "g x" "g y" t], intro mono_intros refl estimate››)

end