diff r ea9b2e5ca9fc r 9c9baae29217 src/HOL/Library/Function_Growth.thy
 a/src/HOL/Library/Function_Growth.thy Sun Oct 08 22:28:19 2017 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ 1,454 +0,0 @@

(* Author: Florian Haftmann, TU Muenchen *)

section \Comparing growth of functions on natural numbers by a preorder relation\

theory Function_Growth
imports Main Preorder Discrete
begin

(* FIXME move *)

context linorder
begin

lemma mono_invE:
 fixes f :: "'a \ 'b::order"
 assumes "mono f"
 assumes "f x < f y"
 obtains "x < y"
proof
 show "x < y"
 proof (rule ccontr)
 assume "\ x < y"
 then have "y \ x" by simp
 with \mono f\ obtain "f y \ f x" by (rule monoE)
 with \f x < f y\ show False by simp
 qed
qed

end

lemma (in semidom_divide) power_diff:
 fixes a :: 'a
 assumes "a \ 0"
 assumes "m \ n"
 shows "a ^ (m  n) = (a ^ m) div (a ^ n)"
proof 
 define q where "q = m  n"
 with assms have "m = q + n" by (simp add: q_def)
 with q_def show ?thesis using \a \ 0\ by (simp add: power_add)
qed


subsection \Motivation\

text \
 When comparing growth of functions in computer science, it is common to adhere
 on Landau Symbols (``ONotation''). However these come at the cost of notational
 oddities, particularly writing \f = O(g)\ for \f \ O(g)\ etc.

 Here we suggest a different way, following Hardy (G.~H.~Hardy and J.~E.~Littlewood,
 Some problems of Diophantine approximation, Acta Mathematica 37 (1914), p.~225).
 We establish a quasi order relation \\\ on functions such that
 \f \ g \ f \ O(g)\. From a didactic point of view, this does not only
 avoid the notational oddities mentioned above but also emphasizes the key insight
 of a growth hierarchy of functions:
 \(\n. 0) \ (\n. k) \ Discrete.log \ Discrete.sqrt \ id \ \\.
\

subsection \Model\

text \
 Our growth functions are of type \\ \ \\. This is different
 to the usual conventions for Landau symbols for which \\ \ \\
 would be appropriate, but we argue that \\ \ \\ is more
 appropriate for analysis, whereas our setting is discrete.

 Note that we also restrict the additional coefficients to \\\, something
 we discuss at the particular definitions.
\

subsection \The \\\ relation\

definition less_eq_fun :: "(nat \ nat) \ (nat \ nat) \ bool" (infix "\" 50)
where
 "f \ g \ (\c>0. \n. \m>n. f m \ c * g m)"

text \
 This yields \f \ g \ f \ O(g)\. Note that \c\ is restricted to
 \\\. This does not pose any problems since if \f \ O(g)\ holds for
 a \c \ \\, it also holds for \\c\ \ \\ by transitivity.
\

lemma less_eq_funI [intro?]:
 assumes "\c>0. \n. \m>n. f m \ c * g m"
 shows "f \ g"
 unfolding less_eq_fun_def by (rule assms)

lemma not_less_eq_funI:
 assumes "\c n. c > 0 \ \m>n. c * g m < f m"
 shows "\ f \ g"
 using assms unfolding less_eq_fun_def linorder_not_le [symmetric] by blast

lemma less_eq_funE [elim?]:
 assumes "f \ g"
 obtains n c where "c > 0" and "\m. m > n \ f m \ c * g m"
 using assms unfolding less_eq_fun_def by blast

lemma not_less_eq_funE:
 assumes "\ f \ g" and "c > 0"
 obtains m where "m > n" and "c * g m < f m"
 using assms unfolding less_eq_fun_def linorder_not_le [symmetric] by blast


subsection \The \\\ relation, the equivalence relation induced by \\\\

definition equiv_fun :: "(nat \ nat) \ (nat \ nat) \ bool" (infix "\" 50)
where
 "f \ g \
 (\c\<^sub>1>0. \c\<^sub>2>0. \n. \m>n. f m \ c\<^sub>1 * g m \ g m \ c\<^sub>2 * f m)"

text \
 This yields \f \ g \ f \ \(g)\. Concerning \c\<^sub>1\ and \c\<^sub>2\
 restricted to @{typ nat}, see note above on \(\)\.
\

lemma equiv_funI:
 assumes "\c\<^sub>1>0. \c\<^sub>2>0. \n. \m>n. f m \ c\<^sub>1 * g m \ g m \ c\<^sub>2 * f m"
 shows "f \ g"
 unfolding equiv_fun_def by (rule assms)

lemma not_equiv_funI:
 assumes "\c\<^sub>1 c\<^sub>2 n. c\<^sub>1 > 0 \ c\<^sub>2 > 0 \
 \m>n. c\<^sub>1 * f m < g m \ c\<^sub>2 * g m < f m"
 shows "\ f \ g"
 using assms unfolding equiv_fun_def linorder_not_le [symmetric] by blast

lemma equiv_funE:
 assumes "f \ g"
 obtains n c\<^sub>1 c\<^sub>2 where "c\<^sub>1 > 0" and "c\<^sub>2 > 0"
 and "\m. m > n \ f m \ c\<^sub>1 * g m \ g m \ c\<^sub>2 * f m"
 using assms unfolding equiv_fun_def by blast

lemma not_equiv_funE:
 fixes n c\<^sub>1 c\<^sub>2
 assumes "\ f \ g" and "c\<^sub>1 > 0" and "c\<^sub>2 > 0"
 obtains m where "m > n"
 and "c\<^sub>1 * f m < g m \ c\<^sub>2 * g m < f m"
 using assms unfolding equiv_fun_def linorder_not_le [symmetric] by blast


subsection \The \\\ relation, the strict part of \\\\

definition less_fun :: "(nat \ nat) \ (nat \ nat) \ bool" (infix "\" 50)
where
 "f \ g \ f \ g \ \ g \ f"

lemma less_funI:
 assumes "\c>0. \n. \m>n. f m \ c * g m"
 and "\c n. c > 0 \ \m>n. c * f m < g m"
 shows "f \ g"
 using assms unfolding less_fun_def less_eq_fun_def linorder_not_less [symmetric] by blast

lemma not_less_funI:
 assumes "\c n. c > 0 \ \m>n. c * g m < f m"
 and "\c>0. \n. \m>n. g m \ c * f m"
 shows "\ f \ g"
 using assms unfolding less_fun_def less_eq_fun_def linorder_not_less [symmetric] by blast

lemma less_funE [elim?]:
 assumes "f \ g"
 obtains n c where "c > 0" and "\m. m > n \ f m \ c * g m"
 and "\c n. c > 0 \ \m>n. c * f m < g m"
proof 
 from assms have "f \ g" and "\ g \ f" by (simp_all add: less_fun_def)
 from \f \ g\ obtain n c where *:"c > 0" "m > n \ f m \ c * g m" for m
 by (rule less_eq_funE) blast
 { fix c n :: nat
 assume "c > 0"
 with \\ g \ f\ obtain m where "m > n" "c * f m < g m"
 by (rule not_less_eq_funE) blast
 then have **: "\m>n. c * f m < g m" by blast
 } note ** = this
 from * ** show thesis by (rule that)
qed

lemma not_less_funE:
 assumes "\ f \ g" and "c > 0"
 obtains m where "m > n" and "c * g m < f m"
  d q where "\m. d > 0 \ m > q \ g q \ d * f q"
 using assms unfolding less_fun_def linorder_not_less [symmetric] by blast

text \
 I did not find a proof for \f \ g \ f \ o(g)\. Maybe this only
 holds if \f\ and/or \g\ are of a certain class of functions.
 However \f \