| author | ballarin |
| Wed, 10 Dec 2008 14:21:42 +0100 | |
| changeset 29035 | b0a0843dfd99 |
| parent 28952 | 15a4b2cf8c34 |
| 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 |
|
| 20550 | 16 |
lemma bigo_LIMSEQ1: "f =o O(g) ==> g ----> 0 ==> f ----> (0::real)" |
|
17211
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 |
| 20550 | 41 |
==> g ----> (a::real)" |
|
17211
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 |
| 26806 | 45 |
apply (simp only: fun_diff_def) |
|
17211
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 |