src/HOL/Library/Function_Growth.thy
author wenzelm
Wed Mar 08 10:50:59 2017 +0100 (2017-03-08)
changeset 65151 a7394aa4d21c
parent 63540 f8652d0534fa
permissions -rw-r--r--
tuned proofs;
haftmann@61833
     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
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 \<Rightarrow> '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 "\<not> x < y"
haftmann@61831
    24
    then have "y \<le> x" by simp
haftmann@61831
    25
    with \<open>mono f\<close> obtain "f y \<le> f x" by (rule monoE)
haftmann@61831
    26
    with \<open>f x < f y\<close> 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 \<noteq> 0"
haftmann@61831
    35
  assumes "m \<ge> n"
haftmann@61831
    36
  shows "a ^ (m - n) = (a ^ m) div (a ^ n)"
haftmann@61831
    37
proof -
wenzelm@63040
    38
  define q where "q = m - n"
wenzelm@63540
    39
  with assms have "m = q + n" by (simp add: q_def)
wenzelm@63540
    40
  with q_def show ?thesis using \<open>a \<noteq> 0\<close> by (simp add: power_add)
haftmann@61831
    41
qed
haftmann@61831
    42
haftmann@61831
    43
wenzelm@60500
    44
subsection \<open>Motivation\<close>
haftmann@51263
    45
wenzelm@60500
    46
text \<open>
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 \<open>f = O(g)\<close> for \<open>f \<in> O(g)\<close> 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 \<open>\<lesssim>\<close> on functions such that
wenzelm@61585
    54
  \<open>f \<lesssim> g \<longleftrightarrow> f \<in> O(g)\<close>.  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
  \<open>(\<lambda>n. 0) \<lesssim> (\<lambda>n. k) \<lesssim> Discrete.log \<lesssim> Discrete.sqrt \<lesssim> id \<lesssim> \<dots>\<close>.
wenzelm@60500
    58
\<close>
haftmann@31381
    59
wenzelm@60500
    60
subsection \<open>Model\<close>
haftmann@31381
    61
wenzelm@60500
    62
text \<open>
wenzelm@61585
    63
  Our growth functions are of type \<open>\<nat> \<Rightarrow> \<nat>\<close>.  This is different
wenzelm@61585
    64
  to the usual conventions for Landau symbols for which \<open>\<real> \<Rightarrow> \<real>\<close>
wenzelm@61585
    65
  would be appropriate, but we argue that \<open>\<real> \<Rightarrow> \<real>\<close> 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 \<open>\<nat>\<close>, something
haftmann@51263
    69
  we discuss at the particular definitions.
wenzelm@60500
    70
\<close>
haftmann@31381
    71
wenzelm@61585
    72
subsection \<open>The \<open>\<lesssim>\<close> relation\<close>
haftmann@31381
    73
haftmann@51263
    74
definition less_eq_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<lesssim>" 50)
haftmann@51263
    75
where
haftmann@51263
    76
  "f \<lesssim> g \<longleftrightarrow> (\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m)"
haftmann@31381
    77
wenzelm@60500
    78
text \<open>
wenzelm@61585
    79
  This yields \<open>f \<lesssim> g \<longleftrightarrow> f \<in> O(g)\<close>.  Note that \<open>c\<close> is restricted to
wenzelm@61585
    80
  \<open>\<nat>\<close>.  This does not pose any problems since if \<open>f \<in> O(g)\<close> holds for
wenzelm@61585
    81
  a \<open>c \<in> \<real>\<close>, it also holds for \<open>\<lceil>c\<rceil> \<in> \<nat>\<close> by transitivity.
wenzelm@60500
    82
\<close>
haftmann@51263
    83
haftmann@51263
    84
lemma less_eq_funI [intro?]:
haftmann@51263
    85
  assumes "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m"
haftmann@31381
    86
  shows "f \<lesssim> 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 "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * g m < f m"
haftmann@31381
    91
  shows "\<not> f \<lesssim> 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 \<lesssim> g"
haftmann@51263
    96
  obtains n c where "c > 0" and "\<And>m. m > n \<Longrightarrow> f m \<le> 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 "\<not> f \<lesssim> 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 \<open>The \<open>\<approx>\<close> relation, the equivalence relation induced by \<open>\<lesssim>\<close>\<close>
haftmann@31381
   106
haftmann@51263
   107
definition equiv_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<cong>" 50)
haftmann@51263
   108
where
haftmann@51263
   109
  "f \<cong> g \<longleftrightarrow>
wenzelm@53015
   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)"
haftmann@31381
   111
wenzelm@60500
   112
text \<open>
wenzelm@61585
   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>
wenzelm@61585
   114
  restricted to @{typ nat}, see note above on \<open>(\<lesssim>)\<close>.
wenzelm@60500
   115
\<close>
haftmann@51263
   116
haftmann@61831
   117
lemma equiv_funI:
wenzelm@53015
   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"
haftmann@31381
   119
  shows "f \<cong> 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 "\<And>c\<^sub>1 c\<^sub>2 n. c\<^sub>1 > 0 \<Longrightarrow> c\<^sub>2 > 0 \<Longrightarrow>
wenzelm@53015
   124
    \<exists>m>n. c\<^sub>1 * f m < g m \<or> c\<^sub>2 * g m < f m"
haftmann@31381
   125
  shows "\<not> f \<cong> 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 \<cong> 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 "\<And>m. m > n \<Longrightarrow> f m \<le> c\<^sub>1 * g m \<and> g m \<le> 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 "\<not> f \<cong> 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 \<or> 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 \<open>The \<open>\<prec>\<close> relation, the strict part of \<open>\<lesssim>\<close>\<close>
haftmann@31381
   143
haftmann@51263
   144
definition less_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<prec>" 50)
haftmann@51263
   145
where
haftmann@31381
   146
  "f \<prec> g \<longleftrightarrow> f \<lesssim> g \<and> \<not> g \<lesssim> f"
haftmann@31381
   147
haftmann@51263
   148
lemma less_funI:
haftmann@51263
   149
  assumes "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m"
haftmann@51263
   150
    and "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * f m < g m"
haftmann@31381
   151
  shows "f \<prec> 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 "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * g m < f m"
haftmann@51263
   156
    and "\<exists>c>0. \<exists>n. \<forall>m>n. g m \<le> c * f m"
haftmann@51263
   157
  shows "\<not> f \<prec> 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 \<prec> g"
haftmann@51263
   162
  obtains n c where "c > 0" and "\<And>m. m > n \<Longrightarrow> f m \<le> c * g m"
haftmann@51263
   163
    and "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * f m < g m"
haftmann@51263
   164
proof -
haftmann@51263
   165
  from assms have "f \<lesssim> g" and "\<not> g \<lesssim> f" by (simp_all add: less_fun_def)
wenzelm@63060
   166
  from \<open>f \<lesssim> g\<close> obtain n c where *:"c > 0" "m > n \<Longrightarrow> f m \<le> c * g m" for 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 \<open>\<not> g \<lesssim> f\<close> 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 **: "\<exists>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 "\<not> f \<prec> g" and "c > 0"
haftmann@51263
   179
  obtains m where "m > n" and "c * g m < f m"
haftmann@51263
   180
    | d q where "\<And>m. d > 0 \<Longrightarrow> m > q \<Longrightarrow> g q \<le> 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 \<open>
wenzelm@61585
   184
  I did not find a proof for \<open>f \<prec> g \<longleftrightarrow> f \<in> o(g)\<close>.  Maybe this only
wenzelm@61585
   185
  holds if \<open>f\<close> and/or \<open>g\<close> are of a certain class of functions.
wenzelm@61585
   186
  However \<open>f \<in> o(g) \<longrightarrow> f \<prec> g\<close> is provable, and this yields a
haftmann@51263
   187
  handy introduction rule.
haftmann@51263
   188
wenzelm@61585
   189
  Note that D. Knuth ignores \<open>o\<close> altogether.  So what \dots
haftmann@51263
   190
wenzelm@61585
   191
  Something still has to be said about the coefficient \<open>c\<close> in
wenzelm@61585
   192
  the definition of \<open>(\<prec>)\<close>.  In the typical definition of \<open>o\<close>,
wenzelm@61585
   193
  it occurs on the \emph{right} hand side of the \<open>(>)\<close>.  The reason
wenzelm@61585
   194
  is that the situation is dual to the definition of \<open>O\<close>: the definition
wenzelm@61585
   195
  works since \<open>c\<close> may become arbitrary small.  Since this is not possible
haftmann@51263
   196
  within @{term \<nat>}, we push the coefficient to the left hand side instead such
haftmann@61831
   197
  that it may become arbitrary big instead.
wenzelm@60500
   198
\<close>
haftmann@31381
   199
haftmann@51263
   200
lemma less_fun_strongI:
haftmann@51263
   201
  assumes "\<And>c. c > 0 \<Longrightarrow> \<exists>n. \<forall>m>n. c * f m < g m"
haftmann@51263
   202
  shows "f \<prec> g"
haftmann@51263
   203
proof (rule less_funI)
haftmann@51263
   204
  have "1 > (0::nat)" by simp
wenzelm@63060
   205
  with assms [OF this] obtain n where *: "m > n \<Longrightarrow> 1 * f m < g m" for m
wenzelm@63060
   206
    by blast
haftmann@51263
   207
  have "\<forall>m>n. f m \<le> 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 \<le> 1 * g m" by simp
haftmann@51263
   213
  qed
wenzelm@60500
   214
  with \<open>1 > 0\<close> show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m" by blast
haftmann@51263
   215
  fix c n :: nat
haftmann@51263
   216
  assume "c > 0"
wenzelm@63060
   217
  with assms obtain q where "m > q \<Longrightarrow> c * f m < g m" for 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 "\<exists>m>n. c * f m < g m" by blast
haftmann@51263
   221
qed
haftmann@31381
   222
haftmann@51263
   223
wenzelm@61585
   224
subsection \<open>\<open>\<lesssim>\<close> is a preorder\<close>
haftmann@51263
   225
wenzelm@61585
   226
text \<open>This yields all lemmas relating \<open>\<lesssim>\<close>, \<open>\<prec>\<close> and \<open>\<cong>\<close>.\<close>
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 \<lesssim> f"
haftmann@51263
   235
    proof
haftmann@51263
   236
      have "\<exists>n. \<forall>m>n. f m \<le> 1 * f m" by auto
haftmann@51263
   237
      then show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * f m" by blast
haftmann@51263
   238
    qed
haftmann@51263
   239
    show "f \<prec> g \<longleftrightarrow> f \<lesssim> g \<and> \<not> g \<lesssim> f"
haftmann@51263
   240
      by (fact less_fun_def)
haftmann@51263
   241
    assume "f \<lesssim> g" and "g \<lesssim> h"
haftmann@51263
   242
    show "f \<lesssim> h"
haftmann@51263
   243
    proof
wenzelm@60500
   244
      from \<open>f \<lesssim> g\<close> obtain n\<^sub>1 c\<^sub>1
wenzelm@53015
   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"
haftmann@51263
   246
        by rule blast
wenzelm@60500
   247
      from \<open>g \<lesssim> h\<close> obtain n\<^sub>2 c\<^sub>2
wenzelm@53015
   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"
haftmann@51263
   249
        by rule blast
wenzelm@53015
   250
      have "\<forall>m>max n\<^sub>1 n\<^sub>2. f m \<le> (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 \<le> c\<^sub>1 * g m" by simp
wenzelm@53015
   255
        from P\<^sub>2 Q have "g m \<le> c\<^sub>2 * h m" by simp
wenzelm@60500
   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
wenzelm@53015
   257
        with * show "f m \<le> (c\<^sub>1 * c\<^sub>2) * h m" by (rule order_trans)
haftmann@51263
   258
      qed
wenzelm@53015
   259
      then have "\<exists>n. \<forall>m>n. f m \<le> (c\<^sub>1 * c\<^sub>2) * h m" by rule
wenzelm@60500
   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
haftmann@51263
   261
      ultimately show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> 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 \<lesssim> g \<and> g \<lesssim> f \<longleftrightarrow> f \<cong> g"
haftmann@51263
   269
    proof
haftmann@51263
   270
      assume "f \<cong> 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 *: "\<And>m. m > n \<Longrightarrow> f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m"
haftmann@61831
   273
        by (rule equiv_funE) blast
wenzelm@53015
   274
      have "\<forall>m>n. f m \<le> 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 \<le> c\<^sub>1 * g m" by simp
haftmann@51263
   279
      qed
wenzelm@60500
   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
haftmann@51263
   281
      then have "f \<lesssim> g" ..
wenzelm@53015
   282
      have "\<forall>m>n. g m \<le> 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 \<le> c\<^sub>2 * f m" by simp
haftmann@51263
   287
      qed
wenzelm@60500
   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
haftmann@51263
   289
      then have "g \<lesssim> f" ..
wenzelm@60500
   290
      from \<open>f \<lesssim> g\<close> and \<open>g \<lesssim> f\<close> show "f \<lesssim> g \<and> g \<lesssim> f" ..
haftmann@51263
   291
    next
haftmann@51263
   292
      assume "f \<lesssim> g \<and> g \<lesssim> f"
haftmann@51263
   293
      then have "f \<lesssim> g" and "g \<lesssim> f" by auto
wenzelm@60500
   294
      from \<open>f \<lesssim> g\<close> obtain n\<^sub>1 c\<^sub>1 where "c\<^sub>1 > 0"
wenzelm@53015
   295
        and P\<^sub>1: "\<And>m. m > n\<^sub>1 \<Longrightarrow> f m \<le> c\<^sub>1 * g m" by rule blast
wenzelm@60500
   296
      from \<open>g \<lesssim> f\<close> obtain n\<^sub>2 c\<^sub>2 where "c\<^sub>2 > 0"
wenzelm@53015
   297
        and P\<^sub>2: "\<And>m. m > n\<^sub>2 \<Longrightarrow> g m \<le> c\<^sub>2 * f m" by rule blast
wenzelm@53015
   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"
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 \<le> c\<^sub>1 * g m" by simp
wenzelm@53015
   303
        moreover from P\<^sub>2 Q have "g m \<le> c\<^sub>2 * f m" by simp
wenzelm@53015
   304
        ultimately show "f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" ..
haftmann@51263
   305
      qed
wenzelm@60500
   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.
wenzelm@53015
   307
        \<forall>m>n. f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" by blast
haftmann@61831
   308
      then show "f \<cong> 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 \<open>Simple examples\<close>
haftmann@31381
   317
wenzelm@60500
   318
text \<open>
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
\<close>
haftmann@51263
   324
wenzelm@60500
   325
text \<open>@{prop "(\<lambda>n. f n + k) \<cong> f"}\<close>
haftmann@51263
   326
haftmann@61831
   327
lemma equiv_fun_mono_const:
haftmann@61831
   328
  assumes "mono f" and "\<exists>n. f n > 0"
haftmann@61831
   329
  shows "(\<lambda>n. f n + k) \<cong> 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 "(\<lambda>n. f n + k) \<lesssim> f"
haftmann@61831
   337
    proof
wenzelm@61975
   338
      from \<open>\<exists>n. f n > 0\<close> obtain n where "f n > 0" ..
haftmann@61831
   339
      have "\<forall>m>n. f m + k \<le> Suc k * f m"
haftmann@61831
   340
      proof (rule allI, rule impI)
haftmann@61831
   341
        fix m
haftmann@61831
   342
        assume "n < m"
wenzelm@61975
   343
        with \<open>mono f\<close> have "f n \<le> f m"
haftmann@61831
   344
          using less_imp_le_nat monoE by blast
wenzelm@61975
   345
        with  \<open>0 < f n\<close> 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 \<le> Suc k * f m" by simp
haftmann@61831
   348
      qed
haftmann@61831
   349
      then show "\<exists>c>0. \<exists>n. \<forall>m>n. f m + k \<le> c * f m" by blast
haftmann@61831
   350
    qed
haftmann@61831
   351
    show "f \<lesssim> (\<lambda>n. f n + k)"
haftmann@61831
   352
    proof
haftmann@61831
   353
      have "f m \<le> 1 * (f m + k)" for m by simp
haftmann@61831
   354
      then show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> 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 "(\<lambda>n. f n + k) \<cong> 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 "\<exists>n. 0 < f n"
haftmann@61831
   365
  proof (rule ccontr)
haftmann@61831
   366
    assume "\<not> (\<exists>n. 0 < f n)"
haftmann@61831
   367
    then have "\<And>n. f n = 0" by simp
haftmann@61831
   368
    then have "f 0 = f 1" by simp
wenzelm@61975
   369
    moreover from \<open>strict_mono f\<close> 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
  "(\<lambda>n. Suc k * f n) \<cong> f"
haftmann@61831
   377
proof
haftmann@61831
   378
  show "(\<lambda>n. Suc k * f n) \<lesssim> f"
haftmann@61831
   379
  proof
haftmann@61831
   380
    have "Suc k * f m \<le> Suc k * f m" for m by simp
haftmann@61831
   381
    then show "\<exists>c>0. \<exists>n. \<forall>m>n. Suc k * f m \<le> c * f m" by blast
haftmann@61831
   382
  qed
haftmann@61831
   383
  show "f \<lesssim> (\<lambda>n. Suc k * f n)"
haftmann@61831
   384
  proof
haftmann@61831
   385
    have "f m \<le> 1 * (Suc k * f m)" for m by simp
haftmann@61831
   386
    then show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> 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 \<lesssim> (\<lambda>n. f n + g n)"
wenzelm@51264
   392
  by rule auto
haftmann@51263
   393
haftmann@61831
   394
lemma
haftmann@61831
   395
  "(\<lambda>_. 0) \<prec> (\<lambda>n. Suc k)"
wenzelm@51264
   396
  by (rule less_fun_strongI) auto
haftmann@51263
   397
haftmann@61831
   398
lemma
haftmann@61831
   399
  "(\<lambda>_. k) \<prec> Discrete.log"
haftmann@51263
   400
proof (rule less_fun_strongI)
haftmann@51263
   401
  fix c :: nat
haftmann@51263
   402
  have "\<forall>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) \<le> m" by simp
haftmann@51263
   407
    with log_mono have "Discrete.log (2 ^ (Suc (c * k))) \<le> 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 "\<exists>n. \<forall>m>n. c * k < Discrete.log m" ..
haftmann@51263
   413
qed
haftmann@61831
   414
haftmann@61831
   415
(*lemma
haftmann@61831
   416
  "Discrete.log \<prec> Discrete.sqrt"
haftmann@61831
   417
proof (rule less_fun_strongI)*)
wenzelm@60500
   418
text \<open>@{prop "Discrete.log \<prec> Discrete.sqrt"}\<close>
haftmann@51263
   419
haftmann@61831
   420
lemma
haftmann@61831
   421
  "Discrete.sqrt \<prec> 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 "\<forall>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 \<le> m" by simp
wenzelm@53015
   430
    with mono_sqrt have "Discrete.sqrt ((Suc c)\<^sup>2) \<le> Discrete.sqrt m" by (rule monoE)
haftmann@51263
   431
    then have "Suc c \<le> Discrete.sqrt m" by simp
haftmann@51263
   432
    then have "c < Discrete.sqrt m" by simp
wenzelm@60500
   433
    moreover from \<open>(Suc c)\<^sup>2 < m\<close> 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 "\<dots> \<le> 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 "\<exists>n. \<forall>m>n. c * Discrete.sqrt m < id m" ..
haftmann@31381
   439
qed
haftmann@31381
   440
haftmann@61831
   441
lemma
haftmann@61831
   442
  "id \<prec> (\<lambda>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
  "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. n ^ Suc k)"
wenzelm@51264
   447
  by (rule less_fun_strongI) auto
haftmann@51263
   448
haftmann@61831
   449
(*lemma 
haftmann@61831
   450
  "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. 2 ^ n)"
haftmann@61831
   451
proof (rule less_fun_strongI)*)
wenzelm@60500
   452
text \<open>@{prop "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. 2 ^ n)"}\<close>
haftmann@31381
   453
haftmann@31381
   454
end