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