src/HOL/Rings.thy
 changeset 57514 bdc2c6b40bf2 parent 57512 cc97b347b301 child 58195 1fee63e0377d
```--- 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"

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 .```