# HG changeset patch
# User haftmann
# Date 1415462006 -3600
# Node ID 5d82cdef6c1b95039a37f0402db1e1566e8e8db8
# Parent  8b7caf447357f072adb5875f67d2d0663e0aadf9
equivalence rules for structures without zero divisors

diff -r 8b7caf447357 -r 5d82cdef6c1b src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sat Nov 08 22:10:16 2014 +0100
+++ b/src/HOL/Nat.thy	Sat Nov 08 16:53:26 2014 +0100
@@ -785,9 +785,10 @@
   show "\<And>m n q :: nat. m < n \<Longrightarrow> 0 < q \<Longrightarrow> q * m < q * n" by (simp add: mult_less_mono2)
 qed
 
-instance nat :: no_zero_divisors
+instance nat :: semiring_no_zero_divisors
 proof
-  fix a::nat and b::nat show "a ~= 0 \<Longrightarrow> b ~= 0 \<Longrightarrow> a * b ~= 0" by auto
+  fix m n :: nat
+  show "m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> m * n \<noteq> 0" by simp
 qed
 
 
diff -r 8b7caf447357 -r 5d82cdef6c1b src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Sat Nov 08 22:10:16 2014 +0100
+++ b/src/HOL/Rings.thy	Sat Nov 08 16:53:26 2014 +0100
@@ -405,11 +405,11 @@
 
 end
 
-class ring_no_zero_divisors = ring + no_zero_divisors
+class semiring_no_zero_divisors = semiring_0 + no_zero_divisors
 begin
 
 lemma mult_eq_0_iff [simp]:
-  shows "a * b = 0 \<longleftrightarrow> (a = 0 \<or> b = 0)"
+  shows "a * b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
 proof (cases "a = 0 \<or> b = 0")
   case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto
     then show ?thesis using no_zero_divisors by simp
@@ -417,6 +417,11 @@
   case True then show ?thesis by auto
 qed
 
+end
+
+class ring_no_zero_divisors = ring + semiring_no_zero_divisors
+begin
+
 text{*Cancellation of equalities with a common factor*}
 lemma mult_cancel_right [simp]:
   "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
@@ -434,11 +439,13 @@
   thus ?thesis by simp
 qed
 
-lemma mult_left_cancel: "c \<noteq> 0 \<Longrightarrow> (c*a=c*b) = (a=b)"
-by simp 
+lemma mult_left_cancel:
+  "c \<noteq> 0 \<Longrightarrow> c * a = c * b \<longleftrightarrow> a = b"
+  by simp 
 
-lemma mult_right_cancel: "c \<noteq> 0 \<Longrightarrow> (a*c=b*c) = (a=b)"
-by simp 
+lemma mult_right_cancel:
+  "c \<noteq> 0 \<Longrightarrow> a * c = b * c \<longleftrightarrow> a = b"
+  by simp 
 
 end