merged Big0
authorhaftmann
Tue Feb 03 16:50:40 2009 +0100 (2009-02-03)
changeset 2978684a3f86441eb
parent 29783 dce05b909056
child 29787 23bf900a21db
merged Big0
src/HOL/Library/BigO.thy
src/HOL/ex/BigO_Complex.thy
     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
     2.1 --- a/src/HOL/ex/BigO_Complex.thy	Tue Feb 03 16:40:10 2009 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,50 +0,0 @@
     2.4 -(*  Title:      HOL/Complex/ex/BigO_Complex.thy
     2.5 -    ID:		$Id$
     2.6 -    Authors:    Jeremy Avigad and Kevin Donnelly
     2.7 -*)
     2.8 -
     2.9 -header {* Big O notation -- continued *}
    2.10 -
    2.11 -theory BigO_Complex
    2.12 -imports BigO Complex
    2.13 -begin
    2.14 -
    2.15 -text {*
    2.16 -  Additional lemmas that require the \texttt{HOL-Complex} logic image.
    2.17 -*}
    2.18 -
    2.19 -lemma bigo_LIMSEQ1: "f =o O(g) ==> g ----> 0 ==> f ----> (0::real)"
    2.20 -  apply (simp add: LIMSEQ_def bigo_alt_def)
    2.21 -  apply clarify
    2.22 -  apply (drule_tac x = "r / c" in spec)
    2.23 -  apply (drule mp)
    2.24 -  apply (erule divide_pos_pos)
    2.25 -  apply assumption
    2.26 -  apply clarify
    2.27 -  apply (rule_tac x = no in exI)
    2.28 -  apply (rule allI)
    2.29 -  apply (drule_tac x = n in spec)+
    2.30 -  apply (rule impI)
    2.31 -  apply (drule mp)
    2.32 -  apply assumption
    2.33 -  apply (rule order_le_less_trans)
    2.34 -  apply assumption
    2.35 -  apply (rule order_less_le_trans)
    2.36 -  apply (subgoal_tac "c * abs(g n) < c * (r / c)")
    2.37 -  apply assumption
    2.38 -  apply (erule mult_strict_left_mono)
    2.39 -  apply assumption
    2.40 -  apply simp
    2.41 -done
    2.42 -
    2.43 -lemma bigo_LIMSEQ2: "f =o g +o O(h) ==> h ----> 0 ==> f ----> a 
    2.44 -    ==> g ----> (a::real)"
    2.45 -  apply (drule set_plus_imp_minus)
    2.46 -  apply (drule bigo_LIMSEQ1)
    2.47 -  apply assumption
    2.48 -  apply (simp only: fun_diff_def)
    2.49 -  apply (erule LIMSEQ_diff_approach_zero2)
    2.50 -  apply assumption
    2.51 -done
    2.52 -
    2.53 -end