prefer ac_simps collections over separate name bindings for add and mult
authorhaftmann
Sat Jul 05 11:01:53 2014 +0200 (2014-07-05)
changeset 57514bdc2c6b40bf2
parent 57513 55b2afc5ddfc
child 57515 adfb932486df
prefer ac_simps collections over separate name bindings for add and mult
src/Doc/How_to_Prove_it/How_to_Prove_it.thy
src/Doc/Tutorial/Types/Numbers.thy
src/Doc/Tutorial/document/numerics.tex
src/HOL/Algebra/IntRing.thy
src/HOL/Decision_Procs/Cooper.thy
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Decision_Procs/Polynomial_List.thy
src/HOL/Decision_Procs/cooper_tac.ML
src/HOL/Decision_Procs/mir_tac.ML
src/HOL/Deriv.thy
src/HOL/Divides.thy
src/HOL/Fact.thy
src/HOL/Fields.thy
src/HOL/GCD.thy
src/HOL/Groups.thy
src/HOL/Int.thy
src/HOL/Library/BigO.thy
src/HOL/Library/Discrete.thy
src/HOL/Library/Extended_Nat.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/Fraction_Field.thy
src/HOL/Library/Fundamental_Theorem_Algebra.thy
src/HOL/Library/Inner_Product.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Numeral_Type.thy
src/HOL/Library/RBT_Set.thy
src/HOL/Library/Set_Algebras.thy
src/HOL/List.thy
src/HOL/MacLaurin.thy
src/HOL/Metis_Examples/Big_O.thy
src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
src/HOL/Multivariate_Analysis/Determinants.thy
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
src/HOL/Multivariate_Analysis/PolyRoots.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/NSA/CLim.thy
src/HOL/NSA/HDeriv.thy
src/HOL/NSA/HTranscendental.thy
src/HOL/NSA/NSA.thy
src/HOL/Nat.thy
src/HOL/NthRoot.thy
src/HOL/Number_Theory/Binomial.thy
src/HOL/Number_Theory/MiscAlgebra.thy
src/HOL/Number_Theory/Pocklington.thy
src/HOL/Number_Theory/Residues.thy
src/HOL/Old_Number_Theory/Chinese.thy
src/HOL/Old_Number_Theory/Euler.thy
src/HOL/Old_Number_Theory/EulerFermat.thy
src/HOL/Old_Number_Theory/Factorization.thy
src/HOL/Old_Number_Theory/Int2.thy
src/HOL/Old_Number_Theory/IntPrimes.thy
src/HOL/Old_Number_Theory/Legacy_GCD.thy
src/HOL/Old_Number_Theory/Pocklington.thy
src/HOL/Old_Number_Theory/Primes.thy
src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
src/HOL/Power.thy
src/HOL/Presburger.thy
src/HOL/Probability/Bochner_Integration.thy
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Convolution.thy
src/HOL/Probability/Distributions.thy
src/HOL/Probability/Lebesgue_Measure.thy
src/HOL/Proofs/Extraction/Euclid.thy
src/HOL/Quotient_Examples/Quotient_Int.thy
src/HOL/Rat.thy
src/HOL/Real.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Rings.thy
src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy
src/HOL/Semiring_Normalization.thy
src/HOL/Set_Interval.thy
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/group_cancel.ML
src/HOL/Tools/nat_arith.ML
src/HOL/Tools/nat_numeral_simprocs.ML
src/HOL/Tools/numeral_simprocs.ML
src/HOL/Transcendental.thy
src/HOL/UNITY/Comp/AllocBase.thy
src/HOL/Word/Bool_List_Representation.thy
src/HOL/Word/Word.thy
src/HOL/Word/Word_Miscellaneous.thy
src/HOL/ex/Dedekind_Real.thy
src/HOL/ex/Sqrt.thy
src/HOL/ex/Sqrt_Script.thy
src/HOL/ex/ThreeDivides.thy
     1.1 --- a/src/Doc/How_to_Prove_it/How_to_Prove_it.thy	Sat Jul 05 10:09:01 2014 +0200
     1.2 +++ b/src/Doc/How_to_Prove_it/How_to_Prove_it.thy	Sat Jul 05 11:01:53 2014 +0200
     1.3 @@ -113,10 +113,10 @@
     1.4  
     1.5  Because @{thm[source]algebra_simps} multiplies out, terms can explode.
     1.6  If one merely wants to bring sums or products into a canonical order
     1.7 -it suffices to rewrite with @{thm [source] add_ac} or @{thm [source] mult_ac}: *}
     1.8 +it suffices to rewrite with @{thm [source] ac_simps}: *}
     1.9  
    1.10  lemma fixes f :: "int \<Rightarrow> int" shows "f(x*y*z) - f(z*x*y) = 0"
    1.11 -by(simp add: mult_ac)
    1.12 +by(simp add: ac_simps)
    1.13  
    1.14  text{* The lemmas @{thm[source]algebra_simps} take care of addition, subtraction
    1.15  and multiplication (algebraic structures up to rings) but ignore division (fields).
     2.1 --- a/src/Doc/Tutorial/Types/Numbers.thy	Sat Jul 05 10:09:01 2014 +0200
     2.2 +++ b/src/Doc/Tutorial/Types/Numbers.thy	Sat Jul 05 11:01:53 2014 +0200
     2.3 @@ -40,14 +40,14 @@
     2.4  @{thm[display] add.left_commute[no_vars]}
     2.5  \rulename{add.left_commute}
     2.6  
     2.7 -these form add_ac; similarly there is mult_ac
     2.8 +these form ac_simps; similarly there is ac_simps
     2.9  *}
    2.10  
    2.11  lemma "Suc(i + j*l*k + m*n) = f (n*m + i + k*j*l)"
    2.12  txt{*
    2.13  @{subgoals[display,indent=0,margin=65]}
    2.14  *};
    2.15 -apply (simp add: add_ac mult_ac)
    2.16 +apply (simp add: ac_simps ac_simps)
    2.17  txt{*
    2.18  @{subgoals[display,indent=0,margin=65]}
    2.19  *};
     3.1 --- a/src/Doc/Tutorial/document/numerics.tex	Sat Jul 05 10:09:01 2014 +0200
     3.2 +++ b/src/Doc/Tutorial/document/numerics.tex	Sat Jul 05 11:01:53 2014 +0200
     3.3 @@ -447,9 +447,9 @@
     3.4  a\ +\ (b\ +\ c)\ =\ b\ +\ (a\ +\ c)
     3.5  \rulename{add.left_commute}
     3.6  \end{isabelle}
     3.7 -The name \isa{add_ac}\index{*add_ac (theorems)} 
     3.8 +The name \isa{ac_simps}\index{*ac_simps (theorems)} 
     3.9  refers to the list of all three theorems; similarly
    3.10 -there is \isa{mult_ac}.\index{*mult_ac (theorems)} 
    3.11 +there is \isa{ac_simps}.\index{*ac_simps (theorems)} 
    3.12  They are all proved for semirings and therefore hold for all numeric types.
    3.13  
    3.14  Here is an example of the sorting effect.  Start
    3.15 @@ -459,9 +459,9 @@
    3.16  f\ (n\ *\ m\ +\ i\ +\ k\ *\ j\ *\ l)
    3.17  \end{isabelle}
    3.18  %
    3.19 -Simplify using  \isa{add_ac} and \isa{mult_ac}.
    3.20 +Simplify using  \isa{ac_simps} and \isa{ac_simps}.
    3.21  \begin{isabelle}
    3.22 -\isacommand{apply}\ (simp\ add:\ add_ac\ mult_ac)
    3.23 +\isacommand{apply}\ (simp\ add:\ ac_simps\ ac_simps)
    3.24  \end{isabelle}
    3.25  %
    3.26  Here is the resulting subgoal.
     4.1 --- a/src/HOL/Algebra/IntRing.thy	Sat Jul 05 10:09:01 2014 +0200
     4.2 +++ b/src/HOL/Algebra/IntRing.thy	Sat Jul 05 11:01:53 2014 +0200
     4.3 @@ -290,7 +290,7 @@
     4.4    apply (subst int_Idl_subset_ideal, subst int_Idl, simp)
     4.5    apply (rule, clarify)
     4.6    apply (simp add: dvd_def)
     4.7 -  apply (simp add: dvd_def mult_ac)
     4.8 +  apply (simp add: dvd_def ac_simps)
     4.9    done
    4.10  
    4.11  lemma dvds_eq_Idl: "l dvd k \<and> k dvd l \<longleftrightarrow> Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l}"
     5.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Sat Jul 05 10:09:01 2014 +0200
     5.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Sat Jul 05 11:01:53 2014 +0200
     5.3 @@ -1695,7 +1695,7 @@
     5.4    also have "\<dots> \<longleftrightarrow> j dvd (- (c * x - ?e))"
     5.5      by (simp only: dvd_minus_iff)
     5.6    also have "\<dots> \<longleftrightarrow> j dvd (c * (- x)) + ?e"
     5.7 -    by (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] add_ac minus_add_distrib)
     5.8 +    by (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] ac_simps minus_add_distrib)
     5.9        (simp add: algebra_simps)
    5.10    also have "\<dots> = Ifm bbs ((- x) # bs) (Dvd j (CN 0 c e))"
    5.11      using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] by simp
    5.12 @@ -1709,7 +1709,7 @@
    5.13    also have "\<dots> \<longleftrightarrow> j dvd (- (c * x - ?e))"
    5.14      by (simp only: dvd_minus_iff)
    5.15    also have "\<dots> \<longleftrightarrow> j dvd (c * (- x)) + ?e"
    5.16 -    by (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] add_ac minus_add_distrib)
    5.17 +    by (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] ac_simps minus_add_distrib)
    5.18        (simp add: algebra_simps)
    5.19    also have "\<dots> \<longleftrightarrow> Ifm bbs ((- x) # bs) (Dvd j (CN 0 c e))"
    5.20      using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] by simp
     6.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Sat Jul 05 10:09:01 2014 +0200
     6.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Sat Jul 05 11:01:53 2014 +0200
     6.3 @@ -1059,7 +1059,7 @@
     6.4    {fix x
     6.5      assume xz: "x < ?z"
     6.6      hence "(real c * x < - ?e)" 
     6.7 -      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) 
     6.8 +      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps) 
     6.9      hence "real c * x + ?e < 0" by arith
    6.10      hence "real c * x + ?e \<noteq> 0" by simp
    6.11      with xz have "?P ?z x (Eq (CN 0 c e))"
    6.12 @@ -1076,7 +1076,7 @@
    6.13    {fix x
    6.14      assume xz: "x < ?z"
    6.15      hence "(real c * x < - ?e)" 
    6.16 -      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) 
    6.17 +      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps) 
    6.18      hence "real c * x + ?e < 0" by arith
    6.19      hence "real c * x + ?e \<noteq> 0" by simp
    6.20      with xz have "?P ?z x (NEq (CN 0 c e))"
    6.21 @@ -1093,7 +1093,7 @@
    6.22    {fix x
    6.23      assume xz: "x < ?z"
    6.24      hence "(real c * x < - ?e)" 
    6.25 -      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) 
    6.26 +      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps) 
    6.27      hence "real c * x + ?e < 0" by arith
    6.28      with xz have "?P ?z x (Lt (CN 0 c e))"
    6.29        using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"]  by simp }
    6.30 @@ -1109,7 +1109,7 @@
    6.31    {fix x
    6.32      assume xz: "x < ?z"
    6.33      hence "(real c * x < - ?e)" 
    6.34 -      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) 
    6.35 +      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps) 
    6.36      hence "real c * x + ?e < 0" by arith
    6.37      with xz have "?P ?z x (Le (CN 0 c e))"
    6.38        using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
    6.39 @@ -1125,7 +1125,7 @@
    6.40    {fix x
    6.41      assume xz: "x < ?z"
    6.42      hence "(real c * x < - ?e)" 
    6.43 -      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) 
    6.44 +      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps) 
    6.45      hence "real c * x + ?e < 0" by arith
    6.46      with xz have "?P ?z x (Gt (CN 0 c e))"
    6.47        using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
    6.48 @@ -1141,7 +1141,7 @@
    6.49    {fix x
    6.50      assume xz: "x < ?z"
    6.51      hence "(real c * x < - ?e)" 
    6.52 -      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) 
    6.53 +      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps) 
    6.54      hence "real c * x + ?e < 0" by arith
    6.55      with xz have "?P ?z x (Ge (CN 0 c e))"
    6.56        using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
    6.57 @@ -1167,7 +1167,7 @@
    6.58    {fix x
    6.59      assume xz: "x > ?z"
    6.60      with mult_strict_right_mono [OF xz cp] cp
    6.61 -    have "(real c * x > - ?e)" by (simp add: mult_ac)
    6.62 +    have "(real c * x > - ?e)" by (simp add: ac_simps)
    6.63      hence "real c * x + ?e > 0" by arith
    6.64      hence "real c * x + ?e \<noteq> 0" by simp
    6.65      with xz have "?P ?z x (Eq (CN 0 c e))"
    6.66 @@ -1184,7 +1184,7 @@
    6.67    {fix x
    6.68      assume xz: "x > ?z"
    6.69      with mult_strict_right_mono [OF xz cp] cp
    6.70 -    have "(real c * x > - ?e)" by (simp add: mult_ac)
    6.71 +    have "(real c * x > - ?e)" by (simp add: ac_simps)
    6.72      hence "real c * x + ?e > 0" by arith
    6.73      hence "real c * x + ?e \<noteq> 0" by simp
    6.74      with xz have "?P ?z x (NEq (CN 0 c e))"
    6.75 @@ -1201,7 +1201,7 @@
    6.76    {fix x
    6.77      assume xz: "x > ?z"
    6.78      with mult_strict_right_mono [OF xz cp] cp
    6.79 -    have "(real c * x > - ?e)" by (simp add: mult_ac)
    6.80 +    have "(real c * x > - ?e)" by (simp add: ac_simps)
    6.81      hence "real c * x + ?e > 0" by arith
    6.82      with xz have "?P ?z x (Lt (CN 0 c e))"
    6.83        using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
    6.84 @@ -1217,7 +1217,7 @@
    6.85    {fix x
    6.86      assume xz: "x > ?z"
    6.87      with mult_strict_right_mono [OF xz cp] cp
    6.88 -    have "(real c * x > - ?e)" by (simp add: mult_ac)
    6.89 +    have "(real c * x > - ?e)" by (simp add: ac_simps)
    6.90      hence "real c * x + ?e > 0" by arith
    6.91      with xz have "?P ?z x (Le (CN 0 c e))"
    6.92        using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
    6.93 @@ -1233,7 +1233,7 @@
    6.94    {fix x
    6.95      assume xz: "x > ?z"
    6.96      with mult_strict_right_mono [OF xz cp] cp
    6.97 -    have "(real c * x > - ?e)" by (simp add: mult_ac)
    6.98 +    have "(real c * x > - ?e)" by (simp add: ac_simps)
    6.99      hence "real c * x + ?e > 0" by arith
   6.100      with xz have "?P ?z x (Gt (CN 0 c e))"
   6.101        using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
   6.102 @@ -1249,7 +1249,7 @@
   6.103    {fix x
   6.104      assume xz: "x > ?z"
   6.105      with mult_strict_right_mono [OF xz cp] cp
   6.106 -    have "(real c * x > - ?e)" by (simp add: mult_ac)
   6.107 +    have "(real c * x > - ?e)" by (simp add: ac_simps)
   6.108      hence "real c * x + ?e > 0" by arith
   6.109      with xz have "?P ?z x (Ge (CN 0 c e))"
   6.110        using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"]   by simp }
     7.1 --- a/src/HOL/Decision_Procs/MIR.thy	Sat Jul 05 10:09:01 2014 +0200
     7.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Sat Jul 05 11:01:53 2014 +0200
     7.3 @@ -1542,10 +1542,10 @@
     7.4    have th': "(real ?nt)*(real x) = real (?nt * x)" by simp
     7.5    have "?I x (Floor t) = ?I x (Floor (CN 0 ?nt ?at))" using th2 by simp
     7.6    also have "\<dots> = real (floor ((real ?nt)* real(x) + ?I x ?at))" by simp
     7.7 -  also have "\<dots> = real (floor (?I x ?at + real (?nt* x)))" by (simp add: add_ac)
     7.8 +  also have "\<dots> = real (floor (?I x ?at + real (?nt* x)))" by (simp add: ac_simps)
     7.9    also have "\<dots> = real (floor (?I x ?at) + (?nt* x))" 
    7.10      using floor_add[where x="?I x ?at" and a="?nt* x"] by simp 
    7.11 -  also have "\<dots> = real (?nt)*(real x) + real (floor (?I x ?at))" by (simp add: add_ac)
    7.12 +  also have "\<dots> = real (?nt)*(real x) + real (floor (?I x ?at))" by (simp add: ac_simps)
    7.13    finally have "?I x (Floor t) = ?I x (CN 0 n a)" using th by simp
    7.14    with na show ?case by simp
    7.15  qed
    7.16 @@ -1733,7 +1733,7 @@
    7.17    {assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Lt a))" 
    7.18        by (simp add: nb Let_def split_def isint_Floor isint_neg)
    7.19      have "?I (Lt a) = (real (?c * i) + (?N ?r) < 0)" using Ia by (simp add: Let_def split_def)
    7.20 -    also from cn cnz have "\<dots> = (?I (?l (Lt a)))" by (simp only: split_int_less_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def add_ac, arith)
    7.21 +    also from cn cnz have "\<dots> = (?I (?l (Lt a)))" by (simp only: split_int_less_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def ac_simps, arith)
    7.22      finally have ?case using l by simp}
    7.23    ultimately show ?case by blast
    7.24  next
    7.25 @@ -1758,7 +1758,7 @@
    7.26    {assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Le a))" 
    7.27        by (simp add: nb Let_def split_def isint_Floor isint_neg)
    7.28      have "?I (Le a) = (real (?c * i) + (?N ?r) \<le> 0)" using Ia by (simp add: Let_def split_def)
    7.29 -    also from cn cnz have "\<dots> = (?I (?l (Le a)))" by (simp only: split_int_le_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def add_ac, arith)
    7.30 +    also from cn cnz have "\<dots> = (?I (?l (Le a)))" by (simp only: split_int_le_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def ac_simps, arith)
    7.31      finally have ?case using l by simp}
    7.32    ultimately show ?case by blast
    7.33  next
    7.34 @@ -1783,7 +1783,7 @@
    7.35    {assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Gt a))" 
    7.36        by (simp add: nb Let_def split_def isint_Floor isint_neg)
    7.37      have "?I (Gt a) = (real (?c * i) + (?N ?r) > 0)" using Ia by (simp add: Let_def split_def)
    7.38 -    also from cn cnz have "\<dots> = (?I (?l (Gt a)))" by (simp only: split_int_gt_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def add_ac, arith)
    7.39 +    also from cn cnz have "\<dots> = (?I (?l (Gt a)))" by (simp only: split_int_gt_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def ac_simps, arith)
    7.40      finally have ?case using l by simp}
    7.41    ultimately show ?case by blast
    7.42  next
    7.43 @@ -1808,7 +1808,7 @@
    7.44    {assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Ge a))" 
    7.45        by (simp add: nb Let_def split_def isint_Floor isint_neg)
    7.46      have "?I (Ge a) = (real (?c * i) + (?N ?r) \<ge> 0)" using Ia by (simp add: Let_def split_def)
    7.47 -    also from cn cnz have "\<dots> = (?I (?l (Ge a)))" by (simp only: split_int_ge_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def add_ac, arith)
    7.48 +    also from cn cnz have "\<dots> = (?I (?l (Ge a)))" by (simp only: split_int_ge_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def ac_simps, arith)
    7.49      finally have ?case using l by simp}
    7.50    ultimately show ?case by blast
    7.51  next
    7.52 @@ -1886,10 +1886,10 @@
    7.53        by (simp only: rdvd_abs1[where d="j" and t="real (?c*i) + ?N ?r", symmetric]) simp
    7.54      also have "\<dots> = ((abs j) dvd (floor ((?N ?r) + real (?c*i))) \<and> 
    7.55         (real (floor ((?N ?r) + real (?c*i))) = (real (?c*i) + (?N ?r))))" 
    7.56 -      by(simp only: int_rdvd_real[where i="abs j" and x="real (?c*i) + (?N ?r)"]) (simp only: add_ac)
    7.57 +      by(simp only: int_rdvd_real[where i="abs j" and x="real (?c*i) + (?N ?r)"]) (simp only: ac_simps)
    7.58      also have "\<dots> = (?I (?l (Dvd j a)))" using cp cnz jnz  
    7.59        by (simp add: Let_def split_def int_rdvd_iff[symmetric]  
    7.60 -        del: real_of_int_mult) (auto simp add: add_ac)
    7.61 +        del: real_of_int_mult) (auto simp add: ac_simps)
    7.62      finally have ?case using l jnz  by simp }
    7.63    moreover
    7.64    {assume cn: "?c < 0" and cnz: "?c\<noteq>0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))" 
    7.65 @@ -1900,11 +1900,11 @@
    7.66        by (simp only: rdvd_abs1[where d="j" and t="real (?c*i) + ?N ?r", symmetric]) simp
    7.67      also have "\<dots> = ((abs j) dvd (floor ((?N ?r) + real (?c*i))) \<and> 
    7.68         (real (floor ((?N ?r) + real (?c*i))) = (real (?c*i) + (?N ?r))))" 
    7.69 -      by(simp only: int_rdvd_real[where i="abs j" and x="real (?c*i) + (?N ?r)"]) (simp only: add_ac)
    7.70 +      by(simp only: int_rdvd_real[where i="abs j" and x="real (?c*i) + (?N ?r)"]) (simp only: ac_simps)
    7.71      also have "\<dots> = (?I (?l (Dvd j a)))" using cn cnz jnz
    7.72        using rdvd_minus [where d="abs j" and t="real (?c*i + floor (?N ?r))", simplified, symmetric]
    7.73        by (simp add: Let_def split_def int_rdvd_iff[symmetric]  
    7.74 -        del: real_of_int_mult) (auto simp add: add_ac)
    7.75 +        del: real_of_int_mult) (auto simp add: ac_simps)
    7.76      finally have ?case using l jnz by blast }
    7.77    ultimately show ?case by blast
    7.78  next
    7.79 @@ -1932,10 +1932,10 @@
    7.80        by (simp only: rdvd_abs1[where d="j" and t="real (?c*i) + ?N ?r", symmetric]) simp
    7.81      also have "\<dots> = (\<not> ((abs j) dvd (floor ((?N ?r) + real (?c*i))) \<and> 
    7.82         (real (floor ((?N ?r) + real (?c*i))) = (real (?c*i) + (?N ?r)))))" 
    7.83 -      by(simp only: int_rdvd_real[where i="abs j" and x="real (?c*i) + (?N ?r)"]) (simp only: add_ac)
    7.84 +      by(simp only: int_rdvd_real[where i="abs j" and x="real (?c*i) + (?N ?r)"]) (simp only: ac_simps)
    7.85      also have "\<dots> = (?I (?l (NDvd j a)))" using cp cnz jnz  
    7.86        by (simp add: Let_def split_def int_rdvd_iff[symmetric]  
    7.87 -        del: real_of_int_mult) (auto simp add: add_ac)
    7.88 +        del: real_of_int_mult) (auto simp add: ac_simps)
    7.89      finally have ?case using l jnz  by simp }
    7.90    moreover
    7.91    {assume cn: "?c < 0" and cnz: "?c\<noteq>0" and jnz: "j\<noteq>0" hence l: "?L (?l (NDvd j a))" 
    7.92 @@ -1946,11 +1946,11 @@
    7.93        by (simp only: rdvd_abs1[where d="j" and t="real (?c*i) + ?N ?r", symmetric]) simp
    7.94      also have "\<dots> = (\<not> ((abs j) dvd (floor ((?N ?r) + real (?c*i))) \<and> 
    7.95         (real (floor ((?N ?r) + real (?c*i))) = (real (?c*i) + (?N ?r)))))" 
    7.96 -      by(simp only: int_rdvd_real[where i="abs j" and x="real (?c*i) + (?N ?r)"]) (simp only: add_ac)
    7.97 +      by(simp only: int_rdvd_real[where i="abs j" and x="real (?c*i) + (?N ?r)"]) (simp only: ac_simps)
    7.98      also have "\<dots> = (?I (?l (NDvd j a)))" using cn cnz jnz
    7.99        using rdvd_minus [where d="abs j" and t="real (?c*i + floor (?N ?r))", simplified, symmetric]
   7.100        by (simp add: Let_def split_def int_rdvd_iff[symmetric]  
   7.101 -        del: real_of_int_mult) (auto simp add: add_ac)
   7.102 +        del: real_of_int_mult) (auto simp add: ac_simps)
   7.103      finally have ?case using l jnz by blast }
   7.104    ultimately show ?case by blast
   7.105  qed auto
   7.106 @@ -4159,7 +4159,7 @@
   7.107    {fix x
   7.108      assume xz: "x < ?z"
   7.109      hence "(real c * x < - ?e)" 
   7.110 -      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) 
   7.111 +      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps) 
   7.112      hence "real c * x + ?e < 0" by arith
   7.113      hence "real c * x + ?e \<noteq> 0" by simp
   7.114      with xz have "?P ?z x (Eq (CN 0 c e))"
   7.115 @@ -4176,7 +4176,7 @@
   7.116    {fix x
   7.117      assume xz: "x < ?z"
   7.118      hence "(real c * x < - ?e)" 
   7.119 -      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) 
   7.120 +      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps) 
   7.121      hence "real c * x + ?e < 0" by arith
   7.122      hence "real c * x + ?e \<noteq> 0" by simp
   7.123      with xz have "?P ?z x (NEq (CN 0 c e))"
   7.124 @@ -4193,7 +4193,7 @@
   7.125    {fix x
   7.126      assume xz: "x < ?z"
   7.127      hence "(real c * x < - ?e)" 
   7.128 -      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) 
   7.129 +      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps) 
   7.130      hence "real c * x + ?e < 0" by arith
   7.131      with xz have "?P ?z x (Lt (CN 0 c e))"
   7.132        using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"]  by simp }
   7.133 @@ -4209,7 +4209,7 @@
   7.134    {fix x
   7.135      assume xz: "x < ?z"
   7.136      hence "(real c * x < - ?e)" 
   7.137 -      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) 
   7.138 +      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps) 
   7.139      hence "real c * x + ?e < 0" by arith
   7.140      with xz have "?P ?z x (Le (CN 0 c e))"
   7.141        using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
   7.142 @@ -4225,7 +4225,7 @@
   7.143    {fix x
   7.144      assume xz: "x < ?z"
   7.145      hence "(real c * x < - ?e)" 
   7.146 -      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) 
   7.147 +      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps) 
   7.148      hence "real c * x + ?e < 0" by arith
   7.149      with xz have "?P ?z x (Gt (CN 0 c e))"
   7.150        using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
   7.151 @@ -4241,7 +4241,7 @@
   7.152    {fix x
   7.153      assume xz: "x < ?z"
   7.154      hence "(real c * x < - ?e)" 
   7.155 -      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac) 
   7.156 +      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps) 
   7.157      hence "real c * x + ?e < 0" by arith
   7.158      with xz have "?P ?z x (Ge (CN 0 c e))"
   7.159        using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
   7.160 @@ -4267,7 +4267,7 @@
   7.161    {fix x
   7.162      assume xz: "x > ?z"
   7.163      with mult_strict_right_mono [OF xz cp] cp
   7.164 -    have "(real c * x > - ?e)" by (simp add: mult_ac)
   7.165 +    have "(real c * x > - ?e)" by (simp add: ac_simps)
   7.166      hence "real c * x + ?e > 0" by arith
   7.167      hence "real c * x + ?e \<noteq> 0" by simp
   7.168      with xz have "?P ?z x (Eq (CN 0 c e))"
   7.169 @@ -4284,7 +4284,7 @@
   7.170    {fix x
   7.171      assume xz: "x > ?z"
   7.172      with mult_strict_right_mono [OF xz cp] cp
   7.173 -    have "(real c * x > - ?e)" by (simp add: mult_ac)
   7.174 +    have "(real c * x > - ?e)" by (simp add: ac_simps)
   7.175      hence "real c * x + ?e > 0" by arith
   7.176      hence "real c * x + ?e \<noteq> 0" by simp
   7.177      with xz have "?P ?z x (NEq (CN 0 c e))"
   7.178 @@ -4301,7 +4301,7 @@
   7.179    {fix x
   7.180      assume xz: "x > ?z"
   7.181      with mult_strict_right_mono [OF xz cp] cp
   7.182 -    have "(real c * x > - ?e)" by (simp add: mult_ac)
   7.183 +    have "(real c * x > - ?e)" by (simp add: ac_simps)
   7.184      hence "real c * x + ?e > 0" by arith
   7.185      with xz have "?P ?z x (Lt (CN 0 c e))"
   7.186        using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
   7.187 @@ -4317,7 +4317,7 @@
   7.188    {fix x
   7.189      assume xz: "x > ?z"
   7.190      with mult_strict_right_mono [OF xz cp] cp
   7.191 -    have "(real c * x > - ?e)" by (simp add: mult_ac)
   7.192 +    have "(real c * x > - ?e)" by (simp add: ac_simps)
   7.193      hence "real c * x + ?e > 0" by arith
   7.194      with xz have "?P ?z x (Le (CN 0 c e))"
   7.195        using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
   7.196 @@ -4333,7 +4333,7 @@
   7.197    {fix x
   7.198      assume xz: "x > ?z"
   7.199      with mult_strict_right_mono [OF xz cp] cp
   7.200 -    have "(real c * x > - ?e)" by (simp add: mult_ac)
   7.201 +    have "(real c * x > - ?e)" by (simp add: ac_simps)
   7.202      hence "real c * x + ?e > 0" by arith
   7.203      with xz have "?P ?z x (Gt (CN 0 c e))"
   7.204        using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
   7.205 @@ -4349,7 +4349,7 @@
   7.206    {fix x
   7.207      assume xz: "x > ?z"
   7.208      with mult_strict_right_mono [OF xz cp] cp
   7.209 -    have "(real c * x > - ?e)" by (simp add: mult_ac)
   7.210 +    have "(real c * x > - ?e)" by (simp add: ac_simps)
   7.211      hence "real c * x + ?e > 0" by arith
   7.212      with xz have "?P ?z x (Ge (CN 0 c e))"
   7.213        using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"]   by simp }
   7.214 @@ -4829,9 +4829,9 @@
   7.215    shows "(Ifm bs (E p)) = (\<exists> (i::int). Ifm (real i#bs) (E (And (And (Ge(CN 0 1 (C 0))) (Lt (CN 0 1 (C (- 1))))) (exsplit p))))" (is "?lhs = ?rhs")
   7.216  proof-
   7.217    have "?rhs = (\<exists> (i::int). \<exists> x. 0\<le> x \<and> x < 1 \<and> Ifm (x#(real i)#bs) (exsplit p))"
   7.218 -    by (simp add: myless[of _ "1"] myless[of _ "0"] add_ac)
   7.219 +    by (simp add: myless[of _ "1"] myless[of _ "0"] ac_simps)
   7.220    also have "\<dots> = (\<exists> (i::int). \<exists> x. 0\<le> x \<and> x < 1 \<and> Ifm ((real i + x) #bs) p)"
   7.221 -    by (simp only: exsplit[OF qf] add_ac)
   7.222 +    by (simp only: exsplit[OF qf] ac_simps)
   7.223    also have "\<dots> = (\<exists> x. Ifm (x#bs) p)" 
   7.224      by (simp only: real_ex_int_real01[where P="\<lambda> x. Ifm (x#bs) p"])
   7.225    finally show ?thesis by simp
     8.1 --- a/src/HOL/Decision_Procs/Polynomial_List.thy	Sat Jul 05 10:09:01 2014 +0200
     8.2 +++ b/src/HOL/Decision_Procs/Polynomial_List.thy	Sat Jul 05 11:01:53 2014 +0200
     8.3 @@ -127,7 +127,7 @@
     8.4  lemma (in comm_semiring_0) padd_assoc: "\<forall>b c. (a +++ b) +++ c = a +++ (b +++ c)"
     8.5    apply (induct a)
     8.6    apply (simp, clarify)
     8.7 -  apply (case_tac b, simp_all add: add_ac)
     8.8 +  apply (case_tac b, simp_all add: ac_simps)
     8.9    done
    8.10  
    8.11  lemma (in semiring_0) poly_cmult_distr: "a %* ( p +++ q) = (a %* p +++ a %* q)"
    8.12 @@ -152,17 +152,17 @@
    8.13  next
    8.14    case (Cons a as p2)
    8.15    thus ?case
    8.16 -    by (cases p2) (simp_all  add: add_ac distrib_left)
    8.17 +    by (cases p2) (simp_all  add: ac_simps distrib_left)
    8.18  qed
    8.19  
    8.20  lemma (in comm_semiring_0) poly_cmult: "poly (c %* p) x = c * poly p x"
    8.21    apply (induct p)
    8.22    apply (case_tac [2] "x = zero")
    8.23 -  apply (auto simp add: distrib_left mult_ac)
    8.24 +  apply (auto simp add: distrib_left ac_simps)
    8.25    done
    8.26  
    8.27  lemma (in comm_semiring_0) poly_cmult_map: "poly (map (op * c) p) x = c*poly p x"
    8.28 -  by (induct p) (auto simp add: distrib_left mult_ac)
    8.29 +  by (induct p) (auto simp add: distrib_left ac_simps)
    8.30  
    8.31  lemma (in comm_ring_1) poly_minus: "poly (-- p) x = - (poly p x)"
    8.32    apply (simp add: poly_minus_def)
    8.33 @@ -176,7 +176,7 @@
    8.34  next
    8.35    case (Cons a as p2)
    8.36    thus ?case by (cases as)
    8.37 -    (simp_all add: poly_cmult poly_add distrib_right distrib_left mult_ac)
    8.38 +    (simp_all add: poly_cmult poly_add distrib_right distrib_left ac_simps)
    8.39  qed
    8.40  
    8.41  class idom_char_0 = idom + ring_char_0
    8.42 @@ -505,7 +505,7 @@
    8.43    apply (auto simp add: poly_linear_divides poly_add poly_cmult distrib_right [symmetric])
    8.44    apply (rule_tac x = "pmult qa q" in exI)
    8.45    apply (rule_tac [2] x = "pmult p qa" in exI)
    8.46 -  apply (auto simp add: poly_add poly_mult poly_cmult mult_ac)
    8.47 +  apply (auto simp add: poly_add poly_mult poly_cmult ac_simps)
    8.48    done
    8.49  
    8.50  lemma (in comm_semiring_1) poly_divides_refl[simp]: "p divides p"
    8.51 @@ -526,7 +526,7 @@
    8.52    apply (rule_tac [2] poly_divides_trans)
    8.53    apply (auto simp add: divides_def)
    8.54    apply (rule_tac x = p in exI)
    8.55 -  apply (auto simp add: poly_mult fun_eq mult_ac)
    8.56 +  apply (auto simp add: poly_mult fun_eq ac_simps)
    8.57    done
    8.58  
    8.59  lemma (in comm_semiring_1) poly_exp_divides:
    8.60 @@ -550,7 +550,7 @@
    8.61  lemma (in comm_ring_1) poly_divides_diff2:
    8.62    "p divides r \<Longrightarrow> p divides (q +++ r) \<Longrightarrow> p divides q"
    8.63    apply (erule poly_divides_diff)
    8.64 -  apply (auto simp add: poly_add fun_eq poly_mult divides_def add_ac)
    8.65 +  apply (auto simp add: poly_add fun_eq poly_mult divides_def ac_simps)
    8.66    done
    8.67  
    8.68  lemma (in semiring_0) poly_divides_zero: "poly p = poly [] \<Longrightarrow> q divides p"
    8.69 @@ -608,7 +608,7 @@
    8.70  
    8.71  
    8.72  lemma (in comm_semiring_1) poly_mulexp: "poly (mulexp n p q) x = (poly p x) ^ n * poly q x"
    8.73 -  by (induct n) (auto simp add: poly_mult mult_ac)
    8.74 +  by (induct n) (auto simp add: poly_mult ac_simps)
    8.75  
    8.76  lemma (in comm_semiring_1) divides_left_mult:
    8.77    assumes d:"(p***q) divides r" shows "p divides r \<and> q divides r"
    8.78 @@ -616,7 +616,7 @@
    8.79    from d obtain t where r:"poly r = poly (p***q *** t)"
    8.80      unfolding divides_def by blast
    8.81    hence "poly r = poly (p *** (q *** t))"
    8.82 -    "poly r = poly (q *** (p***t))" by(auto simp add: fun_eq poly_mult mult_ac)
    8.83 +    "poly r = poly (q *** (p***t))" by(auto simp add: fun_eq poly_mult ac_simps)
    8.84    thus ?thesis unfolding divides_def by blast
    8.85  qed
    8.86  
    8.87 @@ -742,7 +742,7 @@
    8.88    apply (simp add: divides_def del: pexp_Suc pmult_Cons, safe)
    8.89    apply (rule_tac x = q in exI, safe)
    8.90    apply (drule_tac x = qa in spec)
    8.91 -  apply (auto simp add: poly_mult fun_eq poly_exp mult_ac simp del: pmult_Cons)
    8.92 +  apply (auto simp add: poly_mult fun_eq poly_exp ac_simps simp del: pmult_Cons)
    8.93    done
    8.94  
    8.95  text{*Important composition properties of orders.*}
    8.96 @@ -755,7 +755,7 @@
    8.97    apply safe
    8.98    apply (simp add: divides_def fun_eq poly_exp_add poly_mult del: pmult_Cons, safe)
    8.99    apply (rule_tac x = "qa *** qaa" in exI)
   8.100 -  apply (simp add: poly_mult mult_ac del: pmult_Cons)
   8.101 +  apply (simp add: poly_mult ac_simps del: pmult_Cons)
   8.102    apply (drule_tac a = a in order_decomp)+
   8.103    apply safe
   8.104    apply (subgoal_tac "[-a,1] divides (qa *** qaa) ")
   8.105 @@ -766,7 +766,7 @@
   8.106    apply (drule poly_mult_left_cancel [THEN iffD1], force)
   8.107    apply (subgoal_tac "poly ([-a, 1] %^ (order a q) *** ([-a, 1] %^ (order a p) *** (qa *** qaa))) = poly ([-a, 1] %^ (order a q) *** ([-a, 1] %^ (order a p) *** ([-a, 1] *** qb))) ")
   8.108    apply (drule poly_mult_left_cancel [THEN iffD1], force)
   8.109 -  apply (simp add: fun_eq poly_exp_add poly_mult mult_ac del: pmult_Cons)
   8.110 +  apply (simp add: fun_eq poly_exp_add poly_mult ac_simps del: pmult_Cons)
   8.111    done
   8.112  
   8.113  lemma (in idom_char_0) order_mult:
   8.114 @@ -779,7 +779,7 @@
   8.115    apply safe
   8.116    apply (simp add: divides_def fun_eq poly_exp_add poly_mult del: pmult_Cons, safe)
   8.117    apply (rule_tac x = "pmult qa qaa" in exI)
   8.118 -  apply (simp add: poly_mult mult_ac del: pmult_Cons)
   8.119 +  apply (simp add: poly_mult ac_simps del: pmult_Cons)
   8.120    apply (drule_tac a = a in order_decomp)+
   8.121    apply safe
   8.122    apply (subgoal_tac "[uminus a, one] divides pmult qa qaa")
   8.123 @@ -794,7 +794,7 @@
   8.124      poly (pmult (pexp [uminus a, one] (order a q))
   8.125        (pmult (pexp [uminus a, one] (order a p)) (pmult [uminus a, one] qb)))")
   8.126    apply (drule poly_mult_left_cancel [THEN iffD1], force)
   8.127 -  apply (simp add: fun_eq poly_exp_add poly_mult mult_ac del: pmult_Cons)
   8.128 +  apply (simp add: fun_eq poly_exp_add poly_mult ac_simps del: pmult_Cons)
   8.129    done
   8.130  
   8.131  lemma (in idom_char_0) order_root2: "poly p \<noteq> poly [] \<Longrightarrow> poly p a = 0 \<longleftrightarrow> order a p \<noteq> 0"
   8.132 @@ -988,7 +988,7 @@
   8.133    have eq: "poly ([a,1] %^(Suc n) *** p) = poly ([a,1] %^ n *** ([a,1] *** p))"
   8.134      apply (rule ext)
   8.135      apply (simp add: poly_mult poly_add poly_cmult)
   8.136 -    apply (simp add: mult_ac add_ac distrib_left)
   8.137 +    apply (simp add: ac_simps ac_simps distrib_left)
   8.138      done
   8.139    note deq = degree_unique[OF eq]
   8.140    show ?case
     9.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Sat Jul 05 10:09:01 2014 +0200
     9.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Sat Jul 05 11:01:53 2014 +0200
     9.3 @@ -53,7 +53,7 @@
     9.4            div_by_0 mod_by_0 div_0 mod_0
     9.5            div_by_1 mod_by_1 div_1 mod_1
     9.6            Suc_eq_plus1}
     9.7 -      addsimps @{thms add_ac}
     9.8 +      addsimps @{thms ac_simps}
     9.9        addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
    9.10      val simpset0 =
    9.11        put_simpset HOL_basic_ss ctxt
    10.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Sat Jul 05 10:09:01 2014 +0200
    10.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Sat Jul 05 11:01:53 2014 +0200
    10.3 @@ -19,8 +19,7 @@
    10.4    val nat_arith = [@{thm diff_nat_numeral}];
    10.5  
    10.6    val comp_arith = [@{thm "Let_def"}, @{thm "if_False"}, @{thm "if_True"}, @{thm "add_0"},
    10.7 -                 @{thm "add_Suc"}, @{thm add_numeral_left}, @{thm mult_numeral_left(1)},
    10.8 -                 @{thm "Suc_eq_plus1"}] @
    10.9 +                 @{thm "add_Suc"}, @{thm add_numeral_left}, @{thm mult_numeral_left(1)}] @
   10.10                   (map (fn th => th RS sym) [@{thm "numeral_1_eq_1"}])
   10.11                   @ @{thms arith_simps} @ nat_arith @ @{thms rel_simps} 
   10.12    val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"}, 
   10.13 @@ -81,7 +80,7 @@
   10.14                                    @{thm div_0}, @{thm mod_0},
   10.15                                    @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
   10.16                                    @{thm "Suc_eq_plus1"}]
   10.17 -                        addsimps @{thms add_ac}
   10.18 +                        addsimps @{thms add.assoc add.commute add.left_commute}
   10.19                          addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
   10.20      val simpset0 = put_simpset HOL_basic_ss ctxt
   10.21        addsimps [mod_div_equality', @{thm Suc_eq_plus1}]
    11.1 --- a/src/HOL/Deriv.thy	Sat Jul 05 10:09:01 2014 +0200
    11.2 +++ b/src/HOL/Deriv.thy	Sat Jul 05 11:01:53 2014 +0200
    11.3 @@ -681,7 +681,7 @@
    11.4  
    11.5  lemma DERIV_cmult_right:
    11.6    "(f has_field_derivative D) (at x within s) ==> ((\<lambda>x. f x * c) has_field_derivative D * c) (at x within s)"
    11.7 -  using DERIV_cmult by (force simp add: mult_ac)
    11.8 +  using DERIV_cmult by (force simp add: ac_simps)
    11.9  
   11.10  lemma DERIV_cmult_Id [simp]: "(op * c has_field_derivative c) (at x within s)"
   11.11    by (cut_tac c = c and x = x in DERIV_ident [THEN DERIV_cmult], simp)
   11.12 @@ -717,7 +717,7 @@
   11.13  lemma DERIV_inverse_fun:
   11.14    "(f has_field_derivative d) (at x within s) \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow>
   11.15    ((\<lambda>x. inverse (f x)) has_field_derivative (- (d * inverse(f x ^ Suc (Suc 0))))) (at x within s)"
   11.16 -  by (drule (1) DERIV_inverse') (simp add: mult_ac nonzero_inverse_mult_distrib)
   11.17 +  by (drule (1) DERIV_inverse') (simp add: ac_simps nonzero_inverse_mult_distrib)
   11.18  
   11.19  text {* Derivative of quotient *}
   11.20  
   11.21 @@ -1479,7 +1479,7 @@
   11.22    ultimately have "(b - a) * (g'c * (f b - f a) - f'c * (g b - g a)) = 0" by auto
   11.23    with alb have "g'c * (f b - f a) - f'c * (g b - g a) = 0" by simp
   11.24    hence "g'c * (f b - f a) = f'c * (g b - g a)" by simp
   11.25 -  hence "(f b - f a) * g'c = (g b - g a) * f'c" by (simp add: mult_ac)
   11.26 +  hence "(f b - f a) * g'c = (g b - g a) * f'c" by (simp add: ac_simps)
   11.27  
   11.28    with g'cdef f'cdef cint show ?thesis by auto
   11.29  qed
    12.1 --- a/src/HOL/Divides.thy	Sat Jul 05 10:09:01 2014 +0200
    12.2 +++ b/src/HOL/Divides.thy	Sat Jul 05 11:01:53 2014 +0200
    12.3 @@ -34,7 +34,7 @@
    12.4  
    12.5  lemma mod_div_equality': "a mod b + a div b * b = a"
    12.6    using mod_div_equality [of a b]
    12.7 -  by (simp only: add_ac)
    12.8 +  by (simp only: ac_simps)
    12.9  
   12.10  lemma div_mod_equality: "((a div b) * b + a mod b) + c = a + c"
   12.11    by (simp add: mod_div_equality)
   12.12 @@ -228,7 +228,7 @@
   12.13    have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
   12.14      by (simp only: mod_div_equality)
   12.15    also have "\<dots> = (a mod c + b + a div c * c) mod c"
   12.16 -    by (simp only: add_ac)
   12.17 +    by (simp only: ac_simps)
   12.18    also have "\<dots> = (a mod c + b) mod c"
   12.19      by (rule mod_mult_self1)
   12.20    finally show ?thesis .
   12.21 @@ -239,7 +239,7 @@
   12.22    have "(a + b) mod c = (a + (b div c * c + b mod c)) mod c"
   12.23      by (simp only: mod_div_equality)
   12.24    also have "\<dots> = (a + b mod c + b div c * c) mod c"
   12.25 -    by (simp only: add_ac)
   12.26 +    by (simp only: ac_simps)
   12.27    also have "\<dots> = (a + b mod c) mod c"
   12.28      by (rule mod_mult_self1)
   12.29    finally show ?thesis .
   12.30 @@ -321,7 +321,7 @@
   12.31    also have "\<dots> = (a mod (c * k) + a div (c * k) * k * c) mod c"
   12.32      by (simp only: mod_mult_self1)
   12.33    also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
   12.34 -    by (simp only: add_ac mult_ac)
   12.35 +    by (simp only: ac_simps ac_simps)
   12.36    also have "\<dots> = a mod c"
   12.37      by (simp only: mod_div_equality)
   12.38    finally show ?thesis .
   12.39 @@ -421,7 +421,7 @@
   12.40    have "(- a) mod b = (- (a div b * b + a mod b)) mod b"
   12.41      by (simp only: mod_div_equality)
   12.42    also have "\<dots> = (- (a mod b) + - (a div b) * b) mod b"
   12.43 -    by (simp only: minus_add_distrib minus_mult_left add_ac)
   12.44 +    by (simp add: ac_simps)
   12.45    also have "\<dots> = (- (a mod b)) mod b"
   12.46      by (rule mod_mult_self1)
   12.47    finally show ?thesis .
   12.48 @@ -957,7 +957,7 @@
   12.49    val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
   12.50  
   12.51    val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
   12.52 -    (@{thm add_0_left} :: @{thm add_0_right} :: @{thms add_ac}))
   12.53 +    (@{thm add_0_left} :: @{thm add_0_right} :: @{thms ac_simps}))
   12.54  )
   12.55  *}
   12.56  
   12.57 @@ -1059,7 +1059,7 @@
   12.58  lemma divmod_nat_rel_mult2_eq:
   12.59    "divmod_nat_rel a b (q, r)
   12.60     \<Longrightarrow> divmod_nat_rel a (b * c) (q div c, b *(q mod c) + r)"
   12.61 -by (auto simp add: mult_ac divmod_nat_rel_def add_mult_distrib2 [symmetric] mod_lemma)
   12.62 +by (auto simp add: mult.commute mult.left_commute divmod_nat_rel_def add_mult_distrib2 [symmetric] mod_lemma)
   12.63  
   12.64  lemma div_mult2_eq: "a div (b * c) = (a div b) div (c::nat)"
   12.65  by (force simp add: divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN div_nat_unique])
   12.66 @@ -1147,11 +1147,15 @@
   12.67  lemmas mod_eq_0D [dest!] = mod_eq_0_iff [THEN iffD1]
   12.68  
   12.69  (*Loses information, namely we also have r<d provided d is nonzero*)
   12.70 -lemma mod_eqD: "(m mod d = r) ==> \<exists>q::nat. m = r + q*d"
   12.71 -  apply (cut_tac a = m in mod_div_equality)
   12.72 -  apply (simp only: add_ac)
   12.73 -  apply (blast intro: sym)
   12.74 -  done
   12.75 +lemma mod_eqD:
   12.76 +  fixes m d r q :: nat
   12.77 +  assumes "m mod d = r"
   12.78 +  shows "\<exists>q. m = r + q * d"
   12.79 +proof -
   12.80 +  from mod_div_equality obtain q where "q * d + m mod d = m" by blast
   12.81 +  with assms have "m = r + q * d" by simp
   12.82 +  then show ?thesis ..
   12.83 +qed
   12.84  
   12.85  lemma split_div:
   12.86   "P(n div k :: nat) =
   12.87 @@ -1175,7 +1179,7 @@
   12.88          with n j P show "P i" by simp
   12.89        next
   12.90          assume "i \<noteq> 0"
   12.91 -        with not0 n j P show "P i" by(simp add:add_ac)
   12.92 +        with not0 n j P show "P i" by(simp add:ac_simps)
   12.93        qed
   12.94      qed
   12.95    qed
   12.96 @@ -1209,7 +1213,7 @@
   12.97  next
   12.98    assume P: ?lhs
   12.99    then have "divmod_nat_rel m n (q, m - n * q)"
  12.100 -    unfolding divmod_nat_rel_def by (auto simp add: mult_ac)
  12.101 +    unfolding divmod_nat_rel_def by (auto simp add: ac_simps)
  12.102    with divmod_nat_rel_unique divmod_nat_rel [of m n]
  12.103    have "(q, m - n * q) = (m div n, m mod n)" by auto
  12.104    then show ?rhs by simp
  12.105 @@ -1239,7 +1243,7 @@
  12.106      proof (simp, intro allI impI)
  12.107        fix i j
  12.108        assume "n = k*i + j" "j < k"
  12.109 -      thus "P j" using not0 P by(simp add:add_ac mult_ac)
  12.110 +      thus "P j" using not0 P by(simp add:ac_simps ac_simps)
  12.111      qed
  12.112    qed
  12.113  next
  12.114 @@ -1417,7 +1421,7 @@
  12.115  
  12.116    (* Potential use of algebra : Equality modulo n*)
  12.117  lemma mod_mult_self3 [simp]: "(k*n + m) mod n = m mod (n::nat)"
  12.118 -by (simp add: mult_ac add_ac)
  12.119 +by (simp add: ac_simps ac_simps)
  12.120  
  12.121  lemma mod_mult_self4 [simp]: "Suc (k*n + m) mod n = Suc m mod n"
  12.122  proof -
  12.123 @@ -1614,7 +1618,7 @@
  12.124    apply (case_tac "a < b")
  12.125    apply simp_all
  12.126    apply (erule splitE)
  12.127 -  apply (auto simp add: distrib_left Let_def mult_ac mult_2_right)
  12.128 +  apply (auto simp add: distrib_left Let_def ac_simps mult_2_right)
  12.129    done
  12.130  
  12.131  
  12.132 @@ -1644,7 +1648,7 @@
  12.133    apply (case_tac "a + b < (0\<Colon>int)")
  12.134    apply simp_all
  12.135    apply (erule splitE)
  12.136 -  apply (auto simp add: distrib_left Let_def mult_ac mult_2_right)
  12.137 +  apply (auto simp add: distrib_left Let_def ac_simps mult_2_right)
  12.138    done
  12.139  
  12.140  
  12.141 @@ -1744,7 +1748,7 @@
  12.142    val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
  12.143  
  12.144    val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac 
  12.145 -    (@{thm diff_conv_add_uminus} :: @{thms add_0s} @ @{thms add_ac}))
  12.146 +    (@{thm diff_conv_add_uminus} :: @{thms add_0s} @ @{thms ac_simps}))
  12.147  )
  12.148  *}
  12.149  
  12.150 @@ -2072,7 +2076,7 @@
  12.151  lemma zmult1_lemma:
  12.152       "[| divmod_int_rel b c (q, r) |]  
  12.153        ==> divmod_int_rel (a * b) c (a*q + a*r div c, a*r mod c)"
  12.154 -by (auto simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left mult_ac)
  12.155 +by (auto simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left ac_simps)
  12.156  
  12.157  lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
  12.158  apply (case_tac "c = 0", simp)
  12.159 @@ -2176,7 +2180,7 @@
  12.160  
  12.161  lemma zmult2_lemma: "[| divmod_int_rel a b (q, r); 0 < c |]  
  12.162        ==> divmod_int_rel a (b * c) (q div c, b*(q mod c) + r)"
  12.163 -by (auto simp add: mult_ac divmod_int_rel_def linorder_neq_iff
  12.164 +by (auto simp add: mult.assoc divmod_int_rel_def linorder_neq_iff
  12.165                     zero_less_mult_iff distrib_left [symmetric] 
  12.166                     zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: split_if_asm)
  12.167  
    13.1 --- a/src/HOL/Fact.thy	Sat Jul 05 10:09:01 2014 +0200
    13.2 +++ b/src/HOL/Fact.thy	Sat Jul 05 11:01:53 2014 +0200
    13.3 @@ -256,14 +256,10 @@
    13.4    apply (induct k rule: int_ge_induct)
    13.5    apply (simp add: fact_plus_one_int)
    13.6    apply (subst (2) fact_reduce_int)
    13.7 -  apply (auto simp add: add_ac)
    13.8 +  apply (auto simp add: ac_simps)
    13.9    apply (erule order_less_le_trans)
   13.10 -  apply (subst mult_le_cancel_right1)
   13.11    apply auto
   13.12 -  apply (subgoal_tac "fact (i + (1 + m)) >= 0")
   13.13 -  apply force
   13.14 -  apply (rule fact_ge_zero_int)
   13.15 -done
   13.16 +  done
   13.17  
   13.18  lemma fact_less_mono_int: "(0::int) < m \<Longrightarrow> m < n \<Longrightarrow> fact m < fact n"
   13.19    apply (insert fact_less_mono_int_aux [of "n - (m + 1)" "m"])
    14.1 --- a/src/HOL/Fields.thy	Sat Jul 05 10:09:01 2014 +0200
    14.2 +++ b/src/HOL/Fields.thy	Sat Jul 05 11:01:53 2014 +0200
    14.3 @@ -310,7 +310,7 @@
    14.4  lemma inverse_add:
    14.5    "[| a \<noteq> 0;  b \<noteq> 0 |]
    14.6     ==> inverse a + inverse b = (a + b) * inverse a * inverse b"
    14.7 -by (simp add: division_ring_inverse_add mult_ac)
    14.8 +by (simp add: division_ring_inverse_add ac_simps)
    14.9  
   14.10  lemma nonzero_mult_divide_mult_cancel_left [simp]:
   14.11  assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" shows "(c*a)/(c*b) = a/b"
   14.12 @@ -318,7 +318,7 @@
   14.13    have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
   14.14      by (simp add: divide_inverse nonzero_inverse_mult_distrib)
   14.15    also have "... =  a * inverse b * (inverse c * c)"
   14.16 -    by (simp only: mult_ac)
   14.17 +    by (simp only: ac_simps)
   14.18    also have "... =  a * inverse b" by simp
   14.19      finally show ?thesis by (simp add: divide_inverse)
   14.20  qed
   14.21 @@ -328,7 +328,7 @@
   14.22  by (simp add: mult.commute [of _ c])
   14.23  
   14.24  lemma times_divide_eq_left [simp]: "(b / c) * a = (b * a) / c"
   14.25 -  by (simp add: divide_inverse mult_ac)
   14.26 +  by (simp add: divide_inverse ac_simps)
   14.27  
   14.28  text{*It's not obvious whether @{text times_divide_eq} should be
   14.29    simprules or not. Their effect is to gather terms into one big
   14.30 @@ -369,11 +369,11 @@
   14.31  
   14.32  lemma nonzero_mult_divide_mult_cancel_left2 [simp]:
   14.33    "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (c * a) / (b * c) = a / b"
   14.34 -using nonzero_mult_divide_mult_cancel_left [of b c a] by (simp add: mult_ac)
   14.35 +using nonzero_mult_divide_mult_cancel_left [of b c a] by (simp add: ac_simps)
   14.36  
   14.37  lemma nonzero_mult_divide_mult_cancel_right2 [simp]:
   14.38    "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (c * b) = a / b"
   14.39 -using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: mult_ac)
   14.40 +using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: ac_simps)
   14.41  
   14.42  lemma diff_frac_eq:
   14.43    "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y - w / z = (x * z - w * y) / (y * z)"
   14.44 @@ -398,7 +398,7 @@
   14.45    "inverse (a * b) = inverse a * inverse b"
   14.46  proof cases
   14.47    assume "a \<noteq> 0 & b \<noteq> 0" 
   14.48 -  thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_ac)
   14.49 +  thus ?thesis by (simp add: nonzero_inverse_mult_distrib ac_simps)
   14.50  next
   14.51    assume "~ (a \<noteq> 0 & b \<noteq> 0)" 
   14.52    thus ?thesis by force
   14.53 @@ -429,7 +429,7 @@
   14.54  
   14.55  lemma divide_divide_eq_right [simp]:
   14.56    "a / (b / c) = (a * c) / b"
   14.57 -  by (simp add: divide_inverse mult_ac)
   14.58 +  by (simp add: divide_inverse ac_simps)
   14.59  
   14.60  lemma divide_divide_eq_left [simp]:
   14.61    "(a / b) / c = a / (b * c)"
    15.1 --- a/src/HOL/GCD.thy	Sat Jul 05 10:09:01 2014 +0200
    15.2 +++ b/src/HOL/GCD.thy	Sat Jul 05 11:01:53 2014 +0200
    15.3 @@ -1225,7 +1225,7 @@
    15.4            hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)"
    15.5              by (simp only: diff_add_assoc[OF dble, of d, symmetric])
    15.6            hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
    15.7 -            by (simp only: diff_mult_distrib2 add.commute mult_ac)
    15.8 +            by (simp only: diff_mult_distrib2 add.commute ac_simps)
    15.9            hence ?thesis using H(1,2)
   15.10              apply -
   15.11              apply (rule exI[where x=d], simp)
   15.12 @@ -1312,20 +1312,20 @@
   15.13    from pos_k k_m have pos_p: "p > 0" by auto
   15.14    from pos_k k_n have pos_q: "q > 0" by auto
   15.15    have "k * k * gcd q p = k * gcd (k * q) (k * p)"
   15.16 -    by (simp add: mult_ac gcd_mult_distrib_nat)
   15.17 +    by (simp add: ac_simps gcd_mult_distrib_nat)
   15.18    also have "\<dots> = k * gcd (m * p * q) (n * q * p)"
   15.19      by (simp add: k_m [symmetric] k_n [symmetric])
   15.20    also have "\<dots> = k * p * q * gcd m n"
   15.21 -    by (simp add: mult_ac gcd_mult_distrib_nat)
   15.22 +    by (simp add: ac_simps gcd_mult_distrib_nat)
   15.23    finally have "(m * p) * (n * q) * gcd q p = k * p * q * gcd m n"
   15.24      by (simp only: k_m [symmetric] k_n [symmetric])
   15.25    then have "p * q * m * n * gcd q p = p * q * k * gcd m n"
   15.26 -    by (simp add: mult_ac)
   15.27 +    by (simp add: ac_simps)
   15.28    with pos_p pos_q have "m * n * gcd q p = k * gcd m n"
   15.29      by simp
   15.30    with prod_gcd_lcm_nat [of m n]
   15.31    have "lcm m n * gcd q p * gcd m n = k * gcd m n"
   15.32 -    by (simp add: mult_ac)
   15.33 +    by (simp add: ac_simps)
   15.34    with pos_gcd have "lcm m n * gcd q p = k" by auto
   15.35    then show ?thesis using dvd_def by auto
   15.36  qed
   15.37 @@ -1353,7 +1353,7 @@
   15.38      have "gcd m n dvd n" by simp
   15.39      then obtain k where "n = gcd m n * k" using dvd_def by auto
   15.40      then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n"
   15.41 -      by (simp add: mult_ac)
   15.42 +      by (simp add: ac_simps)
   15.43      also have "\<dots> = m * k" using mpos npos gcd_zero_nat by simp
   15.44      finally show ?thesis by (simp add: lcm_nat_def)
   15.45    qed
    16.1 --- a/src/HOL/Groups.thy	Sat Jul 05 10:09:01 2014 +0200
    16.2 +++ b/src/HOL/Groups.thy	Sat Jul 05 11:01:53 2014 +0200
    16.3 @@ -169,14 +169,10 @@
    16.4  
    16.5  declare add.left_commute [algebra_simps, field_simps]
    16.6  
    16.7 -theorems add_ac = add.assoc add.commute add.left_commute
    16.8 -
    16.9  end
   16.10  
   16.11  hide_fact add_commute
   16.12  
   16.13 -theorems add_ac = add.assoc add.commute add.left_commute
   16.14 -
   16.15  class semigroup_mult = times +
   16.16    assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)"
   16.17  begin
   16.18 @@ -197,14 +193,10 @@
   16.19  
   16.20  declare mult.left_commute [algebra_simps, field_simps]
   16.21  
   16.22 -theorems mult_ac = mult.assoc mult.commute mult.left_commute
   16.23 -
   16.24  end
   16.25  
   16.26  hide_fact mult_commute
   16.27  
   16.28 -theorems mult_ac = mult.assoc mult.commute mult.left_commute
   16.29 -
   16.30  class monoid_add = zero + semigroup_add +
   16.31    assumes add_0_left: "0 + a = a"
   16.32      and add_0_right: "a + 0 = a"
    17.1 --- a/src/HOL/Int.thy	Sat Jul 05 10:09:01 2014 +0200
    17.2 +++ b/src/HOL/Int.thy	Sat Jul 05 11:01:53 2014 +0200
    17.3 @@ -518,11 +518,11 @@
    17.4  
    17.5  lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
    17.6    -- {* Unfold all @{text let}s involving constants *}
    17.7 -  unfolding Let_def ..
    17.8 +  by (fact Let_numeral) -- {* FIXME drop *}
    17.9  
   17.10  lemma Let_neg_numeral [simp]: "Let (- numeral v) f = f (- numeral v)"
   17.11    -- {* Unfold all @{text let}s involving constants *}
   17.12 -  unfolding Let_def ..
   17.13 +  by (fact Let_neg_numeral) -- {* FIXME drop *}
   17.14  
   17.15  text {* Unfold @{text min} and @{text max} on numerals. *}
   17.16  
   17.17 @@ -559,7 +559,7 @@
   17.18  proof -
   17.19    have "0 \<le> z" by fact
   17.20    also have "... < z + 1" by (rule less_add_one)
   17.21 -  also have "... = 1 + z" by (simp add: add_ac)
   17.22 +  also have "... = 1 + z" by (simp add: ac_simps)
   17.23    finally show "0 < 1 + z" .
   17.24  qed
   17.25  
    18.1 --- a/src/HOL/Library/BigO.thy	Sat Jul 05 10:09:01 2014 +0200
    18.2 +++ b/src/HOL/Library/BigO.thy	Sat Jul 05 11:01:53 2014 +0200
    18.3 @@ -67,7 +67,7 @@
    18.4    apply (drule_tac x = "xa" in spec)+
    18.5    apply (subgoal_tac "ca * abs (f xa) \<le> ca * (c * abs (g xa))")
    18.6    apply (erule order_trans)
    18.7 -  apply (simp add: mult_ac)
    18.8 +  apply (simp add: ac_simps)
    18.9    apply (rule mult_left_mono, assumption)
   18.10    apply (rule order_less_imp_le, assumption)
   18.11    done
   18.12 @@ -287,7 +287,7 @@
   18.13    apply (rule mult_mono)
   18.14    apply assumption+
   18.15    apply auto
   18.16 -  apply (simp add: mult_ac abs_mult)
   18.17 +  apply (simp add: ac_simps abs_mult)
   18.18    done
   18.19  
   18.20  lemma bigo_mult2 [intro]: "f *o O(g) \<subseteq> O(f * g)"
   18.21 @@ -296,7 +296,7 @@
   18.22    apply auto
   18.23    apply (drule_tac x = x in spec)
   18.24    apply (subgoal_tac "abs (f x) * abs (b x) \<le> abs (f x) * (c * abs (g x))")
   18.25 -  apply (force simp add: mult_ac)
   18.26 +  apply (force simp add: ac_simps)
   18.27    apply (rule mult_left_mono, assumption)
   18.28    apply (rule abs_ge_zero)
   18.29    done
   18.30 @@ -328,7 +328,7 @@
   18.31    also have "(\<lambda>x. 1 / f x) * (f * g) = g"
   18.32      apply (simp add: func_times)
   18.33      apply (rule ext)
   18.34 -    apply (simp add: assms nonzero_divide_eq_eq mult_ac)
   18.35 +    apply (simp add: assms nonzero_divide_eq_eq ac_simps)
   18.36      done
   18.37    finally have "(\<lambda>x. (1::'b) / f x) * h \<in> O(g)" .
   18.38    then have "f * ((\<lambda>x. (1::'b) / f x) * h) \<in> f *o O(g)"
   18.39 @@ -336,7 +336,7 @@
   18.40    also have "f * ((\<lambda>x. (1::'b) / f x) * h) = h"
   18.41      apply (simp add: func_times)
   18.42      apply (rule ext)
   18.43 -    apply (simp add: assms nonzero_divide_eq_eq mult_ac)
   18.44 +    apply (simp add: assms nonzero_divide_eq_eq ac_simps)
   18.45      done
   18.46    finally show "h \<in> f *o O(g)" .
   18.47  qed
   18.48 @@ -432,7 +432,7 @@
   18.49    apply (rule bigo_minus)
   18.50    apply (subst set_minus_plus)
   18.51    apply assumption
   18.52 -  apply (simp add: add_ac)
   18.53 +  apply (simp add: ac_simps)
   18.54    done
   18.55  
   18.56  lemma bigo_add_commute: "f \<in> g +o O(h) \<longleftrightarrow> g \<in> f +o O(h)"
   18.57 @@ -441,7 +441,7 @@
   18.58    done
   18.59  
   18.60  lemma bigo_const1: "(\<lambda>x. c) \<in> O(\<lambda>x. 1)"
   18.61 -  by (auto simp add: bigo_def mult_ac)
   18.62 +  by (auto simp add: bigo_def ac_simps)
   18.63  
   18.64  lemma bigo_const2 [intro]: "O(\<lambda>x. c) \<subseteq> O(\<lambda>x. 1)"
   18.65    apply (rule bigo_elt_subset)
   18.66 @@ -536,7 +536,7 @@
   18.67    apply (rule mult_left_mono)
   18.68    apply (erule spec)
   18.69    apply simp
   18.70 -  apply(simp add: mult_ac)
   18.71 +  apply(simp add: ac_simps)
   18.72    done
   18.73  
   18.74  lemma bigo_const_mult7 [intro]: "f =o O(g) \<Longrightarrow> (\<lambda>x. c * f x) =o O(g)"
    19.1 --- a/src/HOL/Library/Discrete.thy	Sat Jul 05 10:09:01 2014 +0200
    19.2 +++ b/src/HOL/Library/Discrete.thy	Sat Jul 05 11:01:53 2014 +0200
    19.3 @@ -162,7 +162,7 @@
    19.4          case True then have "mono (times q)" by (rule mono_times_nat)
    19.5          then have "q * Max {m. m * m \<le> n} = Max (times q ` {m. m * m \<le> n})"
    19.6            using sqrt_aux [of n] by (auto simp add: power2_eq_square intro: mono_Max_commute)
    19.7 -        then have "Max {m. m * m \<le> n} * q = Max (times q ` {m. m * m \<le> n})" by (simp add: mult_ac)
    19.8 +        then have "Max {m. m * m \<le> n} * q = Max (times q ` {m. m * m \<le> n})" by (simp add: ac_simps)
    19.9          then show ?thesis apply simp
   19.10            apply (subst Max_le_iff)
   19.11            apply auto
    20.1 --- a/src/HOL/Library/Extended_Nat.thy	Sat Jul 05 10:09:01 2014 +0200
    20.2 +++ b/src/HOL/Library/Extended_Nat.thy	Sat Jul 05 11:01:53 2014 +0200
    20.3 @@ -169,10 +169,10 @@
    20.4  lemma plus_1_eSuc:
    20.5    "1 + q = eSuc q"
    20.6    "q + 1 = eSuc q"
    20.7 -  by (simp_all add: eSuc_plus_1 add_ac)
    20.8 +  by (simp_all add: eSuc_plus_1 ac_simps)
    20.9  
   20.10  lemma iadd_Suc: "eSuc m + n = eSuc (m + n)"
   20.11 -  by (simp_all add: eSuc_plus_1 add_ac)
   20.12 +  by (simp_all add: eSuc_plus_1 ac_simps)
   20.13  
   20.14  lemma iadd_Suc_right: "m + eSuc n = eSuc (m + n)"
   20.15    by (simp only: add.commute[of m] iadd_Suc)
   20.16 @@ -523,7 +523,7 @@
   20.17    val trans_tac = Numeral_Simprocs.trans_tac
   20.18    val norm_ss =
   20.19      simpset_of (put_simpset HOL_basic_ss @{context}
   20.20 -      addsimps @{thms add_ac add_0_left add_0_right})
   20.21 +      addsimps @{thms ac_simps add_0_left add_0_right})
   20.22    fun norm_tac ctxt = ALLGOALS (simp_tac (put_simpset norm_ss ctxt))
   20.23    fun simplify_meta_eq ctxt cancel_th th =
   20.24      Arith_Data.simplify_meta_eq [] ctxt
    21.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Sat Jul 05 10:09:01 2014 +0200
    21.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Sat Jul 05 11:01:53 2014 +0200
    21.3 @@ -558,7 +558,7 @@
    21.4    then have "ln y * real k + ln x > 0"
    21.5      by simp
    21.6    then have "exp (real k * ln y + ln x) > exp 0"
    21.7 -    by (simp add: mult_ac)
    21.8 +    by (simp add: ac_simps)
    21.9    then have "y ^ k * x > 1"
   21.10      unfolding exp_zero exp_add exp_real_of_nat_mult exp_ln [OF xp] exp_ln [OF yp]
   21.11      by simp
   21.12 @@ -724,7 +724,7 @@
   21.13    from f0 have if0: "inverse f $ 0 \<noteq> 0" by simp
   21.14    from inverse_mult_eq_1[OF f0] inverse_mult_eq_1[OF if0]
   21.15    have "inverse f * f = inverse f * inverse (inverse f)"
   21.16 -    by (simp add: mult_ac)
   21.17 +    by (simp add: ac_simps)
   21.18    then show ?thesis
   21.19      using f0 unfolding mult_cancel_left by simp
   21.20  qed
   21.21 @@ -736,7 +736,7 @@
   21.22  proof -
   21.23    from inverse_mult_eq_1[OF f0] fg
   21.24    have th0: "inverse f * f = g * f"
   21.25 -    by (simp add: mult_ac)
   21.26 +    by (simp add: ac_simps)
   21.27    then show ?thesis
   21.28      using f0
   21.29      unfolding mult_cancel_right
   21.30 @@ -1400,7 +1400,7 @@
   21.31      using fps_divide_X_minus1_setsum_lemma[of a, symmetric] th0
   21.32      by (simp add: fps_divide_def mult.assoc)
   21.33    also have "\<dots> = (inverse ?X * ?X) * Abs_fps (\<lambda>n::nat. setsum (op $ a) {0..n}) "
   21.34 -    by (simp add: mult_ac)
   21.35 +    by (simp add: ac_simps)
   21.36    finally show ?thesis
   21.37      by (simp add: inverse_mult_eq_1[OF th0])
   21.38  qed
   21.39 @@ -2074,7 +2074,7 @@
   21.40            apply (rule eq_divide_imp')
   21.41            using r00
   21.42            apply (simp del: of_nat_Suc)
   21.43 -          apply (simp add: mult_ac)
   21.44 +          apply (simp add: ac_simps)
   21.45            done
   21.46          then have "a$n = ?r $n"
   21.47            apply (simp del: of_nat_Suc)
   21.48 @@ -2128,7 +2128,7 @@
   21.49    have "fps_deriv (?r ^ Suc k) = fps_deriv a"
   21.50      by simp
   21.51    then have "fps_deriv ?r * ?w = fps_deriv a"
   21.52 -    by (simp add: fps_deriv_power mult_ac del: power_Suc)
   21.53 +    by (simp add: fps_deriv_power ac_simps del: power_Suc)
   21.54    then have "?iw * fps_deriv ?r * ?w = ?iw * fps_deriv a"
   21.55      by simp
   21.56    then have "fps_deriv ?r * (?iw * ?w) = fps_deriv a / ?w"
   21.57 @@ -2294,7 +2294,7 @@
   21.58        setsum (\<lambda>i. of_nat (i + 1) * a$(i+1) * (setsum (\<lambda>j. (b^ i)$j * of_nat (n - j + 1) * b$(n - j + 1)) {0..n})) {0.. n}" .
   21.59  
   21.60      have "(((fps_deriv a) oo b) * (fps_deriv b))$n = setsum (\<lambda>i. (fps_deriv b)$ (n - i) * ((fps_deriv a) oo b)$i) {0..n}"
   21.61 -      unfolding fps_mult_nth by (simp add: mult_ac)
   21.62 +      unfolding fps_mult_nth by (simp add: ac_simps)
   21.63      also have "\<dots> = setsum (\<lambda>i. setsum (\<lambda>j. of_nat (n - i +1) * b$(n - i + 1) * of_nat (j + 1) * a$(j+1) * (b^j)$i) {0..n}) {0..n}"
   21.64        unfolding fps_deriv_nth fps_compose_nth setsum_right_distrib mult.assoc
   21.65        apply (rule setsum.cong)
   21.66 @@ -3532,7 +3532,7 @@
   21.67    apply (subst minus_divide_left)
   21.68    apply (subst eq_divide_iff)
   21.69    apply (simp del: of_nat_add of_nat_Suc)
   21.70 -  apply (simp only: mult_ac)
   21.71 +  apply (simp only: ac_simps)
   21.72    done
   21.73  
   21.74  lemma eq_fps_cos:
   21.75 @@ -3550,7 +3550,7 @@
   21.76    apply (subst minus_divide_left)
   21.77    apply (subst eq_divide_iff)
   21.78    apply (simp del: of_nat_add of_nat_Suc)
   21.79 -  apply (simp only: mult_ac)
   21.80 +  apply (simp only: ac_simps)
   21.81    done
   21.82  
   21.83  lemma mult_nth_0 [simp]: "(a * b) $ 0 = a $ 0 * b $ 0"
   21.84 @@ -3655,7 +3655,7 @@
   21.85  
   21.86  lemma fps_demoivre: "(fps_cos a + fps_const ii * fps_sin a)^n = fps_cos (of_nat n * a) + fps_const ii * fps_sin (of_nat n * a)"
   21.87    unfolding Eii_sin_cos[symmetric] E_power_mult
   21.88 -  by (simp add: mult_ac)
   21.89 +  by (simp add: ac_simps)
   21.90  
   21.91  
   21.92  subsection {* Hypergeometric series *}
    22.1 --- a/src/HOL/Library/Fraction_Field.thy	Sat Jul 05 10:09:01 2014 +0200
    22.2 +++ b/src/HOL/Library/Fraction_Field.thy	Sat Jul 05 11:01:53 2014 +0200
    22.3 @@ -31,11 +31,11 @@
    22.4    fix a b a' b' a'' b'' :: 'a
    22.5    assume A: "((a, b), (a', b')) \<in> fractrel"
    22.6    assume B: "((a', b'), (a'', b'')) \<in> fractrel"
    22.7 -  have "b' * (a * b'') = b'' * (a * b')" by (simp add: mult_ac)
    22.8 +  have "b' * (a * b'') = b'' * (a * b')" by (simp add: ac_simps)
    22.9    also from A have "a * b' = a' * b" by auto
   22.10 -  also have "b'' * (a' * b) = b * (a' * b'')" by (simp add: mult_ac)
   22.11 +  also have "b'' * (a' * b) = b * (a' * b'')" by (simp add: ac_simps)
   22.12    also from B have "a' * b'' = a'' * b'" by auto
   22.13 -  also have "b * (a'' * b') = b' * (a'' * b)" by (simp add: mult_ac)
   22.14 +  also have "b * (a'' * b') = b' * (a'' * b)" by (simp add: ac_simps)
   22.15    finally have "b' * (a * b'') = b' * (a'' * b)" .
   22.16    moreover from B have "b' \<noteq> 0" by auto
   22.17    ultimately have "a * b'' = a'' * b" by simp
   22.18 @@ -288,7 +288,7 @@
   22.19            ((a * d) * (b * d) * (x * x) \<le> (c * b) * (b * d) * (x * x))"
   22.20          by (simp add: mult_le_cancel_right)
   22.21        also have "... = ?le (a * x) (b * x) c d"
   22.22 -        by (simp add: mult_ac)
   22.23 +        by (simp add: ac_simps)
   22.24        finally show ?thesis .
   22.25      qed
   22.26    } note le_factor = this
   22.27 @@ -299,11 +299,11 @@
   22.28    then have "?le a b c d = ?le (a * ?D') (b * ?D') c d"
   22.29      by (rule le_factor)
   22.30    also have "... = ((a * b') * ?D * ?D' * d * d' \<le> (c * d') * ?D * ?D' * b * b')"
   22.31 -    by (simp add: mult_ac)
   22.32 +    by (simp add: ac_simps)
   22.33    also have "... = ((a' * b) * ?D * ?D' * d * d' \<le> (c' * d) * ?D * ?D' * b * b')"
   22.34      by (simp only: eq1 eq2)
   22.35    also have "... = ?le (a' * ?D) (b' * ?D) c' d'"
   22.36 -    by (simp add: mult_ac)
   22.37 +    by (simp add: ac_simps)
   22.38    also from D have "... = ?le a' b' c' d'"
   22.39      by (rule le_factor [symmetric])
   22.40    finally show "?le a b c d = ?le a' b' c' d'" .
   22.41 @@ -328,7 +328,7 @@
   22.42    assumes "b \<noteq> 0"
   22.43      and "d \<noteq> 0"
   22.44    shows "Fract a b < Fract c d \<longleftrightarrow> (a * d) * (b * d) < (c * b) * (b * d)"
   22.45 -  by (simp add: less_fract_def less_le_not_le mult_ac assms)
   22.46 +  by (simp add: less_fract_def less_le_not_le ac_simps assms)
   22.47  
   22.48  instance
   22.49  proof
   22.50 @@ -351,7 +351,7 @@
   22.51          with ff show ?thesis by (simp add: mult_le_cancel_right)
   22.52        qed
   22.53        also have "... = (c * f) * (d * f) * (b * b)"
   22.54 -        by (simp only: mult_ac)
   22.55 +        by (simp only: ac_simps)
   22.56        also have "... \<le> (e * d) * (d * f) * (b * b)"
   22.57        proof -
   22.58          from neq 2 have "(c * f) * (d * f) \<le> (e * d) * (d * f)"
   22.59 @@ -359,7 +359,7 @@
   22.60          with bb show ?thesis by (simp add: mult_le_cancel_right)
   22.61        qed
   22.62        finally have "(a * f) * (b * f) * (d * d) \<le> e * b * (b * f) * (d * d)"
   22.63 -        by (simp only: mult_ac)
   22.64 +        by (simp only: ac_simps)
   22.65        with dd have "(a * f) * (b * f) \<le> (e * b) * (b * f)"
   22.66          by (simp add: mult_le_cancel_right)
   22.67        with neq show ?thesis by simp
   22.68 @@ -382,7 +382,7 @@
   22.69        proof -
   22.70          from neq 2 have "(c * b) * (d * b) \<le> (a * d) * (d * b)"
   22.71            by simp
   22.72 -        then show ?thesis by (simp only: mult_ac)
   22.73 +        then show ?thesis by (simp only: ac_simps)
   22.74        qed
   22.75        finally have "(a * d) * (b * d) = (c * b) * (b * d)" .
   22.76        moreover from neq have "b * d \<noteq> 0" by simp
   22.77 @@ -469,7 +469,7 @@
   22.78        ultimately have "(a * d) * (b * d) * ?E * ?F < (c * b) * (b * d) * ?E * ?F"
   22.79          by (simp add: mult_less_cancel_right)
   22.80        with neq show ?thesis
   22.81 -        by (simp add: mult_ac)
   22.82 +        by (simp add: ac_simps)
   22.83      qed
   22.84    qed
   22.85  qed
    23.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sat Jul 05 10:09:01 2014 +0200
    23.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sat Jul 05 11:01:53 2014 +0200
    23.3 @@ -732,7 +732,7 @@
    23.4      {
    23.5        fix w
    23.6        have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w / ?a0) < 1"
    23.7 -        using qr[rule_format, of w] a00 by (simp add: divide_inverse mult_ac)
    23.8 +        using qr[rule_format, of w] a00 by (simp add: divide_inverse ac_simps)
    23.9        also have "\<dots> \<longleftrightarrow> cmod (poly q w) < cmod ?a0"
   23.10          using a00 unfolding norm_divide by (simp add: field_simps)
   23.11        finally have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w) < cmod ?a0" .
   23.12 @@ -980,7 +980,7 @@
   23.13                  have "p = [:- a, 1:] ^ (Suc ?op) * u"
   23.14                    apply (subst s)
   23.15                    apply (subst u)
   23.16 -                  apply (simp only: power_Suc mult_ac)
   23.17 +                  apply (simp only: power_Suc ac_simps)
   23.18                    done
   23.19                  with ap(2)[unfolded dvd_def] have False
   23.20                    by blast
   23.21 @@ -1010,7 +1010,7 @@
   23.22                apply (subst mult.assoc [where a=u])
   23.23                apply (subst mult.assoc [where b=u, symmetric])
   23.24                apply (subst u [symmetric])
   23.25 -              apply (simp add: mult_ac power_add [symmetric])
   23.26 +              apply (simp add: ac_simps power_add [symmetric])
   23.27                done
   23.28              then have ?ths
   23.29                unfolding dvd_def by blast
    24.1 --- a/src/HOL/Library/Inner_Product.thy	Sat Jul 05 10:09:01 2014 +0200
    24.2 +++ b/src/HOL/Library/Inner_Product.thy	Sat Jul 05 11:01:53 2014 +0200
    24.3 @@ -280,7 +280,7 @@
    24.4       \<Longrightarrow> GDERIV (\<lambda>x. g (f x)) x :> scaleR dg df"
    24.5    unfolding gderiv_def has_field_derivative_def
    24.6    apply (drule (1) has_derivative_compose)
    24.7 -  apply (simp add: mult_ac)
    24.8 +  apply (simp add: ac_simps)
    24.9    done
   24.10  
   24.11  lemma has_derivative_subst: "\<lbrakk>FDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> FDERIV f x :> d"
   24.12 @@ -313,7 +313,7 @@
   24.13    unfolding gderiv_def has_field_derivative_def inner_add_right inner_scaleR_right
   24.14    apply (rule has_derivative_subst)
   24.15    apply (erule (1) has_derivative_scaleR)
   24.16 -  apply (simp add: mult_ac)
   24.17 +  apply (simp add: ac_simps)
   24.18    done
   24.19  
   24.20  lemma GDERIV_mult:
   24.21 @@ -322,7 +322,7 @@
   24.22    unfolding gderiv_def
   24.23    apply (rule has_derivative_subst)
   24.24    apply (erule (1) has_derivative_mult)
   24.25 -  apply (simp add: inner_add mult_ac)
   24.26 +  apply (simp add: inner_add ac_simps)
   24.27    done
   24.28  
   24.29  lemma GDERIV_inverse:
    25.1 --- a/src/HOL/Library/Multiset.thy	Sat Jul 05 10:09:01 2014 +0200
    25.2 +++ b/src/HOL/Library/Multiset.thy	Sat Jul 05 11:01:53 2014 +0200
    25.3 @@ -717,7 +717,7 @@
    25.4      by (blast dest: multi_member_split)
    25.5    have "A + {#b#} = A + {#b#} + {#c#} - {#c#}" by simp
    25.6    then have "A + {#b#} = A + {#c#} + {#b#} - {#c#}" 
    25.7 -    by (simp add: add_ac)
    25.8 +    by (simp add: ac_simps)
    25.9    then show ?thesis using B by simp
   25.10  qed
   25.11  
   25.12 @@ -817,7 +817,7 @@
   25.13  next
   25.14    case (add M x)
   25.15    have "M + {#x#} + N = (M + N) + {#x#}"
   25.16 -    by (simp add: add_ac)
   25.17 +    by (simp add: ac_simps)
   25.18    with add show ?case by (simp add: fold_mset_insert fold_mset_fun_left_comm)
   25.19  qed
   25.20  
   25.21 @@ -851,7 +851,7 @@
   25.22  lemma comp_fun_commute_mset_image:
   25.23    "comp_fun_commute (plus o single o f)"
   25.24  proof
   25.25 -qed (simp add: add_ac fun_eq_iff)
   25.26 +qed (simp add: ac_simps fun_eq_iff)
   25.27  
   25.28  lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
   25.29    by (simp add: image_mset_def)
   25.30 @@ -868,7 +868,7 @@
   25.31  proof -
   25.32    interpret comp_fun_commute "plus o single o f"
   25.33      by (fact comp_fun_commute_mset_image)
   25.34 -  show ?thesis by (induct N) (simp_all add: image_mset_def add_ac)
   25.35 +  show ?thesis by (induct N) (simp_all add: image_mset_def ac_simps)
   25.36  qed
   25.37  
   25.38  corollary image_mset_insert:
   25.39 @@ -956,7 +956,7 @@
   25.40  
   25.41  lemma multiset_of_append [simp]:
   25.42    "multiset_of (xs @ ys) = multiset_of xs + multiset_of ys"
   25.43 -  by (induct xs arbitrary: ys) (auto simp: add_ac)
   25.44 +  by (induct xs arbitrary: ys) (auto simp: ac_simps)
   25.45  
   25.46  lemma multiset_of_filter:
   25.47    "multiset_of (filter P xs) = {#x :# multiset_of xs. P x #}"
   25.48 @@ -1008,7 +1008,7 @@
   25.49  
   25.50  lemma multiset_of_compl_union [simp]:
   25.51    "multiset_of [x\<leftarrow>xs. P x] + multiset_of [x\<leftarrow>xs. \<not>P x] = multiset_of xs"
   25.52 -  by (induct xs) (auto simp: add_ac)
   25.53 +  by (induct xs) (auto simp: ac_simps)
   25.54  
   25.55  lemma count_multiset_of_length_filter:
   25.56    "count (multiset_of xs) x = length (filter (\<lambda>y. x = y) xs)"
   25.57 @@ -1552,7 +1552,7 @@
   25.58      next
   25.59        fix K'
   25.60        assume "M0' = K' + {#a#}"
   25.61 -      with N have n: "N = K' + K + {#a#}" by (simp add: add_ac)
   25.62 +      with N have n: "N = K' + K + {#a#}" by (simp add: ac_simps)
   25.63  
   25.64        assume "M0 = K' + {#a'#}"
   25.65        with r have "?R (K' + K) M0" by blast
   25.66 @@ -1701,7 +1701,7 @@
   25.67  apply (simp add: mult1_def set_of_def)
   25.68  apply (rule_tac x = a in exI)
   25.69  apply (rule_tac x = "I + J'" in exI)
   25.70 -apply (simp add: add_ac)
   25.71 +apply (simp add: ac_simps)
   25.72  done
   25.73  
   25.74  lemma one_step_implies_mult:
   25.75 @@ -1840,14 +1840,14 @@
   25.76        "{#x#} + X = A + ({#y#}+Z) 
   25.77        \<and> {#y#} + Y = B + ({#y#}+Z)
   25.78        \<and> ((set_of A, set_of B) \<in> max_strict \<or> (B = {#} \<and> A = {#}))"
   25.79 -      by (auto simp: add_ac)
   25.80 +      by (auto simp: ac_simps)
   25.81      thus ?case by (intro exI)
   25.82    next
   25.83      assume A: "(x, y) \<in> pair_less"
   25.84      let ?A' = "{#x#} + A" and ?B' = "{#y#} + B"
   25.85      have "{#x#} + X = ?A' + Z"
   25.86        "{#y#} + Y = ?B' + Z"
   25.87 -      by (auto simp add: add_ac)
   25.88 +      by (auto simp add: ac_simps)
   25.89      moreover have 
   25.90        "(set_of ?A', set_of ?B') \<in> max_strict"
   25.91        using 1 A unfolding max_strict_def 
   25.92 @@ -1880,12 +1880,12 @@
   25.93        assume [simp]: "A' = {#} \<and> B' = {#}"
   25.94        show ?thesis by (rule smsI) (auto intro: max)
   25.95      qed
   25.96 -    thus "(Z + A, Z' + B) \<in> ms_strict" by (simp add:add_ac)
   25.97 +    thus "(Z + A, Z' + B) \<in> ms_strict" by (simp add:ac_simps)
   25.98      thus "(Z + A, Z' + B) \<in> ms_weak" by (simp add: ms_weak_def)
   25.99    }
  25.100    from mx_or_empty
  25.101    have "(Z'' + A', Z'' + B') \<in> ms_weak" by (rule wmsI)
  25.102 -  thus "(Z + {#}, Z' + {#}) \<in> ms_weak" by (simp add:add_ac)
  25.103 +  thus "(Z + {#}, Z' + {#}) \<in> ms_weak" by (simp add:ac_simps)
  25.104  qed
  25.105  
  25.106  lemma empty_neutral: "{#} + x = x" "x + {#} = x"
  25.107 @@ -1914,7 +1914,7 @@
  25.108  
  25.109    val regroup_munion_conv =
  25.110        Function_Lib.regroup_conv @{const_abbrev Mempty} @{const_name plus}
  25.111 -        (map (fn t => t RS eq_reflection) (@{thms add_ac} @ @{thms empty_neutral}))
  25.112 +        (map (fn t => t RS eq_reflection) (@{thms ac_simps} @ @{thms empty_neutral}))
  25.113  
  25.114    fun unfold_pwleq_tac i =
  25.115      (rtac @{thm pw_leq_step} i THEN (fn st => unfold_pwleq_tac (i + 1) st))
    26.1 --- a/src/HOL/Library/Numeral_Type.thy	Sat Jul 05 10:09:01 2014 +0200
    26.2 +++ b/src/HOL/Library/Numeral_Type.thy	Sat Jul 05 11:01:53 2014 +0200
    26.3 @@ -147,7 +147,7 @@
    26.4  lemma of_nat_eq: "of_nat k = Abs (int k mod n)"
    26.5  apply (induct k)
    26.6  apply (simp add: zero_def)
    26.7 -apply (simp add: Rep_simps add_def one_def zmod_simps add_ac)
    26.8 +apply (simp add: Rep_simps add_def one_def zmod_simps ac_simps)
    26.9  done
   26.10  
   26.11  lemma of_int_eq: "of_int z = Abs (z mod n)"
    27.1 --- a/src/HOL/Library/RBT_Set.thy	Sat Jul 05 10:09:01 2014 +0200
    27.2 +++ b/src/HOL/Library/RBT_Set.thy	Sat Jul 05 11:01:53 2014 +0200
    27.3 @@ -657,7 +657,7 @@
    27.4  lemma setsum_Set [code]:
    27.5    "setsum f (Set xs) = fold_keys (plus o f) xs 0"
    27.6  proof -
    27.7 -  have "comp_fun_commute (\<lambda>x. op + (f x))" by default (auto simp: add_ac)
    27.8 +  have "comp_fun_commute (\<lambda>x. op + (f x))" by default (auto simp: ac_simps)
    27.9    then show ?thesis 
   27.10      by (auto simp add: setsum.eq_fold finite_fold_fold_keys o_def)
   27.11  qed
    28.1 --- a/src/HOL/Library/Set_Algebras.thy	Sat Jul 05 10:09:01 2014 +0200
    28.2 +++ b/src/HOL/Library/Set_Algebras.thy	Sat Jul 05 11:01:53 2014 +0200
    28.3 @@ -100,11 +100,11 @@
    28.4  
    28.5  lemma set_plus_rearrange:
    28.6    "((a::'a::comm_monoid_add) +o C) + (b +o D) = (a + b) +o (C + D)"
    28.7 -  apply (auto simp add: elt_set_plus_def set_plus_def add_ac)
    28.8 +  apply (auto simp add: elt_set_plus_def set_plus_def ac_simps)
    28.9     apply (rule_tac x = "ba + bb" in exI)
   28.10 -  apply (auto simp add: add_ac)
   28.11 +  apply (auto simp add: ac_simps)
   28.12    apply (rule_tac x = "aa + a" in exI)
   28.13 -  apply (auto simp add: add_ac)
   28.14 +  apply (auto simp add: ac_simps)
   28.15    done
   28.16  
   28.17  lemma set_plus_rearrange2: "(a::'a::semigroup_add) +o (b +o C) = (a + b) +o C"
   28.18 @@ -112,19 +112,19 @@
   28.19  
   28.20  lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) + C = a +o (B + C)"
   28.21    apply (auto simp add: elt_set_plus_def set_plus_def)
   28.22 -   apply (blast intro: add_ac)
   28.23 +   apply (blast intro: ac_simps)
   28.24    apply (rule_tac x = "a + aa" in exI)
   28.25    apply (rule conjI)
   28.26     apply (rule_tac x = "aa" in bexI)
   28.27      apply auto
   28.28    apply (rule_tac x = "ba" in bexI)
   28.29 -   apply (auto simp add: add_ac)
   28.30 +   apply (auto simp add: ac_simps)
   28.31    done
   28.32  
   28.33  theorem set_plus_rearrange4: "C + ((a::'a::comm_monoid_add) +o D) = a +o (C + D)"
   28.34 -  apply (auto simp add: elt_set_plus_def set_plus_def add_ac)
   28.35 +  apply (auto simp add: elt_set_plus_def set_plus_def ac_simps)
   28.36     apply (rule_tac x = "aa + ba" in exI)
   28.37 -   apply (auto simp add: add_ac)
   28.38 +   apply (auto simp add: ac_simps)
   28.39    done
   28.40  
   28.41  theorems set_plus_rearranges = set_plus_rearrange set_plus_rearrange2
   28.42 @@ -140,7 +140,7 @@
   28.43    by (auto simp add: elt_set_plus_def set_plus_def)
   28.44  
   28.45  lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) \<in> C \<Longrightarrow> a +o D \<subseteq> D + C"
   28.46 -  by (auto simp add: elt_set_plus_def set_plus_def add_ac)
   28.47 +  by (auto simp add: elt_set_plus_def set_plus_def ac_simps)
   28.48  
   28.49  lemma set_plus_mono5: "a \<in> C \<Longrightarrow> B \<subseteq> D \<Longrightarrow> a +o B \<subseteq> C + D"
   28.50    apply (subgoal_tac "a +o B \<subseteq> a +o D")
   28.51 @@ -178,17 +178,17 @@
   28.52    apply (auto simp add: set_plus_def)
   28.53    apply (rule_tac x = 0 in bexI)
   28.54     apply (rule_tac x = x in bexI)
   28.55 -    apply (auto simp add: add_ac)
   28.56 +    apply (auto simp add: ac_simps)
   28.57    done
   28.58  
   28.59  lemma set_plus_imp_minus: "(a::'a::ab_group_add) : b +o C \<Longrightarrow> (a - b) \<in> C"
   28.60 -  by (auto simp add: elt_set_plus_def add_ac)
   28.61 +  by (auto simp add: elt_set_plus_def ac_simps)
   28.62  
   28.63  lemma set_minus_imp_plus: "(a::'a::ab_group_add) - b : C \<Longrightarrow> a \<in> b +o C"
   28.64 -  apply (auto simp add: elt_set_plus_def add_ac)
   28.65 +  apply (auto simp add: elt_set_plus_def ac_simps)
   28.66    apply (subgoal_tac "a = (a + - b) + b")
   28.67     apply (rule bexI, assumption)
   28.68 -  apply (auto simp add: add_ac)
   28.69 +  apply (auto simp add: ac_simps)
   28.70    done
   28.71  
   28.72  lemma set_minus_plus: "(a::'a::ab_group_add) - b \<in> C \<longleftrightarrow> a \<in> b +o C"
   28.73 @@ -209,9 +209,9 @@
   28.74    "((a::'a::comm_monoid_mult) *o C) * (b *o D) = (a * b) *o (C * D)"
   28.75    apply (auto simp add: elt_set_times_def set_times_def)
   28.76     apply (rule_tac x = "ba * bb" in exI)
   28.77 -   apply (auto simp add: mult_ac)
   28.78 +   apply (auto simp add: ac_simps)
   28.79    apply (rule_tac x = "aa * a" in exI)
   28.80 -  apply (auto simp add: mult_ac)
   28.81 +  apply (auto simp add: ac_simps)
   28.82    done
   28.83  
   28.84  lemma set_times_rearrange2:
   28.85 @@ -221,20 +221,20 @@
   28.86  lemma set_times_rearrange3:
   28.87    "((a::'a::semigroup_mult) *o B) * C = a *o (B * C)"
   28.88    apply (auto simp add: elt_set_times_def set_times_def)
   28.89 -   apply (blast intro: mult_ac)
   28.90 +   apply (blast intro: ac_simps)
   28.91    apply (rule_tac x = "a * aa" in exI)
   28.92    apply (rule conjI)
   28.93     apply (rule_tac x = "aa" in bexI)
   28.94      apply auto
   28.95    apply (rule_tac x = "ba" in bexI)
   28.96 -   apply (auto simp add: mult_ac)
   28.97 +   apply (auto simp add: ac_simps)
   28.98    done
   28.99  
  28.100  theorem set_times_rearrange4:
  28.101    "C * ((a::'a::comm_monoid_mult) *o D) = a *o (C * D)"
  28.102 -  apply (auto simp add: elt_set_times_def set_times_def mult_ac)
  28.103 +  apply (auto simp add: elt_set_times_def set_times_def ac_simps)
  28.104     apply (rule_tac x = "aa * ba" in exI)
  28.105 -   apply (auto simp add: mult_ac)
  28.106 +   apply (auto simp add: ac_simps)
  28.107    done
  28.108  
  28.109  theorems set_times_rearranges = set_times_rearrange set_times_rearrange2
  28.110 @@ -250,7 +250,7 @@
  28.111    by (auto simp add: elt_set_times_def set_times_def)
  28.112  
  28.113  lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C \<Longrightarrow> a *o D \<subseteq> D * C"
  28.114 -  by (auto simp add: elt_set_times_def set_times_def mult_ac)
  28.115 +  by (auto simp add: elt_set_times_def set_times_def ac_simps)
  28.116  
  28.117  lemma set_times_mono5: "a \<in> C \<Longrightarrow> B \<subseteq> D \<Longrightarrow> a *o B \<subseteq> C * D"
  28.118    apply (subgoal_tac "a *o B \<subseteq> a *o D")
    29.1 --- a/src/HOL/List.thy	Sat Jul 05 10:09:01 2014 +0200
    29.2 +++ b/src/HOL/List.thy	Sat Jul 05 11:01:53 2014 +0200
    29.3 @@ -2104,13 +2104,13 @@
    29.4  by (simp add: butlast_conv_take min.absorb1 min.absorb2)
    29.5  
    29.6  lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)"
    29.7 -by (simp add: butlast_conv_take drop_take add_ac)
    29.8 +by (simp add: butlast_conv_take drop_take ac_simps)
    29.9  
   29.10  lemma take_butlast: "n < length xs ==> take n (butlast xs) = take n xs"
   29.11  by (simp add: butlast_conv_take min.absorb1)
   29.12  
   29.13  lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)"
   29.14 -by (simp add: butlast_conv_take drop_take add_ac)
   29.15 +by (simp add: butlast_conv_take drop_take ac_simps)
   29.16  
   29.17  lemma hd_drop_conv_nth: "n < length xs \<Longrightarrow> hd(drop n xs) = xs!n"
   29.18  by(simp add: hd_conv_nth)
   29.19 @@ -3471,7 +3471,7 @@
   29.20  
   29.21  lemma (in comm_monoid_add) listsum_rev [simp]:
   29.22    "listsum (rev xs) = listsum xs"
   29.23 -  by (simp add: listsum_def foldr_fold fold_rev fun_eq_iff add_ac)
   29.24 +  by (simp add: listsum_def foldr_fold fold_rev fun_eq_iff ac_simps)
   29.25  
   29.26  lemma (in monoid_add) fold_plus_listsum_rev:
   29.27    "fold plus xs = plus (listsum (rev xs))"
    30.1 --- a/src/HOL/MacLaurin.thy	Sat Jul 05 10:09:01 2014 +0200
    30.2 +++ b/src/HOL/MacLaurin.thy	Sat Jul 05 11:01:53 2014 +0200
    30.3 @@ -574,7 +574,7 @@
    30.4      apply (rule setsum.cong[OF refl])
    30.5      apply (subst diff_m_0, simp)
    30.6      apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono
    30.7 -                simp add: est mult_ac divide_inverse power_abs [symmetric] abs_mult)
    30.8 +                simp add: est ac_simps divide_inverse power_abs [symmetric] abs_mult)
    30.9      done
   30.10  qed
   30.11  
    31.1 --- a/src/HOL/Metis_Examples/Big_O.thy	Sat Jul 05 10:09:01 2014 +0200
    31.2 +++ b/src/HOL/Metis_Examples/Big_O.thy	Sat Jul 05 11:01:53 2014 +0200
    31.3 @@ -301,7 +301,7 @@
    31.4  lemma bigo_mult [intro]: "O(f) * O(g) <= O(f * g)"
    31.5  apply (rule subsetI)
    31.6  apply (subst bigo_def)
    31.7 -apply (auto simp del: abs_mult mult_ac
    31.8 +apply (auto simp del: abs_mult ac_simps
    31.9              simp add: bigo_alt_def set_times_def func_times)
   31.10  (* sledgehammer *)
   31.11  apply (rule_tac x = "c * ca" in exI)
   31.12 @@ -334,7 +334,7 @@
   31.13        by (rule bigo_mult2)
   31.14      also have "(\<lambda>x. 1 / f x) * (f * g) = g"
   31.15        apply (simp add: func_times)
   31.16 -      by (metis (lifting, no_types) a ext mult_ac(2) nonzero_divide_eq_eq)
   31.17 +      by (metis (lifting, no_types) a ext mult.commute nonzero_divide_eq_eq)
   31.18      finally have "(\<lambda>x. (1\<Colon>'b) / f x) * h : O(g)".
   31.19      then have "f * ((\<lambda>x. (1\<Colon>'b) / f x) * h) : f *o O(g)"
   31.20        by auto
   31.21 @@ -396,7 +396,7 @@
   31.22  by (metis bigo_add_commute_imp)
   31.23  
   31.24  lemma bigo_const1: "(\<lambda>x. c) : O(\<lambda>x. 1)"
   31.25 -by (auto simp add: bigo_def mult_ac)
   31.26 +by (auto simp add: bigo_def ac_simps)
   31.27  
   31.28  lemma bigo_const2 [intro]: "O(\<lambda>x. c) \<le> O(\<lambda>x. 1)"
   31.29  by (metis bigo_const1 bigo_elt_subset)
   31.30 @@ -462,13 +462,13 @@
   31.31    hence "\<exists>(v\<Colon>'a) (u\<Colon>'a) SKF\<^sub>7\<Colon>'a \<Rightarrow> 'b. \<bar>inverse c\<bar> * \<bar>g (SKF\<^sub>7 (u * v))\<bar> \<le> u * (v * \<bar>f (SKF\<^sub>7 (u * v))\<bar>)"
   31.32      by (metis comm_mult_left_mono)
   31.33    thus "\<exists>ca\<Colon>'a. \<forall>x\<Colon>'b. \<bar>inverse c\<bar> * \<bar>g x\<bar> \<le> ca * \<bar>f x\<bar>"
   31.34 -    using A2 F4 by (metis ab_semigroup_mult_class.mult_ac(1) comm_mult_left_mono)
   31.35 +    using A2 F4 by (metis mult.assoc comm_mult_left_mono)
   31.36  qed
   31.37  
   31.38  lemma bigo_const_mult6 [intro]: "(\<lambda>x. c) *o O(f) <= O(f)"
   31.39    apply (auto intro!: subsetI
   31.40      simp add: bigo_def elt_set_times_def func_times
   31.41 -    simp del: abs_mult mult_ac)
   31.42 +    simp del: abs_mult ac_simps)
   31.43  (* sledgehammer *)
   31.44    apply (rule_tac x = "ca * (abs c)" in exI)
   31.45    apply (rule allI)
   31.46 @@ -478,7 +478,7 @@
   31.47    apply (rule mult_left_mono)
   31.48    apply (erule spec)
   31.49    apply simp
   31.50 -  apply (simp add: mult_ac)
   31.51 +  apply (simp add: ac_simps)
   31.52  done
   31.53  
   31.54  lemma bigo_const_mult7 [intro]: "f =o O(g) \<Longrightarrow> (\<lambda>x. c * f x) =o O(g)"
    32.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sat Jul 05 10:09:01 2014 +0200
    32.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sat Jul 05 11:01:53 2014 +0200
    32.3 @@ -418,7 +418,7 @@
    32.4    by (simp add: matrix_vector_mult_def inner_vec_def)
    32.5  
    32.6  lemma dot_lmul_matrix: "((x::real ^_) v* A) \<bullet> y = x \<bullet> (A *v y)"
    32.7 -  apply (simp add: inner_vec_def matrix_vector_mult_def vector_matrix_mult_def setsum_left_distrib setsum_right_distrib mult_ac)
    32.8 +  apply (simp add: inner_vec_def matrix_vector_mult_def vector_matrix_mult_def setsum_left_distrib setsum_right_distrib ac_simps)
    32.9    apply (subst setsum.commute)
   32.10    apply simp
   32.11    done
   32.12 @@ -525,7 +525,7 @@
   32.13    apply (simp add: transpose_def inner_vec_def matrix_vector_mult_def
   32.14      setsum_left_distrib setsum_right_distrib)
   32.15    apply (subst setsum.commute)
   32.16 -  apply (auto simp add: mult_ac)
   32.17 +  apply (auto simp add: ac_simps)
   32.18    done
   32.19  
   32.20  lemma matrix_adjoint: assumes lf: "linear (f :: real^'n \<Rightarrow> real ^'m)"
   32.21 @@ -1221,7 +1221,7 @@
   32.22    unfolding UNIV_2 by simp
   32.23  
   32.24  lemma setsum_3: "setsum f (UNIV::3 set) = f 1 + f 2 + f 3"
   32.25 -  unfolding UNIV_3 by (simp add: add_ac)
   32.26 +  unfolding UNIV_3 by (simp add: ac_simps)
   32.27  
   32.28  instantiation num1 :: cart_one
   32.29  begin
    33.1 --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Sat Jul 05 10:09:01 2014 +0200
    33.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Sat Jul 05 11:01:53 2014 +0200
    33.3 @@ -1019,7 +1019,7 @@
    33.4                     (of_nat (Suc n) * (f (Suc n) u * (z-u) ^ n)) +
    33.5                     (f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)) -
    33.6                     (f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n))"
    33.7 -          by (simp only: fact_Suc of_nat_mult mult_ac) simp
    33.8 +          by (simp only: fact_Suc of_nat_mult ac_simps) simp
    33.9          also have "... = f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)"
   33.10            by (simp add: algebra_simps)
   33.11          finally show ?thesis
   33.12 @@ -1116,7 +1116,7 @@
   33.13               (\<Sum>i = 0..n.
   33.14                   f (Suc (Suc i)) u * ((z-u) ^ Suc i) / of_nat (fact (Suc i))  - 
   33.15                   f (Suc i) u * (z-u) ^ i / of_nat (fact i))"
   33.16 -      by (simp only: diff_divide_distrib fact_cancel mult_ac)
   33.17 +      by (simp only: diff_divide_distrib fact_cancel ac_simps)
   33.18      also have "... = f (Suc 0) u -
   33.19               (f (Suc (Suc n)) u * (z-u) ^ Suc n - of_nat (Suc n) * (z-u) ^ n * f (Suc n) u) /
   33.20               of_nat (fact (Suc n)) +
   33.21 @@ -1132,7 +1132,7 @@
   33.22        apply (intro derivative_eq_intros)+
   33.23        apply (force intro: u assms)
   33.24        apply (rule refl)+
   33.25 -      apply (auto simp: mult_ac)
   33.26 +      apply (auto simp: ac_simps)
   33.27        done
   33.28    }
   33.29    then show ?thesis
    34.1 --- a/src/HOL/Multivariate_Analysis/Determinants.thy	Sat Jul 05 10:09:01 2014 +0200
    34.2 +++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Sat Jul 05 11:01:53 2014 +0200
    34.3 @@ -476,7 +476,7 @@
    34.4    also have "\<dots> = (c*s a k) $ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk"
    34.5      by (simp add: field_simps)
    34.6    also have "\<dots> = c* (a k $ p k * setprod (\<lambda>i. ?g i $ p i) ?Uk)"
    34.7 -    unfolding th1 by (simp add: mult_ac)
    34.8 +    unfolding th1 by (simp add: ac_simps)
    34.9    also have "\<dots> = c* (setprod (\<lambda>i. ?g i $ p i) (insert k ?Uk))"
   34.10      unfolding setprod.insert[OF th3] by simp
   34.11    finally have "setprod (\<lambda>i. ?f i $ p i) ?U = c* (setprod (\<lambda>i. ?g i $ p i) ?U)"
   34.12 @@ -824,7 +824,7 @@
   34.13          by (simp_all add: sign_idempotent)
   34.14        have ths: "?s q = ?s p * ?s (q \<circ> inv p)"
   34.15          using pp pq permutation_inverse[OF pp] sign_inverse[OF pp]
   34.16 -        by (simp add:  th00 mult_ac sign_idempotent sign_compose)
   34.17 +        by (simp add:  th00 ac_simps sign_idempotent sign_compose)
   34.18        have th001: "setprod (\<lambda>i. B$i$ q (inv p i)) ?U = setprod ((\<lambda>i. B$i$ q (inv p i)) \<circ> p) ?U"
   34.19          by (rule setprod_permute[OF p])
   34.20        have thp: "setprod (\<lambda>i. (\<chi> i. A$i$p i *s B$p i :: 'a^'n^'n) $i $ q i) ?U =
    35.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sat Jul 05 10:09:01 2014 +0200
    35.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sat Jul 05 11:01:53 2014 +0200
    35.3 @@ -1578,7 +1578,7 @@
    35.4      have "\<exists>B. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
    35.5        using `bilinear h` by (rule bilinear_bounded)
    35.6      then show "\<exists>K. \<forall>x y. norm (h x y) \<le> norm x * norm y * K"
    35.7 -      by (simp add: mult_ac)
    35.8 +      by (simp add: ac_simps)
    35.9    qed
   35.10  next
   35.11    assume "bounded_bilinear h"
   35.12 @@ -1597,7 +1597,7 @@
   35.13      using bh [unfolded bilinear_conv_bounded_bilinear]
   35.14      by (rule bounded_bilinear.pos_bounded)
   35.15    then show ?thesis
   35.16 -    by (simp only: mult_ac)
   35.17 +    by (simp only: ac_simps)
   35.18  qed
   35.19  
   35.20  
    36.1 --- a/src/HOL/Multivariate_Analysis/PolyRoots.thy	Sat Jul 05 10:09:01 2014 +0200
    36.2 +++ b/src/HOL/Multivariate_Analysis/PolyRoots.thy	Sat Jul 05 11:01:53 2014 +0200
    36.3 @@ -41,9 +41,9 @@
    36.4    shows "(1 - x) * (\<Sum>i=m..n. x^i) = x^m - x^Suc n"
    36.5  proof -
    36.6    have  "(1 - x) * (\<Sum>i=m..n. x^i) = x^m * (1 - x) * (\<Sum>i\<le>n-m. x^i)"
    36.7 -    by (metis ab_semigroup_mult_class.mult_ac(1) assms mult.commute setsum_power_shift)
    36.8 +    by (metis mult.assoc mult.commute assms setsum_power_shift)
    36.9    also have "... =x^m * (1 - x^Suc(n-m))"
   36.10 -    by (metis ab_semigroup_mult_class.mult_ac(1) setsum_gp_basic)
   36.11 +    by (metis mult.assoc setsum_gp_basic)
   36.12    also have "... = x^m - x^Suc n"
   36.13      using assms
   36.14      by (simp add: algebra_simps) (metis le_add_diff_inverse power_add)
   36.15 @@ -78,9 +78,9 @@
   36.16          (\<Sum>i\<le>n. a i * (x^i - y^i))"
   36.17      by (simp add: algebra_simps setsum_subtractf [symmetric])
   36.18    also have "... = (\<Sum>i\<le>n. a i * (x - y) * (\<Sum>j<i. y^(i - Suc j) * x^j))"
   36.19 -    by (simp add: power_diff_sumr2 mult_ac)
   36.20 +    by (simp add: power_diff_sumr2 ac_simps)
   36.21    also have "... = (x - y) * (\<Sum>i\<le>n. (\<Sum>j<i. a i * y^(i - Suc j) * x^j))"
   36.22 -    by (simp add: setsum_right_distrib mult_ac)
   36.23 +    by (simp add: setsum_right_distrib ac_simps)
   36.24    also have "... = (x - y) * (\<Sum>j<n. (\<Sum>i=Suc j..n. a i * y^(i - Suc j) * x^j))"
   36.25      by (simp add: nested_setsum_swap')
   36.26    finally show ?thesis .
    37.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat Jul 05 10:09:01 2014 +0200
    37.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat Jul 05 11:01:53 2014 +0200
    37.3 @@ -2844,7 +2844,7 @@
    37.4    from assms(1) obtain b where b: "b > 0" "\<forall>x\<in>S. norm x \<le> b"
    37.5      unfolding bounded_pos by auto
    37.6    from assms(2) obtain B where B: "B > 0" "\<forall>x. norm (f x) \<le> B * norm x"
    37.7 -    using bounded_linear.pos_bounded by (auto simp add: mult_ac)
    37.8 +    using bounded_linear.pos_bounded by (auto simp add: ac_simps)
    37.9    {
   37.10      fix x
   37.11      assume "x \<in> S"
    38.1 --- a/src/HOL/NSA/CLim.thy	Sat Jul 05 10:09:01 2014 +0200
    38.2 +++ b/src/HOL/NSA/CLim.thy	Sat Jul 05 11:01:53 2014 +0200
    38.3 @@ -142,7 +142,7 @@
    38.4  apply (drule_tac [2] DERIV_ident [THEN DERIV_mult])
    38.5  apply (auto simp add: distrib_right real_of_nat_Suc)
    38.6  apply (case_tac "n")
    38.7 -apply (auto simp add: mult_ac add.commute)
    38.8 +apply (auto simp add: ac_simps add.commute)
    38.9  done
   38.10  
   38.11  text{*Nonstandard version*}
    39.1 --- a/src/HOL/NSA/HDeriv.thy	Sat Jul 05 10:09:01 2014 +0200
    39.2 +++ b/src/HOL/NSA/HDeriv.thy	Sat Jul 05 11:01:53 2014 +0200
    39.3 @@ -171,7 +171,7 @@
    39.4  apply (auto simp add: NSDERIV_NSLIM_iff NSLIM_def)
    39.5  apply (auto simp add: add_divide_distrib diff_divide_distrib dest!: spec)
    39.6  apply (drule_tac b = "star_of Da" and d = "star_of Db" in approx_add)
    39.7 -apply (auto simp add: add_ac algebra_simps)
    39.8 +apply (auto simp add: ac_simps algebra_simps)
    39.9  done
   39.10  
   39.11  text{*Product of functions - Proof is trivial but tedious
   39.12 @@ -180,7 +180,7 @@
   39.13  lemma lemma_nsderiv1:
   39.14    fixes a b c d :: "'a::comm_ring star"
   39.15    shows "(a*b) - (c*d) = (b*(a - c)) + (c*(b - d))"
   39.16 -by (simp add: right_diff_distrib mult_ac)
   39.17 +by (simp add: right_diff_distrib ac_simps)
   39.18  
   39.19  lemma lemma_nsderiv2:
   39.20    fixes x y z :: "'a::real_normed_field star"
    40.1 --- a/src/HOL/NSA/HTranscendental.thy	Sat Jul 05 10:09:01 2014 +0200
    40.2 +++ b/src/HOL/NSA/HTranscendental.thy	Sat Jul 05 11:01:53 2014 +0200
    40.3 @@ -527,7 +527,7 @@
    40.4                     pi_divide_HNatInfinite_not_zero])
    40.5  apply (auto)
    40.6  apply (rule approx_SReal_mult_cancel [of "inverse (hypreal_of_real pi)"])
    40.7 -apply (auto intro: Reals_inverse simp add: divide_inverse mult_ac)
    40.8 +apply (auto intro: Reals_inverse simp add: divide_inverse ac_simps)
    40.9  done
   40.10  
   40.11  lemma STAR_sin_pi_divide_HNatInfinite_approx_pi2:
    41.1 --- a/src/HOL/NSA/NSA.thy	Sat Jul 05 10:09:01 2014 +0200
    41.2 +++ b/src/HOL/NSA/NSA.thy	Sat Jul 05 11:01:53 2014 +0200
    41.3 @@ -776,7 +776,7 @@
    41.4  
    41.5  lemma approx_add_left_cancel: "d + b  @= d + c ==> b @= c"
    41.6  apply (drule approx_minus_iff [THEN iffD1])
    41.7 -apply (simp add: approx_minus_iff [symmetric] add_ac)
    41.8 +apply (simp add: approx_minus_iff [symmetric] ac_simps)
    41.9  done
   41.10  
   41.11  lemma approx_add_right_cancel: "b + d @= c + d ==> b @= c"
   41.12 @@ -786,7 +786,7 @@
   41.13  
   41.14  lemma approx_add_mono1: "b @= c ==> d + b @= d + c"
   41.15  apply (rule approx_minus_iff [THEN iffD2])
   41.16 -apply (simp add: approx_minus_iff [symmetric] add_ac)
   41.17 +apply (simp add: approx_minus_iff [symmetric] ac_simps)
   41.18  done
   41.19  
   41.20  lemma approx_add_mono2: "b @= c ==> b + a @= c + a"
   41.21 @@ -1714,25 +1714,25 @@
   41.22  lemma Infinitesimal_sum_square_cancel2 [simp]:
   41.23       "(y::hypreal)*y + x*x + z*z \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
   41.24  apply (rule Infinitesimal_sum_square_cancel)
   41.25 -apply (simp add: add_ac)
   41.26 +apply (simp add: ac_simps)
   41.27  done
   41.28  
   41.29  lemma HFinite_sum_square_cancel2 [simp]:
   41.30       "(y::hypreal)*y + x*x + z*z \<in> HFinite ==> x*x \<in> HFinite"
   41.31  apply (rule HFinite_sum_square_cancel)
   41.32 -apply (simp add: add_ac)
   41.33 +apply (simp add: ac_simps)
   41.34  done
   41.35  
   41.36  lemma Infinitesimal_sum_square_cancel3 [simp]:
   41.37       "(z::hypreal)*z + y*y + x*x \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
   41.38  apply (rule Infinitesimal_sum_square_cancel)
   41.39 -apply (simp add: add_ac)
   41.40 +apply (simp add: ac_simps)
   41.41  done
   41.42  
   41.43  lemma HFinite_sum_square_cancel3 [simp]:
   41.44       "(z::hypreal)*z + y*y + x*x \<in> HFinite ==> x*x \<in> HFinite"
   41.45  apply (rule HFinite_sum_square_cancel)
   41.46 -apply (simp add: add_ac)
   41.47 +apply (simp add: ac_simps)
   41.48  done
   41.49  
   41.50  lemma monad_hrabs_less:
    42.1 --- a/src/HOL/Nat.thy	Sat Jul 05 10:09:01 2014 +0200
    42.2 +++ b/src/HOL/Nat.thy	Sat Jul 05 11:01:53 2014 +0200
    42.3 @@ -1075,10 +1075,10 @@
    42.4  lemma add_leE: "(m::nat) + k \<le> n ==> (m \<le> n ==> k \<le> n ==> R) ==> R"
    42.5  by (blast dest: add_leD1 add_leD2)
    42.6  
    42.7 -text {* needs @{text "!!k"} for @{text add_ac} to work *}
    42.8 +text {* needs @{text "!!k"} for @{text ac_simps} to work *}
    42.9  lemma less_add_eq_less: "!!k::nat. k < l ==> m + l = k + n ==> m < n"
   42.10  by (force simp del: add_Suc_right
   42.11 -    simp add: less_iff_Suc_add add_Suc_right [symmetric] add_ac)
   42.12 +    simp add: less_iff_Suc_add add_Suc_right [symmetric] ac_simps)
   42.13  
   42.14  
   42.15  subsubsection {* More results about difference *}
   42.16 @@ -1405,10 +1405,10 @@
   42.17    by (simp add: of_nat_def)
   42.18  
   42.19  lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n"
   42.20 -  by (induct m) (simp_all add: add_ac)
   42.21 +  by (induct m) (simp_all add: ac_simps)
   42.22  
   42.23  lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n"
   42.24 -  by (induct m) (simp_all add: add_ac distrib_right)
   42.25 +  by (induct m) (simp_all add: ac_simps distrib_right)
   42.26  
   42.27  primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
   42.28    "of_nat_aux inc 0 i = i"
   42.29 @@ -1869,7 +1869,7 @@
   42.30  lemma dvd_mult_cancel: "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n"
   42.31    unfolding dvd_def
   42.32    apply (erule exE)
   42.33 -  apply (simp add: mult_ac)
   42.34 +  apply (simp add: ac_simps)
   42.35    done
   42.36  
   42.37  lemma dvd_mult_cancel1: "0<m ==> (m*n dvd m) = (n = (1::nat))"
    43.1 --- a/src/HOL/NthRoot.thy	Sat Jul 05 10:09:01 2014 +0200
    43.2 +++ b/src/HOL/NthRoot.thy	Sat Jul 05 11:01:53 2014 +0200
    43.3 @@ -527,7 +527,7 @@
    43.4  lemma real_divide_square_eq [simp]: "(((r::real) * a) / (r * r)) = a / r"
    43.5  apply (simp add: divide_inverse)
    43.6  apply (case_tac "r=0")
    43.7 -apply (auto simp add: mult_ac)
    43.8 +apply (auto simp add: ac_simps)
    43.9  done
   43.10  
   43.11  lemma lemma_real_divide_sqrt_less: "0 < u ==> u / sqrt 2 < u"
    44.1 --- a/src/HOL/Number_Theory/Binomial.thy	Sat Jul 05 10:09:01 2014 +0200
    44.2 +++ b/src/HOL/Number_Theory/Binomial.thy	Sat Jul 05 11:01:53 2014 +0200
    44.3 @@ -161,7 +161,7 @@
    44.4      by (rule distrib)
    44.5    also have "\<dots> = (\<Sum>k=0..n. of_nat (n choose k) * a^(k+1) * b^(n-k)) +
    44.6                    (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k+1))"
    44.7 -    by (auto simp add: setsum_right_distrib mult_ac)
    44.8 +    by (auto simp add: setsum_right_distrib ac_simps)
    44.9    also have "\<dots> = (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n+1-k)) +
   44.10                    (\<Sum>k=1..n+1. of_nat (n choose (k - 1)) * a^k * b^(n+1-k))"
   44.11      by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le field_simps  
   44.12 @@ -634,7 +634,7 @@
   44.13    also have "... = fact (m+r+k) div (fact r * (fact k * fact m))"
   44.14      apply (subst div_mult_div_if_dvd)
   44.15      apply (auto simp: fact_fact_dvd_fact)
   44.16 -    apply (metis ab_semigroup_add_class.add_ac(1) add.commute fact_fact_dvd_fact)
   44.17 +    apply (metis ac_simps add.commute fact_fact_dvd_fact)
   44.18      done
   44.19    also have "... = (fact (m+r+k) * fact (m+r)) div (fact r * (fact k * fact m) * fact (m+r))"
   44.20      apply (subst div_mult_div_if_dvd [symmetric])
   44.21 @@ -758,7 +758,7 @@
   44.22      also have "\<dots> = - (\<Sum>i = 0..card K. -1 ^ i * int (card K choose i)) + 1"
   44.23        by(subst setsum_right_distrib[symmetric]) simp
   44.24      also have "\<dots> =  - ((-1 + 1) ^ card K) + 1"
   44.25 -      by(subst binomial_ring)(simp add: mult_ac)
   44.26 +      by(subst binomial_ring)(simp add: ac_simps)
   44.27      also have "\<dots> = 1" using x K by(auto simp add: K_def card_gt_0_iff)
   44.28      finally show "?lhs x = 1" .
   44.29    qed
    45.1 --- a/src/HOL/Number_Theory/MiscAlgebra.thy	Sat Jul 05 10:09:01 2014 +0200
    45.2 +++ b/src/HOL/Number_Theory/MiscAlgebra.thy	Sat Jul 05 11:01:53 2014 +0200
    45.3 @@ -115,7 +115,7 @@
    45.4    apply (rule_tac x = "(m_inv G a) \<otimes> x" in bexI)
    45.5    apply auto
    45.6  (* auto should get this. I suppose we need "comm_monoid_simprules"
    45.7 -   for mult_ac rewriting. *)
    45.8 +   for ac_simps rewriting. *)
    45.9    apply (subst m_assoc [symmetric])
   45.10    apply auto
   45.11    done
    46.1 --- a/src/HOL/Number_Theory/Pocklington.thy	Sat Jul 05 10:09:01 2014 +0200
    46.2 +++ b/src/HOL/Number_Theory/Pocklington.thy	Sat Jul 05 11:01:53 2014 +0200
    46.3 @@ -549,7 +549,7 @@
    46.4    from n nqr have aqr0: "a ^ (q * r) \<noteq> 0" using a0 by simp
    46.5    hence "(a ^ (q * r) - 1) + 1  = a ^ (q * r)" by simp
    46.6    with k l have "a ^ (q * r) = p*l*k + 1" by simp
    46.7 -  hence "a ^ (r * q) + p * 0 = 1 + p * (l*k)" by (simp add: mult_ac)
    46.8 +  hence "a ^ (r * q) + p * 0 = 1 + p * (l*k)" by (simp add: ac_simps)
    46.9    hence odq: "ord p (a^r) dvd q"
   46.10      unfolding ord_divides[symmetric] power_mult[symmetric]
   46.11      by (metis an cong_dvd_modulus_nat mult.commute nqr pn) 
    47.1 --- a/src/HOL/Number_Theory/Residues.thy	Sat Jul 05 10:09:01 2014 +0200
    47.2 +++ b/src/HOL/Number_Theory/Residues.thy	Sat Jul 05 11:01:53 2014 +0200
    47.3 @@ -40,7 +40,7 @@
    47.4    apply (insert m_gt_one)
    47.5    apply (rule abelian_groupI)
    47.6    apply (unfold R_def residue_ring_def)
    47.7 -  apply (auto simp add: mod_add_right_eq [symmetric] add_ac)
    47.8 +  apply (auto simp add: mod_add_right_eq [symmetric] ac_simps)
    47.9    apply (case_tac "x = 0")
   47.10    apply force
   47.11    apply (subgoal_tac "(x + (m - x)) mod m = 0")
   47.12 @@ -56,7 +56,7 @@
   47.13    apply (subgoal_tac "x * y mod m * z mod m = z * (x * y mod m) mod m")
   47.14    apply (erule ssubst)
   47.15    apply (subst mod_mult_right_eq [symmetric])+
   47.16 -  apply (simp_all only: mult_ac)
   47.17 +  apply (simp_all only: ac_simps)
   47.18    done
   47.19  
   47.20  lemma cring: "cring R"
    48.1 --- a/src/HOL/Old_Number_Theory/Chinese.thy	Sat Jul 05 10:09:01 2014 +0200
    48.2 +++ b/src/HOL/Old_Number_Theory/Chinese.thy	Sat Jul 05 11:01:53 2014 +0200
    48.3 @@ -238,7 +238,7 @@
    48.4            "0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i
    48.5            \<and> [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)")
    48.6           prefer 6
    48.7 -         apply (simp add: mult_ac)
    48.8 +         apply (simp add: ac_simps)
    48.9          apply (unfold xilin_sol_def)
   48.10          apply (tactic {* asm_simp_tac @{context} 6 *})
   48.11          apply (rule_tac [6] ex1_implies_ex [THEN someI_ex])
    49.1 --- a/src/HOL/Old_Number_Theory/Euler.thy	Sat Jul 05 10:09:01 2014 +0200
    49.2 +++ b/src/HOL/Old_Number_Theory/Euler.thy	Sat Jul 05 11:01:53 2014 +0200
    49.3 @@ -67,7 +67,7 @@
    49.4    then have "[j * j = (a * MultInv p j) * j] (mod p)"
    49.5      by (auto simp add: zcong_scalar)
    49.6    then have a:"[j * j = a * (MultInv p j * j)] (mod p)"
    49.7 -    by (auto simp add: mult_ac)
    49.8 +    by (auto simp add: ac_simps)
    49.9    have "[j * j = a] (mod p)"
   49.10    proof -
   49.11      from assms(1,2,4) have "[MultInv p j * j = 1] (mod p)"
   49.12 @@ -149,7 +149,7 @@
   49.13                     c = "a * (x * MultInv p x)" in  zcong_trans, force)
   49.14    apply (frule_tac p = p and x = x in MultInv_prop2, auto)
   49.15  apply (metis StandardRes_SRStar_prop3 mult_1_right mult.commute zcong_sym zcong_zmult_prop1)
   49.16 -  apply (auto simp add: mult_ac)
   49.17 +  apply (auto simp add: ac_simps)
   49.18    done
   49.19  
   49.20  lemma aux1: "[| 0 < x; (x::int) < a; x \<noteq> (a - 1) |] ==> x < a - 1"
    50.1 --- a/src/HOL/Old_Number_Theory/EulerFermat.thy	Sat Jul 05 10:09:01 2014 +0200
    50.2 +++ b/src/HOL/Old_Number_Theory/EulerFermat.thy	Sat Jul 05 11:01:53 2014 +0200
    50.3 @@ -255,7 +255,7 @@
    50.4    apply (subst setprod.insert)
    50.5      apply (rule_tac [2] Bnor_prod_power_aux)
    50.6       apply (unfold inj_on_def)
    50.7 -     apply (simp_all add: mult_ac Bnor_fin Bnor_mem_zle_swap)
    50.8 +     apply (simp_all add: ac_simps Bnor_fin Bnor_mem_zle_swap)
    50.9    done
   50.10  
   50.11  
    51.1 --- a/src/HOL/Old_Number_Theory/Factorization.thy	Sat Jul 05 10:09:01 2014 +0200
    51.2 +++ b/src/HOL/Old_Number_Theory/Factorization.thy	Sat Jul 05 11:01:53 2014 +0200
    51.3 @@ -188,7 +188,7 @@
    51.4  
    51.5  lemma perm_prod: "xs <~~> ys ==> prod xs = prod ys"
    51.6    apply (induct set: perm)
    51.7 -     apply (simp_all add: mult_ac)
    51.8 +     apply (simp_all add: ac_simps)
    51.9    done
   51.10  
   51.11  lemma perm_subst_oinsert: "xs <~~> ys ==> oinsert a xs <~~> oinsert a ys"
    52.1 --- a/src/HOL/Old_Number_Theory/Int2.thy	Sat Jul 05 10:09:01 2014 +0200
    52.2 +++ b/src/HOL/Old_Number_Theory/Int2.thy	Sat Jul 05 11:01:53 2014 +0200
    52.3 @@ -51,7 +51,7 @@
    52.4    have "(x div z) * z \<le> (x div z) * z" by simp
    52.5    then have "(x div z) * z \<le> (x div z) * z + x mod z" using modth by arith 
    52.6    also have "\<dots> = x"
    52.7 -    by (auto simp add: zmod_zdiv_equality [symmetric] mult_ac)
    52.8 +    by (auto simp add: zmod_zdiv_equality [symmetric] ac_simps)
    52.9    also note `x < y * z`
   52.10    finally show ?thesis
   52.11      apply (auto simp add: mult_less_cancel_right)
   52.12 @@ -115,7 +115,7 @@
   52.13  
   52.14  lemma zcong_zmult_prop2: "[a = b](mod m) ==>
   52.15      ([c = d * a](mod m) = [c = d * b] (mod m))"
   52.16 -  by (auto simp add: mult_ac zcong_zmult_prop1)
   52.17 +  by (auto simp add: ac_simps zcong_zmult_prop1)
   52.18  
   52.19  lemma zcong_zmult_prop3: "[| zprime p; ~[x = 0] (mod p);
   52.20      ~[y = 0] (mod p) |] ==> ~[x * y = 0] (mod p)"
   52.21 @@ -198,7 +198,7 @@
   52.22  
   52.23  lemma MultInv_prop2a: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==>
   52.24      [(MultInv p x) * x = 1] (mod p)"
   52.25 -  by (auto simp add: MultInv_prop2 mult_ac)
   52.26 +  by (auto simp add: MultInv_prop2 ac_simps)
   52.27  
   52.28  lemma aux_1: "2 < p ==> ((nat p) - 2) = (nat (p - 2))"
   52.29    by (simp add: nat_diff_distrib)
   52.30 @@ -227,7 +227,7 @@
   52.31    apply (insert MultInv_prop2 [of p "MultInv p x"], auto)
   52.32    apply (drule MultInv_prop2, auto)
   52.33    apply (drule_tac k = x in zcong_scalar2, auto)
   52.34 -  apply (auto simp add: mult_ac)
   52.35 +  apply (auto simp add: ac_simps)
   52.36    done
   52.37  
   52.38  lemma MultInv_prop4: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==>
   52.39 @@ -244,10 +244,10 @@
   52.40      m = p and k = x in zcong_scalar)
   52.41    apply (insert MultInv_prop2 [of p x], simp)
   52.42    apply (auto simp only: zcong_sym [of "MultInv p x * x"])
   52.43 -  apply (auto simp add: mult_ac)
   52.44 +  apply (auto simp add: ac_simps)
   52.45    apply (drule zcong_trans, auto)
   52.46    apply (drule_tac a = "x * MultInv p y" and k = y in zcong_scalar, auto)
   52.47 -  apply (insert MultInv_prop2a [of p y], auto simp add: mult_ac)
   52.48 +  apply (insert MultInv_prop2a [of p y], auto simp add: ac_simps)
   52.49    apply (insert zcong_zmult_prop2 [of "y * MultInv p y" 1 p y x])
   52.50    apply (auto simp add: zcong_sym)
   52.51    done
   52.52 @@ -264,7 +264,7 @@
   52.53      [j * k = a * MultInv p k * k] (mod p) |] ==> [j * k = a] (mod p)"
   52.54    apply (insert MultInv_prop2a [of p k] zcong_zmult_prop2
   52.55      [of "MultInv p k * k" 1 p "j * k" a])
   52.56 -  apply (auto simp add: mult_ac)
   52.57 +  apply (auto simp add: ac_simps)
   52.58    done
   52.59  
   52.60  lemma aux___3: "[j * k = a] (mod p) ==> [(MultInv p j) * j * k =
   52.61 @@ -276,7 +276,7 @@
   52.62         ==> [k = a * (MultInv p j)] (mod p)"
   52.63    apply (insert MultInv_prop2a [of p j] zcong_zmult_prop1
   52.64      [of "MultInv p j * j" 1 p "MultInv p j * a" k])
   52.65 -  apply (auto simp add: mult_ac zcong_sym)
   52.66 +  apply (auto simp add: ac_simps zcong_sym)
   52.67    done
   52.68  
   52.69  lemma MultInv_zcong_prop2: "[| 2 < p; zprime p; ~([k = 0](mod p));
    53.1 --- a/src/HOL/Old_Number_Theory/IntPrimes.thy	Sat Jul 05 10:09:01 2014 +0200
    53.2 +++ b/src/HOL/Old_Number_Theory/IntPrimes.thy	Sat Jul 05 11:01:53 2014 +0200
    53.3 @@ -253,7 +253,7 @@
    53.4  
    53.5  lemma zcong_zmod_aux:
    53.6       "a - b = (m::int) * (a div m - b div m) + (a mod m - b mod m)"
    53.7 -  by(simp add: right_diff_distrib add_diff_eq eq_diff_eq add_ac)
    53.8 +  by(simp add: right_diff_distrib add_diff_eq eq_diff_eq ac_simps)
    53.9  
   53.10  lemma zcong_zmod: "[a = b] (mod m) = [a mod m = b mod m] (mod m)"
   53.11    apply (unfold zcong_def)
    54.1 --- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Sat Jul 05 10:09:01 2014 +0200
    54.2 +++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Sat Jul 05 11:01:53 2014 +0200
    54.3 @@ -351,7 +351,7 @@
    54.4            hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)" 
    54.5              by (simp only: diff_add_assoc[OF dble, of d, symmetric])
    54.6            hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
    54.7 -            by (simp only: diff_mult_distrib2 add.commute mult_ac)
    54.8 +            by (simp only: diff_mult_distrib2 add.commute ac_simps)
    54.9            hence ?thesis using H(1,2)
   54.10              apply -
   54.11              apply (rule exI[where x=d], simp)
   54.12 @@ -492,20 +492,20 @@
   54.13    from pos_k k_m have pos_p: "p > 0" by auto
   54.14    from pos_k k_n have pos_q: "q > 0" by auto
   54.15    have "k * k * gcd q p = k * gcd (k * q) (k * p)"
   54.16 -    by (simp add: mult_ac gcd_mult_distrib2)
   54.17 +    by (simp add: ac_simps gcd_mult_distrib2)
   54.18    also have "\<dots> = k * gcd (m * p * q) (n * q * p)"
   54.19      by (simp add: k_m [symmetric] k_n [symmetric])
   54.20    also have "\<dots> = k * p * q * gcd m n"
   54.21 -    by (simp add: mult_ac gcd_mult_distrib2)
   54.22 +    by (simp add: ac_simps gcd_mult_distrib2)
   54.23    finally have "(m * p) * (n * q) * gcd q p = k * p * q * gcd m n"
   54.24      by (simp only: k_m [symmetric] k_n [symmetric])
   54.25    then have "p * q * m * n * gcd q p = p * q * k * gcd m n"
   54.26 -    by (simp add: mult_ac)
   54.27 +    by (simp add: ac_simps)
   54.28    with pos_p pos_q have "m * n * gcd q p = k * gcd m n"
   54.29      by simp
   54.30    with prod_gcd_lcm [of m n]
   54.31    have "lcm m n * gcd q p * gcd m n = k * gcd m n"
   54.32 -    by (simp add: mult_ac)
   54.33 +    by (simp add: ac_simps)
   54.34    with pos_gcd have "lcm m n * gcd q p = k" by simp
   54.35    then show ?thesis using dvd_def by auto
   54.36  qed
   54.37 @@ -525,7 +525,7 @@
   54.38      then have npos: "n > 0" by simp
   54.39      have "gcd m n dvd n" by simp
   54.40      then obtain k where "n = gcd m n * k" using dvd_def by auto
   54.41 -    then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n" by (simp add: mult_ac)
   54.42 +    then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n" by (simp add: ac_simps)
   54.43      also have "\<dots> = m * k" using mpos npos gcd_zero by simp
   54.44      finally show ?thesis by (simp add: lcm_def)
   54.45    qed
   54.46 @@ -546,7 +546,7 @@
   54.47      then have mpos: "m > 0" by simp
   54.48      have "gcd m n dvd m" by simp
   54.49      then obtain k where "m = gcd m n * k" using dvd_def by auto
   54.50 -    then have "m * n div gcd m n = (gcd m n * k) * n div gcd m n" by (simp add: mult_ac)
   54.51 +    then have "m * n div gcd m n = (gcd m n * k) * n div gcd m n" by (simp add: ac_simps)
   54.52      also have "\<dots> = n * k" using mpos npos gcd_zero by simp
   54.53      finally show ?thesis by (simp add: lcm_def)
   54.54    qed
    55.1 --- a/src/HOL/Old_Number_Theory/Pocklington.thy	Sat Jul 05 10:09:01 2014 +0200
    55.2 +++ b/src/HOL/Old_Number_Theory/Pocklington.thy	Sat Jul 05 11:01:53 2014 +0200
    55.3 @@ -1020,7 +1020,7 @@
    55.4    from n nqr have aqr0: "a ^ (q * r) \<noteq> 0" using a0 by simp
    55.5    hence "(a ^ (q * r) - 1) + 1  = a ^ (q * r)" by simp
    55.6    with k l have "a ^ (q * r) = p*l*k + 1" by simp
    55.7 -  hence "a ^ (r * q) + p * 0 = 1 + p * (l*k)" by (simp add: mult_ac)
    55.8 +  hence "a ^ (r * q) + p * 0 = 1 + p * (l*k)" by (simp add: ac_simps)
    55.9    hence odq: "ord p (a^r) dvd q"
   55.10      unfolding ord_divides[symmetric] power_mult[symmetric] nat_mod  by blast
   55.11    from odq[unfolded dvd_def] obtain d where d: "q = ord p (a^r) * d" by blast
    56.1 --- a/src/HOL/Old_Number_Theory/Primes.thy	Sat Jul 05 10:09:01 2014 +0200
    56.2 +++ b/src/HOL/Old_Number_Theory/Primes.thy	Sat Jul 05 11:01:53 2014 +0200
    56.3 @@ -227,10 +227,10 @@
    56.4  apply (case_tac "d * x - a * b * y = Suc 0 ", simp_all)
    56.5  apply (rule_tac x="x" in exI)
    56.6  apply (rule_tac x="a*y" in exI)
    56.7 -apply (simp add: mult_ac)
    56.8 +apply (simp add: ac_simps)
    56.9  apply (rule_tac x="a*x" in exI)
   56.10  apply (rule_tac x="y" in exI)
   56.11 -apply (simp add: mult_ac)
   56.12 +apply (simp add: ac_simps)
   56.13  done
   56.14  
   56.15  lemma coprime_rmul2: "coprime d (a * b) \<Longrightarrow> coprime d a"
   56.16 @@ -239,10 +239,10 @@
   56.17  apply (case_tac "d * x - a * b * y = Suc 0 ", simp_all)
   56.18  apply (rule_tac x="x" in exI)
   56.19  apply (rule_tac x="b*y" in exI)
   56.20 -apply (simp add: mult_ac)
   56.21 +apply (simp add: ac_simps)
   56.22  apply (rule_tac x="b*x" in exI)
   56.23  apply (rule_tac x="y" in exI)
   56.24 -apply (simp add: mult_ac)
   56.25 +apply (simp add: ac_simps)
   56.26  done
   56.27  lemma coprime_mul_eq: "coprime d (a * b) \<longleftrightarrow> coprime d a \<and>  coprime d b"
   56.28    using coprime_rmul2[of d a b] coprime_lmul2[of d a b] coprime_mul[of d a b] 
   56.29 @@ -288,7 +288,7 @@
   56.30    moreover
   56.31    {assume z: "?g \<noteq> 0"
   56.32      from gcd_dvd1[of a b] gcd_dvd2[of a b] obtain a' b' where
   56.33 -      ab': "a = a'*?g" "b = b'*?g" unfolding dvd_def by (auto simp add: mult_ac)
   56.34 +      ab': "a = a'*?g" "b = b'*?g" unfolding dvd_def by (auto simp add: ac_simps)
   56.35      hence ab'': "?g*a' = a" "?g * b' = b" by algebra+
   56.36      from coprime_exp_imp[OF gcd_coprime[OF z ab'], unfolded coprime_bezout, of n]
   56.37      obtain x y where "a'^n * x - b'^n * y = 1 \<or> b'^n * x - a'^n * y = 1"  by blast
    57.1 --- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Sat Jul 05 10:09:01 2014 +0200
    57.2 +++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Sat Jul 05 11:01:53 2014 +0200
    57.3 @@ -388,7 +388,7 @@
    57.4      by (auto simp add: int_distrib)
    57.5    then have "((p - 1) * q) div 2 < (((q - 1) * p) + (2 * p)) div 2"
    57.6      apply (rule_tac x = "((p - 1) * q)" in even_div_2_l)
    57.7 -    by (auto simp add: even3, auto simp add: mult_ac)
    57.8 +    by (auto simp add: even3, auto simp add: ac_simps)
    57.9    also have "((p - 1) * q) div 2 = q * ((p - 1) div 2)"
   57.10      by (auto simp add: even1 even_prod_div_2)
   57.11    also have "(((q - 1) * p) + (2 * p)) div 2 = (((q - 1) div 2) * p) + p"
   57.12 @@ -557,11 +557,11 @@
   57.13  
   57.14  lemma S1_carda: "int (card(S1)) =
   57.15      setsum (%j. (j * q) div p) P_set"
   57.16 -  by (auto simp add: S1_card mult_ac)
   57.17 +  by (auto simp add: S1_card ac_simps)
   57.18  
   57.19  lemma S2_carda: "int (card(S2)) =
   57.20      setsum (%j. (j * p) div q) Q_set"
   57.21 -  by (auto simp add: S2_card mult_ac)
   57.22 +  by (auto simp add: S2_card ac_simps)
   57.23  
   57.24  lemma pq_sum_prop: "(setsum (%j. (j * p) div q) Q_set) +
   57.25      (setsum (%j. (j * q) div p) P_set) = ((p - 1) div 2) * ((q - 1) div 2)"
    58.1 --- a/src/HOL/Power.thy	Sat Jul 05 10:09:01 2014 +0200
    58.2 +++ b/src/HOL/Power.thy	Sat Jul 05 11:01:53 2014 +0200
    58.3 @@ -110,7 +110,7 @@
    58.4  
    58.5  lemma power_mult_distrib [field_simps]:
    58.6    "(a * b) ^ n = (a ^ n) * (b ^ n)"
    58.7 -  by (induct n) (simp_all add: mult_ac)
    58.8 +  by (induct n) (simp_all add: ac_simps)
    58.9  
   58.10  end
   58.11  
   58.12 @@ -562,7 +562,7 @@
   58.13  next
   58.14    case (Suc n)
   58.15    have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)"
   58.16 -    by (simp add: mult_ac power_add power2_eq_square)
   58.17 +    by (simp add: ac_simps power_add power2_eq_square)
   58.18    thus ?case
   58.19      by (simp del: power_Suc add: Suc mult_less_0_iff mult_neg_neg)
   58.20  qed
   58.21 @@ -580,7 +580,7 @@
   58.22  next
   58.23    case (Suc n)
   58.24      have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)" 
   58.25 -      by (simp add: mult_ac power_add power2_eq_square)
   58.26 +      by (simp add: ac_simps power_add power2_eq_square)
   58.27      thus ?case
   58.28        by (simp add: Suc zero_le_mult_iff)
   58.29  qed
    59.1 --- a/src/HOL/Presburger.thy	Sat Jul 05 10:09:01 2014 +0200
    59.2 +++ b/src/HOL/Presburger.thy	Sat Jul 05 11:01:53 2014 +0200
    59.3 @@ -185,7 +185,7 @@
    59.4  proof
    59.5    assume ?LHS
    59.6    then obtain x where P: "P x" ..
    59.7 -  have "x mod d = x - (x div d)*d" by(simp add:zmod_zdiv_equality mult_ac eq_diff_eq)
    59.8 +  have "x mod d = x - (x div d)*d" by(simp add:zmod_zdiv_equality ac_simps eq_diff_eq)
    59.9    hence Pmod: "P x = P(x mod d)" using modd by simp
   59.10    show ?RHS
   59.11    proof (cases)
   59.12 @@ -307,7 +307,7 @@
   59.13    {fix x
   59.14      have "P x \<longrightarrow> P (x + i * d)" using step.hyps by blast
   59.15      also have "\<dots> \<longrightarrow> P(x + (i + 1) * d)" using plus[THEN spec, of "x + i * d"]
   59.16 -      by (simp add:int_distrib add_ac)
   59.17 +      by (simp add:int_distrib ac_simps)
   59.18      ultimately have "P x \<longrightarrow> P(x + (i + 1) * d)" by blast}
   59.19    thus ?case ..
   59.20  qed
    60.1 --- a/src/HOL/Probability/Bochner_Integration.thy	Sat Jul 05 10:09:01 2014 +0200
    60.2 +++ b/src/HOL/Probability/Bochner_Integration.thy	Sat Jul 05 11:01:53 2014 +0200
    60.3 @@ -475,7 +475,7 @@
    60.4      by (subst simple_bochner_integral_partition[OF f(1), where g="\<lambda>x. ereal (f x)" and v=real])
    60.5         (auto intro: f simple_function_compose1 elim: simple_bochner_integrable.cases
    60.6               intro!: setsum.cong ereal_cong_mult
    60.7 -             simp: setsum_ereal[symmetric] times_ereal.simps(1)[symmetric] mult_ac
    60.8 +             simp: setsum_ereal[symmetric] times_ereal.simps(1)[symmetric] ac_simps
    60.9               simp del: setsum_ereal times_ereal.simps(1))
   60.10    also have "\<dots> = (\<integral>\<^sup>+x. f x \<partial>M)"
   60.11      using f
   60.12 @@ -631,7 +631,7 @@
   60.13        (is "eventually (\<lambda>i. ?f i \<le> ?g i) sequentially")
   60.14      proof (intro always_eventually allI)
   60.15        fix i have "?f i \<le> (\<integral>\<^sup>+ x. ereal K * norm (f x - s i x) \<partial>M)"
   60.16 -        using K by (intro nn_integral_mono) (auto simp: mult_ac)
   60.17 +        using K by (intro nn_integral_mono) (auto simp: ac_simps)
   60.18        also have "\<dots> = ?g i"
   60.19          using K by (intro nn_integral_cmult) auto
   60.20        finally show "?f i \<le> ?g i" .
    61.1 --- a/src/HOL/Probability/Borel_Space.thy	Sat Jul 05 10:09:01 2014 +0200
    61.2 +++ b/src/HOL/Probability/Borel_Space.thy	Sat Jul 05 11:01:53 2014 +0200
    61.3 @@ -136,7 +136,7 @@
    61.4    shows "f \<in> borel_measurable (restrict_space M \<Omega>) \<longleftrightarrow>
    61.5      (\<lambda>x. indicator \<Omega> x *\<^sub>R f x) \<in> borel_measurable M"
    61.6    by (subst measurable_restrict_space_iff)
    61.7 -     (auto simp: indicator_def if_distrib[where f="\<lambda>x. x *\<^sub>R a" for a] mult_ac cong del: if_cong)
    61.8 +     (auto simp: indicator_def if_distrib[where f="\<lambda>x. x *\<^sub>R a" for a] ac_simps cong del: if_cong)
    61.9  
   61.10  lemma cbox_borel[measurable]: "cbox a b \<in> sets borel"
   61.11    by (auto intro: borel_closed)
    62.1 --- a/src/HOL/Probability/Convolution.thy	Sat Jul 05 10:09:01 2014 +0200
    62.2 +++ b/src/HOL/Probability/Convolution.thy	Sat Jul 05 11:01:53 2014 +0200
    62.3 @@ -41,7 +41,7 @@
    62.4    assumes [simp]: "space M = space N" "space N = space borel"
    62.5    shows "emeasure (M \<star> N) A = \<integral>\<^sup>+x. (emeasure N {a. a + x \<in> A}) \<partial>M "
    62.6    using assms by (auto intro!: nn_integral_cong simp del: nn_integral_indicator simp: nn_integral_convolution 
    62.7 -    nn_integral_indicator[symmetric] ab_semigroup_add_class.add_ac split:split_indicator)
    62.8 +    nn_integral_indicator [symmetric] ac_simps split:split_indicator)
    62.9  
   62.10  lemma convolution_emeasure':
   62.11    assumes [simp]:"A \<in> sets borel"
    63.1 --- a/src/HOL/Probability/Distributions.thy	Sat Jul 05 10:09:01 2014 +0200
    63.2 +++ b/src/HOL/Probability/Distributions.thy	Sat Jul 05 11:01:53 2014 +0200
    63.3 @@ -33,7 +33,7 @@
    63.4      by (auto simp add: field_simps)
    63.5  
    63.6    have eq: "\<And>x. ereal \<bar>c\<bar> * (f x / ereal \<bar>c\<bar>) = f x"
    63.7 -    using c by (simp add: divide_ereal_def mult_ac one_ereal_def[symmetric])
    63.8 +    using c by (simp add: divide_ereal_def ac_simps one_ereal_def[symmetric])
    63.9      
   63.10    have "density lborel f = distr M lborel X"
   63.11      using f by (simp add: distributed_def)
   63.12 @@ -49,7 +49,7 @@
   63.13    shows "distributed M lborel X f"
   63.14  proof -
   63.15    have eq: "\<And>x. f x * ereal \<bar>c\<bar> / ereal \<bar>c\<bar> = f x"
   63.16 -    using c by (simp add: divide_ereal_def mult_ac one_ereal_def[symmetric])
   63.17 +    using c by (simp add: divide_ereal_def ac_simps one_ereal_def[symmetric])
   63.18  
   63.19    show ?thesis
   63.20      using distributed_affine[OF f c, where t=t] c
    64.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Sat Jul 05 10:09:01 2014 +0200
    64.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Sat Jul 05 11:01:53 2014 +0200
    64.3 @@ -1270,7 +1270,7 @@
    64.4    assumes "!!x. DERIV G x :> g x"
    64.5    shows "(\<integral>x. indicator {a .. b} x *\<^sub>R (F x * g x) \<partial>lborel)
    64.6              =  F b * G b - F a * G a - \<integral>x. indicator {a .. b} x *\<^sub>R (f x * G x) \<partial>lborel" 
    64.7 -  using integral_by_parts[OF assms] by (simp add: mult_ac)
    64.8 +  using integral_by_parts[OF assms] by (simp add: ac_simps)
    64.9  
   64.10  lemma has_bochner_integral_even_function:
   64.11    fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
    65.1 --- a/src/HOL/Proofs/Extraction/Euclid.thy	Sat Jul 05 10:09:01 2014 +0200
    65.2 +++ b/src/HOL/Proofs/Extraction/Euclid.thy	Sat Jul 05 11:01:53 2014 +0200
    65.3 @@ -92,7 +92,7 @@
    65.4          from m have "0 < m" by simp
    65.5          moreover note n
    65.6          moreover from False n nmk k have "Suc 0 < k" by auto
    65.7 -        moreover from nmk have "k * m = n" by (simp only: mult_ac)
    65.8 +        moreover from nmk have "k * m = n" by (simp only: ac_simps)
    65.9          ultimately have mn: "m < n" by (rule prod_mn_less_k)
   65.10          with kn A nmk show ?thesis by iprover
   65.11        qed
   65.12 @@ -118,7 +118,7 @@
   65.13    next
   65.14      assume "m = Suc n"
   65.15      then have "m dvd (fact n * Suc n)"
   65.16 -      by (auto intro: dvdI simp: mult_ac)
   65.17 +      by (auto intro: dvdI simp: ac_simps)
   65.18      then show ?thesis by (simp add: mult.commute)
   65.19    qed
   65.20  qed
    66.1 --- a/src/HOL/Quotient_Examples/Quotient_Int.thy	Sat Jul 05 10:09:01 2014 +0200
    66.2 +++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Sat Jul 05 11:01:53 2014 +0200
    66.3 @@ -60,7 +60,7 @@
    66.4    apply(hypsubst_thin)
    66.5    apply(rename_tac u v w x y z)
    66.6    apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
    66.7 -  apply(simp add: mult_ac)
    66.8 +  apply(simp add: ac_simps)
    66.9    apply(simp add: add_mult_distrib [symmetric])
   66.10  done
   66.11  
   66.12 @@ -73,7 +73,7 @@
   66.13    apply(hypsubst_thin)
   66.14    apply(rename_tac u v w x y z)
   66.15    apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
   66.16 -  apply(simp add: mult_ac)
   66.17 +  apply(simp add: ac_simps)
   66.18    apply(simp add: add_mult_distrib [symmetric])
   66.19  done
   66.20  
    67.1 --- a/src/HOL/Rat.thy	Sat Jul 05 10:09:01 2014 +0200
    67.2 +++ b/src/HOL/Rat.thy	Sat Jul 05 11:01:53 2014 +0200
    67.3 @@ -118,7 +118,7 @@
    67.4  
    67.5  lift_definition plus_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat"
    67.6    is "\<lambda>x y. (fst x * snd y + fst y * snd x, snd x * snd y)"
    67.7 -  by (clarsimp, simp add: distrib_right, simp add: mult_ac)
    67.8 +  by (clarsimp, simp add: distrib_right, simp add: ac_simps)
    67.9  
   67.10  lemma add_rat [simp]:
   67.11    assumes "b \<noteq> 0" and "d \<noteq> 0"
   67.12 @@ -144,7 +144,7 @@
   67.13  
   67.14  lift_definition times_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat"
   67.15    is "\<lambda>x y. (fst x * fst y, snd x * snd y)"
   67.16 -  by (simp add: mult_ac)
   67.17 +  by (simp add: ac_simps)
   67.18  
   67.19  lemma mult_rat [simp]: "Fract a b * Fract c d = Fract (a * c) (b * d)"
   67.20    by transfer simp
   67.21 @@ -271,7 +271,7 @@
   67.22    proof -
   67.23      assume "p * gcd r s = sgn (q * s) * r * gcd p q" and "q * gcd r s = sgn (q * s) * s * gcd p q"
   67.24      then have "(p * gcd r s) * (sgn (q * s) * s * gcd p q) = (q * gcd r s) * (sgn (q * s) * r * gcd p q)" by simp
   67.25 -    with assms show "p * s = q * r" by (auto simp add: mult_ac sgn_times sgn_0_0)
   67.26 +    with assms show "p * s = q * r" by (auto simp add: ac_simps sgn_times sgn_0_0)
   67.27    qed
   67.28    from assms show ?thesis
   67.29      by (auto simp add: normalize_def Let_def dvd_div_div_eq_mult mult.commute sgn_times split: if_splits intro: aux)
   67.30 @@ -413,7 +413,7 @@
   67.31    hence "a * d * b * d = c * b * b * d"
   67.32      by simp
   67.33    hence "a * b * d\<^sup>2 = c * d * b\<^sup>2"
   67.34 -    unfolding power2_eq_square by (simp add: mult_ac)
   67.35 +    unfolding power2_eq_square by (simp add: ac_simps)
   67.36    hence "0 < a * b * d\<^sup>2 \<longleftrightarrow> 0 < c * d * b\<^sup>2"
   67.37      by simp
   67.38    thus "0 < a * b \<longleftrightarrow> 0 < c * d"
   67.39 @@ -434,7 +434,7 @@
   67.40  
   67.41  lemma positive_mult:
   67.42    "positive x \<Longrightarrow> positive y \<Longrightarrow> positive (x * y)"
   67.43 -by transfer (drule (1) mult_pos_pos, simp add: mult_ac)
   67.44 +by transfer (drule (1) mult_pos_pos, simp add: ac_simps)
   67.45  
   67.46  lemma positive_minus:
   67.47    "\<not> positive x \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> positive (- x)"
   67.48 @@ -676,7 +676,7 @@
   67.49  
   67.50  lemma of_rat_mult: "of_rat (a * b) = of_rat a * of_rat b"
   67.51  apply transfer
   67.52 -apply (simp add: divide_inverse nonzero_inverse_mult_distrib mult_ac)
   67.53 +apply (simp add: divide_inverse nonzero_inverse_mult_distrib ac_simps)
   67.54  done
   67.55  
   67.56  lemma nonzero_of_rat_inverse:
    68.1 --- a/src/HOL/Real.thy	Sat Jul 05 10:09:01 2014 +0200
    68.2 +++ b/src/HOL/Real.thy	Sat Jul 05 11:01:53 2014 +0200
    68.3 @@ -474,9 +474,9 @@
    68.4  instance proof
    68.5    fix a b c :: real
    68.6    show "a + b = b + a"
    68.7 -    by transfer (simp add: add_ac realrel_def)
    68.8 +    by transfer (simp add: ac_simps realrel_def)
    68.9    show "(a + b) + c = a + (b + c)"
   68.10 -    by transfer (simp add: add_ac realrel_def)
   68.11 +    by transfer (simp add: ac_simps realrel_def)
   68.12    show "0 + a = a"
   68.13      by transfer (simp add: realrel_def)
   68.14    show "- a + a = 0"
   68.15 @@ -484,11 +484,11 @@
   68.16    show "a - b = a + - b"
   68.17      by (rule minus_real_def)
   68.18    show "(a * b) * c = a * (b * c)"
   68.19 -    by transfer (simp add: mult_ac realrel_def)
   68.20 +    by transfer (simp add: ac_simps realrel_def)
   68.21    show "a * b = b * a"
   68.22 -    by transfer (simp add: mult_ac realrel_def)
   68.23 +    by transfer (simp add: ac_simps realrel_def)
   68.24    show "1 * a = a"
   68.25 -    by transfer (simp add: mult_ac realrel_def)
   68.26 +    by transfer (simp add: ac_simps realrel_def)
   68.27    show "(a + b) * c = a * c + b * c"
   68.28      by transfer (simp add: distrib_right realrel_def)
   68.29    show "(0\<Colon>real) \<noteq> (1\<Colon>real)"
   68.30 @@ -707,7 +707,7 @@
   68.31    shows "Real X \<le> Real Y = (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. X n \<le> Y n + r)"
   68.32  unfolding not_less [symmetric, where 'a=real] less_real_def
   68.33  apply (simp add: diff_Real not_positive_Real X Y)
   68.34 -apply (simp add: diff_le_eq add_ac)
   68.35 +apply (simp add: diff_le_eq ac_simps)
   68.36  done
   68.37  
   68.38  lemma le_RealI:
    69.1 --- a/src/HOL/Real_Vector_Spaces.thy	Sat Jul 05 10:09:01 2014 +0200
    69.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Sat Jul 05 11:01:53 2014 +0200
    69.3 @@ -897,7 +897,7 @@
    69.4    also have "norm ((\<Prod>i\<in>I. z i) - (\<Prod>i\<in>I. w i)) \<le> (\<Sum>i\<in>I. norm (z i - w i))"
    69.5      using insert by auto
    69.6    finally show ?case
    69.7 -    by (auto simp add: add_ac mult_right_mono mult_left_mono)
    69.8 +    by (auto simp add: ac_simps mult_right_mono mult_left_mono)
    69.9  qed simp_all
   69.10  
   69.11  lemma norm_power_diff: 
   69.12 @@ -1159,7 +1159,7 @@
   69.13  
   69.14  lemma sgn_scaleR:
   69.15    "sgn (scaleR r x) = scaleR (sgn r) (sgn(x::'a::real_normed_vector))"
   69.16 -by (simp add: sgn_div_norm mult_ac)
   69.17 +by (simp add: sgn_div_norm ac_simps)
   69.18  
   69.19  lemma sgn_one [simp]: "sgn (1::'a::real_normed_algebra_1) = 1"
   69.20  by (simp add: sgn_div_norm)
   69.21 @@ -1308,7 +1308,7 @@
   69.22  apply (rule_tac K="norm b * K" in bounded_linear_intro)
   69.23  apply (rule add_left)
   69.24  apply (rule scaleR_left)
   69.25 -apply (simp add: mult_ac)
   69.26 +apply (simp add: ac_simps)
   69.27  done
   69.28  
   69.29  lemma bounded_linear_right:
   69.30 @@ -1317,7 +1317,7 @@
   69.31  apply (rule_tac K="norm a * K" in bounded_linear_intro)
   69.32  apply (rule add_right)
   69.33  apply (rule scaleR_right)
   69.34 -apply (simp add: mult_ac)
   69.35 +apply (simp add: ac_simps)
   69.36  done
   69.37  
   69.38  lemma prod_diff_prod:
    70.1 --- a/src/HOL/Rings.thy	Sat Jul 05 10:09:01 2014 +0200
    70.2 +++ b/src/HOL/Rings.thy	Sat Jul 05 11:01:53 2014 +0200
    70.3 @@ -21,7 +21,7 @@
    70.4  text{*For the @{text combine_numerals} simproc*}
    70.5  lemma combine_common_factor:
    70.6    "a * e + (b * e + c) = (a + b) * e + c"
    70.7 -by (simp add: distrib_right add_ac)
    70.8 +by (simp add: distrib_right ac_simps)
    70.9  
   70.10  end
   70.11  
   70.12 @@ -55,9 +55,9 @@
   70.13  proof
   70.14    fix a b c :: 'a
   70.15    show "(a + b) * c = a * c + b * c" by (simp add: distrib)
   70.16 -  have "a * (b + c) = (b + c) * a" by (simp add: mult_ac)
   70.17 +  have "a * (b + c) = (b + c) * a" by (simp add: ac_simps)
   70.18    also have "... = b * a + c * a" by (simp only: distrib)
   70.19 -  also have "... = a * b + a * c" by (simp add: mult_ac)
   70.20 +  also have "... = a * b + a * c" by (simp add: ac_simps)
   70.21    finally show "a * (b + c) = a * b + a * c" by blast
   70.22  qed
   70.23  
   70.24 @@ -180,7 +180,7 @@
   70.25  proof -
   70.26    from `a dvd b` obtain b' where "b = a * b'" ..
   70.27    moreover from `c dvd d` obtain d' where "d = c * d'" ..
   70.28 -  ultimately have "b * d = (a * c) * (b' * d')" by (simp add: mult_ac)
   70.29 +  ultimately have "b * d = (a * c) * (b' * d')" by (simp add: ac_simps)
   70.30    then show ?thesis ..
   70.31  qed
   70.32  
   70.33 @@ -188,7 +188,7 @@
   70.34  by (simp add: dvd_def mult.assoc, blast)
   70.35  
   70.36  lemma dvd_mult_right: "a * b dvd c \<Longrightarrow> b dvd c"
   70.37 -  unfolding mult_ac [of a] by (rule dvd_mult_left)
   70.38 +  unfolding mult.commute [of a] by (rule dvd_mult_left)
   70.39  
   70.40  lemma dvd_0_left: "0 dvd a \<Longrightarrow> a = 0"
   70.41  by simp
   70.42 @@ -437,7 +437,7 @@
   70.43    "a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b"
   70.44  proof -
   70.45    have "a * c dvd b * c \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
   70.46 -    unfolding dvd_def by (simp add: mult_ac)
   70.47 +    unfolding dvd_def by (simp add: ac_simps)
   70.48    also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
   70.49      unfolding dvd_def by simp
   70.50    finally show ?thesis .
   70.51 @@ -447,7 +447,7 @@
   70.52    "c * a dvd c * b \<longleftrightarrow> c = 0 \<or> a dvd b"
   70.53  proof -
   70.54    have "c * a dvd c * b \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
   70.55 -    unfolding dvd_def by (simp add: mult_ac)
   70.56 +    unfolding dvd_def by (simp add: ac_simps)
   70.57    also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
   70.58      unfolding dvd_def by simp
   70.59    finally show ?thesis .
    71.1 --- a/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Sat Jul 05 10:09:01 2014 +0200
    71.2 +++ b/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Sat Jul 05 11:01:53 2014 +0200
    71.3 @@ -26,7 +26,7 @@
    71.4  proof -
    71.5    from `0 \<le> c` `0 < d` `c - c sdiv d * d = 0`
    71.6    have "d dvd c"
    71.7 -    by (auto simp add: sdiv_pos_pos dvd_def mult_ac)
    71.8 +    by (auto simp add: sdiv_pos_pos dvd_def ac_simps)
    71.9    with `0 < d` `gcd c d = gcd m n` show ?C1
   71.10      by simp
   71.11  qed
    72.1 --- a/src/HOL/Semiring_Normalization.thy	Sat Jul 05 10:09:01 2014 +0200
    72.2 +++ b/src/HOL/Semiring_Normalization.thy	Sat Jul 05 11:01:53 2014 +0200
    72.3 @@ -47,7 +47,7 @@
    72.4      then have "(y - z) * (w - x) = 0" by (simp add: algebra_simps)
    72.5      then have "y - z = 0 \<or> w - x = 0" by (rule divisors_zero)
    72.6      then show "w = x \<or> y = z" by auto
    72.7 -  qed (auto simp add: add_ac)
    72.8 +  qed (auto simp add: ac_simps)
    72.9  qed
   72.10  
   72.11  instance nat :: comm_semiring_1_cancel_crossproduct
    73.1 --- a/src/HOL/Set_Interval.thy	Sat Jul 05 10:09:01 2014 +0200
    73.2 +++ b/src/HOL/Set_Interval.thy	Sat Jul 05 11:01:53 2014 +0200
    73.3 @@ -1409,22 +1409,22 @@
    73.4  on intervals are not? *)
    73.5  
    73.6  lemma setsum_atMost_Suc[simp]: "(\<Sum>i \<le> Suc n. f i) = (\<Sum>i \<le> n. f i) + f(Suc n)"
    73.7 -by (simp add:atMost_Suc add_ac)
    73.8 +by (simp add:atMost_Suc ac_simps)
    73.9  
   73.10  lemma setsum_lessThan_Suc[simp]: "(\<Sum>i < Suc n. f i) = (\<Sum>i < n. f i) + f n"
   73.11 -by (simp add:lessThan_Suc add_ac)
   73.12 +by (simp add:lessThan_Suc ac_simps)
   73.13  
   73.14  lemma setsum_cl_ivl_Suc[simp]:
   73.15    "setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))"
   73.16 -by (auto simp:add_ac atLeastAtMostSuc_conv)
   73.17 +by (auto simp:ac_simps atLeastAtMostSuc_conv)
   73.18  
   73.19  lemma setsum_op_ivl_Suc[simp]:
   73.20    "setsum f {m..<Suc n} = (if n < m then 0 else setsum f {m..<n} + f(n))"
   73.21 -by (auto simp:add_ac atLeastLessThanSuc)
   73.22 +by (auto simp:ac_simps atLeastLessThanSuc)
   73.23  (*
   73.24  lemma setsum_cl_ivl_add_one_nat: "(n::nat) <= m + 1 ==>
   73.25      (\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)"
   73.26 -by (auto simp:add_ac atLeastAtMostSuc_conv)
   73.27 +by (auto simp:ac_simps atLeastAtMostSuc_conv)
   73.28  *)
   73.29  
   73.30  lemma setsum_head:
   73.31 @@ -1468,7 +1468,7 @@
   73.32  shows "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
   73.33    setsum f {m..<p} - setsum f {m..<n} = setsum f {n..<p}"
   73.34  using setsum_add_nat_ivl [of m n p f,symmetric]
   73.35 -apply (simp add: add_ac)
   73.36 +apply (simp add: ac_simps)
   73.37  done
   73.38  
   73.39  lemma setsum_natinterval_difff:
   73.40 @@ -1600,15 +1600,15 @@
   73.41    also from ngt1 have "\<dots> = ?n*a + (\<Sum>i\<in>{..<n}. ?I i*d)" by simp
   73.42    also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))"
   73.43      unfolding One_nat_def
   73.44 -    by (simp add: setsum_right_distrib atLeast0LessThan[symmetric] setsum_shift_lb_Suc0_0_upt mult_ac)
   73.45 +    by (simp add: setsum_right_distrib atLeast0LessThan[symmetric] setsum_shift_lb_Suc0_0_upt ac_simps)
   73.46    also have "2*\<dots> = 2*?n*a + d*2*(\<Sum>i\<in>{1..<n}. ?I i)"
   73.47      by (simp add: algebra_simps)
   73.48    also from ngt1 have "{1..<n} = {1..n - 1}"
   73.49      by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost)
   73.50    also from ngt1
   73.51    have "2*?n*a + d*2*(\<Sum>i\<in>{1..n - 1}. ?I i) = (2*?n*a + d*?I (n - 1)*?I n)"
   73.52 -    by (simp only: mult_ac gauss_sum [of "n - 1"], unfold One_nat_def)
   73.53 -       (simp add:  mult_ac trans [OF add.commute of_nat_Suc [symmetric]])
   73.54 +    by (simp only: mult.assoc gauss_sum [of "n - 1"], unfold One_nat_def)
   73.55 +      (simp add:  mult.commute trans [OF add.commute of_nat_Suc [symmetric]])
   73.56    finally show ?thesis
   73.57      unfolding mult_2 by (simp add: algebra_simps)
   73.58  next
    74.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Sat Jul 05 10:09:01 2014 +0200
    74.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Sat Jul 05 11:01:53 2014 +0200
    74.3 @@ -76,7 +76,7 @@
    74.4  val presburger_ss = simpset_of (@{context} addsimps [zdvd1_eq]);
    74.5  val lin_ss =
    74.6    simpset_of (put_simpset presburger_ss @{context}
    74.7 -    addsimps (@{thm dvd_eq_mod_eq_0} :: zdvd1_eq :: @{thms add_ac [where 'a=int]}));
    74.8 +    addsimps (@{thm dvd_eq_mod_eq_0} :: zdvd1_eq :: @{thms ac_simps [where 'a=int]}));
    74.9  
   74.10  val iT = HOLogic.intT
   74.11  val bT = HOLogic.boolT;
   74.12 @@ -826,7 +826,7 @@
   74.13      @ [@{thm "mod_self"}, @{thm "mod_by_0"}, @{thm "div_by_0"},
   74.14         @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, 
   74.15         @{thm "mod_1"}, @{thm "Suc_eq_plus1"}]
   74.16 -    @ @{thms add_ac}
   74.17 +    @ @{thms ac_simps}
   74.18     addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}])
   74.19  val splits_ss =
   74.20    simpset_of (put_simpset comp_ss @{context}
    75.1 --- a/src/HOL/Tools/group_cancel.ML	Sat Jul 05 10:09:01 2014 +0200
    75.2 +++ b/src/HOL/Tools/group_cancel.ML	Sat Jul 05 11:01:53 2014 +0200
    75.3 @@ -19,13 +19,13 @@
    75.4  struct
    75.5  
    75.6  val add1 = @{lemma "(A::'a::comm_monoid_add) == k + a ==> A + b == k + (a + b)"
    75.7 -      by (simp only: add_ac)}
    75.8 +      by (simp only: ac_simps)}
    75.9  val add2 = @{lemma "(B::'a::comm_monoid_add) == k + b ==> a + B == k + (a + b)"
   75.10 -      by (simp only: add_ac)}
   75.11 +      by (simp only: ac_simps)}
   75.12  val sub1 = @{lemma "(A::'a::ab_group_add) == k + a ==> A - b == k + (a - b)"
   75.13        by (simp only: add_diff_eq)}
   75.14  val sub2 = @{lemma "(B::'a::ab_group_add) == k + b ==> a - B == - k + (a - b)"
   75.15 -      by (simp only: minus_add diff_conv_add_uminus add_ac)}
   75.16 +      by (simp only: minus_add diff_conv_add_uminus ac_simps)}
   75.17  val neg1 = @{lemma "(A::'a::ab_group_add) == k + a ==> - A == - k + - a"
   75.18        by (simp only: minus_add_distrib)}
   75.19  val rule0 = @{lemma "(a::'a::comm_monoid_add) == a + 0"
    76.1 --- a/src/HOL/Tools/nat_arith.ML	Sat Jul 05 10:09:01 2014 +0200
    76.2 +++ b/src/HOL/Tools/nat_arith.ML	Sat Jul 05 11:01:53 2014 +0200
    76.3 @@ -16,9 +16,9 @@
    76.4  struct
    76.5  
    76.6  val add1 = @{lemma "(A::'a::comm_monoid_add) == k + a ==> A + b == k + (a + b)"
    76.7 -      by (simp only: add_ac)}
    76.8 +      by (simp only: ac_simps)}
    76.9  val add2 = @{lemma "(B::'a::comm_monoid_add) == k + b ==> a + B == k + (a + b)"
   76.10 -      by (simp only: add_ac)}
   76.11 +      by (simp only: ac_simps)}
   76.12  val suc1 = @{lemma "A == k + a ==> Suc A == k + Suc a"
   76.13        by (simp only: add_Suc_right)}
   76.14  val rule0 = @{lemma "(a::'a::comm_monoid_add) == a + 0"
    77.1 --- a/src/HOL/Tools/nat_numeral_simprocs.ML	Sat Jul 05 10:09:01 2014 +0200
    77.2 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Sat Jul 05 11:01:53 2014 +0200
    77.3 @@ -167,10 +167,10 @@
    77.4    val norm_ss1 =
    77.5      simpset_of (put_simpset Numeral_Simprocs.num_ss @{context}
    77.6        addsimps numeral_syms @ add_0s @ mult_1s @
    77.7 -        [@{thm Suc_eq_plus1_left}] @ @{thms add_ac})
    77.8 +        [@{thm Suc_eq_plus1_left}] @ @{thms ac_simps})
    77.9    val norm_ss2 =
   77.10      simpset_of (put_simpset Numeral_Simprocs.num_ss @{context}
   77.11 -      addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac})
   77.12 +      addsimps bin_simps @ @{thms ac_simps} @ @{thms ac_simps})
   77.13    fun norm_tac ctxt = 
   77.14      ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt))
   77.15      THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt))
   77.16 @@ -239,10 +239,10 @@
   77.17  
   77.18    val norm_ss1 =
   77.19      simpset_of (put_simpset Numeral_Simprocs.num_ss @{context}
   77.20 -      addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1}] @ @{thms add_ac})
   77.21 +      addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1}] @ @{thms ac_simps})
   77.22    val norm_ss2 =
   77.23      simpset_of (put_simpset Numeral_Simprocs.num_ss @{context}
   77.24 -      addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac})
   77.25 +      addsimps bin_simps @ @{thms ac_simps} @ @{thms ac_simps})
   77.26    fun norm_tac ctxt =
   77.27      ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt))
   77.28      THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt))
   77.29 @@ -270,10 +270,10 @@
   77.30  
   77.31    val norm_ss1 =
   77.32      simpset_of (put_simpset Numeral_Simprocs.num_ss @{context}
   77.33 -      addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1_left}] @ @{thms add_ac})
   77.34 +      addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1_left}] @ @{thms ac_simps})
   77.35    val norm_ss2 =
   77.36      simpset_of (put_simpset Numeral_Simprocs.num_ss @{context}
   77.37 -      addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac})
   77.38 +      addsimps bin_simps @ @{thms ac_simps} @ @{thms ac_simps})
   77.39    fun norm_tac ctxt =
   77.40      ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt))
   77.41      THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt))
   77.42 @@ -363,7 +363,7 @@
   77.43    val trans_tac = Numeral_Simprocs.trans_tac
   77.44    val norm_ss =
   77.45      simpset_of (put_simpset HOL_basic_ss @{context}
   77.46 -      addsimps mult_1s @ @{thms mult_ac})
   77.47 +      addsimps mult_1s @ @{thms ac_simps})
   77.48    fun norm_tac ctxt =
   77.49      ALLGOALS (simp_tac (put_simpset norm_ss ctxt))
   77.50    val simplify_meta_eq  = cancel_simplify_meta_eq
    78.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Sat Jul 05 10:09:01 2014 +0200
    78.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Sat Jul 05 11:01:53 2014 +0200
    78.3 @@ -232,7 +232,7 @@
    78.4  val norm_ss1 =
    78.5    simpset_of (put_simpset num_ss @{context}
    78.6      addsimps numeral_syms @ add_0s @ mult_1s @
    78.7 -    diff_simps @ minus_simps @ @{thms add_ac})
    78.8 +    diff_simps @ minus_simps @ @{thms ac_simps})
    78.9  
   78.10  val norm_ss2 =
   78.11    simpset_of (put_simpset num_ss @{context}
   78.12 @@ -240,7 +240,7 @@
   78.13  
   78.14  val norm_ss3 =
   78.15    simpset_of (put_simpset num_ss @{context}
   78.16 -    addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac minus_mult_commute})
   78.17 +    addsimps minus_from_mult_simps @ @{thms ac_simps} @ @{thms ac_simps minus_mult_commute})
   78.18  
   78.19  structure CancelNumeralsCommon =
   78.20  struct
   78.21 @@ -361,7 +361,7 @@
   78.22  
   78.23  structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
   78.24  struct
   78.25 -  val assoc_ss = simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms mult_ac minus_mult_commute})
   78.26 +  val assoc_ss = simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms ac_simps minus_mult_commute})
   78.27    val eq_reflection = eq_reflection
   78.28    val is_numeral = can HOLogic.dest_number
   78.29  end;
   78.30 @@ -381,7 +381,7 @@
   78.31    val norm_ss2 =
   78.32      simpset_of (put_simpset HOL_basic_ss @{context} addsimps simps @ mult_minus_simps)
   78.33    val norm_ss3 =
   78.34 -    simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms mult_ac minus_mult_commute})
   78.35 +    simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms ac_simps minus_mult_commute})
   78.36    fun norm_tac ctxt =
   78.37      ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt))
   78.38      THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt))
   78.39 @@ -513,7 +513,7 @@
   78.40    val find_first = find_first_t []
   78.41    val trans_tac = trans_tac
   78.42    val norm_ss =
   78.43 -    simpset_of (put_simpset HOL_basic_ss @{context} addsimps mult_1s @ @{thms mult_ac minus_mult_commute})
   78.44 +    simpset_of (put_simpset HOL_basic_ss @{context} addsimps mult_1s @ @{thms ac_simps minus_mult_commute})
   78.45    fun norm_tac ctxt =
   78.46      ALLGOALS (simp_tac (put_simpset norm_ss ctxt))
   78.47    val simplify_meta_eq  = cancel_simplify_meta_eq 
    79.1 --- a/src/HOL/Transcendental.thy	Sat Jul 05 10:09:01 2014 +0200
    79.2 +++ b/src/HOL/Transcendental.thy	Sat Jul 05 11:01:53 2014 +0200
    79.3 @@ -481,10 +481,10 @@
    79.4    apply (rule setsum.cong [OF refl])
    79.5    apply (simp add: less_iff_Suc_add)
    79.6    apply (clarify)
    79.7 -  apply (simp add: setsum_right_distrib lemma_realpow_diff_sumr2 mult_ac
    79.8 +  apply (simp add: setsum_right_distrib lemma_realpow_diff_sumr2 ac_simps
    79.9                del: setsum_lessThan_Suc power_Suc)
   79.10    apply (subst mult.assoc [symmetric], subst power_add [symmetric])
   79.11 -  apply (simp add: mult_ac)
   79.12 +  apply (simp add: ac_simps)
   79.13    done
   79.14  
   79.15  lemma real_setsum_nat_ivl_bounded2:
   79.16 @@ -958,7 +958,7 @@
   79.17      hence "norm (x * S n) \<le> real (Suc n) * r * norm (S n)"
   79.18        by (rule order_trans [OF norm_mult_ineq])
   79.19      hence "norm (x * S n) / real (Suc n) \<le> r * norm (S n)"
   79.20 -      by (simp add: pos_divide_le_eq mult_ac)
   79.21 +      by (simp add: pos_divide_le_eq ac_simps)
   79.22      thus "norm (S (Suc n)) \<le> r * norm (S n)"
   79.23        by (simp add: S_Suc inverse_eq_divide)
   79.24    qed
   79.25 @@ -1058,7 +1058,7 @@
   79.26      by (rule distrib_right)
   79.27    also have "\<dots> = (\<Sum>i\<le>n. (x * S x i) * S y (n-i))
   79.28                  + (\<Sum>i\<le>n. S x i * (y * S y (n-i)))"
   79.29 -    by (simp only: setsum_right_distrib mult_ac)
   79.30 +    by (simp only: setsum_right_distrib ac_simps)
   79.31    also have "\<dots> = (\<Sum>i\<le>n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i)))
   79.32                  + (\<Sum>i\<le>n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))"
   79.33      by (simp add: times_S Suc_diff_le)
   79.34 @@ -1431,7 +1431,7 @@
   79.35        by (rule mult_mono)
   79.36          (rule mult_mono, simp_all add: power_le_one a b)
   79.37      hence "inverse (fact (n + 2)) * x ^ (n + 2) \<le> (x\<^sup>2/2) * ((1/2)^n)"
   79.38 -      unfolding power_add by (simp add: mult_ac del: fact_Suc) }
   79.39 +      unfolding power_add by (simp add: ac_simps del: fact_Suc) }
   79.40    note aux1 = this
   79.41    have "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums (x\<^sup>2 / 2 * (1 / (1 - 1 / 2)))"
   79.42      by (intro sums_mult geometric_sums, simp)
   79.43 @@ -2476,7 +2476,7 @@
   79.44  proof -
   79.45    have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. sin_coeff k * x ^ k) sums sin x"
   79.46      by (rule sin_converges [THEN sums_group], simp)
   79.47 -  thus ?thesis unfolding One_nat_def sin_coeff_def by (simp add: mult_ac)
   79.48 +  thus ?thesis unfolding One_nat_def sin_coeff_def by (simp add: ac_simps)
   79.49  qed
   79.50  
   79.51  lemma sin_gt_zero:
   79.52 @@ -2512,7 +2512,7 @@
   79.53  proof -
   79.54    have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. cos_coeff k * x ^ k) sums cos x"
   79.55      by (rule cos_converges [THEN sums_group], simp)
   79.56 -  thus ?thesis unfolding cos_coeff_def by (simp add: mult_ac)
   79.57 +  thus ?thesis unfolding cos_coeff_def by (simp add: ac_simps)
   79.58  qed
   79.59  
   79.60  lemmas realpow_num_eq_if = power_eq_if
   79.61 @@ -2533,7 +2533,7 @@
   79.62  apply (drule sums_summable)
   79.63  apply simp
   79.64  apply (erule suminf_pos)
   79.65 -apply (simp add: add_ac)
   79.66 +apply (simp add: ac_simps)
   79.67  done
   79.68  
   79.69  lemma cos_two_less_zero [simp]:
    80.1 --- a/src/HOL/UNITY/Comp/AllocBase.thy	Sat Jul 05 10:09:01 2014 +0200
    80.2 +++ b/src/HOL/UNITY/Comp/AllocBase.thy	Sat Jul 05 11:01:53 2014 +0200
    80.3 @@ -39,7 +39,7 @@
    80.4  (** bag_of **)
    80.5  
    80.6  lemma bag_of_append [simp]: "bag_of (l@l') = bag_of l + bag_of l'"
    80.7 -  by (induct l) (simp_all add: add_ac)
    80.8 +  by (induct l) (simp_all add: ac_simps)
    80.9  
   80.10  lemma mono_bag_of: "mono (bag_of :: 'a list => ('a::order) multiset)"
   80.11  apply (rule monoI)
   80.12 @@ -63,7 +63,7 @@
   80.13        (\<Sum>i\<in> A Int lessThan (length l). {# l!i #})"
   80.14  apply (rule_tac xs = l in rev_induct, simp)
   80.15  apply (simp add: sublist_append Int_insert_right lessThan_Suc nth_append 
   80.16 -                 bag_of_sublist_lemma add_ac)
   80.17 +                 bag_of_sublist_lemma ac_simps)
   80.18  done
   80.19  
   80.20  
    81.1 --- a/src/HOL/Word/Bool_List_Representation.thy	Sat Jul 05 10:09:01 2014 +0200
    81.2 +++ b/src/HOL/Word/Bool_List_Representation.thy	Sat Jul 05 11:01:53 2014 +0200
    81.3 @@ -783,7 +783,7 @@
    81.4    apply (case_tac binb rule: bin_exhaust)
    81.5    apply (case_tac b)
    81.6     apply (case_tac [!] "ba")
    81.7 -     apply (auto simp: rbl_succ bin_to_bl_aux_alt Let_def add_ac)
    81.8 +     apply (auto simp: rbl_succ bin_to_bl_aux_alt Let_def ac_simps)
    81.9    done
   81.10  
   81.11  lemma rbl_add_app2: 
   81.12 @@ -1021,7 +1021,7 @@
   81.13     apply (erule allE)
   81.14     apply (erule (1) impE)
   81.15     apply (drule bin_nth_split, erule conjE, erule allE,
   81.16 -          erule trans, simp add : add_ac)+
   81.17 +          erule trans, simp add : ac_simps)+
   81.18    done
   81.19  
   81.20  lemma bin_rsplit_all:
    82.1 --- a/src/HOL/Word/Word.thy	Sat Jul 05 10:09:01 2014 +0200
    82.2 +++ b/src/HOL/Word/Word.thy	Sat Jul 05 11:01:53 2014 +0200
    82.3 @@ -1592,7 +1592,7 @@
    82.4  lemma no_olen_add':
    82.5    fixes x :: "'a::len0 word"
    82.6    shows "(x \<le> y + x) = (uint y + uint x < 2 ^ len_of TYPE('a))"
    82.7 -  by (simp add: add_ac no_olen_add)
    82.8 +  by (simp add: ac_simps no_olen_add)
    82.9  
   82.10  lemmas olen_add_eqv = trans [OF no_olen_add no_olen_add' [symmetric]]
   82.11  
   82.12 @@ -1906,7 +1906,7 @@
   82.13  
   82.14  lemma Abs_fnat_hom_Suc:
   82.15    "word_succ (of_nat a) = of_nat (Suc a)"
   82.16 -  by (simp add: word_of_nat wi_hom_succ add_ac)
   82.17 +  by (simp add: word_of_nat wi_hom_succ ac_simps)
   82.18  
   82.19  lemma Abs_fnat_hom_0: "(0::'a::len word) = of_nat 0"
   82.20    by simp
    83.1 --- a/src/HOL/Word/Word_Miscellaneous.thy	Sat Jul 05 10:09:01 2014 +0200
    83.2 +++ b/src/HOL/Word/Word_Miscellaneous.thy	Sat Jul 05 11:01:53 2014 +0200
    83.3 @@ -331,7 +331,7 @@
    83.4     prefer 2
    83.5     apply (erule asm_rl)
    83.6    apply (rule_tac f="%n. n div f" in arg_cong)
    83.7 -  apply (simp add : mult_ac)
    83.8 +  apply (simp add : ac_simps)
    83.9    done
   83.10      
   83.11  lemma diff_mod_le: "(a::nat) < d ==> b dvd d ==> a - a mod b <= d - b"
    84.1 --- a/src/HOL/ex/Dedekind_Real.thy	Sat Jul 05 10:09:01 2014 +0200
    84.2 +++ b/src/HOL/ex/Dedekind_Real.thy	Sat Jul 05 11:01:53 2014 +0200
    84.3 @@ -285,7 +285,7 @@
    84.4    show "\<exists>x' \<in> A. \<exists>y'\<in>B. z = x' + y'"
    84.5    proof (intro bexI)
    84.6      show "z = x*?f + y*?f"
    84.7 -      by (simp add: distrib_right [symmetric] divide_inverse mult_ac
    84.8 +      by (simp add: distrib_right [symmetric] divide_inverse ac_simps
    84.9            order_less_imp_not_eq2)
   84.10    next
   84.11      show "y * ?f \<in> B"
   84.12 @@ -326,7 +326,7 @@
   84.13  
   84.14  lemma preal_add_assoc: "((x::preal) + y) + z = x + (y + z)"
   84.15  apply (simp add: preal_add_def mem_add_set Rep_preal)
   84.16 -apply (force simp add: add_set_def add_ac)
   84.17 +apply (force simp add: add_set_def ac_simps)
   84.18  done
   84.19  
   84.20  instance preal :: ab_semigroup_add
   84.21 @@ -454,7 +454,7 @@
   84.22  
   84.23  lemma preal_mult_assoc: "((x::preal) * y) * z = x * (y * z)"
   84.24  apply (simp add: preal_mult_def mem_mult_set Rep_preal)
   84.25 -apply (force simp add: mult_set_def mult_ac)
   84.26 +apply (force simp add: mult_set_def ac_simps)
   84.27  done
   84.28  
   84.29  instance preal :: ab_semigroup_mult
   84.30 @@ -713,7 +713,7 @@
   84.31    have frle: "Fract a b \<le> Fract ?k 1 * (Fract c d)" 
   84.32    proof -
   84.33      have "?thesis = ((a * d * b * d) \<le> c * b * (a * d * b * d))"
   84.34 -      by (simp add: order_less_imp_not_eq2 mult_ac) 
   84.35 +      by (simp add: order_less_imp_not_eq2 ac_simps) 
   84.36      moreover
   84.37      have "(1 * (a * d * b * d)) \<le> c * b * (a * d * b * d)"
   84.38        by (rule mult_mono, 
   84.39 @@ -961,7 +961,7 @@
   84.40  apply (drule Rep_preal [THEN preal_exists_greater], clarify) 
   84.41  apply (cut_tac a="x+y" and b=u in add_eq_exists, clarify)  
   84.42  apply (rule_tac x="y+xa" in exI) 
   84.43 -apply (auto simp add: add_ac)
   84.44 +apply (auto simp add: ac_simps)
   84.45  done
   84.46  
   84.47  lemma mem_diff_set:
   84.48 @@ -1032,7 +1032,7 @@
   84.49    proof (intro exI conjI)
   84.50      show "r \<in> Rep_preal R" by (rule r)
   84.51      show "r + e \<notin> Rep_preal R" by (rule notin)
   84.52 -    show "r + e + y \<in> Rep_preal S" using xe eq by (simp add: add_ac)
   84.53 +    show "r + e + y \<in> Rep_preal S" using xe eq by (simp add: ac_simps)
   84.54      show "x = r + y" by (simp add: eq)
   84.55      show "0 < r + e" using epos preal_imp_pos [OF Rep_preal r]
   84.56        by simp
   84.57 @@ -1236,11 +1236,11 @@
   84.58      and "x + y2 = x2 + y"
   84.59    shows "x1 + y2 = x2 + (y1::preal)"
   84.60  proof -
   84.61 -  have "(x1 + y2) + x = (x + y2) + x1" by (simp add: add_ac)
   84.62 +  have "(x1 + y2) + x = (x + y2) + x1" by (simp add: ac_simps)
   84.63    also have "... = (x2 + y) + x1"  by (simp add: assms)
   84.64 -  also have "... = x2 + (x1 + y)"  by (simp add: add_ac)
   84.65 +  also have "... = x2 + (x1 + y)"  by (simp add: ac_simps)
   84.66    also have "... = x2 + (x + y1)"  by (simp add: assms)
   84.67 -  also have "... = (x2 + y1) + x"  by (simp add: add_ac)
   84.68 +  also have "... = (x2 + y1) + x"  by (simp add: ac_simps)
   84.69    finally have "(x1 + y2) + x = (x2 + y1) + x" .
   84.70    thus ?thesis by (rule add_right_imp_eq)
   84.71  qed
   84.72 @@ -1287,7 +1287,7 @@
   84.73  apply (simp add: add.assoc)
   84.74  apply (rule add.left_commute [of ab, THEN ssubst])
   84.75  apply (simp add: add.assoc [symmetric])
   84.76 -apply (simp add: add_ac)
   84.77 +apply (simp add: ac_simps)
   84.78  done
   84.79  
   84.80  lemma real_add:
   84.81 @@ -1318,7 +1318,7 @@
   84.82    show "x + y = y + x"
   84.83      by (cases x, cases y, simp add: real_add add.commute)
   84.84    show "0 + x = x"
   84.85 -    by (cases x, simp add: real_add real_zero_def add_ac)
   84.86 +    by (cases x, simp add: real_add real_zero_def ac_simps)
   84.87    show "- x + x = 0"
   84.88      by (cases x, simp add: real_minus real_add real_zero_def add.commute)
   84.89    show "x - y = x + - y"
   84.90 @@ -1354,7 +1354,7 @@
   84.91           UN_equiv_class2 [OF equiv_realrel equiv_realrel real_mult_congruent2])
   84.92  
   84.93  lemma real_mult_commute: "(z::real) * w = w * z"
   84.94 -by (cases z, cases w, simp add: real_mult add_ac mult_ac)
   84.95 +by (cases z, cases w, simp add: real_mult ac_simps ac_simps)
   84.96  
   84.97  lemma real_mult_assoc: "((z1::real) * z2) * z3 = z1 * (z2 * z3)"
   84.98  apply (cases z1, cases z2, cases z3)
   84.99 @@ -1456,7 +1456,7 @@
  84.100    shows "x1 + y2 \<le> x2 + (y1::preal)"
  84.101  proof -
  84.102    have "(x1+v1) + (u2+y2) = (u1+y1) + (x2+v2)" by (simp add: assms)
  84.103 -  hence "(x1+y2) + (u2+v1) = (x2+y1) + (u1+v2)" by (simp add: add_ac)
  84.104 +  hence "(x1+y2) + (u2+v1) = (x2+y1) + (u1+v2)" by (simp add: ac_simps)
  84.105    also have "... \<le> (x2+y1) + (u2+v1)" by (simp add: assms)
  84.106    finally show ?thesis by simp
  84.107  qed
  84.108 @@ -1477,10 +1477,10 @@
  84.109      and "x2 + v2 = u2 + y2"
  84.110    shows "x + v' \<le> u' + (y::preal)"
  84.111  proof -
  84.112 -  have "(x+v') + (u+v) = (x+v) + (u+v')" by (simp add: add_ac)
  84.113 +  have "(x+v') + (u+v) = (x+v) + (u+v')" by (simp add: ac_simps)
  84.114    also have "... \<le> (u+y) + (u+v')" by (simp add: assms)
  84.115    also have "... \<le> (u+y) + (u'+v)" by (simp add: assms)
  84.116 -  also have "... = (u'+y) + (u+v)"  by (simp add: add_ac)
  84.117 +  also have "... = (u'+y) + (u+v)"  by (simp add: ac_simps)
  84.118    finally show ?thesis by simp
  84.119  qed
  84.120  
  84.121 @@ -1500,7 +1500,7 @@
  84.122  (* Axiom 'linorder_linear' of class 'linorder': *)
  84.123  lemma real_le_linear: "(z::real) \<le> w | w \<le> z"
  84.124  apply (cases z, cases w)
  84.125 -apply (auto simp add: real_le real_zero_def add_ac)
  84.126 +apply (auto simp add: real_le real_zero_def ac_simps)
  84.127  done
  84.128  
  84.129  instance real :: linorder
  84.130 @@ -1509,7 +1509,7 @@
  84.131  lemma real_le_eq_diff: "(x \<le> y) = (x-y \<le> (0::real))"
  84.132  apply (cases x, cases y) 
  84.133  apply (auto simp add: real_le real_zero_def real_diff_def real_add real_minus
  84.134 -                      add_ac)
  84.135 +                      ac_simps)
  84.136  apply (simp_all add: add.assoc [symmetric])
  84.137  done
  84.138  
  84.139 @@ -1589,7 +1589,7 @@
  84.140  lemma real_of_preal_trichotomy:
  84.141        "\<exists>m. (x::real) = real_of_preal m | x = 0 | x = -(real_of_preal m)"
  84.142  apply (simp add: real_of_preal_def real_zero_def, cases x)
  84.143 -apply (auto simp add: real_minus add_ac)
  84.144 +apply (auto simp add: real_minus ac_simps)
  84.145  apply (cut_tac x = xa and y = y in linorder_less_linear)
  84.146  apply (auto dest!: less_add_left_Ex simp add: add.assoc [symmetric])
  84.147  done
  84.148 @@ -1616,9 +1616,9 @@
  84.149  lemma real_of_preal_zero_less: "0 < real_of_preal m"
  84.150  apply (insert preal_self_less_add_left [of 1 m])
  84.151  apply (auto simp add: real_zero_def real_of_preal_def
  84.152 -                      real_less_def real_le_def add_ac)
  84.153 +                      real_less_def real_le_def ac_simps)
  84.154  apply (rule_tac x="m + 1" in exI, rule_tac x="1" in exI)
  84.155 -apply (simp add: add_ac)
  84.156 +apply (simp add: ac_simps)
  84.157  done
  84.158  
  84.159  lemma real_of_preal_minus_less_zero: "- real_of_preal m < 0"
    85.1 --- a/src/HOL/ex/Sqrt.thy	Sat Jul 05 10:09:01 2014 +0200
    85.2 +++ b/src/HOL/ex/Sqrt.thy	Sat Jul 05 11:01:53 2014 +0200
    85.3 @@ -33,7 +33,7 @@
    85.4      from eq have "p dvd m\<^sup>2" ..
    85.5      with `prime p` show "p dvd m" by (rule prime_dvd_power_nat)
    85.6      then obtain k where "m = p * k" ..
    85.7 -    with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square mult_ac)
    85.8 +    with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square ac_simps)
    85.9      with p have "n\<^sup>2 = p * k\<^sup>2" by (simp add: power2_eq_square)
   85.10      then have "p dvd n\<^sup>2" ..
   85.11      with `prime p` show "p dvd n" by (rule prime_dvd_power_nat)
   85.12 @@ -73,7 +73,7 @@
   85.13    then have "p dvd m\<^sup>2" ..
   85.14    with `prime p` have dvd_m: "p dvd m" by (rule prime_dvd_power_nat)
   85.15    then obtain k where "m = p * k" ..
   85.16 -  with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square mult_ac)
   85.17 +  with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square ac_simps)
   85.18    with p have "n\<^sup>2 = p * k\<^sup>2" by (simp add: power2_eq_square)
   85.19    then have "p dvd n\<^sup>2" ..
   85.20    with `prime p` have "p dvd n" by (rule prime_dvd_power_nat)
    86.1 --- a/src/HOL/ex/Sqrt_Script.thy	Sat Jul 05 10:09:01 2014 +0200
    86.2 +++ b/src/HOL/ex/Sqrt_Script.thy	Sat Jul 05 11:01:53 2014 +0200
    86.3 @@ -36,7 +36,7 @@
    86.4    done
    86.5  
    86.6  lemma rearrange: "(j::nat) * (p * j) = k * k \<Longrightarrow> k * k = p * (j * j)"
    86.7 -  by (simp add: mult_ac)
    86.8 +  by (simp add: ac_simps)
    86.9  
   86.10  lemma prime_not_square:
   86.11      "prime (p::nat) \<Longrightarrow> (\<And>k. 0 < k \<Longrightarrow> m * m \<noteq> p * (k * k))"
    87.1 --- a/src/HOL/ex/ThreeDivides.thy	Sat Jul 05 10:09:01 2014 +0200
    87.2 +++ b/src/HOL/ex/ThreeDivides.thy	Sat Jul 05 11:01:53 2014 +0200
    87.3 @@ -80,7 +80,7 @@
    87.4    hence "?thr dvd (10^(n+1) - 10)" by (simp add: nat_distrib)
    87.5    ultimately
    87.6    have"?thr dvd ((10^(n+1) - 10) + 9)"
    87.7 -    by (simp only: add_ac) (rule dvd_add)
    87.8 +    by (simp only: ac_simps) (rule dvd_add)
    87.9    thus ?case by simp
   87.10  qed
   87.11  
   87.12 @@ -194,7 +194,7 @@
   87.13        "m = 10*(\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x) + c" by simp
   87.14      also have
   87.15        "\<dots> = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^(x+1)) + c"
   87.16 -      by (subst setsum_right_distrib) (simp add: mult_ac)
   87.17 +      by (subst setsum_right_distrib) (simp add: ac_simps)
   87.18      also have
   87.19        "\<dots> = (\<Sum>x<nd. m div 10^(Suc x) mod 10 * 10^(Suc x)) + c"
   87.20        by (simp add: div_mult2_eq[symmetric])