clarified no_zero_devisors: makes only sense in a semiring;
actually turn linorder_semidom into a integral domain

--- a/src/HOL/Divides.thy	Sat Mar 28 20:43:19 2015 +0100
+++ b/src/HOL/Divides.thy	Sat Mar 28 21:32:48 2015 +0100
@@ -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
-

--- a/src/HOL/Groups_Big.thy	Sat Mar 28 20:43:19 2015 +0100
+++ b/src/HOL/Groups_Big.thy	Sat Mar 28 21:32:48 2015 +0100
@@ -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:

--- a/src/HOL/NSA/StarDef.thy	Sat Mar 28 20:43:19 2015 +0100
+++ b/src/HOL/NSA/StarDef.thy	Sat Mar 28 21:32:48 2015 +0100
@@ -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)

--- a/src/HOL/Nat.thy	Sat Mar 28 20:43:19 2015 +0100
+++ b/src/HOL/Nat.thy	Sat Mar 28 21:32:48 2015 +0100
@@ -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
 
 

--- a/src/HOL/Rings.thy	Sat Mar 28 20:43:19 2015 +0100
+++ b/src/HOL/Rings.thy	Sat Mar 28 21:32:48 2015 +0100
@@ -227,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
@@ -431,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")
@@ -507,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 -
@@ -544,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 {*
@@ -1000,7 +999,7 @@
 
 end
 
-class linordered_semidom = comm_semiring_1_cancel + linordered_comm_semiring_strict +
+class linordered_semidom = semidom + linordered_comm_semiring_strict +
   assumes zero_less_one [simp]: "0 < 1"
 begin
 
@@ -1199,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"