src/HOL/ex/Function_Growth.thy
 changeset 66797 9c9baae29217 parent 63540 f8652d0534fa child 66936 cf8d8fc23891
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/ex/Function_Growth.thy	Sun Oct 08 22:28:19 2017 +0200
1.3 @@ -0,0 +1,457 @@
1.4 +
1.5 +(* Author: Florian Haftmann, TU Muenchen *)
1.6 +
1.7 +section \<open>Comparing growth of functions on natural numbers by a preorder relation\<close>
1.8 +
1.9 +theory Function_Growth
1.10 +imports
1.11 +  Main
1.12 +  "HOL-Library.Preorder"
1.13 +  "HOL-Library.Discrete"
1.14 +begin
1.15 +
1.16 +(* FIXME move *)
1.17 +
1.18 +context linorder
1.19 +begin
1.20 +
1.21 +lemma mono_invE:
1.22 +  fixes f :: "'a \<Rightarrow> 'b::order"
1.23 +  assumes "mono f"
1.24 +  assumes "f x < f y"
1.25 +  obtains "x < y"
1.26 +proof
1.27 +  show "x < y"
1.28 +  proof (rule ccontr)
1.29 +    assume "\<not> x < y"
1.30 +    then have "y \<le> x" by simp
1.31 +    with \<open>mono f\<close> obtain "f y \<le> f x" by (rule monoE)
1.32 +    with \<open>f x < f y\<close> show False by simp
1.33 +  qed
1.34 +qed
1.35 +
1.36 +end
1.37 +
1.38 +lemma (in semidom_divide) power_diff:
1.39 +  fixes a :: 'a
1.40 +  assumes "a \<noteq> 0"
1.41 +  assumes "m \<ge> n"
1.42 +  shows "a ^ (m - n) = (a ^ m) div (a ^ n)"
1.43 +proof -
1.44 +  define q where "q = m - n"
1.45 +  with assms have "m = q + n" by (simp add: q_def)
1.46 +  with q_def show ?thesis using \<open>a \<noteq> 0\<close> by (simp add: power_add)
1.47 +qed
1.48 +
1.49 +
1.50 +subsection \<open>Motivation\<close>
1.51 +
1.52 +text \<open>
1.53 +  When comparing growth of functions in computer science, it is common to adhere
1.54 +  on Landau Symbols (O-Notation'').  However these come at the cost of notational
1.55 +  oddities, particularly writing \<open>f = O(g)\<close> for \<open>f \<in> O(g)\<close> etc.
1.56 +
1.57 +  Here we suggest a different way, following Hardy (G.~H.~Hardy and J.~E.~Littlewood,
1.58 +  Some problems of Diophantine approximation, Acta Mathematica 37 (1914), p.~225).
1.59 +  We establish a quasi order relation \<open>\<lesssim>\<close> on functions such that
1.60 +  \<open>f \<lesssim> g \<longleftrightarrow> f \<in> O(g)\<close>.  From a didactic point of view, this does not only
1.61 +  avoid the notational oddities mentioned above but also emphasizes the key insight
1.62 +  of a growth hierarchy of functions:
1.63 +  \<open>(\<lambda>n. 0) \<lesssim> (\<lambda>n. k) \<lesssim> Discrete.log \<lesssim> Discrete.sqrt \<lesssim> id \<lesssim> \<dots>\<close>.
1.64 +\<close>
1.65 +
1.66 +subsection \<open>Model\<close>
1.67 +
1.68 +text \<open>
1.69 +  Our growth functions are of type \<open>\<nat> \<Rightarrow> \<nat>\<close>.  This is different
1.70 +  to the usual conventions for Landau symbols for which \<open>\<real> \<Rightarrow> \<real>\<close>
1.71 +  would be appropriate, but we argue that \<open>\<real> \<Rightarrow> \<real>\<close> is more
1.72 +  appropriate for analysis, whereas our setting is discrete.
1.73 +
1.74 +  Note that we also restrict the additional coefficients to \<open>\<nat>\<close>, something
1.75 +  we discuss at the particular definitions.
1.76 +\<close>
1.77 +
1.78 +subsection \<open>The \<open>\<lesssim>\<close> relation\<close>
1.79 +
1.80 +definition less_eq_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<lesssim>" 50)
1.81 +where
1.82 +  "f \<lesssim> g \<longleftrightarrow> (\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m)"
1.83 +
1.84 +text \<open>
1.85 +  This yields \<open>f \<lesssim> g \<longleftrightarrow> f \<in> O(g)\<close>.  Note that \<open>c\<close> is restricted to
1.86 +  \<open>\<nat>\<close>.  This does not pose any problems since if \<open>f \<in> O(g)\<close> holds for
1.87 +  a \<open>c \<in> \<real>\<close>, it also holds for \<open>\<lceil>c\<rceil> \<in> \<nat>\<close> by transitivity.
1.88 +\<close>
1.89 +
1.90 +lemma less_eq_funI [intro?]:
1.91 +  assumes "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m"
1.92 +  shows "f \<lesssim> g"
1.93 +  unfolding less_eq_fun_def by (rule assms)
1.94 +
1.95 +lemma not_less_eq_funI:
1.96 +  assumes "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * g m < f m"
1.97 +  shows "\<not> f \<lesssim> g"
1.98 +  using assms unfolding less_eq_fun_def linorder_not_le [symmetric] by blast
1.99 +
1.100 +lemma less_eq_funE [elim?]:
1.101 +  assumes "f \<lesssim> g"
1.102 +  obtains n c where "c > 0" and "\<And>m. m > n \<Longrightarrow> f m \<le> c * g m"
1.103 +  using assms unfolding less_eq_fun_def by blast
1.104 +
1.105 +lemma not_less_eq_funE:
1.106 +  assumes "\<not> f \<lesssim> g" and "c > 0"
1.107 +  obtains m where "m > n" and "c * g m < f m"
1.108 +  using assms unfolding less_eq_fun_def linorder_not_le [symmetric] by blast
1.109 +
1.110 +
1.111 +subsection \<open>The \<open>\<approx>\<close> relation, the equivalence relation induced by \<open>\<lesssim>\<close>\<close>
1.112 +
1.113 +definition equiv_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<cong>" 50)
1.114 +where
1.115 +  "f \<cong> g \<longleftrightarrow>
1.116 +    (\<exists>c\<^sub>1>0. \<exists>c\<^sub>2>0. \<exists>n. \<forall>m>n. f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m)"
1.117 +
1.118 +text \<open>
1.119 +  This yields \<open>f \<cong> g \<longleftrightarrow> f \<in> \<Theta>(g)\<close>.  Concerning \<open>c\<^sub>1\<close> and \<open>c\<^sub>2\<close>
1.120 +  restricted to @{typ nat}, see note above on \<open>(\<lesssim>)\<close>.
1.121 +\<close>
1.122 +
1.123 +lemma equiv_funI:
1.124 +  assumes "\<exists>c\<^sub>1>0. \<exists>c\<^sub>2>0. \<exists>n. \<forall>m>n. f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m"
1.125 +  shows "f \<cong> g"
1.126 +  unfolding equiv_fun_def by (rule assms)
1.127 +
1.128 +lemma not_equiv_funI:
1.129 +  assumes "\<And>c\<^sub>1 c\<^sub>2 n. c\<^sub>1 > 0 \<Longrightarrow> c\<^sub>2 > 0 \<Longrightarrow>
1.130 +    \<exists>m>n. c\<^sub>1 * f m < g m \<or> c\<^sub>2 * g m < f m"
1.131 +  shows "\<not> f \<cong> g"
1.132 +  using assms unfolding equiv_fun_def linorder_not_le [symmetric] by blast
1.133 +
1.134 +lemma equiv_funE:
1.135 +  assumes "f \<cong> g"
1.136 +  obtains n c\<^sub>1 c\<^sub>2 where "c\<^sub>1 > 0" and "c\<^sub>2 > 0"
1.137 +    and "\<And>m. m > n \<Longrightarrow> f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m"
1.138 +  using assms unfolding equiv_fun_def by blast
1.139 +
1.140 +lemma not_equiv_funE:
1.141 +  fixes n c\<^sub>1 c\<^sub>2
1.142 +  assumes "\<not> f \<cong> g" and "c\<^sub>1 > 0" and "c\<^sub>2 > 0"
1.143 +  obtains m where "m > n"
1.144 +    and "c\<^sub>1 * f m < g m \<or> c\<^sub>2 * g m < f m"
1.145 +  using assms unfolding equiv_fun_def linorder_not_le [symmetric] by blast
1.146 +
1.147 +
1.148 +subsection \<open>The \<open>\<prec>\<close> relation, the strict part of \<open>\<lesssim>\<close>\<close>
1.149 +
1.150 +definition less_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<prec>" 50)
1.151 +where
1.152 +  "f \<prec> g \<longleftrightarrow> f \<lesssim> g \<and> \<not> g \<lesssim> f"
1.153 +
1.154 +lemma less_funI:
1.155 +  assumes "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m"
1.156 +    and "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * f m < g m"
1.157 +  shows "f \<prec> g"
1.158 +  using assms unfolding less_fun_def less_eq_fun_def linorder_not_less [symmetric] by blast
1.159 +
1.160 +lemma not_less_funI:
1.161 +  assumes "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * g m < f m"
1.162 +    and "\<exists>c>0. \<exists>n. \<forall>m>n. g m \<le> c * f m"
1.163 +  shows "\<not> f \<prec> g"
1.164 +  using assms unfolding less_fun_def less_eq_fun_def linorder_not_less [symmetric] by blast
1.165 +
1.166 +lemma less_funE [elim?]:
1.167 +  assumes "f \<prec> g"
1.168 +  obtains n c where "c > 0" and "\<And>m. m > n \<Longrightarrow> f m \<le> c * g m"
1.169 +    and "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * f m < g m"
1.170 +proof -
1.171 +  from assms have "f \<lesssim> g" and "\<not> g \<lesssim> f" by (simp_all add: less_fun_def)
1.172 +  from \<open>f \<lesssim> g\<close> obtain n c where *:"c > 0" "m > n \<Longrightarrow> f m \<le> c * g m" for m
1.173 +    by (rule less_eq_funE) blast
1.174 +  { fix c n :: nat
1.175 +    assume "c > 0"
1.176 +    with \<open>\<not> g \<lesssim> f\<close> obtain m where "m > n" "c * f m < g m"
1.177 +      by (rule not_less_eq_funE) blast
1.178 +    then have **: "\<exists>m>n. c * f m < g m" by blast
1.179 +  } note ** = this
1.180 +  from * ** show thesis by (rule that)
1.181 +qed
1.182 +
1.183 +lemma not_less_funE:
1.184 +  assumes "\<not> f \<prec> g" and "c > 0"
1.185 +  obtains m where "m > n" and "c * g m < f m"
1.186 +    | d q where "\<And>m. d > 0 \<Longrightarrow> m > q \<Longrightarrow> g q \<le> d * f q"
1.187 +  using assms unfolding less_fun_def linorder_not_less [symmetric] by blast
1.188 +
1.189 +text \<open>
1.190 +  I did not find a proof for \<open>f \<prec> g \<longleftrightarrow> f \<in> o(g)\<close>.  Maybe this only
1.191 +  holds if \<open>f\<close> and/or \<open>g\<close> are of a certain class of functions.
1.192 +  However \<open>f \<in> o(g) \<longrightarrow> f \<prec> g\<close> is provable, and this yields a
1.193 +  handy introduction rule.
1.194 +
1.195 +  Note that D. Knuth ignores \<open>o\<close> altogether.  So what \dots
1.196 +
1.197 +  Something still has to be said about the coefficient \<open>c\<close> in
1.198 +  the definition of \<open>(\<prec>)\<close>.  In the typical definition of \<open>o\<close>,
1.199 +  it occurs on the \emph{right} hand side of the \<open>(>)\<close>.  The reason
1.200 +  is that the situation is dual to the definition of \<open>O\<close>: the definition
1.201 +  works since \<open>c\<close> may become arbitrary small.  Since this is not possible
1.202 +  within @{term \<nat>}, we push the coefficient to the left hand side instead such
1.203 +  that it may become arbitrary big instead.
1.204 +\<close>
1.205 +
1.206 +lemma less_fun_strongI:
1.207 +  assumes "\<And>c. c > 0 \<Longrightarrow> \<exists>n. \<forall>m>n. c * f m < g m"
1.208 +  shows "f \<prec> g"
1.209 +proof (rule less_funI)
1.210 +  have "1 > (0::nat)" by simp
1.211 +  with assms [OF this] obtain n where *: "m > n \<Longrightarrow> 1 * f m < g m" for m
1.212 +    by blast
1.213 +  have "\<forall>m>n. f m \<le> 1 * g m"
1.214 +  proof (rule allI, rule impI)
1.215 +    fix m
1.216 +    assume "m > n"
1.217 +    with * have "1 * f m < g m" by simp
1.218 +    then show "f m \<le> 1 * g m" by simp
1.219 +  qed
1.220 +  with \<open>1 > 0\<close> show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m" by blast
1.221 +  fix c n :: nat
1.222 +  assume "c > 0"
1.223 +  with assms obtain q where "m > q \<Longrightarrow> c * f m < g m" for m by blast
1.224 +  then have "c * f (Suc (q + n)) < g (Suc (q + n))" by simp
1.225 +  moreover have "Suc (q + n) > n" by simp
1.226 +  ultimately show "\<exists>m>n. c * f m < g m" by blast
1.227 +qed
1.228 +
1.229 +
1.230 +subsection \<open>\<open>\<lesssim>\<close> is a preorder\<close>
1.231 +
1.232 +text \<open>This yields all lemmas relating \<open>\<lesssim>\<close>, \<open>\<prec>\<close> and \<open>\<cong>\<close>.\<close>
1.233 +
1.234 +interpretation fun_order: preorder_equiv less_eq_fun less_fun
1.235 +  rewrites "fun_order.equiv = equiv_fun"
1.236 +proof -
1.237 +  interpret preorder: preorder_equiv less_eq_fun less_fun
1.238 +  proof
1.239 +    fix f g h
1.240 +    show "f \<lesssim> f"
1.241 +    proof
1.242 +      have "\<exists>n. \<forall>m>n. f m \<le> 1 * f m" by auto
1.243 +      then show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * f m" by blast
1.244 +    qed
1.245 +    show "f \<prec> g \<longleftrightarrow> f \<lesssim> g \<and> \<not> g \<lesssim> f"
1.246 +      by (fact less_fun_def)
1.247 +    assume "f \<lesssim> g" and "g \<lesssim> h"
1.248 +    show "f \<lesssim> h"
1.249 +    proof
1.250 +      from \<open>f \<lesssim> g\<close> obtain n\<^sub>1 c\<^sub>1
1.251 +        where "c\<^sub>1 > 0" and P\<^sub>1: "\<And>m. m > n\<^sub>1 \<Longrightarrow> f m \<le> c\<^sub>1 * g m"
1.252 +        by rule blast
1.253 +      from \<open>g \<lesssim> h\<close> obtain n\<^sub>2 c\<^sub>2
1.254 +        where "c\<^sub>2 > 0" and P\<^sub>2: "\<And>m. m > n\<^sub>2 \<Longrightarrow> g m \<le> c\<^sub>2 * h m"
1.255 +        by rule blast
1.256 +      have "\<forall>m>max n\<^sub>1 n\<^sub>2. f m \<le> (c\<^sub>1 * c\<^sub>2) * h m"
1.257 +      proof (rule allI, rule impI)
1.258 +        fix m
1.259 +        assume Q: "m > max n\<^sub>1 n\<^sub>2"
1.260 +        from P\<^sub>1 Q have *: "f m \<le> c\<^sub>1 * g m" by simp
1.261 +        from P\<^sub>2 Q have "g m \<le> c\<^sub>2 * h m" by simp
1.262 +        with \<open>c\<^sub>1 > 0\<close> have "c\<^sub>1 * g m \<le> (c\<^sub>1 * c\<^sub>2) * h m" by simp
1.263 +        with * show "f m \<le> (c\<^sub>1 * c\<^sub>2) * h m" by (rule order_trans)
1.264 +      qed
1.265 +      then have "\<exists>n. \<forall>m>n. f m \<le> (c\<^sub>1 * c\<^sub>2) * h m" by rule
1.266 +      moreover from \<open>c\<^sub>1 > 0\<close> \<open>c\<^sub>2 > 0\<close> have "c\<^sub>1 * c\<^sub>2 > 0" by simp
1.267 +      ultimately show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * h m" by blast
1.268 +    qed
1.269 +  qed
1.270 +  from preorder.preorder_equiv_axioms show "class.preorder_equiv less_eq_fun less_fun" .
1.271 +  show "preorder_equiv.equiv less_eq_fun = equiv_fun"
1.272 +  proof (rule ext, rule ext, unfold preorder.equiv_def)
1.273 +    fix f g
1.274 +    show "f \<lesssim> g \<and> g \<lesssim> f \<longleftrightarrow> f \<cong> g"
1.275 +    proof
1.276 +      assume "f \<cong> g"
1.277 +      then obtain n c\<^sub>1 c\<^sub>2 where "c\<^sub>1 > 0" and "c\<^sub>2 > 0"
1.278 +        and *: "\<And>m. m > n \<Longrightarrow> f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m"
1.279 +        by (rule equiv_funE) blast
1.280 +      have "\<forall>m>n. f m \<le> c\<^sub>1 * g m"
1.281 +      proof (rule allI, rule impI)
1.282 +        fix m
1.283 +        assume "m > n"
1.284 +        with * show "f m \<le> c\<^sub>1 * g m" by simp
1.285 +      qed
1.286 +      with \<open>c\<^sub>1 > 0\<close> have "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m" by blast
1.287 +      then have "f \<lesssim> g" ..
1.288 +      have "\<forall>m>n. g m \<le> c\<^sub>2 * f m"
1.289 +      proof (rule allI, rule impI)
1.290 +        fix m
1.291 +        assume "m > n"
1.292 +        with * show "g m \<le> c\<^sub>2 * f m" by simp
1.293 +      qed
1.294 +      with \<open>c\<^sub>2 > 0\<close> have "\<exists>c>0. \<exists>n. \<forall>m>n. g m \<le> c * f m" by blast
1.295 +      then have "g \<lesssim> f" ..
1.296 +      from \<open>f \<lesssim> g\<close> and \<open>g \<lesssim> f\<close> show "f \<lesssim> g \<and> g \<lesssim> f" ..
1.297 +    next
1.298 +      assume "f \<lesssim> g \<and> g \<lesssim> f"
1.299 +      then have "f \<lesssim> g" and "g \<lesssim> f" by auto
1.300 +      from \<open>f \<lesssim> g\<close> obtain n\<^sub>1 c\<^sub>1 where "c\<^sub>1 > 0"
1.301 +        and P\<^sub>1: "\<And>m. m > n\<^sub>1 \<Longrightarrow> f m \<le> c\<^sub>1 * g m" by rule blast
1.302 +      from \<open>g \<lesssim> f\<close> obtain n\<^sub>2 c\<^sub>2 where "c\<^sub>2 > 0"
1.303 +        and P\<^sub>2: "\<And>m. m > n\<^sub>2 \<Longrightarrow> g m \<le> c\<^sub>2 * f m" by rule blast
1.304 +      have "\<forall>m>max n\<^sub>1 n\<^sub>2. f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m"
1.305 +      proof (rule allI, rule impI)
1.306 +        fix m
1.307 +        assume Q: "m > max n\<^sub>1 n\<^sub>2"
1.308 +        from P\<^sub>1 Q have "f m \<le> c\<^sub>1 * g m" by simp
1.309 +        moreover from P\<^sub>2 Q have "g m \<le> c\<^sub>2 * f m" by simp
1.310 +        ultimately show "f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" ..
1.311 +      qed
1.312 +      with \<open>c\<^sub>1 > 0\<close> \<open>c\<^sub>2 > 0\<close> have "\<exists>c\<^sub>1>0. \<exists>c\<^sub>2>0. \<exists>n.
1.313 +        \<forall>m>n. f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" by blast
1.314 +      then show "f \<cong> g" by (rule equiv_funI)
1.315 +    qed
1.316 +  qed
1.317 +qed
1.318 +
1.319 +declare fun_order.antisym [intro?]
1.320 +
1.321 +
1.322 +subsection \<open>Simple examples\<close>
1.323 +
1.324 +text \<open>
1.325 +  Most of these are left as constructive exercises for the reader.  Note that additional
1.326 +  preconditions to the functions may be necessary.  The list here is by no means to be
1.327 +  intended as complete construction set for typical functions, here surely something
1.328 +  has to be added yet.
1.329 +\<close>
1.330 +
1.331 +text \<open>@{prop "(\<lambda>n. f n + k) \<cong> f"}\<close>
1.332 +
1.333 +lemma equiv_fun_mono_const:
1.334 +  assumes "mono f" and "\<exists>n. f n > 0"
1.335 +  shows "(\<lambda>n. f n + k) \<cong> f"
1.336 +proof (cases "k = 0")
1.337 +  case True then show ?thesis by simp
1.338 +next
1.339 +  case False
1.340 +  show ?thesis
1.341 +  proof
1.342 +    show "(\<lambda>n. f n + k) \<lesssim> f"
1.343 +    proof
1.344 +      from \<open>\<exists>n. f n > 0\<close> obtain n where "f n > 0" ..
1.345 +      have "\<forall>m>n. f m + k \<le> Suc k * f m"
1.346 +      proof (rule allI, rule impI)
1.347 +        fix m
1.348 +        assume "n < m"
1.349 +        with \<open>mono f\<close> have "f n \<le> f m"
1.350 +          using less_imp_le_nat monoE by blast
1.351 +        with  \<open>0 < f n\<close> have "0 < f m" by auto
1.352 +        then obtain l where "f m = Suc l" by (cases "f m") simp_all
1.353 +        then show "f m + k \<le> Suc k * f m" by simp
1.354 +      qed
1.355 +      then show "\<exists>c>0. \<exists>n. \<forall>m>n. f m + k \<le> c * f m" by blast
1.356 +    qed
1.357 +    show "f \<lesssim> (\<lambda>n. f n + k)"
1.358 +    proof
1.359 +      have "f m \<le> 1 * (f m + k)" for m by simp
1.360 +      then show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * (f m + k)" by blast
1.361 +    qed
1.362 +  qed
1.363 +qed
1.364 +
1.365 +lemma
1.366 +  assumes "strict_mono f"
1.367 +  shows "(\<lambda>n. f n + k) \<cong> f"
1.368 +proof (rule equiv_fun_mono_const)
1.369 +  from assms show "mono f" by (rule strict_mono_mono)
1.370 +  show "\<exists>n. 0 < f n"
1.371 +  proof (rule ccontr)
1.372 +    assume "\<not> (\<exists>n. 0 < f n)"
1.373 +    then have "\<And>n. f n = 0" by simp
1.374 +    then have "f 0 = f 1" by simp
1.375 +    moreover from \<open>strict_mono f\<close> have "f 0 < f 1"
1.376 +      by (simp add: strict_mono_def)
1.377 +    ultimately show False by simp
1.378 +  qed
1.379 +qed
1.380 +
1.381 +lemma
1.382 +  "(\<lambda>n. Suc k * f n) \<cong> f"
1.383 +proof
1.384 +  show "(\<lambda>n. Suc k * f n) \<lesssim> f"
1.385 +  proof
1.386 +    have "Suc k * f m \<le> Suc k * f m" for m by simp
1.387 +    then show "\<exists>c>0. \<exists>n. \<forall>m>n. Suc k * f m \<le> c * f m" by blast
1.388 +  qed
1.389 +  show "f \<lesssim> (\<lambda>n. Suc k * f n)"
1.390 +  proof
1.391 +    have "f m \<le> 1 * (Suc k * f m)" for m by simp
1.392 +    then show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * (Suc k * f m)" by blast
1.393 +  qed
1.394 +qed
1.395 +
1.396 +lemma
1.397 +  "f \<lesssim> (\<lambda>n. f n + g n)"
1.398 +  by rule auto
1.399 +
1.400 +lemma
1.401 +  "(\<lambda>_. 0) \<prec> (\<lambda>n. Suc k)"
1.402 +  by (rule less_fun_strongI) auto
1.403 +
1.404 +lemma
1.405 +  "(\<lambda>_. k) \<prec> Discrete.log"
1.406 +proof (rule less_fun_strongI)
1.407 +  fix c :: nat
1.408 +  have "\<forall>m>2 ^ (Suc (c * k)). c * k < Discrete.log m"
1.409 +  proof (rule allI, rule impI)
1.410 +    fix m :: nat
1.411 +    assume "2 ^ Suc (c * k) < m"
1.412 +    then have "2 ^ Suc (c * k) \<le> m" by simp
1.413 +    with log_mono have "Discrete.log (2 ^ (Suc (c * k))) \<le> Discrete.log m"
1.414 +      by (blast dest: monoD)
1.415 +    moreover have "c * k < Discrete.log (2 ^ (Suc (c * k)))" by simp
1.416 +    ultimately show "c * k < Discrete.log m" by auto
1.417 +  qed
1.418 +  then show "\<exists>n. \<forall>m>n. c * k < Discrete.log m" ..
1.419 +qed
1.420 +
1.421 +(*lemma
1.422 +  "Discrete.log \<prec> Discrete.sqrt"
1.423 +proof (rule less_fun_strongI)*)
1.424 +text \<open>@{prop "Discrete.log \<prec> Discrete.sqrt"}\<close>
1.425 +
1.426 +lemma
1.427 +  "Discrete.sqrt \<prec> id"
1.428 +proof (rule less_fun_strongI)
1.429 +  fix c :: nat
1.430 +  assume "0 < c"
1.431 +  have "\<forall>m>(Suc c)\<^sup>2. c * Discrete.sqrt m < id m"
1.432 +  proof (rule allI, rule impI)
1.433 +    fix m
1.434 +    assume "(Suc c)\<^sup>2 < m"
1.435 +    then have "(Suc c)\<^sup>2 \<le> m" by simp
1.436 +    with mono_sqrt have "Discrete.sqrt ((Suc c)\<^sup>2) \<le> Discrete.sqrt m" by (rule monoE)
1.437 +    then have "Suc c \<le> Discrete.sqrt m" by simp
1.438 +    then have "c < Discrete.sqrt m" by simp
1.439 +    moreover from \<open>(Suc c)\<^sup>2 < m\<close> have "Discrete.sqrt m > 0" by simp
1.440 +    ultimately have "c * Discrete.sqrt m < Discrete.sqrt m * Discrete.sqrt m" by simp
1.441 +    also have "\<dots> \<le> m" by (simp add: power2_eq_square [symmetric])
1.442 +    finally show "c * Discrete.sqrt m < id m" by simp
1.443 +  qed
1.444 +  then show "\<exists>n. \<forall>m>n. c * Discrete.sqrt m < id m" ..
1.445 +qed
1.446 +
1.447 +lemma
1.448 +  "id \<prec> (\<lambda>n. n\<^sup>2)"
1.449 +  by (rule less_fun_strongI) (auto simp add: power2_eq_square)
1.450 +
1.451 +lemma
1.452 +  "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. n ^ Suc k)"
1.453 +  by (rule less_fun_strongI) auto
1.454 +
1.455 +(*lemma
1.456 +  "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. 2 ^ n)"
1.457 +proof (rule less_fun_strongI)*)
1.458 +text \<open>@{prop "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. 2 ^ n)"}\<close>
1.459 +
1.460 +end