src/HOL/Library/BigO.thy
changeset 54230 b1d955791529
parent 47445 69e96e5500df
child 54863 82acc20ded73
     1.1 --- a/src/HOL/Library/BigO.thy	Thu Oct 31 16:54:22 2013 +0100
     1.2 +++ b/src/HOL/Library/BigO.thy	Fri Nov 01 18:51:14 2013 +0100
     1.3 @@ -215,7 +215,7 @@
     1.4      f : lb +o O(g)"
     1.5    apply (rule set_minus_imp_plus)
     1.6    apply (rule bigo_bounded)
     1.7 -  apply (auto simp add: diff_minus fun_Compl_def func_plus)
     1.8 +  apply (auto simp add: fun_Compl_def func_plus)
     1.9    apply (drule_tac x = x in spec)+
    1.10    apply force
    1.11    apply (drule_tac x = x in spec)+
    1.12 @@ -390,7 +390,7 @@
    1.13    apply (rule set_minus_imp_plus)
    1.14    apply (drule set_plus_imp_minus)
    1.15    apply (drule bigo_minus)
    1.16 -  apply (simp add: diff_minus)
    1.17 +  apply simp
    1.18    done
    1.19  
    1.20  lemma bigo_minus3: "O(-f) = O(f)"
    1.21 @@ -446,7 +446,7 @@
    1.22    apply (rule bigo_minus)
    1.23    apply (subst set_minus_plus)
    1.24    apply assumption
    1.25 -  apply  (simp add: diff_minus add_ac)
    1.26 +  apply (simp add: add_ac)
    1.27    done
    1.28  
    1.29  lemma bigo_add_commute: "(f : g +o O(h)) = (g : f +o O(h))"
    1.30 @@ -545,10 +545,9 @@
    1.31  
    1.32  lemma bigo_compose2: "f =o g +o O(h) ==> (%x. f(k x)) =o (%x. g(k x)) +o 
    1.33      O(%x. h(k x))"
    1.34 -  apply (simp only: set_minus_plus [symmetric] diff_minus fun_Compl_def
    1.35 -      func_plus)
    1.36 -  apply (erule bigo_compose1)
    1.37 -done
    1.38 +  apply (simp only: set_minus_plus [symmetric] fun_Compl_def func_plus)
    1.39 +  apply (drule bigo_compose1) apply (simp add: fun_diff_def)
    1.40 +  done
    1.41  
    1.42  
    1.43  subsection {* Setsum *}
    1.44 @@ -779,7 +778,7 @@
    1.45    apply (subst abs_of_nonneg)
    1.46    apply (drule_tac x = x in spec) back
    1.47    apply (simp add: algebra_simps)
    1.48 -  apply (subst diff_minus)+
    1.49 +  apply (subst diff_conv_add_uminus)+
    1.50    apply (rule add_right_mono)
    1.51    apply (erule spec)
    1.52    apply (rule order_trans) 
    1.53 @@ -803,7 +802,7 @@
    1.54    apply (subst abs_of_nonneg)
    1.55    apply (drule_tac x = x in spec) back
    1.56    apply (simp add: algebra_simps)
    1.57 -  apply (subst diff_minus)+
    1.58 +  apply (subst diff_conv_add_uminus)+
    1.59    apply (rule add_left_mono)
    1.60    apply (rule le_imp_neg_le)
    1.61    apply (erule spec)