8 header {* Metis Example Featuring the Big O Notation *} |
8 header {* Metis Example Featuring the Big O Notation *} |
9 |
9 |
10 theory Big_O |
10 theory Big_O |
11 imports |
11 imports |
12 "~~/src/HOL/Decision_Procs/Dense_Linear_Order" |
12 "~~/src/HOL/Decision_Procs/Dense_Linear_Order" |
13 Main |
|
14 "~~/src/HOL/Library/Function_Algebras" |
13 "~~/src/HOL/Library/Function_Algebras" |
15 "~~/src/HOL/Library/Set_Algebras" |
14 "~~/src/HOL/Library/Set_Algebras" |
16 begin |
15 begin |
17 |
16 |
18 declare [[metis_new_skolemizer]] |
|
19 |
|
20 subsection {* Definitions *} |
17 subsection {* Definitions *} |
21 |
18 |
22 definition bigo :: "('a => 'b::{linordered_idom,number_ring}) => ('a => 'b) set" ("(1O'(_'))") where |
19 definition bigo :: "('a => 'b\<Colon>{linordered_idom,number_ring}) => ('a => 'b) set" ("(1O'(_'))") where |
23 "O(f::('a => 'b)) == {h. EX c. ALL x. abs (h x) <= c * abs (f x)}" |
20 "O(f\<Colon>('a => 'b)) == {h. \<exists>c. \<forall>x. abs (h x) <= c * abs (f x)}" |
24 |
21 |
25 declare [[ sledgehammer_problem_prefix = "BigO__bigo_pos_const" ]] |
22 lemma bigo_pos_const: |
26 lemma bigo_pos_const: "(EX (c::'a::linordered_idom). |
23 "(\<exists>(c\<Colon>'a\<Colon>linordered_idom). |
27 ALL x. (abs (h x)) <= (c * (abs (f x)))) |
24 \<forall>x. (abs (h x)) <= (c * (abs (f x)))) |
28 = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))" |
25 = (\<exists>c. 0 < c & (\<forall>x. (abs(h x)) <= (c * (abs (f x)))))" |
29 apply auto |
26 by (metis (hide_lams, no_types) abs_ge_zero |
30 apply (case_tac "c = 0", simp) |
27 comm_semiring_1_class.normalizing_semiring_rules(7) mult.comm_neutral |
31 apply (rule_tac x = "1" in exI, simp) |
28 mult_nonpos_nonneg not_leE order_trans zero_less_one) |
32 apply (rule_tac x = "abs c" in exI, auto) |
|
33 apply (metis abs_ge_zero abs_of_nonneg Orderings.xt1(6) abs_mult) |
|
34 done |
|
35 |
29 |
36 (*** Now various verions with an increasing shrink factor ***) |
30 (*** Now various verions with an increasing shrink factor ***) |
37 |
31 |
38 sledgehammer_params [isar_proof, isar_shrink_factor = 1] |
32 sledgehammer_params [isar_proof, isar_shrink_factor = 1] |
39 |
33 |
40 lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom). |
34 lemma |
41 ALL x. (abs (h x)) <= (c * (abs (f x)))) |
35 "(\<exists>(c\<Colon>'a\<Colon>linordered_idom). |
42 = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))" |
36 \<forall>x. (abs (h x)) <= (c * (abs (f x)))) |
|
37 = (\<exists>c. 0 < c & (\<forall>x. (abs(h x)) <= (c * (abs (f x)))))" |
43 apply auto |
38 apply auto |
44 apply (case_tac "c = 0", simp) |
39 apply (case_tac "c = 0", simp) |
45 apply (rule_tac x = "1" in exI, simp) |
40 apply (rule_tac x = "1" in exI, simp) |
46 apply (rule_tac x = "abs c" in exI, auto) |
41 apply (rule_tac x = "abs c" in exI, auto) |
47 proof - |
42 proof - |
125 thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis abs_mult) |
123 thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis abs_mult) |
126 qed |
124 qed |
127 |
125 |
128 sledgehammer_params [isar_proof, isar_shrink_factor = 1] |
126 sledgehammer_params [isar_proof, isar_shrink_factor = 1] |
129 |
127 |
130 lemma bigo_alt_def: "O(f) = |
128 lemma bigo_alt_def: "O(f) = {h. \<exists>c. (0 < c & (\<forall>x. abs (h x) <= c * abs (f x)))}" |
131 {h. EX c. (0 < c & (ALL x. abs (h x) <= c * abs (f x)))}" |
|
132 by (auto simp add: bigo_def bigo_pos_const) |
129 by (auto simp add: bigo_def bigo_pos_const) |
133 |
130 |
134 declare [[ sledgehammer_problem_prefix = "BigO__bigo_elt_subset" ]] |
131 lemma bigo_elt_subset [intro]: "f : O(g) \<Longrightarrow> O(f) <= O(g)" |
135 lemma bigo_elt_subset [intro]: "f : O(g) ==> O(f) <= O(g)" |
132 apply (auto simp add: bigo_alt_def) |
136 apply (auto simp add: bigo_alt_def) |
133 apply (rule_tac x = "ca * c" in exI) |
137 apply (rule_tac x = "ca * c" in exI) |
134 apply (rule conjI) |
138 apply (rule conjI) |
135 apply (rule mult_pos_pos) |
139 apply (rule mult_pos_pos) |
|
140 apply (assumption)+ |
136 apply (assumption)+ |
141 (*sledgehammer*) |
137 (* sledgehammer *) |
142 apply (rule allI) |
138 apply (rule allI) |
143 apply (drule_tac x = "xa" in spec)+ |
139 apply (drule_tac x = "xa" in spec)+ |
144 apply (subgoal_tac "ca * abs(f xa) <= ca * (c * abs(g xa))") |
140 apply (subgoal_tac "ca * abs (f xa) <= ca * (c * abs (g xa))") |
145 apply (erule order_trans) |
141 apply (metis comm_semiring_1_class.normalizing_semiring_rules(19) |
146 apply (simp add: mult_ac) |
142 comm_semiring_1_class.normalizing_semiring_rules(7) order_trans) |
147 apply (rule mult_left_mono, assumption) |
143 by (metis mult_le_cancel_left_pos) |
148 apply (rule order_less_imp_le, assumption) |
144 |
149 done |
|
150 |
|
151 |
|
152 declare [[ sledgehammer_problem_prefix = "BigO__bigo_refl" ]] |
|
153 lemma bigo_refl [intro]: "f : O(f)" |
145 lemma bigo_refl [intro]: "f : O(f)" |
154 apply (auto simp add: bigo_def) |
146 apply (auto simp add: bigo_def) |
155 by (metis mult_1 order_refl) |
147 by (metis mult_1 order_refl) |
156 |
148 |
157 declare [[ sledgehammer_problem_prefix = "BigO__bigo_zero" ]] |
|
158 lemma bigo_zero: "0 : O(g)" |
149 lemma bigo_zero: "0 : O(g)" |
159 apply (auto simp add: bigo_def func_zero) |
150 apply (auto simp add: bigo_def func_zero) |
160 by (metis mult_zero_left order_refl) |
151 by (metis mult_zero_left order_refl) |
161 |
152 |
162 lemma bigo_zero2: "O(%x.0) = {%x.0}" |
153 lemma bigo_zero2: "O(\<lambda>x. 0) = {\<lambda>x. 0}" |
163 by (auto simp add: bigo_def) |
154 by (auto simp add: bigo_def) |
164 |
155 |
165 lemma bigo_plus_self_subset [intro]: |
156 lemma bigo_plus_self_subset [intro]: |
166 "O(f) \<oplus> O(f) <= O(f)" |
157 "O(f) \<oplus> O(f) <= O(f)" |
167 apply (auto simp add: bigo_alt_def set_plus_def) |
158 apply (auto simp add: bigo_alt_def set_plus_def) |
168 apply (rule_tac x = "c + ca" in exI) |
159 apply (rule_tac x = "c + ca" in exI) |
|
160 apply auto |
|
161 apply (simp add: ring_distribs func_plus) |
|
162 by (metis order_trans abs_triangle_ineq add_mono) |
|
163 |
|
164 lemma bigo_plus_idemp [simp]: "O(f) \<oplus> O(f) = O(f)" |
|
165 by (metis bigo_plus_self_subset bigo_zero set_eq_subset set_zero_plus2) |
|
166 |
|
167 lemma bigo_plus_subset [intro]: "O(f + g) <= O(f) \<oplus> O(g)" |
|
168 apply (rule subsetI) |
|
169 apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus_def) |
|
170 apply (subst bigo_pos_const [symmetric])+ |
|
171 apply (rule_tac x = "\<lambda>n. if abs (g n) <= (abs (f n)) then x n else 0" in exI) |
|
172 apply (rule conjI) |
|
173 apply (rule_tac x = "c + c" in exI) |
|
174 apply clarsimp |
|
175 apply auto |
|
176 apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (f xa)") |
|
177 apply (metis mult_2 order_trans) |
|
178 apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))") |
|
179 apply (erule order_trans) |
|
180 apply (simp add: ring_distribs) |
|
181 apply (rule mult_left_mono) |
|
182 apply (simp add: abs_triangle_ineq) |
|
183 apply (simp add: order_less_le) |
|
184 apply (rule mult_nonneg_nonneg) |
169 apply auto |
185 apply auto |
170 apply (simp add: ring_distribs func_plus) |
186 apply (rule_tac x = "\<lambda>n. if (abs (f n)) < abs (g n) then x n else 0" in exI) |
171 apply (blast intro:order_trans abs_triangle_ineq add_mono elim:) |
187 apply (rule conjI) |
172 done |
188 apply (rule_tac x = "c + c" in exI) |
173 |
189 apply auto |
174 lemma bigo_plus_idemp [simp]: "O(f) \<oplus> O(f) = O(f)" |
190 apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (g xa)") |
175 apply (rule equalityI) |
191 apply (metis order_trans semiring_mult_2) |
176 apply (rule bigo_plus_self_subset) |
192 apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))") |
177 apply (rule set_zero_plus2) |
|
178 apply (rule bigo_zero) |
|
179 done |
|
180 |
|
181 lemma bigo_plus_subset [intro]: "O(f + g) <= O(f) \<oplus> O(g)" |
|
182 apply (rule subsetI) |
|
183 apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus_def) |
|
184 apply (subst bigo_pos_const [symmetric])+ |
|
185 apply (rule_tac x = |
|
186 "%n. if abs (g n) <= (abs (f n)) then x n else 0" in exI) |
|
187 apply (rule conjI) |
|
188 apply (rule_tac x = "c + c" in exI) |
|
189 apply (clarsimp) |
|
190 apply (auto) |
|
191 apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (f xa)") |
|
192 apply (erule_tac x = xa in allE) |
|
193 apply (erule order_trans) |
|
194 apply (simp) |
|
195 apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))") |
|
196 apply (erule order_trans) |
193 apply (erule order_trans) |
197 apply (simp add: ring_distribs) |
194 apply (simp add: ring_distribs) |
198 apply (rule mult_left_mono) |
195 apply (metis abs_triangle_ineq mult_le_cancel_left_pos) |
199 apply (simp add: abs_triangle_ineq) |
196 by (metis abs_ge_zero abs_of_pos zero_le_mult_iff) |
200 apply (simp add: order_less_le) |
197 |
201 apply (rule mult_nonneg_nonneg) |
198 lemma bigo_plus_subset2 [intro]: "A <= O(f) \<Longrightarrow> B <= O(f) \<Longrightarrow> A \<oplus> B <= O(f)" |
202 apply auto |
199 by (metis bigo_plus_idemp set_plus_mono2) |
203 apply (rule_tac x = "%n. if (abs (f n)) < abs (g n) then x n else 0" |
200 |
204 in exI) |
201 lemma bigo_plus_eq: "\<forall>x. 0 <= f x \<Longrightarrow> \<forall>x. 0 <= g x \<Longrightarrow> O(f + g) = O(f) \<oplus> O(g)" |
205 apply (rule conjI) |
202 apply (rule equalityI) |
206 apply (rule_tac x = "c + c" in exI) |
203 apply (rule bigo_plus_subset) |
207 apply auto |
204 apply (simp add: bigo_alt_def set_plus_def func_plus) |
208 apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (g xa)") |
205 apply clarify |
209 apply (erule_tac x = xa in allE) |
206 (* sledgehammer *) |
210 apply (erule order_trans) |
207 apply (rule_tac x = "max c ca" in exI) |
211 apply (simp) |
208 apply (rule conjI) |
212 apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))") |
209 apply (metis less_max_iff_disj) |
213 apply (erule order_trans) |
210 apply clarify |
214 apply (simp add: ring_distribs) |
211 apply (drule_tac x = "xa" in spec)+ |
215 apply (rule mult_left_mono) |
212 apply (subgoal_tac "0 <= f xa + g xa") |
216 apply (rule abs_triangle_ineq) |
213 apply (simp add: ring_distribs) |
217 apply (simp add: order_less_le) |
214 apply (subgoal_tac "abs (a xa + b xa) <= abs (a xa) + abs (b xa)") |
218 apply (metis abs_not_less_zero even_less_0_iff less_not_permute linorder_not_less mult_less_0_iff) |
215 apply (subgoal_tac "abs (a xa) + abs (b xa) <= |
219 done |
216 max c ca * f xa + max c ca * g xa") |
220 |
217 apply (metis order_trans) |
221 lemma bigo_plus_subset2 [intro]: "A <= O(f) ==> B <= O(f) ==> A \<oplus> B <= O(f)" |
|
222 apply (subgoal_tac "A \<oplus> B <= O(f) \<oplus> O(f)") |
|
223 apply (erule order_trans) |
|
224 apply simp |
|
225 apply (auto del: subsetI simp del: bigo_plus_idemp) |
|
226 done |
|
227 |
|
228 declare [[ sledgehammer_problem_prefix = "BigO__bigo_plus_eq" ]] |
|
229 lemma bigo_plus_eq: "ALL x. 0 <= f x ==> ALL x. 0 <= g x ==> |
|
230 O(f + g) = O(f) \<oplus> O(g)" |
|
231 apply (rule equalityI) |
|
232 apply (rule bigo_plus_subset) |
|
233 apply (simp add: bigo_alt_def set_plus_def func_plus) |
|
234 apply clarify |
|
235 (*sledgehammer*) |
|
236 apply (rule_tac x = "max c ca" in exI) |
|
237 apply (rule conjI) |
|
238 apply (metis Orderings.less_max_iff_disj) |
|
239 apply clarify |
|
240 apply (drule_tac x = "xa" in spec)+ |
|
241 apply (subgoal_tac "0 <= f xa + g xa") |
|
242 apply (simp add: ring_distribs) |
|
243 apply (subgoal_tac "abs(a xa + b xa) <= abs(a xa) + abs(b xa)") |
|
244 apply (subgoal_tac "abs(a xa) + abs(b xa) <= |
|
245 max c ca * f xa + max c ca * g xa") |
|
246 apply (blast intro: order_trans) |
|
247 defer 1 |
218 defer 1 |
248 apply (rule abs_triangle_ineq) |
219 apply (metis abs_triangle_ineq) |
249 apply (metis add_nonneg_nonneg) |
220 apply (metis add_nonneg_nonneg) |
250 apply (rule add_mono) |
221 apply (rule add_mono) |
251 using [[ sledgehammer_problem_prefix = "BigO__bigo_plus_eq_simpler" ]] |
222 apply (metis le_maxI2 linorder_linear min_max.sup_absorb1 mult_right_mono xt1(6)) |
252 apply (metis le_maxI2 linorder_linear min_max.sup_absorb1 mult_right_mono xt1(6)) |
223 by (metis le_maxI2 linorder_not_le mult_le_cancel_right order_trans) |
253 apply (metis le_maxI2 linorder_not_le mult_le_cancel_right order_trans) |
224 |
254 done |
225 lemma bigo_bounded_alt: "\<forall>x. 0 <= f x \<Longrightarrow> \<forall>x. f x <= c * g x \<Longrightarrow> f : O(g)" |
255 |
226 apply (auto simp add: bigo_def) |
256 declare [[ sledgehammer_problem_prefix = "BigO__bigo_bounded_alt" ]] |
|
257 lemma bigo_bounded_alt: "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> |
|
258 f : O(g)" |
|
259 apply (auto simp add: bigo_def) |
|
260 (* Version 1: one-line proof *) |
227 (* Version 1: one-line proof *) |
261 apply (metis abs_le_D1 linorder_class.not_less order_less_le Orderings.xt1(12) abs_mult) |
228 by (metis abs_le_D1 linorder_class.not_less order_less_le Orderings.xt1(12) abs_mult) |
262 done |
229 |
263 |
230 lemma "\<forall>x. 0 <= f x \<Longrightarrow> \<forall>x. f x <= c * g x \<Longrightarrow> f : O(g)" |
264 lemma (*bigo_bounded_alt:*) "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> |
|
265 f : O(g)" |
|
266 apply (auto simp add: bigo_def) |
231 apply (auto simp add: bigo_def) |
267 (* Version 2: structured proof *) |
232 (* Version 2: structured proof *) |
268 proof - |
233 proof - |
269 assume "\<forall>x. f x \<le> c * g x" |
234 assume "\<forall>x. f x \<le> c * g x" |
270 thus "\<exists>c. \<forall>x. f x \<le> c * \<bar>g x\<bar>" by (metis abs_mult abs_ge_self order_trans) |
235 thus "\<exists>c. \<forall>x. f x \<le> c * \<bar>g x\<bar>" by (metis abs_mult abs_ge_self order_trans) |
271 qed |
236 qed |
272 |
237 |
273 text{*So here is the easier (and more natural) problem using transitivity*} |
238 lemma bigo_bounded: "\<forall>x. 0 <= f x \<Longrightarrow> \<forall>x. f x <= g x \<Longrightarrow> f : O(g)" |
274 declare [[ sledgehammer_problem_prefix = "BigO__bigo_bounded_alt_trans" ]] |
239 apply (erule bigo_bounded_alt [of f 1 g]) |
275 lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)" |
240 by (metis mult_1) |
276 apply (auto simp add: bigo_def) |
241 |
277 (* Version 1: one-line proof *) |
242 lemma bigo_bounded2: "\<forall>x. lb x <= f x \<Longrightarrow> \<forall>x. f x <= lb x + g x \<Longrightarrow> f : lb +o O(g)" |
278 by (metis abs_ge_self abs_mult order_trans) |
|
279 |
|
280 text{*So here is the easier (and more natural) problem using transitivity*} |
|
281 declare [[ sledgehammer_problem_prefix = "BigO__bigo_bounded_alt_trans" ]] |
|
282 lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)" |
|
283 apply (auto simp add: bigo_def) |
|
284 (* Version 2: structured proof *) |
|
285 proof - |
|
286 assume "\<forall>x. f x \<le> c * g x" |
|
287 thus "\<exists>c. \<forall>x. f x \<le> c * \<bar>g x\<bar>" by (metis abs_mult abs_ge_self order_trans) |
|
288 qed |
|
289 |
|
290 lemma bigo_bounded: "ALL x. 0 <= f x ==> ALL x. f x <= g x ==> |
|
291 f : O(g)" |
|
292 apply (erule bigo_bounded_alt [of f 1 g]) |
|
293 apply simp |
|
294 done |
|
295 |
|
296 declare [[ sledgehammer_problem_prefix = "BigO__bigo_bounded2" ]] |
|
297 lemma bigo_bounded2: "ALL x. lb x <= f x ==> ALL x. f x <= lb x + g x ==> |
|
298 f : lb +o O(g)" |
|
299 apply (rule set_minus_imp_plus) |
243 apply (rule set_minus_imp_plus) |
300 apply (rule bigo_bounded) |
244 apply (rule bigo_bounded) |
301 apply (auto simp add: diff_minus fun_Compl_def func_plus) |
245 apply (auto simp add: diff_minus fun_Compl_def func_plus) |
302 prefer 2 |
246 prefer 2 |
303 apply (drule_tac x = x in spec)+ |
247 apply (drule_tac x = x in spec)+ |
306 fix x :: 'a |
250 fix x :: 'a |
307 assume "\<forall>x. lb x \<le> f x" |
251 assume "\<forall>x. lb x \<le> f x" |
308 thus "(0\<Colon>'b) \<le> f x + - lb x" by (metis not_leE diff_minus less_iff_diff_less_0 less_le_not_le) |
252 thus "(0\<Colon>'b) \<le> f x + - lb x" by (metis not_leE diff_minus less_iff_diff_less_0 less_le_not_le) |
309 qed |
253 qed |
310 |
254 |
311 declare [[ sledgehammer_problem_prefix = "BigO__bigo_abs" ]] |
255 lemma bigo_abs: "(\<lambda>x. abs(f x)) =o O(f)" |
312 lemma bigo_abs: "(%x. abs(f x)) =o O(f)" |
|
313 apply (unfold bigo_def) |
256 apply (unfold bigo_def) |
314 apply auto |
257 apply auto |
315 by (metis mult_1 order_refl) |
258 by (metis mult_1 order_refl) |
316 |
259 |
317 declare [[ sledgehammer_problem_prefix = "BigO__bigo_abs2" ]] |
260 lemma bigo_abs2: "f =o O(\<lambda>x. abs(f x))" |
318 lemma bigo_abs2: "f =o O(%x. abs(f x))" |
|
319 apply (unfold bigo_def) |
261 apply (unfold bigo_def) |
320 apply auto |
262 apply auto |
321 by (metis mult_1 order_refl) |
263 by (metis mult_1 order_refl) |
322 |
264 |
323 lemma bigo_abs3: "O(f) = O(%x. abs(f x))" |
265 lemma bigo_abs3: "O(f) = O(\<lambda>x. abs(f x))" |
324 proof - |
266 proof - |
325 have F1: "\<forall>v u. u \<in> O(v) \<longrightarrow> O(u) \<subseteq> O(v)" by (metis bigo_elt_subset) |
267 have F1: "\<forall>v u. u \<in> O(v) \<longrightarrow> O(u) \<subseteq> O(v)" by (metis bigo_elt_subset) |
326 have F2: "\<forall>u. (\<lambda>R. \<bar>u R\<bar>) \<in> O(u)" by (metis bigo_abs) |
268 have F2: "\<forall>u. (\<lambda>R. \<bar>u R\<bar>) \<in> O(u)" by (metis bigo_abs) |
327 have "\<forall>u. u \<in> O(\<lambda>R. \<bar>u R\<bar>)" by (metis bigo_abs2) |
269 have "\<forall>u. u \<in> O(\<lambda>R. \<bar>u R\<bar>)" by (metis bigo_abs2) |
328 thus "O(f) = O(\<lambda>x. \<bar>f x\<bar>)" using F1 F2 by auto |
270 thus "O(f) = O(\<lambda>x. \<bar>f x\<bar>)" using F1 F2 by auto |
329 qed |
271 qed |
330 |
272 |
331 lemma bigo_abs4: "f =o g +o O(h) ==> |
273 lemma bigo_abs4: "f =o g +o O(h) \<Longrightarrow> (\<lambda>x. abs (f x)) =o (\<lambda>x. abs (g x)) +o O(h)" |
332 (%x. abs (f x)) =o (%x. abs (g x)) +o O(h)" |
|
333 apply (drule set_plus_imp_minus) |
274 apply (drule set_plus_imp_minus) |
334 apply (rule set_minus_imp_plus) |
275 apply (rule set_minus_imp_plus) |
335 apply (subst fun_diff_def) |
276 apply (subst fun_diff_def) |
336 proof - |
277 proof - |
337 assume a: "f - g : O(h)" |
278 assume a: "f - g : O(h)" |
338 have "(%x. abs (f x) - abs (g x)) =o O(%x. abs(abs (f x) - abs (g x)))" |
279 have "(\<lambda>x. abs (f x) - abs (g x)) =o O(\<lambda>x. abs(abs (f x) - abs (g x)))" |
339 by (rule bigo_abs2) |
280 by (rule bigo_abs2) |
340 also have "... <= O(%x. abs (f x - g x))" |
281 also have "... <= O(\<lambda>x. abs (f x - g x))" |
341 apply (rule bigo_elt_subset) |
282 apply (rule bigo_elt_subset) |
342 apply (rule bigo_bounded) |
283 apply (rule bigo_bounded) |
343 apply force |
284 apply force |
344 apply (rule allI) |
285 apply (rule allI) |
345 apply (rule abs_triangle_ineq3) |
286 apply (rule abs_triangle_ineq3) |
349 apply (subst fun_diff_def) |
290 apply (subst fun_diff_def) |
350 apply (rule bigo_abs) |
291 apply (rule bigo_abs) |
351 done |
292 done |
352 also have "... <= O(h)" |
293 also have "... <= O(h)" |
353 using a by (rule bigo_elt_subset) |
294 using a by (rule bigo_elt_subset) |
354 finally show "(%x. abs (f x) - abs (g x)) : O(h)". |
295 finally show "(\<lambda>x. abs (f x) - abs (g x)) : O(h)". |
355 qed |
296 qed |
356 |
297 |
357 lemma bigo_abs5: "f =o O(g) ==> (%x. abs(f x)) =o O(g)" |
298 lemma bigo_abs5: "f =o O(g) \<Longrightarrow> (\<lambda>x. abs(f x)) =o O(g)" |
358 by (unfold bigo_def, auto) |
299 by (unfold bigo_def, auto) |
359 |
300 |
360 lemma bigo_elt_subset2 [intro]: "f : g +o O(h) ==> O(f) <= O(g) \<oplus> O(h)" |
301 lemma bigo_elt_subset2 [intro]: "f : g +o O(h) \<Longrightarrow> O(f) <= O(g) \<oplus> O(h)" |
361 proof - |
302 proof - |
362 assume "f : g +o O(h)" |
303 assume "f : g +o O(h)" |
363 also have "... <= O(g) \<oplus> O(h)" |
304 also have "... <= O(g) \<oplus> O(h)" |
364 by (auto del: subsetI) |
305 by (auto del: subsetI) |
365 also have "... = O(%x. abs(g x)) \<oplus> O(%x. abs(h x))" |
306 also have "... = O(\<lambda>x. abs(g x)) \<oplus> O(\<lambda>x. abs(h x))" |
366 apply (subst bigo_abs3 [symmetric])+ |
307 apply (subst bigo_abs3 [symmetric])+ |
367 apply (rule refl) |
308 apply (rule refl) |
368 done |
309 done |
369 also have "... = O((%x. abs(g x)) + (%x. abs(h x)))" |
310 also have "... = O((\<lambda>x. abs(g x)) + (\<lambda>x. abs(h x)))" |
370 by (rule bigo_plus_eq [symmetric], auto) |
311 by (rule bigo_plus_eq [symmetric], auto) |
371 finally have "f : ...". |
312 finally have "f : ...". |
372 then have "O(f) <= ..." |
313 then have "O(f) <= ..." |
373 by (elim bigo_elt_subset) |
314 by (elim bigo_elt_subset) |
374 also have "... = O(%x. abs(g x)) \<oplus> O(%x. abs(h x))" |
315 also have "... = O(\<lambda>x. abs(g x)) \<oplus> O(\<lambda>x. abs(h x))" |
375 by (rule bigo_plus_eq, auto) |
316 by (rule bigo_plus_eq, auto) |
376 finally show ?thesis |
317 finally show ?thesis |
377 by (simp add: bigo_abs3 [symmetric]) |
318 by (simp add: bigo_abs3 [symmetric]) |
378 qed |
319 qed |
379 |
320 |
380 declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult" ]] |
|
381 lemma bigo_mult [intro]: "O(f)\<otimes>O(g) <= O(f * g)" |
321 lemma bigo_mult [intro]: "O(f)\<otimes>O(g) <= O(f * g)" |
382 apply (rule subsetI) |
322 apply (rule subsetI) |
383 apply (subst bigo_def) |
323 apply (subst bigo_def) |
384 apply (auto simp del: abs_mult mult_ac |
324 apply (auto simp del: abs_mult mult_ac |
385 simp add: bigo_alt_def set_times_def func_times) |
325 simp add: bigo_alt_def set_times_def func_times) |
386 (*sledgehammer*) |
326 (* sledgehammer *) |
387 apply (rule_tac x = "c * ca" in exI) |
327 apply (rule_tac x = "c * ca" in exI) |
388 apply(rule allI) |
328 apply(rule allI) |
389 apply(erule_tac x = x in allE)+ |
329 apply(erule_tac x = x in allE)+ |
390 apply(subgoal_tac "c * ca * abs(f x * g x) = |
330 apply(subgoal_tac "c * ca * abs(f x * g x) = |
391 (c * abs(f x)) * (ca * abs(g x))") |
331 (c * abs(f x)) * (ca * abs(g x))") |
392 using [[ sledgehammer_problem_prefix = "BigO__bigo_mult_simpler" ]] |
|
393 prefer 2 |
332 prefer 2 |
394 apply (metis mult_assoc mult_left_commute |
333 apply (metis mult_assoc mult_left_commute |
395 abs_of_pos mult_left_commute |
334 abs_of_pos mult_left_commute |
396 abs_mult mult_pos_pos) |
335 abs_mult mult_pos_pos) |
397 apply (erule ssubst) |
336 apply (erule ssubst) |
398 apply (subst abs_mult) |
337 apply (subst abs_mult) |
399 (* not quite as hard as BigO__bigo_mult_simpler_1 (a hard problem!) since |
338 (* not quite as hard as BigO__bigo_mult_simpler_1 (a hard problem!) since |
400 abs_mult has just been done *) |
339 abs_mult has just been done *) |
401 by (metis abs_ge_zero mult_mono') |
340 by (metis abs_ge_zero mult_mono') |
402 |
341 |
403 declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult2" ]] |
|
404 lemma bigo_mult2 [intro]: "f *o O(g) <= O(f * g)" |
342 lemma bigo_mult2 [intro]: "f *o O(g) <= O(f * g)" |
405 apply (auto simp add: bigo_def elt_set_times_def func_times abs_mult) |
343 apply (auto simp add: bigo_def elt_set_times_def func_times abs_mult) |
406 (*sledgehammer*) |
344 (* sledgehammer *) |
407 apply (rule_tac x = c in exI) |
345 apply (rule_tac x = c in exI) |
408 apply clarify |
346 apply clarify |
409 apply (drule_tac x = x in spec) |
347 apply (drule_tac x = x in spec) |
410 using [[ sledgehammer_problem_prefix = "BigO__bigo_mult2_simpler" ]] |
|
411 (*sledgehammer [no luck]*) |
348 (*sledgehammer [no luck]*) |
412 apply (subgoal_tac "abs(f x) * abs(b x) <= abs(f x) * (c * abs(g x))") |
349 apply (subgoal_tac "abs(f x) * abs(b x) <= abs(f x) * (c * abs(g x))") |
413 apply (simp add: mult_ac) |
350 apply (simp add: mult_ac) |
414 apply (rule mult_left_mono, assumption) |
351 apply (rule mult_left_mono, assumption) |
415 apply (rule abs_ge_zero) |
352 apply (rule abs_ge_zero) |
416 done |
353 done |
417 |
354 |
418 declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult3" ]] |
355 lemma bigo_mult3: "f : O(h) \<Longrightarrow> g : O(j) \<Longrightarrow> f * g : O(h * j)" |
419 lemma bigo_mult3: "f : O(h) ==> g : O(j) ==> f * g : O(h * j)" |
|
420 by (metis bigo_mult set_rev_mp set_times_intro) |
356 by (metis bigo_mult set_rev_mp set_times_intro) |
421 |
357 |
422 declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult4" ]] |
358 lemma bigo_mult4 [intro]:"f : k +o O(h) \<Longrightarrow> g * f : (g * k) +o O(g * h)" |
423 lemma bigo_mult4 [intro]:"f : k +o O(h) ==> g * f : (g * k) +o O(g * h)" |
|
424 by (metis bigo_mult2 set_plus_mono_b set_times_intro2 set_times_plus_distrib) |
359 by (metis bigo_mult2 set_plus_mono_b set_times_intro2 set_times_plus_distrib) |
425 |
360 |
426 |
361 lemma bigo_mult5: "\<forall>x. f x ~= 0 \<Longrightarrow> |
427 lemma bigo_mult5: "ALL x. f x ~= 0 ==> |
362 O(f * g) <= (f\<Colon>'a => ('b\<Colon>{linordered_field,number_ring})) *o O(g)" |
428 O(f * g) <= (f::'a => ('b::{linordered_field,number_ring})) *o O(g)" |
363 proof - |
429 proof - |
364 assume a: "\<forall>x. f x ~= 0" |
430 assume a: "ALL x. f x ~= 0" |
|
431 show "O(f * g) <= f *o O(g)" |
365 show "O(f * g) <= f *o O(g)" |
432 proof |
366 proof |
433 fix h |
367 fix h |
434 assume h: "h : O(f * g)" |
368 assume h: "h : O(f * g)" |
435 then have "(%x. 1 / (f x)) * h : (%x. 1 / f x) *o O(f * g)" |
369 then have "(\<lambda>x. 1 / (f x)) * h : (\<lambda>x. 1 / f x) *o O(f * g)" |
436 by auto |
370 by auto |
437 also have "... <= O((%x. 1 / f x) * (f * g))" |
371 also have "... <= O((\<lambda>x. 1 / f x) * (f * g))" |
438 by (rule bigo_mult2) |
372 by (rule bigo_mult2) |
439 also have "(%x. 1 / f x) * (f * g) = g" |
373 also have "(\<lambda>x. 1 / f x) * (f * g) = g" |
440 apply (simp add: func_times) |
374 apply (simp add: func_times) |
441 apply (rule ext) |
375 apply (rule ext) |
442 apply (simp add: a h nonzero_divide_eq_eq mult_ac) |
376 apply (simp add: a h nonzero_divide_eq_eq mult_ac) |
443 done |
377 done |
444 finally have "(%x. (1::'b) / f x) * h : O(g)". |
378 finally have "(\<lambda>x. (1\<Colon>'b) / f x) * h : O(g)". |
445 then have "f * ((%x. (1::'b) / f x) * h) : f *o O(g)" |
379 then have "f * ((\<lambda>x. (1\<Colon>'b) / f x) * h) : f *o O(g)" |
446 by auto |
380 by auto |
447 also have "f * ((%x. (1::'b) / f x) * h) = h" |
381 also have "f * ((\<lambda>x. (1\<Colon>'b) / f x) * h) = h" |
448 apply (simp add: func_times) |
382 apply (simp add: func_times) |
449 apply (rule ext) |
383 apply (rule ext) |
450 apply (simp add: a h nonzero_divide_eq_eq mult_ac) |
384 apply (simp add: a h nonzero_divide_eq_eq mult_ac) |
451 done |
385 done |
452 finally show "h : f *o O(g)". |
386 finally show "h : f *o O(g)". |
453 qed |
387 qed |
454 qed |
388 qed |
455 |
389 |
456 declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult6" ]] |
390 lemma bigo_mult6: "\<forall>x. f x ~= 0 \<Longrightarrow> |
457 lemma bigo_mult6: "ALL x. f x ~= 0 ==> |
391 O(f * g) = (f\<Colon>'a => ('b\<Colon>{linordered_field,number_ring})) *o O(g)" |
458 O(f * g) = (f::'a => ('b::{linordered_field,number_ring})) *o O(g)" |
|
459 by (metis bigo_mult2 bigo_mult5 order_antisym) |
392 by (metis bigo_mult2 bigo_mult5 order_antisym) |
460 |
393 |
461 (*proof requires relaxing relevance: 2007-01-25*) |
394 (*proof requires relaxing relevance: 2007-01-25*) |
462 declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult7" ]] |
|
463 declare bigo_mult6 [simp] |
395 declare bigo_mult6 [simp] |
464 lemma bigo_mult7: "ALL x. f x ~= 0 ==> |
396 lemma bigo_mult7: "\<forall>x. f x ~= 0 \<Longrightarrow> |
465 O(f * g) <= O(f::'a => ('b::{linordered_field,number_ring})) \<otimes> O(g)" |
397 O(f * g) <= O(f\<Colon>'a => ('b\<Colon>{linordered_field,number_ring})) \<otimes> O(g)" |
466 (*sledgehammer*) |
398 (* sledgehammer *) |
467 apply (subst bigo_mult6) |
399 apply (subst bigo_mult6) |
468 apply assumption |
400 apply assumption |
469 apply (rule set_times_mono3) |
401 apply (rule set_times_mono3) |
470 apply (rule bigo_refl) |
402 apply (rule bigo_refl) |
471 done |
403 done |
472 declare bigo_mult6 [simp del] |
404 |
473 |
405 declare bigo_mult6 [simp del] |
474 declare [[ sledgehammer_problem_prefix = "BigO__bigo_mult8" ]] |
406 declare bigo_mult7 [intro!] |
475 declare bigo_mult7[intro!] |
407 |
476 lemma bigo_mult8: "ALL x. f x ~= 0 ==> |
408 lemma bigo_mult8: "\<forall>x. f x ~= 0 \<Longrightarrow> |
477 O(f * g) = O(f::'a => ('b::{linordered_field,number_ring})) \<otimes> O(g)" |
409 O(f * g) = O(f\<Colon>'a => ('b\<Colon>{linordered_field,number_ring})) \<otimes> O(g)" |
478 by (metis bigo_mult bigo_mult7 order_antisym_conv) |
410 by (metis bigo_mult bigo_mult7 order_antisym_conv) |
479 |
411 |
480 lemma bigo_minus [intro]: "f : O(g) ==> - f : O(g)" |
412 lemma bigo_minus [intro]: "f : O(g) \<Longrightarrow> - f : O(g)" |
481 by (auto simp add: bigo_def fun_Compl_def) |
413 by (auto simp add: bigo_def fun_Compl_def) |
482 |
414 |
483 lemma bigo_minus2: "f : g +o O(h) ==> -f : -g +o O(h)" |
415 lemma bigo_minus2: "f : g +o O(h) \<Longrightarrow> -f : -g +o O(h)" |
484 apply (rule set_minus_imp_plus) |
416 apply (rule set_minus_imp_plus) |
485 apply (drule set_plus_imp_minus) |
417 apply (drule set_plus_imp_minus) |
486 apply (drule bigo_minus) |
418 apply (drule bigo_minus) |
487 apply (simp add: diff_minus) |
419 apply (simp add: diff_minus) |
488 done |
420 done |
489 |
421 |
490 lemma bigo_minus3: "O(-f) = O(f)" |
422 lemma bigo_minus3: "O(-f) = O(f)" |
491 by (auto simp add: bigo_def fun_Compl_def abs_minus_cancel) |
423 by (auto simp add: bigo_def fun_Compl_def abs_minus_cancel) |
492 |
424 |
493 lemma bigo_plus_absorb_lemma1: "f : O(g) ==> f +o O(g) <= O(g)" |
425 lemma bigo_plus_absorb_lemma1: "f : O(g) \<Longrightarrow> f +o O(g) <= O(g)" |
494 proof - |
426 proof - |
495 assume a: "f : O(g)" |
427 assume a: "f : O(g)" |
496 show "f +o O(g) <= O(g)" |
428 show "f +o O(g) <= O(g)" |
497 proof - |
429 proof - |
498 have "f : O(f)" by auto |
430 have "f : O(f)" by auto |
520 by (simp add: set_plus_rearranges) |
452 by (simp add: set_plus_rearranges) |
521 finally show ?thesis . |
453 finally show ?thesis . |
522 qed |
454 qed |
523 qed |
455 qed |
524 |
456 |
525 declare [[ sledgehammer_problem_prefix = "BigO__bigo_plus_absorb" ]] |
457 lemma bigo_plus_absorb [simp]: "f : O(g) \<Longrightarrow> f +o O(g) = O(g)" |
526 lemma bigo_plus_absorb [simp]: "f : O(g) ==> f +o O(g) = O(g)" |
|
527 by (metis bigo_plus_absorb_lemma1 bigo_plus_absorb_lemma2 order_eq_iff) |
458 by (metis bigo_plus_absorb_lemma1 bigo_plus_absorb_lemma2 order_eq_iff) |
528 |
459 |
529 lemma bigo_plus_absorb2 [intro]: "f : O(g) ==> A <= O(g) ==> f +o A <= O(g)" |
460 lemma bigo_plus_absorb2 [intro]: "f : O(g) \<Longrightarrow> A <= O(g) \<Longrightarrow> f +o A <= O(g)" |
530 apply (subgoal_tac "f +o A <= f +o O(g)") |
461 apply (subgoal_tac "f +o A <= f +o O(g)") |
531 apply force+ |
462 apply force+ |
532 done |
463 done |
533 |
464 |
534 lemma bigo_add_commute_imp: "f : g +o O(h) ==> g : f +o O(h)" |
465 lemma bigo_add_commute_imp: "f : g +o O(h) \<Longrightarrow> g : f +o O(h)" |
535 apply (subst set_minus_plus [symmetric]) |
466 apply (subst set_minus_plus [symmetric]) |
536 apply (subgoal_tac "g - f = - (f - g)") |
467 apply (subgoal_tac "g - f = - (f - g)") |
537 apply (erule ssubst) |
468 apply (erule ssubst) |
538 apply (rule bigo_minus) |
469 apply (rule bigo_minus) |
539 apply (subst set_minus_plus) |
470 apply (subst set_minus_plus) |
540 apply assumption |
471 apply assumption |
541 apply (simp add: diff_minus add_ac) |
472 apply (simp add: diff_minus add_ac) |
542 done |
473 done |
543 |
474 |
544 lemma bigo_add_commute: "(f : g +o O(h)) = (g : f +o O(h))" |
475 lemma bigo_add_commute: "(f : g +o O(h)) = (g : f +o O(h))" |
545 apply (rule iffI) |
476 apply (rule iffI) |
546 apply (erule bigo_add_commute_imp)+ |
477 apply (erule bigo_add_commute_imp)+ |
547 done |
478 done |
548 |
479 |
549 lemma bigo_const1: "(%x. c) : O(%x. 1)" |
480 lemma bigo_const1: "(\<lambda>x. c) : O(\<lambda>x. 1)" |
550 by (auto simp add: bigo_def mult_ac) |
481 by (auto simp add: bigo_def mult_ac) |
551 |
482 |
552 declare [[ sledgehammer_problem_prefix = "BigO__bigo_const2" ]] |
483 lemma (*bigo_const2 [intro]:*) "O(\<lambda>x. c) <= O(\<lambda>x. 1)" |
553 lemma (*bigo_const2 [intro]:*) "O(%x. c) <= O(%x. 1)" |
|
554 by (metis bigo_const1 bigo_elt_subset) |
484 by (metis bigo_const1 bigo_elt_subset) |
555 |
485 |
556 lemma bigo_const2 [intro]: "O(%x. c::'b::{linordered_idom,number_ring}) <= O(%x. 1)" |
486 lemma bigo_const2 [intro]: "O(\<lambda>x. c\<Colon>'b\<Colon>{linordered_idom,number_ring}) <= O(\<lambda>x. 1)" |
557 (* "thus" had to be replaced by "show" with an explicit reference to "F1" *) |
487 proof - |
558 proof - |
488 have "\<forall>u. (\<lambda>Q. u) \<in> O(\<lambda>Q. 1)" by (metis bigo_const1) |
559 have F1: "\<forall>u. (\<lambda>Q. u) \<in> O(\<lambda>Q. 1)" by (metis bigo_const1) |
489 thus "O(\<lambda>x. c) \<subseteq> O(\<lambda>x. 1)" by (metis bigo_elt_subset) |
560 show "O(\<lambda>x. c) \<subseteq> O(\<lambda>x. 1)" by (metis F1 bigo_elt_subset) |
490 qed |
561 qed |
491 |
562 |
492 lemma bigo_const3: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow> (\<lambda>x. 1) : O(\<lambda>x. c)" |
563 declare [[ sledgehammer_problem_prefix = "BigO__bigo_const3" ]] |
|
564 lemma bigo_const3: "(c::'a::{linordered_field,number_ring}) ~= 0 ==> (%x. 1) : O(%x. c)" |
|
565 apply (simp add: bigo_def) |
493 apply (simp add: bigo_def) |
566 by (metis abs_eq_0 left_inverse order_refl) |
494 by (metis abs_eq_0 left_inverse order_refl) |
567 |
495 |
568 lemma bigo_const4: "(c::'a::{linordered_field,number_ring}) ~= 0 ==> O(%x. 1) <= O(%x. c)" |
496 lemma bigo_const4: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow> O(\<lambda>x. 1) <= O(\<lambda>x. c)" |
569 by (rule bigo_elt_subset, rule bigo_const3, assumption) |
497 by (rule bigo_elt_subset, rule bigo_const3, assumption) |
570 |
498 |
571 lemma bigo_const [simp]: "(c::'a::{linordered_field,number_ring}) ~= 0 ==> |
499 lemma bigo_const [simp]: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow> |
572 O(%x. c) = O(%x. 1)" |
500 O(\<lambda>x. c) = O(\<lambda>x. 1)" |
573 by (rule equalityI, rule bigo_const2, rule bigo_const4, assumption) |
501 by (rule equalityI, rule bigo_const2, rule bigo_const4, assumption) |
574 |
502 |
575 declare [[ sledgehammer_problem_prefix = "BigO__bigo_const_mult1" ]] |
503 lemma bigo_const_mult1: "(\<lambda>x. c * f x) : O(f)" |
576 lemma bigo_const_mult1: "(%x. c * f x) : O(f)" |
|
577 apply (simp add: bigo_def abs_mult) |
504 apply (simp add: bigo_def abs_mult) |
578 by (metis le_less) |
505 by (metis le_less) |
579 |
506 |
580 lemma bigo_const_mult2: "O(%x. c * f x) <= O(f)" |
507 lemma bigo_const_mult2: "O(\<lambda>x. c * f x) <= O(f)" |
581 by (rule bigo_elt_subset, rule bigo_const_mult1) |
508 by (rule bigo_elt_subset, rule bigo_const_mult1) |
582 |
509 |
583 declare [[ sledgehammer_problem_prefix = "BigO__bigo_const_mult3" ]] |
510 lemma bigo_const_mult3: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow> f : O(\<lambda>x. c * f x)" |
584 lemma bigo_const_mult3: "(c::'a::{linordered_field,number_ring}) ~= 0 ==> f : O(%x. c * f x)" |
511 apply (simp add: bigo_def) |
585 apply (simp add: bigo_def) |
512 (* sledgehammer *) |
586 (*sledgehammer [no luck]*) |
513 apply (rule_tac x = "abs(inverse c)" in exI) |
587 apply (rule_tac x = "abs(inverse c)" in exI) |
514 apply (simp only: abs_mult [symmetric] mult_assoc [symmetric]) |
588 apply (simp only: abs_mult [symmetric] mult_assoc [symmetric]) |
|
589 apply (subst left_inverse) |
515 apply (subst left_inverse) |
590 apply (auto ) |
516 by auto |
591 done |
517 |
592 |
518 lemma bigo_const_mult4: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow> |
593 lemma bigo_const_mult4: "(c::'a::{linordered_field,number_ring}) ~= 0 ==> |
519 O(f) <= O(\<lambda>x. c * f x)" |
594 O(f) <= O(%x. c * f x)" |
|
595 by (rule bigo_elt_subset, rule bigo_const_mult3, assumption) |
520 by (rule bigo_elt_subset, rule bigo_const_mult3, assumption) |
596 |
521 |
597 lemma bigo_const_mult [simp]: "(c::'a::{linordered_field,number_ring}) ~= 0 ==> |
522 lemma bigo_const_mult [simp]: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow> |
598 O(%x. c * f x) = O(f)" |
523 O(\<lambda>x. c * f x) = O(f)" |
599 by (rule equalityI, rule bigo_const_mult2, erule bigo_const_mult4) |
524 by (rule equalityI, rule bigo_const_mult2, erule bigo_const_mult4) |
600 |
525 |
601 declare [[ sledgehammer_problem_prefix = "BigO__bigo_const_mult5" ]] |
526 lemma bigo_const_mult5 [simp]: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow> |
602 lemma bigo_const_mult5 [simp]: "(c::'a::{linordered_field,number_ring}) ~= 0 ==> |
527 (\<lambda>x. c) *o O(f) = O(f)" |
603 (%x. c) *o O(f) = O(f)" |
|
604 apply (auto del: subsetI) |
528 apply (auto del: subsetI) |
605 apply (rule order_trans) |
529 apply (rule order_trans) |
606 apply (rule bigo_mult2) |
530 apply (rule bigo_mult2) |
607 apply (simp add: func_times) |
531 apply (simp add: func_times) |
608 apply (auto intro!: subsetI simp add: bigo_def elt_set_times_def func_times) |
532 apply (auto intro!: subsetI simp add: bigo_def elt_set_times_def func_times) |
609 apply (rule_tac x = "%y. inverse c * x y" in exI) |
533 apply (rule_tac x = "\<lambda>y. inverse c * x y" in exI) |
610 apply (rename_tac g d) |
534 apply (rename_tac g d) |
611 apply safe |
535 apply safe |
612 apply (rule_tac [2] ext) |
536 apply (rule_tac [2] ext) |
613 prefer 2 |
537 prefer 2 |
614 apply simp |
538 apply simp |
649 apply (erule spec) |
571 apply (erule spec) |
650 apply simp |
572 apply simp |
651 apply(simp add: mult_ac) |
573 apply(simp add: mult_ac) |
652 done |
574 done |
653 |
575 |
654 lemma bigo_const_mult7 [intro]: "f =o O(g) ==> (%x. c * f x) =o O(g)" |
576 lemma bigo_const_mult7 [intro]: "f =o O(g) \<Longrightarrow> (\<lambda>x. c * f x) =o O(g)" |
655 proof - |
577 proof - |
656 assume "f =o O(g)" |
578 assume "f =o O(g)" |
657 then have "(%x. c) * f =o (%x. c) *o O(g)" |
579 then have "(\<lambda>x. c) * f =o (\<lambda>x. c) *o O(g)" |
658 by auto |
580 by auto |
659 also have "(%x. c) * f = (%x. c * f x)" |
581 also have "(\<lambda>x. c) * f = (\<lambda>x. c * f x)" |
660 by (simp add: func_times) |
582 by (simp add: func_times) |
661 also have "(%x. c) *o O(g) <= O(g)" |
583 also have "(\<lambda>x. c) *o O(g) <= O(g)" |
662 by (auto del: subsetI) |
584 by (auto del: subsetI) |
663 finally show ?thesis . |
585 finally show ?thesis . |
664 qed |
586 qed |
665 |
587 |
666 lemma bigo_compose1: "f =o O(g) ==> (%x. f(k x)) =o O(%x. g(k x))" |
588 lemma bigo_compose1: "f =o O(g) \<Longrightarrow> (\<lambda>x. f(k x)) =o O(\<lambda>x. g(k x))" |
667 by (unfold bigo_def, auto) |
589 by (unfold bigo_def, auto) |
668 |
590 |
669 lemma bigo_compose2: "f =o g +o O(h) ==> (%x. f(k x)) =o (%x. g(k x)) +o |
591 lemma bigo_compose2: "f =o g +o O(h) \<Longrightarrow> (\<lambda>x. f(k x)) =o (\<lambda>x. g(k x)) +o |
670 O(%x. h(k x))" |
592 O(\<lambda>x. h(k x))" |
671 apply (simp only: set_minus_plus [symmetric] diff_minus fun_Compl_def |
593 apply (simp only: set_minus_plus [symmetric] diff_minus fun_Compl_def |
672 func_plus) |
594 func_plus) |
673 apply (erule bigo_compose1) |
595 apply (erule bigo_compose1) |
674 done |
596 done |
675 |
597 |
676 subsection {* Setsum *} |
598 subsection {* Setsum *} |
677 |
599 |
678 lemma bigo_setsum_main: "ALL x. ALL y : A x. 0 <= h x y ==> |
600 lemma bigo_setsum_main: "\<forall>x. \<forall>y \<in> A x. 0 <= h x y \<Longrightarrow> |
679 EX c. ALL x. ALL y : A x. abs(f x y) <= c * (h x y) ==> |
601 \<exists>c. \<forall>x. \<forall>y \<in> A x. abs (f x y) <= c * (h x y) \<Longrightarrow> |
680 (%x. SUM y : A x. f x y) =o O(%x. SUM y : A x. h x y)" |
602 (\<lambda>x. SUM y : A x. f x y) =o O(\<lambda>x. SUM y : A x. h x y)" |
681 apply (auto simp add: bigo_def) |
603 apply (auto simp add: bigo_def) |
682 apply (rule_tac x = "abs c" in exI) |
604 apply (rule_tac x = "abs c" in exI) |
683 apply (subst abs_of_nonneg) back back |
605 apply (subst abs_of_nonneg) back back |
684 apply (rule setsum_nonneg) |
606 apply (rule setsum_nonneg) |
685 apply force |
607 apply force |
689 apply (rule setsum_abs) |
611 apply (rule setsum_abs) |
690 apply (rule setsum_mono) |
612 apply (rule setsum_mono) |
691 apply (blast intro: order_trans mult_right_mono abs_ge_self) |
613 apply (blast intro: order_trans mult_right_mono abs_ge_self) |
692 done |
614 done |
693 |
615 |
694 declare [[ sledgehammer_problem_prefix = "BigO__bigo_setsum1" ]] |
616 lemma bigo_setsum1: "\<forall>x y. 0 <= h x y \<Longrightarrow> |
695 lemma bigo_setsum1: "ALL x y. 0 <= h x y ==> |
617 \<exists>c. \<forall>x y. abs (f x y) <= c * (h x y) \<Longrightarrow> |
696 EX c. ALL x y. abs(f x y) <= c * (h x y) ==> |
618 (\<lambda>x. SUM y : A x. f x y) =o O(\<lambda>x. SUM y : A x. h x y)" |
697 (%x. SUM y : A x. f x y) =o O(%x. SUM y : A x. h x y)" |
619 by (metis (no_types) bigo_setsum_main) |
698 apply (rule bigo_setsum_main) |
620 |
699 (*sledgehammer*) |
621 lemma bigo_setsum2: "\<forall>y. 0 <= h y \<Longrightarrow> |
700 apply force |
622 \<exists>c. \<forall>y. abs(f y) <= c * (h y) \<Longrightarrow> |
701 apply clarsimp |
623 (\<lambda>x. SUM y : A x. f y) =o O(\<lambda>x. SUM y : A x. h y)" |
702 apply (rule_tac x = c in exI) |
|
703 apply force |
|
704 done |
|
705 |
|
706 lemma bigo_setsum2: "ALL y. 0 <= h y ==> |
|
707 EX c. ALL y. abs(f y) <= c * (h y) ==> |
|
708 (%x. SUM y : A x. f y) =o O(%x. SUM y : A x. h y)" |
|
709 by (rule bigo_setsum1, auto) |
624 by (rule bigo_setsum1, auto) |
710 |
625 |
711 declare [[ sledgehammer_problem_prefix = "BigO__bigo_setsum3" ]] |
626 lemma bigo_setsum3: "f =o O(h) \<Longrightarrow> |
712 lemma bigo_setsum3: "f =o O(h) ==> |
627 (\<lambda>x. SUM y : A x. (l x y) * f(k x y)) =o |
713 (%x. SUM y : A x. (l x y) * f(k x y)) =o |
628 O(\<lambda>x. SUM y : A x. abs(l x y * h(k x y)))" |
714 O(%x. SUM y : A x. abs(l x y * h(k x y)))" |
629 apply (rule bigo_setsum1) |
715 apply (rule bigo_setsum1) |
630 apply (rule allI)+ |
716 apply (rule allI)+ |
631 apply (rule abs_ge_zero) |
717 apply (rule abs_ge_zero) |
632 apply (unfold bigo_def) |
718 apply (unfold bigo_def) |
633 apply (auto simp add: abs_mult) |
719 apply (auto simp add: abs_mult) |
634 (* sledgehammer *) |
720 (*sledgehammer*) |
635 apply (rule_tac x = c in exI) |
721 apply (rule_tac x = c in exI) |
636 apply (rule allI)+ |
722 apply (rule allI)+ |
637 apply (subst mult_left_commute) |
723 apply (subst mult_left_commute) |
638 apply (rule mult_left_mono) |
724 apply (rule mult_left_mono) |
639 apply (erule spec) |
725 apply (erule spec) |
640 by (rule abs_ge_zero) |
726 apply (rule abs_ge_zero) |
641 |
727 done |
642 lemma bigo_setsum4: "f =o g +o O(h) \<Longrightarrow> |
728 |
643 (\<lambda>x. SUM y : A x. l x y * f(k x y)) =o |
729 lemma bigo_setsum4: "f =o g +o O(h) ==> |
644 (\<lambda>x. SUM y : A x. l x y * g(k x y)) +o |
730 (%x. SUM y : A x. l x y * f(k x y)) =o |
645 O(\<lambda>x. SUM y : A x. abs(l x y * h(k x y)))" |
731 (%x. SUM y : A x. l x y * g(k x y)) +o |
646 apply (rule set_minus_imp_plus) |
732 O(%x. SUM y : A x. abs(l x y * h(k x y)))" |
647 apply (subst fun_diff_def) |
733 apply (rule set_minus_imp_plus) |
648 apply (subst setsum_subtractf [symmetric]) |
734 apply (subst fun_diff_def) |
649 apply (subst right_diff_distrib [symmetric]) |
735 apply (subst setsum_subtractf [symmetric]) |
650 apply (rule bigo_setsum3) |
736 apply (subst right_diff_distrib [symmetric]) |
651 apply (subst fun_diff_def [symmetric]) |
737 apply (rule bigo_setsum3) |
652 by (erule set_plus_imp_minus) |
738 apply (subst fun_diff_def [symmetric]) |
653 |
739 apply (erule set_plus_imp_minus) |
654 lemma bigo_setsum5: "f =o O(h) \<Longrightarrow> \<forall>x y. 0 <= l x y \<Longrightarrow> |
740 done |
655 \<forall>x. 0 <= h x \<Longrightarrow> |
741 |
656 (\<lambda>x. SUM y : A x. (l x y) * f(k x y)) =o |
742 declare [[ sledgehammer_problem_prefix = "BigO__bigo_setsum5" ]] |
657 O(\<lambda>x. SUM y : A x. (l x y) * h(k x y))" |
743 lemma bigo_setsum5: "f =o O(h) ==> ALL x y. 0 <= l x y ==> |
658 apply (subgoal_tac "(\<lambda>x. SUM y : A x. (l x y) * h(k x y)) = |
744 ALL x. 0 <= h x ==> |
659 (\<lambda>x. SUM y : A x. abs((l x y) * h(k x y)))") |
745 (%x. SUM y : A x. (l x y) * f(k x y)) =o |
|
746 O(%x. SUM y : A x. (l x y) * h(k x y))" |
|
747 apply (subgoal_tac "(%x. SUM y : A x. (l x y) * h(k x y)) = |
|
748 (%x. SUM y : A x. abs((l x y) * h(k x y)))") |
|
749 apply (erule ssubst) |
660 apply (erule ssubst) |
750 apply (erule bigo_setsum3) |
661 apply (erule bigo_setsum3) |
751 apply (rule ext) |
662 apply (rule ext) |
752 apply (rule setsum_cong2) |
663 apply (rule setsum_cong2) |
753 apply (thin_tac "f \<in> O(h)") |
664 apply (thin_tac "f \<in> O(h)") |
754 apply (metis abs_of_nonneg zero_le_mult_iff) |
665 apply (metis abs_of_nonneg zero_le_mult_iff) |
755 done |
666 done |
756 |
667 |
757 lemma bigo_setsum6: "f =o g +o O(h) ==> ALL x y. 0 <= l x y ==> |
668 lemma bigo_setsum6: "f =o g +o O(h) \<Longrightarrow> \<forall>x y. 0 <= l x y \<Longrightarrow> |
758 ALL x. 0 <= h x ==> |
669 \<forall>x. 0 <= h x \<Longrightarrow> |
759 (%x. SUM y : A x. (l x y) * f(k x y)) =o |
670 (\<lambda>x. SUM y : A x. (l x y) * f(k x y)) =o |
760 (%x. SUM y : A x. (l x y) * g(k x y)) +o |
671 (\<lambda>x. SUM y : A x. (l x y) * g(k x y)) +o |
761 O(%x. SUM y : A x. (l x y) * h(k x y))" |
672 O(\<lambda>x. SUM y : A x. (l x y) * h(k x y))" |
762 apply (rule set_minus_imp_plus) |
673 apply (rule set_minus_imp_plus) |
763 apply (subst fun_diff_def) |
674 apply (subst fun_diff_def) |
764 apply (subst setsum_subtractf [symmetric]) |
675 apply (subst setsum_subtractf [symmetric]) |
765 apply (subst right_diff_distrib [symmetric]) |
676 apply (subst right_diff_distrib [symmetric]) |
766 apply (rule bigo_setsum5) |
677 apply (rule bigo_setsum5) |
769 apply auto |
680 apply auto |
770 done |
681 done |
771 |
682 |
772 subsection {* Misc useful stuff *} |
683 subsection {* Misc useful stuff *} |
773 |
684 |
774 lemma bigo_useful_intro: "A <= O(f) ==> B <= O(f) ==> |
685 lemma bigo_useful_intro: "A <= O(f) \<Longrightarrow> B <= O(f) \<Longrightarrow> |
775 A \<oplus> B <= O(f)" |
686 A \<oplus> B <= O(f)" |
776 apply (subst bigo_plus_idemp [symmetric]) |
687 apply (subst bigo_plus_idemp [symmetric]) |
777 apply (rule set_plus_mono2) |
688 apply (rule set_plus_mono2) |
778 apply assumption+ |
689 apply assumption+ |
779 done |
690 done |
780 |
691 |
781 lemma bigo_useful_add: "f =o O(h) ==> g =o O(h) ==> f + g =o O(h)" |
692 lemma bigo_useful_add: "f =o O(h) \<Longrightarrow> g =o O(h) \<Longrightarrow> f + g =o O(h)" |
782 apply (subst bigo_plus_idemp [symmetric]) |
693 apply (subst bigo_plus_idemp [symmetric]) |
783 apply (rule set_plus_intro) |
694 apply (rule set_plus_intro) |
784 apply assumption+ |
695 apply assumption+ |
785 done |
696 done |
786 |
697 |
787 lemma bigo_useful_const_mult: "(c::'a::{linordered_field,number_ring}) ~= 0 ==> |
698 lemma bigo_useful_const_mult: "(c\<Colon>'a\<Colon>{linordered_field,number_ring}) ~= 0 \<Longrightarrow> |
788 (%x. c) * f =o O(h) ==> f =o O(h)" |
699 (\<lambda>x. c) * f =o O(h) \<Longrightarrow> f =o O(h)" |
789 apply (rule subsetD) |
700 apply (rule subsetD) |
790 apply (subgoal_tac "(%x. 1 / c) *o O(h) <= O(h)") |
701 apply (subgoal_tac "(\<lambda>x. 1 / c) *o O(h) <= O(h)") |
791 apply assumption |
702 apply assumption |
792 apply (rule bigo_const_mult6) |
703 apply (rule bigo_const_mult6) |
793 apply (subgoal_tac "f = (%x. 1 / c) * ((%x. c) * f)") |
704 apply (subgoal_tac "f = (\<lambda>x. 1 / c) * ((\<lambda>x. c) * f)") |
794 apply (erule ssubst) |
705 apply (erule ssubst) |
795 apply (erule set_times_intro2) |
706 apply (erule set_times_intro2) |
796 apply (simp add: func_times) |
707 apply (simp add: func_times) |
797 done |
708 done |
798 |
709 |
799 declare [[ sledgehammer_problem_prefix = "BigO__bigo_fix" ]] |
710 lemma bigo_fix: "(\<lambda>x. f ((x\<Colon>nat) + 1)) =o O(\<lambda>x. h(x + 1)) \<Longrightarrow> f 0 = 0 \<Longrightarrow> |
800 lemma bigo_fix: "(%x. f ((x::nat) + 1)) =o O(%x. h(x + 1)) ==> f 0 = 0 ==> |
|
801 f =o O(h)" |
711 f =o O(h)" |
802 apply (simp add: bigo_alt_def) |
712 apply (simp add: bigo_alt_def) |
803 (*sledgehammer*) |
713 by (metis abs_ge_zero abs_mult abs_of_pos abs_zero not0_implies_Suc) |
804 apply clarify |
|
805 apply (rule_tac x = c in exI) |
|
806 apply safe |
|
807 apply (case_tac "x = 0") |
|
808 apply (metis abs_ge_zero abs_zero order_less_le split_mult_pos_le) |
|
809 apply (subgoal_tac "x = Suc (x - 1)") |
|
810 apply metis |
|
811 apply simp |
|
812 done |
|
813 |
|
814 |
714 |
815 lemma bigo_fix2: |
715 lemma bigo_fix2: |
816 "(%x. f ((x::nat) + 1)) =o (%x. g(x + 1)) +o O(%x. h(x + 1)) ==> |
716 "(\<lambda>x. f ((x\<Colon>nat) + 1)) =o (\<lambda>x. g(x + 1)) +o O(\<lambda>x. h(x + 1)) \<Longrightarrow> |
817 f 0 = g 0 ==> f =o g +o O(h)" |
717 f 0 = g 0 \<Longrightarrow> f =o g +o O(h)" |
818 apply (rule set_minus_imp_plus) |
718 apply (rule set_minus_imp_plus) |
819 apply (rule bigo_fix) |
719 apply (rule bigo_fix) |
820 apply (subst fun_diff_def) |
720 apply (subst fun_diff_def) |
821 apply (subst fun_diff_def [symmetric]) |
721 apply (subst fun_diff_def [symmetric]) |
822 apply (rule set_plus_imp_minus) |
722 apply (rule set_plus_imp_minus) |
824 apply (simp add: fun_diff_def) |
724 apply (simp add: fun_diff_def) |
825 done |
725 done |
826 |
726 |
827 subsection {* Less than or equal to *} |
727 subsection {* Less than or equal to *} |
828 |
728 |
829 definition lesso :: "('a => 'b::linordered_idom) => ('a => 'b) => ('a => 'b)" (infixl "<o" 70) where |
729 definition lesso :: "('a => 'b\<Colon>linordered_idom) => ('a => 'b) => ('a => 'b)" (infixl "<o" 70) where |
830 "f <o g == (%x. max (f x - g x) 0)" |
730 "f <o g == (\<lambda>x. max (f x - g x) 0)" |
831 |
731 |
832 lemma bigo_lesseq1: "f =o O(h) ==> ALL x. abs (g x) <= abs (f x) ==> |
732 lemma bigo_lesseq1: "f =o O(h) \<Longrightarrow> \<forall>x. abs (g x) <= abs (f x) \<Longrightarrow> |
833 g =o O(h)" |
733 g =o O(h)" |
834 apply (unfold bigo_def) |
734 apply (unfold bigo_def) |
835 apply clarsimp |
735 apply clarsimp |
836 apply (blast intro: order_trans) |
736 apply (blast intro: order_trans) |
837 done |
737 done |
838 |
738 |
839 lemma bigo_lesseq2: "f =o O(h) ==> ALL x. abs (g x) <= f x ==> |
739 lemma bigo_lesseq2: "f =o O(h) \<Longrightarrow> \<forall>x. abs (g x) <= f x \<Longrightarrow> |
840 g =o O(h)" |
740 g =o O(h)" |
841 apply (erule bigo_lesseq1) |
741 apply (erule bigo_lesseq1) |
842 apply (blast intro: abs_ge_self order_trans) |
742 apply (blast intro: abs_ge_self order_trans) |
843 done |
743 done |
844 |
744 |
845 lemma bigo_lesseq3: "f =o O(h) ==> ALL x. 0 <= g x ==> ALL x. g x <= f x ==> |
745 lemma bigo_lesseq3: "f =o O(h) \<Longrightarrow> \<forall>x. 0 <= g x \<Longrightarrow> \<forall>x. g x <= f x \<Longrightarrow> |
846 g =o O(h)" |
746 g =o O(h)" |
847 apply (erule bigo_lesseq2) |
747 apply (erule bigo_lesseq2) |
848 apply (rule allI) |
748 apply (rule allI) |
849 apply (subst abs_of_nonneg) |
749 apply (subst abs_of_nonneg) |
850 apply (erule spec)+ |
750 apply (erule spec)+ |
851 done |
751 done |
852 |
752 |
853 lemma bigo_lesseq4: "f =o O(h) ==> |
753 lemma bigo_lesseq4: "f =o O(h) \<Longrightarrow> |
854 ALL x. 0 <= g x ==> ALL x. g x <= abs (f x) ==> |
754 \<forall>x. 0 <= g x \<Longrightarrow> \<forall>x. g x <= abs (f x) \<Longrightarrow> |
855 g =o O(h)" |
755 g =o O(h)" |
856 apply (erule bigo_lesseq1) |
756 apply (erule bigo_lesseq1) |
857 apply (rule allI) |
757 apply (rule allI) |
858 apply (subst abs_of_nonneg) |
758 apply (subst abs_of_nonneg) |
859 apply (erule spec)+ |
759 apply (erule spec)+ |
860 done |
760 done |
861 |
761 |
862 declare [[ sledgehammer_problem_prefix = "BigO__bigo_lesso1" ]] |
762 lemma bigo_lesso1: "\<forall>x. f x <= g x \<Longrightarrow> f <o g =o O(h)" |
863 lemma bigo_lesso1: "ALL x. f x <= g x ==> f <o g =o O(h)" |
|
864 apply (unfold lesso_def) |
763 apply (unfold lesso_def) |
865 apply (subgoal_tac "(%x. max (f x - g x) 0) = 0") |
764 apply (subgoal_tac "(\<lambda>x. max (f x - g x) 0) = 0") |
866 proof - |
765 apply (metis bigo_zero) |
867 assume "(\<lambda>x. max (f x - g x) 0) = 0" |
766 by (metis (lam_lifting, no_types) func_zero le_fun_def le_iff_diff_le_0 |
868 thus "(\<lambda>x. max (f x - g x) 0) \<in> O(h)" by (metis bigo_zero) |
767 min_max.sup_absorb2 order_eq_iff) |
869 next |
768 |
870 show "\<forall>x\<Colon>'a. f x \<le> g x \<Longrightarrow> (\<lambda>x\<Colon>'a. max (f x - g x) (0\<Colon>'b)) = (0\<Colon>'a \<Rightarrow> 'b)" |
769 lemma bigo_lesso2: "f =o g +o O(h) \<Longrightarrow> |
871 apply (unfold func_zero) |
770 \<forall>x. 0 <= k x \<Longrightarrow> \<forall>x. k x <= f x \<Longrightarrow> |
872 apply (rule ext) |
|
873 by (simp split: split_max) |
|
874 qed |
|
875 |
|
876 declare [[ sledgehammer_problem_prefix = "BigO__bigo_lesso2" ]] |
|
877 lemma bigo_lesso2: "f =o g +o O(h) ==> |
|
878 ALL x. 0 <= k x ==> ALL x. k x <= f x ==> |
|
879 k <o g =o O(h)" |
771 k <o g =o O(h)" |
880 apply (unfold lesso_def) |
772 apply (unfold lesso_def) |
881 apply (rule bigo_lesseq4) |
773 apply (rule bigo_lesseq4) |
882 apply (erule set_plus_imp_minus) |
774 apply (erule set_plus_imp_minus) |
883 apply (rule allI) |
775 apply (rule allI) |
884 apply (rule le_maxI2) |
776 apply (rule le_maxI2) |
885 apply (rule allI) |
777 apply (rule allI) |
886 apply (subst fun_diff_def) |
778 apply (subst fun_diff_def) |
887 apply (erule thin_rl) |
779 apply (erule thin_rl) |
888 (*sledgehammer*) |
780 (* sledgehammer *) |
889 apply (case_tac "0 <= k x - g x") |
781 apply (case_tac "0 <= k x - g x") |
890 (* apply (metis abs_le_iff add_le_imp_le_right diff_minus le_less |
782 apply (metis (hide_lams, no_types) abs_le_iff add_le_imp_le_right diff_minus le_less |
891 le_max_iff_disj min_max.le_supE min_max.sup_absorb2 |
783 le_max_iff_disj min_max.le_supE min_max.sup_absorb2 |
892 min_max.sup_commute) *) |
784 min_max.sup_commute) |
893 proof - |
785 by (metis abs_ge_zero le_cases min_max.sup_absorb2) |
894 fix x :: 'a |
786 |
895 assume "\<forall>x\<Colon>'a. k x \<le> f x" |
787 lemma bigo_lesso3: "f =o g +o O(h) \<Longrightarrow> |
896 hence F1: "\<forall>x\<^isub>1\<Colon>'a. max (k x\<^isub>1) (f x\<^isub>1) = f x\<^isub>1" by (metis min_max.sup_absorb2) |
788 \<forall>x. 0 <= k x \<Longrightarrow> \<forall>x. g x <= k x \<Longrightarrow> |
897 assume "(0\<Colon>'b) \<le> k x - g x" |
|
898 hence F2: "max (0\<Colon>'b) (k x - g x) = k x - g x" by (metis min_max.sup_absorb2) |
|
899 have F3: "\<forall>x\<^isub>1\<Colon>'b. x\<^isub>1 \<le> \<bar>x\<^isub>1\<bar>" by (metis abs_le_iff le_less) |
|
900 have "\<forall>(x\<^isub>2\<Colon>'b) x\<^isub>1\<Colon>'b. max x\<^isub>1 x\<^isub>2 \<le> x\<^isub>2 \<or> max x\<^isub>1 x\<^isub>2 \<le> x\<^isub>1" by (metis le_less le_max_iff_disj) |
|
901 hence "\<forall>(x\<^isub>3\<Colon>'b) (x\<^isub>2\<Colon>'b) x\<^isub>1\<Colon>'b. x\<^isub>1 - x\<^isub>2 \<le> x\<^isub>3 - x\<^isub>2 \<or> x\<^isub>3 \<le> x\<^isub>1" by (metis add_le_imp_le_right diff_minus min_max.le_supE) |
|
902 hence "k x - g x \<le> f x - g x" by (metis F1 le_less min_max.sup_absorb2 min_max.sup_commute) |
|
903 hence "k x - g x \<le> \<bar>f x - g x\<bar>" by (metis F3 le_max_iff_disj min_max.sup_absorb2) |
|
904 thus "max (k x - g x) (0\<Colon>'b) \<le> \<bar>f x - g x\<bar>" by (metis F2 min_max.sup_commute) |
|
905 next |
|
906 show "\<And>x\<Colon>'a. |
|
907 \<lbrakk>\<forall>x\<Colon>'a. (0\<Colon>'b) \<le> k x; \<forall>x\<Colon>'a. k x \<le> f x; \<not> (0\<Colon>'b) \<le> k x - g x\<rbrakk> |
|
908 \<Longrightarrow> max (k x - g x) (0\<Colon>'b) \<le> \<bar>f x - g x\<bar>" |
|
909 by (metis abs_ge_zero le_cases min_max.sup_absorb2) |
|
910 qed |
|
911 |
|
912 declare [[ sledgehammer_problem_prefix = "BigO__bigo_lesso3" ]] |
|
913 lemma bigo_lesso3: "f =o g +o O(h) ==> |
|
914 ALL x. 0 <= k x ==> ALL x. g x <= k x ==> |
|
915 f <o k =o O(h)" |
789 f <o k =o O(h)" |
916 apply (unfold lesso_def) |
790 apply (unfold lesso_def) |
917 apply (rule bigo_lesseq4) |
791 apply (rule bigo_lesseq4) |
918 apply (erule set_plus_imp_minus) |
792 apply (erule set_plus_imp_minus) |
919 apply (rule allI) |
793 apply (rule allI) |
920 apply (rule le_maxI2) |
794 apply (rule le_maxI2) |
921 apply (rule allI) |
795 apply (rule allI) |
922 apply (subst fun_diff_def) |
796 apply (subst fun_diff_def) |
923 apply (erule thin_rl) |
797 apply (erule thin_rl) |
924 (*sledgehammer*) |
798 (* sledgehammer *) |
925 apply (case_tac "0 <= f x - k x") |
799 apply (case_tac "0 <= f x - k x") |
926 apply (simp) |
800 apply simp |
927 apply (subst abs_of_nonneg) |
801 apply (subst abs_of_nonneg) |
928 apply (drule_tac x = x in spec) back |
802 apply (drule_tac x = x in spec) back |
929 using [[ sledgehammer_problem_prefix = "BigO__bigo_lesso3_simpler" ]] |
803 apply (metis diff_less_0_iff_less linorder_not_le not_leE uminus_add_conv_diff xt1(12) xt1(6)) |
930 apply (metis diff_less_0_iff_less linorder_not_le not_leE uminus_add_conv_diff xt1(12) xt1(6)) |
804 apply (metis add_minus_cancel diff_le_eq le_diff_eq uminus_add_conv_diff) |
931 apply (metis add_minus_cancel diff_le_eq le_diff_eq uminus_add_conv_diff) |
|
932 apply (metis abs_ge_zero linorder_linear min_max.sup_absorb1 min_max.sup_commute) |
805 apply (metis abs_ge_zero linorder_linear min_max.sup_absorb1 min_max.sup_commute) |
933 done |
806 done |
934 |
807 |
935 lemma bigo_lesso4: "f <o g =o O(k::'a=>'b::{linordered_field,number_ring}) ==> |
808 lemma bigo_lesso4: "f <o g =o O(k\<Colon>'a=>'b\<Colon>{linordered_field,number_ring}) \<Longrightarrow> |
936 g =o h +o O(k) ==> f <o h =o O(k)" |
809 g =o h +o O(k) \<Longrightarrow> f <o h =o O(k)" |
937 apply (unfold lesso_def) |
810 apply (unfold lesso_def) |
938 apply (drule set_plus_imp_minus) |
811 apply (drule set_plus_imp_minus) |
939 apply (drule bigo_abs5) back |
812 apply (drule bigo_abs5) back |
940 apply (simp add: fun_diff_def) |
813 apply (simp add: fun_diff_def) |
941 apply (drule bigo_useful_add) |
814 apply (drule bigo_useful_add) |