turned example into library for comparing growth of functions
authorhaftmann
Sun Feb 24 20:29:13 2013 +0100 (2013-02-24)
changeset 5126331e786e0e6a7
parent 51262 e2bdfb2de028
child 51264 aba03f0c6254
turned example into library for comparing growth of functions
src/HOL/Big_Operators.thy
src/HOL/Library/Discrete.thy
src/HOL/Library/Function_Growth.thy
src/HOL/Library/Library.thy
src/HOL/Nat.thy
src/HOL/Orderings.thy
src/HOL/Power.thy
src/HOL/ROOT
src/HOL/ex/Landau.thy
     1.1 --- a/src/HOL/Big_Operators.thy	Sun Feb 24 20:18:32 2013 +0100
     1.2 +++ b/src/HOL/Big_Operators.thy	Sun Feb 24 20:29:13 2013 +0100
     1.3 @@ -1808,4 +1808,20 @@
     1.4  
     1.5  end
     1.6  
     1.7 +lemma (in linorder) mono_Max_commute:
     1.8 +  assumes "mono f"
     1.9 +  assumes "finite A" and "A \<noteq> {}"
    1.10 +  shows "f (Max A) = Max (f ` A)"
    1.11 +proof (rule linorder_class.Max_eqI [symmetric])
    1.12 +  from `finite A` show "finite (f ` A)" by simp
    1.13 +  from assms show "f (Max A) \<in> f ` A" by simp
    1.14 +  fix x
    1.15 +  assume "x \<in> f ` A"
    1.16 +  then obtain y where "y \<in> A" and "x = f y" ..
    1.17 +  with assms have "y \<le> Max A" by auto
    1.18 +  with `mono f` have "f y \<le> f (Max A)" by (rule monoE)
    1.19 +  with `x = f y` show "x \<le> f (Max A)" by simp
    1.20 +qed (* FIXME augment also dual rule mono_Min_commute *)
    1.21 +
    1.22  end
    1.23 +
     2.1 --- a/src/HOL/Library/Discrete.thy	Sun Feb 24 20:18:32 2013 +0100
     2.2 +++ b/src/HOL/Library/Discrete.thy	Sun Feb 24 20:29:13 2013 +0100
     2.3 @@ -6,11 +6,6 @@
     2.4  imports Main
     2.5  begin
     2.6  
     2.7 -lemma power2_nat_le_eq_le:
     2.8 -  fixes m n :: nat
     2.9 -  shows "m ^ 2 \<le> n ^ 2 \<longleftrightarrow> m \<le> n"
    2.10 -  by (auto intro: power2_le_imp_le power_mono)
    2.11 -
    2.12  subsection {* Discrete logarithm *}
    2.13  
    2.14  fun log :: "nat \<Rightarrow> nat" where
    2.15 @@ -81,10 +76,32 @@
    2.16  
    2.17  definition sqrt :: "nat \<Rightarrow> nat"
    2.18  where
    2.19 -  "sqrt n = Max {m. m ^ 2 \<le> n}"
    2.20 +  "sqrt n = Max {m. m\<twosuperior> \<le> n}"
    2.21 +
    2.22 +lemma sqrt_aux:
    2.23 +  fixes n :: nat
    2.24 +  shows "finite {m. m\<twosuperior> \<le> n}" and "{m. m\<twosuperior> \<le> n} \<noteq> {}"
    2.25 +proof -
    2.26 +  { fix m
    2.27 +    assume "m\<twosuperior> \<le> n"
    2.28 +    then have "m \<le> n"
    2.29 +      by (cases m) (simp_all add: power2_eq_square)
    2.30 +  } note ** = this
    2.31 +  then have "{m. m\<twosuperior> \<le> n} \<subseteq> {m. m \<le> n}" by auto
    2.32 +  then show "finite {m. m\<twosuperior> \<le> n}" by (rule finite_subset) rule
    2.33 +  have "0\<twosuperior> \<le> n" by simp
    2.34 +  then show *: "{m. m\<twosuperior> \<le> n} \<noteq> {}" by blast
    2.35 +qed
    2.36 +
    2.37 +lemma [code]:
    2.38 +  "sqrt n = Max (Set.filter (\<lambda>m. m\<twosuperior> \<le> n) {0..n})"
    2.39 +proof -
    2.40 +  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
    2.41 +  then show ?thesis by (simp add: sqrt_def Set.filter_def)
    2.42 +qed
    2.43  
    2.44  lemma sqrt_inverse_power2 [simp]:
    2.45 -  "sqrt (n ^ 2) = n"
    2.46 +  "sqrt (n\<twosuperior>) = n"
    2.47  proof -
    2.48    have "{m. m \<le> n} \<noteq> {}" by auto
    2.49    then have "Max {m. m \<le> n} \<le> n" by auto
    2.50 @@ -92,32 +109,74 @@
    2.51      by (auto simp add: sqrt_def power2_nat_le_eq_le intro: antisym)
    2.52  qed
    2.53  
    2.54 -lemma [code]:
    2.55 -  "sqrt n = Max (Set.filter (\<lambda>m. m ^ 2 \<le> n) {0..n})"
    2.56 +lemma mono_sqrt: "mono sqrt"
    2.57 +proof
    2.58 +  fix m n :: nat
    2.59 +  have *: "0 * 0 \<le> m" by simp
    2.60 +  assume "m \<le> n"
    2.61 +  then show "sqrt m \<le> sqrt n"
    2.62 +    by (auto intro!: Max_mono `0 * 0 \<le> m` finite_less_ub simp add: power2_eq_square sqrt_def)
    2.63 +qed
    2.64 +
    2.65 +lemma sqrt_greater_zero_iff [simp]:
    2.66 +  "sqrt n > 0 \<longleftrightarrow> n > 0"
    2.67  proof -
    2.68 -  { fix m
    2.69 -    assume "m\<twosuperior> \<le> n"
    2.70 -    then have "m \<le> n"
    2.71 -      by (cases m) (simp_all add: power2_eq_square)
    2.72 -  }
    2.73 -  then have "{m. m \<le> n \<and> m\<twosuperior> \<le> n} = {m. m\<twosuperior> \<le> n}" by auto
    2.74 -  then show ?thesis by (simp add: sqrt_def Set.filter_def)
    2.75 +  have *: "0 < Max {m. m\<twosuperior> \<le> n} \<longleftrightarrow> (\<exists>a\<in>{m. m\<twosuperior> \<le> n}. 0 < a)"
    2.76 +    by (rule Max_gr_iff) (fact sqrt_aux)+
    2.77 +  show ?thesis
    2.78 +  proof
    2.79 +    assume "0 < sqrt n"
    2.80 +    then have "0 < Max {m. m\<twosuperior> \<le> n}" by (simp add: sqrt_def)
    2.81 +    with * show "0 < n" by (auto dest: power2_nat_le_imp_le)
    2.82 +  next
    2.83 +    assume "0 < n"
    2.84 +    then have "1\<twosuperior> \<le> n \<and> 0 < (1::nat)" by simp
    2.85 +    then have "\<exists>q. q\<twosuperior> \<le> n \<and> 0 < q" ..
    2.86 +    with * have "0 < Max {m. m\<twosuperior> \<le> n}" by blast
    2.87 +    then show "0 < sqrt n" by  (simp add: sqrt_def)
    2.88 +  qed
    2.89 +qed
    2.90 +
    2.91 +lemma sqrt_power2_le [simp]: (* FIXME tune proof *)
    2.92 +  "(sqrt n)\<twosuperior> \<le> n"
    2.93 +proof (cases "n > 0")
    2.94 +  case False then show ?thesis by (simp add: sqrt_def)
    2.95 +next
    2.96 +  case True then have "sqrt n > 0" by simp
    2.97 +  then have "mono (times (Max {m. m\<twosuperior> \<le> n}))" by (auto intro: mono_times_nat simp add: sqrt_def)
    2.98 +  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})"
    2.99 +    using sqrt_aux [of n] by (rule mono_Max_commute)
   2.100 +  have "Max (op * (Max {m. m * m \<le> n}) ` {m. m * m \<le> n}) \<le> n"
   2.101 +    apply (subst Max_le_iff)
   2.102 +    apply (metis (mono_tags) finite_imageI finite_less_ub le_square)
   2.103 +    apply simp
   2.104 +    apply (metis le0 mult_0_right)
   2.105 +    apply auto
   2.106 +    proof -
   2.107 +      fix q
   2.108 +      assume "q * q \<le> n"
   2.109 +      show "Max {m. m * m \<le> n} * q \<le> n"
   2.110 +      proof (cases "q > 0")
   2.111 +        case False then show ?thesis by simp
   2.112 +      next
   2.113 +        case True then have "mono (times q)" by (rule mono_times_nat)
   2.114 +        then have "q * Max {m. m * m \<le> n} = Max (times q ` {m. m * m \<le> n})"
   2.115 +          using sqrt_aux [of n] by (auto simp add: power2_eq_square intro: mono_Max_commute)
   2.116 +        then have "Max {m. m * m \<le> n} * q = Max (times q ` {m. m * m \<le> n})" by (simp add: mult_ac)
   2.117 +        then show ?thesis apply simp
   2.118 +          apply (subst Max_le_iff)
   2.119 +          apply auto
   2.120 +          apply (metis (mono_tags) finite_imageI finite_less_ub le_square)
   2.121 +          apply (metis `q * q \<le> n`)
   2.122 +          using `q * q \<le> n` by (metis le_cases mult_le_mono1 mult_le_mono2 order_trans)
   2.123 +      qed
   2.124 +    qed
   2.125 +  with * show ?thesis by (simp add: sqrt_def power2_eq_square)
   2.126  qed
   2.127  
   2.128  lemma sqrt_le:
   2.129    "sqrt n \<le> n"
   2.130 -proof -
   2.131 -  have "0\<twosuperior> \<le> n" by simp
   2.132 -  then have *: "{m. m\<twosuperior> \<le> n} \<noteq> {}" by blast
   2.133 -  { fix m
   2.134 -    assume "m\<twosuperior> \<le> n"
   2.135 -    then have "m \<le> n"
   2.136 -      by (cases m) (simp_all add: power2_eq_square)
   2.137 -  } note ** = this
   2.138 -  then have "{m. m\<twosuperior> \<le> n} \<subseteq> {m. m \<le> n}" by auto
   2.139 -  then have "finite {m. m\<twosuperior> \<le> n}" by (rule finite_subset) rule
   2.140 -  with * show ?thesis by (auto simp add: sqrt_def intro: **)
   2.141 -qed
   2.142 +  using sqrt_aux [of n] by (auto simp add: sqrt_def intro: power2_nat_le_imp_le)
   2.143  
   2.144  hide_const (open) log sqrt
   2.145  
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/Function_Growth.thy	Sun Feb 24 20:29:13 2013 +0100
     3.3 @@ -0,0 +1,346 @@
     3.4 +
     3.5 +(* Author: Florian Haftmann, TU Muenchen *)
     3.6 +
     3.7 +header {* Comparing growth of functions on natural numbers by a preorder relation *}
     3.8 +
     3.9 +theory Function_Growth
    3.10 +imports Main "~~/src/HOL/Library/Preorder" "~~/src/HOL/Library/Discrete"
    3.11 +begin
    3.12 +
    3.13 +subsection {* Motivation *}
    3.14 +
    3.15 +text {*
    3.16 +  When comparing growth of functions in computer science, it is common to adhere
    3.17 +  on Landau Symbols (\<guillemotright>O-Notation\<guillemotleft>).  However these come at the cost of notational
    3.18 +  oddities, particularly writing @{text "f = O(g)"} for @{text "f \<in> O(g)"} etc.
    3.19 +  
    3.20 +  Here we suggest a diffent way, following Hardy (G.~H.~Hardy and J.~E.~Littlewood,
    3.21 +  Some problems of Diophantine approximation, Acta Mathematica 37 (1914), p.~225).
    3.22 +  We establish a quasi order relation @{text "\<lesssim>"} on functions such that
    3.23 +  @{text "f \<lesssim> g \<longleftrightarrow> f \<in> O(g)"}.  From a didactic point of view, this does not only
    3.24 +  avoid the notational oddities mentioned above but also emphasizes the key insight
    3.25 +  of a growth hierachy of functions:
    3.26 +  @{text "(\<lambda>n. 0) \<lesssim> (\<lambda>n. k) \<lesssim> Discrete.log \<lesssim> Discrete.sqrt \<lesssim> id \<lesssim> \<dots>"}.
    3.27 +*}
    3.28 +
    3.29 +subsection {* Model *}
    3.30 +
    3.31 +text {*
    3.32 +  Our growth functions are of type @{text "\<nat> \<Rightarrow> \<nat>"}.  This is different
    3.33 +  to the usual conventions for Landau symbols for which @{text "\<real> \<Rightarrow> \<real>"}
    3.34 +  would be appropriate, but we argue that @{text "\<real> \<Rightarrow> \<real>"} is more
    3.35 +  appropriate for analysis, whereas our setting is discrete.
    3.36 +
    3.37 +  Note that we also restrict the additional coefficients to @{text \<nat>}, something
    3.38 +  we discuss at the particular definitions.
    3.39 +*}
    3.40 +
    3.41 +subsection {* The @{text "\<lesssim>"} relation *}
    3.42 +
    3.43 +definition less_eq_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<lesssim>" 50)
    3.44 +where
    3.45 +  "f \<lesssim> g \<longleftrightarrow> (\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m)"
    3.46 +
    3.47 +text {*
    3.48 +  This yields @{text "f \<lesssim> g \<longleftrightarrow> f \<in> O(g)"}.  Note that @{text c} is restricted to
    3.49 +  @{text \<nat>}.  This does not pose any problems since if @{text "f \<in> O(g)"} holds for
    3.50 +  a @{text "c \<in> \<real>"}, it also holds for @{text "\<lceil>c\<rceil> \<in> \<nat>"} by transitivity.
    3.51 +*}
    3.52 +
    3.53 +lemma less_eq_funI [intro?]:
    3.54 +  assumes "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m"
    3.55 +  shows "f \<lesssim> g"
    3.56 +  unfolding less_eq_fun_def by (rule assms)
    3.57 +
    3.58 +lemma not_less_eq_funI:
    3.59 +  assumes "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * g m < f m"
    3.60 +  shows "\<not> f \<lesssim> g"
    3.61 +  using assms unfolding less_eq_fun_def linorder_not_le [symmetric] by blast
    3.62 +
    3.63 +lemma less_eq_funE [elim?]:
    3.64 +  assumes "f \<lesssim> g"
    3.65 +  obtains n c where "c > 0" and "\<And>m. m > n \<Longrightarrow> f m \<le> c * g m"
    3.66 +  using assms unfolding less_eq_fun_def by blast
    3.67 +
    3.68 +lemma not_less_eq_funE:
    3.69 +  assumes "\<not> f \<lesssim> g" and "c > 0"
    3.70 +  obtains m where "m > n" and "c * g m < f m"
    3.71 +  using assms unfolding less_eq_fun_def linorder_not_le [symmetric] by blast
    3.72 +
    3.73 +
    3.74 +subsection {* The @{text "\<approx>"} relation, the equivalence relation induced by @{text "\<lesssim>"} *}
    3.75 +
    3.76 +definition equiv_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<cong>" 50)
    3.77 +where
    3.78 +  "f \<cong> g \<longleftrightarrow>
    3.79 +    (\<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)"
    3.80 +
    3.81 +text {*
    3.82 +  This yields @{text "f \<cong> g \<longleftrightarrow> f \<in> \<Theta>(g)"}.  Concerning @{text "c\<^isub>1"} and @{text "c\<^isub>2"}
    3.83 +  restricted to @{typ nat}, see note above on @{text "(\<lesssim>)"}.
    3.84 +*}
    3.85 +
    3.86 +lemma equiv_funI [intro?]:
    3.87 +  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"
    3.88 +  shows "f \<cong> g"
    3.89 +  unfolding equiv_fun_def by (rule assms)
    3.90 +
    3.91 +lemma not_equiv_funI:
    3.92 +  assumes "\<And>c\<^isub>1 c\<^isub>2 n. c\<^isub>1 > 0 \<Longrightarrow> c\<^isub>2 > 0 \<Longrightarrow>
    3.93 +    \<exists>m>n. c\<^isub>1 * f m < g m \<or> c\<^isub>2 * g m < f m"
    3.94 +  shows "\<not> f \<cong> g"
    3.95 +  using assms unfolding equiv_fun_def linorder_not_le [symmetric] by blast
    3.96 +
    3.97 +lemma equiv_funE [elim?]:
    3.98 +  assumes "f \<cong> g"
    3.99 +  obtains n c\<^isub>1 c\<^isub>2 where "c\<^isub>1 > 0" and "c\<^isub>2 > 0"
   3.100 +    and "\<And>m. m > n \<Longrightarrow> f m \<le> c\<^isub>1 * g m \<and> g m \<le> c\<^isub>2 * f m"
   3.101 +  using assms unfolding equiv_fun_def by blast
   3.102 +
   3.103 +lemma not_equiv_funE:
   3.104 +  fixes n c\<^isub>1 c\<^isub>2
   3.105 +  assumes "\<not> f \<cong> g" and "c\<^isub>1 > 0" and "c\<^isub>2 > 0"
   3.106 +  obtains m where "m > n"
   3.107 +    and "c\<^isub>1 * f m < g m \<or> c\<^isub>2 * g m < f m"
   3.108 +  using assms unfolding equiv_fun_def linorder_not_le [symmetric] by blast
   3.109 +
   3.110 +
   3.111 +subsection {* The @{text "\<prec>"} relation, the strict part of @{text "\<lesssim>"} *}
   3.112 +
   3.113 +definition less_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<prec>" 50)
   3.114 +where
   3.115 +  "f \<prec> g \<longleftrightarrow> f \<lesssim> g \<and> \<not> g \<lesssim> f"
   3.116 +
   3.117 +lemma less_funI:
   3.118 +  assumes "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m"
   3.119 +    and "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * f m < g m"
   3.120 +  shows "f \<prec> g"
   3.121 +  using assms unfolding less_fun_def less_eq_fun_def linorder_not_less [symmetric] by blast
   3.122 +
   3.123 +lemma not_less_funI:
   3.124 +  assumes "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * g m < f m"
   3.125 +    and "\<exists>c>0. \<exists>n. \<forall>m>n. g m \<le> c * f m"
   3.126 +  shows "\<not> f \<prec> g"
   3.127 +  using assms unfolding less_fun_def less_eq_fun_def linorder_not_less [symmetric] by blast
   3.128 +
   3.129 +lemma less_funE [elim?]:
   3.130 +  assumes "f \<prec> g"
   3.131 +  obtains n c where "c > 0" and "\<And>m. m > n \<Longrightarrow> f m \<le> c * g m"
   3.132 +    and "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * f m < g m"
   3.133 +proof -
   3.134 +  from assms have "f \<lesssim> g" and "\<not> g \<lesssim> f" by (simp_all add: less_fun_def)
   3.135 +  from `f \<lesssim> g` obtain n c where *:"c > 0" "\<And>m. m > n \<Longrightarrow> f m \<le> c * g m"
   3.136 +    by (rule less_eq_funE) blast
   3.137 +  { fix c n :: nat
   3.138 +    assume "c > 0"
   3.139 +    with `\<not> g \<lesssim> f` obtain m where "m > n" "c * f m < g m"
   3.140 +      by (rule not_less_eq_funE) blast
   3.141 +    then have **: "\<exists>m>n. c * f m < g m" by blast
   3.142 +  } note ** = this
   3.143 +  from * ** show thesis by (rule that)
   3.144 +qed
   3.145 +
   3.146 +lemma not_less_funE:
   3.147 +  assumes "\<not> f \<prec> g" and "c > 0"
   3.148 +  obtains m where "m > n" and "c * g m < f m"
   3.149 +    | d q where "\<And>m. d > 0 \<Longrightarrow> m > q \<Longrightarrow> g q \<le> d * f q"
   3.150 +  using assms unfolding less_fun_def linorder_not_less [symmetric] by blast
   3.151 +
   3.152 +text {*
   3.153 +  I did not found a proof for @{text "f \<prec> g \<longleftrightarrow> f \<in> o(g)"}.  Maybe this only
   3.154 +  holds if @{text f} and/or @{text g} are of a certain class of functions.
   3.155 +  However @{text "f \<in> o(g) \<longrightarrow> f \<prec> g"} is provable, and this yields a
   3.156 +  handy introduction rule.
   3.157 +
   3.158 +  Note that D. Knuth ignores @{text o} altogether.  So what\<dots>
   3.159 +
   3.160 +  Something still has to be said about the coefficient @{text c} in
   3.161 +  the definition of @{text "(\<prec>)"}.  In the typical definition of @{text o},
   3.162 +  it occurs on the \emph{right} hand side of the @{text "(>)"}.  The reason
   3.163 +  is that the situation is dual to the definition of @{text O}: the definition
   3.164 +  works since @{text c} may become arbitrary small.  Since this is not possible
   3.165 +  within @{term \<nat>}, we push the coefficient to the left hand side instead such
   3.166 +  that it become arbitrary big instead.
   3.167 +*}
   3.168 +
   3.169 +lemma less_fun_strongI:
   3.170 +  assumes "\<And>c. c > 0 \<Longrightarrow> \<exists>n. \<forall>m>n. c * f m < g m"
   3.171 +  shows "f \<prec> g"
   3.172 +proof (rule less_funI)
   3.173 +  have "1 > (0::nat)" by simp
   3.174 +  from assms `1 > 0` have "\<exists>n. \<forall>m>n. 1 * f m < g m" .
   3.175 +  then obtain n where *: "\<And>m. m > n \<Longrightarrow> 1 * f m < g m" by blast
   3.176 +  have "\<forall>m>n. f m \<le> 1 * g m"
   3.177 +  proof (rule allI, rule impI)
   3.178 +    fix m
   3.179 +    assume "m > n"
   3.180 +    with * have "1 * f m < g m" by simp
   3.181 +    then show "f m \<le> 1 * g m" by simp
   3.182 +  qed
   3.183 +  with `1 > 0` show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m" by blast
   3.184 +  fix c n :: nat
   3.185 +  assume "c > 0"
   3.186 +  with assms obtain q where "\<And>m. m > q \<Longrightarrow> c * f m < g m" by blast
   3.187 +  then have "c * f (Suc (q + n)) < g (Suc (q + n))" by simp
   3.188 +  moreover have "Suc (q + n) > n" by simp
   3.189 +  ultimately show "\<exists>m>n. c * f m < g m" by blast
   3.190 +qed
   3.191 +
   3.192 +
   3.193 +subsection {* @{text "\<lesssim>"} is a preorder *}
   3.194 +
   3.195 +text {* This yields all lemmas relating @{text "\<lesssim>"}, @{text "\<prec>"} and @{text "\<cong>"}. *}
   3.196 +
   3.197 +interpretation fun_order: preorder_equiv less_eq_fun less_fun
   3.198 +  where "preorder_equiv.equiv less_eq_fun = equiv_fun"
   3.199 +proof -
   3.200 +  interpret preorder: preorder_equiv less_eq_fun less_fun
   3.201 +  proof
   3.202 +    fix f g h
   3.203 +    show "f \<lesssim> f"
   3.204 +    proof
   3.205 +      have "\<exists>n. \<forall>m>n. f m \<le> 1 * f m" by auto
   3.206 +      then show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * f m" by blast
   3.207 +    qed
   3.208 +    show "f \<prec> g \<longleftrightarrow> f \<lesssim> g \<and> \<not> g \<lesssim> f"
   3.209 +      by (fact less_fun_def)
   3.210 +    assume "f \<lesssim> g" and "g \<lesssim> h"
   3.211 +    show "f \<lesssim> h"
   3.212 +    proof
   3.213 +      from `f \<lesssim> g` obtain n\<^isub>1 c\<^isub>1
   3.214 +        where "c\<^isub>1 > 0" and P\<^isub>1: "\<And>m. m > n\<^isub>1 \<Longrightarrow> f m \<le> c\<^isub>1 * g m"
   3.215 +        by rule blast
   3.216 +      from `g \<lesssim> h` obtain n\<^isub>2 c\<^isub>2
   3.217 +        where "c\<^isub>2 > 0" and P\<^isub>2: "\<And>m. m > n\<^isub>2 \<Longrightarrow> g m \<le> c\<^isub>2 * h m"
   3.218 +        by rule blast
   3.219 +      have "\<forall>m>max n\<^isub>1 n\<^isub>2. f m \<le> (c\<^isub>1 * c\<^isub>2) * h m"
   3.220 +      proof (rule allI, rule impI)
   3.221 +        fix m
   3.222 +        assume Q: "m > max n\<^isub>1 n\<^isub>2"
   3.223 +        from P\<^isub>1 Q have *: "f m \<le> c\<^isub>1 * g m" by simp
   3.224 +        from P\<^isub>2 Q have "g m \<le> c\<^isub>2 * h m" by simp
   3.225 +        with `c\<^isub>1 > 0` have "c\<^isub>1 * g m \<le> (c\<^isub>1 * c\<^isub>2) * h m" by simp
   3.226 +        with * show "f m \<le> (c\<^isub>1 * c\<^isub>2) * h m" by (rule order_trans)
   3.227 +      qed
   3.228 +      then have "\<exists>n. \<forall>m>n. f m \<le> (c\<^isub>1 * c\<^isub>2) * h m" by rule
   3.229 +      moreover from `c\<^isub>1 > 0` `c\<^isub>2 > 0` have "c\<^isub>1 * c\<^isub>2 > 0" by (rule mult_pos_pos)
   3.230 +      ultimately show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * h m" by blast
   3.231 +    qed
   3.232 +  qed
   3.233 +  from preorder.preorder_equiv_axioms show "class.preorder_equiv less_eq_fun less_fun" .
   3.234 +  show "preorder_equiv.equiv less_eq_fun = equiv_fun"
   3.235 +  proof (rule ext, rule ext, unfold preorder.equiv_def)
   3.236 +    fix f g
   3.237 +    show "f \<lesssim> g \<and> g \<lesssim> f \<longleftrightarrow> f \<cong> g"
   3.238 +    proof
   3.239 +      assume "f \<cong> g"
   3.240 +      then obtain n c\<^isub>1 c\<^isub>2 where "c\<^isub>1 > 0" and "c\<^isub>2 > 0"
   3.241 +        and *: "\<And>m. m > n \<Longrightarrow> f m \<le> c\<^isub>1 * g m \<and> g m \<le> c\<^isub>2 * f m"
   3.242 +        by rule blast
   3.243 +      have "\<forall>m>n. f m \<le> c\<^isub>1 * g m"
   3.244 +      proof (rule allI, rule impI)
   3.245 +        fix m
   3.246 +        assume "m > n"
   3.247 +        with * show "f m \<le> c\<^isub>1 * g m" by simp
   3.248 +      qed
   3.249 +      with `c\<^isub>1 > 0` have "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m" by blast
   3.250 +      then have "f \<lesssim> g" ..
   3.251 +      have "\<forall>m>n. g m \<le> c\<^isub>2 * f m"
   3.252 +      proof (rule allI, rule impI)
   3.253 +        fix m
   3.254 +        assume "m > n"
   3.255 +        with * show "g m \<le> c\<^isub>2 * f m" by simp
   3.256 +      qed
   3.257 +      with `c\<^isub>2 > 0` have "\<exists>c>0. \<exists>n. \<forall>m>n. g m \<le> c * f m" by blast
   3.258 +      then have "g \<lesssim> f" ..
   3.259 +      from `f \<lesssim> g` and `g \<lesssim> f` show "f \<lesssim> g \<and> g \<lesssim> f" ..
   3.260 +    next
   3.261 +      assume "f \<lesssim> g \<and> g \<lesssim> f"
   3.262 +      then have "f \<lesssim> g" and "g \<lesssim> f" by auto
   3.263 +      from `f \<lesssim> g` obtain n\<^isub>1 c\<^isub>1 where "c\<^isub>1 > 0"
   3.264 +        and P\<^isub>1: "\<And>m. m > n\<^isub>1 \<Longrightarrow> f m \<le> c\<^isub>1 * g m" by rule blast
   3.265 +      from `g \<lesssim> f` obtain n\<^isub>2 c\<^isub>2 where "c\<^isub>2 > 0"
   3.266 +        and P\<^isub>2: "\<And>m. m > n\<^isub>2 \<Longrightarrow> g m \<le> c\<^isub>2 * f m" by rule blast
   3.267 +      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"
   3.268 +      proof (rule allI, rule impI)
   3.269 +        fix m
   3.270 +        assume Q: "m > max n\<^isub>1 n\<^isub>2"
   3.271 +        from P\<^isub>1 Q have "f m \<le> c\<^isub>1 * g m" by simp
   3.272 +        moreover from P\<^isub>2 Q have "g m \<le> c\<^isub>2 * f m" by simp
   3.273 +        ultimately show "f m \<le> c\<^isub>1 * g m \<and> g m \<le> c\<^isub>2 * f m" ..
   3.274 +      qed
   3.275 +      with `c\<^isub>1 > 0` `c\<^isub>2 > 0` have "\<exists>c\<^isub>1>0. \<exists>c\<^isub>2>0. \<exists>n.
   3.276 +        \<forall>m>n. f m \<le> c\<^isub>1 * g m \<and> g m \<le> c\<^isub>2 * f m" by blast
   3.277 +      then show "f \<cong> g" ..
   3.278 +    qed
   3.279 +  qed
   3.280 +qed
   3.281 +
   3.282 +
   3.283 +subsection {* Simple examples *}
   3.284 +
   3.285 +text {*
   3.286 +  Most of these are left as constructive exercises for the reader.  Note that additional
   3.287 +  preconditions to the functions may be necessary.  The list here is by no means to be
   3.288 +  intended as complete contruction set for typical functions, here surely something
   3.289 +  has to be added yet.
   3.290 +*}
   3.291 +
   3.292 +text {* @{prop "(\<lambda>n. f n + k) \<cong> f"} *}
   3.293 +
   3.294 +text {* @{prop "(\<lambda>n. Suc k * f n) \<cong> f"} *}
   3.295 +
   3.296 +lemma "f \<lesssim> (\<lambda>n. f n + g n)"
   3.297 +by rule auto
   3.298 +
   3.299 +lemma "(\<lambda>_. 0) \<prec> (\<lambda>n. Suc k)"
   3.300 +by (rule less_fun_strongI) auto
   3.301 +
   3.302 +lemma "(\<lambda>_. k) \<prec> Discrete.log"
   3.303 +proof (rule less_fun_strongI)
   3.304 +  fix c :: nat
   3.305 +  have "\<forall>m>2 ^ (Suc (c * k)). c * k < Discrete.log m"
   3.306 +  proof (rule allI, rule impI)
   3.307 +    fix m :: nat
   3.308 +    assume "2 ^ Suc (c * k) < m"
   3.309 +    then have "2 ^ Suc (c * k) \<le> m" by simp
   3.310 +    with log_mono have "Discrete.log (2 ^ (Suc (c * k))) \<le> Discrete.log m"
   3.311 +      by (blast dest: monoD)
   3.312 +    moreover have "c * k < Discrete.log (2 ^ (Suc (c * k)))" by simp
   3.313 +    ultimately show "c * k < Discrete.log m" by auto
   3.314 +  qed
   3.315 +  then show "\<exists>n. \<forall>m>n. c * k < Discrete.log m" ..
   3.316 +qed
   3.317 +  
   3.318 +text {* @{prop "Discrete.log \<prec> Discrete.sqrt"} *}
   3.319 +
   3.320 +lemma "Discrete.sqrt \<prec> id"
   3.321 +proof (rule less_fun_strongI)
   3.322 +  fix c :: nat
   3.323 +  assume "0 < c"
   3.324 +  have "\<forall>m>(Suc c)\<twosuperior>. c * Discrete.sqrt m < id m"
   3.325 +  proof (rule allI, rule impI)
   3.326 +    fix m
   3.327 +    assume "(Suc c)\<twosuperior> < m"
   3.328 +    then have "(Suc c)\<twosuperior> \<le> m" by simp
   3.329 +    with mono_sqrt have "Discrete.sqrt ((Suc c)\<twosuperior>) \<le> Discrete.sqrt m" by (rule monoE)
   3.330 +    then have "Suc c \<le> Discrete.sqrt m" by simp
   3.331 +    then have "c < Discrete.sqrt m" by simp
   3.332 +    moreover from `(Suc c)\<twosuperior> < m` have "Discrete.sqrt m > 0" by simp
   3.333 +    ultimately have "c * Discrete.sqrt m < Discrete.sqrt m * Discrete.sqrt m" by simp
   3.334 +    also have "\<dots> \<le> m" by (simp add: power2_eq_square [symmetric])
   3.335 +    finally show "c * Discrete.sqrt m < id m" by simp
   3.336 +  qed
   3.337 +  then show "\<exists>n. \<forall>m>n. c * Discrete.sqrt m < id m" ..
   3.338 +qed
   3.339 +
   3.340 +lemma "id \<prec> (\<lambda>n. n\<twosuperior>)"
   3.341 +by (rule less_fun_strongI) (auto simp add: power2_eq_square)
   3.342 +
   3.343 +lemma "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. n ^ Suc k)"
   3.344 +by (rule less_fun_strongI) auto
   3.345 +
   3.346 +text {* @{prop "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. 2 ^ n)"} *}
   3.347 +
   3.348 +end
   3.349 +
     4.1 --- a/src/HOL/Library/Library.thy	Sun Feb 24 20:18:32 2013 +0100
     4.2 +++ b/src/HOL/Library/Library.thy	Sun Feb 24 20:29:13 2013 +0100
     4.3 @@ -15,7 +15,6 @@
     4.4    Countable_Set
     4.5    Debug
     4.6    Diagonal_Subsequence
     4.7 -  Discrete
     4.8    Dlist
     4.9    Eval_Witness
    4.10    Extended_Nat
    4.11 @@ -26,6 +25,7 @@
    4.12    FrechetDeriv
    4.13    FuncSet
    4.14    Function_Division
    4.15 +  Function_Growth
    4.16    Fundamental_Theorem_Algebra
    4.17    Indicator_Function
    4.18    Infinite_Set
     5.1 --- a/src/HOL/Nat.thy	Sun Feb 24 20:18:32 2013 +0100
     5.2 +++ b/src/HOL/Nat.thy	Sun Feb 24 20:29:13 2013 +0100
     5.3 @@ -1201,6 +1201,16 @@
     5.4      apply (auto)
     5.5    done
     5.6  
     5.7 +lemma mono_times_nat:
     5.8 +  fixes n :: nat
     5.9 +  assumes "n > 0"
    5.10 +  shows "mono (times n)"
    5.11 +proof
    5.12 +  fix m q :: nat
    5.13 +  assume "m \<le> q"
    5.14 +  with assms show "n * m \<le> n * q" by simp
    5.15 +qed
    5.16 +
    5.17  text {* the lattice order on @{typ nat} *}
    5.18  
    5.19  instantiation nat :: distrib_lattice
     6.1 --- a/src/HOL/Orderings.thy	Sun Feb 24 20:18:32 2013 +0100
     6.2 +++ b/src/HOL/Orderings.thy	Sun Feb 24 20:29:13 2013 +0100
     6.3 @@ -965,6 +965,15 @@
     6.4    shows "mono f \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
     6.5    unfolding mono_def by iprover
     6.6  
     6.7 +lemma monoE:
     6.8 +  fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
     6.9 +  assumes "mono f"
    6.10 +  assumes "x \<le> y"
    6.11 +  obtains "f x \<le> f y"
    6.12 +proof
    6.13 +  from assms show "f x \<le> f y" by (simp add: mono_def)
    6.14 +qed
    6.15 +
    6.16  definition strict_mono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool" where
    6.17    "strict_mono f \<longleftrightarrow> (\<forall>x y. x < y \<longrightarrow> f x < f y)"
    6.18  
    6.19 @@ -998,6 +1007,21 @@
    6.20  context linorder
    6.21  begin
    6.22  
    6.23 +lemma mono_invE:
    6.24 +  fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
    6.25 +  assumes "mono f"
    6.26 +  assumes "f x < f y"
    6.27 +  obtains "x \<le> y"
    6.28 +proof
    6.29 +  show "x \<le> y"
    6.30 +  proof (rule ccontr)
    6.31 +    assume "\<not> x \<le> y"
    6.32 +    then have "y \<le> x" by simp
    6.33 +    with `mono f` obtain "f y \<le> f x" by (rule monoE)
    6.34 +    with `f x < f y` show False by simp
    6.35 +  qed
    6.36 +qed
    6.37 +
    6.38  lemma strict_mono_eq:
    6.39    assumes "strict_mono f"
    6.40    shows "f x = f y \<longleftrightarrow> x = y"
     7.1 --- a/src/HOL/Power.thy	Sun Feb 24 20:18:32 2013 +0100
     7.2 +++ b/src/HOL/Power.thy	Sun Feb 24 20:29:13 2013 +0100
     7.3 @@ -721,6 +721,18 @@
     7.4    apply (erule dvd_imp_le, simp)
     7.5    done
     7.6  
     7.7 +lemma power2_nat_le_eq_le:
     7.8 +  fixes m n :: nat
     7.9 +  shows "m\<twosuperior> \<le> n\<twosuperior> \<longleftrightarrow> m \<le> n"
    7.10 +  by (auto intro: power2_le_imp_le power_mono)
    7.11 +
    7.12 +lemma power2_nat_le_imp_le:
    7.13 +  fixes m n :: nat
    7.14 +  assumes "m\<twosuperior> \<le> n"
    7.15 +  shows "m \<le> n"
    7.16 +  using assms by (cases m) (simp_all add: power2_eq_square)
    7.17 +
    7.18 +
    7.19  
    7.20  subsection {* Code generator tweak *}
    7.21  
     8.1 --- a/src/HOL/ROOT	Sun Feb 24 20:18:32 2013 +0100
     8.2 +++ b/src/HOL/ROOT	Sun Feb 24 20:29:13 2013 +0100
     8.3 @@ -455,7 +455,6 @@
     8.4      Transfer_Int_Nat
     8.5      HarmonicSeries
     8.6      Refute_Examples
     8.7 -    Landau
     8.8      Execute_Choice
     8.9      Summation
    8.10      Gauge_Integration
     9.1 --- a/src/HOL/ex/Landau.thy	Sun Feb 24 20:18:32 2013 +0100
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,226 +0,0 @@
     9.4 -
     9.5 -(* Author: Florian Haftmann, TU Muenchen *)
     9.6 -
     9.7 -header {* Comparing growth of functions on natural numbers by a preorder relation *}
     9.8 -
     9.9 -theory Landau
    9.10 -imports Main "~~/src/HOL/Library/Preorder"
    9.11 -begin
    9.12 -
    9.13 -text {*
    9.14 -  We establish a preorder releation @{text "\<lesssim>"} on functions from
    9.15 -  @{text "\<nat>"} to @{text "\<nat>"} such that @{text "f \<lesssim> g \<longleftrightarrow> f \<in> O(g)"}.
    9.16 -*}
    9.17 -
    9.18 -subsection {* Auxiliary *}
    9.19 -
    9.20 -lemma Ex_All_bounded:
    9.21 -  fixes n :: nat
    9.22 -  assumes "\<exists>n. \<forall>m\<ge>n. P m"
    9.23 -  obtains m where "m \<ge> n" and "P m"
    9.24 -proof -
    9.25 -  from assms obtain q where m_q: "\<forall>m\<ge>q. P m" ..
    9.26 -  let ?m = "max q n"
    9.27 -  have "?m \<ge> n" by auto
    9.28 -  moreover from m_q have "P ?m" by auto
    9.29 -  ultimately show thesis ..
    9.30 -qed
    9.31 -    
    9.32 -
    9.33 -subsection {* The @{text "\<lesssim>"} relation *}
    9.34 -
    9.35 -definition less_eq_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<lesssim>" 50) where
    9.36 -  "f \<lesssim> g \<longleftrightarrow> (\<exists>c n. \<forall>m\<ge>n. f m \<le> Suc c * g m)"
    9.37 -
    9.38 -lemma less_eq_fun_intro:
    9.39 -  assumes "\<exists>c n. \<forall>m\<ge>n. f m \<le> Suc c * g m"
    9.40 -  shows "f \<lesssim> g"
    9.41 -  unfolding less_eq_fun_def by (rule assms)
    9.42 -
    9.43 -lemma less_eq_fun_not_intro:
    9.44 -  assumes "\<And>c n. \<exists>m\<ge>n. Suc c * g m < f m"
    9.45 -  shows "\<not> f \<lesssim> g"
    9.46 -  using assms unfolding less_eq_fun_def linorder_not_le [symmetric]
    9.47 -  by blast
    9.48 -
    9.49 -lemma less_eq_fun_elim:
    9.50 -  assumes "f \<lesssim> g"
    9.51 -  obtains n c where "\<And>m. m \<ge> n \<Longrightarrow> f m \<le> Suc c * g m"
    9.52 -  using assms unfolding less_eq_fun_def by blast
    9.53 -
    9.54 -lemma less_eq_fun_not_elim:
    9.55 -  assumes "\<not> f \<lesssim> g"
    9.56 -  obtains m where "m \<ge> n" and "Suc c * g m < f m"
    9.57 -  using assms unfolding less_eq_fun_def linorder_not_le [symmetric]
    9.58 -  by blast
    9.59 -
    9.60 -lemma less_eq_fun_refl:
    9.61 -  "f \<lesssim> f"
    9.62 -proof (rule less_eq_fun_intro)
    9.63 -  have "\<exists>n. \<forall>m\<ge>n. f m \<le> Suc 0 * f m" by auto
    9.64 -  then show "\<exists>c n. \<forall>m\<ge>n. f m \<le> Suc c * f m" by blast
    9.65 -qed
    9.66 -
    9.67 -lemma less_eq_fun_trans:
    9.68 -  assumes f_g: "f \<lesssim> g" and g_h: "g \<lesssim> h"
    9.69 -  shows f_h: "f \<lesssim> h"
    9.70 -proof -
    9.71 -  from f_g obtain n\<^isub>1 c\<^isub>1
    9.72 -    where P1: "\<And>m. m \<ge> n\<^isub>1 \<Longrightarrow> f m \<le> Suc c\<^isub>1 * g m"
    9.73 -  by (erule less_eq_fun_elim)
    9.74 -  moreover from g_h obtain n\<^isub>2 c\<^isub>2
    9.75 -    where P2: "\<And>m. m \<ge> n\<^isub>2 \<Longrightarrow> g m \<le> Suc c\<^isub>2 * h m"
    9.76 -  by (erule less_eq_fun_elim)
    9.77 -  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"
    9.78 -  by auto
    9.79 -  moreover {
    9.80 -    fix k l r :: nat
    9.81 -    assume k_l: "k \<le> Suc c\<^isub>1 * l" and l_r: "l \<le> Suc c\<^isub>2 * r"
    9.82 -    from l_r have "Suc c\<^isub>1 * l \<le> (Suc c\<^isub>1 * Suc c\<^isub>2) * r"
    9.83 -    by (auto simp add: mult_le_cancel_left mult_assoc simp del: times_nat.simps mult_Suc_right)
    9.84 -    with k_l have "k \<le> (Suc c\<^isub>1 * Suc c\<^isub>2) * r" by (rule preorder_class.order_trans)
    9.85 -  }
    9.86 -  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
    9.87 -  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
    9.88 -  then show ?thesis unfolding less_eq_fun_def by blast
    9.89 -qed
    9.90 -
    9.91 -
    9.92 -subsection {* The @{text "\<approx>"} relation, the equivalence relation induced by @{text "\<lesssim>"} *}
    9.93 -
    9.94 -definition equiv_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<cong>" 50) where
    9.95 -  "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)"
    9.96 -
    9.97 -lemma equiv_fun_intro:
    9.98 -  assumes "\<exists>d c n. \<forall>m\<ge>n. g m \<le> Suc d * f m \<and> f m \<le> Suc c * g m"
    9.99 -  shows "f \<cong> g"
   9.100 -  unfolding equiv_fun_def by (rule assms)
   9.101 -
   9.102 -lemma equiv_fun_not_intro:
   9.103 -  assumes "\<And>d c n. \<exists>m\<ge>n. Suc d * f m < g m \<or> Suc c * g m < f m"
   9.104 -  shows "\<not> f \<cong> g"
   9.105 -  unfolding equiv_fun_def
   9.106 -  by (auto simp add: assms linorder_not_le
   9.107 -    simp del: times_nat.simps mult_Suc_right)
   9.108 -
   9.109 -lemma equiv_fun_elim:
   9.110 -  assumes "f \<cong> g"
   9.111 -  obtains n d c
   9.112 -    where "\<And>m. m \<ge> n \<Longrightarrow> g m \<le> Suc d * f m \<and> f m \<le> Suc c * g m"
   9.113 -  using assms unfolding equiv_fun_def by blast
   9.114 -
   9.115 -lemma equiv_fun_not_elim:
   9.116 -  fixes n d c
   9.117 -  assumes "\<not> f \<cong> g"
   9.118 -  obtains m where "m \<ge> n"
   9.119 -    and "Suc d * f m < g m \<or> Suc c * g m < f m"
   9.120 -  using assms unfolding equiv_fun_def
   9.121 -  by (auto simp add: linorder_not_le, blast)
   9.122 -
   9.123 -lemma equiv_fun_less_eq_fun:
   9.124 -  "f \<cong> g \<longleftrightarrow> f \<lesssim> g \<and> g \<lesssim> f"
   9.125 -proof
   9.126 -  assume x_y: "f \<cong> g"
   9.127 -  then obtain n d c
   9.128 -    where interv: "\<And>m. m \<ge> n \<Longrightarrow> g m \<le> Suc d * f m \<and> f m \<le> Suc c * g m"
   9.129 -  by (erule equiv_fun_elim)
   9.130 -  from interv have "\<exists>c n. \<forall>m \<ge> n. f m \<le> Suc c * g m" by auto
   9.131 -  then have f_g: "f \<lesssim> g" by (rule less_eq_fun_intro)
   9.132 -  from interv have "\<exists>d n. \<forall>m \<ge> n. g m \<le> Suc d * f m" by auto
   9.133 -  then have g_f: "g \<lesssim> f" by (rule less_eq_fun_intro)
   9.134 -  from f_g g_f show "f \<lesssim> g \<and> g \<lesssim> f" by auto
   9.135 -next
   9.136 -  assume assm: "f \<lesssim> g \<and> g \<lesssim> f"
   9.137 -  from assm less_eq_fun_elim obtain c n\<^isub>1 where
   9.138 -    bound1: "\<And>m. m \<ge> n\<^isub>1 \<Longrightarrow> f m \<le> Suc c * g m" 
   9.139 -    by blast
   9.140 -  from assm less_eq_fun_elim obtain d n\<^isub>2 where
   9.141 -    bound2: "\<And>m. m \<ge> n\<^isub>2 \<Longrightarrow> g m \<le> Suc d * f m"
   9.142 -    by blast
   9.143 -  from bound2 have "\<And>m. m \<ge> max n\<^isub>1 n\<^isub>2 \<Longrightarrow> g m \<le> Suc d * f m"
   9.144 -  by auto
   9.145 -  with bound1
   9.146 -    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"
   9.147 -    by auto
   9.148 -  then
   9.149 -    have "\<exists>d c n. \<forall>m\<ge>n. g m \<le> Suc d * f m \<and> f m \<le> Suc c * g m"
   9.150 -    by blast
   9.151 -  then show "f \<cong> g" by (rule equiv_fun_intro)
   9.152 -qed
   9.153 -
   9.154 -subsection {* The @{text "\<prec>"} relation, the strict part of @{text "\<lesssim>"} *}
   9.155 -
   9.156 -definition less_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<prec>" 50) where
   9.157 -  "f \<prec> g \<longleftrightarrow> f \<lesssim> g \<and> \<not> g \<lesssim> f"
   9.158 -
   9.159 -lemma less_fun_intro:
   9.160 -  assumes "\<And>c. \<exists>n. \<forall>m\<ge>n. Suc c * f m < g m"
   9.161 -  shows "f \<prec> g"
   9.162 -proof (unfold less_fun_def, rule conjI)
   9.163 -  from assms obtain n
   9.164 -    where "\<forall>m\<ge>n. Suc 0 * f m < g m" ..
   9.165 -  then have "\<forall>m\<ge>n. f m \<le> Suc 0 * g m" by auto
   9.166 -  then have "\<exists>c n. \<forall>m\<ge>n. f m \<le> Suc c * g m" by blast
   9.167 -  then show "f \<lesssim> g" by (rule less_eq_fun_intro)
   9.168 -next
   9.169 -  show "\<not> g \<lesssim> f"
   9.170 -  proof (rule less_eq_fun_not_intro)
   9.171 -    fix c n :: nat
   9.172 -    from assms have "\<exists>n. \<forall>m\<ge>n. Suc c * f m < g m" by blast
   9.173 -    then obtain m where "m \<ge> n" and "Suc c * f m < g m"
   9.174 -      by (rule Ex_All_bounded)
   9.175 -    then show "\<exists>m\<ge>n. Suc c * f m < g m" by blast
   9.176 -  qed
   9.177 -qed
   9.178 -
   9.179 -text {*
   9.180 -  We would like to show (or refute) that @{text "f \<prec> g \<longleftrightarrow> f \<in> o(g)"},
   9.181 -  i.e.~@{prop "f \<prec> g \<longleftrightarrow> (\<forall>c. \<exists>n. \<forall>m>n. f m < Suc c * g m)"} but did not
   9.182 -  manage to do so.
   9.183 -*}
   9.184 -
   9.185 -
   9.186 -subsection {* Assert that @{text "\<lesssim>"} is indeed a preorder *}
   9.187 -
   9.188 -interpretation fun_order: preorder_equiv less_eq_fun less_fun
   9.189 -  where "preorder_equiv.equiv less_eq_fun = equiv_fun"
   9.190 -proof -
   9.191 -  interpret preorder_equiv less_eq_fun less_fun proof
   9.192 -  qed (simp_all add: less_fun_def less_eq_fun_refl, auto intro: less_eq_fun_trans)
   9.193 -  show "class.preorder_equiv less_eq_fun less_fun" using preorder_equiv_axioms .
   9.194 -  show "preorder_equiv.equiv less_eq_fun = equiv_fun"
   9.195 -    by (simp add: fun_eq_iff equiv_def equiv_fun_less_eq_fun)
   9.196 -qed
   9.197 -
   9.198 -
   9.199 -subsection {* Simple examples *}
   9.200 -
   9.201 -lemma "(\<lambda>_. n) \<lesssim> (\<lambda>n. n)"
   9.202 -proof (rule less_eq_fun_intro)
   9.203 -  show "\<exists>c q. \<forall>m\<ge>q. n \<le> Suc c * m"
   9.204 -  proof -
   9.205 -    have "\<forall>m\<ge>n. n \<le> Suc 0 * m" by simp
   9.206 -    then show ?thesis by blast
   9.207 -  qed
   9.208 -qed
   9.209 -
   9.210 -lemma "(\<lambda>n. n) \<cong> (\<lambda>n. Suc k * n)"
   9.211 -proof (rule equiv_fun_intro)
   9.212 -  show "\<exists>d c n. \<forall>m\<ge>n. Suc k * m \<le> Suc d * m \<and> m \<le> Suc c * (Suc k * m)"
   9.213 -  proof -
   9.214 -    have "\<forall>m\<ge>n. Suc k * m \<le> Suc k * m \<and> m \<le> Suc c * (Suc k * m)" by simp
   9.215 -    then show ?thesis by blast
   9.216 -  qed
   9.217 -qed  
   9.218 -
   9.219 -lemma "(\<lambda>_. n) \<prec> (\<lambda>n. n)"
   9.220 -proof (rule less_fun_intro)
   9.221 -  fix c
   9.222 -  show "\<exists>q. \<forall>m\<ge>q. Suc c * n < m"
   9.223 -  proof -
   9.224 -    have "\<forall>m\<ge>Suc c * n + 1. Suc c * n < m" by simp
   9.225 -    then show ?thesis by blast
   9.226 -  qed
   9.227 -qed
   9.228 -
   9.229 -end