# HG changeset patch
# User wenzelm
# Date 1361822148 -3600
# Node ID 546a9a1c315d84f4a248104342efe335dc928700
# Parent  aba03f0c62548f499397ddc684420f2871dea8c3# Parent  05522141d2440850990be7f583071be3a25a6e2a
merged;

diff -r 05522141d244 -r 546a9a1c315d src/Doc/Codegen/Inductive_Predicate.thy
--- a/src/Doc/Codegen/Inductive_Predicate.thy	Mon Feb 25 17:47:32 2013 +0100
+++ b/src/Doc/Codegen/Inductive_Predicate.thy	Mon Feb 25 20:55:48 2013 +0100
@@ -265,7 +265,7 @@
 
 text {*
   Further examples for compiling inductive predicates can be found in
-  the @{text "HOL/ex/Predicate_Compile_ex.thy"} theory file.  There are
+  the @{text "HOL/Predicate_Compile_Examples.thy"} theory file.  There are
   also some examples in the Archive of Formal Proofs, notably in the
   @{text "POPLmark-deBruijn"} and the @{text "FeatherweightJava"}
   sessions.
diff -r 05522141d244 -r 546a9a1c315d src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Mon Feb 25 17:47:32 2013 +0100
+++ b/src/HOL/Big_Operators.thy	Mon Feb 25 20:55:48 2013 +0100
@@ -1808,4 +1808,20 @@
 
 end
 
+lemma (in linorder) mono_Max_commute:
+  assumes "mono f"
+  assumes "finite A" and "A \<noteq> {}"
+  shows "f (Max A) = Max (f ` A)"
+proof (rule linorder_class.Max_eqI [symmetric])
+  from `finite A` show "finite (f ` A)" by simp
+  from assms show "f (Max A) \<in> f ` A" by simp
+  fix x
+  assume "x \<in> f ` A"
+  then obtain y where "y \<in> A" and "x = f y" ..
+  with assms have "y \<le> Max A" by auto
+  with `mono f` have "f y \<le> f (Max A)" by (rule monoE)
+  with `x = f y` show "x \<le> f (Max A)" by simp
+qed (* FIXME augment also dual rule mono_Min_commute *)
+
 end
+
diff -r 05522141d244 -r 546a9a1c315d src/HOL/IMP/Abs_Int2_ivl.thy
--- a/src/HOL/IMP/Abs_Int2_ivl.thy	Mon Feb 25 17:47:32 2013 +0100
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy	Mon Feb 25 20:55:48 2013 +0100
@@ -37,7 +37,7 @@
 "in_ivl k (Ivl Minf Pinf) \<longleftrightarrow> True"
 
 
-instantiation lb :: order
+instantiation lb :: linorder
 begin
 
 definition less_eq_lb where
@@ -55,11 +55,13 @@
   case goal3 thus ?case by(auto simp: less_eq_lb_def split:lub_splits)
 next
   case goal4 thus ?case by(auto simp: less_eq_lb_def split:lub_splits)
+next
+  case goal5 thus ?case by(auto simp: less_eq_lb_def split:lub_splits)
 qed
 
 end
 
-instantiation ub :: order
+instantiation ub :: linorder
 begin
 
 definition less_eq_ub where
@@ -77,12 +79,19 @@
   case goal3 thus ?case by(auto simp: less_eq_ub_def split:lub_splits)
 next
   case goal4 thus ?case by(auto simp: less_eq_ub_def split:lub_splits)
+next
+  case goal5 thus ?case by(auto simp: less_eq_ub_def split:lub_splits)
 qed
 
 end
 
 lemmas le_lub_defs = less_eq_lb_def less_eq_ub_def
 
+lemma le_lub_simps[simp]:
+  "Minf \<le> l" "Lb i \<le> Lb j = (i \<le> j)" "~ Lb i \<le> Minf"
+  "h \<le> Pinf" "Ub i \<le> Ub j = (i \<le> j)" "~ Pinf \<le> Ub j"
+by(auto simp: le_lub_defs split: lub_splits)
+
 definition empty where "empty = {1\<dots>0}"
 
 fun is_empty where
@@ -200,15 +209,6 @@
 "uminus_lb(Lb( x)) = Ub(-x)" |
 "uminus_lb Minf = Pinf"
 
-instantiation ivl :: minus
-begin
-
-definition "i1 - i2 = (if is_empty i1 | is_empty i2 then empty else
-  case (i1,i2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow> Ivl (l1 + uminus_ub h2) (h1 + uminus_lb l2))"
-
-instance ..
-end
-
 instantiation ivl :: uminus
 begin
 
@@ -218,12 +218,22 @@
 instance ..
 end
 
-lemma minus_ivl_nice_def: "(i1::ivl) - i2 = i1 + -i2"
+instantiation ivl :: minus
+begin
+
+definition minus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" where
+"(i1::ivl) - i2 = i1 + -i2"
+
+instance ..
+end
+
+lemma minus_ivl_cases: "i1 - i2 = (if is_empty i1 | is_empty i2 then empty else
+  case (i1,i2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow> Ivl (l1 + uminus_ub h2) (h1 + uminus_lb l2))"
 by(auto simp: plus_ivl_def minus_ivl_def split: ivl.split lub_splits)
 
 lemma gamma_minus_ivl:
   "n1 : \<gamma>_ivl i1 \<Longrightarrow> n2 : \<gamma>_ivl i2 \<Longrightarrow> n1-n2 : \<gamma>_ivl(i1 - i2)"
-by(auto simp add: minus_ivl_def \<gamma>_ivl_def split: ivl.splits lub_splits)
+by(auto simp add: minus_ivl_def plus_ivl_def \<gamma>_ivl_def split: ivl.splits lub_splits)
 
 definition "filter_plus_ivl i i1 i2 = ((*if is_empty i then empty else*)
   i1 \<sqinter> (i - i2), i2 \<sqinter> (i - i1))"
@@ -261,7 +271,7 @@
 
 lemma mono_minus_ivl: fixes i1 :: ivl
 shows "i1 \<sqsubseteq> i1' \<Longrightarrow> i2 \<sqsubseteq> i2' \<Longrightarrow> i1 - i2 \<sqsubseteq> i1' - i2'"
-apply(auto simp add: minus_ivl_def empty_def le_ivl_def le_lub_defs split: ivl.splits)
+apply(auto simp add: minus_ivl_cases empty_def le_ivl_def le_lub_defs split: ivl.splits)
   apply(simp split: lub_splits)
  apply(simp split: lub_splits)
 apply(simp split: lub_splits)
diff -r 05522141d244 -r 546a9a1c315d src/HOL/Library/Discrete.thy
--- a/src/HOL/Library/Discrete.thy	Mon Feb 25 17:47:32 2013 +0100
+++ b/src/HOL/Library/Discrete.thy	Mon Feb 25 20:55:48 2013 +0100
@@ -6,11 +6,6 @@
 imports Main
 begin
 
-lemma power2_nat_le_eq_le:
-  fixes m n :: nat
-  shows "m ^ 2 \<le> n ^ 2 \<longleftrightarrow> m \<le> n"
-  by (auto intro: power2_le_imp_le power_mono)
-
 subsection {* Discrete logarithm *}
 
 fun log :: "nat \<Rightarrow> nat" where
@@ -81,10 +76,32 @@
 
 definition sqrt :: "nat \<Rightarrow> nat"
 where
-  "sqrt n = Max {m. m ^ 2 \<le> n}"
+  "sqrt n = Max {m. m\<twosuperior> \<le> n}"
+
+lemma sqrt_aux:
+  fixes n :: nat
+  shows "finite {m. m\<twosuperior> \<le> n}" and "{m. m\<twosuperior> \<le> n} \<noteq> {}"
+proof -
+  { fix m
+    assume "m\<twosuperior> \<le> n"
+    then have "m \<le> n"
+      by (cases m) (simp_all add: power2_eq_square)
+  } note ** = this
+  then have "{m. m\<twosuperior> \<le> n} \<subseteq> {m. m \<le> n}" by auto
+  then show "finite {m. m\<twosuperior> \<le> n}" by (rule finite_subset) rule
+  have "0\<twosuperior> \<le> n" by simp
+  then show *: "{m. m\<twosuperior> \<le> n} \<noteq> {}" by blast
+qed
+
+lemma [code]:
+  "sqrt n = Max (Set.filter (\<lambda>m. m\<twosuperior> \<le> n) {0..n})"
+proof -
+  from power2_nat_le_imp_le [of _ n] have "{m. m \<le> n \<and> m\<twosuperior> \<le> n} = {m. m\<twosuperior> \<le> n}" by auto
+  then show ?thesis by (simp add: sqrt_def Set.filter_def)
+qed
 
 lemma sqrt_inverse_power2 [simp]:
-  "sqrt (n ^ 2) = n"
+  "sqrt (n\<twosuperior>) = n"
 proof -
   have "{m. m \<le> n} \<noteq> {}" by auto
   then have "Max {m. m \<le> n} \<le> n" by auto
@@ -92,32 +109,74 @@
     by (auto simp add: sqrt_def power2_nat_le_eq_le intro: antisym)
 qed
 
-lemma [code]:
-  "sqrt n = Max (Set.filter (\<lambda>m. m ^ 2 \<le> n) {0..n})"
+lemma mono_sqrt: "mono sqrt"
+proof
+  fix m n :: nat
+  have *: "0 * 0 \<le> m" by simp
+  assume "m \<le> n"
+  then show "sqrt m \<le> sqrt n"
+    by (auto intro!: Max_mono `0 * 0 \<le> m` finite_less_ub simp add: power2_eq_square sqrt_def)
+qed
+
+lemma sqrt_greater_zero_iff [simp]:
+  "sqrt n > 0 \<longleftrightarrow> n > 0"
 proof -
-  { fix m
-    assume "m\<twosuperior> \<le> n"
-    then have "m \<le> n"
-      by (cases m) (simp_all add: power2_eq_square)
-  }
-  then have "{m. m \<le> n \<and> m\<twosuperior> \<le> n} = {m. m\<twosuperior> \<le> n}" by auto
-  then show ?thesis by (simp add: sqrt_def Set.filter_def)
+  have *: "0 < Max {m. m\<twosuperior> \<le> n} \<longleftrightarrow> (\<exists>a\<in>{m. m\<twosuperior> \<le> n}. 0 < a)"
+    by (rule Max_gr_iff) (fact sqrt_aux)+
+  show ?thesis
+  proof
+    assume "0 < sqrt n"
+    then have "0 < Max {m. m\<twosuperior> \<le> n}" by (simp add: sqrt_def)
+    with * show "0 < n" by (auto dest: power2_nat_le_imp_le)
+  next
+    assume "0 < n"
+    then have "1\<twosuperior> \<le> n \<and> 0 < (1::nat)" by simp
+    then have "\<exists>q. q\<twosuperior> \<le> n \<and> 0 < q" ..
+    with * have "0 < Max {m. m\<twosuperior> \<le> n}" by blast
+    then show "0 < sqrt n" by  (simp add: sqrt_def)
+  qed
+qed
+
+lemma sqrt_power2_le [simp]: (* FIXME tune proof *)
+  "(sqrt n)\<twosuperior> \<le> n"
+proof (cases "n > 0")
+  case False then show ?thesis by (simp add: sqrt_def)
+next
+  case True then have "sqrt n > 0" by simp
+  then have "mono (times (Max {m. m\<twosuperior> \<le> n}))" by (auto intro: mono_times_nat simp add: sqrt_def)
+  then have *: "Max {m. m\<twosuperior> \<le> n} * Max {m. m\<twosuperior> \<le> n} = Max (times (Max {m. m\<twosuperior> \<le> n}) ` {m. m\<twosuperior> \<le> n})"
+    using sqrt_aux [of n] by (rule mono_Max_commute)
+  have "Max (op * (Max {m. m * m \<le> n}) ` {m. m * m \<le> n}) \<le> n"
+    apply (subst Max_le_iff)
+    apply (metis (mono_tags) finite_imageI finite_less_ub le_square)
+    apply simp
+    apply (metis le0 mult_0_right)
+    apply auto
+    proof -
+      fix q
+      assume "q * q \<le> n"
+      show "Max {m. m * m \<le> n} * q \<le> n"
+      proof (cases "q > 0")
+        case False then show ?thesis by simp
+      next
+        case True then have "mono (times q)" by (rule mono_times_nat)
+        then have "q * Max {m. m * m \<le> n} = Max (times q ` {m. m * m \<le> n})"
+          using sqrt_aux [of n] by (auto simp add: power2_eq_square intro: mono_Max_commute)
+        then have "Max {m. m * m \<le> n} * q = Max (times q ` {m. m * m \<le> n})" by (simp add: mult_ac)
+        then show ?thesis apply simp
+          apply (subst Max_le_iff)
+          apply auto
+          apply (metis (mono_tags) finite_imageI finite_less_ub le_square)
+          apply (metis `q * q \<le> n`)
+          using `q * q \<le> n` by (metis le_cases mult_le_mono1 mult_le_mono2 order_trans)
+      qed
+    qed
+  with * show ?thesis by (simp add: sqrt_def power2_eq_square)
 qed
 
 lemma sqrt_le:
   "sqrt n \<le> n"
-proof -
-  have "0\<twosuperior> \<le> n" by simp
-  then have *: "{m. m\<twosuperior> \<le> n} \<noteq> {}" by blast
-  { fix m
-    assume "m\<twosuperior> \<le> n"
-    then have "m \<le> n"
-      by (cases m) (simp_all add: power2_eq_square)
-  } note ** = this
-  then have "{m. m\<twosuperior> \<le> n} \<subseteq> {m. m \<le> n}" by auto
-  then have "finite {m. m\<twosuperior> \<le> n}" by (rule finite_subset) rule
-  with * show ?thesis by (auto simp add: sqrt_def intro: **)
-qed
+  using sqrt_aux [of n] by (auto simp add: sqrt_def intro: power2_nat_le_imp_le)
 
 hide_const (open) log sqrt
 
diff -r 05522141d244 -r 546a9a1c315d src/HOL/Library/Function_Growth.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Function_Growth.thy	Mon Feb 25 20:55:48 2013 +0100
@@ -0,0 +1,346 @@
+
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Comparing growth of functions on natural numbers by a preorder relation *}
+
+theory Function_Growth
+imports Main "~~/src/HOL/Library/Preorder" "~~/src/HOL/Library/Discrete"
+begin
+
+subsection {* Motivation *}
+
+text {*
+  When comparing growth of functions in computer science, it is common to adhere
+  on Landau Symbols (``O-Notation'').  However these come at the cost of notational
+  oddities, particularly writing @{text "f = O(g)"} for @{text "f \<in> O(g)"} etc.
+  
+  Here we suggest a diffent 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 @{text "\<lesssim>"} on functions such that
+  @{text "f \<lesssim> g \<longleftrightarrow> f \<in> 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 hierachy of functions:
+  @{text "(\<lambda>n. 0) \<lesssim> (\<lambda>n. k) \<lesssim> Discrete.log \<lesssim> Discrete.sqrt \<lesssim> id \<lesssim> \<dots>"}.
+*}
+
+subsection {* Model *}
+
+text {*
+  Our growth functions are of type @{text "\<nat> \<Rightarrow> \<nat>"}.  This is different
+  to the usual conventions for Landau symbols for which @{text "\<real> \<Rightarrow> \<real>"}
+  would be appropriate, but we argue that @{text "\<real> \<Rightarrow> \<real>"} is more
+  appropriate for analysis, whereas our setting is discrete.
+
+  Note that we also restrict the additional coefficients to @{text \<nat>}, something
+  we discuss at the particular definitions.
+*}
+
+subsection {* The @{text "\<lesssim>"} relation *}
+
+definition less_eq_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<lesssim>" 50)
+where
+  "f \<lesssim> g \<longleftrightarrow> (\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m)"
+
+text {*
+  This yields @{text "f \<lesssim> g \<longleftrightarrow> f \<in> O(g)"}.  Note that @{text c} is restricted to
+  @{text \<nat>}.  This does not pose any problems since if @{text "f \<in> O(g)"} holds for
+  a @{text "c \<in> \<real>"}, it also holds for @{text "\<lceil>c\<rceil> \<in> \<nat>"} by transitivity.
+*}
+
+lemma less_eq_funI [intro?]:
+  assumes "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m"
+  shows "f \<lesssim> g"
+  unfolding less_eq_fun_def by (rule assms)
+
+lemma not_less_eq_funI:
+  assumes "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * g m < f m"
+  shows "\<not> f \<lesssim> g"
+  using assms unfolding less_eq_fun_def linorder_not_le [symmetric] by blast
+
+lemma less_eq_funE [elim?]:
+  assumes "f \<lesssim> g"
+  obtains n c where "c > 0" and "\<And>m. m > n \<Longrightarrow> f m \<le> c * g m"
+  using assms unfolding less_eq_fun_def by blast
+
+lemma not_less_eq_funE:
+  assumes "\<not> f \<lesssim> 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 @{text "\<approx>"} relation, the equivalence relation induced by @{text "\<lesssim>"} *}
+
+definition equiv_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<cong>" 50)
+where
+  "f \<cong> g \<longleftrightarrow>
+    (\<exists>c\<^isub>1>0. \<exists>c\<^isub>2>0. \<exists>n. \<forall>m>n. f m \<le> c\<^isub>1 * g m \<and> g m \<le> c\<^isub>2 * f m)"
+
+text {*
+  This yields @{text "f \<cong> g \<longleftrightarrow> f \<in> \<Theta>(g)"}.  Concerning @{text "c\<^isub>1"} and @{text "c\<^isub>2"}
+  restricted to @{typ nat}, see note above on @{text "(\<lesssim>)"}.
+*}
+
+lemma equiv_funI [intro?]:
+  assumes "\<exists>c\<^isub>1>0. \<exists>c\<^isub>2>0. \<exists>n. \<forall>m>n. f m \<le> c\<^isub>1 * g m \<and> g m \<le> c\<^isub>2 * f m"
+  shows "f \<cong> g"
+  unfolding equiv_fun_def by (rule assms)
+
+lemma not_equiv_funI:
+  assumes "\<And>c\<^isub>1 c\<^isub>2 n. c\<^isub>1 > 0 \<Longrightarrow> c\<^isub>2 > 0 \<Longrightarrow>
+    \<exists>m>n. c\<^isub>1 * f m < g m \<or> c\<^isub>2 * g m < f m"
+  shows "\<not> f \<cong> g"
+  using assms unfolding equiv_fun_def linorder_not_le [symmetric] by blast
+
+lemma equiv_funE [elim?]:
+  assumes "f \<cong> g"
+  obtains n c\<^isub>1 c\<^isub>2 where "c\<^isub>1 > 0" and "c\<^isub>2 > 0"
+    and "\<And>m. m > n \<Longrightarrow> f m \<le> c\<^isub>1 * g m \<and> g m \<le> c\<^isub>2 * f m"
+  using assms unfolding equiv_fun_def by blast
+
+lemma not_equiv_funE:
+  fixes n c\<^isub>1 c\<^isub>2
+  assumes "\<not> f \<cong> g" and "c\<^isub>1 > 0" and "c\<^isub>2 > 0"
+  obtains m where "m > n"
+    and "c\<^isub>1 * f m < g m \<or> c\<^isub>2 * g m < f m"
+  using assms unfolding equiv_fun_def linorder_not_le [symmetric] by blast
+
+
+subsection {* The @{text "\<prec>"} relation, the strict part of @{text "\<lesssim>"} *}
+
+definition less_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<prec>" 50)
+where
+  "f \<prec> g \<longleftrightarrow> f \<lesssim> g \<and> \<not> g \<lesssim> f"
+
+lemma less_funI:
+  assumes "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m"
+    and "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * f m < g m"
+  shows "f \<prec> g"
+  using assms unfolding less_fun_def less_eq_fun_def linorder_not_less [symmetric] by blast
+
+lemma not_less_funI:
+  assumes "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * g m < f m"
+    and "\<exists>c>0. \<exists>n. \<forall>m>n. g m \<le> c * f m"
+  shows "\<not> f \<prec> g"
+  using assms unfolding less_fun_def less_eq_fun_def linorder_not_less [symmetric] by blast
+
+lemma less_funE [elim?]:
+  assumes "f \<prec> g"
+  obtains n c where "c > 0" and "\<And>m. m > n \<Longrightarrow> f m \<le> c * g m"
+    and "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * f m < g m"
+proof -
+  from assms have "f \<lesssim> g" and "\<not> g \<lesssim> f" by (simp_all add: less_fun_def)
+  from `f \<lesssim> g` obtain n c where *:"c > 0" "\<And>m. m > n \<Longrightarrow> f m \<le> c * g m"
+    by (rule less_eq_funE) blast
+  { fix c n :: nat
+    assume "c > 0"
+    with `\<not> g \<lesssim> f` obtain m where "m > n" "c * f m < g m"
+      by (rule not_less_eq_funE) blast
+    then have **: "\<exists>m>n. c * f m < g m" by blast
+  } note ** = this
+  from * ** show thesis by (rule that)
+qed
+
+lemma not_less_funE:
+  assumes "\<not> f \<prec> g" and "c > 0"
+  obtains m where "m > n" and "c * g m < f m"
+    | d q where "\<And>m. d > 0 \<Longrightarrow> m > q \<Longrightarrow> g q \<le> d * f q"
+  using assms unfolding less_fun_def linorder_not_less [symmetric] by blast
+
+text {*
+  I did not found a proof for @{text "f \<prec> g \<longleftrightarrow> f \<in> o(g)"}.  Maybe this only
+  holds if @{text f} and/or @{text g} are of a certain class of functions.
+  However @{text "f \<in> o(g) \<longrightarrow> f \<prec> g"} is provable, and this yields a
+  handy introduction rule.
+
+  Note that D. Knuth ignores @{text o} altogether.  So what \dots
+
+  Something still has to be said about the coefficient @{text c} in
+  the definition of @{text "(\<prec>)"}.  In the typical definition of @{text o},
+  it occurs on the \emph{right} hand side of the @{text "(>)"}.  The reason
+  is that the situation is dual to the definition of @{text O}: the definition
+  works since @{text c} may become arbitrary small.  Since this is not possible
+  within @{term \<nat>}, we push the coefficient to the left hand side instead such
+  that it become arbitrary big instead.
+*}
+
+lemma less_fun_strongI:
+  assumes "\<And>c. c > 0 \<Longrightarrow> \<exists>n. \<forall>m>n. c * f m < g m"
+  shows "f \<prec> g"
+proof (rule less_funI)
+  have "1 > (0::nat)" by simp
+  from assms `1 > 0` have "\<exists>n. \<forall>m>n. 1 * f m < g m" .
+  then obtain n where *: "\<And>m. m > n \<Longrightarrow> 1 * f m < g m" by blast
+  have "\<forall>m>n. f m \<le> 1 * g m"
+  proof (rule allI, rule impI)
+    fix m
+    assume "m > n"
+    with * have "1 * f m < g m" by simp
+    then show "f m \<le> 1 * g m" by simp
+  qed
+  with `1 > 0` show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m" by blast
+  fix c n :: nat
+  assume "c > 0"
+  with assms obtain q where "\<And>m. m > q \<Longrightarrow> c * f m < g m" by blast
+  then have "c * f (Suc (q + n)) < g (Suc (q + n))" by simp
+  moreover have "Suc (q + n) > n" by simp
+  ultimately show "\<exists>m>n. c * f m < g m" by blast
+qed
+
+
+subsection {* @{text "\<lesssim>"} is a preorder *}
+
+text {* This yields all lemmas relating @{text "\<lesssim>"}, @{text "\<prec>"} and @{text "\<cong>"}. *}
+
+interpretation fun_order: preorder_equiv less_eq_fun less_fun
+  where "preorder_equiv.equiv less_eq_fun = equiv_fun"
+proof -
+  interpret preorder: preorder_equiv less_eq_fun less_fun
+  proof
+    fix f g h
+    show "f \<lesssim> f"
+    proof
+      have "\<exists>n. \<forall>m>n. f m \<le> 1 * f m" by auto
+      then show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * f m" by blast
+    qed
+    show "f \<prec> g \<longleftrightarrow> f \<lesssim> g \<and> \<not> g \<lesssim> f"
+      by (fact less_fun_def)
+    assume "f \<lesssim> g" and "g \<lesssim> h"
+    show "f \<lesssim> h"
+    proof
+      from `f \<lesssim> g` obtain n\<^isub>1 c\<^isub>1
+        where "c\<^isub>1 > 0" and P\<^isub>1: "\<And>m. m > n\<^isub>1 \<Longrightarrow> f m \<le> c\<^isub>1 * g m"
+        by rule blast
+      from `g \<lesssim> h` obtain n\<^isub>2 c\<^isub>2
+        where "c\<^isub>2 > 0" and P\<^isub>2: "\<And>m. m > n\<^isub>2 \<Longrightarrow> g m \<le> c\<^isub>2 * h m"
+        by rule blast
+      have "\<forall>m>max n\<^isub>1 n\<^isub>2. f m \<le> (c\<^isub>1 * c\<^isub>2) * h m"
+      proof (rule allI, rule impI)
+        fix m
+        assume Q: "m > max n\<^isub>1 n\<^isub>2"
+        from P\<^isub>1 Q have *: "f m \<le> c\<^isub>1 * g m" by simp
+        from P\<^isub>2 Q have "g m \<le> c\<^isub>2 * h m" by simp
+        with `c\<^isub>1 > 0` have "c\<^isub>1 * g m \<le> (c\<^isub>1 * c\<^isub>2) * h m" by simp
+        with * show "f m \<le> (c\<^isub>1 * c\<^isub>2) * h m" by (rule order_trans)
+      qed
+      then have "\<exists>n. \<forall>m>n. f m \<le> (c\<^isub>1 * c\<^isub>2) * h m" by rule
+      moreover from `c\<^isub>1 > 0` `c\<^isub>2 > 0` have "c\<^isub>1 * c\<^isub>2 > 0" by (rule mult_pos_pos)
+      ultimately show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * h m" by blast
+    qed
+  qed
+  from preorder.preorder_equiv_axioms show "class.preorder_equiv less_eq_fun less_fun" .
+  show "preorder_equiv.equiv less_eq_fun = equiv_fun"
+  proof (rule ext, rule ext, unfold preorder.equiv_def)
+    fix f g
+    show "f \<lesssim> g \<and> g \<lesssim> f \<longleftrightarrow> f \<cong> g"
+    proof
+      assume "f \<cong> g"
+      then obtain n c\<^isub>1 c\<^isub>2 where "c\<^isub>1 > 0" and "c\<^isub>2 > 0"
+        and *: "\<And>m. m > n \<Longrightarrow> f m \<le> c\<^isub>1 * g m \<and> g m \<le> c\<^isub>2 * f m"
+        by rule blast
+      have "\<forall>m>n. f m \<le> c\<^isub>1 * g m"
+      proof (rule allI, rule impI)
+        fix m
+        assume "m > n"
+        with * show "f m \<le> c\<^isub>1 * g m" by simp
+      qed
+      with `c\<^isub>1 > 0` have "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m" by blast
+      then have "f \<lesssim> g" ..
+      have "\<forall>m>n. g m \<le> c\<^isub>2 * f m"
+      proof (rule allI, rule impI)
+        fix m
+        assume "m > n"
+        with * show "g m \<le> c\<^isub>2 * f m" by simp
+      qed
+      with `c\<^isub>2 > 0` have "\<exists>c>0. \<exists>n. \<forall>m>n. g m \<le> c * f m" by blast
+      then have "g \<lesssim> f" ..
+      from `f \<lesssim> g` and `g \<lesssim> f` show "f \<lesssim> g \<and> g \<lesssim> f" ..
+    next
+      assume "f \<lesssim> g \<and> g \<lesssim> f"
+      then have "f \<lesssim> g" and "g \<lesssim> f" by auto
+      from `f \<lesssim> g` obtain n\<^isub>1 c\<^isub>1 where "c\<^isub>1 > 0"
+        and P\<^isub>1: "\<And>m. m > n\<^isub>1 \<Longrightarrow> f m \<le> c\<^isub>1 * g m" by rule blast
+      from `g \<lesssim> f` obtain n\<^isub>2 c\<^isub>2 where "c\<^isub>2 > 0"
+        and P\<^isub>2: "\<And>m. m > n\<^isub>2 \<Longrightarrow> g m \<le> c\<^isub>2 * f m" by rule blast
+      have "\<forall>m>max n\<^isub>1 n\<^isub>2. f m \<le> c\<^isub>1 * g m \<and> g m \<le> c\<^isub>2 * f m"
+      proof (rule allI, rule impI)
+        fix m
+        assume Q: "m > max n\<^isub>1 n\<^isub>2"
+        from P\<^isub>1 Q have "f m \<le> c\<^isub>1 * g m" by simp
+        moreover from P\<^isub>2 Q have "g m \<le> c\<^isub>2 * f m" by simp
+        ultimately show "f m \<le> c\<^isub>1 * g m \<and> g m \<le> c\<^isub>2 * f m" ..
+      qed
+      with `c\<^isub>1 > 0` `c\<^isub>2 > 0` have "\<exists>c\<^isub>1>0. \<exists>c\<^isub>2>0. \<exists>n.
+        \<forall>m>n. f m \<le> c\<^isub>1 * g m \<and> g m \<le> c\<^isub>2 * f m" by blast
+      then show "f \<cong> g" ..
+    qed
+  qed
+qed
+
+
+subsection {* Simple examples *}
+
+text {*
+  Most of these are left as constructive exercises for the reader.  Note that additional
+  preconditions to the functions may be necessary.  The list here is by no means to be
+  intended as complete contruction set for typical functions, here surely something
+  has to be added yet.
+*}
+
+text {* @{prop "(\<lambda>n. f n + k) \<cong> f"} *}
+
+text {* @{prop "(\<lambda>n. Suc k * f n) \<cong> f"} *}
+
+lemma "f \<lesssim> (\<lambda>n. f n + g n)"
+  by rule auto
+
+lemma "(\<lambda>_. 0) \<prec> (\<lambda>n. Suc k)"
+  by (rule less_fun_strongI) auto
+
+lemma "(\<lambda>_. k) \<prec> Discrete.log"
+proof (rule less_fun_strongI)
+  fix c :: nat
+  have "\<forall>m>2 ^ (Suc (c * k)). c * k < Discrete.log m"
+  proof (rule allI, rule impI)
+    fix m :: nat
+    assume "2 ^ Suc (c * k) < m"
+    then have "2 ^ Suc (c * k) \<le> m" by simp
+    with log_mono have "Discrete.log (2 ^ (Suc (c * k))) \<le> Discrete.log m"
+      by (blast dest: monoD)
+    moreover have "c * k < Discrete.log (2 ^ (Suc (c * k)))" by simp
+    ultimately show "c * k < Discrete.log m" by auto
+  qed
+  then show "\<exists>n. \<forall>m>n. c * k < Discrete.log m" ..
+qed
+  
+text {* @{prop "Discrete.log \<prec> Discrete.sqrt"} *}
+
+lemma "Discrete.sqrt \<prec> id"
+proof (rule less_fun_strongI)
+  fix c :: nat
+  assume "0 < c"
+  have "\<forall>m>(Suc c)\<twosuperior>. c * Discrete.sqrt m < id m"
+  proof (rule allI, rule impI)
+    fix m
+    assume "(Suc c)\<twosuperior> < m"
+    then have "(Suc c)\<twosuperior> \<le> m" by simp
+    with mono_sqrt have "Discrete.sqrt ((Suc c)\<twosuperior>) \<le> Discrete.sqrt m" by (rule monoE)
+    then have "Suc c \<le> Discrete.sqrt m" by simp
+    then have "c < Discrete.sqrt m" by simp
+    moreover from `(Suc c)\<twosuperior> < m` have "Discrete.sqrt m > 0" by simp
+    ultimately have "c * Discrete.sqrt m < Discrete.sqrt m * Discrete.sqrt m" by simp
+    also have "\<dots> \<le> m" by (simp add: power2_eq_square [symmetric])
+    finally show "c * Discrete.sqrt m < id m" by simp
+  qed
+  then show "\<exists>n. \<forall>m>n. c * Discrete.sqrt m < id m" ..
+qed
+
+lemma "id \<prec> (\<lambda>n. n\<twosuperior>)"
+  by (rule less_fun_strongI) (auto simp add: power2_eq_square)
+
+lemma "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. n ^ Suc k)"
+  by (rule less_fun_strongI) auto
+
+text {* @{prop "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. 2 ^ n)"} *}
+
+end
+
diff -r 05522141d244 -r 546a9a1c315d src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Mon Feb 25 17:47:32 2013 +0100
+++ b/src/HOL/Library/Library.thy	Mon Feb 25 20:55:48 2013 +0100
@@ -15,7 +15,6 @@
   Countable_Set
   Debug
   Diagonal_Subsequence
-  Discrete
   Dlist
   Eval_Witness
   Extended_Nat
@@ -26,6 +25,7 @@
   FrechetDeriv
   FuncSet
   Function_Division
+  Function_Growth
   Fundamental_Theorem_Algebra
   Indicator_Function
   Infinite_Set
diff -r 05522141d244 -r 546a9a1c315d src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Mon Feb 25 17:47:32 2013 +0100
+++ b/src/HOL/Nat.thy	Mon Feb 25 20:55:48 2013 +0100
@@ -1201,6 +1201,16 @@
     apply (auto)
   done
 
+lemma mono_times_nat:
+  fixes n :: nat
+  assumes "n > 0"
+  shows "mono (times n)"
+proof
+  fix m q :: nat
+  assume "m \<le> q"
+  with assms show "n * m \<le> n * q" by simp
+qed
+
 text {* the lattice order on @{typ nat} *}
 
 instantiation nat :: distrib_lattice
diff -r 05522141d244 -r 546a9a1c315d src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Mon Feb 25 17:47:32 2013 +0100
+++ b/src/HOL/Orderings.thy	Mon Feb 25 20:55:48 2013 +0100
@@ -965,6 +965,15 @@
   shows "mono f \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
   unfolding mono_def by iprover
 
+lemma monoE:
+  fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
+  assumes "mono f"
+  assumes "x \<le> y"
+  obtains "f x \<le> f y"
+proof
+  from assms show "f x \<le> f y" by (simp add: mono_def)
+qed
+
 definition strict_mono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool" where
   "strict_mono f \<longleftrightarrow> (\<forall>x y. x < y \<longrightarrow> f x < f y)"
 
@@ -998,6 +1007,21 @@
 context linorder
 begin
 
+lemma mono_invE:
+  fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
+  assumes "mono f"
+  assumes "f x < f y"
+  obtains "x \<le> y"
+proof
+  show "x \<le> y"
+  proof (rule ccontr)
+    assume "\<not> x \<le> y"
+    then have "y \<le> x" by simp
+    with `mono f` obtain "f y \<le> f x" by (rule monoE)
+    with `f x < f y` show False by simp
+  qed
+qed
+
 lemma strict_mono_eq:
   assumes "strict_mono f"
   shows "f x = f y \<longleftrightarrow> x = y"
diff -r 05522141d244 -r 546a9a1c315d src/HOL/Power.thy
--- a/src/HOL/Power.thy	Mon Feb 25 17:47:32 2013 +0100
+++ b/src/HOL/Power.thy	Mon Feb 25 20:55:48 2013 +0100
@@ -721,6 +721,18 @@
   apply (erule dvd_imp_le, simp)
   done
 
+lemma power2_nat_le_eq_le:
+  fixes m n :: nat
+  shows "m\<twosuperior> \<le> n\<twosuperior> \<longleftrightarrow> m \<le> n"
+  by (auto intro: power2_le_imp_le power_mono)
+
+lemma power2_nat_le_imp_le:
+  fixes m n :: nat
+  assumes "m\<twosuperior> \<le> n"
+  shows "m \<le> n"
+  using assms by (cases m) (simp_all add: power2_eq_square)
+
+
 
 subsection {* Code generator tweak *}
 
diff -r 05522141d244 -r 546a9a1c315d src/HOL/ROOT
--- a/src/HOL/ROOT	Mon Feb 25 17:47:32 2013 +0100
+++ b/src/HOL/ROOT	Mon Feb 25 20:55:48 2013 +0100
@@ -455,7 +455,6 @@
     Transfer_Int_Nat
     HarmonicSeries
     Refute_Examples
-    Landau
     Execute_Choice
     Summation
     Gauge_Integration
diff -r 05522141d244 -r 546a9a1c315d src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Mon Feb 25 17:47:32 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Mon Feb 25 20:55:48 2013 +0100
@@ -69,11 +69,10 @@
     end
 
     (* compress top level steps - do not compress subproofs *)
-    fun compress_top_level on_top_level ctxt steps =
+    fun compress_top_level on_top_level ctxt n steps =
     let
       (* proof step vector *)
       val step_vect = steps |> map SOME |> Vector.fromList
-      val n = Vector.length step_vect
       val n_metis = add_metis_steps_top_level steps 0
       val target_n_metis = Real.fromInt n_metis / isar_compress |> Real.round
 
@@ -91,7 +90,7 @@
         | SOME (By_Metis (subproofs, (lfs, _))) =>
             maps (steps_of_proof #> maps refs) subproofs @ lookup_indices lfs)
       val refed_by_vect =
-        Vector.tabulate (n, K [])
+        Vector.tabulate (Vector.length step_vect, K [])
         |> fold_index (fn (i, step) => fold (update (cons i)) (refs step)) steps
         |> Vector.map rev (* after rev, indices are sorted in ascending order *)
 
@@ -202,7 +201,7 @@
       merge_steps metis_time step_vect refed_by_vect cand_tab n n_metis
     end
 
-    fun do_proof on_top_level ctxt (Proof (fix, assms,steps)) =
+    fun do_proof on_top_level ctxt (Proof (Fix fix, Assume assms, steps)) =
       let
         (* Enrich context with top-level facts *)
         val thy = Proof_Context.theory_of ctxt
@@ -214,17 +213,18 @@
           | enrich_with_step (Obtain (_, _, l, t, _)) = enrich_with_fact l t
           | enrich_with_step _ = I
         val enrich_with_steps = fold enrich_with_step
-        fun enrich_with_assms (Assume assms) =
-          fold (uncurry enrich_with_fact) assms
+        val enrich_with_assms = fold (uncurry enrich_with_fact)
         val rich_ctxt =
           ctxt |> enrich_with_assms assms |> enrich_with_steps steps
 
+        val n = List.length fix + List.length assms + List.length steps
+
         (* compress subproofs and top-levl steps *)
         val ((steps, top_level_time), lower_level_time) =
           steps |> do_subproofs rich_ctxt
-                |>> compress_top_level on_top_level rich_ctxt
+                |>> compress_top_level on_top_level rich_ctxt n
       in
-        (Proof (fix, assms, steps),
+        (Proof (Fix fix, Assume assms, steps),
           add_preplay_time lower_level_time top_level_time)
       end
 
diff -r 05522141d244 -r 546a9a1c315d src/HOL/ex/Landau.thy
--- a/src/HOL/ex/Landau.thy	Mon Feb 25 17:47:32 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,226 +0,0 @@
-
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* Comparing growth of functions on natural numbers by a preorder relation *}
-
-theory Landau
-imports Main "~~/src/HOL/Library/Preorder"
-begin
-
-text {*
-  We establish a preorder releation @{text "\<lesssim>"} on functions from
-  @{text "\<nat>"} to @{text "\<nat>"} such that @{text "f \<lesssim> g \<longleftrightarrow> f \<in> O(g)"}.
-*}
-
-subsection {* Auxiliary *}
-
-lemma Ex_All_bounded:
-  fixes n :: nat
-  assumes "\<exists>n. \<forall>m\<ge>n. P m"
-  obtains m where "m \<ge> n" and "P m"
-proof -
-  from assms obtain q where m_q: "\<forall>m\<ge>q. P m" ..
-  let ?m = "max q n"
-  have "?m \<ge> n" by auto
-  moreover from m_q have "P ?m" by auto
-  ultimately show thesis ..
-qed
-    
-
-subsection {* The @{text "\<lesssim>"} relation *}
-
-definition less_eq_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<lesssim>" 50) where
-  "f \<lesssim> g \<longleftrightarrow> (\<exists>c n. \<forall>m\<ge>n. f m \<le> Suc c * g m)"
-
-lemma less_eq_fun_intro:
-  assumes "\<exists>c n. \<forall>m\<ge>n. f m \<le> Suc c * g m"
-  shows "f \<lesssim> g"
-  unfolding less_eq_fun_def by (rule assms)
-
-lemma less_eq_fun_not_intro:
-  assumes "\<And>c n. \<exists>m\<ge>n. Suc c * g m < f m"
-  shows "\<not> f \<lesssim> g"
-  using assms unfolding less_eq_fun_def linorder_not_le [symmetric]
-  by blast
-
-lemma less_eq_fun_elim:
-  assumes "f \<lesssim> g"
-  obtains n c where "\<And>m. m \<ge> n \<Longrightarrow> f m \<le> Suc c * g m"
-  using assms unfolding less_eq_fun_def by blast
-
-lemma less_eq_fun_not_elim:
-  assumes "\<not> f \<lesssim> g"
-  obtains m where "m \<ge> n" and "Suc c * g m < f m"
-  using assms unfolding less_eq_fun_def linorder_not_le [symmetric]
-  by blast
-
-lemma less_eq_fun_refl:
-  "f \<lesssim> f"
-proof (rule less_eq_fun_intro)
-  have "\<exists>n. \<forall>m\<ge>n. f m \<le> Suc 0 * f m" by auto
-  then show "\<exists>c n. \<forall>m\<ge>n. f m \<le> Suc c * f m" by blast
-qed
-
-lemma less_eq_fun_trans:
-  assumes f_g: "f \<lesssim> g" and g_h: "g \<lesssim> h"
-  shows f_h: "f \<lesssim> h"
-proof -
-  from f_g obtain n\<^isub>1 c\<^isub>1
-    where P1: "\<And>m. m \<ge> n\<^isub>1 \<Longrightarrow> f m \<le> Suc c\<^isub>1 * g m"
-  by (erule less_eq_fun_elim)
-  moreover from g_h obtain n\<^isub>2 c\<^isub>2
-    where P2: "\<And>m. m \<ge> n\<^isub>2 \<Longrightarrow> g m \<le> Suc c\<^isub>2 * h m"
-  by (erule less_eq_fun_elim)
-  ultimately have "\<And>m. m \<ge> max n\<^isub>1 n\<^isub>2 \<Longrightarrow> f m \<le> Suc c\<^isub>1 * g m \<and> g m \<le> Suc c\<^isub>2 * h m"
-  by auto
-  moreover {
-    fix k l r :: nat
-    assume k_l: "k \<le> Suc c\<^isub>1 * l" and l_r: "l \<le> Suc c\<^isub>2 * r"
-    from l_r have "Suc c\<^isub>1 * l \<le> (Suc c\<^isub>1 * Suc c\<^isub>2) * r"
-    by (auto simp add: mult_le_cancel_left mult_assoc simp del: times_nat.simps mult_Suc_right)
-    with k_l have "k \<le> (Suc c\<^isub>1 * Suc c\<^isub>2) * r" by (rule preorder_class.order_trans)
-  }
-  ultimately have "\<And>m. m \<ge> max n\<^isub>1 n\<^isub>2 \<Longrightarrow> f m \<le> (Suc c\<^isub>1 * Suc c\<^isub>2) * h m" by auto
-  then have "\<And>m. m \<ge> max n\<^isub>1 n\<^isub>2 \<Longrightarrow> f m \<le> Suc ((Suc c\<^isub>1 * Suc c\<^isub>2) - 1) * h m" by auto
-  then show ?thesis unfolding less_eq_fun_def by blast
-qed
-
-
-subsection {* The @{text "\<approx>"} relation, the equivalence relation induced by @{text "\<lesssim>"} *}
-
-definition equiv_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<cong>" 50) where
-  "f \<cong> g \<longleftrightarrow> (\<exists>d c n. \<forall>m\<ge>n. g m \<le> Suc d * f m \<and> f m \<le> Suc c * g m)"
-
-lemma equiv_fun_intro:
-  assumes "\<exists>d c n. \<forall>m\<ge>n. g m \<le> Suc d * f m \<and> f m \<le> Suc c * g m"
-  shows "f \<cong> g"
-  unfolding equiv_fun_def by (rule assms)
-
-lemma equiv_fun_not_intro:
-  assumes "\<And>d c n. \<exists>m\<ge>n. Suc d * f m < g m \<or> Suc c * g m < f m"
-  shows "\<not> f \<cong> g"
-  unfolding equiv_fun_def
-  by (auto simp add: assms linorder_not_le
-    simp del: times_nat.simps mult_Suc_right)
-
-lemma equiv_fun_elim:
-  assumes "f \<cong> g"
-  obtains n d c
-    where "\<And>m. m \<ge> n \<Longrightarrow> g m \<le> Suc d * f m \<and> f m \<le> Suc c * g m"
-  using assms unfolding equiv_fun_def by blast
-
-lemma equiv_fun_not_elim:
-  fixes n d c
-  assumes "\<not> f \<cong> g"
-  obtains m where "m \<ge> n"
-    and "Suc d * f m < g m \<or> Suc c * g m < f m"
-  using assms unfolding equiv_fun_def
-  by (auto simp add: linorder_not_le, blast)
-
-lemma equiv_fun_less_eq_fun:
-  "f \<cong> g \<longleftrightarrow> f \<lesssim> g \<and> g \<lesssim> f"
-proof
-  assume x_y: "f \<cong> g"
-  then obtain n d c
-    where interv: "\<And>m. m \<ge> n \<Longrightarrow> g m \<le> Suc d * f m \<and> f m \<le> Suc c * g m"
-  by (erule equiv_fun_elim)
-  from interv have "\<exists>c n. \<forall>m \<ge> n. f m \<le> Suc c * g m" by auto
-  then have f_g: "f \<lesssim> g" by (rule less_eq_fun_intro)
-  from interv have "\<exists>d n. \<forall>m \<ge> n. g m \<le> Suc d * f m" by auto
-  then have g_f: "g \<lesssim> f" by (rule less_eq_fun_intro)
-  from f_g g_f show "f \<lesssim> g \<and> g \<lesssim> f" by auto
-next
-  assume assm: "f \<lesssim> g \<and> g \<lesssim> f"
-  from assm less_eq_fun_elim obtain c n\<^isub>1 where
-    bound1: "\<And>m. m \<ge> n\<^isub>1 \<Longrightarrow> f m \<le> Suc c * g m" 
-    by blast
-  from assm less_eq_fun_elim obtain d n\<^isub>2 where
-    bound2: "\<And>m. m \<ge> n\<^isub>2 \<Longrightarrow> g m \<le> Suc d * f m"
-    by blast
-  from bound2 have "\<And>m. m \<ge> max n\<^isub>1 n\<^isub>2 \<Longrightarrow> g m \<le> Suc d * f m"
-  by auto
-  with bound1
-    have "\<forall>m \<ge> max n\<^isub>1 n\<^isub>2. g m \<le> Suc d * f m \<and> f m \<le> Suc c * g m"
-    by auto
-  then
-    have "\<exists>d c n. \<forall>m\<ge>n. g m \<le> Suc d * f m \<and> f m \<le> Suc c * g m"
-    by blast
-  then show "f \<cong> g" by (rule equiv_fun_intro)
-qed
-
-subsection {* The @{text "\<prec>"} relation, the strict part of @{text "\<lesssim>"} *}
-
-definition less_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<prec>" 50) where
-  "f \<prec> g \<longleftrightarrow> f \<lesssim> g \<and> \<not> g \<lesssim> f"
-
-lemma less_fun_intro:
-  assumes "\<And>c. \<exists>n. \<forall>m\<ge>n. Suc c * f m < g m"
-  shows "f \<prec> g"
-proof (unfold less_fun_def, rule conjI)
-  from assms obtain n
-    where "\<forall>m\<ge>n. Suc 0 * f m < g m" ..
-  then have "\<forall>m\<ge>n. f m \<le> Suc 0 * g m" by auto
-  then have "\<exists>c n. \<forall>m\<ge>n. f m \<le> Suc c * g m" by blast
-  then show "f \<lesssim> g" by (rule less_eq_fun_intro)
-next
-  show "\<not> g \<lesssim> f"
-  proof (rule less_eq_fun_not_intro)
-    fix c n :: nat
-    from assms have "\<exists>n. \<forall>m\<ge>n. Suc c * f m < g m" by blast
-    then obtain m where "m \<ge> n" and "Suc c * f m < g m"
-      by (rule Ex_All_bounded)
-    then show "\<exists>m\<ge>n. Suc c * f m < g m" by blast
-  qed
-qed
-
-text {*
-  We would like to show (or refute) that @{text "f \<prec> g \<longleftrightarrow> f \<in> o(g)"},
-  i.e.~@{prop "f \<prec> g \<longleftrightarrow> (\<forall>c. \<exists>n. \<forall>m>n. f m < Suc c * g m)"} but did not
-  manage to do so.
-*}
-
-
-subsection {* Assert that @{text "\<lesssim>"} is indeed a preorder *}
-
-interpretation fun_order: preorder_equiv less_eq_fun less_fun
-  where "preorder_equiv.equiv less_eq_fun = equiv_fun"
-proof -
-  interpret preorder_equiv less_eq_fun less_fun proof
-  qed (simp_all add: less_fun_def less_eq_fun_refl, auto intro: less_eq_fun_trans)
-  show "class.preorder_equiv less_eq_fun less_fun" using preorder_equiv_axioms .
-  show "preorder_equiv.equiv less_eq_fun = equiv_fun"
-    by (simp add: fun_eq_iff equiv_def equiv_fun_less_eq_fun)
-qed
-
-
-subsection {* Simple examples *}
-
-lemma "(\<lambda>_. n) \<lesssim> (\<lambda>n. n)"
-proof (rule less_eq_fun_intro)
-  show "\<exists>c q. \<forall>m\<ge>q. n \<le> Suc c * m"
-  proof -
-    have "\<forall>m\<ge>n. n \<le> Suc 0 * m" by simp
-    then show ?thesis by blast
-  qed
-qed
-
-lemma "(\<lambda>n. n) \<cong> (\<lambda>n. Suc k * n)"
-proof (rule equiv_fun_intro)
-  show "\<exists>d c n. \<forall>m\<ge>n. Suc k * m \<le> Suc d * m \<and> m \<le> Suc c * (Suc k * m)"
-  proof -
-    have "\<forall>m\<ge>n. Suc k * m \<le> Suc k * m \<and> m \<le> Suc c * (Suc k * m)" by simp
-    then show ?thesis by blast
-  qed
-qed  
-
-lemma "(\<lambda>_. n) \<prec> (\<lambda>n. n)"
-proof (rule less_fun_intro)
-  fix c
-  show "\<exists>q. \<forall>m\<ge>q. Suc c * n < m"
-  proof -
-    have "\<forall>m\<ge>Suc c * n + 1. Suc c * n < m" by simp
-    then show ?thesis by blast
-  qed
-qed
-
-end