src/HOL/Rings.thy

 lemma dvd_trans [trans]:
   assumes "a dvd b" and "b dvd c"
   shows "a dvd c"
 proof -
   from assms obtain v where "b = a * v"
-    by (auto elim!: dvdE)
+    by auto
   moreover from assms obtain w where "c = b * w"
-    by (auto elim!: dvdE)
+    by auto
   ultimately have "c = a * (v * w)"
     by (simp add: mult.assoc)
   then show ?thesis ..
 qed
 

 
 lemma strict_subset_divisors_dvd: "{c. c dvd a} \<subset> {c. c dvd b} \<longleftrightarrow> a dvd b \<and> \<not> b dvd a"
   by (auto simp add: subset_iff intro: dvd_trans)
 
 lemma one_dvd [simp]: "1 dvd a"
-  by (auto intro!: dvdI)
-
-lemma dvd_mult [simp]: "a dvd c \<Longrightarrow> a dvd (b * c)"
-  by (auto intro!: mult.left_commute dvdI elim!: dvdE)
-
-lemma dvd_mult2 [simp]: "a dvd b \<Longrightarrow> a dvd (b * c)"
-  using dvd_mult [of a b c] by (simp add: ac_simps)
+  by (auto intro: dvdI)
+
+lemma dvd_mult [simp]: "a dvd (b * c)" if "a dvd c"
+  using that by rule (auto intro: mult.left_commute dvdI)
+
+lemma dvd_mult2 [simp]: "a dvd (b * c)" if "a dvd b"
+  using that dvd_mult [of a b c] by (simp add: ac_simps)
 
 lemma dvd_triv_right [simp]: "a dvd b * a"
   by (rule dvd_mult) (rule dvd_refl)
 
 lemma dvd_triv_left [simp]: "a dvd a * b"

 begin
 
 subclass semiring_1 ..
 
 lemma dvd_0_left_iff [simp]: "0 dvd a \<longleftrightarrow> a = 0"
-  by (auto intro: dvd_refl elim!: dvdE)
+  by auto
 
 lemma dvd_0_right [iff]: "a dvd 0"
 proof
   show "0 = a * 0" by simp
 qed

 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult
 begin
 
 subclass ring_1 ..
 subclass comm_semiring_1_cancel
-  by unfold_locales (simp add: algebra_simps)
+  by standard (simp add: algebra_simps)
 
 lemma dvd_minus_iff [simp]: "x dvd - y \<longleftrightarrow> x dvd y"
 proof
   assume "x dvd - y"
   then have "x dvd - 1 * - y" by (rule dvd_mult)

 
 subclass semidom ..
 
 subclass ring_1_no_zero_divisors ..
 
-lemma dvd_mult_cancel_right [simp]: "a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b"
+lemma dvd_mult_cancel_right [simp]:
+  "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: ac_simps)
+    by (auto 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
+    by auto
   finally show ?thesis .
 qed
 
-lemma dvd_mult_cancel_left [simp]: "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: 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 .
-qed
+lemma dvd_mult_cancel_left [simp]:
+  "c * a dvd c * b \<longleftrightarrow> c = 0 \<or> a dvd b"
+  using dvd_mult_cancel_right [of a c b] by (simp add: ac_simps)
 
 lemma square_eq_iff: "a * a = b * b \<longleftrightarrow> a = b \<or> a = - b"
 proof
   assume "a * a = b * b"
   then have "(a - b) * (a + b) = 0"

   case True
   with assms show ?thesis by simp
 next
   case False
   moreover from assms obtain k l where "b = a * k" and "c = a * l"
-    by (auto elim!: dvdE)
+    by blast
   ultimately show ?thesis by simp
 qed
 
 lemma div_add [simp]:
   assumes "c dvd a" and "c dvd b"

   case True
   then show ?thesis by simp
 next
   case False
   moreover from assms obtain k l where "a = c * k" and "b = c * l"
-    by (auto elim!: dvdE)
+    by blast
   moreover have "c * k + c * l = c * (k + l)"
     by (simp add: algebra_simps)
   ultimately show ?thesis
     by simp
 qed

   case True
   with assms show ?thesis by auto
 next
   case False
   moreover from assms obtain k l where "a = b * k" and "c = d * l"
-    by (auto elim!: dvdE)
+    by blast
   moreover have "b * k * (d * l) div (b * d) = (b * d) * (k * l) div (b * d)"
     by (simp add: ac_simps)
   ultimately show ?thesis by simp
 qed
 

   then show ?lhs by (simp add: assms)
 next
   assume ?lhs
   then have "b div a * a = c * a" by simp
   moreover from assms have "b div a * a = b"
-    by (auto elim!: dvdE simp add: ac_simps)
+    by (auto simp add: ac_simps)
   ultimately show ?rhs by simp
 qed
 
 lemma dvd_div_mult_self [simp]: "a dvd b \<Longrightarrow> b div a * a = b"
-  by (cases "a = 0") (auto elim: dvdE simp add: ac_simps)
+  by (cases "a = 0") (auto simp add: ac_simps)
 
 lemma dvd_mult_div_cancel [simp]: "a dvd b \<Longrightarrow> a * (b div a) = b"
   using dvd_div_mult_self [of a b] by (simp add: ac_simps)
 
 lemma div_mult_swap:

   then show ?thesis
     by auto
 next
   case False
   from assms obtain r s where "b = c * r" and "a = c * r * s"
-    by (blast elim: dvdE)
+    by blast
   moreover with False have "r \<noteq> 0"
     by auto
   ultimately show ?thesis using False
     by simp (simp add: mult.commute [of _ r] mult.assoc mult.commute [of c])
 qed

     by auto
 next
   case False
   from assms obtain r s
     where "a = d * r * s" and "b = d * r"
-    by (blast elim: dvdE)
+    by blast
   with False show ?thesis
     by simp (simp add: ac_simps)
 qed