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.7 -by (simp add: distrib_right add_ac)
     1.8 +by (simp add: distrib_right ac_simps)
     1.9  
    1.10  end
    1.11  
    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.23  
    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.32  
    1.33 @@ -188,7 +188,7 @@
    1.34  by (simp add: dvd_def mult.assoc, blast)
    1.35  
    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.39  
    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 .