# HG changeset patch
# User haftmann
# Date 1233676240 -3600
# Node ID 84a3f86441ebcd4293052bba909dc075e969fdb9
# Parent  dce05b909056f776d78197258f25dd7de5e37b52
merged Big0

diff -r dce05b909056 -r 84a3f86441eb src/HOL/Library/BigO.thy
--- 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
diff -r dce05b909056 -r 84a3f86441eb src/HOL/ex/BigO_Complex.thy
--- 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