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