author | traytel |
Thu, 16 Jul 2015 12:23:22 +0200 | |
changeset 60728 | 26ffdb966759 |
parent 60500 | 903bb1495239 |
child 61585 | a9599d3d7610 |
permissions | -rw-r--r-- |
16932 | 1 |
(* Title: HOL/Library/BigO.thy |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
2 |
Authors: Jeremy Avigad and Kevin Donnelly |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
3 |
*) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
4 |
|
60500 | 5 |
section \<open>Big O notation\<close> |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
6 |
|
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
7 |
theory BigO |
38622 | 8 |
imports Complex_Main Function_Algebras Set_Algebras |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
9 |
begin |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
10 |
|
60500 | 11 |
text \<open> |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
12 |
This library is designed to support asymptotic ``big O'' calculations, |
17199
59c1bfc81d91
moved lemmas that require the HOL-Complex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset
|
13 |
i.e.~reasoning with expressions of the form $f = O(g)$ and $f = g + |
59c1bfc81d91
moved lemmas that require the HOL-Complex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset
|
14 |
O(h)$. An earlier version of this library is described in detail in |
58622 | 15 |
@{cite "Avigad-Donnelly"}. |
17199
59c1bfc81d91
moved lemmas that require the HOL-Complex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset
|
16 |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
17 |
The main changes in this version are as follows: |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
18 |
\begin{itemize} |
17199
59c1bfc81d91
moved lemmas that require the HOL-Complex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset
|
19 |
\item We have eliminated the @{text O} operator on sets. (Most uses of this seem |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
20 |
to be inessential.) |
17199
59c1bfc81d91
moved lemmas that require the HOL-Complex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset
|
21 |
\item We no longer use @{text "+"} as output syntax for @{text "+o"} |
55821 | 22 |
\item Lemmas involving @{text "sumr"} have been replaced by more general lemmas |
17199
59c1bfc81d91
moved lemmas that require the HOL-Complex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset
|
23 |
involving `@{text "setsum"}. |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
24 |
\item The library has been expanded, with e.g.~support for expressions of |
17199
59c1bfc81d91
moved lemmas that require the HOL-Complex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset
|
25 |
the form @{text "f < g + O(h)"}. |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
26 |
\end{itemize} |
17199
59c1bfc81d91
moved lemmas that require the HOL-Complex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset
|
27 |
|
59c1bfc81d91
moved lemmas that require the HOL-Complex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset
|
28 |
Note also since the Big O library includes rules that demonstrate set |
59c1bfc81d91
moved lemmas that require the HOL-Complex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset
|
29 |
inclusion, to use the automated reasoners effectively with the library |
59c1bfc81d91
moved lemmas that require the HOL-Complex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset
|
30 |
one should redeclare the theorem @{text "subsetI"} as an intro rule, |
59c1bfc81d91
moved lemmas that require the HOL-Complex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset
|
31 |
rather than as an @{text "intro!"} rule, for example, using |
59c1bfc81d91
moved lemmas that require the HOL-Complex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset
|
32 |
\isa{\isakeyword{declare}}~@{text "subsetI [del, intro]"}. |
60500 | 33 |
\<close> |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
34 |
|
60500 | 35 |
subsection \<open>Definitions\<close> |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
36 |
|
55821 | 37 |
definition bigo :: "('a \<Rightarrow> 'b::linordered_idom) \<Rightarrow> ('a \<Rightarrow> 'b) set" ("(1O'(_'))") |
38 |
where "O(f:: 'a \<Rightarrow> 'b) = {h. \<exists>c. \<forall>x. abs (h x) \<le> c * abs (f x)}" |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
39 |
|
55821 | 40 |
lemma bigo_pos_const: |
41 |
"(\<exists>c::'a::linordered_idom. \<forall>x. abs (h x) \<le> c * abs (f x)) \<longleftrightarrow> |
|
42 |
(\<exists>c. 0 < c \<and> (\<forall>x. abs (h x) \<le> c * abs (f x)))" |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
43 |
apply auto |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
44 |
apply (case_tac "c = 0") |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
45 |
apply simp |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
46 |
apply (rule_tac x = "1" in exI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
47 |
apply simp |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
48 |
apply (rule_tac x = "abs c" in exI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
49 |
apply auto |
55821 | 50 |
apply (subgoal_tac "c * abs (f x) \<le> abs c * abs (f x)") |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
51 |
apply (erule_tac x = x in allE) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
52 |
apply force |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
53 |
apply (rule mult_right_mono) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
54 |
apply (rule abs_ge_self) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
55 |
apply (rule abs_ge_zero) |
22665 | 56 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
57 |
|
55821 | 58 |
lemma bigo_alt_def: "O(f) = {h. \<exists>c. 0 < c \<and> (\<forall>x. abs (h x) \<le> c * abs (f x))}" |
22665 | 59 |
by (auto simp add: bigo_def bigo_pos_const) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
60 |
|
55821 | 61 |
lemma bigo_elt_subset [intro]: "f \<in> O(g) \<Longrightarrow> O(f) \<le> O(g)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
62 |
apply (auto simp add: bigo_alt_def) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
63 |
apply (rule_tac x = "ca * c" in exI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
64 |
apply (rule conjI) |
56544 | 65 |
apply simp |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
66 |
apply (rule allI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
67 |
apply (drule_tac x = "xa" in spec)+ |
55821 | 68 |
apply (subgoal_tac "ca * abs (f xa) \<le> ca * (c * abs (g xa))") |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
69 |
apply (erule order_trans) |
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset
|
70 |
apply (simp add: ac_simps) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
71 |
apply (rule mult_left_mono, assumption) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
72 |
apply (rule order_less_imp_le, assumption) |
22665 | 73 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
74 |
|
55821 | 75 |
lemma bigo_refl [intro]: "f \<in> O(f)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
76 |
apply(auto simp add: bigo_def) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
77 |
apply(rule_tac x = 1 in exI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
78 |
apply simp |
22665 | 79 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
80 |
|
55821 | 81 |
lemma bigo_zero: "0 \<in> O(g)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
82 |
apply (auto simp add: bigo_def func_zero) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
83 |
apply (rule_tac x = 0 in exI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
84 |
apply auto |
22665 | 85 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
86 |
|
55821 | 87 |
lemma bigo_zero2: "O(\<lambda>x. 0) = {\<lambda>x. 0}" |
88 |
by (auto simp add: bigo_def) |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
89 |
|
55821 | 90 |
lemma bigo_plus_self_subset [intro]: "O(f) + O(f) \<subseteq> O(f)" |
26814
b3e8d5ec721d
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe
parents:
25592
diff
changeset
|
91 |
apply (auto simp add: bigo_alt_def set_plus_def) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
92 |
apply (rule_tac x = "c + ca" in exI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
93 |
apply auto |
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset
|
94 |
apply (simp add: ring_distribs func_plus) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
95 |
apply (rule order_trans) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
96 |
apply (rule abs_triangle_ineq) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
97 |
apply (rule add_mono) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
98 |
apply force |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
99 |
apply force |
55821 | 100 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
101 |
|
47445
69e96e5500df
Set_Algebras: removed syntax \<oplus> and \<otimes>, in favour of plain + and *
krauss
parents:
47108
diff
changeset
|
102 |
lemma bigo_plus_idemp [simp]: "O(f) + O(f) = O(f)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
103 |
apply (rule equalityI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
104 |
apply (rule bigo_plus_self_subset) |
55821 | 105 |
apply (rule set_zero_plus2) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
106 |
apply (rule bigo_zero) |
22665 | 107 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
108 |
|
55821 | 109 |
lemma bigo_plus_subset [intro]: "O(f + g) \<subseteq> O(f) + O(g)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
110 |
apply (rule subsetI) |
26814
b3e8d5ec721d
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe
parents:
25592
diff
changeset
|
111 |
apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus_def) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
112 |
apply (subst bigo_pos_const [symmetric])+ |
55821 | 113 |
apply (rule_tac x = "\<lambda>n. if abs (g n) \<le> (abs (f n)) then x n else 0" in exI) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
114 |
apply (rule conjI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
115 |
apply (rule_tac x = "c + c" in exI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
116 |
apply (clarsimp) |
55821 | 117 |
apply (subgoal_tac "c * abs (f xa + g xa) \<le> (c + c) * abs (f xa)") |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
118 |
apply (erule_tac x = xa in allE) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
119 |
apply (erule order_trans) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
120 |
apply (simp) |
55821 | 121 |
apply (subgoal_tac "c * abs (f xa + g xa) \<le> c * (abs (f xa) + abs (g xa))") |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
122 |
apply (erule order_trans) |
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset
|
123 |
apply (simp add: ring_distribs) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
124 |
apply (rule mult_left_mono) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
125 |
apply (simp add: abs_triangle_ineq) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
126 |
apply (simp add: order_less_le) |
55821 | 127 |
apply (rule_tac x = "\<lambda>n. if (abs (f n)) < abs (g n) then x n else 0" in exI) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
128 |
apply (rule conjI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
129 |
apply (rule_tac x = "c + c" in exI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
130 |
apply auto |
55821 | 131 |
apply (subgoal_tac "c * abs (f xa + g xa) \<le> (c + c) * abs (g xa)") |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
132 |
apply (erule_tac x = xa in allE) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
133 |
apply (erule order_trans) |
55821 | 134 |
apply simp |
135 |
apply (subgoal_tac "c * abs (f xa + g xa) \<le> c * (abs (f xa) + abs (g xa))") |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
136 |
apply (erule order_trans) |
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset
|
137 |
apply (simp add: ring_distribs) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
138 |
apply (rule mult_left_mono) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
139 |
apply (rule abs_triangle_ineq) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
140 |
apply (simp add: order_less_le) |
22665 | 141 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
142 |
|
55821 | 143 |
lemma bigo_plus_subset2 [intro]: "A \<subseteq> O(f) \<Longrightarrow> B \<subseteq> O(f) \<Longrightarrow> A + B \<subseteq> O(f)" |
144 |
apply (subgoal_tac "A + B \<subseteq> O(f) + O(f)") |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
145 |
apply (erule order_trans) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
146 |
apply simp |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
147 |
apply (auto del: subsetI simp del: bigo_plus_idemp) |
22665 | 148 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
149 |
|
55821 | 150 |
lemma bigo_plus_eq: "\<forall>x. 0 \<le> f x \<Longrightarrow> \<forall>x. 0 \<le> g x \<Longrightarrow> O(f + g) = O(f) + O(g)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
151 |
apply (rule equalityI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
152 |
apply (rule bigo_plus_subset) |
26814
b3e8d5ec721d
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe
parents:
25592
diff
changeset
|
153 |
apply (simp add: bigo_alt_def set_plus_def func_plus) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
154 |
apply clarify |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
155 |
apply (rule_tac x = "max c ca" in exI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
156 |
apply (rule conjI) |
55821 | 157 |
apply (subgoal_tac "c \<le> max c ca") |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
158 |
apply (erule order_less_le_trans) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
159 |
apply assumption |
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
54230
diff
changeset
|
160 |
apply (rule max.cobounded1) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
161 |
apply clarify |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
162 |
apply (drule_tac x = "xa" in spec)+ |
55821 | 163 |
apply (subgoal_tac "0 \<le> f xa + g xa") |
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23413
diff
changeset
|
164 |
apply (simp add: ring_distribs) |
55821 | 165 |
apply (subgoal_tac "abs (a xa + b xa) \<le> abs (a xa) + abs (b xa)") |
166 |
apply (subgoal_tac "abs (a xa) + abs (b xa) \<le> max c ca * f xa + max c ca * g xa") |
|
167 |
apply force |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
168 |
apply (rule add_mono) |
55821 | 169 |
apply (subgoal_tac "c * f xa \<le> max c ca * f xa") |
170 |
apply force |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
171 |
apply (rule mult_right_mono) |
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
54230
diff
changeset
|
172 |
apply (rule max.cobounded1) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
173 |
apply assumption |
55821 | 174 |
apply (subgoal_tac "ca * g xa \<le> max c ca * g xa") |
175 |
apply force |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
176 |
apply (rule mult_right_mono) |
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
54230
diff
changeset
|
177 |
apply (rule max.cobounded2) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
178 |
apply assumption |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
179 |
apply (rule abs_triangle_ineq) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
180 |
apply (rule add_nonneg_nonneg) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
181 |
apply assumption+ |
22665 | 182 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
183 |
|
55821 | 184 |
lemma bigo_bounded_alt: "\<forall>x. 0 \<le> f x \<Longrightarrow> \<forall>x. f x \<le> c * g x \<Longrightarrow> f \<in> O(g)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
185 |
apply (auto simp add: bigo_def) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
186 |
apply (rule_tac x = "abs c" in exI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
187 |
apply auto |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
188 |
apply (drule_tac x = x in spec)+ |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
189 |
apply (simp add: abs_mult [symmetric]) |
22665 | 190 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
191 |
|
55821 | 192 |
lemma bigo_bounded: "\<forall>x. 0 \<le> f x \<Longrightarrow> \<forall>x. f x \<le> g x \<Longrightarrow> f \<in> O(g)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
193 |
apply (erule bigo_bounded_alt [of f 1 g]) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
194 |
apply simp |
22665 | 195 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
196 |
|
55821 | 197 |
lemma bigo_bounded2: "\<forall>x. lb x \<le> f x \<Longrightarrow> \<forall>x. f x \<le> lb x + g x \<Longrightarrow> f \<in> lb +o O(g)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
198 |
apply (rule set_minus_imp_plus) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
199 |
apply (rule bigo_bounded) |
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
47445
diff
changeset
|
200 |
apply (auto simp add: fun_Compl_def func_plus) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
201 |
apply (drule_tac x = x in spec)+ |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
202 |
apply force |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
203 |
apply (drule_tac x = x in spec)+ |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
204 |
apply force |
22665 | 205 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
206 |
|
55821 | 207 |
lemma bigo_abs: "(\<lambda>x. abs (f x)) =o O(f)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
208 |
apply (unfold bigo_def) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
209 |
apply auto |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
210 |
apply (rule_tac x = 1 in exI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
211 |
apply auto |
22665 | 212 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
213 |
|
55821 | 214 |
lemma bigo_abs2: "f =o O(\<lambda>x. abs (f x))" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
215 |
apply (unfold bigo_def) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
216 |
apply auto |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
217 |
apply (rule_tac x = 1 in exI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
218 |
apply auto |
22665 | 219 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
220 |
|
55821 | 221 |
lemma bigo_abs3: "O(f) = O(\<lambda>x. abs (f x))" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
222 |
apply (rule equalityI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
223 |
apply (rule bigo_elt_subset) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
224 |
apply (rule bigo_abs2) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
225 |
apply (rule bigo_elt_subset) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
226 |
apply (rule bigo_abs) |
22665 | 227 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
228 |
|
55821 | 229 |
lemma bigo_abs4: "f =o g +o O(h) \<Longrightarrow> (\<lambda>x. abs (f x)) =o (\<lambda>x. abs (g x)) +o O(h)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
230 |
apply (drule set_plus_imp_minus) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
231 |
apply (rule set_minus_imp_plus) |
26814
b3e8d5ec721d
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe
parents:
25592
diff
changeset
|
232 |
apply (subst fun_diff_def) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
233 |
proof - |
55821 | 234 |
assume a: "f - g \<in> O(h)" |
235 |
have "(\<lambda>x. abs (f x) - abs (g x)) =o O(\<lambda>x. abs (abs (f x) - abs (g x)))" |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
236 |
by (rule bigo_abs2) |
55821 | 237 |
also have "\<dots> \<subseteq> O(\<lambda>x. abs (f x - g x))" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
238 |
apply (rule bigo_elt_subset) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
239 |
apply (rule bigo_bounded) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
240 |
apply force |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
241 |
apply (rule allI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
242 |
apply (rule abs_triangle_ineq3) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
243 |
done |
55821 | 244 |
also have "\<dots> \<subseteq> O(f - g)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
245 |
apply (rule bigo_elt_subset) |
26814
b3e8d5ec721d
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe
parents:
25592
diff
changeset
|
246 |
apply (subst fun_diff_def) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
247 |
apply (rule bigo_abs) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
248 |
done |
55821 | 249 |
also from a have "\<dots> \<subseteq> O(h)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
250 |
by (rule bigo_elt_subset) |
55821 | 251 |
finally show "(\<lambda>x. abs (f x) - abs (g x)) \<in> O(h)". |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
252 |
qed |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
253 |
|
55821 | 254 |
lemma bigo_abs5: "f =o O(g) \<Longrightarrow> (\<lambda>x. abs (f x)) =o O(g)" |
22665 | 255 |
by (unfold bigo_def, auto) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
256 |
|
55821 | 257 |
lemma bigo_elt_subset2 [intro]: "f \<in> g +o O(h) \<Longrightarrow> O(f) \<subseteq> O(g) + O(h)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
258 |
proof - |
55821 | 259 |
assume "f \<in> g +o O(h)" |
260 |
also have "\<dots> \<subseteq> O(g) + O(h)" |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
261 |
by (auto del: subsetI) |
55821 | 262 |
also have "\<dots> = O(\<lambda>x. abs (g x)) + O(\<lambda>x. abs (h x))" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
263 |
apply (subst bigo_abs3 [symmetric])+ |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
264 |
apply (rule refl) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
265 |
done |
55821 | 266 |
also have "\<dots> = O((\<lambda>x. abs (g x)) + (\<lambda>x. abs (h x)))" |
267 |
by (rule bigo_plus_eq [symmetric]) auto |
|
268 |
finally have "f \<in> \<dots>" . |
|
269 |
then have "O(f) \<subseteq> \<dots>" |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
270 |
by (elim bigo_elt_subset) |
55821 | 271 |
also have "\<dots> = O(\<lambda>x. abs (g x)) + O(\<lambda>x. abs (h x))" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
272 |
by (rule bigo_plus_eq, auto) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
273 |
finally show ?thesis |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
274 |
by (simp add: bigo_abs3 [symmetric]) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
275 |
qed |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
276 |
|
55821 | 277 |
lemma bigo_mult [intro]: "O(f)*O(g) \<subseteq> O(f * g)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
278 |
apply (rule subsetI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
279 |
apply (subst bigo_def) |
26814
b3e8d5ec721d
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe
parents:
25592
diff
changeset
|
280 |
apply (auto simp add: bigo_alt_def set_times_def func_times) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
281 |
apply (rule_tac x = "c * ca" in exI) |
55821 | 282 |
apply (rule allI) |
283 |
apply (erule_tac x = x in allE)+ |
|
284 |
apply (subgoal_tac "c * ca * abs (f x * g x) = (c * abs (f x)) * (ca * abs (g x))") |
|
285 |
apply (erule ssubst) |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
286 |
apply (subst abs_mult) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
287 |
apply (rule mult_mono) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
288 |
apply assumption+ |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
289 |
apply auto |
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset
|
290 |
apply (simp add: ac_simps abs_mult) |
22665 | 291 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
292 |
|
55821 | 293 |
lemma bigo_mult2 [intro]: "f *o O(g) \<subseteq> O(f * g)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
294 |
apply (auto simp add: bigo_def elt_set_times_def func_times abs_mult) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
295 |
apply (rule_tac x = c in exI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
296 |
apply auto |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
297 |
apply (drule_tac x = x in spec) |
55821 | 298 |
apply (subgoal_tac "abs (f x) * abs (b x) \<le> abs (f x) * (c * abs (g x))") |
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset
|
299 |
apply (force simp add: ac_simps) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
300 |
apply (rule mult_left_mono, assumption) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
301 |
apply (rule abs_ge_zero) |
22665 | 302 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
303 |
|
55821 | 304 |
lemma bigo_mult3: "f \<in> O(h) \<Longrightarrow> g \<in> O(j) \<Longrightarrow> f * g \<in> O(h * j)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
305 |
apply (rule subsetD) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
306 |
apply (rule bigo_mult) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
307 |
apply (erule set_times_intro, assumption) |
22665 | 308 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
309 |
|
55821 | 310 |
lemma bigo_mult4 [intro]: "f \<in> k +o O(h) \<Longrightarrow> g * f \<in> (g * k) +o O(g * h)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
311 |
apply (drule set_plus_imp_minus) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
312 |
apply (rule set_minus_imp_plus) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
313 |
apply (drule bigo_mult3 [where g = g and j = g]) |
29667 | 314 |
apply (auto simp add: algebra_simps) |
22665 | 315 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
316 |
|
41528 | 317 |
lemma bigo_mult5: |
55821 | 318 |
fixes f :: "'a \<Rightarrow> 'b::linordered_field" |
319 |
assumes "\<forall>x. f x \<noteq> 0" |
|
320 |
shows "O(f * g) \<subseteq> f *o O(g)" |
|
41528 | 321 |
proof |
322 |
fix h |
|
55821 | 323 |
assume "h \<in> O(f * g)" |
324 |
then have "(\<lambda>x. 1 / (f x)) * h \<in> (\<lambda>x. 1 / f x) *o O(f * g)" |
|
41528 | 325 |
by auto |
55821 | 326 |
also have "\<dots> \<subseteq> O((\<lambda>x. 1 / f x) * (f * g))" |
41528 | 327 |
by (rule bigo_mult2) |
55821 | 328 |
also have "(\<lambda>x. 1 / f x) * (f * g) = g" |
329 |
apply (simp add: func_times) |
|
41528 | 330 |
apply (rule ext) |
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset
|
331 |
apply (simp add: assms nonzero_divide_eq_eq ac_simps) |
41528 | 332 |
done |
55821 | 333 |
finally have "(\<lambda>x. (1::'b) / f x) * h \<in> O(g)" . |
334 |
then have "f * ((\<lambda>x. (1::'b) / f x) * h) \<in> f *o O(g)" |
|
41528 | 335 |
by auto |
55821 | 336 |
also have "f * ((\<lambda>x. (1::'b) / f x) * h) = h" |
337 |
apply (simp add: func_times) |
|
41528 | 338 |
apply (rule ext) |
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset
|
339 |
apply (simp add: assms nonzero_divide_eq_eq ac_simps) |
41528 | 340 |
done |
55821 | 341 |
finally show "h \<in> f *o O(g)" . |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
342 |
qed |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
343 |
|
55821 | 344 |
lemma bigo_mult6: |
345 |
fixes f :: "'a \<Rightarrow> 'b::linordered_field" |
|
346 |
shows "\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) = f *o O(g)" |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
347 |
apply (rule equalityI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
348 |
apply (erule bigo_mult5) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
349 |
apply (rule bigo_mult2) |
22665 | 350 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
351 |
|
55821 | 352 |
lemma bigo_mult7: |
353 |
fixes f :: "'a \<Rightarrow> 'b::linordered_field" |
|
354 |
shows "\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) \<subseteq> O(f) * O(g)" |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
355 |
apply (subst bigo_mult6) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
356 |
apply assumption |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
357 |
apply (rule set_times_mono3) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
358 |
apply (rule bigo_refl) |
22665 | 359 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
360 |
|
55821 | 361 |
lemma bigo_mult8: |
362 |
fixes f :: "'a \<Rightarrow> 'b::linordered_field" |
|
363 |
shows "\<forall>x. f x \<noteq> 0 \<Longrightarrow> O(f * g) = O(f) * O(g)" |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
364 |
apply (rule equalityI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
365 |
apply (erule bigo_mult7) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
366 |
apply (rule bigo_mult) |
22665 | 367 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
368 |
|
55821 | 369 |
lemma bigo_minus [intro]: "f \<in> O(g) \<Longrightarrow> - f \<in> O(g)" |
26814
b3e8d5ec721d
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe
parents:
25592
diff
changeset
|
370 |
by (auto simp add: bigo_def fun_Compl_def) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
371 |
|
55821 | 372 |
lemma bigo_minus2: "f \<in> g +o O(h) \<Longrightarrow> - f \<in> -g +o O(h)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
373 |
apply (rule set_minus_imp_plus) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
374 |
apply (drule set_plus_imp_minus) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
375 |
apply (drule bigo_minus) |
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
47445
diff
changeset
|
376 |
apply simp |
22665 | 377 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
378 |
|
55821 | 379 |
lemma bigo_minus3: "O(- f) = O(f)" |
41528 | 380 |
by (auto simp add: bigo_def fun_Compl_def) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
381 |
|
55821 | 382 |
lemma bigo_plus_absorb_lemma1: "f \<in> O(g) \<Longrightarrow> f +o O(g) \<subseteq> O(g)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
383 |
proof - |
55821 | 384 |
assume a: "f \<in> O(g)" |
385 |
show "f +o O(g) \<subseteq> O(g)" |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
386 |
proof - |
55821 | 387 |
have "f \<in> O(f)" by auto |
388 |
then have "f +o O(g) \<subseteq> O(f) + O(g)" |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
389 |
by (auto del: subsetI) |
55821 | 390 |
also have "\<dots> \<subseteq> O(g) + O(g)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
391 |
proof - |
55821 | 392 |
from a have "O(f) \<subseteq> O(g)" by (auto del: subsetI) |
56796 | 393 |
then show ?thesis by (auto del: subsetI) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
394 |
qed |
55821 | 395 |
also have "\<dots> \<subseteq> O(g)" by simp |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
396 |
finally show ?thesis . |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
397 |
qed |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
398 |
qed |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
399 |
|
55821 | 400 |
lemma bigo_plus_absorb_lemma2: "f \<in> O(g) \<Longrightarrow> O(g) \<subseteq> f +o O(g)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
401 |
proof - |
55821 | 402 |
assume a: "f \<in> O(g)" |
403 |
show "O(g) \<subseteq> f +o O(g)" |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
404 |
proof - |
55821 | 405 |
from a have "- f \<in> O(g)" |
406 |
by auto |
|
407 |
then have "- f +o O(g) \<subseteq> O(g)" |
|
408 |
by (elim bigo_plus_absorb_lemma1) |
|
409 |
then have "f +o (- f +o O(g)) \<subseteq> f +o O(g)" |
|
410 |
by auto |
|
411 |
also have "f +o (- f +o O(g)) = O(g)" |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
412 |
by (simp add: set_plus_rearranges) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
413 |
finally show ?thesis . |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
414 |
qed |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
415 |
qed |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
416 |
|
55821 | 417 |
lemma bigo_plus_absorb [simp]: "f \<in> O(g) \<Longrightarrow> f +o O(g) = O(g)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
418 |
apply (rule equalityI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
419 |
apply (erule bigo_plus_absorb_lemma1) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
420 |
apply (erule bigo_plus_absorb_lemma2) |
22665 | 421 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
422 |
|
55821 | 423 |
lemma bigo_plus_absorb2 [intro]: "f \<in> O(g) \<Longrightarrow> A \<subseteq> O(g) \<Longrightarrow> f +o A \<subseteq> O(g)" |
424 |
apply (subgoal_tac "f +o A \<subseteq> f +o O(g)") |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
425 |
apply force+ |
22665 | 426 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
427 |
|
55821 | 428 |
lemma bigo_add_commute_imp: "f \<in> g +o O(h) \<Longrightarrow> g \<in> f +o O(h)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
429 |
apply (subst set_minus_plus [symmetric]) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
430 |
apply (subgoal_tac "g - f = - (f - g)") |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
431 |
apply (erule ssubst) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
432 |
apply (rule bigo_minus) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
433 |
apply (subst set_minus_plus) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
434 |
apply assumption |
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset
|
435 |
apply (simp add: ac_simps) |
22665 | 436 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
437 |
|
55821 | 438 |
lemma bigo_add_commute: "f \<in> g +o O(h) \<longleftrightarrow> g \<in> f +o O(h)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
439 |
apply (rule iffI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
440 |
apply (erule bigo_add_commute_imp)+ |
22665 | 441 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
442 |
|
55821 | 443 |
lemma bigo_const1: "(\<lambda>x. c) \<in> O(\<lambda>x. 1)" |
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset
|
444 |
by (auto simp add: bigo_def ac_simps) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
445 |
|
55821 | 446 |
lemma bigo_const2 [intro]: "O(\<lambda>x. c) \<subseteq> O(\<lambda>x. 1)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
447 |
apply (rule bigo_elt_subset) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
448 |
apply (rule bigo_const1) |
22665 | 449 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
450 |
|
55821 | 451 |
lemma bigo_const3: |
452 |
fixes c :: "'a::linordered_field" |
|
453 |
shows "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. 1) \<in> O(\<lambda>x. c)" |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
454 |
apply (simp add: bigo_def) |
55821 | 455 |
apply (rule_tac x = "abs (inverse c)" in exI) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
456 |
apply (simp add: abs_mult [symmetric]) |
22665 | 457 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
458 |
|
55821 | 459 |
lemma bigo_const4: |
460 |
fixes c :: "'a::linordered_field" |
|
461 |
shows "c \<noteq> 0 \<Longrightarrow> O(\<lambda>x. 1) \<subseteq> O(\<lambda>x. c)" |
|
462 |
apply (rule bigo_elt_subset) |
|
463 |
apply (rule bigo_const3) |
|
464 |
apply assumption |
|
465 |
done |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
466 |
|
55821 | 467 |
lemma bigo_const [simp]: |
468 |
fixes c :: "'a::linordered_field" |
|
469 |
shows "c \<noteq> 0 \<Longrightarrow> O(\<lambda>x. c) = O(\<lambda>x. 1)" |
|
470 |
apply (rule equalityI) |
|
471 |
apply (rule bigo_const2) |
|
472 |
apply (rule bigo_const4) |
|
473 |
apply assumption |
|
474 |
done |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
475 |
|
55821 | 476 |
lemma bigo_const_mult1: "(\<lambda>x. c * f x) \<in> O(f)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
477 |
apply (simp add: bigo_def) |
55821 | 478 |
apply (rule_tac x = "abs c" in exI) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
479 |
apply (auto simp add: abs_mult [symmetric]) |
22665 | 480 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
481 |
|
55821 | 482 |
lemma bigo_const_mult2: "O(\<lambda>x. c * f x) \<subseteq> O(f)" |
483 |
apply (rule bigo_elt_subset) |
|
484 |
apply (rule bigo_const_mult1) |
|
485 |
done |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
486 |
|
55821 | 487 |
lemma bigo_const_mult3: |
488 |
fixes c :: "'a::linordered_field" |
|
489 |
shows "c \<noteq> 0 \<Longrightarrow> f \<in> O(\<lambda>x. c * f x)" |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
490 |
apply (simp add: bigo_def) |
55821 | 491 |
apply (rule_tac x = "abs (inverse c)" in exI) |
59867
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
58881
diff
changeset
|
492 |
apply (simp add: abs_mult mult.assoc [symmetric]) |
22665 | 493 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
494 |
|
55821 | 495 |
lemma bigo_const_mult4: |
496 |
fixes c :: "'a::linordered_field" |
|
497 |
shows "c \<noteq> 0 \<Longrightarrow> O(f) \<subseteq> O(\<lambda>x. c * f x)" |
|
498 |
apply (rule bigo_elt_subset) |
|
499 |
apply (rule bigo_const_mult3) |
|
500 |
apply assumption |
|
501 |
done |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
502 |
|
55821 | 503 |
lemma bigo_const_mult [simp]: |
504 |
fixes c :: "'a::linordered_field" |
|
505 |
shows "c \<noteq> 0 \<Longrightarrow> O(\<lambda>x. c * f x) = O(f)" |
|
506 |
apply (rule equalityI) |
|
507 |
apply (rule bigo_const_mult2) |
|
508 |
apply (erule bigo_const_mult4) |
|
509 |
done |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
510 |
|
55821 | 511 |
lemma bigo_const_mult5 [simp]: |
512 |
fixes c :: "'a::linordered_field" |
|
513 |
shows "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. c) *o O(f) = O(f)" |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
514 |
apply (auto del: subsetI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
515 |
apply (rule order_trans) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
516 |
apply (rule bigo_mult2) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
517 |
apply (simp add: func_times) |
41528 | 518 |
apply (auto intro!: simp add: bigo_def elt_set_times_def func_times) |
55821 | 519 |
apply (rule_tac x = "\<lambda>y. inverse c * x y" in exI) |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
520 |
apply (simp add: mult.assoc [symmetric] abs_mult) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
521 |
apply (rule_tac x = "abs (inverse c) * ca" in exI) |
59867
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
58881
diff
changeset
|
522 |
apply auto |
22665 | 523 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
524 |
|
55821 | 525 |
lemma bigo_const_mult6 [intro]: "(\<lambda>x. c) *o O(f) \<subseteq> O(f)" |
41528 | 526 |
apply (auto intro!: simp add: bigo_def elt_set_times_def func_times) |
55821 | 527 |
apply (rule_tac x = "ca * abs c" in exI) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
528 |
apply (rule allI) |
55821 | 529 |
apply (subgoal_tac "ca * abs c * abs (f x) = abs c * (ca * abs (f x))") |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
530 |
apply (erule ssubst) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
531 |
apply (subst abs_mult) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
532 |
apply (rule mult_left_mono) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
533 |
apply (erule spec) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
534 |
apply simp |
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset
|
535 |
apply(simp add: ac_simps) |
22665 | 536 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
537 |
|
55821 | 538 |
lemma bigo_const_mult7 [intro]: "f =o O(g) \<Longrightarrow> (\<lambda>x. c * f x) =o O(g)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
539 |
proof - |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
540 |
assume "f =o O(g)" |
55821 | 541 |
then have "(\<lambda>x. c) * f =o (\<lambda>x. c) *o O(g)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
542 |
by auto |
55821 | 543 |
also have "(\<lambda>x. c) * f = (\<lambda>x. c * f x)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
544 |
by (simp add: func_times) |
55821 | 545 |
also have "(\<lambda>x. c) *o O(g) \<subseteq> O(g)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
546 |
by (auto del: subsetI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
547 |
finally show ?thesis . |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
548 |
qed |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
549 |
|
55821 | 550 |
lemma bigo_compose1: "f =o O(g) \<Longrightarrow> (\<lambda>x. f (k x)) =o O(\<lambda>x. g (k x))" |
551 |
unfolding bigo_def by auto |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
552 |
|
55821 | 553 |
lemma bigo_compose2: "f =o g +o O(h) \<Longrightarrow> |
554 |
(\<lambda>x. f (k x)) =o (\<lambda>x. g (k x)) +o O(\<lambda>x. h(k x))" |
|
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
47445
diff
changeset
|
555 |
apply (simp only: set_minus_plus [symmetric] fun_Compl_def func_plus) |
55821 | 556 |
apply (drule bigo_compose1) |
557 |
apply (simp add: fun_diff_def) |
|
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
47445
diff
changeset
|
558 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
559 |
|
22665 | 560 |
|
60500 | 561 |
subsection \<open>Setsum\<close> |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
562 |
|
55821 | 563 |
lemma bigo_setsum_main: "\<forall>x. \<forall>y \<in> A x. 0 \<le> h x y \<Longrightarrow> |
564 |
\<exists>c. \<forall>x. \<forall>y \<in> A x. abs (f x y) \<le> c * (h x y) \<Longrightarrow> |
|
565 |
(\<lambda>x. \<Sum>y \<in> A x. f x y) =o O(\<lambda>x. \<Sum>y \<in> A x. h x y)" |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
566 |
apply (auto simp add: bigo_def) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
567 |
apply (rule_tac x = "abs c" in exI) |
17199
59c1bfc81d91
moved lemmas that require the HOL-Complex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset
|
568 |
apply (subst abs_of_nonneg) back back |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
569 |
apply (rule setsum_nonneg) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
570 |
apply force |
19279 | 571 |
apply (subst setsum_right_distrib) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
572 |
apply (rule allI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
573 |
apply (rule order_trans) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
574 |
apply (rule setsum_abs) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
575 |
apply (rule setsum_mono) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
576 |
apply (rule order_trans) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
577 |
apply (drule spec)+ |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
578 |
apply (drule bspec)+ |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
579 |
apply assumption+ |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
580 |
apply (drule bspec) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
581 |
apply assumption+ |
55821 | 582 |
apply (rule mult_right_mono) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
583 |
apply (rule abs_ge_self) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
584 |
apply force |
22665 | 585 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
586 |
|
55821 | 587 |
lemma bigo_setsum1: "\<forall>x y. 0 \<le> h x y \<Longrightarrow> |
588 |
\<exists>c. \<forall>x y. abs (f x y) \<le> c * h x y \<Longrightarrow> |
|
589 |
(\<lambda>x. \<Sum>y \<in> A x. f x y) =o O(\<lambda>x. \<Sum>y \<in> A x. h x y)" |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
590 |
apply (rule bigo_setsum_main) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
591 |
apply force |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
592 |
apply clarsimp |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
593 |
apply (rule_tac x = c in exI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
594 |
apply force |
22665 | 595 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
596 |
|
55821 | 597 |
lemma bigo_setsum2: "\<forall>y. 0 \<le> h y \<Longrightarrow> |
598 |
\<exists>c. \<forall>y. abs (f y) \<le> c * (h y) \<Longrightarrow> |
|
599 |
(\<lambda>x. \<Sum>y \<in> A x. f y) =o O(\<lambda>x. \<Sum>y \<in> A x. h y)" |
|
600 |
by (rule bigo_setsum1) auto |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
601 |
|
55821 | 602 |
lemma bigo_setsum3: "f =o O(h) \<Longrightarrow> |
603 |
(\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o O(\<lambda>x. \<Sum>y \<in> A x. abs (l x y * h (k x y)))" |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
604 |
apply (rule bigo_setsum1) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
605 |
apply (rule allI)+ |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
606 |
apply (rule abs_ge_zero) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
607 |
apply (unfold bigo_def) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
608 |
apply auto |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
609 |
apply (rule_tac x = c in exI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
610 |
apply (rule allI)+ |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
611 |
apply (subst abs_mult)+ |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
612 |
apply (subst mult.left_commute) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
613 |
apply (rule mult_left_mono) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
614 |
apply (erule spec) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
615 |
apply (rule abs_ge_zero) |
22665 | 616 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
617 |
|
55821 | 618 |
lemma bigo_setsum4: "f =o g +o O(h) \<Longrightarrow> |
619 |
(\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o |
|
620 |
(\<lambda>x. \<Sum>y \<in> A x. l x y * g (k x y)) +o |
|
621 |
O(\<lambda>x. \<Sum>y \<in> A x. abs (l x y * h (k x y)))" |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
622 |
apply (rule set_minus_imp_plus) |
26814
b3e8d5ec721d
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe
parents:
25592
diff
changeset
|
623 |
apply (subst fun_diff_def) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
624 |
apply (subst setsum_subtractf [symmetric]) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
625 |
apply (subst right_diff_distrib [symmetric]) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
626 |
apply (rule bigo_setsum3) |
26814
b3e8d5ec721d
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe
parents:
25592
diff
changeset
|
627 |
apply (subst fun_diff_def [symmetric]) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
628 |
apply (erule set_plus_imp_minus) |
22665 | 629 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
630 |
|
55821 | 631 |
lemma bigo_setsum5: "f =o O(h) \<Longrightarrow> \<forall>x y. 0 \<le> l x y \<Longrightarrow> |
632 |
\<forall>x. 0 \<le> h x \<Longrightarrow> |
|
633 |
(\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o |
|
634 |
O(\<lambda>x. \<Sum>y \<in> A x. l x y * h (k x y))" |
|
635 |
apply (subgoal_tac "(\<lambda>x. \<Sum>y \<in> A x. l x y * h (k x y)) = |
|
636 |
(\<lambda>x. \<Sum>y \<in> A x. abs (l x y * h (k x y)))") |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
637 |
apply (erule ssubst) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
638 |
apply (erule bigo_setsum3) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
639 |
apply (rule ext) |
57418 | 640 |
apply (rule setsum.cong) |
641 |
apply (rule refl) |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
642 |
apply (subst abs_of_nonneg) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
643 |
apply auto |
22665 | 644 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
645 |
|
55821 | 646 |
lemma bigo_setsum6: "f =o g +o O(h) \<Longrightarrow> \<forall>x y. 0 \<le> l x y \<Longrightarrow> |
647 |
\<forall>x. 0 \<le> h x \<Longrightarrow> |
|
648 |
(\<lambda>x. \<Sum>y \<in> A x. l x y * f (k x y)) =o |
|
649 |
(\<lambda>x. \<Sum>y \<in> A x. l x y * g (k x y)) +o |
|
650 |
O(\<lambda>x. \<Sum>y \<in> A x. l x y * h (k x y))" |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
651 |
apply (rule set_minus_imp_plus) |
26814
b3e8d5ec721d
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe
parents:
25592
diff
changeset
|
652 |
apply (subst fun_diff_def) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
653 |
apply (subst setsum_subtractf [symmetric]) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
654 |
apply (subst right_diff_distrib [symmetric]) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
655 |
apply (rule bigo_setsum5) |
26814
b3e8d5ec721d
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe
parents:
25592
diff
changeset
|
656 |
apply (subst fun_diff_def [symmetric]) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
657 |
apply (drule set_plus_imp_minus) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
658 |
apply auto |
22665 | 659 |
done |
660 |
||
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
661 |
|
60500 | 662 |
subsection \<open>Misc useful stuff\<close> |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
663 |
|
55821 | 664 |
lemma bigo_useful_intro: "A \<subseteq> O(f) \<Longrightarrow> B \<subseteq> O(f) \<Longrightarrow> A + B \<subseteq> O(f)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
665 |
apply (subst bigo_plus_idemp [symmetric]) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
666 |
apply (rule set_plus_mono2) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
667 |
apply assumption+ |
22665 | 668 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
669 |
|
55821 | 670 |
lemma bigo_useful_add: "f =o O(h) \<Longrightarrow> g =o O(h) \<Longrightarrow> f + g =o O(h)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
671 |
apply (subst bigo_plus_idemp [symmetric]) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
672 |
apply (rule set_plus_intro) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
673 |
apply assumption+ |
22665 | 674 |
done |
55821 | 675 |
|
676 |
lemma bigo_useful_const_mult: |
|
677 |
fixes c :: "'a::linordered_field" |
|
678 |
shows "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. c) * f =o O(h) \<Longrightarrow> f =o O(h)" |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
679 |
apply (rule subsetD) |
55821 | 680 |
apply (subgoal_tac "(\<lambda>x. 1 / c) *o O(h) \<subseteq> O(h)") |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
681 |
apply assumption |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
682 |
apply (rule bigo_const_mult6) |
55821 | 683 |
apply (subgoal_tac "f = (\<lambda>x. 1 / c) * ((\<lambda>x. c) * f)") |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
684 |
apply (erule ssubst) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
685 |
apply (erule set_times_intro2) |
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23373
diff
changeset
|
686 |
apply (simp add: func_times) |
22665 | 687 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
688 |
|
55821 | 689 |
lemma bigo_fix: "(\<lambda>x::nat. f (x + 1)) =o O(\<lambda>x. h (x + 1)) \<Longrightarrow> f 0 = 0 \<Longrightarrow> f =o O(h)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
690 |
apply (simp add: bigo_alt_def) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
691 |
apply auto |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
692 |
apply (rule_tac x = c in exI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
693 |
apply auto |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
694 |
apply (case_tac "x = 0") |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
695 |
apply simp |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
696 |
apply (subgoal_tac "x = Suc (x - 1)") |
17199
59c1bfc81d91
moved lemmas that require the HOL-Complex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset
|
697 |
apply (erule ssubst) back |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
698 |
apply (erule spec) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
699 |
apply simp |
22665 | 700 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
701 |
|
55821 | 702 |
lemma bigo_fix2: |
703 |
"(\<lambda>x. f ((x::nat) + 1)) =o (\<lambda>x. g(x + 1)) +o O(\<lambda>x. h(x + 1)) \<Longrightarrow> |
|
704 |
f 0 = g 0 \<Longrightarrow> f =o g +o O(h)" |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
705 |
apply (rule set_minus_imp_plus) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
706 |
apply (rule bigo_fix) |
26814
b3e8d5ec721d
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe
parents:
25592
diff
changeset
|
707 |
apply (subst fun_diff_def) |
b3e8d5ec721d
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe
parents:
25592
diff
changeset
|
708 |
apply (subst fun_diff_def [symmetric]) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
709 |
apply (rule set_plus_imp_minus) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
710 |
apply simp |
26814
b3e8d5ec721d
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe
parents:
25592
diff
changeset
|
711 |
apply (simp add: fun_diff_def) |
22665 | 712 |
done |
713 |
||
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
714 |
|
60500 | 715 |
subsection \<open>Less than or equal to\<close> |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
716 |
|
55821 | 717 |
definition lesso :: "('a \<Rightarrow> 'b::linordered_idom) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" (infixl "<o" 70) |
718 |
where "f <o g = (\<lambda>x. max (f x - g x) 0)" |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
719 |
|
55821 | 720 |
lemma bigo_lesseq1: "f =o O(h) \<Longrightarrow> \<forall>x. abs (g x) \<le> abs (f x) \<Longrightarrow> g =o O(h)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
721 |
apply (unfold bigo_def) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
722 |
apply clarsimp |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
723 |
apply (rule_tac x = c in exI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
724 |
apply (rule allI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
725 |
apply (rule order_trans) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
726 |
apply (erule spec)+ |
22665 | 727 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
728 |
|
55821 | 729 |
lemma bigo_lesseq2: "f =o O(h) \<Longrightarrow> \<forall>x. abs (g x) \<le> f x \<Longrightarrow> g =o O(h)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
730 |
apply (erule bigo_lesseq1) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
731 |
apply (rule allI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
732 |
apply (drule_tac x = x in spec) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
733 |
apply (rule order_trans) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
734 |
apply assumption |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
735 |
apply (rule abs_ge_self) |
22665 | 736 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
737 |
|
55821 | 738 |
lemma bigo_lesseq3: "f =o O(h) \<Longrightarrow> \<forall>x. 0 \<le> g x \<Longrightarrow> \<forall>x. g x \<le> f x \<Longrightarrow> g =o O(h)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
739 |
apply (erule bigo_lesseq2) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
740 |
apply (rule allI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
741 |
apply (subst abs_of_nonneg) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
742 |
apply (erule spec)+ |
22665 | 743 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
744 |
|
55821 | 745 |
lemma bigo_lesseq4: "f =o O(h) \<Longrightarrow> |
746 |
\<forall>x. 0 \<le> g x \<Longrightarrow> \<forall>x. g x \<le> abs (f x) \<Longrightarrow> g =o O(h)" |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
747 |
apply (erule bigo_lesseq1) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
748 |
apply (rule allI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
749 |
apply (subst abs_of_nonneg) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
750 |
apply (erule spec)+ |
22665 | 751 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
752 |
|
55821 | 753 |
lemma bigo_lesso1: "\<forall>x. f x \<le> g x \<Longrightarrow> f <o g =o O(h)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
754 |
apply (unfold lesso_def) |
55821 | 755 |
apply (subgoal_tac "(\<lambda>x. max (f x - g x) 0) = 0") |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
756 |
apply (erule ssubst) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
757 |
apply (rule bigo_zero) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
758 |
apply (unfold func_zero) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
759 |
apply (rule ext) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
760 |
apply (simp split: split_max) |
22665 | 761 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
762 |
|
55821 | 763 |
lemma bigo_lesso2: "f =o g +o O(h) \<Longrightarrow> |
764 |
\<forall>x. 0 \<le> k x \<Longrightarrow> \<forall>x. k x \<le> f x \<Longrightarrow> k <o g =o O(h)" |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
765 |
apply (unfold lesso_def) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
766 |
apply (rule bigo_lesseq4) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
767 |
apply (erule set_plus_imp_minus) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
768 |
apply (rule allI) |
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
54230
diff
changeset
|
769 |
apply (rule max.cobounded2) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
770 |
apply (rule allI) |
26814
b3e8d5ec721d
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe
parents:
25592
diff
changeset
|
771 |
apply (subst fun_diff_def) |
55821 | 772 |
apply (case_tac "0 \<le> k x - g x") |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
773 |
apply simp |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
774 |
apply (subst abs_of_nonneg) |
17199
59c1bfc81d91
moved lemmas that require the HOL-Complex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset
|
775 |
apply (drule_tac x = x in spec) back |
29667 | 776 |
apply (simp add: algebra_simps) |
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
47445
diff
changeset
|
777 |
apply (subst diff_conv_add_uminus)+ |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
778 |
apply (rule add_right_mono) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
779 |
apply (erule spec) |
55821 | 780 |
apply (rule order_trans) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
781 |
prefer 2 |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
782 |
apply (rule abs_ge_zero) |
29667 | 783 |
apply (simp add: algebra_simps) |
22665 | 784 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
785 |
|
55821 | 786 |
lemma bigo_lesso3: "f =o g +o O(h) \<Longrightarrow> |
787 |
\<forall>x. 0 \<le> k x \<Longrightarrow> \<forall>x. g x \<le> k x \<Longrightarrow> f <o k =o O(h)" |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
788 |
apply (unfold lesso_def) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
789 |
apply (rule bigo_lesseq4) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
790 |
apply (erule set_plus_imp_minus) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
791 |
apply (rule allI) |
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
54230
diff
changeset
|
792 |
apply (rule max.cobounded2) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
793 |
apply (rule allI) |
26814
b3e8d5ec721d
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe
parents:
25592
diff
changeset
|
794 |
apply (subst fun_diff_def) |
55821 | 795 |
apply (case_tac "0 \<le> f x - k x") |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
796 |
apply simp |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
797 |
apply (subst abs_of_nonneg) |
17199
59c1bfc81d91
moved lemmas that require the HOL-Complex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset
|
798 |
apply (drule_tac x = x in spec) back |
29667 | 799 |
apply (simp add: algebra_simps) |
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
47445
diff
changeset
|
800 |
apply (subst diff_conv_add_uminus)+ |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
801 |
apply (rule add_left_mono) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
802 |
apply (rule le_imp_neg_le) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
803 |
apply (erule spec) |
55821 | 804 |
apply (rule order_trans) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
805 |
prefer 2 |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
806 |
apply (rule abs_ge_zero) |
29667 | 807 |
apply (simp add: algebra_simps) |
22665 | 808 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
809 |
|
55821 | 810 |
lemma bigo_lesso4: |
811 |
fixes k :: "'a \<Rightarrow> 'b::linordered_field" |
|
812 |
shows "f <o g =o O(k) \<Longrightarrow> g =o h +o O(k) \<Longrightarrow> f <o h =o O(k)" |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
813 |
apply (unfold lesso_def) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
814 |
apply (drule set_plus_imp_minus) |
17199
59c1bfc81d91
moved lemmas that require the HOL-Complex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset
|
815 |
apply (drule bigo_abs5) back |
26814
b3e8d5ec721d
Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with
berghofe
parents:
25592
diff
changeset
|
816 |
apply (simp add: fun_diff_def) |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
817 |
apply (drule bigo_useful_add) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
818 |
apply assumption |
17199
59c1bfc81d91
moved lemmas that require the HOL-Complex logic image to Complex/ex/BigO_Complex.thy;
wenzelm
parents:
16961
diff
changeset
|
819 |
apply (erule bigo_lesseq2) back |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
820 |
apply (rule allI) |
55821 | 821 |
apply (auto simp add: func_plus fun_diff_def algebra_simps split: split_max abs_split) |
22665 | 822 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
823 |
|
55821 | 824 |
lemma bigo_lesso5: "f <o g =o O(h) \<Longrightarrow> \<exists>C. \<forall>x. f x \<le> g x + C * abs (h x)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
825 |
apply (simp only: lesso_def bigo_alt_def) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
826 |
apply clarsimp |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
827 |
apply (rule_tac x = c in exI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
828 |
apply (rule allI) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
829 |
apply (drule_tac x = x in spec) |
55821 | 830 |
apply (subgoal_tac "abs (max (f x - g x) 0) = max (f x - g x) 0") |
831 |
apply (clarsimp simp add: algebra_simps) |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
832 |
apply (rule abs_of_nonneg) |
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
54230
diff
changeset
|
833 |
apply (rule max.cobounded2) |
22665 | 834 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
835 |
|
55821 | 836 |
lemma lesso_add: "f <o g =o O(h) \<Longrightarrow> k <o l =o O(h) \<Longrightarrow> (f + k) <o (g + l) =o O(h)" |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
837 |
apply (unfold lesso_def) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
838 |
apply (rule bigo_lesseq3) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
839 |
apply (erule bigo_useful_add) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
840 |
apply assumption |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
841 |
apply (force split: split_max) |
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
842 |
apply (auto split: split_max simp add: func_plus) |
22665 | 843 |
done |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
844 |
|
55821 | 845 |
lemma bigo_LIMSEQ1: "f =o O(g) \<Longrightarrow> g ----> 0 \<Longrightarrow> f ----> (0::real)" |
31337 | 846 |
apply (simp add: LIMSEQ_iff bigo_alt_def) |
29786 | 847 |
apply clarify |
848 |
apply (drule_tac x = "r / c" in spec) |
|
849 |
apply (drule mp) |
|
56541 | 850 |
apply simp |
29786 | 851 |
apply clarify |
852 |
apply (rule_tac x = no in exI) |
|
853 |
apply (rule allI) |
|
854 |
apply (drule_tac x = n in spec)+ |
|
855 |
apply (rule impI) |
|
856 |
apply (drule mp) |
|
857 |
apply assumption |
|
858 |
apply (rule order_le_less_trans) |
|
859 |
apply assumption |
|
860 |
apply (rule order_less_le_trans) |
|
55821 | 861 |
apply (subgoal_tac "c * abs (g n) < c * (r / c)") |
29786 | 862 |
apply assumption |
863 |
apply (erule mult_strict_left_mono) |
|
864 |
apply assumption |
|
865 |
apply simp |
|
55821 | 866 |
done |
29786 | 867 |
|
55821 | 868 |
lemma bigo_LIMSEQ2: "f =o g +o O(h) \<Longrightarrow> h ----> 0 \<Longrightarrow> f ----> a \<Longrightarrow> g ----> (a::real)" |
29786 | 869 |
apply (drule set_plus_imp_minus) |
870 |
apply (drule bigo_LIMSEQ1) |
|
871 |
apply assumption |
|
872 |
apply (simp only: fun_diff_def) |
|
60142 | 873 |
apply (erule Lim_transform2) |
29786 | 874 |
apply assumption |
55821 | 875 |
done |
29786 | 876 |
|
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
diff
changeset
|
877 |
end |