src/HOL/Rings.thy
 changeset 59833 ab828c2c5d67 parent 59832 d5ccdca16cca child 59865 8a20dd967385
```     1.1 --- a/src/HOL/Rings.thy	Sat Mar 28 20:43:19 2015 +0100
1.2 +++ b/src/HOL/Rings.thy	Sat Mar 28 21:32:48 2015 +0100
1.3 @@ -227,22 +227,6 @@
1.4
1.5  end
1.6
1.7 -class no_zero_divisors = zero + times +
1.8 -  assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
1.9 -begin
1.10 -
1.11 -lemma divisors_zero:
1.12 -  assumes "a * b = 0"
1.13 -  shows "a = 0 \<or> b = 0"
1.14 -proof (rule classical)
1.15 -  assume "\<not> (a = 0 \<or> b = 0)"
1.16 -  then have "a \<noteq> 0" and "b \<noteq> 0" by auto
1.17 -  with no_zero_divisors have "a * b \<noteq> 0" by blast
1.18 -  with assms show ?thesis by simp
1.19 -qed
1.20 -
1.21 -end
1.22 -
1.23  class semiring_1_cancel = semiring + cancel_comm_monoid_add
1.24    + zero_neq_one + monoid_mult
1.25  begin
1.26 @@ -431,9 +415,20 @@
1.27
1.28  end
1.29
1.30 -class semiring_no_zero_divisors = semiring_0 + no_zero_divisors
1.31 +class semiring_no_zero_divisors = semiring_0 +
1.32 +  assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
1.33  begin
1.34
1.35 +lemma divisors_zero:
1.36 +  assumes "a * b = 0"
1.37 +  shows "a = 0 \<or> b = 0"
1.38 +proof (rule classical)
1.39 +  assume "\<not> (a = 0 \<or> b = 0)"
1.40 +  then have "a \<noteq> 0" and "b \<noteq> 0" by auto
1.41 +  with no_zero_divisors have "a * b \<noteq> 0" by blast
1.42 +  with assms show ?thesis by simp
1.43 +qed
1.44 +
1.45  lemma mult_eq_0_iff [simp]:
1.46    shows "a * b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
1.47  proof (cases "a = 0 \<or> b = 0")
1.48 @@ -507,23 +502,15 @@
1.49
1.50  end
1.51
1.52 -class idom = comm_ring_1 + no_zero_divisors
1.53 +class semidom = comm_semiring_1_cancel + semiring_no_zero_divisors
1.54 +
1.55 +class idom = comm_ring_1 + semiring_no_zero_divisors
1.56  begin
1.57
1.58 +subclass semidom ..
1.59 +
1.60  subclass ring_1_no_zero_divisors ..
1.61
1.62 -lemma square_eq_iff: "a * a = b * b \<longleftrightarrow> (a = b \<or> a = - b)"
1.63 -proof
1.64 -  assume "a * a = b * b"
1.65 -  then have "(a - b) * (a + b) = 0"
1.66 -    by (simp add: algebra_simps)
1.67 -  then show "a = b \<or> a = - b"
1.69 -next
1.70 -  assume "a = b \<or> a = - b"
1.71 -  then show "a * a = b * b" by auto
1.72 -qed
1.73 -
1.74  lemma dvd_mult_cancel_right [simp]:
1.75    "a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b"
1.76  proof -
1.77 @@ -544,6 +531,18 @@
1.78    finally show ?thesis .
1.79  qed
1.80
1.81 +lemma square_eq_iff: "a * a = b * b \<longleftrightarrow> (a = b \<or> a = - b)"
1.82 +proof
1.83 +  assume "a * a = b * b"
1.84 +  then have "(a - b) * (a + b) = 0"
1.85 +    by (simp add: algebra_simps)
1.86 +  then show "a = b \<or> a = - b"
1.88 +next
1.89 +  assume "a = b \<or> a = - b"
1.90 +  then show "a * a = b * b" by auto
1.91 +qed
1.92 +
1.93  end
1.94
1.95  text {*
1.96 @@ -1000,7 +999,7 @@
1.97
1.98  end
1.99
1.100 -class linordered_semidom = comm_semiring_1_cancel + linordered_comm_semiring_strict +
1.101 +class linordered_semidom = semidom + linordered_comm_semiring_strict +
1.102    assumes zero_less_one [simp]: "0 < 1"
1.103  begin
1.104
1.105 @@ -1199,7 +1198,7 @@
1.106
1.107  lemma mult_right_le_one_le:
1.108    "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> x * y \<le> x"
1.109 -  by (auto simp add: mult_le_cancel_left2)
1.110 +  by (rule mult_left_le)
1.111
1.112  lemma mult_left_le_one_le:
1.113    "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> y * x \<le> x"
```