Theory Karatsuba.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