equal
deleted
inserted
replaced
1 (* Title: HOL/Library/BigO.thy |
1 (* Title: HOL/Library/BigO.thy |
2 ID: $Id$ |
|
3 Authors: Jeremy Avigad and Kevin Donnelly |
2 Authors: Jeremy Avigad and Kevin Donnelly |
4 *) |
3 *) |
5 |
4 |
6 header {* Big O notation *} |
5 header {* Big O notation *} |
7 |
6 |
8 theory BigO |
7 theory BigO |
9 imports Plain "~~/src/HOL/Presburger" SetsAndFunctions |
8 imports Complex_Main SetsAndFunctions |
10 begin |
9 begin |
11 |
10 |
12 text {* |
11 text {* |
13 This library is designed to support asymptotic ``big O'' calculations, |
12 This library is designed to support asymptotic ``big O'' calculations, |
14 i.e.~reasoning with expressions of the form $f = O(g)$ and $f = g + |
13 i.e.~reasoning with expressions of the form $f = O(g)$ and $f = g + |
869 apply assumption |
868 apply assumption |
870 apply (force split: split_max) |
869 apply (force split: split_max) |
871 apply (auto split: split_max simp add: func_plus) |
870 apply (auto split: split_max simp add: func_plus) |
872 done |
871 done |
873 |
872 |
|
873 lemma bigo_LIMSEQ1: "f =o O(g) ==> g ----> 0 ==> f ----> (0::real)" |
|
874 apply (simp add: LIMSEQ_def bigo_alt_def) |
|
875 apply clarify |
|
876 apply (drule_tac x = "r / c" in spec) |
|
877 apply (drule mp) |
|
878 apply (erule divide_pos_pos) |
|
879 apply assumption |
|
880 apply clarify |
|
881 apply (rule_tac x = no in exI) |
|
882 apply (rule allI) |
|
883 apply (drule_tac x = n in spec)+ |
|
884 apply (rule impI) |
|
885 apply (drule mp) |
|
886 apply assumption |
|
887 apply (rule order_le_less_trans) |
|
888 apply assumption |
|
889 apply (rule order_less_le_trans) |
|
890 apply (subgoal_tac "c * abs(g n) < c * (r / c)") |
|
891 apply assumption |
|
892 apply (erule mult_strict_left_mono) |
|
893 apply assumption |
|
894 apply simp |
|
895 done |
|
896 |
|
897 lemma bigo_LIMSEQ2: "f =o g +o O(h) ==> h ----> 0 ==> f ----> a |
|
898 ==> g ----> (a::real)" |
|
899 apply (drule set_plus_imp_minus) |
|
900 apply (drule bigo_LIMSEQ1) |
|
901 apply assumption |
|
902 apply (simp only: fun_diff_def) |
|
903 apply (erule LIMSEQ_diff_approach_zero2) |
|
904 apply assumption |
|
905 done |
|
906 |
874 end |
907 end |