src/HOL/Library/BigO.thy
changeset 47108 2a1953f0d20d
parent 45270 d5b5c9259afd
child 47445 69e96e5500df
     1.1 --- a/src/HOL/Library/BigO.thy	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Library/BigO.thy	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -132,7 +132,6 @@
     1.4    apply (simp add: abs_triangle_ineq)
     1.5    apply (simp add: order_less_le)
     1.6    apply (rule mult_nonneg_nonneg)
     1.7 -  apply (rule add_nonneg_nonneg)
     1.8    apply auto
     1.9    apply (rule_tac x = "%n. if (abs (f n)) <  abs (g n) then x n else 0" 
    1.10       in exI)
    1.11 @@ -150,11 +149,8 @@
    1.12    apply (rule abs_triangle_ineq)
    1.13    apply (simp add: order_less_le)
    1.14    apply (rule mult_nonneg_nonneg)
    1.15 -  apply (rule add_nonneg_nonneg)
    1.16 -  apply (erule order_less_imp_le)+
    1.17 +  apply (erule order_less_imp_le)
    1.18    apply simp
    1.19 -  apply (rule ext)
    1.20 -  apply (auto simp add: if_splits linorder_not_le)
    1.21    done
    1.22  
    1.23  lemma bigo_plus_subset2 [intro]: "A <= O(f) ==> B <= O(f) ==> A \<oplus> B <= O(f)"