more fine-grained type class hierarchy for div and mod
authorhaftmann
Sat Dec 17 15:22:14 2016 +0100 (2016-12-17)
changeset 645927759f1766189
parent 64591 240a39af9ec4
child 64593 50c715579715
more fine-grained type class hierarchy for div and mod
src/HOL/Code_Numeral.thy
src/HOL/Divides.thy
src/HOL/Enum.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/Normalized_Fraction.thy
src/HOL/Library/Polynomial.thy
src/HOL/Number_Theory/Euclidean_Algorithm.thy
src/HOL/Rings.thy
     1.1 --- a/src/HOL/Code_Numeral.thy	Sat Dec 17 15:22:13 2016 +0100
     1.2 +++ b/src/HOL/Code_Numeral.thy	Sat Dec 17 15:22:14 2016 +0100
     1.3 @@ -168,21 +168,9 @@
     1.4    "integer_of_num (Num.Bit0 Num.One) = 2"
     1.5    by (transfer, simp)+
     1.6  
     1.7 -instantiation integer :: "{ring_div, equal, linordered_idom}"
     1.8 +instantiation integer :: "{linordered_idom, equal}"
     1.9  begin
    1.10  
    1.11 -lift_definition divide_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
    1.12 -  is "divide :: int \<Rightarrow> int \<Rightarrow> int"
    1.13 -  .
    1.14 -
    1.15 -declare divide_integer.rep_eq [simp]
    1.16 -
    1.17 -lift_definition modulo_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
    1.18 -  is "modulo :: int \<Rightarrow> int \<Rightarrow> int"
    1.19 -  .
    1.20 -
    1.21 -declare modulo_integer.rep_eq [simp]
    1.22 -
    1.23  lift_definition abs_integer :: "integer \<Rightarrow> integer"
    1.24    is "abs :: int \<Rightarrow> int"
    1.25    .
    1.26 @@ -199,6 +187,7 @@
    1.27    is "less_eq :: int \<Rightarrow> int \<Rightarrow> bool"
    1.28    .
    1.29  
    1.30 +
    1.31  lift_definition less_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
    1.32    is "less :: int \<Rightarrow> int \<Rightarrow> bool"
    1.33    .
    1.34 @@ -207,8 +196,8 @@
    1.35    is "HOL.equal :: int \<Rightarrow> int \<Rightarrow> bool"
    1.36    .
    1.37  
    1.38 -instance proof
    1.39 -qed (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] mult_strict_right_mono linear)+
    1.40 +instance
    1.41 +  by standard (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] mult_strict_right_mono linear)+
    1.42  
    1.43  end
    1.44  
    1.45 @@ -236,6 +225,38 @@
    1.46    "of_nat (nat_of_integer k) = max 0 k"
    1.47    by transfer auto
    1.48  
    1.49 +instantiation integer :: "{ring_div, normalization_semidom}"
    1.50 +begin
    1.51 +
    1.52 +lift_definition normalize_integer :: "integer \<Rightarrow> integer"
    1.53 +  is "normalize :: int \<Rightarrow> int"
    1.54 +  .
    1.55 +
    1.56 +declare normalize_integer.rep_eq [simp]
    1.57 +
    1.58 +lift_definition unit_factor_integer :: "integer \<Rightarrow> integer"
    1.59 +  is "unit_factor :: int \<Rightarrow> int"
    1.60 +  .
    1.61 +
    1.62 +declare unit_factor_integer.rep_eq [simp]
    1.63 +
    1.64 +lift_definition divide_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
    1.65 +  is "divide :: int \<Rightarrow> int \<Rightarrow> int"
    1.66 +  .
    1.67 +
    1.68 +declare divide_integer.rep_eq [simp]
    1.69 +
    1.70 +lift_definition modulo_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
    1.71 +  is "modulo :: int \<Rightarrow> int \<Rightarrow> int"
    1.72 +  .
    1.73 +
    1.74 +declare modulo_integer.rep_eq [simp]
    1.75 +
    1.76 +instance
    1.77 +  by standard (transfer, simp add: mult_sgn_abs sgn_mult)+
    1.78 +
    1.79 +end
    1.80 +
    1.81  instantiation integer :: semiring_numeral_div
    1.82  begin
    1.83  
    1.84 @@ -389,6 +410,14 @@
    1.85    "Neg m * Neg n = Pos (m * n)"
    1.86    by simp_all
    1.87  
    1.88 +lemma normalize_integer_code [code]:
    1.89 +  "normalize = (abs :: integer \<Rightarrow> integer)"
    1.90 +  by transfer simp
    1.91 +
    1.92 +lemma unit_factor_integer_code [code]:
    1.93 +  "unit_factor = (sgn :: integer \<Rightarrow> integer)"
    1.94 +  by transfer simp
    1.95 +
    1.96  definition divmod_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer \<times> integer"
    1.97  where
    1.98    "divmod_integer k l = (k div l, k mod l)"
    1.99 @@ -760,21 +789,9 @@
   1.100    "nat_of_natural (numeral k) = numeral k"
   1.101    by transfer rule
   1.102  
   1.103 -instantiation natural :: "{semiring_div, equal, linordered_semiring}"
   1.104 +instantiation natural :: "{linordered_semiring, equal}"
   1.105  begin
   1.106  
   1.107 -lift_definition divide_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
   1.108 -  is "divide :: nat \<Rightarrow> nat \<Rightarrow> nat"
   1.109 -  .
   1.110 -
   1.111 -declare divide_natural.rep_eq [simp]
   1.112 -
   1.113 -lift_definition modulo_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
   1.114 -  is "modulo :: nat \<Rightarrow> nat \<Rightarrow> nat"
   1.115 -  .
   1.116 -
   1.117 -declare modulo_natural.rep_eq [simp]
   1.118 -
   1.119  lift_definition less_eq_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
   1.120    is "less_eq :: nat \<Rightarrow> nat \<Rightarrow> bool"
   1.121    .
   1.122 @@ -812,6 +829,38 @@
   1.123    "nat_of_natural (max k l) = max (nat_of_natural k) (nat_of_natural l)"
   1.124    by transfer rule
   1.125  
   1.126 +instantiation natural :: "{semiring_div, normalization_semidom}"
   1.127 +begin
   1.128 +
   1.129 +lift_definition normalize_natural :: "natural \<Rightarrow> natural"
   1.130 +  is "normalize :: nat \<Rightarrow> nat"
   1.131 +  .
   1.132 +
   1.133 +declare normalize_natural.rep_eq [simp]
   1.134 +
   1.135 +lift_definition unit_factor_natural :: "natural \<Rightarrow> natural"
   1.136 +  is "unit_factor :: nat \<Rightarrow> nat"
   1.137 +  .
   1.138 +
   1.139 +declare unit_factor_natural.rep_eq [simp]
   1.140 +
   1.141 +lift_definition divide_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
   1.142 +  is "divide :: nat \<Rightarrow> nat \<Rightarrow> nat"
   1.143 +  .
   1.144 +
   1.145 +declare divide_natural.rep_eq [simp]
   1.146 +
   1.147 +lift_definition modulo_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
   1.148 +  is "modulo :: nat \<Rightarrow> nat \<Rightarrow> nat"
   1.149 +  .
   1.150 +
   1.151 +declare modulo_natural.rep_eq [simp]
   1.152 +
   1.153 +instance
   1.154 +  by standard (transfer, auto simp add: algebra_simps unit_factor_nat_def gr0_conv_Suc)+
   1.155 +
   1.156 +end
   1.157 +
   1.158  lift_definition natural_of_integer :: "integer \<Rightarrow> natural"
   1.159    is "nat :: int \<Rightarrow> nat"
   1.160    .
   1.161 @@ -945,7 +994,32 @@
   1.162  
   1.163  lemma [code abstract]:
   1.164    "integer_of_natural (m * n) = integer_of_natural m * integer_of_natural n"
   1.165 -  by transfer (simp add: of_nat_mult)
   1.166 +  by transfer simp
   1.167 +
   1.168 +lemma [code]:
   1.169 +  "normalize n = n" for n :: natural
   1.170 +  by transfer simp
   1.171 +
   1.172 +lemma [code]:
   1.173 +  "unit_factor n = of_bool (n \<noteq> 0)" for n :: natural
   1.174 +proof (cases "n = 0")
   1.175 +  case True
   1.176 +  then show ?thesis
   1.177 +    by simp
   1.178 +next
   1.179 +  case False
   1.180 +  then have "unit_factor n = 1"
   1.181 +  proof transfer
   1.182 +    fix n :: nat
   1.183 +    assume "n \<noteq> 0"
   1.184 +    then obtain m where "n = Suc m"
   1.185 +      by (cases n) auto
   1.186 +    then show "unit_factor n = 1"
   1.187 +      by simp
   1.188 +  qed
   1.189 +  with False show ?thesis
   1.190 +    by simp
   1.191 +qed
   1.192  
   1.193  lemma [code abstract]:
   1.194    "integer_of_natural (m div n) = integer_of_natural m div integer_of_natural n"
     2.1 --- a/src/HOL/Divides.thy	Sat Dec 17 15:22:13 2016 +0100
     2.2 +++ b/src/HOL/Divides.thy	Sat Dec 17 15:22:14 2016 +0100
     2.3 @@ -3,37 +3,95 @@
     2.4      Copyright   1999  University of Cambridge
     2.5  *)
     2.6  
     2.7 -section \<open>The division operators div and mod\<close>
     2.8 +section \<open>Quotient and remainder\<close>
     2.9  
    2.10  theory Divides
    2.11  imports Parity
    2.12  begin
    2.13  
    2.14 -subsection \<open>Abstract division in commutative semirings.\<close>
    2.15 -
    2.16 -class semiring_div = semidom + semiring_modulo +
    2.17 -  assumes div_by_0: "a div 0 = 0"
    2.18 -    and div_0: "0 div a = 0"
    2.19 -    and div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
    2.20 +subsection \<open>Quotient and remainder in integral domains\<close>
    2.21 +
    2.22 +class semidom_modulo = algebraic_semidom + semiring_modulo
    2.23 +begin
    2.24 +
    2.25 +lemma mod_0 [simp]: "0 mod a = 0"
    2.26 +  using div_mult_mod_eq [of 0 a] by simp
    2.27 +
    2.28 +lemma mod_by_0 [simp]: "a mod 0 = a"
    2.29 +  using div_mult_mod_eq [of a 0] by simp
    2.30 +
    2.31 +lemma mod_by_1 [simp]:
    2.32 +  "a mod 1 = 0"
    2.33 +proof -
    2.34 +  from div_mult_mod_eq [of a one] div_by_1 have "a + a mod 1 = a" by simp
    2.35 +  then have "a + a mod 1 = a + 0" by simp
    2.36 +  then show ?thesis by (rule add_left_imp_eq)
    2.37 +qed
    2.38 +
    2.39 +lemma mod_self [simp]:
    2.40 +  "a mod a = 0"
    2.41 +  using div_mult_mod_eq [of a a] by simp
    2.42 +
    2.43 +lemma dvd_imp_mod_0 [simp]:
    2.44 +  assumes "a dvd b"
    2.45 +  shows "b mod a = 0"
    2.46 +  using assms minus_div_mult_eq_mod [of b a] by simp
    2.47 +
    2.48 +lemma mod_0_imp_dvd: 
    2.49 +  assumes "a mod b = 0"
    2.50 +  shows   "b dvd a"
    2.51 +proof -
    2.52 +  have "b dvd ((a div b) * b)" by simp
    2.53 +  also have "(a div b) * b = a"
    2.54 +    using div_mult_mod_eq [of a b] by (simp add: assms)
    2.55 +  finally show ?thesis .
    2.56 +qed
    2.57 +
    2.58 +lemma mod_eq_0_iff_dvd:
    2.59 +  "a mod b = 0 \<longleftrightarrow> b dvd a"
    2.60 +  by (auto intro: mod_0_imp_dvd)
    2.61 +
    2.62 +lemma dvd_eq_mod_eq_0 [nitpick_unfold, code]:
    2.63 +  "a dvd b \<longleftrightarrow> b mod a = 0"
    2.64 +  by (simp add: mod_eq_0_iff_dvd)
    2.65 +
    2.66 +lemma dvd_mod_iff: 
    2.67 +  assumes "c dvd b"
    2.68 +  shows "c dvd a mod b \<longleftrightarrow> c dvd a"
    2.69 +proof -
    2.70 +  from assms have "(c dvd a mod b) \<longleftrightarrow> (c dvd ((a div b) * b + a mod b))" 
    2.71 +    by (simp add: dvd_add_right_iff)
    2.72 +  also have "(a div b) * b + a mod b = a"
    2.73 +    using div_mult_mod_eq [of a b] by simp
    2.74 +  finally show ?thesis .
    2.75 +qed
    2.76 +
    2.77 +lemma dvd_mod_imp_dvd:
    2.78 +  assumes "c dvd a mod b" and "c dvd b"
    2.79 +  shows "c dvd a"
    2.80 +  using assms dvd_mod_iff [of c b a] by simp
    2.81 +
    2.82 +end
    2.83 +
    2.84 +class idom_modulo = idom + semidom_modulo
    2.85 +begin
    2.86 +
    2.87 +subclass idom_divide ..
    2.88 +
    2.89 +lemma div_diff [simp]:
    2.90 +  "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> (a - b) div c = a div c - b div c"
    2.91 +  using div_add [of _  _ "- b"] by (simp add: dvd_neg_div)
    2.92 +
    2.93 +end
    2.94 +
    2.95 +
    2.96 +subsection \<open>Quotient and remainder in integral domains with additional properties\<close>
    2.97 +
    2.98 +class semiring_div = semidom_modulo +
    2.99 +  assumes div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
   2.100      and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
   2.101  begin
   2.102  
   2.103 -subclass algebraic_semidom
   2.104 -proof
   2.105 -  fix b a
   2.106 -  assume "b \<noteq> 0"
   2.107 -  then show "a * b div b = a"
   2.108 -    using div_mult_self1 [of b 0 a] by (simp add: ac_simps div_0)
   2.109 -qed (simp add: div_by_0)
   2.110 -
   2.111 -text \<open>@{const divide} and @{const modulo}\<close>
   2.112 -
   2.113 -lemma mod_by_0 [simp]: "a mod 0 = a"
   2.114 -  using div_mult_mod_eq [of a zero] by simp
   2.115 -
   2.116 -lemma mod_0 [simp]: "0 mod a = 0"
   2.117 -  using div_mult_mod_eq [of zero a] div_0 by simp
   2.118 -
   2.119  lemma div_mult_self2 [simp]:
   2.120    assumes "b \<noteq> 0"
   2.121    shows "(a + b * c) div b = c + a div b"
   2.122 @@ -86,18 +144,6 @@
   2.123    "a * b mod b = 0"
   2.124    using mod_mult_self1 [of 0 a b] by simp
   2.125  
   2.126 -lemma mod_by_1 [simp]:
   2.127 -  "a mod 1 = 0"
   2.128 -proof -
   2.129 -  from div_mult_mod_eq [of a one] div_by_1 have "a + a mod 1 = a" by simp
   2.130 -  then have "a + a mod 1 = a + 0" by simp
   2.131 -  then show ?thesis by (rule add_left_imp_eq)
   2.132 -qed
   2.133 -
   2.134 -lemma mod_self [simp]:
   2.135 -  "a mod a = 0"
   2.136 -  using mod_mult_self2_is_0 [of 1] by simp
   2.137 -
   2.138  lemma div_add_self1:
   2.139    assumes "b \<noteq> 0"
   2.140    shows "(b + a) div b = a div b + 1"
   2.141 @@ -116,31 +162,6 @@
   2.142    "(a + b) mod b = a mod b"
   2.143    using mod_mult_self1 [of a 1 b] by simp
   2.144  
   2.145 -lemma dvd_imp_mod_0 [simp]:
   2.146 -  assumes "a dvd b"
   2.147 -  shows "b mod a = 0"
   2.148 -proof -
   2.149 -  from assms obtain c where "b = a * c" ..
   2.150 -  then have "b mod a = a * c mod a" by simp
   2.151 -  then show "b mod a = 0" by simp
   2.152 -qed
   2.153 -
   2.154 -lemma mod_eq_0_iff_dvd:
   2.155 -  "a mod b = 0 \<longleftrightarrow> b dvd a"
   2.156 -proof
   2.157 -  assume "b dvd a"
   2.158 -  then show "a mod b = 0" by simp
   2.159 -next
   2.160 -  assume "a mod b = 0"
   2.161 -  with div_mult_mod_eq [of a b] have "a div b * b = a" by simp
   2.162 -  then have "a = b * (a div b)" by (simp add: ac_simps)
   2.163 -  then show "b dvd a" ..
   2.164 -qed
   2.165 -
   2.166 -lemma dvd_eq_mod_eq_0 [nitpick_unfold, code]:
   2.167 -  "a dvd b \<longleftrightarrow> b mod a = 0"
   2.168 -  by (simp add: mod_eq_0_iff_dvd)
   2.169 -
   2.170  lemma mod_div_trivial [simp]:
   2.171    "a mod b div b = 0"
   2.172  proof (cases "b = 0")
   2.173 @@ -168,15 +189,6 @@
   2.174    finally show ?thesis .
   2.175  qed
   2.176  
   2.177 -lemma dvd_mod_imp_dvd:
   2.178 -  assumes "k dvd m mod n" and "k dvd n"
   2.179 -  shows "k dvd m"
   2.180 -proof -
   2.181 -  from assms have "k dvd (m div n) * n + m mod n"
   2.182 -    by (simp only: dvd_add dvd_mult)
   2.183 -  then show ?thesis by (simp add: div_mult_mod_eq)
   2.184 -qed
   2.185 -
   2.186  text \<open>Addition respects modular equivalence.\<close>
   2.187  
   2.188  lemma mod_add_left_eq: \<comment> \<open>FIXME reorient\<close>
   2.189 @@ -319,31 +331,6 @@
   2.190  lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
   2.191    unfolding dvd_def by (auto simp add: mod_mult_mult1)
   2.192  
   2.193 -lemma dvd_mod_iff: "k dvd n \<Longrightarrow> k dvd (m mod n) \<longleftrightarrow> k dvd m"
   2.194 -by (blast intro: dvd_mod_imp_dvd dvd_mod)
   2.195 -
   2.196 -lemma div_div_eq_right:
   2.197 -  assumes "c dvd b" "b dvd a"
   2.198 -  shows   "a div (b div c) = a div b * c"
   2.199 -proof -
   2.200 -  from assms have "a div b * c = (a * c) div b"
   2.201 -    by (subst dvd_div_mult) simp_all
   2.202 -  also from assms have "\<dots> = (a * c) div ((b div c) * c)" by simp
   2.203 -  also have "a * c div (b div c * c) = a div (b div c)"
   2.204 -    by (cases "c = 0") simp_all
   2.205 -  finally show ?thesis ..
   2.206 -qed
   2.207 -
   2.208 -lemma div_div_div_same:
   2.209 -  assumes "d dvd a" "d dvd b" "b dvd a"
   2.210 -  shows   "(a div d) div (b div d) = a div b"
   2.211 -  using assms by (subst dvd_div_mult2_eq [symmetric]) simp_all
   2.212 -
   2.213 -lemma cancel_div_mod_rules:
   2.214 -  "((a div b) * b + a mod b) + c = a + c"
   2.215 -  "(b * (a div b) + a mod b) + c = a + c"
   2.216 -  by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
   2.217 -
   2.218  end
   2.219  
   2.220  class ring_div = comm_ring_1 + semiring_div
   2.221 @@ -394,28 +381,6 @@
   2.222    shows "(a - b) mod c = (a' - b') mod c"
   2.223    using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"] by simp
   2.224  
   2.225 -lemma dvd_neg_div: "y dvd x \<Longrightarrow> -x div y = - (x div y)"
   2.226 -apply (case_tac "y = 0") apply simp
   2.227 -apply (auto simp add: dvd_def)
   2.228 -apply (subgoal_tac "-(y * k) = y * - k")
   2.229 - apply (simp only:)
   2.230 - apply (erule nonzero_mult_div_cancel_left)
   2.231 -apply simp
   2.232 -done
   2.233 -
   2.234 -lemma dvd_div_neg: "y dvd x \<Longrightarrow> x div -y = - (x div y)"
   2.235 -apply (case_tac "y = 0") apply simp
   2.236 -apply (auto simp add: dvd_def)
   2.237 -apply (subgoal_tac "y * k = -y * -k")
   2.238 - apply (erule ssubst, rule nonzero_mult_div_cancel_left)
   2.239 - apply simp
   2.240 -apply simp
   2.241 -done
   2.242 -
   2.243 -lemma div_diff [simp]:
   2.244 -  "z dvd x \<Longrightarrow> z dvd y \<Longrightarrow> (x - y) div z = x div z - y div z"
   2.245 -  using div_add [of _ _ "- y"] by (simp add: dvd_neg_div)
   2.246 -
   2.247  lemma div_minus_minus [simp]: "(-a) div (-b) = a div b"
   2.248    using div_mult_mult1 [of "- 1" a b]
   2.249    unfolding neg_equal_0_iff_equal by simp
   2.250 @@ -446,7 +411,7 @@
   2.251  end
   2.252  
   2.253  
   2.254 -subsubsection \<open>Parity and division\<close>
   2.255 +subsection \<open>Parity\<close>
   2.256  
   2.257  class semiring_div_parity = semiring_div + comm_semiring_1_cancel + numeral +
   2.258    assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
   2.259 @@ -532,7 +497,7 @@
   2.260  end
   2.261  
   2.262  
   2.263 -subsection \<open>Generic numeral division with a pragmatic type class\<close>
   2.264 +subsection \<open>Numeral division with a pragmatic type class\<close>
   2.265  
   2.266  text \<open>
   2.267    The following type class contains everything necessary to formulate
   2.268 @@ -826,8 +791,10 @@
   2.269        from m n have "Suc m = q' * n + Suc r'" by simp
   2.270        with True show ?thesis by blast
   2.271      next
   2.272 -      case False then have "n \<le> Suc r'" by auto
   2.273 -      moreover from n have "Suc r' \<le> n" by auto
   2.274 +      case False then have "n \<le> Suc r'"
   2.275 +        by (simp add: not_less)
   2.276 +      moreover from n have "Suc r' \<le> n"
   2.277 +        by (simp add: Suc_le_eq)
   2.278        ultimately have "n = Suc r'" by auto
   2.279        with m have "Suc m = Suc q' * n + 0" by simp
   2.280        with \<open>n \<noteq> 0\<close> show ?thesis by blast
   2.281 @@ -855,7 +822,7 @@
   2.282    apply (auto simp add: add_mult_distrib)
   2.283    done
   2.284    from \<open>n \<noteq> 0\<close> assms have *: "fst qr = fst qr'"
   2.285 -    by (auto simp add: divmod_nat_rel_def intro: order_antisym dest: aux sym)
   2.286 +    by (auto simp add: divmod_nat_rel_def intro: order_antisym dest: aux sym split: if_splits)
   2.287    with assms have "snd qr = snd qr'"
   2.288      by (simp add: divmod_nat_rel_def)
   2.289    with * show ?thesis by (cases qr, cases qr') simp
   2.290 @@ -884,10 +851,10 @@
   2.291    using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)
   2.292  
   2.293  qualified lemma divmod_nat_zero: "divmod_nat m 0 = (0, m)"
   2.294 -  by (simp add: Divides.divmod_nat_unique divmod_nat_rel_def)
   2.295 +  by (simp add: divmod_nat_unique divmod_nat_rel_def)
   2.296  
   2.297  qualified lemma divmod_nat_zero_left: "divmod_nat 0 n = (0, 0)"
   2.298 -  by (simp add: Divides.divmod_nat_unique divmod_nat_rel_def)
   2.299 +  by (simp add: divmod_nat_unique divmod_nat_rel_def)
   2.300  
   2.301  qualified lemma divmod_nat_base: "m < n \<Longrightarrow> divmod_nat m n = (0, m)"
   2.302    by (simp add: divmod_nat_unique divmod_nat_rel_def)
   2.303 @@ -899,19 +866,31 @@
   2.304    have "divmod_nat_rel (m - n) n (divmod_nat (m - n) n)"
   2.305      by (fact divmod_nat_rel_divmod_nat)
   2.306    then show "divmod_nat_rel m n (apfst Suc (divmod_nat (m - n) n))"
   2.307 -    unfolding divmod_nat_rel_def using assms by auto
   2.308 +    unfolding divmod_nat_rel_def using assms
   2.309 +      by (auto split: if_splits simp add: algebra_simps)
   2.310  qed
   2.311  
   2.312  end
   2.313 -  
   2.314 -instantiation nat :: semiring_div
   2.315 +
   2.316 +instantiation nat :: "{semidom_modulo, normalization_semidom}"
   2.317  begin
   2.318  
   2.319 -definition divide_nat where
   2.320 -  div_nat_def: "m div n = fst (Divides.divmod_nat m n)"
   2.321 -
   2.322 -definition modulo_nat where
   2.323 -  mod_nat_def: "m mod n = snd (Divides.divmod_nat m n)"
   2.324 +definition normalize_nat :: "nat \<Rightarrow> nat"
   2.325 +  where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
   2.326 +
   2.327 +definition unit_factor_nat :: "nat \<Rightarrow> nat"
   2.328 +  where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
   2.329 +
   2.330 +lemma unit_factor_simps [simp]:
   2.331 +  "unit_factor 0 = (0::nat)"
   2.332 +  "unit_factor (Suc n) = 1"
   2.333 +  by (simp_all add: unit_factor_nat_def)
   2.334 +
   2.335 +definition divide_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   2.336 +  where div_nat_def: "m div n = fst (Divides.divmod_nat m n)"
   2.337 +
   2.338 +definition modulo_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   2.339 +  where mod_nat_def: "m mod n = snd (Divides.divmod_nat m n)"
   2.340  
   2.341  lemma fst_divmod_nat [simp]:
   2.342    "fst (Divides.divmod_nat m n) = m div n"
   2.343 @@ -928,15 +907,18 @@
   2.344  lemma div_nat_unique:
   2.345    assumes "divmod_nat_rel m n (q, r)"
   2.346    shows "m div n = q"
   2.347 -  using assms by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
   2.348 +  using assms
   2.349 +  by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
   2.350  
   2.351  lemma mod_nat_unique:
   2.352    assumes "divmod_nat_rel m n (q, r)"
   2.353    shows "m mod n = r"
   2.354 -  using assms by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
   2.355 +  using assms
   2.356 +  by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
   2.357  
   2.358  lemma divmod_nat_rel: "divmod_nat_rel m n (m div n, m mod n)"
   2.359 -  using Divides.divmod_nat_rel_divmod_nat by (simp add: divmod_nat_div_mod)
   2.360 +  using Divides.divmod_nat_rel_divmod_nat
   2.361 +  by (simp add: divmod_nat_div_mod)
   2.362  
   2.363  text \<open>The ''recursion'' equations for @{const divide} and @{const modulo}\<close>
   2.364  
   2.365 @@ -964,11 +946,40 @@
   2.366    shows "m mod n = (m - n) mod n"
   2.367    using assms Divides.divmod_nat_step by (cases "n = 0") (simp_all add: prod_eq_iff)
   2.368  
   2.369 +lemma mod_less_divisor [simp]:
   2.370 +  fixes m n :: nat
   2.371 +  assumes "n > 0"
   2.372 +  shows "m mod n < n"
   2.373 +  using assms divmod_nat_rel [of m n] unfolding divmod_nat_rel_def
   2.374 +  by (auto split: if_splits)
   2.375 +
   2.376 +lemma mod_le_divisor [simp]:
   2.377 +  fixes m n :: nat
   2.378 +  assumes "n > 0"
   2.379 +  shows "m mod n \<le> n"
   2.380 +proof (rule less_imp_le)
   2.381 +  from assms show "m mod n < n"
   2.382 +    by simp
   2.383 +qed
   2.384 +
   2.385  instance proof
   2.386    fix m n :: nat
   2.387    show "m div n * n + m mod n = m"
   2.388      using divmod_nat_rel [of m n] by (simp add: divmod_nat_rel_def)
   2.389  next
   2.390 +  fix n :: nat show "n div 0 = 0"
   2.391 +    by (simp add: div_nat_def Divides.divmod_nat_zero)
   2.392 +next
   2.393 +  fix m n :: nat
   2.394 +  assume "n \<noteq> 0"
   2.395 +  then show "m * n div n = m"
   2.396 +    by (auto simp add: divmod_nat_rel_def intro: div_nat_unique [of _ _ _ 0])
   2.397 +qed (simp_all add: unit_factor_nat_def)
   2.398 +
   2.399 +end
   2.400 +
   2.401 +instance nat :: semiring_div
   2.402 +proof
   2.403    fix m n q :: nat
   2.404    assume "n \<noteq> 0"
   2.405    then show "(q + m * n) div n = m + q div n"
   2.406 @@ -976,48 +987,33 @@
   2.407  next
   2.408    fix m n q :: nat
   2.409    assume "m \<noteq> 0"
   2.410 -  hence "\<And>a b. divmod_nat_rel n q (a, b) \<Longrightarrow> divmod_nat_rel (m * n) (m * q) (a, m * b)"
   2.411 -    unfolding divmod_nat_rel_def
   2.412 -    by (auto split: if_split_asm, simp_all add: algebra_simps)
   2.413 -  moreover from divmod_nat_rel have "divmod_nat_rel n q (n div q, n mod q)" .
   2.414 -  ultimately have "divmod_nat_rel (m * n) (m * q) (n div q, m * (n mod q))" .
   2.415 -  thus "(m * n) div (m * q) = n div q" by (rule div_nat_unique)
   2.416 -next
   2.417 -  fix n :: nat show "n div 0 = 0"
   2.418 -    by (simp add: div_nat_def Divides.divmod_nat_zero)
   2.419 -next
   2.420 -  fix n :: nat show "0 div n = 0"
   2.421 -    by (simp add: div_nat_def Divides.divmod_nat_zero_left)
   2.422 +  then have "divmod_nat_rel (m * n) (m * q) (n div q, m * (n mod q))"
   2.423 +    using div_mult_mod_eq [of n q]
   2.424 +    by (auto simp add: divmod_nat_rel_def algebra_simps distrib_left [symmetric] simp del: distrib_left)
   2.425 +  then show "(m * n) div (m * q) = n div q"
   2.426 +    by (rule div_nat_unique)
   2.427  qed
   2.428  
   2.429 -end
   2.430 -
   2.431 -instantiation nat :: normalization_semidom
   2.432 -begin
   2.433 -
   2.434 -definition normalize_nat
   2.435 -  where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
   2.436 -
   2.437 -definition unit_factor_nat
   2.438 -  where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
   2.439 -
   2.440 -lemma unit_factor_simps [simp]:
   2.441 -  "unit_factor 0 = (0::nat)"
   2.442 -  "unit_factor (Suc n) = 1"
   2.443 -  by (simp_all add: unit_factor_nat_def)
   2.444 -
   2.445 -instance
   2.446 -  by standard (simp_all add: unit_factor_nat_def)
   2.447 -  
   2.448 -end
   2.449 -
   2.450 -lemma divmod_nat_if [code]:
   2.451 -  "Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
   2.452 -    let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
   2.453 -  by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
   2.454 +lemma div_by_Suc_0 [simp]:
   2.455 +  "m div Suc 0 = m"
   2.456 +  using div_by_1 [of m] by simp
   2.457 +
   2.458 +lemma mod_by_Suc_0 [simp]:
   2.459 +  "m mod Suc 0 = 0"
   2.460 +  using mod_by_1 [of m] by simp
   2.461 +
   2.462 +lemma mod_greater_zero_iff_not_dvd:
   2.463 +  fixes m n :: nat
   2.464 +  shows "m mod n > 0 \<longleftrightarrow> \<not> n dvd m"
   2.465 +  by (simp add: dvd_eq_mod_eq_0)
   2.466  
   2.467  text \<open>Simproc for cancelling @{const divide} and @{const modulo}\<close>
   2.468  
   2.469 +lemma (in semiring_modulo) cancel_div_mod_rules:
   2.470 +  "((a div b) * b + a mod b) + c = a + c"
   2.471 +  "(b * (a div b) + a mod b) + c = a + c"
   2.472 +  by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
   2.473 +
   2.474  ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
   2.475  
   2.476  ML \<open>
   2.477 @@ -1048,7 +1044,13 @@
   2.478  )
   2.479  \<close>
   2.480  
   2.481 -simproc_setup cancel_div_mod_nat ("(m::nat) + n") = \<open>K Cancel_Div_Mod_Nat.proc\<close>
   2.482 +simproc_setup cancel_div_mod_nat ("(m::nat) + n") =
   2.483 +  \<open>K Cancel_Div_Mod_Nat.proc\<close>
   2.484 +
   2.485 +lemma divmod_nat_if [code]:
   2.486 +  "Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
   2.487 +    let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
   2.488 +  by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
   2.489  
   2.490  
   2.491  subsubsection \<open>Quotient\<close>
   2.492 @@ -1077,16 +1079,11 @@
   2.493  qed
   2.494  
   2.495  lemma div_eq_0_iff: "(a div b::nat) = 0 \<longleftrightarrow> a < b \<or> b = 0"
   2.496 -  by (metis div_less div_positive div_by_0 gr0I less_numeral_extra(3) not_less)
   2.497 +  by auto (metis div_positive less_numeral_extra(3) not_less)
   2.498 +
   2.499  
   2.500  subsubsection \<open>Remainder\<close>
   2.501  
   2.502 -lemma mod_less_divisor [simp]:
   2.503 -  fixes m n :: nat
   2.504 -  assumes "n > 0"
   2.505 -  shows "m mod n < (n::nat)"
   2.506 -  using assms divmod_nat_rel [of m n] unfolding divmod_nat_rel_def by auto
   2.507 -
   2.508  lemma mod_Suc_le_divisor [simp]:
   2.509    "m mod Suc n \<le> n"
   2.510    using mod_less_divisor [of "Suc n" m] by arith
   2.511 @@ -1105,13 +1102,6 @@
   2.512  lemma mod_if: "m mod (n::nat) = (if m < n then m else (m - n) mod n)"
   2.513  by (simp add: le_mod_geq)
   2.514  
   2.515 -lemma mod_by_Suc_0 [simp]: "m mod Suc 0 = 0"
   2.516 -by (induct m) (simp_all add: mod_geq)
   2.517 -
   2.518 -lemma mod_le_divisor[simp]: "0 < n \<Longrightarrow> m mod n \<le> (n::nat)"
   2.519 -  apply (drule mod_less_divisor [where m = m])
   2.520 -  apply simp
   2.521 -  done
   2.522  
   2.523  subsubsection \<open>Quotient and Remainder\<close>
   2.524  
   2.525 @@ -1180,25 +1170,16 @@
   2.526  
   2.527  subsubsection \<open>Further Facts about Quotient and Remainder\<close>
   2.528  
   2.529 -lemma div_by_Suc_0 [simp]:
   2.530 -  "m div Suc 0 = m"
   2.531 -  using div_by_1 [of m] by simp
   2.532 -
   2.533 -(* Monotonicity of div in first argument *)
   2.534 -lemma div_le_mono [rule_format (no_asm)]:
   2.535 -    "\<forall>m::nat. m \<le> n --> (m div k) \<le> (n div k)"
   2.536 -apply (case_tac "k=0", simp)
   2.537 -apply (induct "n" rule: nat_less_induct, clarify)
   2.538 -apply (case_tac "n<k")
   2.539 -(* 1  case n<k *)
   2.540 -apply simp
   2.541 -(* 2  case n >= k *)
   2.542 -apply (case_tac "m<k")
   2.543 -(* 2.1  case m<k *)
   2.544 -apply simp
   2.545 -(* 2.2  case m>=k *)
   2.546 -apply (simp add: div_geq diff_le_mono)
   2.547 -done
   2.548 +lemma div_le_mono:
   2.549 +  fixes m n k :: nat
   2.550 +  assumes "m \<le> n"
   2.551 +  shows "m div k \<le> n div k"
   2.552 +proof -
   2.553 +  from assms obtain q where "n = m + q"
   2.554 +    by (auto simp add: le_iff_add)
   2.555 +  then show ?thesis
   2.556 +    by (simp add: div_add1_eq [of m q k])
   2.557 +qed
   2.558  
   2.559  (* Antimonotonicity of div in second argument *)
   2.560  lemma div_le_mono2: "!!m::nat. [| 0<m; m\<le>n |] ==> (k div n) \<le> (k div m)"
   2.561 @@ -1519,11 +1500,6 @@
   2.562  
   2.563  declare Suc_times_mod_eq [of "numeral w", simp] for w
   2.564  
   2.565 -lemma mod_greater_zero_iff_not_dvd:
   2.566 -  fixes m n :: nat
   2.567 -  shows "m mod n > 0 \<longleftrightarrow> \<not> n dvd m"
   2.568 -  by (simp add: dvd_eq_mod_eq_0)
   2.569 -
   2.570  lemma Suc_div_le_mono [simp]: "n div k \<le> (Suc n) div k"
   2.571  by (simp add: div_le_mono)
   2.572  
   2.573 @@ -1643,6 +1619,9 @@
   2.574  
   2.575  subsection \<open>Division on @{typ int}\<close>
   2.576  
   2.577 +context
   2.578 +begin
   2.579 +
   2.580  definition divmod_int_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" \<comment> \<open>definition of quotient and remainder\<close>
   2.581    where "divmod_int_rel a b = (\<lambda>(q, r). a = b * q + r \<and>
   2.582      (if 0 < b then 0 \<le> r \<and> r < b else if b < 0 then b < r \<and> r \<le> 0 else q = 0))"
   2.583 @@ -1678,10 +1657,18 @@
   2.584  apply (blast intro: unique_quotient)
   2.585  done
   2.586  
   2.587 -instantiation int :: modulo
   2.588 +end
   2.589 +
   2.590 +instantiation int :: "{idom_modulo, normalization_semidom}"
   2.591  begin
   2.592  
   2.593 -definition divide_int
   2.594 +definition normalize_int :: "int \<Rightarrow> int"
   2.595 +  where [simp]: "normalize = (abs :: int \<Rightarrow> int)"
   2.596 +
   2.597 +definition unit_factor_int :: "int \<Rightarrow> int"
   2.598 +  where [simp]: "unit_factor = (sgn :: int \<Rightarrow> int)"
   2.599 +
   2.600 +definition divide_int :: "int \<Rightarrow> int \<Rightarrow> int"
   2.601    where "k div l = (if l = 0 \<or> k = 0 then 0
   2.602      else if k > 0 \<and> l > 0 \<or> k < 0 \<and> l < 0
   2.603        then int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
   2.604 @@ -1689,32 +1676,35 @@
   2.605          if l dvd k then - int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
   2.606          else - int (Suc (nat \<bar>k\<bar> div nat \<bar>l\<bar>)))"
   2.607  
   2.608 -definition modulo_int
   2.609 +definition modulo_int :: "int \<Rightarrow> int \<Rightarrow> int"
   2.610    where "k mod l = (if l = 0 then k else if l dvd k then 0
   2.611      else if k > 0 \<and> l > 0 \<or> k < 0 \<and> l < 0
   2.612        then sgn l * int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)
   2.613        else sgn l * (\<bar>l\<bar> - int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)))"
   2.614  
   2.615 -instance ..      
   2.616 -
   2.617 -end
   2.618 -
   2.619  lemma divmod_int_rel:
   2.620    "divmod_int_rel k l (k div l, k mod l)"
   2.621 -  unfolding divmod_int_rel_def divide_int_def modulo_int_def
   2.622 -  apply (cases k rule: int_cases3)
   2.623 -  apply (simp add: mod_greater_zero_iff_not_dvd not_le algebra_simps)
   2.624 -  apply (cases l rule: int_cases3)
   2.625 -  apply (simp add: mod_greater_zero_iff_not_dvd not_le algebra_simps)
   2.626 -  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])
   2.627 -  apply (cases l rule: int_cases3)
   2.628 -  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])
   2.629 -  done
   2.630 -
   2.631 -instantiation int :: ring_div
   2.632 -begin
   2.633 -
   2.634 -subsubsection \<open>Uniqueness and Monotonicity of Quotients and Remainders\<close>
   2.635 +proof (cases k rule: int_cases3)
   2.636 +  case zero
   2.637 +  then show ?thesis
   2.638 +    by (simp add: divmod_int_rel_def divide_int_def modulo_int_def)
   2.639 +next
   2.640 +  case (pos n)
   2.641 +  then show ?thesis
   2.642 +    using div_mult_mod_eq [of n]
   2.643 +    by (cases l rule: int_cases3)
   2.644 +      (auto simp del: of_nat_mult of_nat_add
   2.645 +        simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
   2.646 +        divmod_int_rel_def divide_int_def modulo_int_def int_dvd_iff)
   2.647 +next
   2.648 +  case (neg n)
   2.649 +  then show ?thesis
   2.650 +    using div_mult_mod_eq [of n]
   2.651 +    by (cases l rule: int_cases3)
   2.652 +      (auto simp del: of_nat_mult of_nat_add
   2.653 +        simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
   2.654 +        divmod_int_rel_def divide_int_def modulo_int_def int_dvd_iff)
   2.655 +qed
   2.656  
   2.657  lemma divmod_int_unique:
   2.658    assumes "divmod_int_rel k l (q, r)"
   2.659 @@ -1722,42 +1712,21 @@
   2.660    using assms divmod_int_rel [of k l]
   2.661    using unique_quotient [of k l] unique_remainder [of k l]
   2.662    by auto
   2.663 -  
   2.664 -instance
   2.665 -proof
   2.666 -  fix a b :: int
   2.667 -  show "a div b * b + a mod b = a"
   2.668 -    using divmod_int_rel [of a b]
   2.669 -    unfolding divmod_int_rel_def by (simp add: mult.commute)
   2.670 -next
   2.671 -  fix a b c :: int
   2.672 -  assume "b \<noteq> 0"
   2.673 -  hence "divmod_int_rel (a + c * b) b (c + a div b, a mod b)"
   2.674 -    using divmod_int_rel [of a b]
   2.675 -    unfolding divmod_int_rel_def by (auto simp: algebra_simps)
   2.676 -  thus "(a + c * b) div b = c + a div b"
   2.677 -    by (rule div_int_unique)
   2.678 +
   2.679 +instance proof
   2.680 +  fix k l :: int
   2.681 +  show "k div l * l + k mod l = k"
   2.682 +    using divmod_int_rel [of k l]
   2.683 +    unfolding divmod_int_rel_def by (simp add: ac_simps)
   2.684  next
   2.685 -  fix a b c :: int
   2.686 -  assume c: "c \<noteq> 0"
   2.687 -  have "\<And>q r. divmod_int_rel a b (q, r)
   2.688 -    \<Longrightarrow> divmod_int_rel (c * a) (c * b) (q, c * r)"
   2.689 -    unfolding divmod_int_rel_def
   2.690 -    by (rule linorder_cases [of 0 b])
   2.691 -      (use c in \<open>auto simp: algebra_simps
   2.692 -      mult_less_0_iff zero_less_mult_iff mult_strict_right_mono
   2.693 -      mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff\<close>)
   2.694 -  hence "divmod_int_rel (c * a) (c * b) (a div b, c * (a mod b))"
   2.695 -    using divmod_int_rel [of a b] .
   2.696 -  thus "(c * a) div (c * b) = a div b"
   2.697 -    by (rule div_int_unique)
   2.698 -next
   2.699 -  fix a :: int show "a div 0 = 0"
   2.700 +  fix k :: int show "k div 0 = 0"
   2.701      by (rule div_int_unique, simp add: divmod_int_rel_def)
   2.702  next
   2.703 -  fix a :: int show "0 div a = 0"
   2.704 -    by (rule div_int_unique, auto simp add: divmod_int_rel_def)
   2.705 -qed
   2.706 +  fix k l :: int
   2.707 +  assume "l \<noteq> 0"
   2.708 +  then show "k * l div l = k"
   2.709 +    by (auto simp add: divmod_int_rel_def ac_simps intro: div_int_unique [of _ _ _ 0])
   2.710 +qed (simp_all add: sgn_mult mult_sgn_abs abs_sgn_eq)
   2.711  
   2.712  end
   2.713  
   2.714 @@ -1765,36 +1734,30 @@
   2.715    "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
   2.716    by auto
   2.717  
   2.718 -instantiation int :: normalization_semidom
   2.719 -begin
   2.720 -
   2.721 -definition normalize_int
   2.722 -  where [simp]: "normalize = (abs :: int \<Rightarrow> int)"
   2.723 -
   2.724 -definition unit_factor_int
   2.725 -  where [simp]: "unit_factor = (sgn :: int \<Rightarrow> int)"
   2.726 -
   2.727 -instance
   2.728 +instance int :: ring_div
   2.729  proof
   2.730 -  fix k :: int
   2.731 -  assume "k \<noteq> 0"
   2.732 -  then have "\<bar>sgn k\<bar> = 1"
   2.733 -    by (cases "0::int" k rule: linorder_cases) simp_all
   2.734 -  then show "is_unit (unit_factor k)"
   2.735 -    by simp
   2.736 -qed (simp_all add: sgn_mult mult_sgn_abs)
   2.737 -  
   2.738 -end
   2.739 -  
   2.740 -text\<open>Basic laws about division and remainder\<close>
   2.741 -
   2.742 -lemma zdiv_int: "int (a div b) = int a div int b"
   2.743 -  by (simp add: divide_int_def)
   2.744 -
   2.745 -lemma zmod_int: "int (a mod b) = int a mod int b"
   2.746 -  by (simp add: modulo_int_def int_dvd_iff)
   2.747 -  
   2.748 -text \<open>Tool setup\<close>
   2.749 +  fix k l s :: int
   2.750 +  assume "l \<noteq> 0"
   2.751 +  then have "divmod_int_rel (k + s * l) l (s + k div l, k mod l)"
   2.752 +    using divmod_int_rel [of k l]
   2.753 +    unfolding divmod_int_rel_def by (auto simp: algebra_simps)
   2.754 +  then show "(k + s * l) div l = s + k div l"
   2.755 +    by (rule div_int_unique)
   2.756 +next
   2.757 +  fix k l s :: int
   2.758 +  assume "s \<noteq> 0"
   2.759 +  have "\<And>q r. divmod_int_rel k l (q, r)
   2.760 +    \<Longrightarrow> divmod_int_rel (s * k) (s * l) (q, s * r)"
   2.761 +    unfolding divmod_int_rel_def
   2.762 +    by (rule linorder_cases [of 0 l])
   2.763 +      (use \<open>s \<noteq> 0\<close> in \<open>auto simp: algebra_simps
   2.764 +      mult_less_0_iff zero_less_mult_iff mult_strict_right_mono
   2.765 +      mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff\<close>)
   2.766 +  then have "divmod_int_rel (s * k) (s * l) (k div l, s * (k mod l))"
   2.767 +    using divmod_int_rel [of k l] .
   2.768 +  then show "(s * k) div (s * l) = k div l"
   2.769 +    by (rule div_int_unique)
   2.770 +qed
   2.771  
   2.772  ML \<open>
   2.773  structure Cancel_Div_Mod_Int = Cancel_Div_Mod
   2.774 @@ -1807,12 +1770,22 @@
   2.775  
   2.776    val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
   2.777  
   2.778 -  val prove_eq_sums = Arith_Data.prove_conv2 all_tac
   2.779 -    (Arith_Data.simp_all_tac @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps})
   2.780 +  val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
   2.781 +    @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps})
   2.782  )
   2.783  \<close>
   2.784  
   2.785 -simproc_setup cancel_div_mod_int ("(k::int) + l") = \<open>K Cancel_Div_Mod_Int.proc\<close>
   2.786 +simproc_setup cancel_div_mod_int ("(k::int) + l") =
   2.787 +  \<open>K Cancel_Div_Mod_Int.proc\<close>
   2.788 +
   2.789 +
   2.790 +text\<open>Basic laws about division and remainder\<close>
   2.791 +
   2.792 +lemma zdiv_int: "int (a div b) = int a div int b"
   2.793 +  by (simp add: divide_int_def)
   2.794 +
   2.795 +lemma zmod_int: "int (a mod b) = int a mod int b"
   2.796 +  by (simp add: modulo_int_def int_dvd_iff)
   2.797  
   2.798  lemma pos_mod_conj: "(0::int) < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b"
   2.799    using divmod_int_rel [of a b]
   2.800 @@ -1887,10 +1860,15 @@
   2.801  apply (blast intro: divmod_int_rel [THEN zminus1_lemma, THEN mod_int_unique])
   2.802  done
   2.803  
   2.804 -lemma zmod_zminus1_not_zero:
   2.805 +lemma zmod_zminus1_not_zero: -- \<open>FIXME generalize\<close>
   2.806    fixes k l :: int
   2.807    shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
   2.808 -  unfolding zmod_zminus1_eq_if by auto
   2.809 +  by (simp add: mod_eq_0_iff_dvd)
   2.810 +
   2.811 +lemma zmod_zminus2_not_zero: -- \<open>FIXME generalize\<close>
   2.812 +  fixes k l :: int
   2.813 +  shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
   2.814 +  by (simp add: mod_eq_0_iff_dvd)
   2.815  
   2.816  lemma zdiv_zminus2_eq_if:
   2.817       "b \<noteq> (0::int)
   2.818 @@ -1902,11 +1880,6 @@
   2.819       "a mod (-b::int) = (if a mod b = 0 then 0 else  (a mod b) - b)"
   2.820  by (simp add: zmod_zminus1_eq_if mod_minus_right)
   2.821  
   2.822 -lemma zmod_zminus2_not_zero:
   2.823 -  fixes k l :: int
   2.824 -  shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
   2.825 -  unfolding zmod_zminus2_eq_if by auto
   2.826 -
   2.827  
   2.828  subsubsection \<open>Monotonicity in the First Argument (Dividend)\<close>
   2.829  
   2.830 @@ -2666,6 +2639,4 @@
   2.831  
   2.832  declare minus_div_mult_eq_mod [symmetric, nitpick_unfold]
   2.833  
   2.834 -hide_fact (open) div_0 div_by_0
   2.835 -
   2.836  end
     3.1 --- a/src/HOL/Enum.thy	Sat Dec 17 15:22:13 2016 +0100
     3.2 +++ b/src/HOL/Enum.thy	Sat Dec 17 15:22:14 2016 +0100
     3.3 @@ -683,7 +683,7 @@
     3.4  
     3.5  instance finite_2 :: complete_linorder ..
     3.6  
     3.7 -instantiation finite_2 :: "{field, ring_div, idom_abs_sgn}" begin
     3.8 +instantiation finite_2 :: "{field, idom_abs_sgn}" begin
     3.9  definition [simp]: "0 = a\<^sub>1"
    3.10  definition [simp]: "1 = a\<^sub>2"
    3.11  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)"
    3.12 @@ -693,19 +693,33 @@
    3.13  definition "inverse = (\<lambda>x :: finite_2. x)"
    3.14  definition "divide = (op * :: finite_2 \<Rightarrow> _)"
    3.15  definition "abs = (\<lambda>x :: finite_2. x)"
    3.16 -definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
    3.17  definition "sgn = (\<lambda>x :: finite_2. x)"
    3.18  instance
    3.19 -by intro_classes
    3.20 -  (simp_all add: plus_finite_2_def uminus_finite_2_def minus_finite_2_def times_finite_2_def
    3.21 -       inverse_finite_2_def divide_finite_2_def abs_finite_2_def modulo_finite_2_def sgn_finite_2_def
    3.22 -     split: finite_2.splits)
    3.23 +  by standard
    3.24 +    (simp_all add: plus_finite_2_def uminus_finite_2_def minus_finite_2_def times_finite_2_def
    3.25 +      inverse_finite_2_def divide_finite_2_def abs_finite_2_def sgn_finite_2_def
    3.26 +      split: finite_2.splits)
    3.27  end
    3.28  
    3.29  lemma two_finite_2 [simp]:
    3.30    "2 = a\<^sub>1"
    3.31    by (simp add: numeral.simps plus_finite_2_def)
    3.32 -  
    3.33 +
    3.34 +lemma dvd_finite_2_unfold:
    3.35 +  "x dvd y \<longleftrightarrow> x = a\<^sub>2 \<or> y = a\<^sub>1"
    3.36 +  by (auto simp add: dvd_def times_finite_2_def split: finite_2.splits)
    3.37 +
    3.38 +instantiation finite_2 :: "{ring_div, normalization_semidom}" begin
    3.39 +definition [simp]: "normalize = (id :: finite_2 \<Rightarrow> _)"
    3.40 +definition [simp]: "unit_factor = (id :: finite_2 \<Rightarrow> _)"
    3.41 +definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
    3.42 +instance
    3.43 +  by standard
    3.44 +    (simp_all add: dvd_finite_2_unfold times_finite_2_def
    3.45 +      divide_finite_2_def modulo_finite_2_def split: finite_2.splits)
    3.46 +end
    3.47 +
    3.48 + 
    3.49  hide_const (open) a\<^sub>1 a\<^sub>2
    3.50  
    3.51  datatype (plugins only: code "quickcheck" extraction) finite_3 =
    3.52 @@ -736,6 +750,12 @@
    3.53  
    3.54  end
    3.55  
    3.56 +lemma finite_3_not_eq_unfold:
    3.57 +  "x \<noteq> a\<^sub>1 \<longleftrightarrow> x \<in> {a\<^sub>2, a\<^sub>3}"
    3.58 +  "x \<noteq> a\<^sub>2 \<longleftrightarrow> x \<in> {a\<^sub>1, a\<^sub>3}"
    3.59 +  "x \<noteq> a\<^sub>3 \<longleftrightarrow> x \<in> {a\<^sub>1, a\<^sub>2}"
    3.60 +  by (cases x; simp)+
    3.61 +
    3.62  instantiation finite_3 :: linorder
    3.63  begin
    3.64  
    3.65 @@ -806,7 +826,7 @@
    3.66  
    3.67  instance finite_3 :: complete_linorder ..
    3.68  
    3.69 -instantiation finite_3 :: "{field, ring_div, idom_abs_sgn}" begin
    3.70 +instantiation finite_3 :: "{field, idom_abs_sgn}" begin
    3.71  definition [simp]: "0 = a\<^sub>1"
    3.72  definition [simp]: "1 = a\<^sub>2"
    3.73  definition
    3.74 @@ -820,14 +840,33 @@
    3.75  definition "inverse = (\<lambda>x :: finite_3. x)" 
    3.76  definition "x div y = x * inverse (y :: finite_3)"
    3.77  definition "abs = (\<lambda>x. case x of a\<^sub>3 \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> x)"
    3.78 -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)"
    3.79  definition "sgn = (\<lambda>x :: finite_3. x)"
    3.80  instance
    3.81 -by intro_classes
    3.82 -  (simp_all add: plus_finite_3_def uminus_finite_3_def minus_finite_3_def times_finite_3_def
    3.83 -       inverse_finite_3_def divide_finite_3_def abs_finite_3_def modulo_finite_3_def sgn_finite_3_def
    3.84 -       less_finite_3_def
    3.85 -     split: finite_3.splits)
    3.86 +  by standard
    3.87 +    (simp_all add: plus_finite_3_def uminus_finite_3_def minus_finite_3_def times_finite_3_def
    3.88 +      inverse_finite_3_def divide_finite_3_def abs_finite_3_def sgn_finite_3_def
    3.89 +      less_finite_3_def
    3.90 +      split: finite_3.splits)
    3.91 +end
    3.92 +
    3.93 +lemma two_finite_3 [simp]:
    3.94 +  "2 = a\<^sub>3"
    3.95 +  by (simp add: numeral.simps plus_finite_3_def)
    3.96 +
    3.97 +lemma dvd_finite_3_unfold:
    3.98 +  "x dvd y \<longleftrightarrow> x = a\<^sub>2 \<or> x = a\<^sub>3 \<or> y = a\<^sub>1"
    3.99 +  by (cases x) (auto simp add: dvd_def times_finite_3_def split: finite_3.splits)
   3.100 +
   3.101 +instantiation finite_3 :: "{ring_div, normalization_semidom}" begin
   3.102 +definition "normalize x = (case x of a\<^sub>3 \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> x)"
   3.103 +definition [simp]: "unit_factor = (id :: finite_3 \<Rightarrow> _)"
   3.104 +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)"
   3.105 +instance
   3.106 +  by standard
   3.107 +    (auto simp add: finite_3_not_eq_unfold plus_finite_3_def
   3.108 +      dvd_finite_3_unfold times_finite_3_def inverse_finite_3_def
   3.109 +      normalize_finite_3_def divide_finite_3_def modulo_finite_3_def
   3.110 +      split: finite_3.splits)
   3.111  end
   3.112  
   3.113  
     4.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Sat Dec 17 15:22:13 2016 +0100
     4.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Sat Dec 17 15:22:14 2016 +0100
     4.3 @@ -1157,7 +1157,40 @@
     4.4  lemma fps_unit_dvd [simp]: "(f $ 0 :: 'a :: field) \<noteq> 0 \<Longrightarrow> f dvd g"
     4.5    by (rule dvd_trans, subst fps_is_unit_iff) simp_all
     4.6  
     4.7 -
     4.8 +instantiation fps :: (field) normalization_semidom
     4.9 +begin
    4.10 +
    4.11 +definition fps_unit_factor_def [simp]:
    4.12 +  "unit_factor f = fps_shift (subdegree f) f"
    4.13 +
    4.14 +definition fps_normalize_def [simp]:
    4.15 +  "normalize f = (if f = 0 then 0 else X ^ subdegree f)"
    4.16 +
    4.17 +instance proof
    4.18 +  fix f :: "'a fps"
    4.19 +  show "unit_factor f * normalize f = f"
    4.20 +    by (simp add: fps_shift_times_X_power)
    4.21 +next
    4.22 +  fix f g :: "'a fps"
    4.23 +  show "unit_factor (f * g) = unit_factor f * unit_factor g"
    4.24 +  proof (cases "f = 0 \<or> g = 0")
    4.25 +    assume "\<not>(f = 0 \<or> g = 0)"
    4.26 +    thus "unit_factor (f * g) = unit_factor f * unit_factor g"
    4.27 +    unfolding fps_unit_factor_def
    4.28 +      by (auto simp: fps_shift_fps_shift fps_shift_mult fps_shift_mult_right)
    4.29 +  qed auto
    4.30 +next
    4.31 +  fix f g :: "'a fps"
    4.32 +  assume "g \<noteq> 0"
    4.33 +  then have "f * (fps_shift (subdegree g) g * inverse (fps_shift (subdegree g) g)) = f"
    4.34 +    by (metis add_cancel_right_left fps_shift_nth inverse_mult_eq_1 mult.commute mult_cancel_left2 nth_subdegree_nonzero)
    4.35 +  then have "fps_shift (subdegree g) (g * (f * inverse (fps_shift (subdegree g) g))) = f"
    4.36 +    by (simp add: fps_shift_mult_right mult.commute)
    4.37 +  with \<open>g \<noteq> 0\<close> show "f * g / g = f"
    4.38 +    by (simp add: fps_divide_def Let_def ac_simps)
    4.39 +qed (auto simp add: fps_divide_def Let_def)
    4.40 +
    4.41 +end
    4.42  
    4.43  instantiation fps :: (field) ring_div
    4.44  begin
    4.45 @@ -1291,7 +1324,7 @@
    4.46    also have "fps_shift n (f * inverse h') = f div h"
    4.47      by (simp add: fps_divide_def Let_def dfs)
    4.48    finally show "(f + g * h) div h = g + f div h" by simp
    4.49 -qed (auto simp: fps_divide_def fps_mod_def Let_def)
    4.50 +qed
    4.51  
    4.52  end
    4.53  end
    4.54 @@ -1365,36 +1398,6 @@
    4.55    fps_numeral_divide_divide fps_numeral_mult_divide inverse_fps_numeral neg_numeral_fps_const
    4.56  
    4.57  
    4.58 -
    4.59 -instantiation fps :: (field) normalization_semidom
    4.60 -begin
    4.61 -
    4.62 -definition fps_unit_factor_def [simp]:
    4.63 -  "unit_factor f = fps_shift (subdegree f) f"
    4.64 -
    4.65 -definition fps_normalize_def [simp]:
    4.66 -  "normalize f = (if f = 0 then 0 else X ^ subdegree f)"
    4.67 -
    4.68 -instance proof
    4.69 -  fix f :: "'a fps"
    4.70 -  show "unit_factor f * normalize f = f"
    4.71 -    by (simp add: fps_shift_times_X_power)
    4.72 -next
    4.73 -  fix f g :: "'a fps"
    4.74 -  show "unit_factor (f * g) = unit_factor f * unit_factor g"
    4.75 -  proof (cases "f = 0 \<or> g = 0")
    4.76 -    assume "\<not>(f = 0 \<or> g = 0)"
    4.77 -    thus "unit_factor (f * g) = unit_factor f * unit_factor g"
    4.78 -    unfolding fps_unit_factor_def
    4.79 -      by (auto simp: fps_shift_fps_shift fps_shift_mult fps_shift_mult_right)
    4.80 -  qed auto
    4.81 -qed auto
    4.82 -
    4.83 -end
    4.84 -
    4.85 -instance fps :: (field) algebraic_semidom ..
    4.86 -
    4.87 -
    4.88  subsection \<open>Formal power series form a Euclidean ring\<close>
    4.89  
    4.90  instantiation fps :: (field) euclidean_ring
     5.1 --- a/src/HOL/Library/Normalized_Fraction.thy	Sat Dec 17 15:22:13 2016 +0100
     5.2 +++ b/src/HOL/Library/Normalized_Fraction.thy	Sat Dec 17 15:22:14 2016 +0100
     5.3 @@ -184,7 +184,7 @@
     5.4  
     5.5  lemma quot_of_fract_uminus:
     5.6    "quot_of_fract (-x) = (let (a,b) = quot_of_fract x in (-a, b))"
     5.7 -  by transfer (auto simp: case_prod_unfold Let_def normalize_quot_def dvd_neg_div' mult_unit_dvd_iff)
     5.8 +  by transfer (auto simp: case_prod_unfold Let_def normalize_quot_def dvd_neg_div mult_unit_dvd_iff)
     5.9  
    5.10  lemma quot_of_fract_diff:
    5.11    "quot_of_fract (x - y) = 
     6.1 --- a/src/HOL/Library/Polynomial.thy	Sat Dec 17 15:22:13 2016 +0100
     6.2 +++ b/src/HOL/Library/Polynomial.thy	Sat Dec 17 15:22:14 2016 +0100
     6.3 @@ -2274,12 +2274,6 @@
     6.4    from pdivmod_rel[of x y,unfolded pdivmod_rel_def]
     6.5    show "x div y * y + x mod y = x" by auto
     6.6  next
     6.7 -  fix x :: "'a poly"
     6.8 -  show "x div 0 = 0" by simp
     6.9 -next
    6.10 -  fix y :: "'a poly"
    6.11 -  show "0 div y = 0" by simp
    6.12 -next
    6.13    fix x y z :: "'a poly"
    6.14    assume "y \<noteq> 0"
    6.15    hence "pdivmod_rel (x + z * y) y (z + x div y) (x mod y)"
     7.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sat Dec 17 15:22:13 2016 +0100
     7.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sat Dec 17 15:22:14 2016 +0100
     7.3 @@ -17,7 +17,7 @@
     7.4    The existence of these functions makes it possible to derive gcd and lcm functions 
     7.5    for any Euclidean semiring.
     7.6  \<close> 
     7.7 -class euclidean_semiring = semiring_modulo + normalization_semidom + 
     7.8 +class euclidean_semiring = semidom_modulo + normalization_semidom + 
     7.9    fixes euclidean_size :: "'a \<Rightarrow> nat"
    7.10    assumes size_0 [simp]: "euclidean_size 0 = 0"
    7.11    assumes mod_size_less: 
    7.12 @@ -26,30 +26,6 @@
    7.13      "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)"
    7.14  begin
    7.15  
    7.16 -lemma mod_0 [simp]: "0 mod a = 0"
    7.17 -  using div_mult_mod_eq [of 0 a] by simp
    7.18 -
    7.19 -lemma dvd_mod_iff: 
    7.20 -  assumes "k dvd n"
    7.21 -  shows   "(k dvd m mod n) = (k dvd m)"
    7.22 -proof -
    7.23 -  from assms have "(k dvd m mod n) \<longleftrightarrow> (k dvd ((m div n) * n + m mod n))" 
    7.24 -    by (simp add: dvd_add_right_iff)
    7.25 -  also have "(m div n) * n + m mod n = m"
    7.26 -    using div_mult_mod_eq [of m n] by simp
    7.27 -  finally show ?thesis .
    7.28 -qed
    7.29 -
    7.30 -lemma mod_0_imp_dvd: 
    7.31 -  assumes "a mod b = 0"
    7.32 -  shows   "b dvd a"
    7.33 -proof -
    7.34 -  have "b dvd ((a div b) * b)" by simp
    7.35 -  also have "(a div b) * b = a"
    7.36 -    using div_mult_mod_eq [of a b] by (simp add: assms)
    7.37 -  finally show ?thesis .
    7.38 -qed
    7.39 -
    7.40  lemma euclidean_size_normalize [simp]:
    7.41    "euclidean_size (normalize a) = euclidean_size a"
    7.42  proof (cases "a = 0")
     8.1 --- a/src/HOL/Rings.thy	Sat Dec 17 15:22:13 2016 +0100
     8.2 +++ b/src/HOL/Rings.thy	Sat Dec 17 15:22:14 2016 +0100
     8.3 @@ -731,7 +731,7 @@
     8.4  class idom_divide = idom + semidom_divide
     8.5  begin
     8.6  
     8.7 -lemma dvd_neg_div':
     8.8 +lemma dvd_neg_div:
     8.9    assumes "b dvd a"
    8.10    shows "- a div b = - (a div b)"
    8.11  proof (cases "b = 0")
    8.12 @@ -740,10 +740,30 @@
    8.13  next
    8.14    case False
    8.15    from assms obtain c where "a = b * c" ..
    8.16 -  moreover from False have "b * - c div b = - (b * c div b)"
    8.17 -    using nonzero_mult_div_cancel_left [of b "- c"]
    8.18 +  then have "- a div b = (b * - c) div b"
    8.19 +    by simp
    8.20 +  from False also have "\<dots> = - c"
    8.21 +    by (rule nonzero_mult_div_cancel_left)  
    8.22 +  with False \<open>a = b * c\<close> show ?thesis
    8.23      by simp
    8.24 -  ultimately show ?thesis
    8.25 +qed
    8.26 +
    8.27 +lemma dvd_div_neg:
    8.28 +  assumes "b dvd a"
    8.29 +  shows "a div - b = - (a div b)"
    8.30 +proof (cases "b = 0")
    8.31 +  case True
    8.32 +  then show ?thesis by simp
    8.33 +next
    8.34 +  case False
    8.35 +  then have "- b \<noteq> 0"
    8.36 +    by simp
    8.37 +  from assms obtain c where "a = b * c" ..
    8.38 +  then have "a div - b = (- b * - c) div - b"
    8.39 +    by simp
    8.40 +  from \<open>- b \<noteq> 0\<close> also have "\<dots> = - c"
    8.41 +    by (rule nonzero_mult_div_cancel_left)  
    8.42 +  with False \<open>a = b * c\<close> show ?thesis
    8.43      by simp
    8.44  qed
    8.45  
    8.46 @@ -916,6 +936,39 @@
    8.47      by (simp add: mult.commute [of a] mult.assoc)
    8.48  qed
    8.49  
    8.50 +lemma div_div_eq_right:
    8.51 +  assumes "c dvd b" "b dvd a"
    8.52 +  shows   "a div (b div c) = a div b * c"
    8.53 +proof (cases "c = 0 \<or> b = 0")
    8.54 +  case True
    8.55 +  then show ?thesis
    8.56 +    by auto
    8.57 +next
    8.58 +  case False
    8.59 +  from assms obtain r s where "b = c * r" and "a = c * r * s"
    8.60 +    by (blast elim: dvdE)
    8.61 +  moreover with False have "r \<noteq> 0"
    8.62 +    by auto
    8.63 +  ultimately show ?thesis using False
    8.64 +    by simp (simp add: mult.commute [of _ r] mult.assoc mult.commute [of c])
    8.65 +qed
    8.66 +
    8.67 +lemma div_div_div_same:
    8.68 +  assumes "d dvd b" "b dvd a"
    8.69 +  shows   "(a div d) div (b div d) = a div b"
    8.70 +proof (cases "b = 0 \<or> d = 0")
    8.71 +  case True
    8.72 +  with assms show ?thesis
    8.73 +    by auto
    8.74 +next
    8.75 +  case False
    8.76 +  from assms obtain r s
    8.77 +    where "a = d * r * s" and "b = d * r"
    8.78 +    by (blast elim: dvdE)
    8.79 +  with False show ?thesis
    8.80 +    by simp (simp add: ac_simps)
    8.81 +qed
    8.82 +
    8.83  
    8.84  text \<open>Units: invertible elements in a ring\<close>
    8.85