src/HOL/Library/Function_Growth.thy
author Andreas Lochbihler
Wed Feb 27 10:33:30 2013 +0100 (2013-02-27)
changeset 51288 be7e9a675ec9
parent 51264 aba03f0c6254
child 51542 738598beeb26
permissions -rw-r--r--
add wellorder instance for Numeral_Type (suggested by Jesus Aransay)
haftmann@31381
     1
haftmann@31381
     2
(* Author: Florian Haftmann, TU Muenchen *)
haftmann@31381
     3
haftmann@31381
     4
header {* Comparing growth of functions on natural numbers by a preorder relation *}
haftmann@31381
     5
haftmann@51263
     6
theory Function_Growth
haftmann@51263
     7
imports Main "~~/src/HOL/Library/Preorder" "~~/src/HOL/Library/Discrete"
haftmann@31381
     8
begin
haftmann@31381
     9
haftmann@51263
    10
subsection {* Motivation *}
haftmann@51263
    11
haftmann@31381
    12
text {*
haftmann@51263
    13
  When comparing growth of functions in computer science, it is common to adhere
wenzelm@51264
    14
  on Landau Symbols (``O-Notation'').  However these come at the cost of notational
haftmann@51263
    15
  oddities, particularly writing @{text "f = O(g)"} for @{text "f \<in> O(g)"} etc.
haftmann@51263
    16
  
haftmann@51263
    17
  Here we suggest a diffent way, following Hardy (G.~H.~Hardy and J.~E.~Littlewood,
haftmann@51263
    18
  Some problems of Diophantine approximation, Acta Mathematica 37 (1914), p.~225).
haftmann@51263
    19
  We establish a quasi order relation @{text "\<lesssim>"} on functions such that
haftmann@51263
    20
  @{text "f \<lesssim> g \<longleftrightarrow> f \<in> O(g)"}.  From a didactic point of view, this does not only
haftmann@51263
    21
  avoid the notational oddities mentioned above but also emphasizes the key insight
haftmann@51263
    22
  of a growth hierachy of functions:
haftmann@51263
    23
  @{text "(\<lambda>n. 0) \<lesssim> (\<lambda>n. k) \<lesssim> Discrete.log \<lesssim> Discrete.sqrt \<lesssim> id \<lesssim> \<dots>"}.
haftmann@31381
    24
*}
haftmann@31381
    25
haftmann@51263
    26
subsection {* Model *}
haftmann@31381
    27
haftmann@51263
    28
text {*
haftmann@51263
    29
  Our growth functions are of type @{text "\<nat> \<Rightarrow> \<nat>"}.  This is different
haftmann@51263
    30
  to the usual conventions for Landau symbols for which @{text "\<real> \<Rightarrow> \<real>"}
haftmann@51263
    31
  would be appropriate, but we argue that @{text "\<real> \<Rightarrow> \<real>"} is more
haftmann@51263
    32
  appropriate for analysis, whereas our setting is discrete.
haftmann@51263
    33
haftmann@51263
    34
  Note that we also restrict the additional coefficients to @{text \<nat>}, something
haftmann@51263
    35
  we discuss at the particular definitions.
haftmann@51263
    36
*}
haftmann@31381
    37
haftmann@31381
    38
subsection {* The @{text "\<lesssim>"} relation *}
haftmann@31381
    39
haftmann@51263
    40
definition less_eq_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<lesssim>" 50)
haftmann@51263
    41
where
haftmann@51263
    42
  "f \<lesssim> g \<longleftrightarrow> (\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m)"
haftmann@31381
    43
haftmann@51263
    44
text {*
haftmann@51263
    45
  This yields @{text "f \<lesssim> g \<longleftrightarrow> f \<in> O(g)"}.  Note that @{text c} is restricted to
haftmann@51263
    46
  @{text \<nat>}.  This does not pose any problems since if @{text "f \<in> O(g)"} holds for
haftmann@51263
    47
  a @{text "c \<in> \<real>"}, it also holds for @{text "\<lceil>c\<rceil> \<in> \<nat>"} by transitivity.
haftmann@51263
    48
*}
haftmann@51263
    49
haftmann@51263
    50
lemma less_eq_funI [intro?]:
haftmann@51263
    51
  assumes "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m"
haftmann@31381
    52
  shows "f \<lesssim> g"
haftmann@31381
    53
  unfolding less_eq_fun_def by (rule assms)
haftmann@31381
    54
haftmann@51263
    55
lemma not_less_eq_funI:
haftmann@51263
    56
  assumes "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * g m < f m"
haftmann@31381
    57
  shows "\<not> f \<lesssim> g"
haftmann@51263
    58
  using assms unfolding less_eq_fun_def linorder_not_le [symmetric] by blast
haftmann@31381
    59
haftmann@51263
    60
lemma less_eq_funE [elim?]:
haftmann@31381
    61
  assumes "f \<lesssim> g"
haftmann@51263
    62
  obtains n c where "c > 0" and "\<And>m. m > n \<Longrightarrow> f m \<le> c * g m"
haftmann@31381
    63
  using assms unfolding less_eq_fun_def by blast
haftmann@31381
    64
haftmann@51263
    65
lemma not_less_eq_funE:
haftmann@51263
    66
  assumes "\<not> f \<lesssim> g" and "c > 0"
haftmann@51263
    67
  obtains m where "m > n" and "c * g m < f m"
haftmann@51263
    68
  using assms unfolding less_eq_fun_def linorder_not_le [symmetric] by blast
haftmann@31381
    69
haftmann@31381
    70
haftmann@31381
    71
subsection {* The @{text "\<approx>"} relation, the equivalence relation induced by @{text "\<lesssim>"} *}
haftmann@31381
    72
haftmann@51263
    73
definition equiv_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<cong>" 50)
haftmann@51263
    74
where
haftmann@51263
    75
  "f \<cong> g \<longleftrightarrow>
haftmann@51263
    76
    (\<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)"
haftmann@31381
    77
haftmann@51263
    78
text {*
haftmann@51263
    79
  This yields @{text "f \<cong> g \<longleftrightarrow> f \<in> \<Theta>(g)"}.  Concerning @{text "c\<^isub>1"} and @{text "c\<^isub>2"}
haftmann@51263
    80
  restricted to @{typ nat}, see note above on @{text "(\<lesssim>)"}.
haftmann@51263
    81
*}
haftmann@51263
    82
haftmann@51263
    83
lemma equiv_funI [intro?]:
haftmann@51263
    84
  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"
haftmann@31381
    85
  shows "f \<cong> g"
haftmann@31381
    86
  unfolding equiv_fun_def by (rule assms)
haftmann@31381
    87
haftmann@51263
    88
lemma not_equiv_funI:
haftmann@51263
    89
  assumes "\<And>c\<^isub>1 c\<^isub>2 n. c\<^isub>1 > 0 \<Longrightarrow> c\<^isub>2 > 0 \<Longrightarrow>
haftmann@51263
    90
    \<exists>m>n. c\<^isub>1 * f m < g m \<or> c\<^isub>2 * g m < f m"
haftmann@31381
    91
  shows "\<not> f \<cong> g"
haftmann@51263
    92
  using assms unfolding equiv_fun_def linorder_not_le [symmetric] by blast
haftmann@31381
    93
haftmann@51263
    94
lemma equiv_funE [elim?]:
haftmann@31381
    95
  assumes "f \<cong> g"
haftmann@51263
    96
  obtains n c\<^isub>1 c\<^isub>2 where "c\<^isub>1 > 0" and "c\<^isub>2 > 0"
haftmann@51263
    97
    and "\<And>m. m > n \<Longrightarrow> f m \<le> c\<^isub>1 * g m \<and> g m \<le> c\<^isub>2 * f m"
haftmann@31381
    98
  using assms unfolding equiv_fun_def by blast
haftmann@31381
    99
haftmann@51263
   100
lemma not_equiv_funE:
haftmann@51263
   101
  fixes n c\<^isub>1 c\<^isub>2
haftmann@51263
   102
  assumes "\<not> f \<cong> g" and "c\<^isub>1 > 0" and "c\<^isub>2 > 0"
haftmann@51263
   103
  obtains m where "m > n"
haftmann@51263
   104
    and "c\<^isub>1 * f m < g m \<or> c\<^isub>2 * g m < f m"
haftmann@51263
   105
  using assms unfolding equiv_fun_def linorder_not_le [symmetric] by blast
haftmann@31381
   106
haftmann@31381
   107
haftmann@31381
   108
subsection {* The @{text "\<prec>"} relation, the strict part of @{text "\<lesssim>"} *}
haftmann@31381
   109
haftmann@51263
   110
definition less_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<prec>" 50)
haftmann@51263
   111
where
haftmann@31381
   112
  "f \<prec> g \<longleftrightarrow> f \<lesssim> g \<and> \<not> g \<lesssim> f"
haftmann@31381
   113
haftmann@51263
   114
lemma less_funI:
haftmann@51263
   115
  assumes "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m"
haftmann@51263
   116
    and "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * f m < g m"
haftmann@31381
   117
  shows "f \<prec> g"
haftmann@51263
   118
  using assms unfolding less_fun_def less_eq_fun_def linorder_not_less [symmetric] by blast
haftmann@51263
   119
haftmann@51263
   120
lemma not_less_funI:
haftmann@51263
   121
  assumes "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * g m < f m"
haftmann@51263
   122
    and "\<exists>c>0. \<exists>n. \<forall>m>n. g m \<le> c * f m"
haftmann@51263
   123
  shows "\<not> f \<prec> g"
haftmann@51263
   124
  using assms unfolding less_fun_def less_eq_fun_def linorder_not_less [symmetric] by blast
haftmann@51263
   125
haftmann@51263
   126
lemma less_funE [elim?]:
haftmann@51263
   127
  assumes "f \<prec> g"
haftmann@51263
   128
  obtains n c where "c > 0" and "\<And>m. m > n \<Longrightarrow> f m \<le> c * g m"
haftmann@51263
   129
    and "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * f m < g m"
haftmann@51263
   130
proof -
haftmann@51263
   131
  from assms have "f \<lesssim> g" and "\<not> g \<lesssim> f" by (simp_all add: less_fun_def)
haftmann@51263
   132
  from `f \<lesssim> g` obtain n c where *:"c > 0" "\<And>m. m > n \<Longrightarrow> f m \<le> c * g m"
haftmann@51263
   133
    by (rule less_eq_funE) blast
haftmann@51263
   134
  { fix c n :: nat
haftmann@51263
   135
    assume "c > 0"
haftmann@51263
   136
    with `\<not> g \<lesssim> f` obtain m where "m > n" "c * f m < g m"
haftmann@51263
   137
      by (rule not_less_eq_funE) blast
haftmann@51263
   138
    then have **: "\<exists>m>n. c * f m < g m" by blast
haftmann@51263
   139
  } note ** = this
haftmann@51263
   140
  from * ** show thesis by (rule that)
haftmann@31381
   141
qed
haftmann@31381
   142
haftmann@51263
   143
lemma not_less_funE:
haftmann@51263
   144
  assumes "\<not> f \<prec> g" and "c > 0"
haftmann@51263
   145
  obtains m where "m > n" and "c * g m < f m"
haftmann@51263
   146
    | d q where "\<And>m. d > 0 \<Longrightarrow> m > q \<Longrightarrow> g q \<le> d * f q"
haftmann@51263
   147
  using assms unfolding less_fun_def linorder_not_less [symmetric] by blast
haftmann@51263
   148
haftmann@31381
   149
text {*
haftmann@51263
   150
  I did not found a proof for @{text "f \<prec> g \<longleftrightarrow> f \<in> o(g)"}.  Maybe this only
haftmann@51263
   151
  holds if @{text f} and/or @{text g} are of a certain class of functions.
haftmann@51263
   152
  However @{text "f \<in> o(g) \<longrightarrow> f \<prec> g"} is provable, and this yields a
haftmann@51263
   153
  handy introduction rule.
haftmann@51263
   154
wenzelm@51264
   155
  Note that D. Knuth ignores @{text o} altogether.  So what \dots
haftmann@51263
   156
haftmann@51263
   157
  Something still has to be said about the coefficient @{text c} in
haftmann@51263
   158
  the definition of @{text "(\<prec>)"}.  In the typical definition of @{text o},
haftmann@51263
   159
  it occurs on the \emph{right} hand side of the @{text "(>)"}.  The reason
haftmann@51263
   160
  is that the situation is dual to the definition of @{text O}: the definition
haftmann@51263
   161
  works since @{text c} may become arbitrary small.  Since this is not possible
haftmann@51263
   162
  within @{term \<nat>}, we push the coefficient to the left hand side instead such
haftmann@51263
   163
  that it become arbitrary big instead.
haftmann@31381
   164
*}
haftmann@31381
   165
haftmann@51263
   166
lemma less_fun_strongI:
haftmann@51263
   167
  assumes "\<And>c. c > 0 \<Longrightarrow> \<exists>n. \<forall>m>n. c * f m < g m"
haftmann@51263
   168
  shows "f \<prec> g"
haftmann@51263
   169
proof (rule less_funI)
haftmann@51263
   170
  have "1 > (0::nat)" by simp
haftmann@51263
   171
  from assms `1 > 0` have "\<exists>n. \<forall>m>n. 1 * f m < g m" .
haftmann@51263
   172
  then obtain n where *: "\<And>m. m > n \<Longrightarrow> 1 * f m < g m" by blast
haftmann@51263
   173
  have "\<forall>m>n. f m \<le> 1 * g m"
haftmann@51263
   174
  proof (rule allI, rule impI)
haftmann@51263
   175
    fix m
haftmann@51263
   176
    assume "m > n"
haftmann@51263
   177
    with * have "1 * f m < g m" by simp
haftmann@51263
   178
    then show "f m \<le> 1 * g m" by simp
haftmann@51263
   179
  qed
haftmann@51263
   180
  with `1 > 0` show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m" by blast
haftmann@51263
   181
  fix c n :: nat
haftmann@51263
   182
  assume "c > 0"
haftmann@51263
   183
  with assms obtain q where "\<And>m. m > q \<Longrightarrow> c * f m < g m" by blast
haftmann@51263
   184
  then have "c * f (Suc (q + n)) < g (Suc (q + n))" by simp
haftmann@51263
   185
  moreover have "Suc (q + n) > n" by simp
haftmann@51263
   186
  ultimately show "\<exists>m>n. c * f m < g m" by blast
haftmann@51263
   187
qed
haftmann@31381
   188
haftmann@51263
   189
haftmann@51263
   190
subsection {* @{text "\<lesssim>"} is a preorder *}
haftmann@51263
   191
haftmann@51263
   192
text {* This yields all lemmas relating @{text "\<lesssim>"}, @{text "\<prec>"} and @{text "\<cong>"}. *}
haftmann@31381
   193
haftmann@31381
   194
interpretation fun_order: preorder_equiv less_eq_fun less_fun
haftmann@31381
   195
  where "preorder_equiv.equiv less_eq_fun = equiv_fun"
haftmann@31381
   196
proof -
haftmann@51263
   197
  interpret preorder: preorder_equiv less_eq_fun less_fun
haftmann@51263
   198
  proof
haftmann@51263
   199
    fix f g h
haftmann@51263
   200
    show "f \<lesssim> f"
haftmann@51263
   201
    proof
haftmann@51263
   202
      have "\<exists>n. \<forall>m>n. f m \<le> 1 * f m" by auto
haftmann@51263
   203
      then show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * f m" by blast
haftmann@51263
   204
    qed
haftmann@51263
   205
    show "f \<prec> g \<longleftrightarrow> f \<lesssim> g \<and> \<not> g \<lesssim> f"
haftmann@51263
   206
      by (fact less_fun_def)
haftmann@51263
   207
    assume "f \<lesssim> g" and "g \<lesssim> h"
haftmann@51263
   208
    show "f \<lesssim> h"
haftmann@51263
   209
    proof
haftmann@51263
   210
      from `f \<lesssim> g` obtain n\<^isub>1 c\<^isub>1
haftmann@51263
   211
        where "c\<^isub>1 > 0" and P\<^isub>1: "\<And>m. m > n\<^isub>1 \<Longrightarrow> f m \<le> c\<^isub>1 * g m"
haftmann@51263
   212
        by rule blast
haftmann@51263
   213
      from `g \<lesssim> h` obtain n\<^isub>2 c\<^isub>2
haftmann@51263
   214
        where "c\<^isub>2 > 0" and P\<^isub>2: "\<And>m. m > n\<^isub>2 \<Longrightarrow> g m \<le> c\<^isub>2 * h m"
haftmann@51263
   215
        by rule blast
haftmann@51263
   216
      have "\<forall>m>max n\<^isub>1 n\<^isub>2. f m \<le> (c\<^isub>1 * c\<^isub>2) * h m"
haftmann@51263
   217
      proof (rule allI, rule impI)
haftmann@51263
   218
        fix m
haftmann@51263
   219
        assume Q: "m > max n\<^isub>1 n\<^isub>2"
haftmann@51263
   220
        from P\<^isub>1 Q have *: "f m \<le> c\<^isub>1 * g m" by simp
haftmann@51263
   221
        from P\<^isub>2 Q have "g m \<le> c\<^isub>2 * h m" by simp
haftmann@51263
   222
        with `c\<^isub>1 > 0` have "c\<^isub>1 * g m \<le> (c\<^isub>1 * c\<^isub>2) * h m" by simp
haftmann@51263
   223
        with * show "f m \<le> (c\<^isub>1 * c\<^isub>2) * h m" by (rule order_trans)
haftmann@51263
   224
      qed
haftmann@51263
   225
      then have "\<exists>n. \<forall>m>n. f m \<le> (c\<^isub>1 * c\<^isub>2) * h m" by rule
haftmann@51263
   226
      moreover from `c\<^isub>1 > 0` `c\<^isub>2 > 0` have "c\<^isub>1 * c\<^isub>2 > 0" by (rule mult_pos_pos)
haftmann@51263
   227
      ultimately show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * h m" by blast
haftmann@51263
   228
    qed
haftmann@51263
   229
  qed
haftmann@51263
   230
  from preorder.preorder_equiv_axioms show "class.preorder_equiv less_eq_fun less_fun" .
haftmann@31381
   231
  show "preorder_equiv.equiv less_eq_fun = equiv_fun"
haftmann@51263
   232
  proof (rule ext, rule ext, unfold preorder.equiv_def)
haftmann@51263
   233
    fix f g
haftmann@51263
   234
    show "f \<lesssim> g \<and> g \<lesssim> f \<longleftrightarrow> f \<cong> g"
haftmann@51263
   235
    proof
haftmann@51263
   236
      assume "f \<cong> g"
haftmann@51263
   237
      then obtain n c\<^isub>1 c\<^isub>2 where "c\<^isub>1 > 0" and "c\<^isub>2 > 0"
haftmann@51263
   238
        and *: "\<And>m. m > n \<Longrightarrow> f m \<le> c\<^isub>1 * g m \<and> g m \<le> c\<^isub>2 * f m"
haftmann@51263
   239
        by rule blast
haftmann@51263
   240
      have "\<forall>m>n. f m \<le> c\<^isub>1 * g m"
haftmann@51263
   241
      proof (rule allI, rule impI)
haftmann@51263
   242
        fix m
haftmann@51263
   243
        assume "m > n"
haftmann@51263
   244
        with * show "f m \<le> c\<^isub>1 * g m" by simp
haftmann@51263
   245
      qed
haftmann@51263
   246
      with `c\<^isub>1 > 0` have "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m" by blast
haftmann@51263
   247
      then have "f \<lesssim> g" ..
haftmann@51263
   248
      have "\<forall>m>n. g m \<le> c\<^isub>2 * f m"
haftmann@51263
   249
      proof (rule allI, rule impI)
haftmann@51263
   250
        fix m
haftmann@51263
   251
        assume "m > n"
haftmann@51263
   252
        with * show "g m \<le> c\<^isub>2 * f m" by simp
haftmann@51263
   253
      qed
haftmann@51263
   254
      with `c\<^isub>2 > 0` have "\<exists>c>0. \<exists>n. \<forall>m>n. g m \<le> c * f m" by blast
haftmann@51263
   255
      then have "g \<lesssim> f" ..
haftmann@51263
   256
      from `f \<lesssim> g` and `g \<lesssim> f` show "f \<lesssim> g \<and> g \<lesssim> f" ..
haftmann@51263
   257
    next
haftmann@51263
   258
      assume "f \<lesssim> g \<and> g \<lesssim> f"
haftmann@51263
   259
      then have "f \<lesssim> g" and "g \<lesssim> f" by auto
haftmann@51263
   260
      from `f \<lesssim> g` obtain n\<^isub>1 c\<^isub>1 where "c\<^isub>1 > 0"
haftmann@51263
   261
        and P\<^isub>1: "\<And>m. m > n\<^isub>1 \<Longrightarrow> f m \<le> c\<^isub>1 * g m" by rule blast
haftmann@51263
   262
      from `g \<lesssim> f` obtain n\<^isub>2 c\<^isub>2 where "c\<^isub>2 > 0"
haftmann@51263
   263
        and P\<^isub>2: "\<And>m. m > n\<^isub>2 \<Longrightarrow> g m \<le> c\<^isub>2 * f m" by rule blast
haftmann@51263
   264
      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"
haftmann@51263
   265
      proof (rule allI, rule impI)
haftmann@51263
   266
        fix m
haftmann@51263
   267
        assume Q: "m > max n\<^isub>1 n\<^isub>2"
haftmann@51263
   268
        from P\<^isub>1 Q have "f m \<le> c\<^isub>1 * g m" by simp
haftmann@51263
   269
        moreover from P\<^isub>2 Q have "g m \<le> c\<^isub>2 * f m" by simp
haftmann@51263
   270
        ultimately show "f m \<le> c\<^isub>1 * g m \<and> g m \<le> c\<^isub>2 * f m" ..
haftmann@51263
   271
      qed
haftmann@51263
   272
      with `c\<^isub>1 > 0` `c\<^isub>2 > 0` have "\<exists>c\<^isub>1>0. \<exists>c\<^isub>2>0. \<exists>n.
haftmann@51263
   273
        \<forall>m>n. f m \<le> c\<^isub>1 * g m \<and> g m \<le> c\<^isub>2 * f m" by blast
haftmann@51263
   274
      then show "f \<cong> g" ..
haftmann@51263
   275
    qed
haftmann@51263
   276
  qed
haftmann@31381
   277
qed
haftmann@31381
   278
haftmann@31381
   279
haftmann@31381
   280
subsection {* Simple examples *}
haftmann@31381
   281
haftmann@51263
   282
text {*
haftmann@51263
   283
  Most of these are left as constructive exercises for the reader.  Note that additional
haftmann@51263
   284
  preconditions to the functions may be necessary.  The list here is by no means to be
haftmann@51263
   285
  intended as complete contruction set for typical functions, here surely something
haftmann@51263
   286
  has to be added yet.
haftmann@51263
   287
*}
haftmann@51263
   288
haftmann@51263
   289
text {* @{prop "(\<lambda>n. f n + k) \<cong> f"} *}
haftmann@51263
   290
haftmann@51263
   291
text {* @{prop "(\<lambda>n. Suc k * f n) \<cong> f"} *}
haftmann@51263
   292
haftmann@51263
   293
lemma "f \<lesssim> (\<lambda>n. f n + g n)"
wenzelm@51264
   294
  by rule auto
haftmann@51263
   295
haftmann@51263
   296
lemma "(\<lambda>_. 0) \<prec> (\<lambda>n. Suc k)"
wenzelm@51264
   297
  by (rule less_fun_strongI) auto
haftmann@51263
   298
haftmann@51263
   299
lemma "(\<lambda>_. k) \<prec> Discrete.log"
haftmann@51263
   300
proof (rule less_fun_strongI)
haftmann@51263
   301
  fix c :: nat
haftmann@51263
   302
  have "\<forall>m>2 ^ (Suc (c * k)). c * k < Discrete.log m"
haftmann@51263
   303
  proof (rule allI, rule impI)
haftmann@51263
   304
    fix m :: nat
haftmann@51263
   305
    assume "2 ^ Suc (c * k) < m"
haftmann@51263
   306
    then have "2 ^ Suc (c * k) \<le> m" by simp
haftmann@51263
   307
    with log_mono have "Discrete.log (2 ^ (Suc (c * k))) \<le> Discrete.log m"
haftmann@51263
   308
      by (blast dest: monoD)
haftmann@51263
   309
    moreover have "c * k < Discrete.log (2 ^ (Suc (c * k)))" by simp
haftmann@51263
   310
    ultimately show "c * k < Discrete.log m" by auto
haftmann@31381
   311
  qed
haftmann@51263
   312
  then show "\<exists>n. \<forall>m>n. c * k < Discrete.log m" ..
haftmann@51263
   313
qed
haftmann@51263
   314
  
haftmann@51263
   315
text {* @{prop "Discrete.log \<prec> Discrete.sqrt"} *}
haftmann@51263
   316
haftmann@51263
   317
lemma "Discrete.sqrt \<prec> id"
haftmann@51263
   318
proof (rule less_fun_strongI)
haftmann@51263
   319
  fix c :: nat
haftmann@51263
   320
  assume "0 < c"
haftmann@51263
   321
  have "\<forall>m>(Suc c)\<twosuperior>. c * Discrete.sqrt m < id m"
haftmann@51263
   322
  proof (rule allI, rule impI)
haftmann@51263
   323
    fix m
haftmann@51263
   324
    assume "(Suc c)\<twosuperior> < m"
haftmann@51263
   325
    then have "(Suc c)\<twosuperior> \<le> m" by simp
haftmann@51263
   326
    with mono_sqrt have "Discrete.sqrt ((Suc c)\<twosuperior>) \<le> Discrete.sqrt m" by (rule monoE)
haftmann@51263
   327
    then have "Suc c \<le> Discrete.sqrt m" by simp
haftmann@51263
   328
    then have "c < Discrete.sqrt m" by simp
haftmann@51263
   329
    moreover from `(Suc c)\<twosuperior> < m` have "Discrete.sqrt m > 0" by simp
haftmann@51263
   330
    ultimately have "c * Discrete.sqrt m < Discrete.sqrt m * Discrete.sqrt m" by simp
haftmann@51263
   331
    also have "\<dots> \<le> m" by (simp add: power2_eq_square [symmetric])
haftmann@51263
   332
    finally show "c * Discrete.sqrt m < id m" by simp
haftmann@51263
   333
  qed
haftmann@51263
   334
  then show "\<exists>n. \<forall>m>n. c * Discrete.sqrt m < id m" ..
haftmann@31381
   335
qed
haftmann@31381
   336
haftmann@51263
   337
lemma "id \<prec> (\<lambda>n. n\<twosuperior>)"
wenzelm@51264
   338
  by (rule less_fun_strongI) (auto simp add: power2_eq_square)
haftmann@31381
   339
haftmann@51263
   340
lemma "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. n ^ Suc k)"
wenzelm@51264
   341
  by (rule less_fun_strongI) auto
haftmann@51263
   342
haftmann@51263
   343
text {* @{prop "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. 2 ^ n)"} *}
haftmann@31381
   344
haftmann@31381
   345
end
haftmann@51263
   346