src/HOL/Rings.thy
 changeset 57514 bdc2c6b40bf2 parent 57512 cc97b347b301 child 58195 1fee63e0377d
1.1 --- a/src/HOL/Rings.thy	Sat Jul 05 10:09:01 2014 +0200
1.2 +++ b/src/HOL/Rings.thy	Sat Jul 05 11:01:53 2014 +0200
1.3 @@ -21,7 +21,7 @@
1.4  text{*For the @{text combine_numerals} simproc*}
1.5  lemma combine_common_factor:
1.6    "a * e + (b * e + c) = (a + b) * e + c"
1.8 +by (simp add: distrib_right ac_simps)
1.10  end
1.12 @@ -55,9 +55,9 @@
1.13  proof
1.14    fix a b c :: 'a
1.15    show "(a + b) * c = a * c + b * c" by (simp add: distrib)
1.16 -  have "a * (b + c) = (b + c) * a" by (simp add: mult_ac)
1.17 +  have "a * (b + c) = (b + c) * a" by (simp add: ac_simps)
1.18    also have "... = b * a + c * a" by (simp only: distrib)
1.19 -  also have "... = a * b + a * c" by (simp add: mult_ac)
1.20 +  also have "... = a * b + a * c" by (simp add: ac_simps)
1.21    finally show "a * (b + c) = a * b + a * c" by blast
1.22  qed
1.24 @@ -180,7 +180,7 @@
1.25  proof -
1.26    from `a dvd b` obtain b' where "b = a * b'" ..
1.27    moreover from `c dvd d` obtain d' where "d = c * d'" ..
1.28 -  ultimately have "b * d = (a * c) * (b' * d')" by (simp add: mult_ac)
1.29 +  ultimately have "b * d = (a * c) * (b' * d')" by (simp add: ac_simps)
1.30    then show ?thesis ..
1.31  qed
1.33 @@ -188,7 +188,7 @@
1.34  by (simp add: dvd_def mult.assoc, blast)
1.36  lemma dvd_mult_right: "a * b dvd c \<Longrightarrow> b dvd c"
1.37 -  unfolding mult_ac [of a] by (rule dvd_mult_left)
1.38 +  unfolding mult.commute [of a] by (rule dvd_mult_left)
1.40  lemma dvd_0_left: "0 dvd a \<Longrightarrow> a = 0"
1.41  by simp
1.42 @@ -437,7 +437,7 @@
1.43    "a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b"
1.44  proof -
1.45    have "a * c dvd b * c \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
1.46 -    unfolding dvd_def by (simp add: mult_ac)
1.47 +    unfolding dvd_def by (simp add: ac_simps)
1.48    also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
1.49      unfolding dvd_def by simp
1.50    finally show ?thesis .
1.51 @@ -447,7 +447,7 @@
1.52    "c * a dvd c * b \<longleftrightarrow> c = 0 \<or> a dvd b"
1.53  proof -
1.54    have "c * a dvd c * b \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
1.55 -    unfolding dvd_def by (simp add: mult_ac)
1.56 +    unfolding dvd_def by (simp add: ac_simps)
1.57    also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
1.58      unfolding dvd_def by simp
1.59    finally show ?thesis .