# HG changeset patch
# User haftmann
# Date 1555145013 0
# Node ID 1657688a64060cc78820070186bf5e164897a250
# Parent  9839da71621f6e4dcb925f2d27eba5f4463cd023
backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is

diff -r 9839da71621f -r 1657688a6406 src/HOL/Euclidean_Division.thy
--- a/src/HOL/Euclidean_Division.thy	Sat Apr 13 08:11:48 2019 +0000
+++ b/src/HOL/Euclidean_Division.thy	Sat Apr 13 08:43:33 2019 +0000
@@ -165,31 +165,25 @@
 
 subsection \<open>Euclidean (semi)rings with cancel rules\<close>
 
-class euclidean_semiring_cancel = euclidean_semiring + semidom_divide_cancel
+class euclidean_semiring_cancel = euclidean_semiring +
+  assumes div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
+  and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
 begin
 
-context
-  fixes b
-  assumes "b \<noteq> 0"
-begin
-
-lemma div_mult_self1 [simp]:
-  "(a + c * b) div b = c + a div b"
-  using \<open>b \<noteq> 0\<close> by (rule div_mult_self1)
-
 lemma div_mult_self2 [simp]:
-  "(a + b * c) div b = c + a div b"
-  using \<open>b \<noteq> 0\<close> by (rule div_mult_self2)
+  assumes "b \<noteq> 0"
+  shows "(a + b * c) div b = c + a div b"
+  using assms div_mult_self1 [of b a c] by (simp add: mult.commute)
 
 lemma div_mult_self3 [simp]:
-  "(c * b + a) div b = c + a div b"
-  using \<open>b \<noteq> 0\<close> by (rule div_mult_self3)
+  assumes "b \<noteq> 0"
+  shows "(c * b + a) div b = c + a div b"
+  using assms by (simp add: add.commute)
 
 lemma div_mult_self4 [simp]:
-  "(b * c + a) div b = c + a div b"
-  using \<open>b \<noteq> 0\<close> by (rule div_mult_self4)
-
-end
+  assumes "b \<noteq> 0"
+  shows "(b * c + a) div b = c + a div b"
+  using assms by (simp add: add.commute)
 
 lemma mod_mult_self1 [simp]: "(a + c * b) mod b = a mod b"
 proof (cases "b = 0")
@@ -200,7 +194,7 @@
     by (simp add: div_mult_mod_eq)
   also from False div_mult_self1 [of b a c] have
     "\<dots> = (c + a div b) * b + (a + c * b) mod b"
-    by (simp add: algebra_simps)
+      by (simp add: algebra_simps)
   finally have "a = a div b * b + (a + c * b) mod b"
     by (simp add: add.commute [of a] add.assoc distrib_right)
   then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b"
@@ -228,6 +222,16 @@
   "a * b mod b = 0"
   using mod_mult_self1 [of 0 a b] by simp
 
+lemma div_add_self1:
+  assumes "b \<noteq> 0"
+  shows "(b + a) div b = a div b + 1"
+  using assms div_mult_self1 [of b a 1] by (simp add: add.commute)
+
+lemma div_add_self2:
+  assumes "b \<noteq> 0"
+  shows "(a + b) div b = a div b + 1"
+  using assms div_add_self1 [of b a] by (simp add: add.commute)
+
 lemma mod_add_self1 [simp]:
   "(b + a) mod b = a mod b"
   using mod_mult_self1 [of a 1 b] by (simp add: add.commute)
@@ -280,6 +284,14 @@
   finally show ?thesis .
 qed
 
+lemma div_mult_mult2 [simp]:
+  "c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b"
+  by (drule div_mult_mult1) (simp add: mult.commute)
+
+lemma div_mult_mult1_if [simp]:
+  "(c * a) div (c * b) = (if c = 0 then 0 else a div b)"
+  by simp_all
+
 lemma mod_mult_mult1:
   "(c * a) mod (c * b) = c * (a mod b)"
 proof (cases "c = 0")
@@ -436,14 +448,23 @@
 class euclidean_ring_cancel = euclidean_ring + euclidean_semiring_cancel
 begin
 
-subclass idom_divide_cancel ..
+subclass idom_divide ..
+
+lemma div_minus_minus [simp]: "(- a) div (- b) = a div b"
+  using div_mult_mult1 [of "- 1" a b] by simp
 
 lemma mod_minus_minus [simp]: "(- a) mod (- b) = - (a mod b)"
   using mod_mult_mult1 [of "- 1" a b] by simp
 
+lemma div_minus_right: "a div (- b) = (- a) div b"
+  using div_minus_minus [of "- a" b] by simp
+
 lemma mod_minus_right: "a mod (- b) = - ((- a) mod b)"
   using mod_minus_minus [of "- a" b] by simp
 
+lemma div_minus1_right [simp]: "a div (- 1) = - a"
+  using div_minus_right [of a 1] by simp
+
 lemma mod_minus1_right [simp]: "a mod (- 1) = 0"
   using mod_minus_right [of a 1] by simp
 
diff -r 9839da71621f -r 1657688a6406 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Sat Apr 13 08:11:48 2019 +0000
+++ b/src/HOL/Fields.thy	Sat Apr 13 08:43:33 2019 +0000
@@ -378,42 +378,30 @@
     by (simp add: divide_inverse)
 qed
 
-subclass idom_divide_cancel
-proof
-  fix a b c
-  assume [simp]: "c \<noteq> 0"
-  show "(c * a) / (c * b) = a / b"
-  proof (cases "b = 0")
-    case True then show ?thesis
-      by simp
-  next
-    case False
-    then have "(c * a) / (c * b) = c * a * (inverse b * inverse c)"
-      by (simp add: divide_inverse nonzero_inverse_mult_distrib)
-    also have "... =  a * inverse b * (inverse c * c)"
-      by (simp only: ac_simps)
-    also have "... =  a * inverse b" by simp
-    finally show ?thesis by (simp add: divide_inverse)
-  qed
-next
-  fix a b c
-  assume "b \<noteq> 0"
-  have "((a * inverse b) * b + c * b) = (c + a * inverse b) * b"
-    using distrib [of c "a * inverse b" b] by (simp add: ac_simps)
-  also have "(a * inverse b) * b = a"
-    using \<open>b \<noteq> 0\<close> by (simp add: ac_simps)
-  finally show "(a + c * b) / b = c + a / b"
-    using \<open>b \<noteq> 0\<close> by (simp add: ac_simps divide_inverse [symmetric])
-qed
-
-lemmas nonzero_mult_divide_mult_cancel_left = div_mult_mult1 \<comment> \<open>duplicate\<close>
-lemmas nonzero_mult_divide_mult_cancel_right = div_mult_mult2 \<comment> \<open>duplicate\<close>
-
 text\<open>There is no slick version using division by zero.\<close>
 lemma inverse_add:
   "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a + inverse b = (a + b) * inverse a * inverse b"
   by (simp add: division_ring_inverse_add ac_simps)
 
+lemma nonzero_mult_divide_mult_cancel_left [simp]:
+  assumes [simp]: "c \<noteq> 0"
+  shows "(c * a) / (c * b) = a / b"
+proof (cases "b = 0")
+  case True then show ?thesis by simp
+next
+  case False
+  then have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
+    by (simp add: divide_inverse nonzero_inverse_mult_distrib)
+  also have "... =  a * inverse b * (inverse c * c)"
+    by (simp only: ac_simps)
+  also have "... =  a * inverse b" by simp
+    finally show ?thesis by (simp add: divide_inverse)
+qed
+
+lemma nonzero_mult_divide_mult_cancel_right [simp]:
+  "c \<noteq> 0 \<Longrightarrow> (a * c) / (b * c) = a / b"
+  using nonzero_mult_divide_mult_cancel_left [of c a b] by (simp add: ac_simps)
+
 lemma times_divide_eq_left [simp]: "(b / c) * a = (b * a) / c"
   by (simp add: divide_inverse ac_simps)
 
diff -r 9839da71621f -r 1657688a6406 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Sat Apr 13 08:11:48 2019 +0000
+++ b/src/HOL/Rings.thy	Sat Apr 13 08:43:33 2019 +0000
@@ -780,71 +780,6 @@
 
 end
 
-text \<open>Integral (semi)domains with cancellation rules\<close>
-
-class semidom_divide_cancel = semidom_divide +
-  assumes div_mult_self1: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
-    and div_mult_mult1: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
-begin
-
-context
-  fixes b
-  assumes "b \<noteq> 0"
-begin
-
-lemma div_mult_self2:
-  "(a + b * c) div b = c + a div b"
-  using \<open>b \<noteq> 0\<close> div_mult_self1 [of b a c] by (simp add: ac_simps)
-
-lemma div_mult_self3:
-  "(c * b + a) div b = c + a div b"
-  using \<open>b \<noteq> 0\<close> div_mult_self1 [of b a c] by (simp add: ac_simps)
-
-lemma div_mult_self4:
-  "(b * c + a) div b = c + a div b"
-  using \<open>b \<noteq> 0\<close> div_mult_self1 [of b a c] by (simp add: ac_simps)
-
-lemma div_add_self1:
-  "(b + a) div b = a div b + 1"
-  using \<open>b \<noteq> 0\<close> div_mult_self1 [of b a 1] by (simp add: ac_simps)
-
-lemma div_add_self2:
-  "(a + b) div b = a div b + 1"
-  using \<open>b \<noteq> 0\<close> div_add_self1 [of a] by (simp add: ac_simps)
-
-end
-
-lemma div_mult_mult2:
-  "(a * c) div (b * c) = a div b" if "c \<noteq> 0"
-  using that div_mult_mult1 [of c a b] by (simp add: ac_simps)
-
-lemma div_mult_mult1_if [simp]:
-  "(c * a) div (c * b) = (if c = 0 then 0 else a div b)"
-  by (simp add: div_mult_mult1)
-
-lemma div_mult_mult2_if [simp]:
-  "(a * c) div (b * c) = (if c = 0 then 0 else a div b)"
-  using div_mult_mult1_if [of c a b] by (simp add: ac_simps)
-
-end
-
-class idom_divide_cancel = idom_divide + semidom_divide_cancel
-begin
-
-lemma div_minus_minus [simp]: "(- a) div (- b) = a div b"
-  using div_mult_mult1 [of "- 1" a b] by simp
-
-lemma div_minus_right: "a div (- b) = (- a) div b"
-  using div_minus_minus [of "- a" b] by simp
-
-lemma div_minus1_right [simp]: "a div (- 1) = - a"
-  using div_minus_right [of a 1] by simp
-
-end
-
-
-subsection \<open>Basic notions following from divisibility\<close>
-
 class algebraic_semidom = semidom_divide
 begin