src/HOL/Library/Function_Growth.thy
author wenzelm
Wed Jun 17 11:03:05 2015 +0200 (2015-06-17)
changeset 60500 903bb1495239
parent 59113 3cded6b57a82
child 61566 c3d6e570ccef
permissions -rw-r--r--
isabelle update_cartouches;
haftmann@31381
     1
haftmann@31381
     2
(* Author: Florian Haftmann, TU Muenchen *)
haftmann@31381
     3
wenzelm@60500
     4
section \<open>Comparing growth of functions on natural numbers by a preorder relation\<close>
haftmann@31381
     5
haftmann@51263
     6
theory Function_Growth
wenzelm@51542
     7
imports Main Preorder Discrete
haftmann@31381
     8
begin
haftmann@31381
     9
wenzelm@60500
    10
subsection \<open>Motivation\<close>
haftmann@51263
    11
wenzelm@60500
    12
text \<open>
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
  
wenzelm@59113
    17
  Here we suggest a different 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
wenzelm@59113
    22
  of a growth hierarchy of functions:
haftmann@51263
    23
  @{text "(\<lambda>n. 0) \<lesssim> (\<lambda>n. k) \<lesssim> Discrete.log \<lesssim> Discrete.sqrt \<lesssim> id \<lesssim> \<dots>"}.
wenzelm@60500
    24
\<close>
haftmann@31381
    25
wenzelm@60500
    26
subsection \<open>Model\<close>
haftmann@31381
    27
wenzelm@60500
    28
text \<open>
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.
wenzelm@60500
    36
\<close>
haftmann@31381
    37
wenzelm@60500
    38
subsection \<open>The @{text "\<lesssim>"} relation\<close>
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
wenzelm@60500
    44
text \<open>
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.
wenzelm@60500
    48
\<close>
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
wenzelm@60500
    71
subsection \<open>The @{text "\<approx>"} relation, the equivalence relation induced by @{text "\<lesssim>"}\<close>
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>
wenzelm@53015
    76
    (\<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)"
haftmann@31381
    77
wenzelm@60500
    78
text \<open>
wenzelm@53015
    79
  This yields @{text "f \<cong> g \<longleftrightarrow> f \<in> \<Theta>(g)"}.  Concerning @{text "c\<^sub>1"} and @{text "c\<^sub>2"}
haftmann@51263
    80
  restricted to @{typ nat}, see note above on @{text "(\<lesssim>)"}.
wenzelm@60500
    81
\<close>
haftmann@51263
    82
haftmann@51263
    83
lemma equiv_funI [intro?]:
wenzelm@53015
    84
  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"
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:
wenzelm@53015
    89
  assumes "\<And>c\<^sub>1 c\<^sub>2 n. c\<^sub>1 > 0 \<Longrightarrow> c\<^sub>2 > 0 \<Longrightarrow>
wenzelm@53015
    90
    \<exists>m>n. c\<^sub>1 * f m < g m \<or> c\<^sub>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"
wenzelm@53015
    96
  obtains n c\<^sub>1 c\<^sub>2 where "c\<^sub>1 > 0" and "c\<^sub>2 > 0"
wenzelm@53015
    97
    and "\<And>m. m > n \<Longrightarrow> f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m"
haftmann@31381
    98
  using assms unfolding equiv_fun_def by blast
haftmann@31381
    99
haftmann@51263
   100
lemma not_equiv_funE:
wenzelm@53015
   101
  fixes n c\<^sub>1 c\<^sub>2
wenzelm@53015
   102
  assumes "\<not> f \<cong> g" and "c\<^sub>1 > 0" and "c\<^sub>2 > 0"
haftmann@51263
   103
  obtains m where "m > n"
wenzelm@53015
   104
    and "c\<^sub>1 * f m < g m \<or> c\<^sub>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
wenzelm@60500
   108
subsection \<open>The @{text "\<prec>"} relation, the strict part of @{text "\<lesssim>"}\<close>
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)
wenzelm@60500
   132
  from \<open>f \<lesssim> g\<close> 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"
wenzelm@60500
   136
    with \<open>\<not> g \<lesssim> f\<close> 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
wenzelm@60500
   149
text \<open>
wenzelm@59113
   150
  I did not find 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.
wenzelm@60500
   164
\<close>
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
wenzelm@60500
   171
  from assms \<open>1 > 0\<close> 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
wenzelm@60500
   180
  with \<open>1 > 0\<close> 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
wenzelm@60500
   190
subsection \<open>@{text "\<lesssim>"} is a preorder\<close>
haftmann@51263
   191
wenzelm@60500
   192
text \<open>This yields all lemmas relating @{text "\<lesssim>"}, @{text "\<prec>"} and @{text "\<cong>"}.\<close>
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
wenzelm@60500
   210
      from \<open>f \<lesssim> g\<close> obtain n\<^sub>1 c\<^sub>1
wenzelm@53015
   211
        where "c\<^sub>1 > 0" and P\<^sub>1: "\<And>m. m > n\<^sub>1 \<Longrightarrow> f m \<le> c\<^sub>1 * g m"
haftmann@51263
   212
        by rule blast
wenzelm@60500
   213
      from \<open>g \<lesssim> h\<close> obtain n\<^sub>2 c\<^sub>2
wenzelm@53015
   214
        where "c\<^sub>2 > 0" and P\<^sub>2: "\<And>m. m > n\<^sub>2 \<Longrightarrow> g m \<le> c\<^sub>2 * h m"
haftmann@51263
   215
        by rule blast
wenzelm@53015
   216
      have "\<forall>m>max n\<^sub>1 n\<^sub>2. f m \<le> (c\<^sub>1 * c\<^sub>2) * h m"
haftmann@51263
   217
      proof (rule allI, rule impI)
haftmann@51263
   218
        fix m
wenzelm@53015
   219
        assume Q: "m > max n\<^sub>1 n\<^sub>2"
wenzelm@53015
   220
        from P\<^sub>1 Q have *: "f m \<le> c\<^sub>1 * g m" by simp
wenzelm@53015
   221
        from P\<^sub>2 Q have "g m \<le> c\<^sub>2 * h m" by simp
wenzelm@60500
   222
        with \<open>c\<^sub>1 > 0\<close> have "c\<^sub>1 * g m \<le> (c\<^sub>1 * c\<^sub>2) * h m" by simp
wenzelm@53015
   223
        with * show "f m \<le> (c\<^sub>1 * c\<^sub>2) * h m" by (rule order_trans)
haftmann@51263
   224
      qed
wenzelm@53015
   225
      then have "\<exists>n. \<forall>m>n. f m \<le> (c\<^sub>1 * c\<^sub>2) * h m" by rule
wenzelm@60500
   226
      moreover from \<open>c\<^sub>1 > 0\<close> \<open>c\<^sub>2 > 0\<close> have "c\<^sub>1 * c\<^sub>2 > 0" by simp
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"
wenzelm@53015
   237
      then obtain n c\<^sub>1 c\<^sub>2 where "c\<^sub>1 > 0" and "c\<^sub>2 > 0"
wenzelm@53015
   238
        and *: "\<And>m. m > n \<Longrightarrow> f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m"
haftmann@51263
   239
        by rule blast
wenzelm@53015
   240
      have "\<forall>m>n. f m \<le> c\<^sub>1 * g m"
haftmann@51263
   241
      proof (rule allI, rule impI)
haftmann@51263
   242
        fix m
haftmann@51263
   243
        assume "m > n"
wenzelm@53015
   244
        with * show "f m \<le> c\<^sub>1 * g m" by simp
haftmann@51263
   245
      qed
wenzelm@60500
   246
      with \<open>c\<^sub>1 > 0\<close> 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" ..
wenzelm@53015
   248
      have "\<forall>m>n. g m \<le> c\<^sub>2 * f m"
haftmann@51263
   249
      proof (rule allI, rule impI)
haftmann@51263
   250
        fix m
haftmann@51263
   251
        assume "m > n"
wenzelm@53015
   252
        with * show "g m \<le> c\<^sub>2 * f m" by simp
haftmann@51263
   253
      qed
wenzelm@60500
   254
      with \<open>c\<^sub>2 > 0\<close> 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" ..
wenzelm@60500
   256
      from \<open>f \<lesssim> g\<close> and \<open>g \<lesssim> f\<close> 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
wenzelm@60500
   260
      from \<open>f \<lesssim> g\<close> obtain n\<^sub>1 c\<^sub>1 where "c\<^sub>1 > 0"
wenzelm@53015
   261
        and P\<^sub>1: "\<And>m. m > n\<^sub>1 \<Longrightarrow> f m \<le> c\<^sub>1 * g m" by rule blast
wenzelm@60500
   262
      from \<open>g \<lesssim> f\<close> obtain n\<^sub>2 c\<^sub>2 where "c\<^sub>2 > 0"
wenzelm@53015
   263
        and P\<^sub>2: "\<And>m. m > n\<^sub>2 \<Longrightarrow> g m \<le> c\<^sub>2 * f m" by rule blast
wenzelm@53015
   264
      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"
haftmann@51263
   265
      proof (rule allI, rule impI)
haftmann@51263
   266
        fix m
wenzelm@53015
   267
        assume Q: "m > max n\<^sub>1 n\<^sub>2"
wenzelm@53015
   268
        from P\<^sub>1 Q have "f m \<le> c\<^sub>1 * g m" by simp
wenzelm@53015
   269
        moreover from P\<^sub>2 Q have "g m \<le> c\<^sub>2 * f m" by simp
wenzelm@53015
   270
        ultimately show "f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" ..
haftmann@51263
   271
      qed
wenzelm@60500
   272
      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.
wenzelm@53015
   273
        \<forall>m>n. f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>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
wenzelm@60500
   280
subsection \<open>Simple examples\<close>
haftmann@31381
   281
wenzelm@60500
   282
text \<open>
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
wenzelm@59113
   285
  intended as complete construction set for typical functions, here surely something
haftmann@51263
   286
  has to be added yet.
wenzelm@60500
   287
\<close>
haftmann@51263
   288
wenzelm@60500
   289
text \<open>@{prop "(\<lambda>n. f n + k) \<cong> f"}\<close>
haftmann@51263
   290
wenzelm@60500
   291
text \<open>@{prop "(\<lambda>n. Suc k * f n) \<cong> f"}\<close>
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
  
wenzelm@60500
   315
text \<open>@{prop "Discrete.log \<prec> Discrete.sqrt"}\<close>
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"
wenzelm@53015
   321
  have "\<forall>m>(Suc c)\<^sup>2. c * Discrete.sqrt m < id m"
haftmann@51263
   322
  proof (rule allI, rule impI)
haftmann@51263
   323
    fix m
wenzelm@53015
   324
    assume "(Suc c)\<^sup>2 < m"
wenzelm@53015
   325
    then have "(Suc c)\<^sup>2 \<le> m" by simp
wenzelm@53015
   326
    with mono_sqrt have "Discrete.sqrt ((Suc c)\<^sup>2) \<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
wenzelm@60500
   329
    moreover from \<open>(Suc c)\<^sup>2 < m\<close> 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
wenzelm@53015
   337
lemma "id \<prec> (\<lambda>n. n\<^sup>2)"
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
wenzelm@60500
   343
text \<open>@{prop "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. 2 ^ n)"}\<close>
haftmann@31381
   344
haftmann@31381
   345
end
haftmann@51263
   346