4 section \<open>Comparing growth of functions on natural numbers by a preorder relation\<close> |
4 section \<open>Comparing growth of functions on natural numbers by a preorder relation\<close> |
5 |
5 |
6 theory Function_Growth |
6 theory Function_Growth |
7 imports Main Preorder Discrete |
7 imports Main Preorder Discrete |
8 begin |
8 begin |
|
9 |
|
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 |
9 |
43 |
10 subsection \<open>Motivation\<close> |
44 subsection \<open>Motivation\<close> |
11 |
45 |
12 text \<open> |
46 text \<open> |
13 When comparing growth of functions in computer science, it is common to adhere |
47 When comparing growth of functions in computer science, it is common to adhere |
78 text \<open> |
112 text \<open> |
79 This yields \<open>f \<cong> g \<longleftrightarrow> f \<in> \<Theta>(g)\<close>. Concerning \<open>c\<^sub>1\<close> and \<open>c\<^sub>2\<close> |
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> |
80 restricted to @{typ nat}, see note above on \<open>(\<lesssim>)\<close>. |
114 restricted to @{typ nat}, see note above on \<open>(\<lesssim>)\<close>. |
81 \<close> |
115 \<close> |
82 |
116 |
83 lemma equiv_funI [intro?]: |
117 lemma equiv_funI: |
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" |
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" |
85 shows "f \<cong> g" |
119 shows "f \<cong> g" |
86 unfolding equiv_fun_def by (rule assms) |
120 unfolding equiv_fun_def by (rule assms) |
87 |
121 |
88 lemma not_equiv_funI: |
122 lemma not_equiv_funI: |
89 assumes "\<And>c\<^sub>1 c\<^sub>2 n. c\<^sub>1 > 0 \<Longrightarrow> c\<^sub>2 > 0 \<Longrightarrow> |
123 assumes "\<And>c\<^sub>1 c\<^sub>2 n. c\<^sub>1 > 0 \<Longrightarrow> c\<^sub>2 > 0 \<Longrightarrow> |
90 \<exists>m>n. c\<^sub>1 * f m < g m \<or> c\<^sub>2 * g m < f m" |
124 \<exists>m>n. c\<^sub>1 * f m < g m \<or> c\<^sub>2 * g m < f m" |
91 shows "\<not> f \<cong> g" |
125 shows "\<not> f \<cong> g" |
92 using assms unfolding equiv_fun_def linorder_not_le [symmetric] by blast |
126 using assms unfolding equiv_fun_def linorder_not_le [symmetric] by blast |
93 |
127 |
94 lemma equiv_funE [elim?]: |
128 lemma equiv_funE: |
95 assumes "f \<cong> g" |
129 assumes "f \<cong> g" |
96 obtains n c\<^sub>1 c\<^sub>2 where "c\<^sub>1 > 0" and "c\<^sub>2 > 0" |
130 obtains n c\<^sub>1 c\<^sub>2 where "c\<^sub>1 > 0" and "c\<^sub>2 > 0" |
97 and "\<And>m. m > n \<Longrightarrow> f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" |
131 and "\<And>m. m > n \<Longrightarrow> f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" |
98 using assms unfolding equiv_fun_def by blast |
132 using assms unfolding equiv_fun_def by blast |
99 |
133 |
158 the definition of \<open>(\<prec>)\<close>. In the typical definition of \<open>o\<close>, |
192 the definition of \<open>(\<prec>)\<close>. In the typical definition of \<open>o\<close>, |
159 it occurs on the \emph{right} hand side of the \<open>(>)\<close>. The reason |
193 it occurs on the \emph{right} hand side of the \<open>(>)\<close>. The reason |
160 is that the situation is dual to the definition of \<open>O\<close>: the definition |
194 is that the situation is dual to the definition of \<open>O\<close>: the definition |
161 works since \<open>c\<close> may become arbitrary small. Since this is not possible |
195 works since \<open>c\<close> may become arbitrary small. Since this is not possible |
162 within @{term \<nat>}, we push the coefficient to the left hand side instead such |
196 within @{term \<nat>}, we push the coefficient to the left hand side instead such |
163 that it become arbitrary big instead. |
197 that it may become arbitrary big instead. |
164 \<close> |
198 \<close> |
165 |
199 |
166 lemma less_fun_strongI: |
200 lemma less_fun_strongI: |
167 assumes "\<And>c. c > 0 \<Longrightarrow> \<exists>n. \<forall>m>n. c * f m < g m" |
201 assumes "\<And>c. c > 0 \<Longrightarrow> \<exists>n. \<forall>m>n. c * f m < g m" |
168 shows "f \<prec> g" |
202 shows "f \<prec> g" |
190 subsection \<open>\<open>\<lesssim>\<close> is a preorder\<close> |
224 subsection \<open>\<open>\<lesssim>\<close> is a preorder\<close> |
191 |
225 |
192 text \<open>This yields all lemmas relating \<open>\<lesssim>\<close>, \<open>\<prec>\<close> and \<open>\<cong>\<close>.\<close> |
226 text \<open>This yields all lemmas relating \<open>\<lesssim>\<close>, \<open>\<prec>\<close> and \<open>\<cong>\<close>.\<close> |
193 |
227 |
194 interpretation fun_order: preorder_equiv less_eq_fun less_fun |
228 interpretation fun_order: preorder_equiv less_eq_fun less_fun |
195 rewrites "preorder_equiv.equiv less_eq_fun = equiv_fun" |
229 rewrites "fun_order.equiv = equiv_fun" |
196 proof - |
230 proof - |
197 interpret preorder: preorder_equiv less_eq_fun less_fun |
231 interpret preorder: preorder_equiv less_eq_fun less_fun |
198 proof |
232 proof |
199 fix f g h |
233 fix f g h |
200 show "f \<lesssim> f" |
234 show "f \<lesssim> f" |
234 show "f \<lesssim> g \<and> g \<lesssim> f \<longleftrightarrow> f \<cong> g" |
268 show "f \<lesssim> g \<and> g \<lesssim> f \<longleftrightarrow> f \<cong> g" |
235 proof |
269 proof |
236 assume "f \<cong> g" |
270 assume "f \<cong> g" |
237 then obtain n c\<^sub>1 c\<^sub>2 where "c\<^sub>1 > 0" and "c\<^sub>2 > 0" |
271 then obtain n c\<^sub>1 c\<^sub>2 where "c\<^sub>1 > 0" and "c\<^sub>2 > 0" |
238 and *: "\<And>m. m > n \<Longrightarrow> f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" |
272 and *: "\<And>m. m > n \<Longrightarrow> f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" |
239 by rule blast |
273 by (rule equiv_funE) blast |
240 have "\<forall>m>n. f m \<le> c\<^sub>1 * g m" |
274 have "\<forall>m>n. f m \<le> c\<^sub>1 * g m" |
241 proof (rule allI, rule impI) |
275 proof (rule allI, rule impI) |
242 fix m |
276 fix m |
243 assume "m > n" |
277 assume "m > n" |
244 with * show "f m \<le> c\<^sub>1 * g m" by simp |
278 with * show "f m \<le> c\<^sub>1 * g m" by simp |
269 moreover from P\<^sub>2 Q have "g m \<le> c\<^sub>2 * f m" by simp |
303 moreover from P\<^sub>2 Q have "g m \<le> c\<^sub>2 * f m" by simp |
270 ultimately show "f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" .. |
304 ultimately show "f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" .. |
271 qed |
305 qed |
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. |
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. |
273 \<forall>m>n. f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" by blast |
307 \<forall>m>n. f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" by blast |
274 then show "f \<cong> g" .. |
308 then show "f \<cong> g" by (rule equiv_funI) |
275 qed |
309 qed |
276 qed |
310 qed |
277 qed |
311 qed |
|
312 |
|
313 declare fun_order.antisym [intro?] |
278 |
314 |
279 |
315 |
280 subsection \<open>Simple examples\<close> |
316 subsection \<open>Simple examples\<close> |
281 |
317 |
282 text \<open> |
318 text \<open> |
286 has to be added yet. |
322 has to be added yet. |
287 \<close> |
323 \<close> |
288 |
324 |
289 text \<open>@{prop "(\<lambda>n. f n + k) \<cong> f"}\<close> |
325 text \<open>@{prop "(\<lambda>n. f n + k) \<cong> f"}\<close> |
290 |
326 |
291 text \<open>@{prop "(\<lambda>n. Suc k * f n) \<cong> f"}\<close> |
327 lemma equiv_fun_mono_const: |
292 |
328 assumes "mono f" and "\<exists>n. f n > 0" |
293 lemma "f \<lesssim> (\<lambda>n. f n + g n)" |
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 |
|
358 |
|
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)" |
294 by rule auto |
392 by rule auto |
295 |
393 |
296 lemma "(\<lambda>_. 0) \<prec> (\<lambda>n. Suc k)" |
394 lemma |
|
395 "(\<lambda>_. 0) \<prec> (\<lambda>n. Suc k)" |
297 by (rule less_fun_strongI) auto |
396 by (rule less_fun_strongI) auto |
298 |
397 |
299 lemma "(\<lambda>_. k) \<prec> Discrete.log" |
398 lemma |
|
399 "(\<lambda>_. k) \<prec> Discrete.log" |
300 proof (rule less_fun_strongI) |
400 proof (rule less_fun_strongI) |
301 fix c :: nat |
401 fix c :: nat |
302 have "\<forall>m>2 ^ (Suc (c * k)). c * k < Discrete.log m" |
402 have "\<forall>m>2 ^ (Suc (c * k)). c * k < Discrete.log m" |
303 proof (rule allI, rule impI) |
403 proof (rule allI, rule impI) |
304 fix m :: nat |
404 fix m :: nat |
309 moreover have "c * k < Discrete.log (2 ^ (Suc (c * k)))" by simp |
409 moreover have "c * k < Discrete.log (2 ^ (Suc (c * k)))" by simp |
310 ultimately show "c * k < Discrete.log m" by auto |
410 ultimately show "c * k < Discrete.log m" by auto |
311 qed |
411 qed |
312 then show "\<exists>n. \<forall>m>n. c * k < Discrete.log m" .. |
412 then show "\<exists>n. \<forall>m>n. c * k < Discrete.log m" .. |
313 qed |
413 qed |
314 |
414 |
|
415 (*lemma |
|
416 "Discrete.log \<prec> Discrete.sqrt" |
|
417 proof (rule less_fun_strongI)*) |
315 text \<open>@{prop "Discrete.log \<prec> Discrete.sqrt"}\<close> |
418 text \<open>@{prop "Discrete.log \<prec> Discrete.sqrt"}\<close> |
316 |
419 |
317 lemma "Discrete.sqrt \<prec> id" |
420 lemma |
|
421 "Discrete.sqrt \<prec> id" |
318 proof (rule less_fun_strongI) |
422 proof (rule less_fun_strongI) |
319 fix c :: nat |
423 fix c :: nat |
320 assume "0 < c" |
424 assume "0 < c" |
321 have "\<forall>m>(Suc c)\<^sup>2. c * Discrete.sqrt m < id m" |
425 have "\<forall>m>(Suc c)\<^sup>2. c * Discrete.sqrt m < id m" |
322 proof (rule allI, rule impI) |
426 proof (rule allI, rule impI) |
332 finally show "c * Discrete.sqrt m < id m" by simp |
436 finally show "c * Discrete.sqrt m < id m" by simp |
333 qed |
437 qed |
334 then show "\<exists>n. \<forall>m>n. c * Discrete.sqrt m < id m" .. |
438 then show "\<exists>n. \<forall>m>n. c * Discrete.sqrt m < id m" .. |
335 qed |
439 qed |
336 |
440 |
337 lemma "id \<prec> (\<lambda>n. n\<^sup>2)" |
441 lemma |
|
442 "id \<prec> (\<lambda>n. n\<^sup>2)" |
338 by (rule less_fun_strongI) (auto simp add: power2_eq_square) |
443 by (rule less_fun_strongI) (auto simp add: power2_eq_square) |
339 |
444 |
340 lemma "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. n ^ Suc k)" |
445 lemma |
|
446 "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. n ^ Suc k)" |
341 by (rule less_fun_strongI) auto |
447 by (rule less_fun_strongI) auto |
342 |
448 |
|
449 (*lemma |
|
450 "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. 2 ^ n)" |
|
451 proof (rule less_fun_strongI)*) |
343 text \<open>@{prop "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. 2 ^ n)"}\<close> |
452 text \<open>@{prop "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. 2 ^ n)"}\<close> |
344 |
453 |
345 end |
454 end |
346 |
|