# HG changeset patch
# User haftmann
# Date 1481984534 -3600
# Node ID 7759f176618947850d06742edb84530e48ed280c
# Parent  240a39af9ec4d73738d5d2ec08380617fd8dc412
more fine-grained type class hierarchy for div and mod

diff -r 240a39af9ec4 -r 7759f1766189 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Code_Numeral.thy	Sat Dec 17 15:22:14 2016 +0100
@@ -168,21 +168,9 @@
   "integer_of_num (Num.Bit0 Num.One) = 2"
   by (transfer, simp)+
 
-instantiation integer :: "{ring_div, equal, linordered_idom}"
+instantiation integer :: "{linordered_idom, equal}"
 begin
 
-lift_definition divide_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
-  is "divide :: int \<Rightarrow> int \<Rightarrow> int"
-  .
-
-declare divide_integer.rep_eq [simp]
-
-lift_definition modulo_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
-  is "modulo :: int \<Rightarrow> int \<Rightarrow> int"
-  .
-
-declare modulo_integer.rep_eq [simp]
-
 lift_definition abs_integer :: "integer \<Rightarrow> integer"
   is "abs :: int \<Rightarrow> int"
   .
@@ -199,6 +187,7 @@
   is "less_eq :: int \<Rightarrow> int \<Rightarrow> bool"
   .
 
+
 lift_definition less_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
   is "less :: int \<Rightarrow> int \<Rightarrow> bool"
   .
@@ -207,8 +196,8 @@
   is "HOL.equal :: int \<Rightarrow> int \<Rightarrow> bool"
   .
 
-instance proof
-qed (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] mult_strict_right_mono linear)+
+instance
+  by standard (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] mult_strict_right_mono linear)+
 
 end
 
@@ -236,6 +225,38 @@
   "of_nat (nat_of_integer k) = max 0 k"
   by transfer auto
 
+instantiation integer :: "{ring_div, normalization_semidom}"
+begin
+
+lift_definition normalize_integer :: "integer \<Rightarrow> integer"
+  is "normalize :: int \<Rightarrow> int"
+  .
+
+declare normalize_integer.rep_eq [simp]
+
+lift_definition unit_factor_integer :: "integer \<Rightarrow> integer"
+  is "unit_factor :: int \<Rightarrow> int"
+  .
+
+declare unit_factor_integer.rep_eq [simp]
+
+lift_definition divide_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
+  is "divide :: int \<Rightarrow> int \<Rightarrow> int"
+  .
+
+declare divide_integer.rep_eq [simp]
+
+lift_definition modulo_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
+  is "modulo :: int \<Rightarrow> int \<Rightarrow> int"
+  .
+
+declare modulo_integer.rep_eq [simp]
+
+instance
+  by standard (transfer, simp add: mult_sgn_abs sgn_mult)+
+
+end
+
 instantiation integer :: semiring_numeral_div
 begin
 
@@ -389,6 +410,14 @@
   "Neg m * Neg n = Pos (m * n)"
   by simp_all
 
+lemma normalize_integer_code [code]:
+  "normalize = (abs :: integer \<Rightarrow> integer)"
+  by transfer simp
+
+lemma unit_factor_integer_code [code]:
+  "unit_factor = (sgn :: integer \<Rightarrow> integer)"
+  by transfer simp
+
 definition divmod_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer \<times> integer"
 where
   "divmod_integer k l = (k div l, k mod l)"
@@ -760,21 +789,9 @@
   "nat_of_natural (numeral k) = numeral k"
   by transfer rule
 
-instantiation natural :: "{semiring_div, equal, linordered_semiring}"
+instantiation natural :: "{linordered_semiring, equal}"
 begin
 
-lift_definition divide_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
-  is "divide :: nat \<Rightarrow> nat \<Rightarrow> nat"
-  .
-
-declare divide_natural.rep_eq [simp]
-
-lift_definition modulo_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
-  is "modulo :: nat \<Rightarrow> nat \<Rightarrow> nat"
-  .
-
-declare modulo_natural.rep_eq [simp]
-
 lift_definition less_eq_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
   is "less_eq :: nat \<Rightarrow> nat \<Rightarrow> bool"
   .
@@ -812,6 +829,38 @@
   "nat_of_natural (max k l) = max (nat_of_natural k) (nat_of_natural l)"
   by transfer rule
 
+instantiation natural :: "{semiring_div, normalization_semidom}"
+begin
+
+lift_definition normalize_natural :: "natural \<Rightarrow> natural"
+  is "normalize :: nat \<Rightarrow> nat"
+  .
+
+declare normalize_natural.rep_eq [simp]
+
+lift_definition unit_factor_natural :: "natural \<Rightarrow> natural"
+  is "unit_factor :: nat \<Rightarrow> nat"
+  .
+
+declare unit_factor_natural.rep_eq [simp]
+
+lift_definition divide_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
+  is "divide :: nat \<Rightarrow> nat \<Rightarrow> nat"
+  .
+
+declare divide_natural.rep_eq [simp]
+
+lift_definition modulo_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
+  is "modulo :: nat \<Rightarrow> nat \<Rightarrow> nat"
+  .
+
+declare modulo_natural.rep_eq [simp]
+
+instance
+  by standard (transfer, auto simp add: algebra_simps unit_factor_nat_def gr0_conv_Suc)+
+
+end
+
 lift_definition natural_of_integer :: "integer \<Rightarrow> natural"
   is "nat :: int \<Rightarrow> nat"
   .
@@ -945,7 +994,32 @@
 
 lemma [code abstract]:
   "integer_of_natural (m * n) = integer_of_natural m * integer_of_natural n"
-  by transfer (simp add: of_nat_mult)
+  by transfer simp
+
+lemma [code]:
+  "normalize n = n" for n :: natural
+  by transfer simp
+
+lemma [code]:
+  "unit_factor n = of_bool (n \<noteq> 0)" for n :: natural
+proof (cases "n = 0")
+  case True
+  then show ?thesis
+    by simp
+next
+  case False
+  then have "unit_factor n = 1"
+  proof transfer
+    fix n :: nat
+    assume "n \<noteq> 0"
+    then obtain m where "n = Suc m"
+      by (cases n) auto
+    then show "unit_factor n = 1"
+      by simp
+  qed
+  with False show ?thesis
+    by simp
+qed
 
 lemma [code abstract]:
   "integer_of_natural (m div n) = integer_of_natural m div integer_of_natural n"
diff -r 240a39af9ec4 -r 7759f1766189 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Divides.thy	Sat Dec 17 15:22:14 2016 +0100
@@ -3,37 +3,95 @@
     Copyright   1999  University of Cambridge
 *)
 
-section \<open>The division operators div and mod\<close>
+section \<open>Quotient and remainder\<close>
 
 theory Divides
 imports Parity
 begin
 
-subsection \<open>Abstract division in commutative semirings.\<close>
-
-class semiring_div = semidom + semiring_modulo +
-  assumes div_by_0: "a div 0 = 0"
-    and div_0: "0 div a = 0"
-    and div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
+subsection \<open>Quotient and remainder in integral domains\<close>
+
+class semidom_modulo = algebraic_semidom + semiring_modulo
+begin
+
+lemma mod_0 [simp]: "0 mod a = 0"
+  using div_mult_mod_eq [of 0 a] by simp
+
+lemma mod_by_0 [simp]: "a mod 0 = a"
+  using div_mult_mod_eq [of a 0] by simp
+
+lemma mod_by_1 [simp]:
+  "a mod 1 = 0"
+proof -
+  from div_mult_mod_eq [of a one] div_by_1 have "a + a mod 1 = a" by simp
+  then have "a + a mod 1 = a + 0" by simp
+  then show ?thesis by (rule add_left_imp_eq)
+qed
+
+lemma mod_self [simp]:
+  "a mod a = 0"
+  using div_mult_mod_eq [of a a] by simp
+
+lemma dvd_imp_mod_0 [simp]:
+  assumes "a dvd b"
+  shows "b mod a = 0"
+  using assms minus_div_mult_eq_mod [of b a] by simp
+
+lemma mod_0_imp_dvd: 
+  assumes "a mod b = 0"
+  shows   "b dvd a"
+proof -
+  have "b dvd ((a div b) * b)" by simp
+  also have "(a div b) * b = a"
+    using div_mult_mod_eq [of a b] by (simp add: assms)
+  finally show ?thesis .
+qed
+
+lemma mod_eq_0_iff_dvd:
+  "a mod b = 0 \<longleftrightarrow> b dvd a"
+  by (auto intro: mod_0_imp_dvd)
+
+lemma dvd_eq_mod_eq_0 [nitpick_unfold, code]:
+  "a dvd b \<longleftrightarrow> b mod a = 0"
+  by (simp add: mod_eq_0_iff_dvd)
+
+lemma dvd_mod_iff: 
+  assumes "c dvd b"
+  shows "c dvd a mod b \<longleftrightarrow> c dvd a"
+proof -
+  from assms have "(c dvd a mod b) \<longleftrightarrow> (c dvd ((a div b) * b + a mod b))" 
+    by (simp add: dvd_add_right_iff)
+  also have "(a div b) * b + a mod b = a"
+    using div_mult_mod_eq [of a b] by simp
+  finally show ?thesis .
+qed
+
+lemma dvd_mod_imp_dvd:
+  assumes "c dvd a mod b" and "c dvd b"
+  shows "c dvd a"
+  using assms dvd_mod_iff [of c b a] by simp
+
+end
+
+class idom_modulo = idom + semidom_modulo
+begin
+
+subclass idom_divide ..
+
+lemma div_diff [simp]:
+  "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> (a - b) div c = a div c - b div c"
+  using div_add [of _  _ "- b"] by (simp add: dvd_neg_div)
+
+end
+
+
+subsection \<open>Quotient and remainder in integral domains with additional properties\<close>
+
+class semiring_div = semidom_modulo +
+  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
 
-subclass algebraic_semidom
-proof
-  fix b a
-  assume "b \<noteq> 0"
-  then show "a * b div b = a"
-    using div_mult_self1 [of b 0 a] by (simp add: ac_simps div_0)
-qed (simp add: div_by_0)
-
-text \<open>@{const divide} and @{const modulo}\<close>
-
-lemma mod_by_0 [simp]: "a mod 0 = a"
-  using div_mult_mod_eq [of a zero] by simp
-
-lemma mod_0 [simp]: "0 mod a = 0"
-  using div_mult_mod_eq [of zero a] div_0 by simp
-
 lemma div_mult_self2 [simp]:
   assumes "b \<noteq> 0"
   shows "(a + b * c) div b = c + a div b"
@@ -86,18 +144,6 @@
   "a * b mod b = 0"
   using mod_mult_self1 [of 0 a b] by simp
 
-lemma mod_by_1 [simp]:
-  "a mod 1 = 0"
-proof -
-  from div_mult_mod_eq [of a one] div_by_1 have "a + a mod 1 = a" by simp
-  then have "a + a mod 1 = a + 0" by simp
-  then show ?thesis by (rule add_left_imp_eq)
-qed
-
-lemma mod_self [simp]:
-  "a mod a = 0"
-  using mod_mult_self2_is_0 [of 1] by simp
-
 lemma div_add_self1:
   assumes "b \<noteq> 0"
   shows "(b + a) div b = a div b + 1"
@@ -116,31 +162,6 @@
   "(a + b) mod b = a mod b"
   using mod_mult_self1 [of a 1 b] by simp
 
-lemma dvd_imp_mod_0 [simp]:
-  assumes "a dvd b"
-  shows "b mod a = 0"
-proof -
-  from assms obtain c where "b = a * c" ..
-  then have "b mod a = a * c mod a" by simp
-  then show "b mod a = 0" by simp
-qed
-
-lemma mod_eq_0_iff_dvd:
-  "a mod b = 0 \<longleftrightarrow> b dvd a"
-proof
-  assume "b dvd a"
-  then show "a mod b = 0" by simp
-next
-  assume "a mod b = 0"
-  with div_mult_mod_eq [of a b] have "a div b * b = a" by simp
-  then have "a = b * (a div b)" by (simp add: ac_simps)
-  then show "b dvd a" ..
-qed
-
-lemma dvd_eq_mod_eq_0 [nitpick_unfold, code]:
-  "a dvd b \<longleftrightarrow> b mod a = 0"
-  by (simp add: mod_eq_0_iff_dvd)
-
 lemma mod_div_trivial [simp]:
   "a mod b div b = 0"
 proof (cases "b = 0")
@@ -168,15 +189,6 @@
   finally show ?thesis .
 qed
 
-lemma dvd_mod_imp_dvd:
-  assumes "k dvd m mod n" and "k dvd n"
-  shows "k dvd m"
-proof -
-  from assms have "k dvd (m div n) * n + m mod n"
-    by (simp only: dvd_add dvd_mult)
-  then show ?thesis by (simp add: div_mult_mod_eq)
-qed
-
 text \<open>Addition respects modular equivalence.\<close>
 
 lemma mod_add_left_eq: \<comment> \<open>FIXME reorient\<close>
@@ -319,31 +331,6 @@
 lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
   unfolding dvd_def by (auto simp add: mod_mult_mult1)
 
-lemma dvd_mod_iff: "k dvd n \<Longrightarrow> k dvd (m mod n) \<longleftrightarrow> k dvd m"
-by (blast intro: dvd_mod_imp_dvd dvd_mod)
-
-lemma div_div_eq_right:
-  assumes "c dvd b" "b dvd a"
-  shows   "a div (b div c) = a div b * c"
-proof -
-  from assms have "a div b * c = (a * c) div b"
-    by (subst dvd_div_mult) simp_all
-  also from assms have "\<dots> = (a * c) div ((b div c) * c)" by simp
-  also have "a * c div (b div c * c) = a div (b div c)"
-    by (cases "c = 0") simp_all
-  finally show ?thesis ..
-qed
-
-lemma div_div_div_same:
-  assumes "d dvd a" "d dvd b" "b dvd a"
-  shows   "(a div d) div (b div d) = a div b"
-  using assms by (subst dvd_div_mult2_eq [symmetric]) simp_all
-
-lemma cancel_div_mod_rules:
-  "((a div b) * b + a mod b) + c = a + c"
-  "(b * (a div b) + a mod b) + c = a + c"
-  by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
-
 end
 
 class ring_div = comm_ring_1 + semiring_div
@@ -394,28 +381,6 @@
   shows "(a - b) mod c = (a' - b') mod c"
   using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"] by simp
 
-lemma dvd_neg_div: "y dvd x \<Longrightarrow> -x div y = - (x div y)"
-apply (case_tac "y = 0") apply simp
-apply (auto simp add: dvd_def)
-apply (subgoal_tac "-(y * k) = y * - k")
- apply (simp only:)
- apply (erule nonzero_mult_div_cancel_left)
-apply simp
-done
-
-lemma dvd_div_neg: "y dvd x \<Longrightarrow> x div -y = - (x div y)"
-apply (case_tac "y = 0") apply simp
-apply (auto simp add: dvd_def)
-apply (subgoal_tac "y * k = -y * -k")
- apply (erule ssubst, rule nonzero_mult_div_cancel_left)
- apply simp
-apply simp
-done
-
-lemma div_diff [simp]:
-  "z dvd x \<Longrightarrow> z dvd y \<Longrightarrow> (x - y) div z = x div z - y div z"
-  using div_add [of _ _ "- y"] by (simp add: dvd_neg_div)
-
 lemma div_minus_minus [simp]: "(-a) div (-b) = a div b"
   using div_mult_mult1 [of "- 1" a b]
   unfolding neg_equal_0_iff_equal by simp
@@ -446,7 +411,7 @@
 end
 
 
-subsubsection \<open>Parity and division\<close>
+subsection \<open>Parity\<close>
 
 class semiring_div_parity = semiring_div + comm_semiring_1_cancel + numeral +
   assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
@@ -532,7 +497,7 @@
 end
 
 
-subsection \<open>Generic numeral division with a pragmatic type class\<close>
+subsection \<open>Numeral division with a pragmatic type class\<close>
 
 text \<open>
   The following type class contains everything necessary to formulate
@@ -826,8 +791,10 @@
       from m n have "Suc m = q' * n + Suc r'" by simp
       with True show ?thesis by blast
     next
-      case False then have "n \<le> Suc r'" by auto
-      moreover from n have "Suc r' \<le> n" by auto
+      case False then have "n \<le> Suc r'"
+        by (simp add: not_less)
+      moreover from n have "Suc r' \<le> n"
+        by (simp add: Suc_le_eq)
       ultimately have "n = Suc r'" by auto
       with m have "Suc m = Suc q' * n + 0" by simp
       with \<open>n \<noteq> 0\<close> show ?thesis by blast
@@ -855,7 +822,7 @@
   apply (auto simp add: add_mult_distrib)
   done
   from \<open>n \<noteq> 0\<close> assms have *: "fst qr = fst qr'"
-    by (auto simp add: divmod_nat_rel_def intro: order_antisym dest: aux sym)
+    by (auto simp add: divmod_nat_rel_def intro: order_antisym dest: aux sym split: if_splits)
   with assms have "snd qr = snd qr'"
     by (simp add: divmod_nat_rel_def)
   with * show ?thesis by (cases qr, cases qr') simp
@@ -884,10 +851,10 @@
   using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)
 
 qualified lemma divmod_nat_zero: "divmod_nat m 0 = (0, m)"
-  by (simp add: Divides.divmod_nat_unique divmod_nat_rel_def)
+  by (simp add: divmod_nat_unique divmod_nat_rel_def)
 
 qualified lemma divmod_nat_zero_left: "divmod_nat 0 n = (0, 0)"
-  by (simp add: Divides.divmod_nat_unique divmod_nat_rel_def)
+  by (simp add: divmod_nat_unique divmod_nat_rel_def)
 
 qualified lemma divmod_nat_base: "m < n \<Longrightarrow> divmod_nat m n = (0, m)"
   by (simp add: divmod_nat_unique divmod_nat_rel_def)
@@ -899,19 +866,31 @@
   have "divmod_nat_rel (m - n) n (divmod_nat (m - n) n)"
     by (fact divmod_nat_rel_divmod_nat)
   then show "divmod_nat_rel m n (apfst Suc (divmod_nat (m - n) n))"
-    unfolding divmod_nat_rel_def using assms by auto
+    unfolding divmod_nat_rel_def using assms
+      by (auto split: if_splits simp add: algebra_simps)
 qed
 
 end
-  
-instantiation nat :: semiring_div
+
+instantiation nat :: "{semidom_modulo, normalization_semidom}"
 begin
 
-definition divide_nat where
-  div_nat_def: "m div n = fst (Divides.divmod_nat m n)"
-
-definition modulo_nat where
-  mod_nat_def: "m mod n = snd (Divides.divmod_nat m n)"
+definition normalize_nat :: "nat \<Rightarrow> nat"
+  where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
+
+definition unit_factor_nat :: "nat \<Rightarrow> nat"
+  where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
+
+lemma unit_factor_simps [simp]:
+  "unit_factor 0 = (0::nat)"
+  "unit_factor (Suc n) = 1"
+  by (simp_all add: unit_factor_nat_def)
+
+definition divide_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+  where div_nat_def: "m div n = fst (Divides.divmod_nat m n)"
+
+definition modulo_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+  where mod_nat_def: "m mod n = snd (Divides.divmod_nat m n)"
 
 lemma fst_divmod_nat [simp]:
   "fst (Divides.divmod_nat m n) = m div n"
@@ -928,15 +907,18 @@
 lemma div_nat_unique:
   assumes "divmod_nat_rel m n (q, r)"
   shows "m div n = q"
-  using assms by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
+  using assms
+  by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
 
 lemma mod_nat_unique:
   assumes "divmod_nat_rel m n (q, r)"
   shows "m mod n = r"
-  using assms by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
+  using assms
+  by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
 
 lemma divmod_nat_rel: "divmod_nat_rel m n (m div n, m mod n)"
-  using Divides.divmod_nat_rel_divmod_nat by (simp add: divmod_nat_div_mod)
+  using Divides.divmod_nat_rel_divmod_nat
+  by (simp add: divmod_nat_div_mod)
 
 text \<open>The ''recursion'' equations for @{const divide} and @{const modulo}\<close>
 
@@ -964,11 +946,40 @@
   shows "m mod n = (m - n) mod n"
   using assms Divides.divmod_nat_step by (cases "n = 0") (simp_all add: prod_eq_iff)
 
+lemma mod_less_divisor [simp]:
+  fixes m n :: nat
+  assumes "n > 0"
+  shows "m mod n < n"
+  using assms divmod_nat_rel [of m n] unfolding divmod_nat_rel_def
+  by (auto split: if_splits)
+
+lemma mod_le_divisor [simp]:
+  fixes m n :: nat
+  assumes "n > 0"
+  shows "m mod n \<le> n"
+proof (rule less_imp_le)
+  from assms show "m mod n < n"
+    by simp
+qed
+
 instance proof
   fix m n :: nat
   show "m div n * n + m mod n = m"
     using divmod_nat_rel [of m n] by (simp add: divmod_nat_rel_def)
 next
+  fix n :: nat show "n div 0 = 0"
+    by (simp add: div_nat_def Divides.divmod_nat_zero)
+next
+  fix m n :: nat
+  assume "n \<noteq> 0"
+  then show "m * n div n = m"
+    by (auto simp add: divmod_nat_rel_def intro: div_nat_unique [of _ _ _ 0])
+qed (simp_all add: unit_factor_nat_def)
+
+end
+
+instance nat :: semiring_div
+proof
   fix m n q :: nat
   assume "n \<noteq> 0"
   then show "(q + m * n) div n = m + q div n"
@@ -976,48 +987,33 @@
 next
   fix m n q :: nat
   assume "m \<noteq> 0"
-  hence "\<And>a b. divmod_nat_rel n q (a, b) \<Longrightarrow> divmod_nat_rel (m * n) (m * q) (a, m * b)"
-    unfolding divmod_nat_rel_def
-    by (auto split: if_split_asm, simp_all add: algebra_simps)
-  moreover from divmod_nat_rel have "divmod_nat_rel n q (n div q, n mod q)" .
-  ultimately have "divmod_nat_rel (m * n) (m * q) (n div q, m * (n mod q))" .
-  thus "(m * n) div (m * q) = n div q" by (rule div_nat_unique)
-next
-  fix n :: nat show "n div 0 = 0"
-    by (simp add: div_nat_def Divides.divmod_nat_zero)
-next
-  fix n :: nat show "0 div n = 0"
-    by (simp add: div_nat_def Divides.divmod_nat_zero_left)
+  then have "divmod_nat_rel (m * n) (m * q) (n div q, m * (n mod q))"
+    using div_mult_mod_eq [of n q]
+    by (auto simp add: divmod_nat_rel_def algebra_simps distrib_left [symmetric] simp del: distrib_left)
+  then show "(m * n) div (m * q) = n div q"
+    by (rule div_nat_unique)
 qed
 
-end
-
-instantiation nat :: normalization_semidom
-begin
-
-definition normalize_nat
-  where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
-
-definition unit_factor_nat
-  where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
-
-lemma unit_factor_simps [simp]:
-  "unit_factor 0 = (0::nat)"
-  "unit_factor (Suc n) = 1"
-  by (simp_all add: unit_factor_nat_def)
-
-instance
-  by standard (simp_all add: unit_factor_nat_def)
-  
-end
-
-lemma divmod_nat_if [code]:
-  "Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
-    let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
-  by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
+lemma div_by_Suc_0 [simp]:
+  "m div Suc 0 = m"
+  using div_by_1 [of m] by simp
+
+lemma mod_by_Suc_0 [simp]:
+  "m mod Suc 0 = 0"
+  using mod_by_1 [of m] by simp
+
+lemma mod_greater_zero_iff_not_dvd:
+  fixes m n :: nat
+  shows "m mod n > 0 \<longleftrightarrow> \<not> n dvd m"
+  by (simp add: dvd_eq_mod_eq_0)
 
 text \<open>Simproc for cancelling @{const divide} and @{const modulo}\<close>
 
+lemma (in semiring_modulo) cancel_div_mod_rules:
+  "((a div b) * b + a mod b) + c = a + c"
+  "(b * (a div b) + a mod b) + c = a + c"
+  by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
+
 ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
 
 ML \<open>
@@ -1048,7 +1044,13 @@
 )
 \<close>
 
-simproc_setup cancel_div_mod_nat ("(m::nat) + n") = \<open>K Cancel_Div_Mod_Nat.proc\<close>
+simproc_setup cancel_div_mod_nat ("(m::nat) + n") =
+  \<open>K Cancel_Div_Mod_Nat.proc\<close>
+
+lemma divmod_nat_if [code]:
+  "Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
+    let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
+  by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
 
 
 subsubsection \<open>Quotient\<close>
@@ -1077,16 +1079,11 @@
 qed
 
 lemma div_eq_0_iff: "(a div b::nat) = 0 \<longleftrightarrow> a < b \<or> b = 0"
-  by (metis div_less div_positive div_by_0 gr0I less_numeral_extra(3) not_less)
+  by auto (metis div_positive less_numeral_extra(3) not_less)
+
 
 subsubsection \<open>Remainder\<close>
 
-lemma mod_less_divisor [simp]:
-  fixes m n :: nat
-  assumes "n > 0"
-  shows "m mod n < (n::nat)"
-  using assms divmod_nat_rel [of m n] unfolding divmod_nat_rel_def by auto
-
 lemma mod_Suc_le_divisor [simp]:
   "m mod Suc n \<le> n"
   using mod_less_divisor [of "Suc n" m] by arith
@@ -1105,13 +1102,6 @@
 lemma mod_if: "m mod (n::nat) = (if m < n then m else (m - n) mod n)"
 by (simp add: le_mod_geq)
 
-lemma mod_by_Suc_0 [simp]: "m mod Suc 0 = 0"
-by (induct m) (simp_all add: mod_geq)
-
-lemma mod_le_divisor[simp]: "0 < n \<Longrightarrow> m mod n \<le> (n::nat)"
-  apply (drule mod_less_divisor [where m = m])
-  apply simp
-  done
 
 subsubsection \<open>Quotient and Remainder\<close>
 
@@ -1180,25 +1170,16 @@
 
 subsubsection \<open>Further Facts about Quotient and Remainder\<close>
 
-lemma div_by_Suc_0 [simp]:
-  "m div Suc 0 = m"
-  using div_by_1 [of m] by simp
-
-(* Monotonicity of div in first argument *)
-lemma div_le_mono [rule_format (no_asm)]:
-    "\<forall>m::nat. m \<le> n --> (m div k) \<le> (n div k)"
-apply (case_tac "k=0", simp)
-apply (induct "n" rule: nat_less_induct, clarify)
-apply (case_tac "n<k")
-(* 1  case n<k *)
-apply simp
-(* 2  case n >= k *)
-apply (case_tac "m<k")
-(* 2.1  case m<k *)
-apply simp
-(* 2.2  case m>=k *)
-apply (simp add: div_geq diff_le_mono)
-done
+lemma div_le_mono:
+  fixes m n k :: nat
+  assumes "m \<le> n"
+  shows "m div k \<le> n div k"
+proof -
+  from assms obtain q where "n = m + q"
+    by (auto simp add: le_iff_add)
+  then show ?thesis
+    by (simp add: div_add1_eq [of m q k])
+qed
 
 (* Antimonotonicity of div in second argument *)
 lemma div_le_mono2: "!!m::nat. [| 0<m; m\<le>n |] ==> (k div n) \<le> (k div m)"
@@ -1519,11 +1500,6 @@
 
 declare Suc_times_mod_eq [of "numeral w", simp] for w
 
-lemma mod_greater_zero_iff_not_dvd:
-  fixes m n :: nat
-  shows "m mod n > 0 \<longleftrightarrow> \<not> n dvd m"
-  by (simp add: dvd_eq_mod_eq_0)
-
 lemma Suc_div_le_mono [simp]: "n div k \<le> (Suc n) div k"
 by (simp add: div_le_mono)
 
@@ -1643,6 +1619,9 @@
 
 subsection \<open>Division on @{typ int}\<close>
 
+context
+begin
+
 definition divmod_int_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" \<comment> \<open>definition of quotient and remainder\<close>
   where "divmod_int_rel a b = (\<lambda>(q, r). a = b * q + r \<and>
     (if 0 < b then 0 \<le> r \<and> r < b else if b < 0 then b < r \<and> r \<le> 0 else q = 0))"
@@ -1678,10 +1657,18 @@
 apply (blast intro: unique_quotient)
 done
 
-instantiation int :: modulo
+end
+
+instantiation int :: "{idom_modulo, normalization_semidom}"
 begin
 
-definition divide_int
+definition normalize_int :: "int \<Rightarrow> int"
+  where [simp]: "normalize = (abs :: int \<Rightarrow> int)"
+
+definition unit_factor_int :: "int \<Rightarrow> int"
+  where [simp]: "unit_factor = (sgn :: int \<Rightarrow> int)"
+
+definition divide_int :: "int \<Rightarrow> int \<Rightarrow> int"
   where "k div l = (if l = 0 \<or> k = 0 then 0
     else if k > 0 \<and> l > 0 \<or> k < 0 \<and> l < 0
       then int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
@@ -1689,32 +1676,35 @@
         if l dvd k then - int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
         else - int (Suc (nat \<bar>k\<bar> div nat \<bar>l\<bar>)))"
 
-definition modulo_int
+definition modulo_int :: "int \<Rightarrow> int \<Rightarrow> int"
   where "k mod l = (if l = 0 then k else if l dvd k then 0
     else if k > 0 \<and> l > 0 \<or> k < 0 \<and> l < 0
       then sgn l * int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)
       else sgn l * (\<bar>l\<bar> - int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)))"
 
-instance ..      
-
-end
-
 lemma divmod_int_rel:
   "divmod_int_rel k l (k div l, k mod l)"
-  unfolding divmod_int_rel_def divide_int_def modulo_int_def
-  apply (cases k rule: int_cases3)
-  apply (simp add: mod_greater_zero_iff_not_dvd not_le algebra_simps)
-  apply (cases l rule: int_cases3)
-  apply (simp add: mod_greater_zero_iff_not_dvd not_le algebra_simps)
-  apply (simp_all del: of_nat_add of_nat_mult add: mod_greater_zero_iff_not_dvd not_le algebra_simps int_dvd_iff of_nat_add [symmetric] of_nat_mult [symmetric])
-  apply (cases l rule: int_cases3)
-  apply (simp_all del: of_nat_add of_nat_mult add: not_le algebra_simps int_dvd_iff of_nat_add [symmetric] of_nat_mult [symmetric])
-  done
-
-instantiation int :: ring_div
-begin
-
-subsubsection \<open>Uniqueness and Monotonicity of Quotients and Remainders\<close>
+proof (cases k rule: int_cases3)
+  case zero
+  then show ?thesis
+    by (simp add: divmod_int_rel_def divide_int_def modulo_int_def)
+next
+  case (pos n)
+  then show ?thesis
+    using div_mult_mod_eq [of n]
+    by (cases l rule: int_cases3)
+      (auto simp del: of_nat_mult of_nat_add
+        simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
+        divmod_int_rel_def divide_int_def modulo_int_def int_dvd_iff)
+next
+  case (neg n)
+  then show ?thesis
+    using div_mult_mod_eq [of n]
+    by (cases l rule: int_cases3)
+      (auto simp del: of_nat_mult of_nat_add
+        simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
+        divmod_int_rel_def divide_int_def modulo_int_def int_dvd_iff)
+qed
 
 lemma divmod_int_unique:
   assumes "divmod_int_rel k l (q, r)"
@@ -1722,42 +1712,21 @@
   using assms divmod_int_rel [of k l]
   using unique_quotient [of k l] unique_remainder [of k l]
   by auto
-  
-instance
-proof
-  fix a b :: int
-  show "a div b * b + a mod b = a"
-    using divmod_int_rel [of a b]
-    unfolding divmod_int_rel_def by (simp add: mult.commute)
-next
-  fix a b c :: int
-  assume "b \<noteq> 0"
-  hence "divmod_int_rel (a + c * b) b (c + a div b, a mod b)"
-    using divmod_int_rel [of a b]
-    unfolding divmod_int_rel_def by (auto simp: algebra_simps)
-  thus "(a + c * b) div b = c + a div b"
-    by (rule div_int_unique)
+
+instance proof
+  fix k l :: int
+  show "k div l * l + k mod l = k"
+    using divmod_int_rel [of k l]
+    unfolding divmod_int_rel_def by (simp add: ac_simps)
 next
-  fix a b c :: int
-  assume c: "c \<noteq> 0"
-  have "\<And>q r. divmod_int_rel a b (q, r)
-    \<Longrightarrow> divmod_int_rel (c * a) (c * b) (q, c * r)"
-    unfolding divmod_int_rel_def
-    by (rule linorder_cases [of 0 b])
-      (use c in \<open>auto simp: algebra_simps
-      mult_less_0_iff zero_less_mult_iff mult_strict_right_mono
-      mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff\<close>)
-  hence "divmod_int_rel (c * a) (c * b) (a div b, c * (a mod b))"
-    using divmod_int_rel [of a b] .
-  thus "(c * a) div (c * b) = a div b"
-    by (rule div_int_unique)
-next
-  fix a :: int show "a div 0 = 0"
+  fix k :: int show "k div 0 = 0"
     by (rule div_int_unique, simp add: divmod_int_rel_def)
 next
-  fix a :: int show "0 div a = 0"
-    by (rule div_int_unique, auto simp add: divmod_int_rel_def)
-qed
+  fix k l :: int
+  assume "l \<noteq> 0"
+  then show "k * l div l = k"
+    by (auto simp add: divmod_int_rel_def ac_simps intro: div_int_unique [of _ _ _ 0])
+qed (simp_all add: sgn_mult mult_sgn_abs abs_sgn_eq)
 
 end
 
@@ -1765,36 +1734,30 @@
   "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
   by auto
 
-instantiation int :: normalization_semidom
-begin
-
-definition normalize_int
-  where [simp]: "normalize = (abs :: int \<Rightarrow> int)"
-
-definition unit_factor_int
-  where [simp]: "unit_factor = (sgn :: int \<Rightarrow> int)"
-
-instance
+instance int :: ring_div
 proof
-  fix k :: int
-  assume "k \<noteq> 0"
-  then have "\<bar>sgn k\<bar> = 1"
-    by (cases "0::int" k rule: linorder_cases) simp_all
-  then show "is_unit (unit_factor k)"
-    by simp
-qed (simp_all add: sgn_mult mult_sgn_abs)
-  
-end
-  
-text\<open>Basic laws about division and remainder\<close>
-
-lemma zdiv_int: "int (a div b) = int a div int b"
-  by (simp add: divide_int_def)
-
-lemma zmod_int: "int (a mod b) = int a mod int b"
-  by (simp add: modulo_int_def int_dvd_iff)
-  
-text \<open>Tool setup\<close>
+  fix k l s :: int
+  assume "l \<noteq> 0"
+  then have "divmod_int_rel (k + s * l) l (s + k div l, k mod l)"
+    using divmod_int_rel [of k l]
+    unfolding divmod_int_rel_def by (auto simp: algebra_simps)
+  then show "(k + s * l) div l = s + k div l"
+    by (rule div_int_unique)
+next
+  fix k l s :: int
+  assume "s \<noteq> 0"
+  have "\<And>q r. divmod_int_rel k l (q, r)
+    \<Longrightarrow> divmod_int_rel (s * k) (s * l) (q, s * r)"
+    unfolding divmod_int_rel_def
+    by (rule linorder_cases [of 0 l])
+      (use \<open>s \<noteq> 0\<close> in \<open>auto simp: algebra_simps
+      mult_less_0_iff zero_less_mult_iff mult_strict_right_mono
+      mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff\<close>)
+  then have "divmod_int_rel (s * k) (s * l) (k div l, s * (k mod l))"
+    using divmod_int_rel [of k l] .
+  then show "(s * k) div (s * l) = k div l"
+    by (rule div_int_unique)
+qed
 
 ML \<open>
 structure Cancel_Div_Mod_Int = Cancel_Div_Mod
@@ -1807,12 +1770,22 @@
 
   val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
 
-  val prove_eq_sums = Arith_Data.prove_conv2 all_tac
-    (Arith_Data.simp_all_tac @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps})
+  val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
+    @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps})
 )
 \<close>
 
-simproc_setup cancel_div_mod_int ("(k::int) + l") = \<open>K Cancel_Div_Mod_Int.proc\<close>
+simproc_setup cancel_div_mod_int ("(k::int) + l") =
+  \<open>K Cancel_Div_Mod_Int.proc\<close>
+
+
+text\<open>Basic laws about division and remainder\<close>
+
+lemma zdiv_int: "int (a div b) = int a div int b"
+  by (simp add: divide_int_def)
+
+lemma zmod_int: "int (a mod b) = int a mod int b"
+  by (simp add: modulo_int_def int_dvd_iff)
 
 lemma pos_mod_conj: "(0::int) < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b"
   using divmod_int_rel [of a b]
@@ -1887,10 +1860,15 @@
 apply (blast intro: divmod_int_rel [THEN zminus1_lemma, THEN mod_int_unique])
 done
 
-lemma zmod_zminus1_not_zero:
+lemma zmod_zminus1_not_zero: -- \<open>FIXME generalize\<close>
   fixes k l :: int
   shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
-  unfolding zmod_zminus1_eq_if by auto
+  by (simp add: mod_eq_0_iff_dvd)
+
+lemma zmod_zminus2_not_zero: -- \<open>FIXME generalize\<close>
+  fixes k l :: int
+  shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
+  by (simp add: mod_eq_0_iff_dvd)
 
 lemma zdiv_zminus2_eq_if:
      "b \<noteq> (0::int)
@@ -1902,11 +1880,6 @@
      "a mod (-b::int) = (if a mod b = 0 then 0 else  (a mod b) - b)"
 by (simp add: zmod_zminus1_eq_if mod_minus_right)
 
-lemma zmod_zminus2_not_zero:
-  fixes k l :: int
-  shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
-  unfolding zmod_zminus2_eq_if by auto
-
 
 subsubsection \<open>Monotonicity in the First Argument (Dividend)\<close>
 
@@ -2666,6 +2639,4 @@
 
 declare minus_div_mult_eq_mod [symmetric, nitpick_unfold]
 
-hide_fact (open) div_0 div_by_0
-
 end
diff -r 240a39af9ec4 -r 7759f1766189 src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Enum.thy	Sat Dec 17 15:22:14 2016 +0100
@@ -683,7 +683,7 @@
 
 instance finite_2 :: complete_linorder ..
 
-instantiation finite_2 :: "{field, ring_div, idom_abs_sgn}" begin
+instantiation finite_2 :: "{field, idom_abs_sgn}" begin
 definition [simp]: "0 = a\<^sub>1"
 definition [simp]: "1 = a\<^sub>2"
 definition "x + y = (case (x, y) of (a\<^sub>1, a\<^sub>1) \<Rightarrow> a\<^sub>1 | (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>1 | _ \<Rightarrow> a\<^sub>2)"
@@ -693,19 +693,33 @@
 definition "inverse = (\<lambda>x :: finite_2. x)"
 definition "divide = (op * :: finite_2 \<Rightarrow> _)"
 definition "abs = (\<lambda>x :: finite_2. x)"
-definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
 definition "sgn = (\<lambda>x :: finite_2. x)"
 instance
-by intro_classes
-  (simp_all add: plus_finite_2_def uminus_finite_2_def minus_finite_2_def times_finite_2_def
-       inverse_finite_2_def divide_finite_2_def abs_finite_2_def modulo_finite_2_def sgn_finite_2_def
-     split: finite_2.splits)
+  by standard
+    (simp_all add: plus_finite_2_def uminus_finite_2_def minus_finite_2_def times_finite_2_def
+      inverse_finite_2_def divide_finite_2_def abs_finite_2_def sgn_finite_2_def
+      split: finite_2.splits)
 end
 
 lemma two_finite_2 [simp]:
   "2 = a\<^sub>1"
   by (simp add: numeral.simps plus_finite_2_def)
-  
+
+lemma dvd_finite_2_unfold:
+  "x dvd y \<longleftrightarrow> x = a\<^sub>2 \<or> y = a\<^sub>1"
+  by (auto simp add: dvd_def times_finite_2_def split: finite_2.splits)
+
+instantiation finite_2 :: "{ring_div, normalization_semidom}" begin
+definition [simp]: "normalize = (id :: finite_2 \<Rightarrow> _)"
+definition [simp]: "unit_factor = (id :: finite_2 \<Rightarrow> _)"
+definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
+instance
+  by standard
+    (simp_all add: dvd_finite_2_unfold times_finite_2_def
+      divide_finite_2_def modulo_finite_2_def split: finite_2.splits)
+end
+
+ 
 hide_const (open) a\<^sub>1 a\<^sub>2
 
 datatype (plugins only: code "quickcheck" extraction) finite_3 =
@@ -736,6 +750,12 @@
 
 end
 
+lemma finite_3_not_eq_unfold:
+  "x \<noteq> a\<^sub>1 \<longleftrightarrow> x \<in> {a\<^sub>2, a\<^sub>3}"
+  "x \<noteq> a\<^sub>2 \<longleftrightarrow> x \<in> {a\<^sub>1, a\<^sub>3}"
+  "x \<noteq> a\<^sub>3 \<longleftrightarrow> x \<in> {a\<^sub>1, a\<^sub>2}"
+  by (cases x; simp)+
+
 instantiation finite_3 :: linorder
 begin
 
@@ -806,7 +826,7 @@
 
 instance finite_3 :: complete_linorder ..
 
-instantiation finite_3 :: "{field, ring_div, idom_abs_sgn}" begin
+instantiation finite_3 :: "{field, idom_abs_sgn}" begin
 definition [simp]: "0 = a\<^sub>1"
 definition [simp]: "1 = a\<^sub>2"
 definition
@@ -820,14 +840,33 @@
 definition "inverse = (\<lambda>x :: finite_3. x)" 
 definition "x div y = x * inverse (y :: finite_3)"
 definition "abs = (\<lambda>x. case x of a\<^sub>3 \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> x)"
-definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | (a\<^sub>3, a\<^sub>1) \<Rightarrow> a\<^sub>3 | _ \<Rightarrow> a\<^sub>1)"
 definition "sgn = (\<lambda>x :: finite_3. x)"
 instance
-by intro_classes
-  (simp_all add: plus_finite_3_def uminus_finite_3_def minus_finite_3_def times_finite_3_def
-       inverse_finite_3_def divide_finite_3_def abs_finite_3_def modulo_finite_3_def sgn_finite_3_def
-       less_finite_3_def
-     split: finite_3.splits)
+  by standard
+    (simp_all add: plus_finite_3_def uminus_finite_3_def minus_finite_3_def times_finite_3_def
+      inverse_finite_3_def divide_finite_3_def abs_finite_3_def sgn_finite_3_def
+      less_finite_3_def
+      split: finite_3.splits)
+end
+
+lemma two_finite_3 [simp]:
+  "2 = a\<^sub>3"
+  by (simp add: numeral.simps plus_finite_3_def)
+
+lemma dvd_finite_3_unfold:
+  "x dvd y \<longleftrightarrow> x = a\<^sub>2 \<or> x = a\<^sub>3 \<or> y = a\<^sub>1"
+  by (cases x) (auto simp add: dvd_def times_finite_3_def split: finite_3.splits)
+
+instantiation finite_3 :: "{ring_div, normalization_semidom}" begin
+definition "normalize x = (case x of a\<^sub>3 \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> x)"
+definition [simp]: "unit_factor = (id :: finite_3 \<Rightarrow> _)"
+definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | (a\<^sub>3, a\<^sub>1) \<Rightarrow> a\<^sub>3 | _ \<Rightarrow> a\<^sub>1)"
+instance
+  by standard
+    (auto simp add: finite_3_not_eq_unfold plus_finite_3_def
+      dvd_finite_3_unfold times_finite_3_def inverse_finite_3_def
+      normalize_finite_3_def divide_finite_3_def modulo_finite_3_def
+      split: finite_3.splits)
 end
 
 
diff -r 240a39af9ec4 -r 7759f1766189 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Sat Dec 17 15:22:14 2016 +0100
@@ -1157,7 +1157,40 @@
 lemma fps_unit_dvd [simp]: "(f $ 0 :: 'a :: field) \<noteq> 0 \<Longrightarrow> f dvd g"
   by (rule dvd_trans, subst fps_is_unit_iff) simp_all
 
-
+instantiation fps :: (field) normalization_semidom
+begin
+
+definition fps_unit_factor_def [simp]:
+  "unit_factor f = fps_shift (subdegree f) f"
+
+definition fps_normalize_def [simp]:
+  "normalize f = (if f = 0 then 0 else X ^ subdegree f)"
+
+instance proof
+  fix f :: "'a fps"
+  show "unit_factor f * normalize f = f"
+    by (simp add: fps_shift_times_X_power)
+next
+  fix f g :: "'a fps"
+  show "unit_factor (f * g) = unit_factor f * unit_factor g"
+  proof (cases "f = 0 \<or> g = 0")
+    assume "\<not>(f = 0 \<or> g = 0)"
+    thus "unit_factor (f * g) = unit_factor f * unit_factor g"
+    unfolding fps_unit_factor_def
+      by (auto simp: fps_shift_fps_shift fps_shift_mult fps_shift_mult_right)
+  qed auto
+next
+  fix f g :: "'a fps"
+  assume "g \<noteq> 0"
+  then have "f * (fps_shift (subdegree g) g * inverse (fps_shift (subdegree g) g)) = f"
+    by (metis add_cancel_right_left fps_shift_nth inverse_mult_eq_1 mult.commute mult_cancel_left2 nth_subdegree_nonzero)
+  then have "fps_shift (subdegree g) (g * (f * inverse (fps_shift (subdegree g) g))) = f"
+    by (simp add: fps_shift_mult_right mult.commute)
+  with \<open>g \<noteq> 0\<close> show "f * g / g = f"
+    by (simp add: fps_divide_def Let_def ac_simps)
+qed (auto simp add: fps_divide_def Let_def)
+
+end
 
 instantiation fps :: (field) ring_div
 begin
@@ -1291,7 +1324,7 @@
   also have "fps_shift n (f * inverse h') = f div h"
     by (simp add: fps_divide_def Let_def dfs)
   finally show "(f + g * h) div h = g + f div h" by simp
-qed (auto simp: fps_divide_def fps_mod_def Let_def)
+qed
 
 end
 end
@@ -1365,36 +1398,6 @@
   fps_numeral_divide_divide fps_numeral_mult_divide inverse_fps_numeral neg_numeral_fps_const
 
 
-
-instantiation fps :: (field) normalization_semidom
-begin
-
-definition fps_unit_factor_def [simp]:
-  "unit_factor f = fps_shift (subdegree f) f"
-
-definition fps_normalize_def [simp]:
-  "normalize f = (if f = 0 then 0 else X ^ subdegree f)"
-
-instance proof
-  fix f :: "'a fps"
-  show "unit_factor f * normalize f = f"
-    by (simp add: fps_shift_times_X_power)
-next
-  fix f g :: "'a fps"
-  show "unit_factor (f * g) = unit_factor f * unit_factor g"
-  proof (cases "f = 0 \<or> g = 0")
-    assume "\<not>(f = 0 \<or> g = 0)"
-    thus "unit_factor (f * g) = unit_factor f * unit_factor g"
-    unfolding fps_unit_factor_def
-      by (auto simp: fps_shift_fps_shift fps_shift_mult fps_shift_mult_right)
-  qed auto
-qed auto
-
-end
-
-instance fps :: (field) algebraic_semidom ..
-
-
 subsection \<open>Formal power series form a Euclidean ring\<close>
 
 instantiation fps :: (field) euclidean_ring
diff -r 240a39af9ec4 -r 7759f1766189 src/HOL/Library/Normalized_Fraction.thy
--- a/src/HOL/Library/Normalized_Fraction.thy	Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Library/Normalized_Fraction.thy	Sat Dec 17 15:22:14 2016 +0100
@@ -184,7 +184,7 @@
 
 lemma quot_of_fract_uminus:
   "quot_of_fract (-x) = (let (a,b) = quot_of_fract x in (-a, b))"
-  by transfer (auto simp: case_prod_unfold Let_def normalize_quot_def dvd_neg_div' mult_unit_dvd_iff)
+  by transfer (auto simp: case_prod_unfold Let_def normalize_quot_def dvd_neg_div mult_unit_dvd_iff)
 
 lemma quot_of_fract_diff:
   "quot_of_fract (x - y) = 
diff -r 240a39af9ec4 -r 7759f1766189 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Library/Polynomial.thy	Sat Dec 17 15:22:14 2016 +0100
@@ -2274,12 +2274,6 @@
   from pdivmod_rel[of x y,unfolded pdivmod_rel_def]
   show "x div y * y + x mod y = x" by auto
 next
-  fix x :: "'a poly"
-  show "x div 0 = 0" by simp
-next
-  fix y :: "'a poly"
-  show "0 div y = 0" by simp
-next
   fix x y z :: "'a poly"
   assume "y \<noteq> 0"
   hence "pdivmod_rel (x + z * y) y (z + x div y) (x mod y)"
diff -r 240a39af9ec4 -r 7759f1766189 src/HOL/Number_Theory/Euclidean_Algorithm.thy
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sat Dec 17 15:22:14 2016 +0100
@@ -17,7 +17,7 @@
   The existence of these functions makes it possible to derive gcd and lcm functions 
   for any Euclidean semiring.
 \<close> 
-class euclidean_semiring = semiring_modulo + normalization_semidom + 
+class euclidean_semiring = semidom_modulo + normalization_semidom + 
   fixes euclidean_size :: "'a \<Rightarrow> nat"
   assumes size_0 [simp]: "euclidean_size 0 = 0"
   assumes mod_size_less: 
@@ -26,30 +26,6 @@
     "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)"
 begin
 
-lemma mod_0 [simp]: "0 mod a = 0"
-  using div_mult_mod_eq [of 0 a] by simp
-
-lemma dvd_mod_iff: 
-  assumes "k dvd n"
-  shows   "(k dvd m mod n) = (k dvd m)"
-proof -
-  from assms have "(k dvd m mod n) \<longleftrightarrow> (k dvd ((m div n) * n + m mod n))" 
-    by (simp add: dvd_add_right_iff)
-  also have "(m div n) * n + m mod n = m"
-    using div_mult_mod_eq [of m n] by simp
-  finally show ?thesis .
-qed
-
-lemma mod_0_imp_dvd: 
-  assumes "a mod b = 0"
-  shows   "b dvd a"
-proof -
-  have "b dvd ((a div b) * b)" by simp
-  also have "(a div b) * b = a"
-    using div_mult_mod_eq [of a b] by (simp add: assms)
-  finally show ?thesis .
-qed
-
 lemma euclidean_size_normalize [simp]:
   "euclidean_size (normalize a) = euclidean_size a"
 proof (cases "a = 0")
diff -r 240a39af9ec4 -r 7759f1766189 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Rings.thy	Sat Dec 17 15:22:14 2016 +0100
@@ -731,7 +731,7 @@
 class idom_divide = idom + semidom_divide
 begin
 
-lemma dvd_neg_div':
+lemma dvd_neg_div:
   assumes "b dvd a"
   shows "- a div b = - (a div b)"
 proof (cases "b = 0")
@@ -740,10 +740,30 @@
 next
   case False
   from assms obtain c where "a = b * c" ..
-  moreover from False have "b * - c div b = - (b * c div b)"
-    using nonzero_mult_div_cancel_left [of b "- c"]
+  then have "- a div b = (b * - c) div b"
+    by simp
+  from False also have "\<dots> = - c"
+    by (rule nonzero_mult_div_cancel_left)  
+  with False \<open>a = b * c\<close> show ?thesis
     by simp
-  ultimately show ?thesis
+qed
+
+lemma dvd_div_neg:
+  assumes "b dvd a"
+  shows "a div - b = - (a div b)"
+proof (cases "b = 0")
+  case True
+  then show ?thesis by simp
+next
+  case False
+  then have "- b \<noteq> 0"
+    by simp
+  from assms obtain c where "a = b * c" ..
+  then have "a div - b = (- b * - c) div - b"
+    by simp
+  from \<open>- b \<noteq> 0\<close> also have "\<dots> = - c"
+    by (rule nonzero_mult_div_cancel_left)  
+  with False \<open>a = b * c\<close> show ?thesis
     by simp
 qed
 
@@ -916,6 +936,39 @@
     by (simp add: mult.commute [of a] mult.assoc)
 qed
 
+lemma div_div_eq_right:
+  assumes "c dvd b" "b dvd a"
+  shows   "a div (b div c) = a div b * c"
+proof (cases "c = 0 \<or> b = 0")
+  case True
+  then show ?thesis
+    by auto
+next
+  case False
+  from assms obtain r s where "b = c * r" and "a = c * r * s"
+    by (blast elim: dvdE)
+  moreover with False have "r \<noteq> 0"
+    by auto
+  ultimately show ?thesis using False
+    by simp (simp add: mult.commute [of _ r] mult.assoc mult.commute [of c])
+qed
+
+lemma div_div_div_same:
+  assumes "d dvd b" "b dvd a"
+  shows   "(a div d) div (b div d) = a div b"
+proof (cases "b = 0 \<or> d = 0")
+  case True
+  with assms show ?thesis
+    by auto
+next
+  case False
+  from assms obtain r s
+    where "a = d * r * s" and "b = d * r"
+    by (blast elim: dvdE)
+  with False show ?thesis
+    by simp (simp add: ac_simps)
+qed
+
 
 text \<open>Units: invertible elements in a ring\<close>