diff -r 484559628038 -r 0826b7025d07 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Fri Jun 19 15:55:22 2015 +0200
+++ b/src/HOL/Rings.thy	Fri Jun 19 07:53:33 2015 +0200
@@ -440,26 +440,11 @@
 
 end
 
-class ring_no_zero_divisors = ring + semiring_no_zero_divisors
+class semiring_no_zero_divisors_cancel = semiring_no_zero_divisors +
+  assumes mult_cancel_right [simp]: "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
+    and mult_cancel_left [simp]: "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
 begin
 
-text{*Cancellation of equalities with a common factor*}
-lemma mult_cancel_right [simp]:
-  "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
-proof -
-  have "(a * c = b * c) = ((a - b) * c = 0)"
-    by (simp add: algebra_simps)
-  thus ?thesis by (simp add: disj_commute)
-qed
-
-lemma mult_cancel_left [simp]:
-  "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
-proof -
-  have "(c * a = c * b) = (c * (a - b) = 0)"
-    by (simp add: algebra_simps)
-  thus ?thesis by simp
-qed
-
 lemma mult_left_cancel:
   "c \<noteq> 0 \<Longrightarrow> c * a = c * b \<longleftrightarrow> a = b"
   by simp 
@@ -470,6 +455,26 @@
 
 end
 
+class ring_no_zero_divisors = ring + semiring_no_zero_divisors
+begin
+
+subclass semiring_no_zero_divisors_cancel
+proof
+  fix a b c
+  have "a * c = b * c \<longleftrightarrow> (a - b) * c = 0"
+    by (simp add: algebra_simps)
+  also have "\<dots> \<longleftrightarrow> c = 0 \<or> a = b"
+    by auto
+  finally show "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b" .
+  have "c * a = c * b \<longleftrightarrow> c * (a - b) = 0"
+    by (simp add: algebra_simps)
+  also have "\<dots> \<longleftrightarrow> c = 0 \<or> a = b"
+    by auto
+  finally show "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b" .
+qed
+
+end
+
 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
 begin
 
@@ -531,7 +536,7 @@
   finally show ?thesis .
 qed
 
-lemma square_eq_iff: "a * a = b * b \<longleftrightarrow> (a = b \<or> a = - b)"
+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"
@@ -594,6 +599,33 @@
   "a \<noteq> 0 \<Longrightarrow> (a * b) div a = b"
   using nonzero_mult_divide_cancel_right [of a b] by (simp add: ac_simps)
 
+subclass semiring_no_zero_divisors_cancel
+proof
+  fix a b c
+  { fix a b c
+    show "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
+    proof (cases "c = 0")
+      case True then show ?thesis by simp
+    next
+      case False
+      { assume "a * c = b * c"
+        then have "a * c div c = b * c div c"
+          by simp
+        with False have "a = b"
+          by simp
+      } then show ?thesis by auto
+    qed
+  }
+  from this [of a c b]
+  show "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
+    by (simp add: ac_simps)
+qed
+
+lemma div_self [simp]:
+  assumes "a \<noteq> 0"
+  shows "a div a = 1"
+  using assms nonzero_mult_divide_cancel_left [of a 1] by simp
+
 end
 
 class idom_divide = idom + semidom_divide