--- a/src/Doc/How_to_Prove_it/How_to_Prove_it.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/Doc/How_to_Prove_it/How_to_Prove_it.thy Sat Jul 05 11:01:53 2014 +0200
@@ -113,10 +113,10 @@
Because @{thm[source]algebra_simps} multiplies out, terms can explode.
If one merely wants to bring sums or products into a canonical order
-it suffices to rewrite with @{thm [source] add_ac} or @{thm [source] mult_ac}: *}
+it suffices to rewrite with @{thm [source] ac_simps}: *}
lemma fixes f :: "int \<Rightarrow> int" shows "f(x*y*z) - f(z*x*y) = 0"
-by(simp add: mult_ac)
+by(simp add: ac_simps)
text{* The lemmas @{thm[source]algebra_simps} take care of addition, subtraction
and multiplication (algebraic structures up to rings) but ignore division (fields).
--- a/src/Doc/Tutorial/Types/Numbers.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/Doc/Tutorial/Types/Numbers.thy Sat Jul 05 11:01:53 2014 +0200
@@ -40,14 +40,14 @@
@{thm[display] add.left_commute[no_vars]}
\rulename{add.left_commute}
-these form add_ac; similarly there is mult_ac
+these form ac_simps; similarly there is ac_simps
*}
lemma "Suc(i + j*l*k + m*n) = f (n*m + i + k*j*l)"
txt{*
@{subgoals[display,indent=0,margin=65]}
*};
-apply (simp add: add_ac mult_ac)
+apply (simp add: ac_simps ac_simps)
txt{*
@{subgoals[display,indent=0,margin=65]}
*};
--- a/src/Doc/Tutorial/document/numerics.tex Sat Jul 05 10:09:01 2014 +0200
+++ b/src/Doc/Tutorial/document/numerics.tex Sat Jul 05 11:01:53 2014 +0200
@@ -447,9 +447,9 @@
a\ +\ (b\ +\ c)\ =\ b\ +\ (a\ +\ c)
\rulename{add.left_commute}
\end{isabelle}
-The name \isa{add_ac}\index{*add_ac (theorems)}
+The name \isa{ac_simps}\index{*ac_simps (theorems)}
refers to the list of all three theorems; similarly
-there is \isa{mult_ac}.\index{*mult_ac (theorems)}
+there is \isa{ac_simps}.\index{*ac_simps (theorems)}
They are all proved for semirings and therefore hold for all numeric types.
Here is an example of the sorting effect. Start
@@ -459,9 +459,9 @@
f\ (n\ *\ m\ +\ i\ +\ k\ *\ j\ *\ l)
\end{isabelle}
%
-Simplify using \isa{add_ac} and \isa{mult_ac}.
+Simplify using \isa{ac_simps} and \isa{ac_simps}.
\begin{isabelle}
-\isacommand{apply}\ (simp\ add:\ add_ac\ mult_ac)
+\isacommand{apply}\ (simp\ add:\ ac_simps\ ac_simps)
\end{isabelle}
%
Here is the resulting subgoal.
--- a/src/HOL/Algebra/IntRing.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Algebra/IntRing.thy Sat Jul 05 11:01:53 2014 +0200
@@ -290,7 +290,7 @@
apply (subst int_Idl_subset_ideal, subst int_Idl, simp)
apply (rule, clarify)
apply (simp add: dvd_def)
- apply (simp add: dvd_def mult_ac)
+ apply (simp add: dvd_def ac_simps)
done
lemma dvds_eq_Idl: "l dvd k \<and> k dvd l \<longleftrightarrow> Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l}"
--- a/src/HOL/Decision_Procs/Cooper.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy Sat Jul 05 11:01:53 2014 +0200
@@ -1695,7 +1695,7 @@
also have "\<dots> \<longleftrightarrow> j dvd (- (c * x - ?e))"
by (simp only: dvd_minus_iff)
also have "\<dots> \<longleftrightarrow> j dvd (c * (- x)) + ?e"
- by (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] add_ac minus_add_distrib)
+ by (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] ac_simps minus_add_distrib)
(simp add: algebra_simps)
also have "\<dots> = Ifm bbs ((- x) # bs) (Dvd j (CN 0 c e))"
using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] by simp
@@ -1709,7 +1709,7 @@
also have "\<dots> \<longleftrightarrow> j dvd (- (c * x - ?e))"
by (simp only: dvd_minus_iff)
also have "\<dots> \<longleftrightarrow> j dvd (c * (- x)) + ?e"
- by (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] add_ac minus_add_distrib)
+ by (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] ac_simps minus_add_distrib)
(simp add: algebra_simps)
also have "\<dots> \<longleftrightarrow> Ifm bbs ((- x) # bs) (Dvd j (CN 0 c e))"
using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] by simp
--- a/src/HOL/Decision_Procs/Ferrack.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy Sat Jul 05 11:01:53 2014 +0200
@@ -1059,7 +1059,7 @@
{fix x
assume xz: "x < ?z"
hence "(real c * x < - ?e)"
- by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac)
+ by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps)
hence "real c * x + ?e < 0" by arith
hence "real c * x + ?e \<noteq> 0" by simp
with xz have "?P ?z x (Eq (CN 0 c e))"
@@ -1076,7 +1076,7 @@
{fix x
assume xz: "x < ?z"
hence "(real c * x < - ?e)"
- by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac)
+ by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps)
hence "real c * x + ?e < 0" by arith
hence "real c * x + ?e \<noteq> 0" by simp
with xz have "?P ?z x (NEq (CN 0 c e))"
@@ -1093,7 +1093,7 @@
{fix x
assume xz: "x < ?z"
hence "(real c * x < - ?e)"
- by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac)
+ by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps)
hence "real c * x + ?e < 0" by arith
with xz have "?P ?z x (Lt (CN 0 c e))"
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -1109,7 +1109,7 @@
{fix x
assume xz: "x < ?z"
hence "(real c * x < - ?e)"
- by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac)
+ by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps)
hence "real c * x + ?e < 0" by arith
with xz have "?P ?z x (Le (CN 0 c e))"
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -1125,7 +1125,7 @@
{fix x
assume xz: "x < ?z"
hence "(real c * x < - ?e)"
- by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac)
+ by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps)
hence "real c * x + ?e < 0" by arith
with xz have "?P ?z x (Gt (CN 0 c e))"
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -1141,7 +1141,7 @@
{fix x
assume xz: "x < ?z"
hence "(real c * x < - ?e)"
- by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac)
+ by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps)
hence "real c * x + ?e < 0" by arith
with xz have "?P ?z x (Ge (CN 0 c e))"
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -1167,7 +1167,7 @@
{fix x
assume xz: "x > ?z"
with mult_strict_right_mono [OF xz cp] cp
- have "(real c * x > - ?e)" by (simp add: mult_ac)
+ have "(real c * x > - ?e)" by (simp add: ac_simps)
hence "real c * x + ?e > 0" by arith
hence "real c * x + ?e \<noteq> 0" by simp
with xz have "?P ?z x (Eq (CN 0 c e))"
@@ -1184,7 +1184,7 @@
{fix x
assume xz: "x > ?z"
with mult_strict_right_mono [OF xz cp] cp
- have "(real c * x > - ?e)" by (simp add: mult_ac)
+ have "(real c * x > - ?e)" by (simp add: ac_simps)
hence "real c * x + ?e > 0" by arith
hence "real c * x + ?e \<noteq> 0" by simp
with xz have "?P ?z x (NEq (CN 0 c e))"
@@ -1201,7 +1201,7 @@
{fix x
assume xz: "x > ?z"
with mult_strict_right_mono [OF xz cp] cp
- have "(real c * x > - ?e)" by (simp add: mult_ac)
+ have "(real c * x > - ?e)" by (simp add: ac_simps)
hence "real c * x + ?e > 0" by arith
with xz have "?P ?z x (Lt (CN 0 c e))"
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -1217,7 +1217,7 @@
{fix x
assume xz: "x > ?z"
with mult_strict_right_mono [OF xz cp] cp
- have "(real c * x > - ?e)" by (simp add: mult_ac)
+ have "(real c * x > - ?e)" by (simp add: ac_simps)
hence "real c * x + ?e > 0" by arith
with xz have "?P ?z x (Le (CN 0 c e))"
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -1233,7 +1233,7 @@
{fix x
assume xz: "x > ?z"
with mult_strict_right_mono [OF xz cp] cp
- have "(real c * x > - ?e)" by (simp add: mult_ac)
+ have "(real c * x > - ?e)" by (simp add: ac_simps)
hence "real c * x + ?e > 0" by arith
with xz have "?P ?z x (Gt (CN 0 c e))"
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -1249,7 +1249,7 @@
{fix x
assume xz: "x > ?z"
with mult_strict_right_mono [OF xz cp] cp
- have "(real c * x > - ?e)" by (simp add: mult_ac)
+ have "(real c * x > - ?e)" by (simp add: ac_simps)
hence "real c * x + ?e > 0" by arith
with xz have "?P ?z x (Ge (CN 0 c e))"
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
--- a/src/HOL/Decision_Procs/MIR.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Sat Jul 05 11:01:53 2014 +0200
@@ -1542,10 +1542,10 @@
have th': "(real ?nt)*(real x) = real (?nt * x)" by simp
have "?I x (Floor t) = ?I x (Floor (CN 0 ?nt ?at))" using th2 by simp
also have "\<dots> = real (floor ((real ?nt)* real(x) + ?I x ?at))" by simp
- also have "\<dots> = real (floor (?I x ?at + real (?nt* x)))" by (simp add: add_ac)
+ also have "\<dots> = real (floor (?I x ?at + real (?nt* x)))" by (simp add: ac_simps)
also have "\<dots> = real (floor (?I x ?at) + (?nt* x))"
using floor_add[where x="?I x ?at" and a="?nt* x"] by simp
- also have "\<dots> = real (?nt)*(real x) + real (floor (?I x ?at))" by (simp add: add_ac)
+ also have "\<dots> = real (?nt)*(real x) + real (floor (?I x ?at))" by (simp add: ac_simps)
finally have "?I x (Floor t) = ?I x (CN 0 n a)" using th by simp
with na show ?case by simp
qed
@@ -1733,7 +1733,7 @@
{assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Lt a))"
by (simp add: nb Let_def split_def isint_Floor isint_neg)
have "?I (Lt a) = (real (?c * i) + (?N ?r) < 0)" using Ia by (simp add: Let_def split_def)
- 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)
+ 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)
finally have ?case using l by simp}
ultimately show ?case by blast
next
@@ -1758,7 +1758,7 @@
{assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Le a))"
by (simp add: nb Let_def split_def isint_Floor isint_neg)
have "?I (Le a) = (real (?c * i) + (?N ?r) \<le> 0)" using Ia by (simp add: Let_def split_def)
- 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)
+ 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)
finally have ?case using l by simp}
ultimately show ?case by blast
next
@@ -1783,7 +1783,7 @@
{assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Gt a))"
by (simp add: nb Let_def split_def isint_Floor isint_neg)
have "?I (Gt a) = (real (?c * i) + (?N ?r) > 0)" using Ia by (simp add: Let_def split_def)
- 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)
+ 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)
finally have ?case using l by simp}
ultimately show ?case by blast
next
@@ -1808,7 +1808,7 @@
{assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Ge a))"
by (simp add: nb Let_def split_def isint_Floor isint_neg)
have "?I (Ge a) = (real (?c * i) + (?N ?r) \<ge> 0)" using Ia by (simp add: Let_def split_def)
- 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)
+ 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)
finally have ?case using l by simp}
ultimately show ?case by blast
next
@@ -1886,10 +1886,10 @@
by (simp only: rdvd_abs1[where d="j" and t="real (?c*i) + ?N ?r", symmetric]) simp
also have "\<dots> = ((abs j) dvd (floor ((?N ?r) + real (?c*i))) \<and>
(real (floor ((?N ?r) + real (?c*i))) = (real (?c*i) + (?N ?r))))"
- by(simp only: int_rdvd_real[where i="abs j" and x="real (?c*i) + (?N ?r)"]) (simp only: add_ac)
+ by(simp only: int_rdvd_real[where i="abs j" and x="real (?c*i) + (?N ?r)"]) (simp only: ac_simps)
also have "\<dots> = (?I (?l (Dvd j a)))" using cp cnz jnz
by (simp add: Let_def split_def int_rdvd_iff[symmetric]
- del: real_of_int_mult) (auto simp add: add_ac)
+ del: real_of_int_mult) (auto simp add: ac_simps)
finally have ?case using l jnz by simp }
moreover
{assume cn: "?c < 0" and cnz: "?c\<noteq>0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))"
@@ -1900,11 +1900,11 @@
by (simp only: rdvd_abs1[where d="j" and t="real (?c*i) + ?N ?r", symmetric]) simp
also have "\<dots> = ((abs j) dvd (floor ((?N ?r) + real (?c*i))) \<and>
(real (floor ((?N ?r) + real (?c*i))) = (real (?c*i) + (?N ?r))))"
- by(simp only: int_rdvd_real[where i="abs j" and x="real (?c*i) + (?N ?r)"]) (simp only: add_ac)
+ by(simp only: int_rdvd_real[where i="abs j" and x="real (?c*i) + (?N ?r)"]) (simp only: ac_simps)
also have "\<dots> = (?I (?l (Dvd j a)))" using cn cnz jnz
using rdvd_minus [where d="abs j" and t="real (?c*i + floor (?N ?r))", simplified, symmetric]
by (simp add: Let_def split_def int_rdvd_iff[symmetric]
- del: real_of_int_mult) (auto simp add: add_ac)
+ del: real_of_int_mult) (auto simp add: ac_simps)
finally have ?case using l jnz by blast }
ultimately show ?case by blast
next
@@ -1932,10 +1932,10 @@
by (simp only: rdvd_abs1[where d="j" and t="real (?c*i) + ?N ?r", symmetric]) simp
also have "\<dots> = (\<not> ((abs j) dvd (floor ((?N ?r) + real (?c*i))) \<and>
(real (floor ((?N ?r) + real (?c*i))) = (real (?c*i) + (?N ?r)))))"
- by(simp only: int_rdvd_real[where i="abs j" and x="real (?c*i) + (?N ?r)"]) (simp only: add_ac)
+ by(simp only: int_rdvd_real[where i="abs j" and x="real (?c*i) + (?N ?r)"]) (simp only: ac_simps)
also have "\<dots> = (?I (?l (NDvd j a)))" using cp cnz jnz
by (simp add: Let_def split_def int_rdvd_iff[symmetric]
- del: real_of_int_mult) (auto simp add: add_ac)
+ del: real_of_int_mult) (auto simp add: ac_simps)
finally have ?case using l jnz by simp }
moreover
{assume cn: "?c < 0" and cnz: "?c\<noteq>0" and jnz: "j\<noteq>0" hence l: "?L (?l (NDvd j a))"
@@ -1946,11 +1946,11 @@
by (simp only: rdvd_abs1[where d="j" and t="real (?c*i) + ?N ?r", symmetric]) simp
also have "\<dots> = (\<not> ((abs j) dvd (floor ((?N ?r) + real (?c*i))) \<and>
(real (floor ((?N ?r) + real (?c*i))) = (real (?c*i) + (?N ?r)))))"
- by(simp only: int_rdvd_real[where i="abs j" and x="real (?c*i) + (?N ?r)"]) (simp only: add_ac)
+ by(simp only: int_rdvd_real[where i="abs j" and x="real (?c*i) + (?N ?r)"]) (simp only: ac_simps)
also have "\<dots> = (?I (?l (NDvd j a)))" using cn cnz jnz
using rdvd_minus [where d="abs j" and t="real (?c*i + floor (?N ?r))", simplified, symmetric]
by (simp add: Let_def split_def int_rdvd_iff[symmetric]
- del: real_of_int_mult) (auto simp add: add_ac)
+ del: real_of_int_mult) (auto simp add: ac_simps)
finally have ?case using l jnz by blast }
ultimately show ?case by blast
qed auto
@@ -4159,7 +4159,7 @@
{fix x
assume xz: "x < ?z"
hence "(real c * x < - ?e)"
- by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac)
+ by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps)
hence "real c * x + ?e < 0" by arith
hence "real c * x + ?e \<noteq> 0" by simp
with xz have "?P ?z x (Eq (CN 0 c e))"
@@ -4176,7 +4176,7 @@
{fix x
assume xz: "x < ?z"
hence "(real c * x < - ?e)"
- by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac)
+ by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps)
hence "real c * x + ?e < 0" by arith
hence "real c * x + ?e \<noteq> 0" by simp
with xz have "?P ?z x (NEq (CN 0 c e))"
@@ -4193,7 +4193,7 @@
{fix x
assume xz: "x < ?z"
hence "(real c * x < - ?e)"
- by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac)
+ by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps)
hence "real c * x + ?e < 0" by arith
with xz have "?P ?z x (Lt (CN 0 c e))"
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -4209,7 +4209,7 @@
{fix x
assume xz: "x < ?z"
hence "(real c * x < - ?e)"
- by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac)
+ by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps)
hence "real c * x + ?e < 0" by arith
with xz have "?P ?z x (Le (CN 0 c e))"
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -4225,7 +4225,7 @@
{fix x
assume xz: "x < ?z"
hence "(real c * x < - ?e)"
- by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac)
+ by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps)
hence "real c * x + ?e < 0" by arith
with xz have "?P ?z x (Gt (CN 0 c e))"
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -4241,7 +4241,7 @@
{fix x
assume xz: "x < ?z"
hence "(real c * x < - ?e)"
- by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] mult_ac)
+ by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps)
hence "real c * x + ?e < 0" by arith
with xz have "?P ?z x (Ge (CN 0 c e))"
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -4267,7 +4267,7 @@
{fix x
assume xz: "x > ?z"
with mult_strict_right_mono [OF xz cp] cp
- have "(real c * x > - ?e)" by (simp add: mult_ac)
+ have "(real c * x > - ?e)" by (simp add: ac_simps)
hence "real c * x + ?e > 0" by arith
hence "real c * x + ?e \<noteq> 0" by simp
with xz have "?P ?z x (Eq (CN 0 c e))"
@@ -4284,7 +4284,7 @@
{fix x
assume xz: "x > ?z"
with mult_strict_right_mono [OF xz cp] cp
- have "(real c * x > - ?e)" by (simp add: mult_ac)
+ have "(real c * x > - ?e)" by (simp add: ac_simps)
hence "real c * x + ?e > 0" by arith
hence "real c * x + ?e \<noteq> 0" by simp
with xz have "?P ?z x (NEq (CN 0 c e))"
@@ -4301,7 +4301,7 @@
{fix x
assume xz: "x > ?z"
with mult_strict_right_mono [OF xz cp] cp
- have "(real c * x > - ?e)" by (simp add: mult_ac)
+ have "(real c * x > - ?e)" by (simp add: ac_simps)
hence "real c * x + ?e > 0" by arith
with xz have "?P ?z x (Lt (CN 0 c e))"
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -4317,7 +4317,7 @@
{fix x
assume xz: "x > ?z"
with mult_strict_right_mono [OF xz cp] cp
- have "(real c * x > - ?e)" by (simp add: mult_ac)
+ have "(real c * x > - ?e)" by (simp add: ac_simps)
hence "real c * x + ?e > 0" by arith
with xz have "?P ?z x (Le (CN 0 c e))"
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -4333,7 +4333,7 @@
{fix x
assume xz: "x > ?z"
with mult_strict_right_mono [OF xz cp] cp
- have "(real c * x > - ?e)" by (simp add: mult_ac)
+ have "(real c * x > - ?e)" by (simp add: ac_simps)
hence "real c * x + ?e > 0" by arith
with xz have "?P ?z x (Gt (CN 0 c e))"
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -4349,7 +4349,7 @@
{fix x
assume xz: "x > ?z"
with mult_strict_right_mono [OF xz cp] cp
- have "(real c * x > - ?e)" by (simp add: mult_ac)
+ have "(real c * x > - ?e)" by (simp add: ac_simps)
hence "real c * x + ?e > 0" by arith
with xz have "?P ?z x (Ge (CN 0 c e))"
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -4829,9 +4829,9 @@
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")
proof-
have "?rhs = (\<exists> (i::int). \<exists> x. 0\<le> x \<and> x < 1 \<and> Ifm (x#(real i)#bs) (exsplit p))"
- by (simp add: myless[of _ "1"] myless[of _ "0"] add_ac)
+ by (simp add: myless[of _ "1"] myless[of _ "0"] ac_simps)
also have "\<dots> = (\<exists> (i::int). \<exists> x. 0\<le> x \<and> x < 1 \<and> Ifm ((real i + x) #bs) p)"
- by (simp only: exsplit[OF qf] add_ac)
+ by (simp only: exsplit[OF qf] ac_simps)
also have "\<dots> = (\<exists> x. Ifm (x#bs) p)"
by (simp only: real_ex_int_real01[where P="\<lambda> x. Ifm (x#bs) p"])
finally show ?thesis by simp
--- a/src/HOL/Decision_Procs/Polynomial_List.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Decision_Procs/Polynomial_List.thy Sat Jul 05 11:01:53 2014 +0200
@@ -127,7 +127,7 @@
lemma (in comm_semiring_0) padd_assoc: "\<forall>b c. (a +++ b) +++ c = a +++ (b +++ c)"
apply (induct a)
apply (simp, clarify)
- apply (case_tac b, simp_all add: add_ac)
+ apply (case_tac b, simp_all add: ac_simps)
done
lemma (in semiring_0) poly_cmult_distr: "a %* ( p +++ q) = (a %* p +++ a %* q)"
@@ -152,17 +152,17 @@
next
case (Cons a as p2)
thus ?case
- by (cases p2) (simp_all add: add_ac distrib_left)
+ by (cases p2) (simp_all add: ac_simps distrib_left)
qed
lemma (in comm_semiring_0) poly_cmult: "poly (c %* p) x = c * poly p x"
apply (induct p)
apply (case_tac [2] "x = zero")
- apply (auto simp add: distrib_left mult_ac)
+ apply (auto simp add: distrib_left ac_simps)
done
lemma (in comm_semiring_0) poly_cmult_map: "poly (map (op * c) p) x = c*poly p x"
- by (induct p) (auto simp add: distrib_left mult_ac)
+ by (induct p) (auto simp add: distrib_left ac_simps)
lemma (in comm_ring_1) poly_minus: "poly (-- p) x = - (poly p x)"
apply (simp add: poly_minus_def)
@@ -176,7 +176,7 @@
next
case (Cons a as p2)
thus ?case by (cases as)
- (simp_all add: poly_cmult poly_add distrib_right distrib_left mult_ac)
+ (simp_all add: poly_cmult poly_add distrib_right distrib_left ac_simps)
qed
class idom_char_0 = idom + ring_char_0
@@ -505,7 +505,7 @@
apply (auto simp add: poly_linear_divides poly_add poly_cmult distrib_right [symmetric])
apply (rule_tac x = "pmult qa q" in exI)
apply (rule_tac [2] x = "pmult p qa" in exI)
- apply (auto simp add: poly_add poly_mult poly_cmult mult_ac)
+ apply (auto simp add: poly_add poly_mult poly_cmult ac_simps)
done
lemma (in comm_semiring_1) poly_divides_refl[simp]: "p divides p"
@@ -526,7 +526,7 @@
apply (rule_tac [2] poly_divides_trans)
apply (auto simp add: divides_def)
apply (rule_tac x = p in exI)
- apply (auto simp add: poly_mult fun_eq mult_ac)
+ apply (auto simp add: poly_mult fun_eq ac_simps)
done
lemma (in comm_semiring_1) poly_exp_divides:
@@ -550,7 +550,7 @@
lemma (in comm_ring_1) poly_divides_diff2:
"p divides r \<Longrightarrow> p divides (q +++ r) \<Longrightarrow> p divides q"
apply (erule poly_divides_diff)
- apply (auto simp add: poly_add fun_eq poly_mult divides_def add_ac)
+ apply (auto simp add: poly_add fun_eq poly_mult divides_def ac_simps)
done
lemma (in semiring_0) poly_divides_zero: "poly p = poly [] \<Longrightarrow> q divides p"
@@ -608,7 +608,7 @@
lemma (in comm_semiring_1) poly_mulexp: "poly (mulexp n p q) x = (poly p x) ^ n * poly q x"
- by (induct n) (auto simp add: poly_mult mult_ac)
+ by (induct n) (auto simp add: poly_mult ac_simps)
lemma (in comm_semiring_1) divides_left_mult:
assumes d:"(p***q) divides r" shows "p divides r \<and> q divides r"
@@ -616,7 +616,7 @@
from d obtain t where r:"poly r = poly (p***q *** t)"
unfolding divides_def by blast
hence "poly r = poly (p *** (q *** t))"
- "poly r = poly (q *** (p***t))" by(auto simp add: fun_eq poly_mult mult_ac)
+ "poly r = poly (q *** (p***t))" by(auto simp add: fun_eq poly_mult ac_simps)
thus ?thesis unfolding divides_def by blast
qed
@@ -742,7 +742,7 @@
apply (simp add: divides_def del: pexp_Suc pmult_Cons, safe)
apply (rule_tac x = q in exI, safe)
apply (drule_tac x = qa in spec)
- apply (auto simp add: poly_mult fun_eq poly_exp mult_ac simp del: pmult_Cons)
+ apply (auto simp add: poly_mult fun_eq poly_exp ac_simps simp del: pmult_Cons)
done
text{*Important composition properties of orders.*}
@@ -755,7 +755,7 @@
apply safe
apply (simp add: divides_def fun_eq poly_exp_add poly_mult del: pmult_Cons, safe)
apply (rule_tac x = "qa *** qaa" in exI)
- apply (simp add: poly_mult mult_ac del: pmult_Cons)
+ apply (simp add: poly_mult ac_simps del: pmult_Cons)
apply (drule_tac a = a in order_decomp)+
apply safe
apply (subgoal_tac "[-a,1] divides (qa *** qaa) ")
@@ -766,7 +766,7 @@
apply (drule poly_mult_left_cancel [THEN iffD1], force)
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))) ")
apply (drule poly_mult_left_cancel [THEN iffD1], force)
- apply (simp add: fun_eq poly_exp_add poly_mult mult_ac del: pmult_Cons)
+ apply (simp add: fun_eq poly_exp_add poly_mult ac_simps del: pmult_Cons)
done
lemma (in idom_char_0) order_mult:
@@ -779,7 +779,7 @@
apply safe
apply (simp add: divides_def fun_eq poly_exp_add poly_mult del: pmult_Cons, safe)
apply (rule_tac x = "pmult qa qaa" in exI)
- apply (simp add: poly_mult mult_ac del: pmult_Cons)
+ apply (simp add: poly_mult ac_simps del: pmult_Cons)
apply (drule_tac a = a in order_decomp)+
apply safe
apply (subgoal_tac "[uminus a, one] divides pmult qa qaa")
@@ -794,7 +794,7 @@
poly (pmult (pexp [uminus a, one] (order a q))
(pmult (pexp [uminus a, one] (order a p)) (pmult [uminus a, one] qb)))")
apply (drule poly_mult_left_cancel [THEN iffD1], force)
- apply (simp add: fun_eq poly_exp_add poly_mult mult_ac del: pmult_Cons)
+ apply (simp add: fun_eq poly_exp_add poly_mult ac_simps del: pmult_Cons)
done
lemma (in idom_char_0) order_root2: "poly p \<noteq> poly [] \<Longrightarrow> poly p a = 0 \<longleftrightarrow> order a p \<noteq> 0"
@@ -988,7 +988,7 @@
have eq: "poly ([a,1] %^(Suc n) *** p) = poly ([a,1] %^ n *** ([a,1] *** p))"
apply (rule ext)
apply (simp add: poly_mult poly_add poly_cmult)
- apply (simp add: mult_ac add_ac distrib_left)
+ apply (simp add: ac_simps ac_simps distrib_left)
done
note deq = degree_unique[OF eq]
show ?case
--- a/src/HOL/Decision_Procs/cooper_tac.ML Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Sat Jul 05 11:01:53 2014 +0200
@@ -53,7 +53,7 @@
div_by_0 mod_by_0 div_0 mod_0
div_by_1 mod_by_1 div_1 mod_1
Suc_eq_plus1}
- addsimps @{thms add_ac}
+ addsimps @{thms ac_simps}
addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
val simpset0 =
put_simpset HOL_basic_ss ctxt
--- a/src/HOL/Decision_Procs/mir_tac.ML Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML Sat Jul 05 11:01:53 2014 +0200
@@ -19,8 +19,7 @@
val nat_arith = [@{thm diff_nat_numeral}];
val comp_arith = [@{thm "Let_def"}, @{thm "if_False"}, @{thm "if_True"}, @{thm "add_0"},
- @{thm "add_Suc"}, @{thm add_numeral_left}, @{thm mult_numeral_left(1)},
- @{thm "Suc_eq_plus1"}] @
+ @{thm "add_Suc"}, @{thm add_numeral_left}, @{thm mult_numeral_left(1)}] @
(map (fn th => th RS sym) [@{thm "numeral_1_eq_1"}])
@ @{thms arith_simps} @ nat_arith @ @{thms rel_simps}
val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
@@ -81,7 +80,7 @@
@{thm div_0}, @{thm mod_0},
@{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
@{thm "Suc_eq_plus1"}]
- addsimps @{thms add_ac}
+ addsimps @{thms add.assoc add.commute add.left_commute}
addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
val simpset0 = put_simpset HOL_basic_ss ctxt
addsimps [mod_div_equality', @{thm Suc_eq_plus1}]
--- a/src/HOL/Deriv.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Deriv.thy Sat Jul 05 11:01:53 2014 +0200
@@ -681,7 +681,7 @@
lemma DERIV_cmult_right:
"(f has_field_derivative D) (at x within s) ==> ((\<lambda>x. f x * c) has_field_derivative D * c) (at x within s)"
- using DERIV_cmult by (force simp add: mult_ac)
+ using DERIV_cmult by (force simp add: ac_simps)
lemma DERIV_cmult_Id [simp]: "(op * c has_field_derivative c) (at x within s)"
by (cut_tac c = c and x = x in DERIV_ident [THEN DERIV_cmult], simp)
@@ -717,7 +717,7 @@
lemma DERIV_inverse_fun:
"(f has_field_derivative d) (at x within s) \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow>
((\<lambda>x. inverse (f x)) has_field_derivative (- (d * inverse(f x ^ Suc (Suc 0))))) (at x within s)"
- by (drule (1) DERIV_inverse') (simp add: mult_ac nonzero_inverse_mult_distrib)
+ by (drule (1) DERIV_inverse') (simp add: ac_simps nonzero_inverse_mult_distrib)
text {* Derivative of quotient *}
@@ -1479,7 +1479,7 @@
ultimately have "(b - a) * (g'c * (f b - f a) - f'c * (g b - g a)) = 0" by auto
with alb have "g'c * (f b - f a) - f'c * (g b - g a) = 0" by simp
hence "g'c * (f b - f a) = f'c * (g b - g a)" by simp
- hence "(f b - f a) * g'c = (g b - g a) * f'c" by (simp add: mult_ac)
+ hence "(f b - f a) * g'c = (g b - g a) * f'c" by (simp add: ac_simps)
with g'cdef f'cdef cint show ?thesis by auto
qed
--- a/src/HOL/Divides.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Divides.thy Sat Jul 05 11:01:53 2014 +0200
@@ -34,7 +34,7 @@
lemma mod_div_equality': "a mod b + a div b * b = a"
using mod_div_equality [of a b]
- by (simp only: add_ac)
+ by (simp only: ac_simps)
lemma div_mod_equality: "((a div b) * b + a mod b) + c = a + c"
by (simp add: mod_div_equality)
@@ -228,7 +228,7 @@
have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
by (simp only: mod_div_equality)
also have "\<dots> = (a mod c + b + a div c * c) mod c"
- by (simp only: add_ac)
+ by (simp only: ac_simps)
also have "\<dots> = (a mod c + b) mod c"
by (rule mod_mult_self1)
finally show ?thesis .
@@ -239,7 +239,7 @@
have "(a + b) mod c = (a + (b div c * c + b mod c)) mod c"
by (simp only: mod_div_equality)
also have "\<dots> = (a + b mod c + b div c * c) mod c"
- by (simp only: add_ac)
+ by (simp only: ac_simps)
also have "\<dots> = (a + b mod c) mod c"
by (rule mod_mult_self1)
finally show ?thesis .
@@ -321,7 +321,7 @@
also have "\<dots> = (a mod (c * k) + a div (c * k) * k * c) mod c"
by (simp only: mod_mult_self1)
also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
- by (simp only: add_ac mult_ac)
+ by (simp only: ac_simps ac_simps)
also have "\<dots> = a mod c"
by (simp only: mod_div_equality)
finally show ?thesis .
@@ -421,7 +421,7 @@
have "(- a) mod b = (- (a div b * b + a mod b)) mod b"
by (simp only: mod_div_equality)
also have "\<dots> = (- (a mod b) + - (a div b) * b) mod b"
- by (simp only: minus_add_distrib minus_mult_left add_ac)
+ by (simp add: ac_simps)
also have "\<dots> = (- (a mod b)) mod b"
by (rule mod_mult_self1)
finally show ?thesis .
@@ -957,7 +957,7 @@
val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
- (@{thm add_0_left} :: @{thm add_0_right} :: @{thms add_ac}))
+ (@{thm add_0_left} :: @{thm add_0_right} :: @{thms ac_simps}))
)
*}
@@ -1059,7 +1059,7 @@
lemma divmod_nat_rel_mult2_eq:
"divmod_nat_rel a b (q, r)
\<Longrightarrow> divmod_nat_rel a (b * c) (q div c, b *(q mod c) + r)"
-by (auto simp add: mult_ac divmod_nat_rel_def add_mult_distrib2 [symmetric] mod_lemma)
+by (auto simp add: mult.commute mult.left_commute divmod_nat_rel_def add_mult_distrib2 [symmetric] mod_lemma)
lemma div_mult2_eq: "a div (b * c) = (a div b) div (c::nat)"
by (force simp add: divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN div_nat_unique])
@@ -1147,11 +1147,15 @@
lemmas mod_eq_0D [dest!] = mod_eq_0_iff [THEN iffD1]
(*Loses information, namely we also have r<d provided d is nonzero*)
-lemma mod_eqD: "(m mod d = r) ==> \<exists>q::nat. m = r + q*d"
- apply (cut_tac a = m in mod_div_equality)
- apply (simp only: add_ac)
- apply (blast intro: sym)
- done
+lemma mod_eqD:
+ fixes m d r q :: nat
+ assumes "m mod d = r"
+ shows "\<exists>q. m = r + q * d"
+proof -
+ from mod_div_equality obtain q where "q * d + m mod d = m" by blast
+ with assms have "m = r + q * d" by simp
+ then show ?thesis ..
+qed
lemma split_div:
"P(n div k :: nat) =
@@ -1175,7 +1179,7 @@
with n j P show "P i" by simp
next
assume "i \<noteq> 0"
- with not0 n j P show "P i" by(simp add:add_ac)
+ with not0 n j P show "P i" by(simp add:ac_simps)
qed
qed
qed
@@ -1209,7 +1213,7 @@
next
assume P: ?lhs
then have "divmod_nat_rel m n (q, m - n * q)"
- unfolding divmod_nat_rel_def by (auto simp add: mult_ac)
+ unfolding divmod_nat_rel_def by (auto simp add: ac_simps)
with divmod_nat_rel_unique divmod_nat_rel [of m n]
have "(q, m - n * q) = (m div n, m mod n)" by auto
then show ?rhs by simp
@@ -1239,7 +1243,7 @@
proof (simp, intro allI impI)
fix i j
assume "n = k*i + j" "j < k"
- thus "P j" using not0 P by(simp add:add_ac mult_ac)
+ thus "P j" using not0 P by(simp add:ac_simps ac_simps)
qed
qed
next
@@ -1417,7 +1421,7 @@
(* Potential use of algebra : Equality modulo n*)
lemma mod_mult_self3 [simp]: "(k*n + m) mod n = m mod (n::nat)"
-by (simp add: mult_ac add_ac)
+by (simp add: ac_simps ac_simps)
lemma mod_mult_self4 [simp]: "Suc (k*n + m) mod n = Suc m mod n"
proof -
@@ -1614,7 +1618,7 @@
apply (case_tac "a < b")
apply simp_all
apply (erule splitE)
- apply (auto simp add: distrib_left Let_def mult_ac mult_2_right)
+ apply (auto simp add: distrib_left Let_def ac_simps mult_2_right)
done
@@ -1644,7 +1648,7 @@
apply (case_tac "a + b < (0\<Colon>int)")
apply simp_all
apply (erule splitE)
- apply (auto simp add: distrib_left Let_def mult_ac mult_2_right)
+ apply (auto simp add: distrib_left Let_def ac_simps mult_2_right)
done
@@ -1744,7 +1748,7 @@
val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
- (@{thm diff_conv_add_uminus} :: @{thms add_0s} @ @{thms add_ac}))
+ (@{thm diff_conv_add_uminus} :: @{thms add_0s} @ @{thms ac_simps}))
)
*}
@@ -2072,7 +2076,7 @@
lemma zmult1_lemma:
"[| divmod_int_rel b c (q, r) |]
==> divmod_int_rel (a * b) c (a*q + a*r div c, a*r mod c)"
-by (auto simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left mult_ac)
+by (auto simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left ac_simps)
lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
apply (case_tac "c = 0", simp)
@@ -2176,7 +2180,7 @@
lemma zmult2_lemma: "[| divmod_int_rel a b (q, r); 0 < c |]
==> divmod_int_rel a (b * c) (q div c, b*(q mod c) + r)"
-by (auto simp add: mult_ac divmod_int_rel_def linorder_neq_iff
+by (auto simp add: mult.assoc divmod_int_rel_def linorder_neq_iff
zero_less_mult_iff distrib_left [symmetric]
zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: split_if_asm)
--- a/src/HOL/Fact.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Fact.thy Sat Jul 05 11:01:53 2014 +0200
@@ -256,14 +256,10 @@
apply (induct k rule: int_ge_induct)
apply (simp add: fact_plus_one_int)
apply (subst (2) fact_reduce_int)
- apply (auto simp add: add_ac)
+ apply (auto simp add: ac_simps)
apply (erule order_less_le_trans)
- apply (subst mult_le_cancel_right1)
apply auto
- apply (subgoal_tac "fact (i + (1 + m)) >= 0")
- apply force
- apply (rule fact_ge_zero_int)
-done
+ done
lemma fact_less_mono_int: "(0::int) < m \<Longrightarrow> m < n \<Longrightarrow> fact m < fact n"
apply (insert fact_less_mono_int_aux [of "n - (m + 1)" "m"])
--- a/src/HOL/Fields.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Fields.thy Sat Jul 05 11:01:53 2014 +0200
@@ -310,7 +310,7 @@
lemma inverse_add:
"[| a \<noteq> 0; b \<noteq> 0 |]
==> inverse a + inverse b = (a + b) * inverse a * inverse b"
-by (simp add: division_ring_inverse_add mult_ac)
+by (simp add: division_ring_inverse_add ac_simps)
lemma nonzero_mult_divide_mult_cancel_left [simp]:
assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" shows "(c*a)/(c*b) = a/b"
@@ -318,7 +318,7 @@
have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
by (simp add: divide_inverse nonzero_inverse_mult_distrib)
also have "... = a * inverse b * (inverse c * c)"
- by (simp only: mult_ac)
+ by (simp only: ac_simps)
also have "... = a * inverse b" by simp
finally show ?thesis by (simp add: divide_inverse)
qed
@@ -328,7 +328,7 @@
by (simp add: mult.commute [of _ c])
lemma times_divide_eq_left [simp]: "(b / c) * a = (b * a) / c"
- by (simp add: divide_inverse mult_ac)
+ by (simp add: divide_inverse ac_simps)
text{*It's not obvious whether @{text times_divide_eq} should be
simprules or not. Their effect is to gather terms into one big
@@ -369,11 +369,11 @@
lemma nonzero_mult_divide_mult_cancel_left2 [simp]:
"\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (c * a) / (b * c) = a / b"
-using nonzero_mult_divide_mult_cancel_left [of b c a] by (simp add: mult_ac)
+using nonzero_mult_divide_mult_cancel_left [of b c a] by (simp add: ac_simps)
lemma nonzero_mult_divide_mult_cancel_right2 [simp]:
"\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (c * b) = a / b"
-using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: mult_ac)
+using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: ac_simps)
lemma diff_frac_eq:
"y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y - w / z = (x * z - w * y) / (y * z)"
@@ -398,7 +398,7 @@
"inverse (a * b) = inverse a * inverse b"
proof cases
assume "a \<noteq> 0 & b \<noteq> 0"
- thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_ac)
+ thus ?thesis by (simp add: nonzero_inverse_mult_distrib ac_simps)
next
assume "~ (a \<noteq> 0 & b \<noteq> 0)"
thus ?thesis by force
@@ -429,7 +429,7 @@
lemma divide_divide_eq_right [simp]:
"a / (b / c) = (a * c) / b"
- by (simp add: divide_inverse mult_ac)
+ by (simp add: divide_inverse ac_simps)
lemma divide_divide_eq_left [simp]:
"(a / b) / c = a / (b * c)"
--- a/src/HOL/GCD.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/GCD.thy Sat Jul 05 11:01:53 2014 +0200
@@ -1225,7 +1225,7 @@
hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)"
by (simp only: diff_add_assoc[OF dble, of d, symmetric])
hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
- by (simp only: diff_mult_distrib2 add.commute mult_ac)
+ by (simp only: diff_mult_distrib2 add.commute ac_simps)
hence ?thesis using H(1,2)
apply -
apply (rule exI[where x=d], simp)
@@ -1312,20 +1312,20 @@
from pos_k k_m have pos_p: "p > 0" by auto
from pos_k k_n have pos_q: "q > 0" by auto
have "k * k * gcd q p = k * gcd (k * q) (k * p)"
- by (simp add: mult_ac gcd_mult_distrib_nat)
+ by (simp add: ac_simps gcd_mult_distrib_nat)
also have "\<dots> = k * gcd (m * p * q) (n * q * p)"
by (simp add: k_m [symmetric] k_n [symmetric])
also have "\<dots> = k * p * q * gcd m n"
- by (simp add: mult_ac gcd_mult_distrib_nat)
+ by (simp add: ac_simps gcd_mult_distrib_nat)
finally have "(m * p) * (n * q) * gcd q p = k * p * q * gcd m n"
by (simp only: k_m [symmetric] k_n [symmetric])
then have "p * q * m * n * gcd q p = p * q * k * gcd m n"
- by (simp add: mult_ac)
+ by (simp add: ac_simps)
with pos_p pos_q have "m * n * gcd q p = k * gcd m n"
by simp
with prod_gcd_lcm_nat [of m n]
have "lcm m n * gcd q p * gcd m n = k * gcd m n"
- by (simp add: mult_ac)
+ by (simp add: ac_simps)
with pos_gcd have "lcm m n * gcd q p = k" by auto
then show ?thesis using dvd_def by auto
qed
@@ -1353,7 +1353,7 @@
have "gcd m n dvd n" by simp
then obtain k where "n = gcd m n * k" using dvd_def by auto
then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n"
- by (simp add: mult_ac)
+ by (simp add: ac_simps)
also have "\<dots> = m * k" using mpos npos gcd_zero_nat by simp
finally show ?thesis by (simp add: lcm_nat_def)
qed
--- a/src/HOL/Groups.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Groups.thy Sat Jul 05 11:01:53 2014 +0200
@@ -169,14 +169,10 @@
declare add.left_commute [algebra_simps, field_simps]
-theorems add_ac = add.assoc add.commute add.left_commute
-
end
hide_fact add_commute
-theorems add_ac = add.assoc add.commute add.left_commute
-
class semigroup_mult = times +
assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)"
begin
@@ -197,14 +193,10 @@
declare mult.left_commute [algebra_simps, field_simps]
-theorems mult_ac = mult.assoc mult.commute mult.left_commute
-
end
hide_fact mult_commute
-theorems mult_ac = mult.assoc mult.commute mult.left_commute
-
class monoid_add = zero + semigroup_add +
assumes add_0_left: "0 + a = a"
and add_0_right: "a + 0 = a"
--- a/src/HOL/Int.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Int.thy Sat Jul 05 11:01:53 2014 +0200
@@ -518,11 +518,11 @@
lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
-- {* Unfold all @{text let}s involving constants *}
- unfolding Let_def ..
+ by (fact Let_numeral) -- {* FIXME drop *}
lemma Let_neg_numeral [simp]: "Let (- numeral v) f = f (- numeral v)"
-- {* Unfold all @{text let}s involving constants *}
- unfolding Let_def ..
+ by (fact Let_neg_numeral) -- {* FIXME drop *}
text {* Unfold @{text min} and @{text max} on numerals. *}
@@ -559,7 +559,7 @@
proof -
have "0 \<le> z" by fact
also have "... < z + 1" by (rule less_add_one)
- also have "... = 1 + z" by (simp add: add_ac)
+ also have "... = 1 + z" by (simp add: ac_simps)
finally show "0 < 1 + z" .
qed
--- a/src/HOL/Library/BigO.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Library/BigO.thy Sat Jul 05 11:01:53 2014 +0200
@@ -67,7 +67,7 @@
apply (drule_tac x = "xa" in spec)+
apply (subgoal_tac "ca * abs (f xa) \<le> ca * (c * abs (g xa))")
apply (erule order_trans)
- apply (simp add: mult_ac)
+ apply (simp add: ac_simps)
apply (rule mult_left_mono, assumption)
apply (rule order_less_imp_le, assumption)
done
@@ -287,7 +287,7 @@
apply (rule mult_mono)
apply assumption+
apply auto
- apply (simp add: mult_ac abs_mult)
+ apply (simp add: ac_simps abs_mult)
done
lemma bigo_mult2 [intro]: "f *o O(g) \<subseteq> O(f * g)"
@@ -296,7 +296,7 @@
apply auto
apply (drule_tac x = x in spec)
apply (subgoal_tac "abs (f x) * abs (b x) \<le> abs (f x) * (c * abs (g x))")
- apply (force simp add: mult_ac)
+ apply (force simp add: ac_simps)
apply (rule mult_left_mono, assumption)
apply (rule abs_ge_zero)
done
@@ -328,7 +328,7 @@
also have "(\<lambda>x. 1 / f x) * (f * g) = g"
apply (simp add: func_times)
apply (rule ext)
- apply (simp add: assms nonzero_divide_eq_eq mult_ac)
+ apply (simp add: assms nonzero_divide_eq_eq ac_simps)
done
finally have "(\<lambda>x. (1::'b) / f x) * h \<in> O(g)" .
then have "f * ((\<lambda>x. (1::'b) / f x) * h) \<in> f *o O(g)"
@@ -336,7 +336,7 @@
also have "f * ((\<lambda>x. (1::'b) / f x) * h) = h"
apply (simp add: func_times)
apply (rule ext)
- apply (simp add: assms nonzero_divide_eq_eq mult_ac)
+ apply (simp add: assms nonzero_divide_eq_eq ac_simps)
done
finally show "h \<in> f *o O(g)" .
qed
@@ -432,7 +432,7 @@
apply (rule bigo_minus)
apply (subst set_minus_plus)
apply assumption
- apply (simp add: add_ac)
+ apply (simp add: ac_simps)
done
lemma bigo_add_commute: "f \<in> g +o O(h) \<longleftrightarrow> g \<in> f +o O(h)"
@@ -441,7 +441,7 @@
done
lemma bigo_const1: "(\<lambda>x. c) \<in> O(\<lambda>x. 1)"
- by (auto simp add: bigo_def mult_ac)
+ by (auto simp add: bigo_def ac_simps)
lemma bigo_const2 [intro]: "O(\<lambda>x. c) \<subseteq> O(\<lambda>x. 1)"
apply (rule bigo_elt_subset)
@@ -536,7 +536,7 @@
apply (rule mult_left_mono)
apply (erule spec)
apply simp
- apply(simp add: mult_ac)
+ apply(simp add: ac_simps)
done
lemma bigo_const_mult7 [intro]: "f =o O(g) \<Longrightarrow> (\<lambda>x. c * f x) =o O(g)"
--- a/src/HOL/Library/Discrete.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Library/Discrete.thy Sat Jul 05 11:01:53 2014 +0200
@@ -162,7 +162,7 @@
case True then have "mono (times q)" by (rule mono_times_nat)
then have "q * Max {m. m * m \<le> n} = Max (times q ` {m. m * m \<le> n})"
using sqrt_aux [of n] by (auto simp add: power2_eq_square intro: mono_Max_commute)
- then have "Max {m. m * m \<le> n} * q = Max (times q ` {m. m * m \<le> n})" by (simp add: mult_ac)
+ then have "Max {m. m * m \<le> n} * q = Max (times q ` {m. m * m \<le> n})" by (simp add: ac_simps)
then show ?thesis apply simp
apply (subst Max_le_iff)
apply auto
--- a/src/HOL/Library/Extended_Nat.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Library/Extended_Nat.thy Sat Jul 05 11:01:53 2014 +0200
@@ -169,10 +169,10 @@
lemma plus_1_eSuc:
"1 + q = eSuc q"
"q + 1 = eSuc q"
- by (simp_all add: eSuc_plus_1 add_ac)
+ by (simp_all add: eSuc_plus_1 ac_simps)
lemma iadd_Suc: "eSuc m + n = eSuc (m + n)"
- by (simp_all add: eSuc_plus_1 add_ac)
+ by (simp_all add: eSuc_plus_1 ac_simps)
lemma iadd_Suc_right: "m + eSuc n = eSuc (m + n)"
by (simp only: add.commute[of m] iadd_Suc)
@@ -523,7 +523,7 @@
val trans_tac = Numeral_Simprocs.trans_tac
val norm_ss =
simpset_of (put_simpset HOL_basic_ss @{context}
- addsimps @{thms add_ac add_0_left add_0_right})
+ addsimps @{thms ac_simps add_0_left add_0_right})
fun norm_tac ctxt = ALLGOALS (simp_tac (put_simpset norm_ss ctxt))
fun simplify_meta_eq ctxt cancel_th th =
Arith_Data.simplify_meta_eq [] ctxt
--- a/src/HOL/Library/Formal_Power_Series.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Sat Jul 05 11:01:53 2014 +0200
@@ -558,7 +558,7 @@
then have "ln y * real k + ln x > 0"
by simp
then have "exp (real k * ln y + ln x) > exp 0"
- by (simp add: mult_ac)
+ by (simp add: ac_simps)
then have "y ^ k * x > 1"
unfolding exp_zero exp_add exp_real_of_nat_mult exp_ln [OF xp] exp_ln [OF yp]
by simp
@@ -724,7 +724,7 @@
from f0 have if0: "inverse f $ 0 \<noteq> 0" by simp
from inverse_mult_eq_1[OF f0] inverse_mult_eq_1[OF if0]
have "inverse f * f = inverse f * inverse (inverse f)"
- by (simp add: mult_ac)
+ by (simp add: ac_simps)
then show ?thesis
using f0 unfolding mult_cancel_left by simp
qed
@@ -736,7 +736,7 @@
proof -
from inverse_mult_eq_1[OF f0] fg
have th0: "inverse f * f = g * f"
- by (simp add: mult_ac)
+ by (simp add: ac_simps)
then show ?thesis
using f0
unfolding mult_cancel_right
@@ -1400,7 +1400,7 @@
using fps_divide_X_minus1_setsum_lemma[of a, symmetric] th0
by (simp add: fps_divide_def mult.assoc)
also have "\<dots> = (inverse ?X * ?X) * Abs_fps (\<lambda>n::nat. setsum (op $ a) {0..n}) "
- by (simp add: mult_ac)
+ by (simp add: ac_simps)
finally show ?thesis
by (simp add: inverse_mult_eq_1[OF th0])
qed
@@ -2074,7 +2074,7 @@
apply (rule eq_divide_imp')
using r00
apply (simp del: of_nat_Suc)
- apply (simp add: mult_ac)
+ apply (simp add: ac_simps)
done
then have "a$n = ?r $n"
apply (simp del: of_nat_Suc)
@@ -2128,7 +2128,7 @@
have "fps_deriv (?r ^ Suc k) = fps_deriv a"
by simp
then have "fps_deriv ?r * ?w = fps_deriv a"
- by (simp add: fps_deriv_power mult_ac del: power_Suc)
+ by (simp add: fps_deriv_power ac_simps del: power_Suc)
then have "?iw * fps_deriv ?r * ?w = ?iw * fps_deriv a"
by simp
then have "fps_deriv ?r * (?iw * ?w) = fps_deriv a / ?w"
@@ -2294,7 +2294,7 @@
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}" .
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}"
- unfolding fps_mult_nth by (simp add: mult_ac)
+ unfolding fps_mult_nth by (simp add: ac_simps)
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}"
unfolding fps_deriv_nth fps_compose_nth setsum_right_distrib mult.assoc
apply (rule setsum.cong)
@@ -3532,7 +3532,7 @@
apply (subst minus_divide_left)
apply (subst eq_divide_iff)
apply (simp del: of_nat_add of_nat_Suc)
- apply (simp only: mult_ac)
+ apply (simp only: ac_simps)
done
lemma eq_fps_cos:
@@ -3550,7 +3550,7 @@
apply (subst minus_divide_left)
apply (subst eq_divide_iff)
apply (simp del: of_nat_add of_nat_Suc)
- apply (simp only: mult_ac)
+ apply (simp only: ac_simps)
done
lemma mult_nth_0 [simp]: "(a * b) $ 0 = a $ 0 * b $ 0"
@@ -3655,7 +3655,7 @@
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)"
unfolding Eii_sin_cos[symmetric] E_power_mult
- by (simp add: mult_ac)
+ by (simp add: ac_simps)
subsection {* Hypergeometric series *}
--- a/src/HOL/Library/Fraction_Field.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Library/Fraction_Field.thy Sat Jul 05 11:01:53 2014 +0200
@@ -31,11 +31,11 @@
fix a b a' b' a'' b'' :: 'a
assume A: "((a, b), (a', b')) \<in> fractrel"
assume B: "((a', b'), (a'', b'')) \<in> fractrel"
- have "b' * (a * b'') = b'' * (a * b')" by (simp add: mult_ac)
+ have "b' * (a * b'') = b'' * (a * b')" by (simp add: ac_simps)
also from A have "a * b' = a' * b" by auto
- also have "b'' * (a' * b) = b * (a' * b'')" by (simp add: mult_ac)
+ also have "b'' * (a' * b) = b * (a' * b'')" by (simp add: ac_simps)
also from B have "a' * b'' = a'' * b'" by auto
- also have "b * (a'' * b') = b' * (a'' * b)" by (simp add: mult_ac)
+ also have "b * (a'' * b') = b' * (a'' * b)" by (simp add: ac_simps)
finally have "b' * (a * b'') = b' * (a'' * b)" .
moreover from B have "b' \<noteq> 0" by auto
ultimately have "a * b'' = a'' * b" by simp
@@ -288,7 +288,7 @@
((a * d) * (b * d) * (x * x) \<le> (c * b) * (b * d) * (x * x))"
by (simp add: mult_le_cancel_right)
also have "... = ?le (a * x) (b * x) c d"
- by (simp add: mult_ac)
+ by (simp add: ac_simps)
finally show ?thesis .
qed
} note le_factor = this
@@ -299,11 +299,11 @@
then have "?le a b c d = ?le (a * ?D') (b * ?D') c d"
by (rule le_factor)
also have "... = ((a * b') * ?D * ?D' * d * d' \<le> (c * d') * ?D * ?D' * b * b')"
- by (simp add: mult_ac)
+ by (simp add: ac_simps)
also have "... = ((a' * b) * ?D * ?D' * d * d' \<le> (c' * d) * ?D * ?D' * b * b')"
by (simp only: eq1 eq2)
also have "... = ?le (a' * ?D) (b' * ?D) c' d'"
- by (simp add: mult_ac)
+ by (simp add: ac_simps)
also from D have "... = ?le a' b' c' d'"
by (rule le_factor [symmetric])
finally show "?le a b c d = ?le a' b' c' d'" .
@@ -328,7 +328,7 @@
assumes "b \<noteq> 0"
and "d \<noteq> 0"
shows "Fract a b < Fract c d \<longleftrightarrow> (a * d) * (b * d) < (c * b) * (b * d)"
- by (simp add: less_fract_def less_le_not_le mult_ac assms)
+ by (simp add: less_fract_def less_le_not_le ac_simps assms)
instance
proof
@@ -351,7 +351,7 @@
with ff show ?thesis by (simp add: mult_le_cancel_right)
qed
also have "... = (c * f) * (d * f) * (b * b)"
- by (simp only: mult_ac)
+ by (simp only: ac_simps)
also have "... \<le> (e * d) * (d * f) * (b * b)"
proof -
from neq 2 have "(c * f) * (d * f) \<le> (e * d) * (d * f)"
@@ -359,7 +359,7 @@
with bb show ?thesis by (simp add: mult_le_cancel_right)
qed
finally have "(a * f) * (b * f) * (d * d) \<le> e * b * (b * f) * (d * d)"
- by (simp only: mult_ac)
+ by (simp only: ac_simps)
with dd have "(a * f) * (b * f) \<le> (e * b) * (b * f)"
by (simp add: mult_le_cancel_right)
with neq show ?thesis by simp
@@ -382,7 +382,7 @@
proof -
from neq 2 have "(c * b) * (d * b) \<le> (a * d) * (d * b)"
by simp
- then show ?thesis by (simp only: mult_ac)
+ then show ?thesis by (simp only: ac_simps)
qed
finally have "(a * d) * (b * d) = (c * b) * (b * d)" .
moreover from neq have "b * d \<noteq> 0" by simp
@@ -469,7 +469,7 @@
ultimately have "(a * d) * (b * d) * ?E * ?F < (c * b) * (b * d) * ?E * ?F"
by (simp add: mult_less_cancel_right)
with neq show ?thesis
- by (simp add: mult_ac)
+ by (simp add: ac_simps)
qed
qed
qed
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Sat Jul 05 11:01:53 2014 +0200
@@ -732,7 +732,7 @@
{
fix w
have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w / ?a0) < 1"
- using qr[rule_format, of w] a00 by (simp add: divide_inverse mult_ac)
+ using qr[rule_format, of w] a00 by (simp add: divide_inverse ac_simps)
also have "\<dots> \<longleftrightarrow> cmod (poly q w) < cmod ?a0"
using a00 unfolding norm_divide by (simp add: field_simps)
finally have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w) < cmod ?a0" .
@@ -980,7 +980,7 @@
have "p = [:- a, 1:] ^ (Suc ?op) * u"
apply (subst s)
apply (subst u)
- apply (simp only: power_Suc mult_ac)
+ apply (simp only: power_Suc ac_simps)
done
with ap(2)[unfolded dvd_def] have False
by blast
@@ -1010,7 +1010,7 @@
apply (subst mult.assoc [where a=u])
apply (subst mult.assoc [where b=u, symmetric])
apply (subst u [symmetric])
- apply (simp add: mult_ac power_add [symmetric])
+ apply (simp add: ac_simps power_add [symmetric])
done
then have ?ths
unfolding dvd_def by blast
--- a/src/HOL/Library/Inner_Product.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Library/Inner_Product.thy Sat Jul 05 11:01:53 2014 +0200
@@ -280,7 +280,7 @@
\<Longrightarrow> GDERIV (\<lambda>x. g (f x)) x :> scaleR dg df"
unfolding gderiv_def has_field_derivative_def
apply (drule (1) has_derivative_compose)
- apply (simp add: mult_ac)
+ apply (simp add: ac_simps)
done
lemma has_derivative_subst: "\<lbrakk>FDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> FDERIV f x :> d"
@@ -313,7 +313,7 @@
unfolding gderiv_def has_field_derivative_def inner_add_right inner_scaleR_right
apply (rule has_derivative_subst)
apply (erule (1) has_derivative_scaleR)
- apply (simp add: mult_ac)
+ apply (simp add: ac_simps)
done
lemma GDERIV_mult:
@@ -322,7 +322,7 @@
unfolding gderiv_def
apply (rule has_derivative_subst)
apply (erule (1) has_derivative_mult)
- apply (simp add: inner_add mult_ac)
+ apply (simp add: inner_add ac_simps)
done
lemma GDERIV_inverse:
--- a/src/HOL/Library/Multiset.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Library/Multiset.thy Sat Jul 05 11:01:53 2014 +0200
@@ -717,7 +717,7 @@
by (blast dest: multi_member_split)
have "A + {#b#} = A + {#b#} + {#c#} - {#c#}" by simp
then have "A + {#b#} = A + {#c#} + {#b#} - {#c#}"
- by (simp add: add_ac)
+ by (simp add: ac_simps)
then show ?thesis using B by simp
qed
@@ -817,7 +817,7 @@
next
case (add M x)
have "M + {#x#} + N = (M + N) + {#x#}"
- by (simp add: add_ac)
+ by (simp add: ac_simps)
with add show ?case by (simp add: fold_mset_insert fold_mset_fun_left_comm)
qed
@@ -851,7 +851,7 @@
lemma comp_fun_commute_mset_image:
"comp_fun_commute (plus o single o f)"
proof
-qed (simp add: add_ac fun_eq_iff)
+qed (simp add: ac_simps fun_eq_iff)
lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
by (simp add: image_mset_def)
@@ -868,7 +868,7 @@
proof -
interpret comp_fun_commute "plus o single o f"
by (fact comp_fun_commute_mset_image)
- show ?thesis by (induct N) (simp_all add: image_mset_def add_ac)
+ show ?thesis by (induct N) (simp_all add: image_mset_def ac_simps)
qed
corollary image_mset_insert:
@@ -956,7 +956,7 @@
lemma multiset_of_append [simp]:
"multiset_of (xs @ ys) = multiset_of xs + multiset_of ys"
- by (induct xs arbitrary: ys) (auto simp: add_ac)
+ by (induct xs arbitrary: ys) (auto simp: ac_simps)
lemma multiset_of_filter:
"multiset_of (filter P xs) = {#x :# multiset_of xs. P x #}"
@@ -1008,7 +1008,7 @@
lemma multiset_of_compl_union [simp]:
"multiset_of [x\<leftarrow>xs. P x] + multiset_of [x\<leftarrow>xs. \<not>P x] = multiset_of xs"
- by (induct xs) (auto simp: add_ac)
+ by (induct xs) (auto simp: ac_simps)
lemma count_multiset_of_length_filter:
"count (multiset_of xs) x = length (filter (\<lambda>y. x = y) xs)"
@@ -1552,7 +1552,7 @@
next
fix K'
assume "M0' = K' + {#a#}"
- with N have n: "N = K' + K + {#a#}" by (simp add: add_ac)
+ with N have n: "N = K' + K + {#a#}" by (simp add: ac_simps)
assume "M0 = K' + {#a'#}"
with r have "?R (K' + K) M0" by blast
@@ -1701,7 +1701,7 @@
apply (simp add: mult1_def set_of_def)
apply (rule_tac x = a in exI)
apply (rule_tac x = "I + J'" in exI)
-apply (simp add: add_ac)
+apply (simp add: ac_simps)
done
lemma one_step_implies_mult:
@@ -1840,14 +1840,14 @@
"{#x#} + X = A + ({#y#}+Z)
\<and> {#y#} + Y = B + ({#y#}+Z)
\<and> ((set_of A, set_of B) \<in> max_strict \<or> (B = {#} \<and> A = {#}))"
- by (auto simp: add_ac)
+ by (auto simp: ac_simps)
thus ?case by (intro exI)
next
assume A: "(x, y) \<in> pair_less"
let ?A' = "{#x#} + A" and ?B' = "{#y#} + B"
have "{#x#} + X = ?A' + Z"
"{#y#} + Y = ?B' + Z"
- by (auto simp add: add_ac)
+ by (auto simp add: ac_simps)
moreover have
"(set_of ?A', set_of ?B') \<in> max_strict"
using 1 A unfolding max_strict_def
@@ -1880,12 +1880,12 @@
assume [simp]: "A' = {#} \<and> B' = {#}"
show ?thesis by (rule smsI) (auto intro: max)
qed
- thus "(Z + A, Z' + B) \<in> ms_strict" by (simp add:add_ac)
+ thus "(Z + A, Z' + B) \<in> ms_strict" by (simp add:ac_simps)
thus "(Z + A, Z' + B) \<in> ms_weak" by (simp add: ms_weak_def)
}
from mx_or_empty
have "(Z'' + A', Z'' + B') \<in> ms_weak" by (rule wmsI)
- thus "(Z + {#}, Z' + {#}) \<in> ms_weak" by (simp add:add_ac)
+ thus "(Z + {#}, Z' + {#}) \<in> ms_weak" by (simp add:ac_simps)
qed
lemma empty_neutral: "{#} + x = x" "x + {#} = x"
@@ -1914,7 +1914,7 @@
val regroup_munion_conv =
Function_Lib.regroup_conv @{const_abbrev Mempty} @{const_name plus}
- (map (fn t => t RS eq_reflection) (@{thms add_ac} @ @{thms empty_neutral}))
+ (map (fn t => t RS eq_reflection) (@{thms ac_simps} @ @{thms empty_neutral}))
fun unfold_pwleq_tac i =
(rtac @{thm pw_leq_step} i THEN (fn st => unfold_pwleq_tac (i + 1) st))
--- a/src/HOL/Library/Numeral_Type.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Library/Numeral_Type.thy Sat Jul 05 11:01:53 2014 +0200
@@ -147,7 +147,7 @@
lemma of_nat_eq: "of_nat k = Abs (int k mod n)"
apply (induct k)
apply (simp add: zero_def)
-apply (simp add: Rep_simps add_def one_def zmod_simps add_ac)
+apply (simp add: Rep_simps add_def one_def zmod_simps ac_simps)
done
lemma of_int_eq: "of_int z = Abs (z mod n)"
--- a/src/HOL/Library/RBT_Set.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Library/RBT_Set.thy Sat Jul 05 11:01:53 2014 +0200
@@ -657,7 +657,7 @@
lemma setsum_Set [code]:
"setsum f (Set xs) = fold_keys (plus o f) xs 0"
proof -
- have "comp_fun_commute (\<lambda>x. op + (f x))" by default (auto simp: add_ac)
+ have "comp_fun_commute (\<lambda>x. op + (f x))" by default (auto simp: ac_simps)
then show ?thesis
by (auto simp add: setsum.eq_fold finite_fold_fold_keys o_def)
qed
--- a/src/HOL/Library/Set_Algebras.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Library/Set_Algebras.thy Sat Jul 05 11:01:53 2014 +0200
@@ -100,11 +100,11 @@
lemma set_plus_rearrange:
"((a::'a::comm_monoid_add) +o C) + (b +o D) = (a + b) +o (C + D)"
- apply (auto simp add: elt_set_plus_def set_plus_def add_ac)
+ apply (auto simp add: elt_set_plus_def set_plus_def ac_simps)
apply (rule_tac x = "ba + bb" in exI)
- apply (auto simp add: add_ac)
+ apply (auto simp add: ac_simps)
apply (rule_tac x = "aa + a" in exI)
- apply (auto simp add: add_ac)
+ apply (auto simp add: ac_simps)
done
lemma set_plus_rearrange2: "(a::'a::semigroup_add) +o (b +o C) = (a + b) +o C"
@@ -112,19 +112,19 @@
lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) + C = a +o (B + C)"
apply (auto simp add: elt_set_plus_def set_plus_def)
- apply (blast intro: add_ac)
+ apply (blast intro: ac_simps)
apply (rule_tac x = "a + aa" in exI)
apply (rule conjI)
apply (rule_tac x = "aa" in bexI)
apply auto
apply (rule_tac x = "ba" in bexI)
- apply (auto simp add: add_ac)
+ apply (auto simp add: ac_simps)
done
theorem set_plus_rearrange4: "C + ((a::'a::comm_monoid_add) +o D) = a +o (C + D)"
- apply (auto simp add: elt_set_plus_def set_plus_def add_ac)
+ apply (auto simp add: elt_set_plus_def set_plus_def ac_simps)
apply (rule_tac x = "aa + ba" in exI)
- apply (auto simp add: add_ac)
+ apply (auto simp add: ac_simps)
done
theorems set_plus_rearranges = set_plus_rearrange set_plus_rearrange2
@@ -140,7 +140,7 @@
by (auto simp add: elt_set_plus_def set_plus_def)
lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) \<in> C \<Longrightarrow> a +o D \<subseteq> D + C"
- by (auto simp add: elt_set_plus_def set_plus_def add_ac)
+ by (auto simp add: elt_set_plus_def set_plus_def ac_simps)
lemma set_plus_mono5: "a \<in> C \<Longrightarrow> B \<subseteq> D \<Longrightarrow> a +o B \<subseteq> C + D"
apply (subgoal_tac "a +o B \<subseteq> a +o D")
@@ -178,17 +178,17 @@
apply (auto simp add: set_plus_def)
apply (rule_tac x = 0 in bexI)
apply (rule_tac x = x in bexI)
- apply (auto simp add: add_ac)
+ apply (auto simp add: ac_simps)
done
lemma set_plus_imp_minus: "(a::'a::ab_group_add) : b +o C \<Longrightarrow> (a - b) \<in> C"
- by (auto simp add: elt_set_plus_def add_ac)
+ by (auto simp add: elt_set_plus_def ac_simps)
lemma set_minus_imp_plus: "(a::'a::ab_group_add) - b : C \<Longrightarrow> a \<in> b +o C"
- apply (auto simp add: elt_set_plus_def add_ac)
+ apply (auto simp add: elt_set_plus_def ac_simps)
apply (subgoal_tac "a = (a + - b) + b")
apply (rule bexI, assumption)
- apply (auto simp add: add_ac)
+ apply (auto simp add: ac_simps)
done
lemma set_minus_plus: "(a::'a::ab_group_add) - b \<in> C \<longleftrightarrow> a \<in> b +o C"
@@ -209,9 +209,9 @@
"((a::'a::comm_monoid_mult) *o C) * (b *o D) = (a * b) *o (C * D)"
apply (auto simp add: elt_set_times_def set_times_def)
apply (rule_tac x = "ba * bb" in exI)
- apply (auto simp add: mult_ac)
+ apply (auto simp add: ac_simps)
apply (rule_tac x = "aa * a" in exI)
- apply (auto simp add: mult_ac)
+ apply (auto simp add: ac_simps)
done
lemma set_times_rearrange2:
@@ -221,20 +221,20 @@
lemma set_times_rearrange3:
"((a::'a::semigroup_mult) *o B) * C = a *o (B * C)"
apply (auto simp add: elt_set_times_def set_times_def)
- apply (blast intro: mult_ac)
+ apply (blast intro: ac_simps)
apply (rule_tac x = "a * aa" in exI)
apply (rule conjI)
apply (rule_tac x = "aa" in bexI)
apply auto
apply (rule_tac x = "ba" in bexI)
- apply (auto simp add: mult_ac)
+ apply (auto simp add: ac_simps)
done
theorem set_times_rearrange4:
"C * ((a::'a::comm_monoid_mult) *o D) = a *o (C * D)"
- apply (auto simp add: elt_set_times_def set_times_def mult_ac)
+ apply (auto simp add: elt_set_times_def set_times_def ac_simps)
apply (rule_tac x = "aa * ba" in exI)
- apply (auto simp add: mult_ac)
+ apply (auto simp add: ac_simps)
done
theorems set_times_rearranges = set_times_rearrange set_times_rearrange2
@@ -250,7 +250,7 @@
by (auto simp add: elt_set_times_def set_times_def)
lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C \<Longrightarrow> a *o D \<subseteq> D * C"
- by (auto simp add: elt_set_times_def set_times_def mult_ac)
+ by (auto simp add: elt_set_times_def set_times_def ac_simps)
lemma set_times_mono5: "a \<in> C \<Longrightarrow> B \<subseteq> D \<Longrightarrow> a *o B \<subseteq> C * D"
apply (subgoal_tac "a *o B \<subseteq> a *o D")
--- a/src/HOL/List.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/List.thy Sat Jul 05 11:01:53 2014 +0200
@@ -2104,13 +2104,13 @@
by (simp add: butlast_conv_take min.absorb1 min.absorb2)
lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)"
-by (simp add: butlast_conv_take drop_take add_ac)
+by (simp add: butlast_conv_take drop_take ac_simps)
lemma take_butlast: "n < length xs ==> take n (butlast xs) = take n xs"
by (simp add: butlast_conv_take min.absorb1)
lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)"
-by (simp add: butlast_conv_take drop_take add_ac)
+by (simp add: butlast_conv_take drop_take ac_simps)
lemma hd_drop_conv_nth: "n < length xs \<Longrightarrow> hd(drop n xs) = xs!n"
by(simp add: hd_conv_nth)
@@ -3471,7 +3471,7 @@
lemma (in comm_monoid_add) listsum_rev [simp]:
"listsum (rev xs) = listsum xs"
- by (simp add: listsum_def foldr_fold fold_rev fun_eq_iff add_ac)
+ by (simp add: listsum_def foldr_fold fold_rev fun_eq_iff ac_simps)
lemma (in monoid_add) fold_plus_listsum_rev:
"fold plus xs = plus (listsum (rev xs))"
--- a/src/HOL/MacLaurin.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/MacLaurin.thy Sat Jul 05 11:01:53 2014 +0200
@@ -574,7 +574,7 @@
apply (rule setsum.cong[OF refl])
apply (subst diff_m_0, simp)
apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono
- simp add: est mult_ac divide_inverse power_abs [symmetric] abs_mult)
+ simp add: est ac_simps divide_inverse power_abs [symmetric] abs_mult)
done
qed
--- a/src/HOL/Metis_Examples/Big_O.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Metis_Examples/Big_O.thy Sat Jul 05 11:01:53 2014 +0200
@@ -301,7 +301,7 @@
lemma bigo_mult [intro]: "O(f) * O(g) <= O(f * g)"
apply (rule subsetI)
apply (subst bigo_def)
-apply (auto simp del: abs_mult mult_ac
+apply (auto simp del: abs_mult ac_simps
simp add: bigo_alt_def set_times_def func_times)
(* sledgehammer *)
apply (rule_tac x = "c * ca" in exI)
@@ -334,7 +334,7 @@
by (rule bigo_mult2)
also have "(\<lambda>x. 1 / f x) * (f * g) = g"
apply (simp add: func_times)
- by (metis (lifting, no_types) a ext mult_ac(2) nonzero_divide_eq_eq)
+ by (metis (lifting, no_types) a ext mult.commute nonzero_divide_eq_eq)
finally have "(\<lambda>x. (1\<Colon>'b) / f x) * h : O(g)".
then have "f * ((\<lambda>x. (1\<Colon>'b) / f x) * h) : f *o O(g)"
by auto
@@ -396,7 +396,7 @@
by (metis bigo_add_commute_imp)
lemma bigo_const1: "(\<lambda>x. c) : O(\<lambda>x. 1)"
-by (auto simp add: bigo_def mult_ac)
+by (auto simp add: bigo_def ac_simps)
lemma bigo_const2 [intro]: "O(\<lambda>x. c) \<le> O(\<lambda>x. 1)"
by (metis bigo_const1 bigo_elt_subset)
@@ -462,13 +462,13 @@
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>)"
by (metis comm_mult_left_mono)
thus "\<exists>ca\<Colon>'a. \<forall>x\<Colon>'b. \<bar>inverse c\<bar> * \<bar>g x\<bar> \<le> ca * \<bar>f x\<bar>"
- using A2 F4 by (metis ab_semigroup_mult_class.mult_ac(1) comm_mult_left_mono)
+ using A2 F4 by (metis mult.assoc comm_mult_left_mono)
qed
lemma bigo_const_mult6 [intro]: "(\<lambda>x. c) *o O(f) <= O(f)"
apply (auto intro!: subsetI
simp add: bigo_def elt_set_times_def func_times
- simp del: abs_mult mult_ac)
+ simp del: abs_mult ac_simps)
(* sledgehammer *)
apply (rule_tac x = "ca * (abs c)" in exI)
apply (rule allI)
@@ -478,7 +478,7 @@
apply (rule mult_left_mono)
apply (erule spec)
apply simp
- apply (simp add: mult_ac)
+ apply (simp add: ac_simps)
done
lemma bigo_const_mult7 [intro]: "f =o O(g) \<Longrightarrow> (\<lambda>x. c * f x) =o O(g)"
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Sat Jul 05 11:01:53 2014 +0200
@@ -418,7 +418,7 @@
by (simp add: matrix_vector_mult_def inner_vec_def)
lemma dot_lmul_matrix: "((x::real ^_) v* A) \<bullet> y = x \<bullet> (A *v y)"
- apply (simp add: inner_vec_def matrix_vector_mult_def vector_matrix_mult_def setsum_left_distrib setsum_right_distrib mult_ac)
+ apply (simp add: inner_vec_def matrix_vector_mult_def vector_matrix_mult_def setsum_left_distrib setsum_right_distrib ac_simps)
apply (subst setsum.commute)
apply simp
done
@@ -525,7 +525,7 @@
apply (simp add: transpose_def inner_vec_def matrix_vector_mult_def
setsum_left_distrib setsum_right_distrib)
apply (subst setsum.commute)
- apply (auto simp add: mult_ac)
+ apply (auto simp add: ac_simps)
done
lemma matrix_adjoint: assumes lf: "linear (f :: real^'n \<Rightarrow> real ^'m)"
@@ -1221,7 +1221,7 @@
unfolding UNIV_2 by simp
lemma setsum_3: "setsum f (UNIV::3 set) = f 1 + f 2 + f 3"
- unfolding UNIV_3 by (simp add: add_ac)
+ unfolding UNIV_3 by (simp add: ac_simps)
instantiation num1 :: cart_one
begin
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Sat Jul 05 11:01:53 2014 +0200
@@ -1019,7 +1019,7 @@
(of_nat (Suc n) * (f (Suc n) u * (z-u) ^ n)) +
(f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)) -
(f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n))"
- by (simp only: fact_Suc of_nat_mult mult_ac) simp
+ by (simp only: fact_Suc of_nat_mult ac_simps) simp
also have "... = f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)"
by (simp add: algebra_simps)
finally show ?thesis
@@ -1116,7 +1116,7 @@
(\<Sum>i = 0..n.
f (Suc (Suc i)) u * ((z-u) ^ Suc i) / of_nat (fact (Suc i)) -
f (Suc i) u * (z-u) ^ i / of_nat (fact i))"
- by (simp only: diff_divide_distrib fact_cancel mult_ac)
+ by (simp only: diff_divide_distrib fact_cancel ac_simps)
also have "... = f (Suc 0) u -
(f (Suc (Suc n)) u * (z-u) ^ Suc n - of_nat (Suc n) * (z-u) ^ n * f (Suc n) u) /
of_nat (fact (Suc n)) +
@@ -1132,7 +1132,7 @@
apply (intro derivative_eq_intros)+
apply (force intro: u assms)
apply (rule refl)+
- apply (auto simp: mult_ac)
+ apply (auto simp: ac_simps)
done
}
then show ?thesis
--- a/src/HOL/Multivariate_Analysis/Determinants.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy Sat Jul 05 11:01:53 2014 +0200
@@ -476,7 +476,7 @@
also have "\<dots> = (c*s a k) $ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk"
by (simp add: field_simps)
also have "\<dots> = c* (a k $ p k * setprod (\<lambda>i. ?g i $ p i) ?Uk)"
- unfolding th1 by (simp add: mult_ac)
+ unfolding th1 by (simp add: ac_simps)
also have "\<dots> = c* (setprod (\<lambda>i. ?g i $ p i) (insert k ?Uk))"
unfolding setprod.insert[OF th3] by simp
finally have "setprod (\<lambda>i. ?f i $ p i) ?U = c* (setprod (\<lambda>i. ?g i $ p i) ?U)"
@@ -824,7 +824,7 @@
by (simp_all add: sign_idempotent)
have ths: "?s q = ?s p * ?s (q \<circ> inv p)"
using pp pq permutation_inverse[OF pp] sign_inverse[OF pp]
- by (simp add: th00 mult_ac sign_idempotent sign_compose)
+ by (simp add: th00 ac_simps sign_idempotent sign_compose)
have th001: "setprod (\<lambda>i. B$i$ q (inv p i)) ?U = setprod ((\<lambda>i. B$i$ q (inv p i)) \<circ> p) ?U"
by (rule setprod_permute[OF p])
have thp: "setprod (\<lambda>i. (\<chi> i. A$i$p i *s B$p i :: 'a^'n^'n) $i $ q i) ?U =
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Sat Jul 05 11:01:53 2014 +0200
@@ -1578,7 +1578,7 @@
have "\<exists>B. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
using `bilinear h` by (rule bilinear_bounded)
then show "\<exists>K. \<forall>x y. norm (h x y) \<le> norm x * norm y * K"
- by (simp add: mult_ac)
+ by (simp add: ac_simps)
qed
next
assume "bounded_bilinear h"
@@ -1597,7 +1597,7 @@
using bh [unfolded bilinear_conv_bounded_bilinear]
by (rule bounded_bilinear.pos_bounded)
then show ?thesis
- by (simp only: mult_ac)
+ by (simp only: ac_simps)
qed
--- a/src/HOL/Multivariate_Analysis/PolyRoots.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/PolyRoots.thy Sat Jul 05 11:01:53 2014 +0200
@@ -41,9 +41,9 @@
shows "(1 - x) * (\<Sum>i=m..n. x^i) = x^m - x^Suc n"
proof -
have "(1 - x) * (\<Sum>i=m..n. x^i) = x^m * (1 - x) * (\<Sum>i\<le>n-m. x^i)"
- by (metis ab_semigroup_mult_class.mult_ac(1) assms mult.commute setsum_power_shift)
+ by (metis mult.assoc mult.commute assms setsum_power_shift)
also have "... =x^m * (1 - x^Suc(n-m))"
- by (metis ab_semigroup_mult_class.mult_ac(1) setsum_gp_basic)
+ by (metis mult.assoc setsum_gp_basic)
also have "... = x^m - x^Suc n"
using assms
by (simp add: algebra_simps) (metis le_add_diff_inverse power_add)
@@ -78,9 +78,9 @@
(\<Sum>i\<le>n. a i * (x^i - y^i))"
by (simp add: algebra_simps setsum_subtractf [symmetric])
also have "... = (\<Sum>i\<le>n. a i * (x - y) * (\<Sum>j<i. y^(i - Suc j) * x^j))"
- by (simp add: power_diff_sumr2 mult_ac)
+ by (simp add: power_diff_sumr2 ac_simps)
also have "... = (x - y) * (\<Sum>i\<le>n. (\<Sum>j<i. a i * y^(i - Suc j) * x^j))"
- by (simp add: setsum_right_distrib mult_ac)
+ by (simp add: setsum_right_distrib ac_simps)
also have "... = (x - y) * (\<Sum>j<n. (\<Sum>i=Suc j..n. a i * y^(i - Suc j) * x^j))"
by (simp add: nested_setsum_swap')
finally show ?thesis .
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sat Jul 05 11:01:53 2014 +0200
@@ -2844,7 +2844,7 @@
from assms(1) obtain b where b: "b > 0" "\<forall>x\<in>S. norm x \<le> b"
unfolding bounded_pos by auto
from assms(2) obtain B where B: "B > 0" "\<forall>x. norm (f x) \<le> B * norm x"
- using bounded_linear.pos_bounded by (auto simp add: mult_ac)
+ using bounded_linear.pos_bounded by (auto simp add: ac_simps)
{
fix x
assume "x \<in> S"
--- a/src/HOL/NSA/CLim.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/NSA/CLim.thy Sat Jul 05 11:01:53 2014 +0200
@@ -142,7 +142,7 @@
apply (drule_tac [2] DERIV_ident [THEN DERIV_mult])
apply (auto simp add: distrib_right real_of_nat_Suc)
apply (case_tac "n")
-apply (auto simp add: mult_ac add.commute)
+apply (auto simp add: ac_simps add.commute)
done
text{*Nonstandard version*}
--- a/src/HOL/NSA/HDeriv.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/NSA/HDeriv.thy Sat Jul 05 11:01:53 2014 +0200
@@ -171,7 +171,7 @@
apply (auto simp add: NSDERIV_NSLIM_iff NSLIM_def)
apply (auto simp add: add_divide_distrib diff_divide_distrib dest!: spec)
apply (drule_tac b = "star_of Da" and d = "star_of Db" in approx_add)
-apply (auto simp add: add_ac algebra_simps)
+apply (auto simp add: ac_simps algebra_simps)
done
text{*Product of functions - Proof is trivial but tedious
@@ -180,7 +180,7 @@
lemma lemma_nsderiv1:
fixes a b c d :: "'a::comm_ring star"
shows "(a*b) - (c*d) = (b*(a - c)) + (c*(b - d))"
-by (simp add: right_diff_distrib mult_ac)
+by (simp add: right_diff_distrib ac_simps)
lemma lemma_nsderiv2:
fixes x y z :: "'a::real_normed_field star"
--- a/src/HOL/NSA/HTranscendental.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/NSA/HTranscendental.thy Sat Jul 05 11:01:53 2014 +0200
@@ -527,7 +527,7 @@
pi_divide_HNatInfinite_not_zero])
apply (auto)
apply (rule approx_SReal_mult_cancel [of "inverse (hypreal_of_real pi)"])
-apply (auto intro: Reals_inverse simp add: divide_inverse mult_ac)
+apply (auto intro: Reals_inverse simp add: divide_inverse ac_simps)
done
lemma STAR_sin_pi_divide_HNatInfinite_approx_pi2:
--- a/src/HOL/NSA/NSA.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/NSA/NSA.thy Sat Jul 05 11:01:53 2014 +0200
@@ -776,7 +776,7 @@
lemma approx_add_left_cancel: "d + b @= d + c ==> b @= c"
apply (drule approx_minus_iff [THEN iffD1])
-apply (simp add: approx_minus_iff [symmetric] add_ac)
+apply (simp add: approx_minus_iff [symmetric] ac_simps)
done
lemma approx_add_right_cancel: "b + d @= c + d ==> b @= c"
@@ -786,7 +786,7 @@
lemma approx_add_mono1: "b @= c ==> d + b @= d + c"
apply (rule approx_minus_iff [THEN iffD2])
-apply (simp add: approx_minus_iff [symmetric] add_ac)
+apply (simp add: approx_minus_iff [symmetric] ac_simps)
done
lemma approx_add_mono2: "b @= c ==> b + a @= c + a"
@@ -1714,25 +1714,25 @@
lemma Infinitesimal_sum_square_cancel2 [simp]:
"(y::hypreal)*y + x*x + z*z \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
apply (rule Infinitesimal_sum_square_cancel)
-apply (simp add: add_ac)
+apply (simp add: ac_simps)
done
lemma HFinite_sum_square_cancel2 [simp]:
"(y::hypreal)*y + x*x + z*z \<in> HFinite ==> x*x \<in> HFinite"
apply (rule HFinite_sum_square_cancel)
-apply (simp add: add_ac)
+apply (simp add: ac_simps)
done
lemma Infinitesimal_sum_square_cancel3 [simp]:
"(z::hypreal)*z + y*y + x*x \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
apply (rule Infinitesimal_sum_square_cancel)
-apply (simp add: add_ac)
+apply (simp add: ac_simps)
done
lemma HFinite_sum_square_cancel3 [simp]:
"(z::hypreal)*z + y*y + x*x \<in> HFinite ==> x*x \<in> HFinite"
apply (rule HFinite_sum_square_cancel)
-apply (simp add: add_ac)
+apply (simp add: ac_simps)
done
lemma monad_hrabs_less:
--- a/src/HOL/Nat.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Nat.thy Sat Jul 05 11:01:53 2014 +0200
@@ -1075,10 +1075,10 @@
lemma add_leE: "(m::nat) + k \<le> n ==> (m \<le> n ==> k \<le> n ==> R) ==> R"
by (blast dest: add_leD1 add_leD2)
-text {* needs @{text "!!k"} for @{text add_ac} to work *}
+text {* needs @{text "!!k"} for @{text ac_simps} to work *}
lemma less_add_eq_less: "!!k::nat. k < l ==> m + l = k + n ==> m < n"
by (force simp del: add_Suc_right
- simp add: less_iff_Suc_add add_Suc_right [symmetric] add_ac)
+ simp add: less_iff_Suc_add add_Suc_right [symmetric] ac_simps)
subsubsection {* More results about difference *}
@@ -1405,10 +1405,10 @@
by (simp add: of_nat_def)
lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n"
- by (induct m) (simp_all add: add_ac)
+ by (induct m) (simp_all add: ac_simps)
lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n"
- by (induct m) (simp_all add: add_ac distrib_right)
+ by (induct m) (simp_all add: ac_simps distrib_right)
primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
"of_nat_aux inc 0 i = i"
@@ -1869,7 +1869,7 @@
lemma dvd_mult_cancel: "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n"
unfolding dvd_def
apply (erule exE)
- apply (simp add: mult_ac)
+ apply (simp add: ac_simps)
done
lemma dvd_mult_cancel1: "0<m ==> (m*n dvd m) = (n = (1::nat))"
--- a/src/HOL/NthRoot.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/NthRoot.thy Sat Jul 05 11:01:53 2014 +0200
@@ -527,7 +527,7 @@
lemma real_divide_square_eq [simp]: "(((r::real) * a) / (r * r)) = a / r"
apply (simp add: divide_inverse)
apply (case_tac "r=0")
-apply (auto simp add: mult_ac)
+apply (auto simp add: ac_simps)
done
lemma lemma_real_divide_sqrt_less: "0 < u ==> u / sqrt 2 < u"
--- a/src/HOL/Number_Theory/Binomial.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Number_Theory/Binomial.thy Sat Jul 05 11:01:53 2014 +0200
@@ -161,7 +161,7 @@
by (rule distrib)
also have "\<dots> = (\<Sum>k=0..n. of_nat (n choose k) * a^(k+1) * b^(n-k)) +
(\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k+1))"
- by (auto simp add: setsum_right_distrib mult_ac)
+ by (auto simp add: setsum_right_distrib ac_simps)
also have "\<dots> = (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n+1-k)) +
(\<Sum>k=1..n+1. of_nat (n choose (k - 1)) * a^k * b^(n+1-k))"
by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le field_simps
@@ -634,7 +634,7 @@
also have "... = fact (m+r+k) div (fact r * (fact k * fact m))"
apply (subst div_mult_div_if_dvd)
apply (auto simp: fact_fact_dvd_fact)
- apply (metis ab_semigroup_add_class.add_ac(1) add.commute fact_fact_dvd_fact)
+ apply (metis ac_simps add.commute fact_fact_dvd_fact)
done
also have "... = (fact (m+r+k) * fact (m+r)) div (fact r * (fact k * fact m) * fact (m+r))"
apply (subst div_mult_div_if_dvd [symmetric])
@@ -758,7 +758,7 @@
also have "\<dots> = - (\<Sum>i = 0..card K. -1 ^ i * int (card K choose i)) + 1"
by(subst setsum_right_distrib[symmetric]) simp
also have "\<dots> = - ((-1 + 1) ^ card K) + 1"
- by(subst binomial_ring)(simp add: mult_ac)
+ by(subst binomial_ring)(simp add: ac_simps)
also have "\<dots> = 1" using x K by(auto simp add: K_def card_gt_0_iff)
finally show "?lhs x = 1" .
qed
--- a/src/HOL/Number_Theory/MiscAlgebra.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Number_Theory/MiscAlgebra.thy Sat Jul 05 11:01:53 2014 +0200
@@ -115,7 +115,7 @@
apply (rule_tac x = "(m_inv G a) \<otimes> x" in bexI)
apply auto
(* auto should get this. I suppose we need "comm_monoid_simprules"
- for mult_ac rewriting. *)
+ for ac_simps rewriting. *)
apply (subst m_assoc [symmetric])
apply auto
done
--- a/src/HOL/Number_Theory/Pocklington.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Number_Theory/Pocklington.thy Sat Jul 05 11:01:53 2014 +0200
@@ -549,7 +549,7 @@
from n nqr have aqr0: "a ^ (q * r) \<noteq> 0" using a0 by simp
hence "(a ^ (q * r) - 1) + 1 = a ^ (q * r)" by simp
with k l have "a ^ (q * r) = p*l*k + 1" by simp
- hence "a ^ (r * q) + p * 0 = 1 + p * (l*k)" by (simp add: mult_ac)
+ hence "a ^ (r * q) + p * 0 = 1 + p * (l*k)" by (simp add: ac_simps)
hence odq: "ord p (a^r) dvd q"
unfolding ord_divides[symmetric] power_mult[symmetric]
by (metis an cong_dvd_modulus_nat mult.commute nqr pn)
--- a/src/HOL/Number_Theory/Residues.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Number_Theory/Residues.thy Sat Jul 05 11:01:53 2014 +0200
@@ -40,7 +40,7 @@
apply (insert m_gt_one)
apply (rule abelian_groupI)
apply (unfold R_def residue_ring_def)
- apply (auto simp add: mod_add_right_eq [symmetric] add_ac)
+ apply (auto simp add: mod_add_right_eq [symmetric] ac_simps)
apply (case_tac "x = 0")
apply force
apply (subgoal_tac "(x + (m - x)) mod m = 0")
@@ -56,7 +56,7 @@
apply (subgoal_tac "x * y mod m * z mod m = z * (x * y mod m) mod m")
apply (erule ssubst)
apply (subst mod_mult_right_eq [symmetric])+
- apply (simp_all only: mult_ac)
+ apply (simp_all only: ac_simps)
done
lemma cring: "cring R"
--- a/src/HOL/Old_Number_Theory/Chinese.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Chinese.thy Sat Jul 05 11:01:53 2014 +0200
@@ -238,7 +238,7 @@
"0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i
\<and> [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)")
prefer 6
- apply (simp add: mult_ac)
+ apply (simp add: ac_simps)
apply (unfold xilin_sol_def)
apply (tactic {* asm_simp_tac @{context} 6 *})
apply (rule_tac [6] ex1_implies_ex [THEN someI_ex])
--- a/src/HOL/Old_Number_Theory/Euler.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Euler.thy Sat Jul 05 11:01:53 2014 +0200
@@ -67,7 +67,7 @@
then have "[j * j = (a * MultInv p j) * j] (mod p)"
by (auto simp add: zcong_scalar)
then have a:"[j * j = a * (MultInv p j * j)] (mod p)"
- by (auto simp add: mult_ac)
+ by (auto simp add: ac_simps)
have "[j * j = a] (mod p)"
proof -
from assms(1,2,4) have "[MultInv p j * j = 1] (mod p)"
@@ -149,7 +149,7 @@
c = "a * (x * MultInv p x)" in zcong_trans, force)
apply (frule_tac p = p and x = x in MultInv_prop2, auto)
apply (metis StandardRes_SRStar_prop3 mult_1_right mult.commute zcong_sym zcong_zmult_prop1)
- apply (auto simp add: mult_ac)
+ apply (auto simp add: ac_simps)
done
lemma aux1: "[| 0 < x; (x::int) < a; x \<noteq> (a - 1) |] ==> x < a - 1"
--- a/src/HOL/Old_Number_Theory/EulerFermat.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Old_Number_Theory/EulerFermat.thy Sat Jul 05 11:01:53 2014 +0200
@@ -255,7 +255,7 @@
apply (subst setprod.insert)
apply (rule_tac [2] Bnor_prod_power_aux)
apply (unfold inj_on_def)
- apply (simp_all add: mult_ac Bnor_fin Bnor_mem_zle_swap)
+ apply (simp_all add: ac_simps Bnor_fin Bnor_mem_zle_swap)
done
--- a/src/HOL/Old_Number_Theory/Factorization.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Factorization.thy Sat Jul 05 11:01:53 2014 +0200
@@ -188,7 +188,7 @@
lemma perm_prod: "xs <~~> ys ==> prod xs = prod ys"
apply (induct set: perm)
- apply (simp_all add: mult_ac)
+ apply (simp_all add: ac_simps)
done
lemma perm_subst_oinsert: "xs <~~> ys ==> oinsert a xs <~~> oinsert a ys"
--- a/src/HOL/Old_Number_Theory/Int2.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Int2.thy Sat Jul 05 11:01:53 2014 +0200
@@ -51,7 +51,7 @@
have "(x div z) * z \<le> (x div z) * z" by simp
then have "(x div z) * z \<le> (x div z) * z + x mod z" using modth by arith
also have "\<dots> = x"
- by (auto simp add: zmod_zdiv_equality [symmetric] mult_ac)
+ by (auto simp add: zmod_zdiv_equality [symmetric] ac_simps)
also note `x < y * z`
finally show ?thesis
apply (auto simp add: mult_less_cancel_right)
@@ -115,7 +115,7 @@
lemma zcong_zmult_prop2: "[a = b](mod m) ==>
([c = d * a](mod m) = [c = d * b] (mod m))"
- by (auto simp add: mult_ac zcong_zmult_prop1)
+ by (auto simp add: ac_simps zcong_zmult_prop1)
lemma zcong_zmult_prop3: "[| zprime p; ~[x = 0] (mod p);
~[y = 0] (mod p) |] ==> ~[x * y = 0] (mod p)"
@@ -198,7 +198,7 @@
lemma MultInv_prop2a: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==>
[(MultInv p x) * x = 1] (mod p)"
- by (auto simp add: MultInv_prop2 mult_ac)
+ by (auto simp add: MultInv_prop2 ac_simps)
lemma aux_1: "2 < p ==> ((nat p) - 2) = (nat (p - 2))"
by (simp add: nat_diff_distrib)
@@ -227,7 +227,7 @@
apply (insert MultInv_prop2 [of p "MultInv p x"], auto)
apply (drule MultInv_prop2, auto)
apply (drule_tac k = x in zcong_scalar2, auto)
- apply (auto simp add: mult_ac)
+ apply (auto simp add: ac_simps)
done
lemma MultInv_prop4: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==>
@@ -244,10 +244,10 @@
m = p and k = x in zcong_scalar)
apply (insert MultInv_prop2 [of p x], simp)
apply (auto simp only: zcong_sym [of "MultInv p x * x"])
- apply (auto simp add: mult_ac)
+ apply (auto simp add: ac_simps)
apply (drule zcong_trans, auto)
apply (drule_tac a = "x * MultInv p y" and k = y in zcong_scalar, auto)
- apply (insert MultInv_prop2a [of p y], auto simp add: mult_ac)
+ apply (insert MultInv_prop2a [of p y], auto simp add: ac_simps)
apply (insert zcong_zmult_prop2 [of "y * MultInv p y" 1 p y x])
apply (auto simp add: zcong_sym)
done
@@ -264,7 +264,7 @@
[j * k = a * MultInv p k * k] (mod p) |] ==> [j * k = a] (mod p)"
apply (insert MultInv_prop2a [of p k] zcong_zmult_prop2
[of "MultInv p k * k" 1 p "j * k" a])
- apply (auto simp add: mult_ac)
+ apply (auto simp add: ac_simps)
done
lemma aux___3: "[j * k = a] (mod p) ==> [(MultInv p j) * j * k =
@@ -276,7 +276,7 @@
==> [k = a * (MultInv p j)] (mod p)"
apply (insert MultInv_prop2a [of p j] zcong_zmult_prop1
[of "MultInv p j * j" 1 p "MultInv p j * a" k])
- apply (auto simp add: mult_ac zcong_sym)
+ apply (auto simp add: ac_simps zcong_sym)
done
lemma MultInv_zcong_prop2: "[| 2 < p; zprime p; ~([k = 0](mod p));
--- a/src/HOL/Old_Number_Theory/IntPrimes.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Old_Number_Theory/IntPrimes.thy Sat Jul 05 11:01:53 2014 +0200
@@ -253,7 +253,7 @@
lemma zcong_zmod_aux:
"a - b = (m::int) * (a div m - b div m) + (a mod m - b mod m)"
- by(simp add: right_diff_distrib add_diff_eq eq_diff_eq add_ac)
+ by(simp add: right_diff_distrib add_diff_eq eq_diff_eq ac_simps)
lemma zcong_zmod: "[a = b] (mod m) = [a mod m = b mod m] (mod m)"
apply (unfold zcong_def)
--- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy Sat Jul 05 11:01:53 2014 +0200
@@ -351,7 +351,7 @@
hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)"
by (simp only: diff_add_assoc[OF dble, of d, symmetric])
hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
- by (simp only: diff_mult_distrib2 add.commute mult_ac)
+ by (simp only: diff_mult_distrib2 add.commute ac_simps)
hence ?thesis using H(1,2)
apply -
apply (rule exI[where x=d], simp)
@@ -492,20 +492,20 @@
from pos_k k_m have pos_p: "p > 0" by auto
from pos_k k_n have pos_q: "q > 0" by auto
have "k * k * gcd q p = k * gcd (k * q) (k * p)"
- by (simp add: mult_ac gcd_mult_distrib2)
+ by (simp add: ac_simps gcd_mult_distrib2)
also have "\<dots> = k * gcd (m * p * q) (n * q * p)"
by (simp add: k_m [symmetric] k_n [symmetric])
also have "\<dots> = k * p * q * gcd m n"
- by (simp add: mult_ac gcd_mult_distrib2)
+ by (simp add: ac_simps gcd_mult_distrib2)
finally have "(m * p) * (n * q) * gcd q p = k * p * q * gcd m n"
by (simp only: k_m [symmetric] k_n [symmetric])
then have "p * q * m * n * gcd q p = p * q * k * gcd m n"
- by (simp add: mult_ac)
+ by (simp add: ac_simps)
with pos_p pos_q have "m * n * gcd q p = k * gcd m n"
by simp
with prod_gcd_lcm [of m n]
have "lcm m n * gcd q p * gcd m n = k * gcd m n"
- by (simp add: mult_ac)
+ by (simp add: ac_simps)
with pos_gcd have "lcm m n * gcd q p = k" by simp
then show ?thesis using dvd_def by auto
qed
@@ -525,7 +525,7 @@
then have npos: "n > 0" by simp
have "gcd m n dvd n" by simp
then obtain k where "n = gcd m n * k" using dvd_def by auto
- then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n" by (simp add: mult_ac)
+ then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n" by (simp add: ac_simps)
also have "\<dots> = m * k" using mpos npos gcd_zero by simp
finally show ?thesis by (simp add: lcm_def)
qed
@@ -546,7 +546,7 @@
then have mpos: "m > 0" by simp
have "gcd m n dvd m" by simp
then obtain k where "m = gcd m n * k" using dvd_def by auto
- then have "m * n div gcd m n = (gcd m n * k) * n div gcd m n" by (simp add: mult_ac)
+ then have "m * n div gcd m n = (gcd m n * k) * n div gcd m n" by (simp add: ac_simps)
also have "\<dots> = n * k" using mpos npos gcd_zero by simp
finally show ?thesis by (simp add: lcm_def)
qed
--- a/src/HOL/Old_Number_Theory/Pocklington.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Pocklington.thy Sat Jul 05 11:01:53 2014 +0200
@@ -1020,7 +1020,7 @@
from n nqr have aqr0: "a ^ (q * r) \<noteq> 0" using a0 by simp
hence "(a ^ (q * r) - 1) + 1 = a ^ (q * r)" by simp
with k l have "a ^ (q * r) = p*l*k + 1" by simp
- hence "a ^ (r * q) + p * 0 = 1 + p * (l*k)" by (simp add: mult_ac)
+ hence "a ^ (r * q) + p * 0 = 1 + p * (l*k)" by (simp add: ac_simps)
hence odq: "ord p (a^r) dvd q"
unfolding ord_divides[symmetric] power_mult[symmetric] nat_mod by blast
from odq[unfolded dvd_def] obtain d where d: "q = ord p (a^r) * d" by blast
--- a/src/HOL/Old_Number_Theory/Primes.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Primes.thy Sat Jul 05 11:01:53 2014 +0200
@@ -227,10 +227,10 @@
apply (case_tac "d * x - a * b * y = Suc 0 ", simp_all)
apply (rule_tac x="x" in exI)
apply (rule_tac x="a*y" in exI)
-apply (simp add: mult_ac)
+apply (simp add: ac_simps)
apply (rule_tac x="a*x" in exI)
apply (rule_tac x="y" in exI)
-apply (simp add: mult_ac)
+apply (simp add: ac_simps)
done
lemma coprime_rmul2: "coprime d (a * b) \<Longrightarrow> coprime d a"
@@ -239,10 +239,10 @@
apply (case_tac "d * x - a * b * y = Suc 0 ", simp_all)
apply (rule_tac x="x" in exI)
apply (rule_tac x="b*y" in exI)
-apply (simp add: mult_ac)
+apply (simp add: ac_simps)
apply (rule_tac x="b*x" in exI)
apply (rule_tac x="y" in exI)
-apply (simp add: mult_ac)
+apply (simp add: ac_simps)
done
lemma coprime_mul_eq: "coprime d (a * b) \<longleftrightarrow> coprime d a \<and> coprime d b"
using coprime_rmul2[of d a b] coprime_lmul2[of d a b] coprime_mul[of d a b]
@@ -288,7 +288,7 @@
moreover
{assume z: "?g \<noteq> 0"
from gcd_dvd1[of a b] gcd_dvd2[of a b] obtain a' b' where
- ab': "a = a'*?g" "b = b'*?g" unfolding dvd_def by (auto simp add: mult_ac)
+ ab': "a = a'*?g" "b = b'*?g" unfolding dvd_def by (auto simp add: ac_simps)
hence ab'': "?g*a' = a" "?g * b' = b" by algebra+
from coprime_exp_imp[OF gcd_coprime[OF z ab'], unfolded coprime_bezout, of n]
obtain x y where "a'^n * x - b'^n * y = 1 \<or> b'^n * x - a'^n * y = 1" by blast
--- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy Sat Jul 05 11:01:53 2014 +0200
@@ -388,7 +388,7 @@
by (auto simp add: int_distrib)
then have "((p - 1) * q) div 2 < (((q - 1) * p) + (2 * p)) div 2"
apply (rule_tac x = "((p - 1) * q)" in even_div_2_l)
- by (auto simp add: even3, auto simp add: mult_ac)
+ by (auto simp add: even3, auto simp add: ac_simps)
also have "((p - 1) * q) div 2 = q * ((p - 1) div 2)"
by (auto simp add: even1 even_prod_div_2)
also have "(((q - 1) * p) + (2 * p)) div 2 = (((q - 1) div 2) * p) + p"
@@ -557,11 +557,11 @@
lemma S1_carda: "int (card(S1)) =
setsum (%j. (j * q) div p) P_set"
- by (auto simp add: S1_card mult_ac)
+ by (auto simp add: S1_card ac_simps)
lemma S2_carda: "int (card(S2)) =
setsum (%j. (j * p) div q) Q_set"
- by (auto simp add: S2_card mult_ac)
+ by (auto simp add: S2_card ac_simps)
lemma pq_sum_prop: "(setsum (%j. (j * p) div q) Q_set) +
(setsum (%j. (j * q) div p) P_set) = ((p - 1) div 2) * ((q - 1) div 2)"
--- a/src/HOL/Power.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Power.thy Sat Jul 05 11:01:53 2014 +0200
@@ -110,7 +110,7 @@
lemma power_mult_distrib [field_simps]:
"(a * b) ^ n = (a ^ n) * (b ^ n)"
- by (induct n) (simp_all add: mult_ac)
+ by (induct n) (simp_all add: ac_simps)
end
@@ -562,7 +562,7 @@
next
case (Suc n)
have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)"
- by (simp add: mult_ac power_add power2_eq_square)
+ by (simp add: ac_simps power_add power2_eq_square)
thus ?case
by (simp del: power_Suc add: Suc mult_less_0_iff mult_neg_neg)
qed
@@ -580,7 +580,7 @@
next
case (Suc n)
have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)"
- by (simp add: mult_ac power_add power2_eq_square)
+ by (simp add: ac_simps power_add power2_eq_square)
thus ?case
by (simp add: Suc zero_le_mult_iff)
qed
--- a/src/HOL/Presburger.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Presburger.thy Sat Jul 05 11:01:53 2014 +0200
@@ -185,7 +185,7 @@
proof
assume ?LHS
then obtain x where P: "P x" ..
- have "x mod d = x - (x div d)*d" by(simp add:zmod_zdiv_equality mult_ac eq_diff_eq)
+ have "x mod d = x - (x div d)*d" by(simp add:zmod_zdiv_equality ac_simps eq_diff_eq)
hence Pmod: "P x = P(x mod d)" using modd by simp
show ?RHS
proof (cases)
@@ -307,7 +307,7 @@
{fix x
have "P x \<longrightarrow> P (x + i * d)" using step.hyps by blast
also have "\<dots> \<longrightarrow> P(x + (i + 1) * d)" using plus[THEN spec, of "x + i * d"]
- by (simp add:int_distrib add_ac)
+ by (simp add:int_distrib ac_simps)
ultimately have "P x \<longrightarrow> P(x + (i + 1) * d)" by blast}
thus ?case ..
qed
--- a/src/HOL/Probability/Bochner_Integration.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Probability/Bochner_Integration.thy Sat Jul 05 11:01:53 2014 +0200
@@ -475,7 +475,7 @@
by (subst simple_bochner_integral_partition[OF f(1), where g="\<lambda>x. ereal (f x)" and v=real])
(auto intro: f simple_function_compose1 elim: simple_bochner_integrable.cases
intro!: setsum.cong ereal_cong_mult
- simp: setsum_ereal[symmetric] times_ereal.simps(1)[symmetric] mult_ac
+ simp: setsum_ereal[symmetric] times_ereal.simps(1)[symmetric] ac_simps
simp del: setsum_ereal times_ereal.simps(1))
also have "\<dots> = (\<integral>\<^sup>+x. f x \<partial>M)"
using f
@@ -631,7 +631,7 @@
(is "eventually (\<lambda>i. ?f i \<le> ?g i) sequentially")
proof (intro always_eventually allI)
fix i have "?f i \<le> (\<integral>\<^sup>+ x. ereal K * norm (f x - s i x) \<partial>M)"
- using K by (intro nn_integral_mono) (auto simp: mult_ac)
+ using K by (intro nn_integral_mono) (auto simp: ac_simps)
also have "\<dots> = ?g i"
using K by (intro nn_integral_cmult) auto
finally show "?f i \<le> ?g i" .
--- a/src/HOL/Probability/Borel_Space.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Probability/Borel_Space.thy Sat Jul 05 11:01:53 2014 +0200
@@ -136,7 +136,7 @@
shows "f \<in> borel_measurable (restrict_space M \<Omega>) \<longleftrightarrow>
(\<lambda>x. indicator \<Omega> x *\<^sub>R f x) \<in> borel_measurable M"
by (subst measurable_restrict_space_iff)
- (auto simp: indicator_def if_distrib[where f="\<lambda>x. x *\<^sub>R a" for a] mult_ac cong del: if_cong)
+ (auto simp: indicator_def if_distrib[where f="\<lambda>x. x *\<^sub>R a" for a] ac_simps cong del: if_cong)
lemma cbox_borel[measurable]: "cbox a b \<in> sets borel"
by (auto intro: borel_closed)
--- a/src/HOL/Probability/Convolution.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Probability/Convolution.thy Sat Jul 05 11:01:53 2014 +0200
@@ -41,7 +41,7 @@
assumes [simp]: "space M = space N" "space N = space borel"
shows "emeasure (M \<star> N) A = \<integral>\<^sup>+x. (emeasure N {a. a + x \<in> A}) \<partial>M "
using assms by (auto intro!: nn_integral_cong simp del: nn_integral_indicator simp: nn_integral_convolution
- nn_integral_indicator[symmetric] ab_semigroup_add_class.add_ac split:split_indicator)
+ nn_integral_indicator [symmetric] ac_simps split:split_indicator)
lemma convolution_emeasure':
assumes [simp]:"A \<in> sets borel"
--- a/src/HOL/Probability/Distributions.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Probability/Distributions.thy Sat Jul 05 11:01:53 2014 +0200
@@ -33,7 +33,7 @@
by (auto simp add: field_simps)
have eq: "\<And>x. ereal \<bar>c\<bar> * (f x / ereal \<bar>c\<bar>) = f x"
- using c by (simp add: divide_ereal_def mult_ac one_ereal_def[symmetric])
+ using c by (simp add: divide_ereal_def ac_simps one_ereal_def[symmetric])
have "density lborel f = distr M lborel X"
using f by (simp add: distributed_def)
@@ -49,7 +49,7 @@
shows "distributed M lborel X f"
proof -
have eq: "\<And>x. f x * ereal \<bar>c\<bar> / ereal \<bar>c\<bar> = f x"
- using c by (simp add: divide_ereal_def mult_ac one_ereal_def[symmetric])
+ using c by (simp add: divide_ereal_def ac_simps one_ereal_def[symmetric])
show ?thesis
using distributed_affine[OF f c, where t=t] c
--- a/src/HOL/Probability/Lebesgue_Measure.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Sat Jul 05 11:01:53 2014 +0200
@@ -1270,7 +1270,7 @@
assumes "!!x. DERIV G x :> g x"
shows "(\<integral>x. indicator {a .. b} x *\<^sub>R (F x * g x) \<partial>lborel)
= F b * G b - F a * G a - \<integral>x. indicator {a .. b} x *\<^sub>R (f x * G x) \<partial>lborel"
- using integral_by_parts[OF assms] by (simp add: mult_ac)
+ using integral_by_parts[OF assms] by (simp add: ac_simps)
lemma has_bochner_integral_even_function:
fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
--- a/src/HOL/Proofs/Extraction/Euclid.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Proofs/Extraction/Euclid.thy Sat Jul 05 11:01:53 2014 +0200
@@ -92,7 +92,7 @@
from m have "0 < m" by simp
moreover note n
moreover from False n nmk k have "Suc 0 < k" by auto
- moreover from nmk have "k * m = n" by (simp only: mult_ac)
+ moreover from nmk have "k * m = n" by (simp only: ac_simps)
ultimately have mn: "m < n" by (rule prod_mn_less_k)
with kn A nmk show ?thesis by iprover
qed
@@ -118,7 +118,7 @@
next
assume "m = Suc n"
then have "m dvd (fact n * Suc n)"
- by (auto intro: dvdI simp: mult_ac)
+ by (auto intro: dvdI simp: ac_simps)
then show ?thesis by (simp add: mult.commute)
qed
qed
--- a/src/HOL/Quotient_Examples/Quotient_Int.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Sat Jul 05 11:01:53 2014 +0200
@@ -60,7 +60,7 @@
apply(hypsubst_thin)
apply(rename_tac u v w x y z)
apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")
- apply(simp add: mult_ac)
+ apply(simp add: ac_simps)
apply(simp add: add_mult_distrib [symmetric])
done
@@ -73,7 +73,7 @@
apply(hypsubst_thin)
apply(rename_tac u v w x y z)
apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")
- apply(simp add: mult_ac)
+ apply(simp add: ac_simps)
apply(simp add: add_mult_distrib [symmetric])
done
--- a/src/HOL/Rat.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Rat.thy Sat Jul 05 11:01:53 2014 +0200
@@ -118,7 +118,7 @@
lift_definition plus_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat"
is "\<lambda>x y. (fst x * snd y + fst y * snd x, snd x * snd y)"
- by (clarsimp, simp add: distrib_right, simp add: mult_ac)
+ by (clarsimp, simp add: distrib_right, simp add: ac_simps)
lemma add_rat [simp]:
assumes "b \<noteq> 0" and "d \<noteq> 0"
@@ -144,7 +144,7 @@
lift_definition times_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat"
is "\<lambda>x y. (fst x * fst y, snd x * snd y)"
- by (simp add: mult_ac)
+ by (simp add: ac_simps)
lemma mult_rat [simp]: "Fract a b * Fract c d = Fract (a * c) (b * d)"
by transfer simp
@@ -271,7 +271,7 @@
proof -
assume "p * gcd r s = sgn (q * s) * r * gcd p q" and "q * gcd r s = sgn (q * s) * s * gcd p q"
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
- with assms show "p * s = q * r" by (auto simp add: mult_ac sgn_times sgn_0_0)
+ with assms show "p * s = q * r" by (auto simp add: ac_simps sgn_times sgn_0_0)
qed
from assms show ?thesis
by (auto simp add: normalize_def Let_def dvd_div_div_eq_mult mult.commute sgn_times split: if_splits intro: aux)
@@ -413,7 +413,7 @@
hence "a * d * b * d = c * b * b * d"
by simp
hence "a * b * d\<^sup>2 = c * d * b\<^sup>2"
- unfolding power2_eq_square by (simp add: mult_ac)
+ unfolding power2_eq_square by (simp add: ac_simps)
hence "0 < a * b * d\<^sup>2 \<longleftrightarrow> 0 < c * d * b\<^sup>2"
by simp
thus "0 < a * b \<longleftrightarrow> 0 < c * d"
@@ -434,7 +434,7 @@
lemma positive_mult:
"positive x \<Longrightarrow> positive y \<Longrightarrow> positive (x * y)"
-by transfer (drule (1) mult_pos_pos, simp add: mult_ac)
+by transfer (drule (1) mult_pos_pos, simp add: ac_simps)
lemma positive_minus:
"\<not> positive x \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> positive (- x)"
@@ -676,7 +676,7 @@
lemma of_rat_mult: "of_rat (a * b) = of_rat a * of_rat b"
apply transfer
-apply (simp add: divide_inverse nonzero_inverse_mult_distrib mult_ac)
+apply (simp add: divide_inverse nonzero_inverse_mult_distrib ac_simps)
done
lemma nonzero_of_rat_inverse:
--- a/src/HOL/Real.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Real.thy Sat Jul 05 11:01:53 2014 +0200
@@ -474,9 +474,9 @@
instance proof
fix a b c :: real
show "a + b = b + a"
- by transfer (simp add: add_ac realrel_def)
+ by transfer (simp add: ac_simps realrel_def)
show "(a + b) + c = a + (b + c)"
- by transfer (simp add: add_ac realrel_def)
+ by transfer (simp add: ac_simps realrel_def)
show "0 + a = a"
by transfer (simp add: realrel_def)
show "- a + a = 0"
@@ -484,11 +484,11 @@
show "a - b = a + - b"
by (rule minus_real_def)
show "(a * b) * c = a * (b * c)"
- by transfer (simp add: mult_ac realrel_def)
+ by transfer (simp add: ac_simps realrel_def)
show "a * b = b * a"
- by transfer (simp add: mult_ac realrel_def)
+ by transfer (simp add: ac_simps realrel_def)
show "1 * a = a"
- by transfer (simp add: mult_ac realrel_def)
+ by transfer (simp add: ac_simps realrel_def)
show "(a + b) * c = a * c + b * c"
by transfer (simp add: distrib_right realrel_def)
show "(0\<Colon>real) \<noteq> (1\<Colon>real)"
@@ -707,7 +707,7 @@
shows "Real X \<le> Real Y = (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. X n \<le> Y n + r)"
unfolding not_less [symmetric, where 'a=real] less_real_def
apply (simp add: diff_Real not_positive_Real X Y)
-apply (simp add: diff_le_eq add_ac)
+apply (simp add: diff_le_eq ac_simps)
done
lemma le_RealI:
--- a/src/HOL/Real_Vector_Spaces.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy Sat Jul 05 11:01:53 2014 +0200
@@ -897,7 +897,7 @@
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))"
using insert by auto
finally show ?case
- by (auto simp add: add_ac mult_right_mono mult_left_mono)
+ by (auto simp add: ac_simps mult_right_mono mult_left_mono)
qed simp_all
lemma norm_power_diff:
@@ -1159,7 +1159,7 @@
lemma sgn_scaleR:
"sgn (scaleR r x) = scaleR (sgn r) (sgn(x::'a::real_normed_vector))"
-by (simp add: sgn_div_norm mult_ac)
+by (simp add: sgn_div_norm ac_simps)
lemma sgn_one [simp]: "sgn (1::'a::real_normed_algebra_1) = 1"
by (simp add: sgn_div_norm)
@@ -1308,7 +1308,7 @@
apply (rule_tac K="norm b * K" in bounded_linear_intro)
apply (rule add_left)
apply (rule scaleR_left)
-apply (simp add: mult_ac)
+apply (simp add: ac_simps)
done
lemma bounded_linear_right:
@@ -1317,7 +1317,7 @@
apply (rule_tac K="norm a * K" in bounded_linear_intro)
apply (rule add_right)
apply (rule scaleR_right)
-apply (simp add: mult_ac)
+apply (simp add: ac_simps)
done
lemma prod_diff_prod:
--- a/src/HOL/Rings.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Rings.thy Sat Jul 05 11:01:53 2014 +0200
@@ -21,7 +21,7 @@
text{*For the @{text combine_numerals} simproc*}
lemma combine_common_factor:
"a * e + (b * e + c) = (a + b) * e + c"
-by (simp add: distrib_right add_ac)
+by (simp add: distrib_right ac_simps)
end
@@ -55,9 +55,9 @@
proof
fix a b c :: 'a
show "(a + b) * c = a * c + b * c" by (simp add: distrib)
- have "a * (b + c) = (b + c) * a" by (simp add: mult_ac)
+ have "a * (b + c) = (b + c) * a" by (simp add: ac_simps)
also have "... = b * a + c * a" by (simp only: distrib)
- also have "... = a * b + a * c" by (simp add: mult_ac)
+ also have "... = a * b + a * c" by (simp add: ac_simps)
finally show "a * (b + c) = a * b + a * c" by blast
qed
@@ -180,7 +180,7 @@
proof -
from `a dvd b` obtain b' where "b = a * b'" ..
moreover from `c dvd d` obtain d' where "d = c * d'" ..
- ultimately have "b * d = (a * c) * (b' * d')" by (simp add: mult_ac)
+ ultimately have "b * d = (a * c) * (b' * d')" by (simp add: ac_simps)
then show ?thesis ..
qed
@@ -188,7 +188,7 @@
by (simp add: dvd_def mult.assoc, blast)
lemma dvd_mult_right: "a * b dvd c \<Longrightarrow> b dvd c"
- unfolding mult_ac [of a] by (rule dvd_mult_left)
+ unfolding mult.commute [of a] by (rule dvd_mult_left)
lemma dvd_0_left: "0 dvd a \<Longrightarrow> a = 0"
by simp
@@ -437,7 +437,7 @@
"a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b"
proof -
have "a * c dvd b * c \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
- unfolding dvd_def by (simp add: mult_ac)
+ unfolding dvd_def by (simp add: ac_simps)
also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
unfolding dvd_def by simp
finally show ?thesis .
@@ -447,7 +447,7 @@
"c * a dvd c * b \<longleftrightarrow> c = 0 \<or> a dvd b"
proof -
have "c * a dvd c * b \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
- unfolding dvd_def by (simp add: mult_ac)
+ unfolding dvd_def by (simp add: ac_simps)
also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
unfolding dvd_def by simp
finally show ?thesis .
--- a/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy Sat Jul 05 11:01:53 2014 +0200
@@ -26,7 +26,7 @@
proof -
from `0 \<le> c` `0 < d` `c - c sdiv d * d = 0`
have "d dvd c"
- by (auto simp add: sdiv_pos_pos dvd_def mult_ac)
+ by (auto simp add: sdiv_pos_pos dvd_def ac_simps)
with `0 < d` `gcd c d = gcd m n` show ?C1
by simp
qed
--- a/src/HOL/Semiring_Normalization.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Semiring_Normalization.thy Sat Jul 05 11:01:53 2014 +0200
@@ -47,7 +47,7 @@
then have "(y - z) * (w - x) = 0" by (simp add: algebra_simps)
then have "y - z = 0 \<or> w - x = 0" by (rule divisors_zero)
then show "w = x \<or> y = z" by auto
- qed (auto simp add: add_ac)
+ qed (auto simp add: ac_simps)
qed
instance nat :: comm_semiring_1_cancel_crossproduct
--- a/src/HOL/Set_Interval.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Set_Interval.thy Sat Jul 05 11:01:53 2014 +0200
@@ -1409,22 +1409,22 @@
on intervals are not? *)
lemma setsum_atMost_Suc[simp]: "(\<Sum>i \<le> Suc n. f i) = (\<Sum>i \<le> n. f i) + f(Suc n)"
-by (simp add:atMost_Suc add_ac)
+by (simp add:atMost_Suc ac_simps)
lemma setsum_lessThan_Suc[simp]: "(\<Sum>i < Suc n. f i) = (\<Sum>i < n. f i) + f n"
-by (simp add:lessThan_Suc add_ac)
+by (simp add:lessThan_Suc ac_simps)
lemma setsum_cl_ivl_Suc[simp]:
"setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))"
-by (auto simp:add_ac atLeastAtMostSuc_conv)
+by (auto simp:ac_simps atLeastAtMostSuc_conv)
lemma setsum_op_ivl_Suc[simp]:
"setsum f {m..<Suc n} = (if n < m then 0 else setsum f {m..<n} + f(n))"
-by (auto simp:add_ac atLeastLessThanSuc)
+by (auto simp:ac_simps atLeastLessThanSuc)
(*
lemma setsum_cl_ivl_add_one_nat: "(n::nat) <= m + 1 ==>
(\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)"
-by (auto simp:add_ac atLeastAtMostSuc_conv)
+by (auto simp:ac_simps atLeastAtMostSuc_conv)
*)
lemma setsum_head:
@@ -1468,7 +1468,7 @@
shows "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
setsum f {m..<p} - setsum f {m..<n} = setsum f {n..<p}"
using setsum_add_nat_ivl [of m n p f,symmetric]
-apply (simp add: add_ac)
+apply (simp add: ac_simps)
done
lemma setsum_natinterval_difff:
@@ -1600,15 +1600,15 @@
also from ngt1 have "\<dots> = ?n*a + (\<Sum>i\<in>{..<n}. ?I i*d)" by simp
also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))"
unfolding One_nat_def
- by (simp add: setsum_right_distrib atLeast0LessThan[symmetric] setsum_shift_lb_Suc0_0_upt mult_ac)
+ by (simp add: setsum_right_distrib atLeast0LessThan[symmetric] setsum_shift_lb_Suc0_0_upt ac_simps)
also have "2*\<dots> = 2*?n*a + d*2*(\<Sum>i\<in>{1..<n}. ?I i)"
by (simp add: algebra_simps)
also from ngt1 have "{1..<n} = {1..n - 1}"
by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost)
also from ngt1
have "2*?n*a + d*2*(\<Sum>i\<in>{1..n - 1}. ?I i) = (2*?n*a + d*?I (n - 1)*?I n)"
- by (simp only: mult_ac gauss_sum [of "n - 1"], unfold One_nat_def)
- (simp add: mult_ac trans [OF add.commute of_nat_Suc [symmetric]])
+ by (simp only: mult.assoc gauss_sum [of "n - 1"], unfold One_nat_def)
+ (simp add: mult.commute trans [OF add.commute of_nat_Suc [symmetric]])
finally show ?thesis
unfolding mult_2 by (simp add: algebra_simps)
next
--- a/src/HOL/Tools/Qelim/cooper.ML Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Sat Jul 05 11:01:53 2014 +0200
@@ -76,7 +76,7 @@
val presburger_ss = simpset_of (@{context} addsimps [zdvd1_eq]);
val lin_ss =
simpset_of (put_simpset presburger_ss @{context}
- addsimps (@{thm dvd_eq_mod_eq_0} :: zdvd1_eq :: @{thms add_ac [where 'a=int]}));
+ addsimps (@{thm dvd_eq_mod_eq_0} :: zdvd1_eq :: @{thms ac_simps [where 'a=int]}));
val iT = HOLogic.intT
val bT = HOLogic.boolT;
@@ -826,7 +826,7 @@
@ [@{thm "mod_self"}, @{thm "mod_by_0"}, @{thm "div_by_0"},
@{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"},
@{thm "mod_1"}, @{thm "Suc_eq_plus1"}]
- @ @{thms add_ac}
+ @ @{thms ac_simps}
addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}])
val splits_ss =
simpset_of (put_simpset comp_ss @{context}
--- a/src/HOL/Tools/group_cancel.ML Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Tools/group_cancel.ML Sat Jul 05 11:01:53 2014 +0200
@@ -19,13 +19,13 @@
struct
val add1 = @{lemma "(A::'a::comm_monoid_add) == k + a ==> A + b == k + (a + b)"
- by (simp only: add_ac)}
+ by (simp only: ac_simps)}
val add2 = @{lemma "(B::'a::comm_monoid_add) == k + b ==> a + B == k + (a + b)"
- by (simp only: add_ac)}
+ by (simp only: ac_simps)}
val sub1 = @{lemma "(A::'a::ab_group_add) == k + a ==> A - b == k + (a - b)"
by (simp only: add_diff_eq)}
val sub2 = @{lemma "(B::'a::ab_group_add) == k + b ==> a - B == - k + (a - b)"
- by (simp only: minus_add diff_conv_add_uminus add_ac)}
+ by (simp only: minus_add diff_conv_add_uminus ac_simps)}
val neg1 = @{lemma "(A::'a::ab_group_add) == k + a ==> - A == - k + - a"
by (simp only: minus_add_distrib)}
val rule0 = @{lemma "(a::'a::comm_monoid_add) == a + 0"
--- a/src/HOL/Tools/nat_arith.ML Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Tools/nat_arith.ML Sat Jul 05 11:01:53 2014 +0200
@@ -16,9 +16,9 @@
struct
val add1 = @{lemma "(A::'a::comm_monoid_add) == k + a ==> A + b == k + (a + b)"
- by (simp only: add_ac)}
+ by (simp only: ac_simps)}
val add2 = @{lemma "(B::'a::comm_monoid_add) == k + b ==> a + B == k + (a + b)"
- by (simp only: add_ac)}
+ by (simp only: ac_simps)}
val suc1 = @{lemma "A == k + a ==> Suc A == k + Suc a"
by (simp only: add_Suc_right)}
val rule0 = @{lemma "(a::'a::comm_monoid_add) == a + 0"
--- a/src/HOL/Tools/nat_numeral_simprocs.ML Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML Sat Jul 05 11:01:53 2014 +0200
@@ -167,10 +167,10 @@
val norm_ss1 =
simpset_of (put_simpset Numeral_Simprocs.num_ss @{context}
addsimps numeral_syms @ add_0s @ mult_1s @
- [@{thm Suc_eq_plus1_left}] @ @{thms add_ac})
+ [@{thm Suc_eq_plus1_left}] @ @{thms ac_simps})
val norm_ss2 =
simpset_of (put_simpset Numeral_Simprocs.num_ss @{context}
- addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac})
+ addsimps bin_simps @ @{thms ac_simps} @ @{thms ac_simps})
fun norm_tac ctxt =
ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt))
THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt))
@@ -239,10 +239,10 @@
val norm_ss1 =
simpset_of (put_simpset Numeral_Simprocs.num_ss @{context}
- addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1}] @ @{thms add_ac})
+ addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1}] @ @{thms ac_simps})
val norm_ss2 =
simpset_of (put_simpset Numeral_Simprocs.num_ss @{context}
- addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac})
+ addsimps bin_simps @ @{thms ac_simps} @ @{thms ac_simps})
fun norm_tac ctxt =
ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt))
THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt))
@@ -270,10 +270,10 @@
val norm_ss1 =
simpset_of (put_simpset Numeral_Simprocs.num_ss @{context}
- addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1_left}] @ @{thms add_ac})
+ addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1_left}] @ @{thms ac_simps})
val norm_ss2 =
simpset_of (put_simpset Numeral_Simprocs.num_ss @{context}
- addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac})
+ addsimps bin_simps @ @{thms ac_simps} @ @{thms ac_simps})
fun norm_tac ctxt =
ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt))
THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt))
@@ -363,7 +363,7 @@
val trans_tac = Numeral_Simprocs.trans_tac
val norm_ss =
simpset_of (put_simpset HOL_basic_ss @{context}
- addsimps mult_1s @ @{thms mult_ac})
+ addsimps mult_1s @ @{thms ac_simps})
fun norm_tac ctxt =
ALLGOALS (simp_tac (put_simpset norm_ss ctxt))
val simplify_meta_eq = cancel_simplify_meta_eq
--- a/src/HOL/Tools/numeral_simprocs.ML Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML Sat Jul 05 11:01:53 2014 +0200
@@ -232,7 +232,7 @@
val norm_ss1 =
simpset_of (put_simpset num_ss @{context}
addsimps numeral_syms @ add_0s @ mult_1s @
- diff_simps @ minus_simps @ @{thms add_ac})
+ diff_simps @ minus_simps @ @{thms ac_simps})
val norm_ss2 =
simpset_of (put_simpset num_ss @{context}
@@ -240,7 +240,7 @@
val norm_ss3 =
simpset_of (put_simpset num_ss @{context}
- addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac minus_mult_commute})
+ addsimps minus_from_mult_simps @ @{thms ac_simps} @ @{thms ac_simps minus_mult_commute})
structure CancelNumeralsCommon =
struct
@@ -361,7 +361,7 @@
structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
struct
- val assoc_ss = simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms mult_ac minus_mult_commute})
+ val assoc_ss = simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms ac_simps minus_mult_commute})
val eq_reflection = eq_reflection
val is_numeral = can HOLogic.dest_number
end;
@@ -381,7 +381,7 @@
val norm_ss2 =
simpset_of (put_simpset HOL_basic_ss @{context} addsimps simps @ mult_minus_simps)
val norm_ss3 =
- simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms mult_ac minus_mult_commute})
+ simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms ac_simps minus_mult_commute})
fun norm_tac ctxt =
ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt))
THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt))
@@ -513,7 +513,7 @@
val find_first = find_first_t []
val trans_tac = trans_tac
val norm_ss =
- simpset_of (put_simpset HOL_basic_ss @{context} addsimps mult_1s @ @{thms mult_ac minus_mult_commute})
+ simpset_of (put_simpset HOL_basic_ss @{context} addsimps mult_1s @ @{thms ac_simps minus_mult_commute})
fun norm_tac ctxt =
ALLGOALS (simp_tac (put_simpset norm_ss ctxt))
val simplify_meta_eq = cancel_simplify_meta_eq
--- a/src/HOL/Transcendental.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Transcendental.thy Sat Jul 05 11:01:53 2014 +0200
@@ -481,10 +481,10 @@
apply (rule setsum.cong [OF refl])
apply (simp add: less_iff_Suc_add)
apply (clarify)
- apply (simp add: setsum_right_distrib lemma_realpow_diff_sumr2 mult_ac
+ apply (simp add: setsum_right_distrib lemma_realpow_diff_sumr2 ac_simps
del: setsum_lessThan_Suc power_Suc)
apply (subst mult.assoc [symmetric], subst power_add [symmetric])
- apply (simp add: mult_ac)
+ apply (simp add: ac_simps)
done
lemma real_setsum_nat_ivl_bounded2:
@@ -958,7 +958,7 @@
hence "norm (x * S n) \<le> real (Suc n) * r * norm (S n)"
by (rule order_trans [OF norm_mult_ineq])
hence "norm (x * S n) / real (Suc n) \<le> r * norm (S n)"
- by (simp add: pos_divide_le_eq mult_ac)
+ by (simp add: pos_divide_le_eq ac_simps)
thus "norm (S (Suc n)) \<le> r * norm (S n)"
by (simp add: S_Suc inverse_eq_divide)
qed
@@ -1058,7 +1058,7 @@
by (rule distrib_right)
also have "\<dots> = (\<Sum>i\<le>n. (x * S x i) * S y (n-i))
+ (\<Sum>i\<le>n. S x i * (y * S y (n-i)))"
- by (simp only: setsum_right_distrib mult_ac)
+ by (simp only: setsum_right_distrib ac_simps)
also have "\<dots> = (\<Sum>i\<le>n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i)))
+ (\<Sum>i\<le>n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))"
by (simp add: times_S Suc_diff_le)
@@ -1431,7 +1431,7 @@
by (rule mult_mono)
(rule mult_mono, simp_all add: power_le_one a b)
hence "inverse (fact (n + 2)) * x ^ (n + 2) \<le> (x\<^sup>2/2) * ((1/2)^n)"
- unfolding power_add by (simp add: mult_ac del: fact_Suc) }
+ unfolding power_add by (simp add: ac_simps del: fact_Suc) }
note aux1 = this
have "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums (x\<^sup>2 / 2 * (1 / (1 - 1 / 2)))"
by (intro sums_mult geometric_sums, simp)
@@ -2476,7 +2476,7 @@
proof -
have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. sin_coeff k * x ^ k) sums sin x"
by (rule sin_converges [THEN sums_group], simp)
- thus ?thesis unfolding One_nat_def sin_coeff_def by (simp add: mult_ac)
+ thus ?thesis unfolding One_nat_def sin_coeff_def by (simp add: ac_simps)
qed
lemma sin_gt_zero:
@@ -2512,7 +2512,7 @@
proof -
have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. cos_coeff k * x ^ k) sums cos x"
by (rule cos_converges [THEN sums_group], simp)
- thus ?thesis unfolding cos_coeff_def by (simp add: mult_ac)
+ thus ?thesis unfolding cos_coeff_def by (simp add: ac_simps)
qed
lemmas realpow_num_eq_if = power_eq_if
@@ -2533,7 +2533,7 @@
apply (drule sums_summable)
apply simp
apply (erule suminf_pos)
-apply (simp add: add_ac)
+apply (simp add: ac_simps)
done
lemma cos_two_less_zero [simp]:
--- a/src/HOL/UNITY/Comp/AllocBase.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.thy Sat Jul 05 11:01:53 2014 +0200
@@ -39,7 +39,7 @@
(** bag_of **)
lemma bag_of_append [simp]: "bag_of (l@l') = bag_of l + bag_of l'"
- by (induct l) (simp_all add: add_ac)
+ by (induct l) (simp_all add: ac_simps)
lemma mono_bag_of: "mono (bag_of :: 'a list => ('a::order) multiset)"
apply (rule monoI)
@@ -63,7 +63,7 @@
(\<Sum>i\<in> A Int lessThan (length l). {# l!i #})"
apply (rule_tac xs = l in rev_induct, simp)
apply (simp add: sublist_append Int_insert_right lessThan_Suc nth_append
- bag_of_sublist_lemma add_ac)
+ bag_of_sublist_lemma ac_simps)
done
--- a/src/HOL/Word/Bool_List_Representation.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Word/Bool_List_Representation.thy Sat Jul 05 11:01:53 2014 +0200
@@ -783,7 +783,7 @@
apply (case_tac binb rule: bin_exhaust)
apply (case_tac b)
apply (case_tac [!] "ba")
- apply (auto simp: rbl_succ bin_to_bl_aux_alt Let_def add_ac)
+ apply (auto simp: rbl_succ bin_to_bl_aux_alt Let_def ac_simps)
done
lemma rbl_add_app2:
@@ -1021,7 +1021,7 @@
apply (erule allE)
apply (erule (1) impE)
apply (drule bin_nth_split, erule conjE, erule allE,
- erule trans, simp add : add_ac)+
+ erule trans, simp add : ac_simps)+
done
lemma bin_rsplit_all:
--- a/src/HOL/Word/Word.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Word/Word.thy Sat Jul 05 11:01:53 2014 +0200
@@ -1592,7 +1592,7 @@
lemma no_olen_add':
fixes x :: "'a::len0 word"
shows "(x \<le> y + x) = (uint y + uint x < 2 ^ len_of TYPE('a))"
- by (simp add: add_ac no_olen_add)
+ by (simp add: ac_simps no_olen_add)
lemmas olen_add_eqv = trans [OF no_olen_add no_olen_add' [symmetric]]
@@ -1906,7 +1906,7 @@
lemma Abs_fnat_hom_Suc:
"word_succ (of_nat a) = of_nat (Suc a)"
- by (simp add: word_of_nat wi_hom_succ add_ac)
+ by (simp add: word_of_nat wi_hom_succ ac_simps)
lemma Abs_fnat_hom_0: "(0::'a::len word) = of_nat 0"
by simp
--- a/src/HOL/Word/Word_Miscellaneous.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Word/Word_Miscellaneous.thy Sat Jul 05 11:01:53 2014 +0200
@@ -331,7 +331,7 @@
prefer 2
apply (erule asm_rl)
apply (rule_tac f="%n. n div f" in arg_cong)
- apply (simp add : mult_ac)
+ apply (simp add : ac_simps)
done
lemma diff_mod_le: "(a::nat) < d ==> b dvd d ==> a - a mod b <= d - b"
--- a/src/HOL/ex/Dedekind_Real.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/ex/Dedekind_Real.thy Sat Jul 05 11:01:53 2014 +0200
@@ -285,7 +285,7 @@
show "\<exists>x' \<in> A. \<exists>y'\<in>B. z = x' + y'"
proof (intro bexI)
show "z = x*?f + y*?f"
- by (simp add: distrib_right [symmetric] divide_inverse mult_ac
+ by (simp add: distrib_right [symmetric] divide_inverse ac_simps
order_less_imp_not_eq2)
next
show "y * ?f \<in> B"
@@ -326,7 +326,7 @@
lemma preal_add_assoc: "((x::preal) + y) + z = x + (y + z)"
apply (simp add: preal_add_def mem_add_set Rep_preal)
-apply (force simp add: add_set_def add_ac)
+apply (force simp add: add_set_def ac_simps)
done
instance preal :: ab_semigroup_add
@@ -454,7 +454,7 @@
lemma preal_mult_assoc: "((x::preal) * y) * z = x * (y * z)"
apply (simp add: preal_mult_def mem_mult_set Rep_preal)
-apply (force simp add: mult_set_def mult_ac)
+apply (force simp add: mult_set_def ac_simps)
done
instance preal :: ab_semigroup_mult
@@ -713,7 +713,7 @@
have frle: "Fract a b \<le> Fract ?k 1 * (Fract c d)"
proof -
have "?thesis = ((a * d * b * d) \<le> c * b * (a * d * b * d))"
- by (simp add: order_less_imp_not_eq2 mult_ac)
+ by (simp add: order_less_imp_not_eq2 ac_simps)
moreover
have "(1 * (a * d * b * d)) \<le> c * b * (a * d * b * d)"
by (rule mult_mono,
@@ -961,7 +961,7 @@
apply (drule Rep_preal [THEN preal_exists_greater], clarify)
apply (cut_tac a="x+y" and b=u in add_eq_exists, clarify)
apply (rule_tac x="y+xa" in exI)
-apply (auto simp add: add_ac)
+apply (auto simp add: ac_simps)
done
lemma mem_diff_set:
@@ -1032,7 +1032,7 @@
proof (intro exI conjI)
show "r \<in> Rep_preal R" by (rule r)
show "r + e \<notin> Rep_preal R" by (rule notin)
- show "r + e + y \<in> Rep_preal S" using xe eq by (simp add: add_ac)
+ show "r + e + y \<in> Rep_preal S" using xe eq by (simp add: ac_simps)
show "x = r + y" by (simp add: eq)
show "0 < r + e" using epos preal_imp_pos [OF Rep_preal r]
by simp
@@ -1236,11 +1236,11 @@
and "x + y2 = x2 + y"
shows "x1 + y2 = x2 + (y1::preal)"
proof -
- have "(x1 + y2) + x = (x + y2) + x1" by (simp add: add_ac)
+ have "(x1 + y2) + x = (x + y2) + x1" by (simp add: ac_simps)
also have "... = (x2 + y) + x1" by (simp add: assms)
- also have "... = x2 + (x1 + y)" by (simp add: add_ac)
+ also have "... = x2 + (x1 + y)" by (simp add: ac_simps)
also have "... = x2 + (x + y1)" by (simp add: assms)
- also have "... = (x2 + y1) + x" by (simp add: add_ac)
+ also have "... = (x2 + y1) + x" by (simp add: ac_simps)
finally have "(x1 + y2) + x = (x2 + y1) + x" .
thus ?thesis by (rule add_right_imp_eq)
qed
@@ -1287,7 +1287,7 @@
apply (simp add: add.assoc)
apply (rule add.left_commute [of ab, THEN ssubst])
apply (simp add: add.assoc [symmetric])
-apply (simp add: add_ac)
+apply (simp add: ac_simps)
done
lemma real_add:
@@ -1318,7 +1318,7 @@
show "x + y = y + x"
by (cases x, cases y, simp add: real_add add.commute)
show "0 + x = x"
- by (cases x, simp add: real_add real_zero_def add_ac)
+ by (cases x, simp add: real_add real_zero_def ac_simps)
show "- x + x = 0"
by (cases x, simp add: real_minus real_add real_zero_def add.commute)
show "x - y = x + - y"
@@ -1354,7 +1354,7 @@
UN_equiv_class2 [OF equiv_realrel equiv_realrel real_mult_congruent2])
lemma real_mult_commute: "(z::real) * w = w * z"
-by (cases z, cases w, simp add: real_mult add_ac mult_ac)
+by (cases z, cases w, simp add: real_mult ac_simps ac_simps)
lemma real_mult_assoc: "((z1::real) * z2) * z3 = z1 * (z2 * z3)"
apply (cases z1, cases z2, cases z3)
@@ -1456,7 +1456,7 @@
shows "x1 + y2 \<le> x2 + (y1::preal)"
proof -
have "(x1+v1) + (u2+y2) = (u1+y1) + (x2+v2)" by (simp add: assms)
- hence "(x1+y2) + (u2+v1) = (x2+y1) + (u1+v2)" by (simp add: add_ac)
+ hence "(x1+y2) + (u2+v1) = (x2+y1) + (u1+v2)" by (simp add: ac_simps)
also have "... \<le> (x2+y1) + (u2+v1)" by (simp add: assms)
finally show ?thesis by simp
qed
@@ -1477,10 +1477,10 @@
and "x2 + v2 = u2 + y2"
shows "x + v' \<le> u' + (y::preal)"
proof -
- have "(x+v') + (u+v) = (x+v) + (u+v')" by (simp add: add_ac)
+ have "(x+v') + (u+v) = (x+v) + (u+v')" by (simp add: ac_simps)
also have "... \<le> (u+y) + (u+v')" by (simp add: assms)
also have "... \<le> (u+y) + (u'+v)" by (simp add: assms)
- also have "... = (u'+y) + (u+v)" by (simp add: add_ac)
+ also have "... = (u'+y) + (u+v)" by (simp add: ac_simps)
finally show ?thesis by simp
qed
@@ -1500,7 +1500,7 @@
(* Axiom 'linorder_linear' of class 'linorder': *)
lemma real_le_linear: "(z::real) \<le> w | w \<le> z"
apply (cases z, cases w)
-apply (auto simp add: real_le real_zero_def add_ac)
+apply (auto simp add: real_le real_zero_def ac_simps)
done
instance real :: linorder
@@ -1509,7 +1509,7 @@
lemma real_le_eq_diff: "(x \<le> y) = (x-y \<le> (0::real))"
apply (cases x, cases y)
apply (auto simp add: real_le real_zero_def real_diff_def real_add real_minus
- add_ac)
+ ac_simps)
apply (simp_all add: add.assoc [symmetric])
done
@@ -1589,7 +1589,7 @@
lemma real_of_preal_trichotomy:
"\<exists>m. (x::real) = real_of_preal m | x = 0 | x = -(real_of_preal m)"
apply (simp add: real_of_preal_def real_zero_def, cases x)
-apply (auto simp add: real_minus add_ac)
+apply (auto simp add: real_minus ac_simps)
apply (cut_tac x = xa and y = y in linorder_less_linear)
apply (auto dest!: less_add_left_Ex simp add: add.assoc [symmetric])
done
@@ -1616,9 +1616,9 @@
lemma real_of_preal_zero_less: "0 < real_of_preal m"
apply (insert preal_self_less_add_left [of 1 m])
apply (auto simp add: real_zero_def real_of_preal_def
- real_less_def real_le_def add_ac)
+ real_less_def real_le_def ac_simps)
apply (rule_tac x="m + 1" in exI, rule_tac x="1" in exI)
-apply (simp add: add_ac)
+apply (simp add: ac_simps)
done
lemma real_of_preal_minus_less_zero: "- real_of_preal m < 0"
--- a/src/HOL/ex/Sqrt.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/ex/Sqrt.thy Sat Jul 05 11:01:53 2014 +0200
@@ -33,7 +33,7 @@
from eq have "p dvd m\<^sup>2" ..
with `prime p` show "p dvd m" by (rule prime_dvd_power_nat)
then obtain k where "m = p * k" ..
- with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square mult_ac)
+ with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square ac_simps)
with p have "n\<^sup>2 = p * k\<^sup>2" by (simp add: power2_eq_square)
then have "p dvd n\<^sup>2" ..
with `prime p` show "p dvd n" by (rule prime_dvd_power_nat)
@@ -73,7 +73,7 @@
then have "p dvd m\<^sup>2" ..
with `prime p` have dvd_m: "p dvd m" by (rule prime_dvd_power_nat)
then obtain k where "m = p * k" ..
- with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square mult_ac)
+ with eq have "p * n\<^sup>2 = p\<^sup>2 * k\<^sup>2" by (auto simp add: power2_eq_square ac_simps)
with p have "n\<^sup>2 = p * k\<^sup>2" by (simp add: power2_eq_square)
then have "p dvd n\<^sup>2" ..
with `prime p` have "p dvd n" by (rule prime_dvd_power_nat)
--- a/src/HOL/ex/Sqrt_Script.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/ex/Sqrt_Script.thy Sat Jul 05 11:01:53 2014 +0200
@@ -36,7 +36,7 @@
done
lemma rearrange: "(j::nat) * (p * j) = k * k \<Longrightarrow> k * k = p * (j * j)"
- by (simp add: mult_ac)
+ by (simp add: ac_simps)
lemma prime_not_square:
"prime (p::nat) \<Longrightarrow> (\<And>k. 0 < k \<Longrightarrow> m * m \<noteq> p * (k * k))"
--- a/src/HOL/ex/ThreeDivides.thy Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/ex/ThreeDivides.thy Sat Jul 05 11:01:53 2014 +0200
@@ -80,7 +80,7 @@
hence "?thr dvd (10^(n+1) - 10)" by (simp add: nat_distrib)
ultimately
have"?thr dvd ((10^(n+1) - 10) + 9)"
- by (simp only: add_ac) (rule dvd_add)
+ by (simp only: ac_simps) (rule dvd_add)
thus ?case by simp
qed
@@ -194,7 +194,7 @@
"m = 10*(\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x) + c" by simp
also have
"\<dots> = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^(x+1)) + c"
- by (subst setsum_right_distrib) (simp add: mult_ac)
+ by (subst setsum_right_distrib) (simp add: ac_simps)
also have
"\<dots> = (\<Sum>x<nd. m div 10^(Suc x) mod 10 * 10^(Suc x)) + c"
by (simp add: div_mult2_eq[symmetric])