--- 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
--- 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