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.68 -    by (simp add: eq_neg_iff_add_eq_0)
    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.87 +    by (simp add: eq_neg_iff_add_eq_0)
    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"