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.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.48 -  apply (subst diff_minus)+