| author | kleing |
| Sun, 19 Feb 2006 13:21:32 +0100 | |
| changeset 19106 | 6e6b5b1fdc06 |
| parent 17211 | ebd268806589 |
| child 20550 | 5a925ad63f4d |
| permissions | -rw-r--r-- |
|
17211
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: HOL/Complex/ex/BigO_Complex.thy |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
3 |
Authors: Jeremy Avigad and Kevin Donnelly |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
4 |
*) |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
5 |
|
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
6 |
header {* Big O notation -- continued *}
|
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
7 |
|
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
8 |
theory BigO_Complex |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
9 |
imports BigO Complex |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
10 |
begin |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
11 |
|
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
12 |
text {*
|
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
13 |
Additional lemmas that require the \texttt{HOL-Complex} logic image.
|
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
14 |
*} |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
15 |
|
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
16 |
lemma bigo_LIMSEQ1: "f =o O(g) ==> g ----> 0 ==> f ----> 0" |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
17 |
apply (simp add: LIMSEQ_def bigo_alt_def) |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
18 |
apply clarify |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
19 |
apply (drule_tac x = "r / c" in spec) |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
20 |
apply (drule mp) |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
21 |
apply (erule divide_pos_pos) |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
22 |
apply assumption |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
23 |
apply clarify |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
24 |
apply (rule_tac x = no in exI) |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
25 |
apply (rule allI) |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
26 |
apply (drule_tac x = n in spec)+ |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
27 |
apply (rule impI) |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
28 |
apply (drule mp) |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
29 |
apply assumption |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
30 |
apply (rule order_le_less_trans) |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
31 |
apply assumption |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
32 |
apply (rule order_less_le_trans) |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
33 |
apply (subgoal_tac "c * abs(g n) < c * (r / c)") |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
34 |
apply assumption |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
35 |
apply (erule mult_strict_left_mono) |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
36 |
apply assumption |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
37 |
apply simp |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
38 |
done |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
39 |
|
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
40 |
lemma bigo_LIMSEQ2: "f =o g +o O(h) ==> h ----> 0 ==> f ----> a |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
41 |
==> g ----> a" |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
42 |
apply (drule set_plus_imp_minus) |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
43 |
apply (drule bigo_LIMSEQ1) |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
44 |
apply assumption |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
45 |
apply (simp only: func_diff) |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
46 |
apply (erule LIMSEQ_diff_approach_zero2) |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
47 |
apply assumption |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
48 |
done |
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
49 |
|
|
ebd268806589
Additional BigO lemmas that require the HOL-Complex logic image;
wenzelm
parents:
diff
changeset
|
50 |
end |