# HG changeset patch
# User wenzelm
# Date 1427661498 -7200
# Node ID c5c4a936357acdb45e2dbe5891a06af5c4e8e948
# Parent  ab828c2c5d6759d6f2674fb25cf28f97363516d3# Parent  c7b7bca8592cf84846198346f5a37162ceeb7b23
merged

diff -r c7b7bca8592c -r c5c4a936357a src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sun Mar 29 21:58:10 2015 +0200
+++ b/src/HOL/Divides.thy	Sun Mar 29 22:38:18 2015 +0200
@@ -18,7 +18,7 @@
 
 subsection {* Abstract division in commutative semirings. *}
 
-class semiring_div = comm_semiring_1_cancel + no_zero_divisors + div +
+class semiring_div = semidom + div +
   assumes mod_div_equality: "a div b * b + a mod b = a"
     and div_by_0 [simp]: "a div 0 = 0"
     and div_0 [simp]: "0 div a = 0"
@@ -445,10 +445,10 @@
 
 end
 
-class ring_div = semiring_div + comm_ring_1
+class ring_div = comm_ring_1 + semiring_div
 begin
 
-subclass ring_1_no_zero_divisors ..
+subclass idom ..
 
 text {* Negation respects modular equivalence. *}
 
@@ -548,7 +548,7 @@
 
 subsubsection {* Parity and division *}
 
-class semiring_div_parity = comm_semiring_1_diff_distrib + numeral + semiring_div +
+class semiring_div_parity = semiring_div + comm_semiring_1_diff_distrib + numeral + 
   assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
   assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1"
   assumes zero_not_eq_two: "0 \<noteq> 2"
@@ -638,7 +638,7 @@
   and less technical class hierarchy.
 *}
 
-class semiring_numeral_div = comm_semiring_1_diff_distrib + linordered_semidom + semiring_div +
+class semiring_numeral_div = semiring_div + comm_semiring_1_diff_distrib + linordered_semidom +
   assumes le_add_diff_inverse2: "b \<le> a \<Longrightarrow> a - b + b = a"
   assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
     and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
@@ -2849,4 +2849,3 @@
   code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
 
 end
-
diff -r c7b7bca8592c -r c5c4a936357a src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Sun Mar 29 21:58:10 2015 +0200
+++ b/src/HOL/Groups_Big.thy	Sun Mar 29 22:38:18 2015 +0200
@@ -1150,7 +1150,7 @@
 
 lemma setprod_zero_iff [simp]:
   assumes "finite A"
-  shows "setprod f A = (0::'a::{comm_semiring_1,no_zero_divisors}) \<longleftrightarrow> (\<exists>a\<in>A. f a = 0)"
+  shows "setprod f A = (0::'a::semidom) \<longleftrightarrow> (\<exists>a\<in>A. f a = 0)"
   using assms by (induct A) (auto simp: no_zero_divisors)
 
 lemma (in field) setprod_diff1:
diff -r c7b7bca8592c -r c5c4a936357a src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Sun Mar 29 21:58:10 2015 +0200
+++ b/src/HOL/NSA/StarDef.thy	Sun Mar 29 22:38:18 2015 +0200
@@ -853,7 +853,7 @@
 instance star :: (comm_semiring_1_diff_distrib) comm_semiring_1_diff_distrib
 by intro_classes (transfer, fact right_diff_distrib')
 
-instance star :: (no_zero_divisors) no_zero_divisors
+instance star :: (semiring_no_zero_divisors) semiring_no_zero_divisors
 by (intro_classes, transfer, rule no_zero_divisors)
 
 instance star :: (semiring_1_cancel) semiring_1_cancel ..
@@ -862,7 +862,7 @@
 instance star :: (comm_ring) comm_ring ..
 instance star :: (ring_1) ring_1 ..
 instance star :: (comm_ring_1) comm_ring_1 ..
-instance star :: (semiring_no_zero_divisors) semiring_no_zero_divisors ..
+instance star :: (semidom) semidom ..
 instance star :: (semiring_div) semiring_div
 apply intro_classes
 apply(transfer, rule mod_div_equality)
diff -r c7b7bca8592c -r c5c4a936357a src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sun Mar 29 21:58:10 2015 +0200
+++ b/src/HOL/Nat.thy	Sun Mar 29 22:38:18 2015 +0200
@@ -783,18 +783,13 @@
 apply (simp_all add: add_less_mono)
 done
 
-text{*The naturals form an ordered @{text comm_semiring_1_cancel}*}
+text{*The naturals form an ordered @{text semidom}*}
 instance nat :: linordered_semidom
 proof
   show "0 < (1::nat)" by simp
   show "\<And>m n q :: nat. m \<le> n \<Longrightarrow> q + m \<le> q + n" by simp
   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 :: semiring_no_zero_divisors
-proof
-  fix m n :: nat
-  show "m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> m * n \<noteq> 0" by simp
+  show "\<And>m n :: nat. m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> m * n \<noteq> 0" by simp
 qed
 
 
diff -r c7b7bca8592c -r c5c4a936357a src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Sun Mar 29 21:58:10 2015 +0200
+++ b/src/HOL/Rings.thy	Sun Mar 29 22:38:18 2015 +0200
@@ -197,7 +197,6 @@
 end
 
 class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult
-  (*previously almost_semiring*)
 begin
 
 subclass semiring_1 ..
@@ -228,22 +227,6 @@
 
 end
 
-class no_zero_divisors = zero + times +
-  assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
-begin
-
-lemma divisors_zero:
-  assumes "a * b = 0"
-  shows "a = 0 \<or> b = 0"
-proof (rule classical)
-  assume "\<not> (a = 0 \<or> b = 0)"
-  then have "a \<noteq> 0" and "b \<noteq> 0" by auto
-  with no_zero_divisors have "a * b \<noteq> 0" by blast
-  with assms show ?thesis by simp
-qed
-
-end
-
 class semiring_1_cancel = semiring + cancel_comm_monoid_add
   + zero_neq_one + monoid_mult
 begin
@@ -394,7 +377,6 @@
 end
 
 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult
-  (*previously ring*)
 begin
 
 subclass ring_1 ..
@@ -433,9 +415,20 @@
 
 end
 
-class semiring_no_zero_divisors = semiring_0 + no_zero_divisors
+class semiring_no_zero_divisors = semiring_0 +
+  assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
 begin
 
+lemma divisors_zero:
+  assumes "a * b = 0"
+  shows "a = 0 \<or> b = 0"
+proof (rule classical)
+  assume "\<not> (a = 0 \<or> b = 0)"
+  then have "a \<noteq> 0" and "b \<noteq> 0" by auto
+  with no_zero_divisors have "a * b \<noteq> 0" by blast
+  with assms show ?thesis by simp
+qed
+
 lemma mult_eq_0_iff [simp]:
   shows "a * b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
 proof (cases "a = 0 \<or> b = 0")
@@ -509,23 +502,15 @@
 
 end
 
-class idom = comm_ring_1 + no_zero_divisors
+class semidom = comm_semiring_1_cancel + semiring_no_zero_divisors
+
+class idom = comm_ring_1 + semiring_no_zero_divisors
 begin
 
+subclass semidom ..
+
 subclass ring_1_no_zero_divisors ..
 
-lemma square_eq_iff: "a * a = b * b \<longleftrightarrow> (a = b \<or> a = - b)"
-proof
-  assume "a * a = b * b"
-  then have "(a - b) * (a + b) = 0"
-    by (simp add: algebra_simps)
-  then show "a = b \<or> a = - b"
-    by (simp add: eq_neg_iff_add_eq_0)
-next
-  assume "a = b \<or> a = - b"
-  then show "a * a = b * b" by auto
-qed
-
 lemma dvd_mult_cancel_right [simp]:
   "a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b"
 proof -
@@ -546,6 +531,18 @@
   finally show ?thesis .
 qed
 
+lemma square_eq_iff: "a * a = b * b \<longleftrightarrow> (a = b \<or> a = - b)"
+proof
+  assume "a * a = b * b"
+  then have "(a - b) * (a + b) = 0"
+    by (simp add: algebra_simps)
+  then show "a = b \<or> a = - b"
+    by (simp add: eq_neg_iff_add_eq_0)
+next
+  assume "a = b \<or> a = - b"
+  then show "a * a = b * b" by auto
+qed
+
 end
 
 text {*
@@ -857,9 +854,6 @@
 
 end
 
-(* The "strict" suffix can be seen as describing the combination of linordered_ring and no_zero_divisors.
-   Basically, linordered_ring + no_zero_divisors = linordered_ring_strict.
- *)
 class linordered_ring_strict = ring + linordered_semiring_strict
   + ordered_ab_group_add + abs_if
 begin
@@ -1005,8 +999,7 @@
 
 end
 
-class linordered_semidom = comm_semiring_1_cancel + linordered_comm_semiring_strict +
-  (*previously linordered_semiring*)
+class linordered_semidom = semidom + linordered_comm_semiring_strict +
   assumes zero_less_one [simp]: "0 < 1"
 begin
 
@@ -1040,7 +1033,6 @@
 class linordered_idom = comm_ring_1 +
   linordered_comm_semiring_strict + ordered_ab_group_add +
   abs_if + sgn_if
-  (*previously linordered_ring*)
 begin
 
 subclass linordered_semiring_1_strict ..
@@ -1206,7 +1198,7 @@
 
 lemma mult_right_le_one_le:
   "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> x * y \<le> x"
-  by (auto simp add: mult_le_cancel_left2)
+  by (rule mult_left_le)
 
 lemma mult_left_le_one_le:
   "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> y * x \<le> x"