src/HOL/Rings.thy

   "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
   using dvd_add [of x y "- z"] by simp
 
 end
 
-class divide =
-  fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
-
-setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
-
-context semiring
-begin
-
-lemma [field_simps]:
-  shows distrib_left_NO_MATCH: "NO_MATCH (divide x y) a \<Longrightarrow> a * (b + c) = a * b + a * c"
-    and distrib_right_NO_MATCH: "NO_MATCH (divide x y) c \<Longrightarrow> (a + b) * c = a * c + b * c"
-  by (rule distrib_left distrib_right)+
-
-end
-
-context ring
-begin
-
-lemma [field_simps]:
-  shows left_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) c \<Longrightarrow> (a - b) * c = a * c - b * c"
-    and right_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) a \<Longrightarrow> a * (b - c) = a * b - a * c"
-  by (rule left_diff_distrib right_diff_distrib)+
-
-end
-
-setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
-  
 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:

   \begin{itemize}
   \item @{url "http://www.mathworld.com"} by Eric Weisstein et. al.
   \item \emph{Algebra I} by van der Waerden, Springer.
   \end{itemize}
 *}
+
+class divide =
+  fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+
+setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
+
+context semiring
+begin
+
+lemma [field_simps]:
+  shows distrib_left_NO_MATCH: "NO_MATCH (divide x y) a \<Longrightarrow> a * (b + c) = a * b + a * c"
+    and distrib_right_NO_MATCH: "NO_MATCH (divide x y) c \<Longrightarrow> (a + b) * c = a * c + b * c"
+  by (rule distrib_left distrib_right)+
+
+end
+
+context ring
+begin
+
+lemma [field_simps]:
+  shows left_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) c \<Longrightarrow> (a - b) * c = a * c - b * c"
+    and right_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) a \<Longrightarrow> a * (b - c) = a * b - a * c"
+  by (rule left_diff_distrib right_diff_distrib)+
+
+end
+
+setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
+
+class semidom_divide = semidom + divide +
+  assumes nonzero_mult_divide_cancel_right [simp]: "b \<noteq> 0 \<Longrightarrow> divide (a * b) b = a"
+  assumes divide_zero [simp]: "divide a 0 = 0"
+begin
+
+lemma nonzero_mult_divide_cancel_left [simp]:
+  "a \<noteq> 0 \<Longrightarrow> divide (a * b) a = b"
+  using nonzero_mult_divide_cancel_right [of a b] by (simp add: ac_simps)
+
+end
+
+class idom_divide = idom + semidom_divide
 
 class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add +
   assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
   assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
 begin