97 apply (rule ext) |
97 apply (rule ext) |
98 apply auto |
98 apply auto |
99 done |
99 done |
100 |
100 |
101 lemma bigo_plus_self_subset [intro]: |
101 lemma bigo_plus_self_subset [intro]: |
102 "O(f) + O(f) <= O(f)" |
102 "O(f) \<oplus> O(f) <= O(f)" |
103 apply (auto simp add: bigo_alt_def set_plus) |
103 apply (auto simp add: bigo_alt_def set_plus_def) |
104 apply (rule_tac x = "c + ca" in exI) |
104 apply (rule_tac x = "c + ca" in exI) |
105 apply auto |
105 apply auto |
106 apply (simp add: ring_distribs func_plus) |
106 apply (simp add: ring_distribs func_plus) |
107 apply (rule order_trans) |
107 apply (rule order_trans) |
108 apply (rule abs_triangle_ineq) |
108 apply (rule abs_triangle_ineq) |
109 apply (rule add_mono) |
109 apply (rule add_mono) |
110 apply force |
110 apply force |
111 apply force |
111 apply force |
112 done |
112 done |
113 |
113 |
114 lemma bigo_plus_idemp [simp]: "O(f) + O(f) = O(f)" |
114 lemma bigo_plus_idemp [simp]: "O(f) \<oplus> O(f) = O(f)" |
115 apply (rule equalityI) |
115 apply (rule equalityI) |
116 apply (rule bigo_plus_self_subset) |
116 apply (rule bigo_plus_self_subset) |
117 apply (rule set_zero_plus2) |
117 apply (rule set_zero_plus2) |
118 apply (rule bigo_zero) |
118 apply (rule bigo_zero) |
119 done |
119 done |
120 |
120 |
121 lemma bigo_plus_subset [intro]: "O(f + g) <= O(f) + O(g)" |
121 lemma bigo_plus_subset [intro]: "O(f + g) <= O(f) \<oplus> O(g)" |
122 apply (rule subsetI) |
122 apply (rule subsetI) |
123 apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus) |
123 apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus_def) |
124 apply (subst bigo_pos_const [symmetric])+ |
124 apply (subst bigo_pos_const [symmetric])+ |
125 apply (rule_tac x = |
125 apply (rule_tac x = |
126 "%n. if abs (g n) <= (abs (f n)) then x n else 0" in exI) |
126 "%n. if abs (g n) <= (abs (f n)) then x n else 0" in exI) |
127 apply (rule conjI) |
127 apply (rule conjI) |
128 apply (rule_tac x = "c + c" in exI) |
128 apply (rule_tac x = "c + c" in exI) |
168 apply simp |
168 apply simp |
169 apply (rule ext) |
169 apply (rule ext) |
170 apply (auto simp add: if_splits linorder_not_le) |
170 apply (auto simp add: if_splits linorder_not_le) |
171 done |
171 done |
172 |
172 |
173 lemma bigo_plus_subset2 [intro]: "A <= O(f) ==> B <= O(f) ==> A + B <= O(f)" |
173 lemma bigo_plus_subset2 [intro]: "A <= O(f) ==> B <= O(f) ==> A \<oplus> B <= O(f)" |
174 apply (subgoal_tac "A + B <= O(f) + O(f)") |
174 apply (subgoal_tac "A \<oplus> B <= O(f) \<oplus> O(f)") |
175 apply (erule order_trans) |
175 apply (erule order_trans) |
176 apply simp |
176 apply simp |
177 apply (auto del: subsetI simp del: bigo_plus_idemp) |
177 apply (auto del: subsetI simp del: bigo_plus_idemp) |
178 done |
178 done |
179 |
179 |
180 lemma bigo_plus_eq: "ALL x. 0 <= f x ==> ALL x. 0 <= g x ==> |
180 lemma bigo_plus_eq: "ALL x. 0 <= f x ==> ALL x. 0 <= g x ==> |
181 O(f + g) = O(f) + O(g)" |
181 O(f + g) = O(f) \<oplus> O(g)" |
182 apply (rule equalityI) |
182 apply (rule equalityI) |
183 apply (rule bigo_plus_subset) |
183 apply (rule bigo_plus_subset) |
184 apply (simp add: bigo_alt_def set_plus func_plus) |
184 apply (simp add: bigo_alt_def set_plus_def func_plus) |
185 apply clarify |
185 apply clarify |
186 apply (rule_tac x = "max c ca" in exI) |
186 apply (rule_tac x = "max c ca" in exI) |
187 apply (rule conjI) |
187 apply (rule conjI) |
188 apply (subgoal_tac "c <= max c ca") |
188 apply (subgoal_tac "c <= max c ca") |
189 apply (erule order_less_le_trans) |
189 apply (erule order_less_le_trans) |
263 |
263 |
264 lemma bigo_abs4: "f =o g +o O(h) ==> |
264 lemma bigo_abs4: "f =o g +o O(h) ==> |
265 (%x. abs (f x)) =o (%x. abs (g x)) +o O(h)" |
265 (%x. abs (f x)) =o (%x. abs (g x)) +o O(h)" |
266 apply (drule set_plus_imp_minus) |
266 apply (drule set_plus_imp_minus) |
267 apply (rule set_minus_imp_plus) |
267 apply (rule set_minus_imp_plus) |
268 apply (subst func_diff) |
268 apply (subst fun_diff_def) |
269 proof - |
269 proof - |
270 assume a: "f - g : O(h)" |
270 assume a: "f - g : O(h)" |
271 have "(%x. abs (f x) - abs (g x)) =o O(%x. abs(abs (f x) - abs (g x)))" |
271 have "(%x. abs (f x) - abs (g x)) =o O(%x. abs(abs (f x) - abs (g x)))" |
272 by (rule bigo_abs2) |
272 by (rule bigo_abs2) |
273 also have "... <= O(%x. abs (f x - g x))" |
273 also have "... <= O(%x. abs (f x - g x))" |
277 apply (rule allI) |
277 apply (rule allI) |
278 apply (rule abs_triangle_ineq3) |
278 apply (rule abs_triangle_ineq3) |
279 done |
279 done |
280 also have "... <= O(f - g)" |
280 also have "... <= O(f - g)" |
281 apply (rule bigo_elt_subset) |
281 apply (rule bigo_elt_subset) |
282 apply (subst func_diff) |
282 apply (subst fun_diff_def) |
283 apply (rule bigo_abs) |
283 apply (rule bigo_abs) |
284 done |
284 done |
285 also from a have "... <= O(h)" |
285 also from a have "... <= O(h)" |
286 by (rule bigo_elt_subset) |
286 by (rule bigo_elt_subset) |
287 finally show "(%x. abs (f x) - abs (g x)) : O(h)". |
287 finally show "(%x. abs (f x) - abs (g x)) : O(h)". |
288 qed |
288 qed |
289 |
289 |
290 lemma bigo_abs5: "f =o O(g) ==> (%x. abs(f x)) =o O(g)" |
290 lemma bigo_abs5: "f =o O(g) ==> (%x. abs(f x)) =o O(g)" |
291 by (unfold bigo_def, auto) |
291 by (unfold bigo_def, auto) |
292 |
292 |
293 lemma bigo_elt_subset2 [intro]: "f : g +o O(h) ==> O(f) <= O(g) + O(h)" |
293 lemma bigo_elt_subset2 [intro]: "f : g +o O(h) ==> O(f) <= O(g) \<oplus> O(h)" |
294 proof - |
294 proof - |
295 assume "f : g +o O(h)" |
295 assume "f : g +o O(h)" |
296 also have "... <= O(g) + O(h)" |
296 also have "... <= O(g) \<oplus> O(h)" |
297 by (auto del: subsetI) |
297 by (auto del: subsetI) |
298 also have "... = O(%x. abs(g x)) + O(%x. abs(h x))" |
298 also have "... = O(%x. abs(g x)) \<oplus> O(%x. abs(h x))" |
299 apply (subst bigo_abs3 [symmetric])+ |
299 apply (subst bigo_abs3 [symmetric])+ |
300 apply (rule refl) |
300 apply (rule refl) |
301 done |
301 done |
302 also have "... = O((%x. abs(g x)) + (%x. abs(h x)))" |
302 also have "... = O((%x. abs(g x)) + (%x. abs(h x)))" |
303 by (rule bigo_plus_eq [symmetric], auto) |
303 by (rule bigo_plus_eq [symmetric], auto) |
304 finally have "f : ...". |
304 finally have "f : ...". |
305 then have "O(f) <= ..." |
305 then have "O(f) <= ..." |
306 by (elim bigo_elt_subset) |
306 by (elim bigo_elt_subset) |
307 also have "... = O(%x. abs(g x)) + O(%x. abs(h x))" |
307 also have "... = O(%x. abs(g x)) \<oplus> O(%x. abs(h x))" |
308 by (rule bigo_plus_eq, auto) |
308 by (rule bigo_plus_eq, auto) |
309 finally show ?thesis |
309 finally show ?thesis |
310 by (simp add: bigo_abs3 [symmetric]) |
310 by (simp add: bigo_abs3 [symmetric]) |
311 qed |
311 qed |
312 |
312 |
313 lemma bigo_mult [intro]: "O(f)*O(g) <= O(f * g)" |
313 lemma bigo_mult [intro]: "O(f)\<otimes>O(g) <= O(f * g)" |
314 apply (rule subsetI) |
314 apply (rule subsetI) |
315 apply (subst bigo_def) |
315 apply (subst bigo_def) |
316 apply (auto simp add: bigo_alt_def set_times func_times) |
316 apply (auto simp add: bigo_alt_def set_times_def func_times) |
317 apply (rule_tac x = "c * ca" in exI) |
317 apply (rule_tac x = "c * ca" in exI) |
318 apply(rule allI) |
318 apply(rule allI) |
319 apply(erule_tac x = x in allE)+ |
319 apply(erule_tac x = x in allE)+ |
320 apply(subgoal_tac "c * ca * abs(f x * g x) = |
320 apply(subgoal_tac "c * ca * abs(f x * g x) = |
321 (c * abs(f x)) * (ca * abs(g x))") |
321 (c * abs(f x)) * (ca * abs(g x))") |
387 apply (erule bigo_mult5) |
387 apply (erule bigo_mult5) |
388 apply (rule bigo_mult2) |
388 apply (rule bigo_mult2) |
389 done |
389 done |
390 |
390 |
391 lemma bigo_mult7: "ALL x. f x ~= 0 ==> |
391 lemma bigo_mult7: "ALL x. f x ~= 0 ==> |
392 O(f * g) <= O(f::'a => ('b::ordered_field)) * O(g)" |
392 O(f * g) <= O(f::'a => ('b::ordered_field)) \<otimes> O(g)" |
393 apply (subst bigo_mult6) |
393 apply (subst bigo_mult6) |
394 apply assumption |
394 apply assumption |
395 apply (rule set_times_mono3) |
395 apply (rule set_times_mono3) |
396 apply (rule bigo_refl) |
396 apply (rule bigo_refl) |
397 done |
397 done |
398 |
398 |
399 lemma bigo_mult8: "ALL x. f x ~= 0 ==> |
399 lemma bigo_mult8: "ALL x. f x ~= 0 ==> |
400 O(f * g) = O(f::'a => ('b::ordered_field)) * O(g)" |
400 O(f * g) = O(f::'a => ('b::ordered_field)) \<otimes> O(g)" |
401 apply (rule equalityI) |
401 apply (rule equalityI) |
402 apply (erule bigo_mult7) |
402 apply (erule bigo_mult7) |
403 apply (rule bigo_mult) |
403 apply (rule bigo_mult) |
404 done |
404 done |
405 |
405 |
406 lemma bigo_minus [intro]: "f : O(g) ==> - f : O(g)" |
406 lemma bigo_minus [intro]: "f : O(g) ==> - f : O(g)" |
407 by (auto simp add: bigo_def func_minus) |
407 by (auto simp add: bigo_def fun_Compl_def) |
408 |
408 |
409 lemma bigo_minus2: "f : g +o O(h) ==> -f : -g +o O(h)" |
409 lemma bigo_minus2: "f : g +o O(h) ==> -f : -g +o O(h)" |
410 apply (rule set_minus_imp_plus) |
410 apply (rule set_minus_imp_plus) |
411 apply (drule set_plus_imp_minus) |
411 apply (drule set_plus_imp_minus) |
412 apply (drule bigo_minus) |
412 apply (drule bigo_minus) |
413 apply (simp add: diff_minus) |
413 apply (simp add: diff_minus) |
414 done |
414 done |
415 |
415 |
416 lemma bigo_minus3: "O(-f) = O(f)" |
416 lemma bigo_minus3: "O(-f) = O(f)" |
417 by (auto simp add: bigo_def func_minus abs_minus_cancel) |
417 by (auto simp add: bigo_def fun_Compl_def abs_minus_cancel) |
418 |
418 |
419 lemma bigo_plus_absorb_lemma1: "f : O(g) ==> f +o O(g) <= O(g)" |
419 lemma bigo_plus_absorb_lemma1: "f : O(g) ==> f +o O(g) <= O(g)" |
420 proof - |
420 proof - |
421 assume a: "f : O(g)" |
421 assume a: "f : O(g)" |
422 show "f +o O(g) <= O(g)" |
422 show "f +o O(g) <= O(g)" |
423 proof - |
423 proof - |
424 have "f : O(f)" by auto |
424 have "f : O(f)" by auto |
425 then have "f +o O(g) <= O(f) + O(g)" |
425 then have "f +o O(g) <= O(f) \<oplus> O(g)" |
426 by (auto del: subsetI) |
426 by (auto del: subsetI) |
427 also have "... <= O(g) + O(g)" |
427 also have "... <= O(g) \<oplus> O(g)" |
428 proof - |
428 proof - |
429 from a have "O(f) <= O(g)" by (auto del: subsetI) |
429 from a have "O(f) <= O(g)" by (auto del: subsetI) |
430 thus ?thesis by (auto del: subsetI) |
430 thus ?thesis by (auto del: subsetI) |
431 qed |
431 qed |
432 also have "... <= O(g)" by (simp add: bigo_plus_idemp) |
432 also have "... <= O(g)" by (simp add: bigo_plus_idemp) |
633 lemma bigo_setsum4: "f =o g +o O(h) ==> |
633 lemma bigo_setsum4: "f =o g +o O(h) ==> |
634 (%x. SUM y : A x. l x y * f(k x y)) =o |
634 (%x. SUM y : A x. l x y * f(k x y)) =o |
635 (%x. SUM y : A x. l x y * g(k x y)) +o |
635 (%x. SUM y : A x. l x y * g(k x y)) +o |
636 O(%x. SUM y : A x. abs(l x y * h(k x y)))" |
636 O(%x. SUM y : A x. abs(l x y * h(k x y)))" |
637 apply (rule set_minus_imp_plus) |
637 apply (rule set_minus_imp_plus) |
638 apply (subst func_diff) |
638 apply (subst fun_diff_def) |
639 apply (subst setsum_subtractf [symmetric]) |
639 apply (subst setsum_subtractf [symmetric]) |
640 apply (subst right_diff_distrib [symmetric]) |
640 apply (subst right_diff_distrib [symmetric]) |
641 apply (rule bigo_setsum3) |
641 apply (rule bigo_setsum3) |
642 apply (subst func_diff [symmetric]) |
642 apply (subst fun_diff_def [symmetric]) |
643 apply (erule set_plus_imp_minus) |
643 apply (erule set_plus_imp_minus) |
644 done |
644 done |
645 |
645 |
646 lemma bigo_setsum5: "f =o O(h) ==> ALL x y. 0 <= l x y ==> |
646 lemma bigo_setsum5: "f =o O(h) ==> ALL x y. 0 <= l x y ==> |
647 ALL x. 0 <= h x ==> |
647 ALL x. 0 <= h x ==> |
662 ALL x. 0 <= h x ==> |
662 ALL x. 0 <= h x ==> |
663 (%x. SUM y : A x. (l x y) * f(k x y)) =o |
663 (%x. SUM y : A x. (l x y) * f(k x y)) =o |
664 (%x. SUM y : A x. (l x y) * g(k x y)) +o |
664 (%x. SUM y : A x. (l x y) * g(k x y)) +o |
665 O(%x. SUM y : A x. (l x y) * h(k x y))" |
665 O(%x. SUM y : A x. (l x y) * h(k x y))" |
666 apply (rule set_minus_imp_plus) |
666 apply (rule set_minus_imp_plus) |
667 apply (subst func_diff) |
667 apply (subst fun_diff_def) |
668 apply (subst setsum_subtractf [symmetric]) |
668 apply (subst setsum_subtractf [symmetric]) |
669 apply (subst right_diff_distrib [symmetric]) |
669 apply (subst right_diff_distrib [symmetric]) |
670 apply (rule bigo_setsum5) |
670 apply (rule bigo_setsum5) |
671 apply (subst func_diff [symmetric]) |
671 apply (subst fun_diff_def [symmetric]) |
672 apply (drule set_plus_imp_minus) |
672 apply (drule set_plus_imp_minus) |
673 apply auto |
673 apply auto |
674 done |
674 done |
675 |
675 |
676 |
676 |
677 subsection {* Misc useful stuff *} |
677 subsection {* Misc useful stuff *} |
678 |
678 |
679 lemma bigo_useful_intro: "A <= O(f) ==> B <= O(f) ==> |
679 lemma bigo_useful_intro: "A <= O(f) ==> B <= O(f) ==> |
680 A + B <= O(f)" |
680 A \<oplus> B <= O(f)" |
681 apply (subst bigo_plus_idemp [symmetric]) |
681 apply (subst bigo_plus_idemp [symmetric]) |
682 apply (rule set_plus_mono2) |
682 apply (rule set_plus_mono2) |
683 apply assumption+ |
683 apply assumption+ |
684 done |
684 done |
685 |
685 |
721 lemma bigo_fix2: |
721 lemma bigo_fix2: |
722 "(%x. f ((x::nat) + 1)) =o (%x. g(x + 1)) +o O(%x. h(x + 1)) ==> |
722 "(%x. f ((x::nat) + 1)) =o (%x. g(x + 1)) +o O(%x. h(x + 1)) ==> |
723 f 0 = g 0 ==> f =o g +o O(h)" |
723 f 0 = g 0 ==> f =o g +o O(h)" |
724 apply (rule set_minus_imp_plus) |
724 apply (rule set_minus_imp_plus) |
725 apply (rule bigo_fix) |
725 apply (rule bigo_fix) |
726 apply (subst func_diff) |
726 apply (subst fun_diff_def) |
727 apply (subst func_diff [symmetric]) |
727 apply (subst fun_diff_def [symmetric]) |
728 apply (rule set_plus_imp_minus) |
728 apply (rule set_plus_imp_minus) |
729 apply simp |
729 apply simp |
730 apply (simp add: func_diff) |
730 apply (simp add: fun_diff_def) |
731 done |
731 done |
732 |
732 |
733 |
733 |
734 subsection {* Less than or equal to *} |
734 subsection {* Less than or equal to *} |
735 |
735 |
792 apply (rule bigo_lesseq4) |
792 apply (rule bigo_lesseq4) |
793 apply (erule set_plus_imp_minus) |
793 apply (erule set_plus_imp_minus) |
794 apply (rule allI) |
794 apply (rule allI) |
795 apply (rule le_maxI2) |
795 apply (rule le_maxI2) |
796 apply (rule allI) |
796 apply (rule allI) |
797 apply (subst func_diff) |
797 apply (subst fun_diff_def) |
798 apply (case_tac "0 <= k x - g x") |
798 apply (case_tac "0 <= k x - g x") |
799 apply simp |
799 apply simp |
800 apply (subst abs_of_nonneg) |
800 apply (subst abs_of_nonneg) |
801 apply (drule_tac x = x in spec) back |
801 apply (drule_tac x = x in spec) back |
802 apply (simp add: compare_rls) |
802 apply (simp add: compare_rls) |
816 apply (rule bigo_lesseq4) |
816 apply (rule bigo_lesseq4) |
817 apply (erule set_plus_imp_minus) |
817 apply (erule set_plus_imp_minus) |
818 apply (rule allI) |
818 apply (rule allI) |
819 apply (rule le_maxI2) |
819 apply (rule le_maxI2) |
820 apply (rule allI) |
820 apply (rule allI) |
821 apply (subst func_diff) |
821 apply (subst fun_diff_def) |
822 apply (case_tac "0 <= f x - k x") |
822 apply (case_tac "0 <= f x - k x") |
823 apply simp |
823 apply simp |
824 apply (subst abs_of_nonneg) |
824 apply (subst abs_of_nonneg) |
825 apply (drule_tac x = x in spec) back |
825 apply (drule_tac x = x in spec) back |
826 apply (simp add: compare_rls) |
826 apply (simp add: compare_rls) |
837 lemma bigo_lesso4: "f <o g =o O(k::'a=>'b::ordered_field) ==> |
837 lemma bigo_lesso4: "f <o g =o O(k::'a=>'b::ordered_field) ==> |
838 g =o h +o O(k) ==> f <o h =o O(k)" |
838 g =o h +o O(k) ==> f <o h =o O(k)" |
839 apply (unfold lesso_def) |
839 apply (unfold lesso_def) |
840 apply (drule set_plus_imp_minus) |
840 apply (drule set_plus_imp_minus) |
841 apply (drule bigo_abs5) back |
841 apply (drule bigo_abs5) back |
842 apply (simp add: func_diff) |
842 apply (simp add: fun_diff_def) |
843 apply (drule bigo_useful_add) |
843 apply (drule bigo_useful_add) |
844 apply assumption |
844 apply assumption |
845 apply (erule bigo_lesseq2) back |
845 apply (erule bigo_lesseq2) back |
846 apply (rule allI) |
846 apply (rule allI) |
847 apply (auto simp add: func_plus func_diff compare_rls |
847 apply (auto simp add: func_plus fun_diff_def compare_rls |
848 split: split_max abs_split) |
848 split: split_max abs_split) |
849 done |
849 done |
850 |
850 |
851 lemma bigo_lesso5: "f <o g =o O(h) ==> |
851 lemma bigo_lesso5: "f <o g =o O(h) ==> |
852 EX C. ALL x. f x <= g x + C * abs(h x)" |
852 EX C. ALL x. f x <= g x + C * abs(h x)" |