src/HOL/Library/Function_Growth.thy
 author wenzelm Wed Dec 30 11:37:29 2015 +0100 (2015-12-30) changeset 61975 b4b11391c676 parent 61833 c601d3c76362 child 63040 eb4ddd18d635 permissions -rw-r--r--
isabelle update_cartouches -c -t;
     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   def q == "m - n"

    39   moreover with assms have "m = q + n" by (simp add: q_def)

    40   ultimately 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" "\<And>m. m > n \<Longrightarrow> f m \<le> c * g 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   from assms \<open>1 > 0\<close> have "\<exists>n. \<forall>m>n. 1 * f m < g m" .

   206   then obtain n where *: "\<And>m. m > n \<Longrightarrow> 1 * f m < g m" 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 "\<And>m. m > q \<Longrightarrow> c * f m < g 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