src/HOL/Library/BigO.thy
changeset 23477 f4b83f03cac9
parent 23413 5caa2710dd5b
child 25592 e8ddaf6bf5df
     1.1 --- a/src/HOL/Library/BigO.thy	Fri Jun 22 22:41:17 2007 +0200
     1.2 +++ b/src/HOL/Library/BigO.thy	Sat Jun 23 19:33:22 2007 +0200
     1.3 @@ -103,7 +103,7 @@
     1.4    apply (auto simp add: bigo_alt_def set_plus)
     1.5    apply (rule_tac x = "c + ca" in exI)
     1.6    apply auto
     1.7 -  apply (simp add: ring_distrib func_plus)
     1.8 +  apply (simp add: ring_distribs func_plus)
     1.9    apply (rule order_trans)
    1.10    apply (rule abs_triangle_ineq)
    1.11    apply (rule add_mono)
    1.12 @@ -134,7 +134,7 @@
    1.13    apply (simp)
    1.14    apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
    1.15    apply (erule order_trans)
    1.16 -  apply (simp add: ring_distrib)
    1.17 +  apply (simp add: ring_distribs)
    1.18    apply (rule mult_left_mono)
    1.19    apply assumption
    1.20    apply (simp add: order_less_le)
    1.21 @@ -155,7 +155,7 @@
    1.22    apply (simp)
    1.23    apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
    1.24    apply (erule order_trans)
    1.25 -  apply (simp add: ring_distrib)
    1.26 +  apply (simp add: ring_distribs)
    1.27    apply (rule mult_left_mono)
    1.28    apply (simp add: order_less_le)
    1.29    apply (simp add: order_less_le)
    1.30 @@ -192,7 +192,7 @@
    1.31    apply clarify
    1.32    apply (drule_tac x = "xa" in spec)+
    1.33    apply (subgoal_tac "0 <= f xa + g xa")
    1.34 -  apply (simp add: ring_distrib)
    1.35 +  apply (simp add: ring_distribs)
    1.36    apply (subgoal_tac "abs(a xa + b xa) <= abs(a xa) + abs(b xa)")
    1.37    apply (subgoal_tac "abs(a xa) + abs(b xa) <= 
    1.38        max c ca * f xa + max c ca * g xa")
    1.39 @@ -349,7 +349,7 @@
    1.40    apply (drule set_plus_imp_minus)
    1.41    apply (rule set_minus_imp_plus)
    1.42    apply (drule bigo_mult3 [where g = g and j = g])
    1.43 -  apply (auto simp add: ring_eq_simps mult_ac)
    1.44 +  apply (auto simp add: ring_simps)
    1.45    done
    1.46  
    1.47  lemma bigo_mult5: "ALL x. f x ~= 0 ==>