src/HOL/Library/Function_Growth.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 63540 f8652d0534fa
permissions -rw-r--r--
executable domain membership checks
     1   
     2 (* Author: Florian Haftmann, TU Muenchen *)
     3 
     4 section \<open>Comparing growth of functions on natural numbers by a preorder relation\<close>
     5 
     6 theory Function_Growth
     7 imports Main Preorder Discrete
     8 begin
     9 
    10 (* FIXME move *)
    11 
    12 context linorder
    13 begin
    14 
    15 lemma mono_invE:
    16   fixes f :: "'a \<Rightarrow> 'b::order"
    17   assumes "mono f"
    18   assumes "f x < f y"
    19   obtains "x < y"
    20 proof
    21   show "x < y"
    22   proof (rule ccontr)
    23     assume "\<not> x < y"
    24     then have "y \<le> x" by simp
    25     with \<open>mono f\<close> obtain "f y \<le> f x" by (rule monoE)
    26     with \<open>f x < f y\<close> show False by simp
    27   qed
    28 qed
    29 
    30 end
    31 
    32 lemma (in semidom_divide) power_diff:
    33   fixes a :: 'a
    34   assumes "a \<noteq> 0"
    35   assumes "m \<ge> n"
    36   shows "a ^ (m - n) = (a ^ m) div (a ^ n)"
    37 proof -
    38   define q where "q = m - n"
    39   with assms have "m = q + n" by (simp add: q_def)
    40   with q_def show ?thesis using \<open>a \<noteq> 0\<close> by (simp add: power_add)
    41 qed
    42 
    43 
    44 subsection \<open>Motivation\<close>
    45 
    46 text \<open>
    47   When comparing growth of functions in computer science, it is common to adhere
    48   on Landau Symbols (``O-Notation'').  However these come at the cost of notational
    49   oddities, particularly writing \<open>f = O(g)\<close> for \<open>f \<in> O(g)\<close> etc.
    50   
    51   Here we suggest a different way, following Hardy (G.~H.~Hardy and J.~E.~Littlewood,
    52   Some problems of Diophantine approximation, Acta Mathematica 37 (1914), p.~225).
    53   We establish a quasi order relation \<open>\<lesssim>\<close> on functions such that
    54   \<open>f \<lesssim> g \<longleftrightarrow> f \<in> O(g)\<close>.  From a didactic point of view, this does not only
    55   avoid the notational oddities mentioned above but also emphasizes the key insight
    56   of a growth hierarchy of functions:
    57   \<open>(\<lambda>n. 0) \<lesssim> (\<lambda>n. k) \<lesssim> Discrete.log \<lesssim> Discrete.sqrt \<lesssim> id \<lesssim> \<dots>\<close>.
    58 \<close>
    59 
    60 subsection \<open>Model\<close>
    61 
    62 text \<open>
    63   Our growth functions are of type \<open>\<nat> \<Rightarrow> \<nat>\<close>.  This is different
    64   to the usual conventions for Landau symbols for which \<open>\<real> \<Rightarrow> \<real>\<close>
    65   would be appropriate, but we argue that \<open>\<real> \<Rightarrow> \<real>\<close> is more
    66   appropriate for analysis, whereas our setting is discrete.
    67 
    68   Note that we also restrict the additional coefficients to \<open>\<nat>\<close>, something
    69   we discuss at the particular definitions.
    70 \<close>
    71 
    72 subsection \<open>The \<open>\<lesssim>\<close> relation\<close>
    73 
    74 definition less_eq_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<lesssim>" 50)
    75 where
    76   "f \<lesssim> g \<longleftrightarrow> (\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m)"
    77 
    78 text \<open>
    79   This yields \<open>f \<lesssim> g \<longleftrightarrow> f \<in> O(g)\<close>.  Note that \<open>c\<close> is restricted to
    80   \<open>\<nat>\<close>.  This does not pose any problems since if \<open>f \<in> O(g)\<close> holds for
    81   a \<open>c \<in> \<real>\<close>, it also holds for \<open>\<lceil>c\<rceil> \<in> \<nat>\<close> by transitivity.
    82 \<close>
    83 
    84 lemma less_eq_funI [intro?]:
    85   assumes "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m"
    86   shows "f \<lesssim> g"
    87   unfolding less_eq_fun_def by (rule assms)
    88 
    89 lemma not_less_eq_funI:
    90   assumes "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * g m < f m"
    91   shows "\<not> f \<lesssim> g"
    92   using assms unfolding less_eq_fun_def linorder_not_le [symmetric] by blast
    93 
    94 lemma less_eq_funE [elim?]:
    95   assumes "f \<lesssim> g"
    96   obtains n c where "c > 0" and "\<And>m. m > n \<Longrightarrow> f m \<le> c * g m"
    97   using assms unfolding less_eq_fun_def by blast
    98 
    99 lemma not_less_eq_funE:
   100   assumes "\<not> f \<lesssim> g" and "c > 0"
   101   obtains m where "m > n" and "c * g m < f m"
   102   using assms unfolding less_eq_fun_def linorder_not_le [symmetric] by blast
   103 
   104 
   105 subsection \<open>The \<open>\<approx>\<close> relation, the equivalence relation induced by \<open>\<lesssim>\<close>\<close>
   106 
   107 definition equiv_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<cong>" 50)
   108 where
   109   "f \<cong> g \<longleftrightarrow>
   110     (\<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)"
   111 
   112 text \<open>
   113   This yields \<open>f \<cong> g \<longleftrightarrow> f \<in> \<Theta>(g)\<close>.  Concerning \<open>c\<^sub>1\<close> and \<open>c\<^sub>2\<close>
   114   restricted to @{typ nat}, see note above on \<open>(\<lesssim>)\<close>.
   115 \<close>
   116 
   117 lemma equiv_funI:
   118   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"
   119   shows "f \<cong> g"
   120   unfolding equiv_fun_def by (rule assms)
   121 
   122 lemma not_equiv_funI:
   123   assumes "\<And>c\<^sub>1 c\<^sub>2 n. c\<^sub>1 > 0 \<Longrightarrow> c\<^sub>2 > 0 \<Longrightarrow>
   124     \<exists>m>n. c\<^sub>1 * f m < g m \<or> c\<^sub>2 * g m < f m"
   125   shows "\<not> f \<cong> g"
   126   using assms unfolding equiv_fun_def linorder_not_le [symmetric] by blast
   127 
   128 lemma equiv_funE:
   129   assumes "f \<cong> g"
   130   obtains n c\<^sub>1 c\<^sub>2 where "c\<^sub>1 > 0" and "c\<^sub>2 > 0"
   131     and "\<And>m. m > n \<Longrightarrow> f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m"
   132   using assms unfolding equiv_fun_def by blast
   133 
   134 lemma not_equiv_funE:
   135   fixes n c\<^sub>1 c\<^sub>2
   136   assumes "\<not> f \<cong> g" and "c\<^sub>1 > 0" and "c\<^sub>2 > 0"
   137   obtains m where "m > n"
   138     and "c\<^sub>1 * f m < g m \<or> c\<^sub>2 * g m < f m"
   139   using assms unfolding equiv_fun_def linorder_not_le [symmetric] by blast
   140 
   141 
   142 subsection \<open>The \<open>\<prec>\<close> relation, the strict part of \<open>\<lesssim>\<close>\<close>
   143 
   144 definition less_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<prec>" 50)
   145 where
   146   "f \<prec> g \<longleftrightarrow> f \<lesssim> g \<and> \<not> g \<lesssim> f"
   147 
   148 lemma less_funI:
   149   assumes "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m"
   150     and "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * f m < g m"
   151   shows "f \<prec> g"
   152   using assms unfolding less_fun_def less_eq_fun_def linorder_not_less [symmetric] by blast
   153 
   154 lemma not_less_funI:
   155   assumes "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * g m < f m"
   156     and "\<exists>c>0. \<exists>n. \<forall>m>n. g m \<le> c * f m"
   157   shows "\<not> f \<prec> g"
   158   using assms unfolding less_fun_def less_eq_fun_def linorder_not_less [symmetric] by blast
   159 
   160 lemma less_funE [elim?]:
   161   assumes "f \<prec> g"
   162   obtains n c where "c > 0" and "\<And>m. m > n \<Longrightarrow> f m \<le> c * g m"
   163     and "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * f m < g m"
   164 proof -
   165   from assms have "f \<lesssim> g" and "\<not> g \<lesssim> f" by (simp_all add: less_fun_def)
   166   from \<open>f \<lesssim> g\<close> obtain n c where *:"c > 0" "m > n \<Longrightarrow> f m \<le> c * g m" for m
   167     by (rule less_eq_funE) blast
   168   { fix c n :: nat
   169     assume "c > 0"
   170     with \<open>\<not> g \<lesssim> f\<close> obtain m where "m > n" "c * f m < g m"
   171       by (rule not_less_eq_funE) blast
   172     then have **: "\<exists>m>n. c * f m < g m" by blast
   173   } note ** = this
   174   from * ** show thesis by (rule that)
   175 qed
   176 
   177 lemma not_less_funE:
   178   assumes "\<not> f \<prec> g" and "c > 0"
   179   obtains m where "m > n" and "c * g m < f m"
   180     | d q where "\<And>m. d > 0 \<Longrightarrow> m > q \<Longrightarrow> g q \<le> d * f q"
   181   using assms unfolding less_fun_def linorder_not_less [symmetric] by blast
   182 
   183 text \<open>
   184   I did not find a proof for \<open>f \<prec> g \<longleftrightarrow> f \<in> o(g)\<close>.  Maybe this only
   185   holds if \<open>f\<close> and/or \<open>g\<close> are of a certain class of functions.
   186   However \<open>f \<in> o(g) \<longrightarrow> f \<prec> g\<close> is provable, and this yields a
   187   handy introduction rule.
   188 
   189   Note that D. Knuth ignores \<open>o\<close> altogether.  So what \dots
   190 
   191   Something still has to be said about the coefficient \<open>c\<close> in
   192   the definition of \<open>(\<prec>)\<close>.  In the typical definition of \<open>o\<close>,
   193   it occurs on the \emph{right} hand side of the \<open>(>)\<close>.  The reason
   194   is that the situation is dual to the definition of \<open>O\<close>: the definition
   195   works since \<open>c\<close> may become arbitrary small.  Since this is not possible
   196   within @{term \<nat>}, we push the coefficient to the left hand side instead such
   197   that it may become arbitrary big instead.
   198 \<close>
   199 
   200 lemma less_fun_strongI:
   201   assumes "\<And>c. c > 0 \<Longrightarrow> \<exists>n. \<forall>m>n. c * f m < g m"
   202   shows "f \<prec> g"
   203 proof (rule less_funI)
   204   have "1 > (0::nat)" by simp
   205   with assms [OF this] obtain n where *: "m > n \<Longrightarrow> 1 * f m < g m" for m
   206     by blast
   207   have "\<forall>m>n. f m \<le> 1 * g m"
   208   proof (rule allI, rule impI)
   209     fix m
   210     assume "m > n"
   211     with * have "1 * f m < g m" by simp
   212     then show "f m \<le> 1 * g m" by simp
   213   qed
   214   with \<open>1 > 0\<close> show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m" by blast
   215   fix c n :: nat
   216   assume "c > 0"
   217   with assms obtain q where "m > q \<Longrightarrow> c * f m < g m" for m by blast
   218   then have "c * f (Suc (q + n)) < g (Suc (q + n))" by simp
   219   moreover have "Suc (q + n) > n" by simp
   220   ultimately show "\<exists>m>n. c * f m < g m" by blast
   221 qed
   222 
   223 
   224 subsection \<open>\<open>\<lesssim>\<close> is a preorder\<close>
   225 
   226 text \<open>This yields all lemmas relating \<open>\<lesssim>\<close>, \<open>\<prec>\<close> and \<open>\<cong>\<close>.\<close>
   227 
   228 interpretation fun_order: preorder_equiv less_eq_fun less_fun
   229   rewrites "fun_order.equiv = equiv_fun"
   230 proof -
   231   interpret preorder: preorder_equiv less_eq_fun less_fun
   232   proof
   233     fix f g h
   234     show "f \<lesssim> f"
   235     proof
   236       have "\<exists>n. \<forall>m>n. f m \<le> 1 * f m" by auto
   237       then show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * f m" by blast
   238     qed
   239     show "f \<prec> g \<longleftrightarrow> f \<lesssim> g \<and> \<not> g \<lesssim> f"
   240       by (fact less_fun_def)
   241     assume "f \<lesssim> g" and "g \<lesssim> h"
   242     show "f \<lesssim> h"
   243     proof
   244       from \<open>f \<lesssim> g\<close> obtain n\<^sub>1 c\<^sub>1
   245         where "c\<^sub>1 > 0" and P\<^sub>1: "\<And>m. m > n\<^sub>1 \<Longrightarrow> f m \<le> c\<^sub>1 * g m"
   246         by rule blast
   247       from \<open>g \<lesssim> h\<close> obtain n\<^sub>2 c\<^sub>2
   248         where "c\<^sub>2 > 0" and P\<^sub>2: "\<And>m. m > n\<^sub>2 \<Longrightarrow> g m \<le> c\<^sub>2 * h m"
   249         by rule blast
   250       have "\<forall>m>max n\<^sub>1 n\<^sub>2. f m \<le> (c\<^sub>1 * c\<^sub>2) * h m"
   251       proof (rule allI, rule impI)
   252         fix m
   253         assume Q: "m > max n\<^sub>1 n\<^sub>2"
   254         from P\<^sub>1 Q have *: "f m \<le> c\<^sub>1 * g m" by simp
   255         from P\<^sub>2 Q have "g m \<le> c\<^sub>2 * h m" by simp
   256         with \<open>c\<^sub>1 > 0\<close> have "c\<^sub>1 * g m \<le> (c\<^sub>1 * c\<^sub>2) * h m" by simp
   257         with * show "f m \<le> (c\<^sub>1 * c\<^sub>2) * h m" by (rule order_trans)
   258       qed
   259       then have "\<exists>n. \<forall>m>n. f m \<le> (c\<^sub>1 * c\<^sub>2) * h m" by rule
   260       moreover from \<open>c\<^sub>1 > 0\<close> \<open>c\<^sub>2 > 0\<close> have "c\<^sub>1 * c\<^sub>2 > 0" by simp
   261       ultimately show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * h m" by blast
   262     qed
   263   qed
   264   from preorder.preorder_equiv_axioms show "class.preorder_equiv less_eq_fun less_fun" .
   265   show "preorder_equiv.equiv less_eq_fun = equiv_fun"
   266   proof (rule ext, rule ext, unfold preorder.equiv_def)
   267     fix f g
   268     show "f \<lesssim> g \<and> g \<lesssim> f \<longleftrightarrow> f \<cong> g"
   269     proof
   270       assume "f \<cong> g"
   271       then obtain n c\<^sub>1 c\<^sub>2 where "c\<^sub>1 > 0" and "c\<^sub>2 > 0"
   272         and *: "\<And>m. m > n \<Longrightarrow> f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m"
   273         by (rule equiv_funE) blast
   274       have "\<forall>m>n. f m \<le> c\<^sub>1 * g m"
   275       proof (rule allI, rule impI)
   276         fix m
   277         assume "m > n"
   278         with * show "f m \<le> c\<^sub>1 * g m" by simp
   279       qed
   280       with \<open>c\<^sub>1 > 0\<close> have "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m" by blast
   281       then have "f \<lesssim> g" ..
   282       have "\<forall>m>n. g m \<le> c\<^sub>2 * f m"
   283       proof (rule allI, rule impI)
   284         fix m
   285         assume "m > n"
   286         with * show "g m \<le> c\<^sub>2 * f m" by simp
   287       qed
   288       with \<open>c\<^sub>2 > 0\<close> have "\<exists>c>0. \<exists>n. \<forall>m>n. g m \<le> c * f m" by blast
   289       then have "g \<lesssim> f" ..
   290       from \<open>f \<lesssim> g\<close> and \<open>g \<lesssim> f\<close> show "f \<lesssim> g \<and> g \<lesssim> f" ..
   291     next
   292       assume "f \<lesssim> g \<and> g \<lesssim> f"
   293       then have "f \<lesssim> g" and "g \<lesssim> f" by auto
   294       from \<open>f \<lesssim> g\<close> obtain n\<^sub>1 c\<^sub>1 where "c\<^sub>1 > 0"
   295         and P\<^sub>1: "\<And>m. m > n\<^sub>1 \<Longrightarrow> f m \<le> c\<^sub>1 * g m" by rule blast
   296       from \<open>g \<lesssim> f\<close> obtain n\<^sub>2 c\<^sub>2 where "c\<^sub>2 > 0"
   297         and P\<^sub>2: "\<And>m. m > n\<^sub>2 \<Longrightarrow> g m \<le> c\<^sub>2 * f m" by rule blast
   298       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"
   299       proof (rule allI, rule impI)
   300         fix m
   301         assume Q: "m > max n\<^sub>1 n\<^sub>2"
   302         from P\<^sub>1 Q have "f m \<le> c\<^sub>1 * g m" by simp
   303         moreover from P\<^sub>2 Q have "g m \<le> c\<^sub>2 * f m" by simp
   304         ultimately show "f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" ..
   305       qed
   306       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.
   307         \<forall>m>n. f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" by blast
   308       then show "f \<cong> g" by (rule equiv_funI)
   309     qed
   310   qed
   311 qed
   312 
   313 declare fun_order.antisym [intro?]
   314 
   315 
   316 subsection \<open>Simple examples\<close>
   317 
   318 text \<open>
   319   Most of these are left as constructive exercises for the reader.  Note that additional
   320   preconditions to the functions may be necessary.  The list here is by no means to be
   321   intended as complete construction set for typical functions, here surely something
   322   has to be added yet.
   323 \<close>
   324 
   325 text \<open>@{prop "(\<lambda>n. f n + k) \<cong> f"}\<close>
   326 
   327 lemma equiv_fun_mono_const:
   328   assumes "mono f" and "\<exists>n. f n > 0"
   329   shows "(\<lambda>n. f n + k) \<cong> f"
   330 proof (cases "k = 0")
   331   case True then show ?thesis by simp
   332 next
   333   case False
   334   show ?thesis
   335   proof
   336     show "(\<lambda>n. f n + k) \<lesssim> f"
   337     proof
   338       from \<open>\<exists>n. f n > 0\<close> obtain n where "f n > 0" ..
   339       have "\<forall>m>n. f m + k \<le> Suc k * f m"
   340       proof (rule allI, rule impI)
   341         fix m
   342         assume "n < m"
   343         with \<open>mono f\<close> have "f n \<le> f m"
   344           using less_imp_le_nat monoE by blast
   345         with  \<open>0 < f n\<close> have "0 < f m" by auto
   346         then obtain l where "f m = Suc l" by (cases "f m") simp_all
   347         then show "f m + k \<le> Suc k * f m" by simp
   348       qed
   349       then show "\<exists>c>0. \<exists>n. \<forall>m>n. f m + k \<le> c * f m" by blast
   350     qed
   351     show "f \<lesssim> (\<lambda>n. f n + k)"
   352     proof
   353       have "f m \<le> 1 * (f m + k)" for m by simp
   354       then show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * (f m + k)" by blast
   355     qed
   356   qed
   357 qed
   358 
   359 lemma
   360   assumes "strict_mono f"
   361   shows "(\<lambda>n. f n + k) \<cong> f"
   362 proof (rule equiv_fun_mono_const)
   363   from assms show "mono f" by (rule strict_mono_mono)
   364   show "\<exists>n. 0 < f n"
   365   proof (rule ccontr)
   366     assume "\<not> (\<exists>n. 0 < f n)"
   367     then have "\<And>n. f n = 0" by simp
   368     then have "f 0 = f 1" by simp
   369     moreover from \<open>strict_mono f\<close> have "f 0 < f 1"
   370       by (simp add: strict_mono_def) 
   371     ultimately show False by simp
   372   qed
   373 qed
   374   
   375 lemma
   376   "(\<lambda>n. Suc k * f n) \<cong> f"
   377 proof
   378   show "(\<lambda>n. Suc k * f n) \<lesssim> f"
   379   proof
   380     have "Suc k * f m \<le> Suc k * f m" for m by simp
   381     then show "\<exists>c>0. \<exists>n. \<forall>m>n. Suc k * f m \<le> c * f m" by blast
   382   qed
   383   show "f \<lesssim> (\<lambda>n. Suc k * f n)"
   384   proof
   385     have "f m \<le> 1 * (Suc k * f m)" for m by simp
   386     then show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * (Suc k * f m)" by blast
   387   qed
   388 qed
   389 
   390 lemma
   391   "f \<lesssim> (\<lambda>n. f n + g n)"
   392   by rule auto
   393 
   394 lemma
   395   "(\<lambda>_. 0) \<prec> (\<lambda>n. Suc k)"
   396   by (rule less_fun_strongI) auto
   397 
   398 lemma
   399   "(\<lambda>_. k) \<prec> Discrete.log"
   400 proof (rule less_fun_strongI)
   401   fix c :: nat
   402   have "\<forall>m>2 ^ (Suc (c * k)). c * k < Discrete.log m"
   403   proof (rule allI, rule impI)
   404     fix m :: nat
   405     assume "2 ^ Suc (c * k) < m"
   406     then have "2 ^ Suc (c * k) \<le> m" by simp
   407     with log_mono have "Discrete.log (2 ^ (Suc (c * k))) \<le> Discrete.log m"
   408       by (blast dest: monoD)
   409     moreover have "c * k < Discrete.log (2 ^ (Suc (c * k)))" by simp
   410     ultimately show "c * k < Discrete.log m" by auto
   411   qed
   412   then show "\<exists>n. \<forall>m>n. c * k < Discrete.log m" ..
   413 qed
   414 
   415 (*lemma
   416   "Discrete.log \<prec> Discrete.sqrt"
   417 proof (rule less_fun_strongI)*)
   418 text \<open>@{prop "Discrete.log \<prec> Discrete.sqrt"}\<close>
   419 
   420 lemma
   421   "Discrete.sqrt \<prec> id"
   422 proof (rule less_fun_strongI)
   423   fix c :: nat
   424   assume "0 < c"
   425   have "\<forall>m>(Suc c)\<^sup>2. c * Discrete.sqrt m < id m"
   426   proof (rule allI, rule impI)
   427     fix m
   428     assume "(Suc c)\<^sup>2 < m"
   429     then have "(Suc c)\<^sup>2 \<le> m" by simp
   430     with mono_sqrt have "Discrete.sqrt ((Suc c)\<^sup>2) \<le> Discrete.sqrt m" by (rule monoE)
   431     then have "Suc c \<le> Discrete.sqrt m" by simp
   432     then have "c < Discrete.sqrt m" by simp
   433     moreover from \<open>(Suc c)\<^sup>2 < m\<close> have "Discrete.sqrt m > 0" by simp
   434     ultimately have "c * Discrete.sqrt m < Discrete.sqrt m * Discrete.sqrt m" by simp
   435     also have "\<dots> \<le> m" by (simp add: power2_eq_square [symmetric])
   436     finally show "c * Discrete.sqrt m < id m" by simp
   437   qed
   438   then show "\<exists>n. \<forall>m>n. c * Discrete.sqrt m < id m" ..
   439 qed
   440 
   441 lemma
   442   "id \<prec> (\<lambda>n. n\<^sup>2)"
   443   by (rule less_fun_strongI) (auto simp add: power2_eq_square)
   444 
   445 lemma
   446   "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. n ^ Suc k)"
   447   by (rule less_fun_strongI) auto
   448 
   449 (*lemma 
   450   "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. 2 ^ n)"
   451 proof (rule less_fun_strongI)*)
   452 text \<open>@{prop "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. 2 ^ n)"}\<close>
   453 
   454 end