src/HOL/Library/BigO.thy
changeset 57514 bdc2c6b40bf2
parent 57512 cc97b347b301
child 58622 aa99568f56de
     1.1 --- a/src/HOL/Library/BigO.thy	Sat Jul 05 10:09:01 2014 +0200
     1.2 +++ b/src/HOL/Library/BigO.thy	Sat Jul 05 11:01:53 2014 +0200
     1.3 @@ -67,7 +67,7 @@
     1.4    apply (drule_tac x = "xa" in spec)+
     1.5    apply (subgoal_tac "ca * abs (f xa) \<le> ca * (c * abs (g xa))")
     1.6    apply (erule order_trans)
     1.7 -  apply (simp add: mult_ac)
     1.8 +  apply (simp add: ac_simps)
     1.9    apply (rule mult_left_mono, assumption)
    1.10    apply (rule order_less_imp_le, assumption)
    1.11    done
    1.12 @@ -287,7 +287,7 @@
    1.13    apply (rule mult_mono)
    1.14    apply assumption+
    1.15    apply auto
    1.16 -  apply (simp add: mult_ac abs_mult)
    1.17 +  apply (simp add: ac_simps abs_mult)
    1.18    done
    1.19  
    1.20  lemma bigo_mult2 [intro]: "f *o O(g) \<subseteq> O(f * g)"
    1.21 @@ -296,7 +296,7 @@
    1.22    apply auto
    1.23    apply (drule_tac x = x in spec)
    1.24    apply (subgoal_tac "abs (f x) * abs (b x) \<le> abs (f x) * (c * abs (g x))")
    1.25 -  apply (force simp add: mult_ac)
    1.26 +  apply (force simp add: ac_simps)
    1.27    apply (rule mult_left_mono, assumption)
    1.28    apply (rule abs_ge_zero)
    1.29    done
    1.30 @@ -328,7 +328,7 @@
    1.31    also have "(\<lambda>x. 1 / f x) * (f * g) = g"
    1.32      apply (simp add: func_times)
    1.33      apply (rule ext)
    1.34 -    apply (simp add: assms nonzero_divide_eq_eq mult_ac)
    1.35 +    apply (simp add: assms nonzero_divide_eq_eq ac_simps)
    1.36      done
    1.37    finally have "(\<lambda>x. (1::'b) / f x) * h \<in> O(g)" .
    1.38    then have "f * ((\<lambda>x. (1::'b) / f x) * h) \<in> f *o O(g)"
    1.39 @@ -336,7 +336,7 @@
    1.40    also have "f * ((\<lambda>x. (1::'b) / f x) * h) = h"
    1.41      apply (simp add: func_times)
    1.42      apply (rule ext)
    1.43 -    apply (simp add: assms nonzero_divide_eq_eq mult_ac)
    1.44 +    apply (simp add: assms nonzero_divide_eq_eq ac_simps)
    1.45      done
    1.46    finally show "h \<in> f *o O(g)" .
    1.47  qed
    1.48 @@ -432,7 +432,7 @@
    1.49    apply (rule bigo_minus)
    1.50    apply (subst set_minus_plus)
    1.51    apply assumption
    1.52 -  apply (simp add: add_ac)
    1.53 +  apply (simp add: ac_simps)
    1.54    done
    1.55  
    1.56  lemma bigo_add_commute: "f \<in> g +o O(h) \<longleftrightarrow> g \<in> f +o O(h)"
    1.57 @@ -441,7 +441,7 @@
    1.58    done
    1.59  
    1.60  lemma bigo_const1: "(\<lambda>x. c) \<in> O(\<lambda>x. 1)"
    1.61 -  by (auto simp add: bigo_def mult_ac)
    1.62 +  by (auto simp add: bigo_def ac_simps)
    1.63  
    1.64  lemma bigo_const2 [intro]: "O(\<lambda>x. c) \<subseteq> O(\<lambda>x. 1)"
    1.65    apply (rule bigo_elt_subset)
    1.66 @@ -536,7 +536,7 @@
    1.67    apply (rule mult_left_mono)
    1.68    apply (erule spec)
    1.69    apply simp
    1.70 -  apply(simp add: mult_ac)
    1.71 +  apply(simp add: ac_simps)
    1.72    done
    1.73  
    1.74  lemma bigo_const_mult7 [intro]: "f =o O(g) \<Longrightarrow> (\<lambda>x. c * f x) =o O(g)"