author haftmann Sat, 08 Nov 2014 16:53:26 +0100 changeset 58952 5d82cdef6c1b parent 58951 8b7caf447357 child 58953 2e19b392d9e3
equivalence rules for structures without zero divisors
 src/HOL/Nat.thy file | annotate | diff | comparison | revisions src/HOL/Rings.thy file | annotate | diff | comparison | revisions
```--- 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
```