1.1 --- a/src/HOL/Library/BigO.thy	Tue Feb 03 16:40:10 2009 +0100
     1.2 +++ b/src/HOL/Library/BigO.thy	Tue Feb 03 16:50:40 2009 +0100
     1.3 @@ -1,12 +1,11 @@
     1.4  (*  Title:      HOL/Library/BigO.thy
     1.5 -    ID:		$Id$
     1.6      Authors:    Jeremy Avigad and Kevin Donnelly
     1.7  *)
     1.8  
     1.9  header {* Big O notation *}
    1.10  
    1.11  theory BigO
    1.12 -imports Plain "~~/src/HOL/Presburger" SetsAndFunctions
    1.13 +imports Complex_Main SetsAndFunctions
    1.14  begin
    1.15  
    1.16  text {*
    1.17 @@ -871,4 +870,38 @@
    1.18    apply (auto split: split_max simp add: func_plus)
    1.19    done
    1.20  
    1.21 +lemma bigo_LIMSEQ1: "f =o O(g) ==> g ----> 0 ==> f ----> (0::real)"
    1.22 +  apply (simp add: LIMSEQ_def bigo_alt_def)
    1.23 +  apply clarify
    1.24 +  apply (drule_tac x = "r / c" in spec)
    1.25 +  apply (drule mp)
    1.26 +  apply (erule divide_pos_pos)
    1.27 +  apply assumption
    1.28 +  apply clarify
    1.29 +  apply (rule_tac x = no in exI)
    1.30 +  apply (rule allI)
    1.31 +  apply (drule_tac x = n in spec)+
    1.32 +  apply (rule impI)
    1.33 +  apply (drule mp)
    1.34 +  apply assumption
    1.35 +  apply (rule order_le_less_trans)
    1.36 +  apply assumption
    1.37 +  apply (rule order_less_le_trans)
    1.38 +  apply (subgoal_tac "c * abs(g n) < c * (r / c)")
    1.39 +  apply assumption
    1.40 +  apply (erule mult_strict_left_mono)
    1.41 +  apply assumption
    1.42 +  apply simp
    1.43 +done
    1.44 +
    1.45 +lemma bigo_LIMSEQ2: "f =o g +o O(h) ==> h ----> 0 ==> f ----> a 
    1.46 +    ==> g ----> (a::real)"
    1.47 +  apply (drule set_plus_imp_minus)
    1.48 +  apply (drule bigo_LIMSEQ1)
    1.49 +  apply assumption
    1.50 +  apply (simp only: fun_diff_def)
    1.51 +  apply (erule LIMSEQ_diff_approach_zero2)
    1.52 +  apply assumption
    1.53 +done
    1.54 +
    1.55  end