author haftmann Sun Feb 24 20:29:13 2013 +0100 (2013-02-24) changeset 51263 31e786e0e6a7 parent 51262 e2bdfb2de028 child 51264 aba03f0c6254
turned example into library for comparing growth of functions
 src/HOL/Big_Operators.thy file | annotate | diff | revisions src/HOL/Library/Discrete.thy file | annotate | diff | revisions src/HOL/Library/Function_Growth.thy file | annotate | diff | revisions src/HOL/Library/Library.thy file | annotate | diff | revisions src/HOL/Nat.thy file | annotate | diff | revisions src/HOL/Orderings.thy file | annotate | diff | revisions src/HOL/Power.thy file | annotate | diff | revisions src/HOL/ROOT file | annotate | diff | revisions src/HOL/ex/Landau.thy file | annotate | diff | revisions
     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