equivalence rules for structures without zero divisors
authorhaftmann
Sat Nov 08 16:53:26 2014 +0100 (2014-11-08)
changeset 589525d82cdef6c1b
parent 58951 8b7caf447357
child 58953 2e19b392d9e3
equivalence rules for structures without zero divisors
src/HOL/Nat.thy
src/HOL/Rings.thy
     1.1 --- a/src/HOL/Nat.thy	Sat Nov 08 22:10:16 2014 +0100
     1.2 +++ b/src/HOL/Nat.thy	Sat Nov 08 16:53:26 2014 +0100
     1.3 @@ -785,9 +785,10 @@
     1.4    show "\<And>m n q :: nat. m < n \<Longrightarrow> 0 < q \<Longrightarrow> q * m < q * n" by (simp add: mult_less_mono2)
     1.5  qed
     1.6  
     1.7 -instance nat :: no_zero_divisors
     1.8 +instance nat :: semiring_no_zero_divisors
     1.9  proof
    1.10 -  fix a::nat and b::nat show "a ~= 0 \<Longrightarrow> b ~= 0 \<Longrightarrow> a * b ~= 0" by auto
    1.11 +  fix m n :: nat
    1.12 +  show "m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> m * n \<noteq> 0" by simp
    1.13  qed
    1.14  
    1.15  
     2.1 --- a/src/HOL/Rings.thy	Sat Nov 08 22:10:16 2014 +0100
     2.2 +++ b/src/HOL/Rings.thy	Sat Nov 08 16:53:26 2014 +0100
     2.3 @@ -405,11 +405,11 @@
     2.4  
     2.5  end
     2.6  
     2.7 -class ring_no_zero_divisors = ring + no_zero_divisors
     2.8 +class semiring_no_zero_divisors = semiring_0 + no_zero_divisors
     2.9  begin
    2.10  
    2.11  lemma mult_eq_0_iff [simp]:
    2.12 -  shows "a * b = 0 \<longleftrightarrow> (a = 0 \<or> b = 0)"
    2.13 +  shows "a * b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
    2.14  proof (cases "a = 0 \<or> b = 0")
    2.15    case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto
    2.16      then show ?thesis using no_zero_divisors by simp
    2.17 @@ -417,6 +417,11 @@
    2.18    case True then show ?thesis by auto
    2.19  qed
    2.20  
    2.21 +end
    2.22 +
    2.23 +class ring_no_zero_divisors = ring + semiring_no_zero_divisors
    2.24 +begin
    2.25 +
    2.26  text{*Cancellation of equalities with a common factor*}
    2.27  lemma mult_cancel_right [simp]:
    2.28    "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
    2.29 @@ -434,11 +439,13 @@
    2.30    thus ?thesis by simp
    2.31  qed
    2.32  
    2.33 -lemma mult_left_cancel: "c \<noteq> 0 \<Longrightarrow> (c*a=c*b) = (a=b)"
    2.34 -by simp 
    2.35 +lemma mult_left_cancel:
    2.36 +  "c \<noteq> 0 \<Longrightarrow> c * a = c * b \<longleftrightarrow> a = b"
    2.37 +  by simp 
    2.38  
    2.39 -lemma mult_right_cancel: "c \<noteq> 0 \<Longrightarrow> (a*c=b*c) = (a=b)"
    2.40 -by simp 
    2.41 +lemma mult_right_cancel:
    2.42 +  "c \<noteq> 0 \<Longrightarrow> a * c = b * c \<longleftrightarrow> a = b"
    2.43 +  by simp 
    2.44  
    2.45  end
    2.46