clarified no_zero_devisors: makes only sense in a semiring;
authorhaftmann
Sat Mar 28 21:32:48 2015 +0100 (2015-03-28)
changeset 59833ab828c2c5d67
parent 59832 d5ccdca16cca
child 59847 c5c4a936357a
clarified no_zero_devisors: makes only sense in a semiring;
actually turn linorder_semidom into a integral domain
src/HOL/Divides.thy
src/HOL/Groups_Big.thy
src/HOL/NSA/StarDef.thy
src/HOL/Nat.thy
src/HOL/Rings.thy
     1.1 --- a/src/HOL/Divides.thy	Sat Mar 28 20:43:19 2015 +0100
     1.2 +++ b/src/HOL/Divides.thy	Sat Mar 28 21:32:48 2015 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4  
     1.5  subsection {* Abstract division in commutative semirings. *}
     1.6  
     1.7 -class semiring_div = comm_semiring_1_cancel + no_zero_divisors + div +
     1.8 +class semiring_div = semidom + div +
     1.9    assumes mod_div_equality: "a div b * b + a mod b = a"
    1.10      and div_by_0 [simp]: "a div 0 = 0"
    1.11      and div_0 [simp]: "0 div a = 0"
    1.12 @@ -445,10 +445,10 @@
    1.13  
    1.14  end
    1.15  
    1.16 -class ring_div = semiring_div + comm_ring_1
    1.17 +class ring_div = comm_ring_1 + semiring_div
    1.18  begin
    1.19  
    1.20 -subclass ring_1_no_zero_divisors ..
    1.21 +subclass idom ..
    1.22  
    1.23  text {* Negation respects modular equivalence. *}
    1.24  
    1.25 @@ -548,7 +548,7 @@
    1.26  
    1.27  subsubsection {* Parity and division *}
    1.28  
    1.29 -class semiring_div_parity = comm_semiring_1_diff_distrib + numeral + semiring_div +
    1.30 +class semiring_div_parity = semiring_div + comm_semiring_1_diff_distrib + numeral + 
    1.31    assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
    1.32    assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1"
    1.33    assumes zero_not_eq_two: "0 \<noteq> 2"
    1.34 @@ -638,7 +638,7 @@
    1.35    and less technical class hierarchy.
    1.36  *}
    1.37  
    1.38 -class semiring_numeral_div = comm_semiring_1_diff_distrib + linordered_semidom + semiring_div +
    1.39 +class semiring_numeral_div = semiring_div + comm_semiring_1_diff_distrib + linordered_semidom +
    1.40    assumes le_add_diff_inverse2: "b \<le> a \<Longrightarrow> a - b + b = a"
    1.41    assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
    1.42      and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
    1.43 @@ -2849,4 +2849,3 @@
    1.44    code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
    1.45  
    1.46  end
    1.47 -
     2.1 --- a/src/HOL/Groups_Big.thy	Sat Mar 28 20:43:19 2015 +0100
     2.2 +++ b/src/HOL/Groups_Big.thy	Sat Mar 28 21:32:48 2015 +0100
     2.3 @@ -1150,7 +1150,7 @@
     2.4  
     2.5  lemma setprod_zero_iff [simp]:
     2.6    assumes "finite A"
     2.7 -  shows "setprod f A = (0::'a::{comm_semiring_1,no_zero_divisors}) \<longleftrightarrow> (\<exists>a\<in>A. f a = 0)"
     2.8 +  shows "setprod f A = (0::'a::semidom) \<longleftrightarrow> (\<exists>a\<in>A. f a = 0)"
     2.9    using assms by (induct A) (auto simp: no_zero_divisors)
    2.10  
    2.11  lemma (in field) setprod_diff1:
     3.1 --- a/src/HOL/NSA/StarDef.thy	Sat Mar 28 20:43:19 2015 +0100
     3.2 +++ b/src/HOL/NSA/StarDef.thy	Sat Mar 28 21:32:48 2015 +0100
     3.3 @@ -853,7 +853,7 @@
     3.4  instance star :: (comm_semiring_1_diff_distrib) comm_semiring_1_diff_distrib
     3.5  by intro_classes (transfer, fact right_diff_distrib')
     3.6  
     3.7 -instance star :: (no_zero_divisors) no_zero_divisors
     3.8 +instance star :: (semiring_no_zero_divisors) semiring_no_zero_divisors
     3.9  by (intro_classes, transfer, rule no_zero_divisors)
    3.10  
    3.11  instance star :: (semiring_1_cancel) semiring_1_cancel ..
    3.12 @@ -862,7 +862,7 @@
    3.13  instance star :: (comm_ring) comm_ring ..
    3.14  instance star :: (ring_1) ring_1 ..
    3.15  instance star :: (comm_ring_1) comm_ring_1 ..
    3.16 -instance star :: (semiring_no_zero_divisors) semiring_no_zero_divisors ..
    3.17 +instance star :: (semidom) semidom ..
    3.18  instance star :: (semiring_div) semiring_div
    3.19  apply intro_classes
    3.20  apply(transfer, rule mod_div_equality)
     4.1 --- a/src/HOL/Nat.thy	Sat Mar 28 20:43:19 2015 +0100
     4.2 +++ b/src/HOL/Nat.thy	Sat Mar 28 21:32:48 2015 +0100
     4.3 @@ -783,18 +783,13 @@
     4.4  apply (simp_all add: add_less_mono)
     4.5  done
     4.6  
     4.7 -text{*The naturals form an ordered @{text comm_semiring_1_cancel}*}
     4.8 +text{*The naturals form an ordered @{text semidom}*}
     4.9  instance nat :: linordered_semidom
    4.10  proof
    4.11    show "0 < (1::nat)" by simp
    4.12    show "\<And>m n q :: nat. m \<le> n \<Longrightarrow> q + m \<le> q + n" by simp
    4.13    show "\<And>m n q :: nat. m < n \<Longrightarrow> 0 < q \<Longrightarrow> q * m < q * n" by (simp add: mult_less_mono2)
    4.14 -qed
    4.15 -
    4.16 -instance nat :: semiring_no_zero_divisors
    4.17 -proof
    4.18 -  fix m n :: nat
    4.19 -  show "m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> m * n \<noteq> 0" by simp
    4.20 +  show "\<And>m n :: nat. m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> m * n \<noteq> 0" by simp
    4.21  qed
    4.22  
    4.23  
     5.1 --- a/src/HOL/Rings.thy	Sat Mar 28 20:43:19 2015 +0100
     5.2 +++ b/src/HOL/Rings.thy	Sat Mar 28 21:32:48 2015 +0100
     5.3 @@ -227,22 +227,6 @@
     5.4  
     5.5  end
     5.6  
     5.7 -class no_zero_divisors = zero + times +
     5.8 -  assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
     5.9 -begin
    5.10 -
    5.11 -lemma divisors_zero:
    5.12 -  assumes "a * b = 0"
    5.13 -  shows "a = 0 \<or> b = 0"
    5.14 -proof (rule classical)
    5.15 -  assume "\<not> (a = 0 \<or> b = 0)"
    5.16 -  then have "a \<noteq> 0" and "b \<noteq> 0" by auto
    5.17 -  with no_zero_divisors have "a * b \<noteq> 0" by blast
    5.18 -  with assms show ?thesis by simp
    5.19 -qed
    5.20 -
    5.21 -end
    5.22 -
    5.23  class semiring_1_cancel = semiring + cancel_comm_monoid_add
    5.24    + zero_neq_one + monoid_mult
    5.25  begin
    5.26 @@ -431,9 +415,20 @@
    5.27  
    5.28  end
    5.29  
    5.30 -class semiring_no_zero_divisors = semiring_0 + no_zero_divisors
    5.31 +class semiring_no_zero_divisors = semiring_0 +
    5.32 +  assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
    5.33  begin
    5.34  
    5.35 +lemma divisors_zero:
    5.36 +  assumes "a * b = 0"
    5.37 +  shows "a = 0 \<or> b = 0"
    5.38 +proof (rule classical)
    5.39 +  assume "\<not> (a = 0 \<or> b = 0)"
    5.40 +  then have "a \<noteq> 0" and "b \<noteq> 0" by auto
    5.41 +  with no_zero_divisors have "a * b \<noteq> 0" by blast
    5.42 +  with assms show ?thesis by simp
    5.43 +qed
    5.44 +
    5.45  lemma mult_eq_0_iff [simp]:
    5.46    shows "a * b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
    5.47  proof (cases "a = 0 \<or> b = 0")
    5.48 @@ -507,23 +502,15 @@
    5.49  
    5.50  end
    5.51  
    5.52 -class idom = comm_ring_1 + no_zero_divisors
    5.53 +class semidom = comm_semiring_1_cancel + semiring_no_zero_divisors
    5.54 +
    5.55 +class idom = comm_ring_1 + semiring_no_zero_divisors
    5.56  begin
    5.57  
    5.58 +subclass semidom ..
    5.59 +
    5.60  subclass ring_1_no_zero_divisors ..
    5.61  
    5.62 -lemma square_eq_iff: "a * a = b * b \<longleftrightarrow> (a = b \<or> a = - b)"
    5.63 -proof
    5.64 -  assume "a * a = b * b"
    5.65 -  then have "(a - b) * (a + b) = 0"
    5.66 -    by (simp add: algebra_simps)
    5.67 -  then show "a = b \<or> a = - b"
    5.68 -    by (simp add: eq_neg_iff_add_eq_0)
    5.69 -next
    5.70 -  assume "a = b \<or> a = - b"
    5.71 -  then show "a * a = b * b" by auto
    5.72 -qed
    5.73 -
    5.74  lemma dvd_mult_cancel_right [simp]:
    5.75    "a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b"
    5.76  proof -
    5.77 @@ -544,6 +531,18 @@
    5.78    finally show ?thesis .
    5.79  qed
    5.80  
    5.81 +lemma square_eq_iff: "a * a = b * b \<longleftrightarrow> (a = b \<or> a = - b)"
    5.82 +proof
    5.83 +  assume "a * a = b * b"
    5.84 +  then have "(a - b) * (a + b) = 0"
    5.85 +    by (simp add: algebra_simps)
    5.86 +  then show "a = b \<or> a = - b"
    5.87 +    by (simp add: eq_neg_iff_add_eq_0)
    5.88 +next
    5.89 +  assume "a = b \<or> a = - b"
    5.90 +  then show "a * a = b * b" by auto
    5.91 +qed
    5.92 +
    5.93  end
    5.94  
    5.95  text {*
    5.96 @@ -1000,7 +999,7 @@
    5.97  
    5.98  end
    5.99  
   5.100 -class linordered_semidom = comm_semiring_1_cancel + linordered_comm_semiring_strict +
   5.101 +class linordered_semidom = semidom + linordered_comm_semiring_strict +
   5.102    assumes zero_less_one [simp]: "0 < 1"
   5.103  begin
   5.104  
   5.105 @@ -1199,7 +1198,7 @@
   5.106  
   5.107  lemma mult_right_le_one_le:
   5.108    "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> x * y \<le> x"
   5.109 -  by (auto simp add: mult_le_cancel_left2)
   5.110 +  by (rule mult_left_le)
   5.111  
   5.112  lemma mult_left_le_one_le:
   5.113    "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> y * x \<le> x"