--- a/src/HOL/Library/BigO.thy Tue Feb 03 16:40:10 2009 +0100
+++ b/src/HOL/Library/BigO.thy Tue Feb 03 16:50:40 2009 +0100
@@ -1,12 +1,11 @@
(* Title: HOL/Library/BigO.thy
- ID: $Id$
Authors: Jeremy Avigad and Kevin Donnelly
*)
header {* Big O notation *}
theory BigO
-imports Plain "~~/src/HOL/Presburger" SetsAndFunctions
+imports Complex_Main SetsAndFunctions
begin
text {*
@@ -871,4 +870,38 @@
apply (auto split: split_max simp add: func_plus)
done
+lemma bigo_LIMSEQ1: "f =o O(g) ==> g ----> 0 ==> f ----> (0::real)"
+ apply (simp add: LIMSEQ_def bigo_alt_def)
+ apply clarify
+ apply (drule_tac x = "r / c" in spec)
+ apply (drule mp)
+ apply (erule divide_pos_pos)
+ apply assumption
+ apply clarify
+ apply (rule_tac x = no in exI)
+ apply (rule allI)
+ apply (drule_tac x = n in spec)+
+ apply (rule impI)
+ apply (drule mp)
+ apply assumption
+ apply (rule order_le_less_trans)
+ apply assumption
+ apply (rule order_less_le_trans)
+ apply (subgoal_tac "c * abs(g n) < c * (r / c)")
+ apply assumption
+ apply (erule mult_strict_left_mono)
+ apply assumption
+ apply simp
+done
+
+lemma bigo_LIMSEQ2: "f =o g +o O(h) ==> h ----> 0 ==> f ----> a
+ ==> g ----> (a::real)"
+ apply (drule set_plus_imp_minus)
+ apply (drule bigo_LIMSEQ1)
+ apply assumption
+ apply (simp only: fun_diff_def)
+ apply (erule LIMSEQ_diff_approach_zero2)
+ apply assumption
+done
+
end
--- a/src/HOL/ex/BigO_Complex.thy Tue Feb 03 16:40:10 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,50 +0,0 @@
-(* Title: HOL/Complex/ex/BigO_Complex.thy
- ID: $Id$
- Authors: Jeremy Avigad and Kevin Donnelly
-*)
-
-header {* Big O notation -- continued *}
-
-theory BigO_Complex
-imports BigO Complex
-begin
-
-text {*
- Additional lemmas that require the \texttt{HOL-Complex} logic image.
-*}
-
-lemma bigo_LIMSEQ1: "f =o O(g) ==> g ----> 0 ==> f ----> (0::real)"
- apply (simp add: LIMSEQ_def bigo_alt_def)
- apply clarify
- apply (drule_tac x = "r / c" in spec)
- apply (drule mp)
- apply (erule divide_pos_pos)
- apply assumption
- apply clarify
- apply (rule_tac x = no in exI)
- apply (rule allI)
- apply (drule_tac x = n in spec)+
- apply (rule impI)
- apply (drule mp)
- apply assumption
- apply (rule order_le_less_trans)
- apply assumption
- apply (rule order_less_le_trans)
- apply (subgoal_tac "c * abs(g n) < c * (r / c)")
- apply assumption
- apply (erule mult_strict_left_mono)
- apply assumption
- apply simp
-done
-
-lemma bigo_LIMSEQ2: "f =o g +o O(h) ==> h ----> 0 ==> f ----> a
- ==> g ----> (a::real)"
- apply (drule set_plus_imp_minus)
- apply (drule bigo_LIMSEQ1)
- apply assumption
- apply (simp only: fun_diff_def)
- apply (erule LIMSEQ_diff_approach_zero2)
- apply assumption
-done
-
-end