# HG changeset patch
# User haftmann
# Date 1527059591 0
# Node ID a8660a39e304ce64919680f025006ed973b19517
# Parent  8b284d24f43464b7d6e47f643d077e23884c0bb3
grouped material on numeral division

diff -r 8b284d24f434 -r a8660a39e304 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Tue May 22 18:14:29 2018 +0000
+++ b/src/HOL/Divides.thy	Wed May 23 07:13:11 2018 +0000
@@ -9,323 +9,8 @@
 imports Parity
 begin
 
-subsection \<open>Numeral division with a pragmatic type class\<close>
-
-text \<open>
-  The following type class contains everything necessary to formulate
-  a division algorithm in ring structures with numerals, restricted
-  to its positive segments.  This is its primary motivation, and it
-  could surely be formulated using a more fine-grained, more algebraic
-  and less technical class hierarchy.
-\<close>
-
-class unique_euclidean_semiring_numeral = semiring_parity + linordered_semidom +
-  assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
-    and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
-    and div_positive: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0"
-    and mod_less_eq_dividend: "0 \<le> a \<Longrightarrow> a mod b \<le> a"
-    and pos_mod_bound: "0 < b \<Longrightarrow> a mod b < b"
-    and pos_mod_sign: "0 < b \<Longrightarrow> 0 \<le> a mod b"
-    and mod_mult2_eq: "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
-    and div_mult2_eq: "0 \<le> c \<Longrightarrow> a div (b * c) = a div b div c"
-  assumes discrete: "a < b \<longleftrightarrow> a + 1 \<le> b"
-  fixes divmod :: "num \<Rightarrow> num \<Rightarrow> 'a \<times> 'a"
-    and divmod_step :: "num \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<times> 'a"
-  assumes divmod_def: "divmod m n = (numeral m div numeral n, numeral m mod numeral n)"
-    and divmod_step_def: "divmod_step l qr = (let (q, r) = qr
-    in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
-    else (2 * q, r))"
-    \<comment> \<open>These are conceptually definitions but force generated code
-    to be monomorphic wrt. particular instances of this class which
-    yields a significant speedup.\<close>
-begin
-
-lemma divmod_digit_1:
-  assumes "0 \<le> a" "0 < b" and "b \<le> a mod (2 * b)"
-  shows "2 * (a div (2 * b)) + 1 = a div b" (is "?P")
-    and "a mod (2 * b) - b = a mod b" (is "?Q")
-proof -
-  from assms mod_less_eq_dividend [of a "2 * b"] have "b \<le> a"
-    by (auto intro: trans)
-  with \<open>0 < b\<close> have "0 < a div b" by (auto intro: div_positive)
-  then have [simp]: "1 \<le> a div b" by (simp add: discrete)
-  with \<open>0 < b\<close> have mod_less: "a mod b < b" by (simp add: pos_mod_bound)
-  define w where "w = a div b mod 2"
-  then have w_exhaust: "w = 0 \<or> w = 1" by auto
-  have mod_w: "a mod (2 * b) = a mod b + b * w"
-    by (simp add: w_def mod_mult2_eq ac_simps)
-  from assms w_exhaust have "w = 1"
-    by (auto simp add: mod_w) (insert mod_less, auto)
-  with mod_w have mod: "a mod (2 * b) = a mod b + b" by simp
-  have "2 * (a div (2 * b)) = a div b - w"
-    by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps)
-  with \<open>w = 1\<close> have div: "2 * (a div (2 * b)) = a div b - 1" by simp
-  then show ?P and ?Q
-    by (simp_all add: div mod add_implies_diff [symmetric])
-qed
-
-lemma divmod_digit_0:
-  assumes "0 < b" and "a mod (2 * b) < b"
-  shows "2 * (a div (2 * b)) = a div b" (is "?P")
-    and "a mod (2 * b) = a mod b" (is "?Q")
-proof -
-  define w where "w = a div b mod 2"
-  then have w_exhaust: "w = 0 \<or> w = 1" by auto
-  have mod_w: "a mod (2 * b) = a mod b + b * w"
-    by (simp add: w_def mod_mult2_eq ac_simps)
-  moreover have "b \<le> a mod b + b"
-  proof -
-    from \<open>0 < b\<close> pos_mod_sign have "0 \<le> a mod b" by blast
-    then have "0 + b \<le> a mod b + b" by (rule add_right_mono)
-    then show ?thesis by simp
-  qed
-  moreover note assms w_exhaust
-  ultimately have "w = 0" by auto
-  with mod_w have mod: "a mod (2 * b) = a mod b" by simp
-  have "2 * (a div (2 * b)) = a div b - w"
-    by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps)
-  with \<open>w = 0\<close> have div: "2 * (a div (2 * b)) = a div b" by simp
-  then show ?P and ?Q
-    by (simp_all add: div mod)
-qed
-
-lemma fst_divmod:
-  "fst (divmod m n) = numeral m div numeral n"
-  by (simp add: divmod_def)
-
-lemma snd_divmod:
-  "snd (divmod m n) = numeral m mod numeral n"
-  by (simp add: divmod_def)
-
-text \<open>
-  This is a formulation of one step (referring to one digit position)
-  in school-method division: compare the dividend at the current
-  digit position with the remainder from previous division steps
-  and evaluate accordingly.
-\<close>
-
-lemma divmod_step_eq [simp]:
-  "divmod_step l (q, r) = (if numeral l \<le> r
-    then (2 * q + 1, r - numeral l) else (2 * q, r))"
-  by (simp add: divmod_step_def)
-
-text \<open>
-  This is a formulation of school-method division.
-  If the divisor is smaller than the dividend, terminate.
-  If not, shift the dividend to the right until termination
-  occurs and then reiterate single division steps in the
-  opposite direction.
-\<close>
-
-lemma divmod_divmod_step:
-  "divmod m n = (if m < n then (0, numeral m)
-    else divmod_step n (divmod m (Num.Bit0 n)))"
-proof (cases "m < n")
-  case True then have "numeral m < numeral n" by simp
-  then show ?thesis
-    by (simp add: prod_eq_iff div_less mod_less fst_divmod snd_divmod)
-next
-  case False
-  have "divmod m n =
-    divmod_step n (numeral m div (2 * numeral n),
-      numeral m mod (2 * numeral n))"
-  proof (cases "numeral n \<le> numeral m mod (2 * numeral n)")
-    case True
-    with divmod_step_eq
-      have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
-        (2 * (numeral m div (2 * numeral n)) + 1, numeral m mod (2 * numeral n) - numeral n)"
-        by simp
-    moreover from True divmod_digit_1 [of "numeral m" "numeral n"]
-      have "2 * (numeral m div (2 * numeral n)) + 1 = numeral m div numeral n"
-      and "numeral m mod (2 * numeral n) - numeral n = numeral m mod numeral n"
-      by simp_all
-    ultimately show ?thesis by (simp only: divmod_def)
-  next
-    case False then have *: "numeral m mod (2 * numeral n) < numeral n"
-      by (simp add: not_le)
-    with divmod_step_eq
-      have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
-        (2 * (numeral m div (2 * numeral n)), numeral m mod (2 * numeral n))"
-        by auto
-    moreover from * divmod_digit_0 [of "numeral n" "numeral m"]
-      have "2 * (numeral m div (2 * numeral n)) = numeral m div numeral n"
-      and "numeral m mod (2 * numeral n) = numeral m mod numeral n"
-      by (simp_all only: zero_less_numeral)
-    ultimately show ?thesis by (simp only: divmod_def)
-  qed
-  then have "divmod m n =
-    divmod_step n (numeral m div numeral (Num.Bit0 n),
-      numeral m mod numeral (Num.Bit0 n))"
-    by (simp only: numeral.simps distrib mult_1)
-  then have "divmod m n = divmod_step n (divmod m (Num.Bit0 n))"
-    by (simp add: divmod_def)
-  with False show ?thesis by simp
-qed
-
-text \<open>The division rewrite proper -- first, trivial results involving \<open>1\<close>\<close>
-
-lemma divmod_trivial [simp]:
-  "divmod Num.One Num.One = (numeral Num.One, 0)"
-  "divmod (Num.Bit0 m) Num.One = (numeral (Num.Bit0 m), 0)"
-  "divmod (Num.Bit1 m) Num.One = (numeral (Num.Bit1 m), 0)"
-  "divmod num.One (num.Bit0 n) = (0, Numeral1)"
-  "divmod num.One (num.Bit1 n) = (0, Numeral1)"
-  using divmod_divmod_step [of "Num.One"] by (simp_all add: divmod_def)
-
-text \<open>Division by an even number is a right-shift\<close>
-
-lemma divmod_cancel [simp]:
-  "divmod (Num.Bit0 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r))" (is ?P)
-  "divmod (Num.Bit1 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r + 1))" (is ?Q)
-proof -
-  have *: "\<And>q. numeral (Num.Bit0 q) = 2 * numeral q"
-    "\<And>q. numeral (Num.Bit1 q) = 2 * numeral q + 1"
-    by (simp_all only: numeral_mult numeral.simps distrib) simp_all
-  have "1 div 2 = 0" "1 mod 2 = 1" by (auto intro: div_less mod_less)
-  then show ?P and ?Q
-    by (simp_all add: fst_divmod snd_divmod prod_eq_iff split_def * [of m] * [of n] mod_mult_mult1
-      div_mult2_eq [of _ _ 2] mod_mult2_eq [of _ _ 2]
-      add.commute del: numeral_times_numeral)
-qed
-
-text \<open>The really hard work\<close>
-
-lemma divmod_steps [simp]:
-  "divmod (num.Bit0 m) (num.Bit1 n) =
-      (if m \<le> n then (0, numeral (num.Bit0 m))
-       else divmod_step (num.Bit1 n)
-             (divmod (num.Bit0 m)
-               (num.Bit0 (num.Bit1 n))))"
-  "divmod (num.Bit1 m) (num.Bit1 n) =
-      (if m < n then (0, numeral (num.Bit1 m))
-       else divmod_step (num.Bit1 n)
-             (divmod (num.Bit1 m)
-               (num.Bit0 (num.Bit1 n))))"
-  by (simp_all add: divmod_divmod_step)
-
-lemmas divmod_algorithm_code = divmod_step_eq divmod_trivial divmod_cancel divmod_steps  
-
-text \<open>Special case: divisibility\<close>
-
-definition divides_aux :: "'a \<times> 'a \<Rightarrow> bool"
-where
-  "divides_aux qr \<longleftrightarrow> snd qr = 0"
-
-lemma divides_aux_eq [simp]:
-  "divides_aux (q, r) \<longleftrightarrow> r = 0"
-  by (simp add: divides_aux_def)
-
-lemma dvd_numeral_simp [simp]:
-  "numeral m dvd numeral n \<longleftrightarrow> divides_aux (divmod n m)"
-  by (simp add: divmod_def mod_eq_0_iff_dvd)
-
-text \<open>Generic computation of quotient and remainder\<close>  
-
-lemma numeral_div_numeral [simp]: 
-  "numeral k div numeral l = fst (divmod k l)"
-  by (simp add: fst_divmod)
-
-lemma numeral_mod_numeral [simp]: 
-  "numeral k mod numeral l = snd (divmod k l)"
-  by (simp add: snd_divmod)
-
-lemma one_div_numeral [simp]:
-  "1 div numeral n = fst (divmod num.One n)"
-  by (simp add: fst_divmod)
-
-lemma one_mod_numeral [simp]:
-  "1 mod numeral n = snd (divmod num.One n)"
-  by (simp add: snd_divmod)
-
-text \<open>Computing congruences modulo \<open>2 ^ q\<close>\<close>
-
-lemma cong_exp_iff_simps:
-  "numeral n mod numeral Num.One = 0
-    \<longleftrightarrow> True"
-  "numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) = 0
-    \<longleftrightarrow> numeral n mod numeral q = 0"
-  "numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) = 0
-    \<longleftrightarrow> False"
-  "numeral m mod numeral Num.One = (numeral n mod numeral Num.One)
-    \<longleftrightarrow> True"
-  "numeral Num.One mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
-    \<longleftrightarrow> True"
-  "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
-    \<longleftrightarrow> False"
-  "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
-    \<longleftrightarrow> (numeral n mod numeral q) = 0"
-  "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
-    \<longleftrightarrow> False"
-  "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
-    \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)"
-  "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
-    \<longleftrightarrow> False"
-  "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
-    \<longleftrightarrow> (numeral m mod numeral q) = 0"
-  "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
-    \<longleftrightarrow> False"
-  "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
-    \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)"
-  by (auto simp add: case_prod_beta dest: arg_cong [of _ _ even])
-
-end
-
-hide_fact (open) div_less mod_less mod_less_eq_dividend mod_mult2_eq div_mult2_eq
-
-
 subsection \<open>More on division\<close>
 
-instantiation nat :: unique_euclidean_semiring_numeral
-begin
-
-definition divmod_nat :: "num \<Rightarrow> num \<Rightarrow> nat \<times> nat"
-where
-  divmod'_nat_def: "divmod_nat m n = (numeral m div numeral n, numeral m mod numeral n)"
-
-definition divmod_step_nat :: "num \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"
-where
-  "divmod_step_nat l qr = (let (q, r) = qr
-    in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
-    else (2 * q, r))"
-
-instance by standard
-  (auto simp add: divmod'_nat_def divmod_step_nat_def div_greater_zero_iff div_mult2_eq mod_mult2_eq)
-
-end
-
-declare divmod_algorithm_code [where ?'a = nat, code]
-
-lemma Suc_0_div_numeral [simp]:
-  fixes k l :: num
-  shows "Suc 0 div numeral k = fst (divmod Num.One k)"
-  by (simp_all add: fst_divmod)
-
-lemma Suc_0_mod_numeral [simp]:
-  fixes k l :: num
-  shows "Suc 0 mod numeral k = snd (divmod Num.One k)"
-  by (simp_all add: snd_divmod)
-
-definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat"
-  where "divmod_nat m n = (m div n, m mod n)"
-
-lemma fst_divmod_nat [simp]:
-  "fst (divmod_nat m n) = m div n"
-  by (simp add: divmod_nat_def)
-
-lemma snd_divmod_nat [simp]:
-  "snd (divmod_nat m n) = m mod n"
-  by (simp add: divmod_nat_def)
-
-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 [code]:
-  "m div n = fst (divmod_nat m n)"
-  "m mod n = snd (divmod_nat m n)"
-  by simp_all
-
 inductive eucl_rel_int :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool"
   where eucl_rel_int_by0: "eucl_rel_int k 0 (0, k)"
   | eucl_rel_int_dividesI: "l \<noteq> 0 \<Longrightarrow> k = q * l \<Longrightarrow> eucl_rel_int k l (q, 0)"
@@ -514,10 +199,6 @@
 apply (auto simp add: eucl_rel_int_iff)
 done
 
-lemma div_positive_int:
-  "k div l > 0" if "k \<ge> l" and "l > 0" for k l :: int
-  using that by (simp add: divide_int_def div_positive)
-
 (*There is no div_neg_pos_trivial because  0 div b = 0 would supersede it*)
 
 lemma mod_pos_pos_trivial [simp]:
@@ -972,107 +653,6 @@
 
 subsubsection \<open>Computation of Division and Remainder\<close>
 
-instantiation int :: unique_euclidean_semiring_numeral
-begin
-
-definition divmod_int :: "num \<Rightarrow> num \<Rightarrow> int \<times> int"
-where
-  "divmod_int m n = (numeral m div numeral n, numeral m mod numeral n)"
-
-definition divmod_step_int :: "num \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int"
-where
-  "divmod_step_int l qr = (let (q, r) = qr
-    in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
-    else (2 * q, r))"
-
-instance
-  by standard (auto intro: zmod_le_nonneg_dividend simp add: divmod_int_def divmod_step_int_def
-    pos_imp_zdiv_pos_iff zmod_zmult2_eq zdiv_zmult2_eq)
-
-end
-
-declare divmod_algorithm_code [where ?'a = int, code]
-
-context
-begin
-  
-qualified definition adjust_div :: "int \<times> int \<Rightarrow> int"
-where
-  "adjust_div qr = (let (q, r) = qr in q + of_bool (r \<noteq> 0))"
-
-qualified lemma adjust_div_eq [simp, code]:
-  "adjust_div (q, r) = q + of_bool (r \<noteq> 0)"
-  by (simp add: adjust_div_def)
-
-qualified definition adjust_mod :: "int \<Rightarrow> int \<Rightarrow> int"
-where
-  [simp]: "adjust_mod l r = (if r = 0 then 0 else l - r)"
-
-lemma minus_numeral_div_numeral [simp]:
-  "- numeral m div numeral n = - (adjust_div (divmod m n) :: int)"
-proof -
-  have "int (fst (divmod m n)) = fst (divmod m n)"
-    by (simp only: fst_divmod divide_int_def) auto
-  then show ?thesis
-    by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def)
-qed
-
-lemma minus_numeral_mod_numeral [simp]:
-  "- numeral m mod numeral n = adjust_mod (numeral n) (snd (divmod m n) :: int)"
-proof (cases "snd (divmod m n) = (0::int)")
-  case True
-  then show ?thesis
-    by (simp add: mod_eq_0_iff_dvd divides_aux_def)
-next
-  case False
-  then have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
-    by (simp only: snd_divmod modulo_int_def) auto
-  then show ?thesis
-    by (simp add: divides_aux_def adjust_div_def)
-      (simp add: divides_aux_def modulo_int_def)
-qed
-
-lemma numeral_div_minus_numeral [simp]:
-  "numeral m div - numeral n = - (adjust_div (divmod m n) :: int)"
-proof -
-  have "int (fst (divmod m n)) = fst (divmod m n)"
-    by (simp only: fst_divmod divide_int_def) auto
-  then show ?thesis
-    by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def)
-qed
-  
-lemma numeral_mod_minus_numeral [simp]:
-  "numeral m mod - numeral n = - adjust_mod (numeral n) (snd (divmod m n) :: int)"
-proof (cases "snd (divmod m n) = (0::int)")
-  case True
-  then show ?thesis
-    by (simp add: mod_eq_0_iff_dvd divides_aux_def)
-next
-  case False
-  then have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
-    by (simp only: snd_divmod modulo_int_def) auto
-  then show ?thesis
-    by (simp add: divides_aux_def adjust_div_def)
-      (simp add: divides_aux_def modulo_int_def)
-qed
-
-lemma minus_one_div_numeral [simp]:
-  "- 1 div numeral n = - (adjust_div (divmod Num.One n) :: int)"
-  using minus_numeral_div_numeral [of Num.One n] by simp  
-
-lemma minus_one_mod_numeral [simp]:
-  "- 1 mod numeral n = adjust_mod (numeral n) (snd (divmod Num.One n) :: int)"
-  using minus_numeral_mod_numeral [of Num.One n] by simp
-
-lemma one_div_minus_numeral [simp]:
-  "1 div - numeral n = - (adjust_div (divmod Num.One n) :: int)"
-  using numeral_div_minus_numeral [of Num.One n] by simp
-  
-lemma one_mod_minus_numeral [simp]:
-  "1 mod - numeral n = - adjust_mod (numeral n) (snd (divmod Num.One n) :: int)"
-  using numeral_mod_minus_numeral [of Num.One n] by simp
-
-end
 
 
 subsubsection \<open>Further properties\<close>
@@ -1202,6 +782,406 @@
 qed
 
 
+subsection \<open>Numeral division with a pragmatic type class\<close>
+
+text \<open>
+  The following type class contains everything necessary to formulate
+  a division algorithm in ring structures with numerals, restricted
+  to its positive segments.  This is its primary motivation, and it
+  could surely be formulated using a more fine-grained, more algebraic
+  and less technical class hierarchy.
+\<close>
+
+class unique_euclidean_semiring_numeral = semiring_parity + linordered_semidom +
+  assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
+    and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
+    and div_positive: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0"
+    and mod_less_eq_dividend: "0 \<le> a \<Longrightarrow> a mod b \<le> a"
+    and pos_mod_bound: "0 < b \<Longrightarrow> a mod b < b"
+    and pos_mod_sign: "0 < b \<Longrightarrow> 0 \<le> a mod b"
+    and mod_mult2_eq: "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
+    and div_mult2_eq: "0 \<le> c \<Longrightarrow> a div (b * c) = a div b div c"
+  assumes discrete: "a < b \<longleftrightarrow> a + 1 \<le> b"
+  fixes divmod :: "num \<Rightarrow> num \<Rightarrow> 'a \<times> 'a"
+    and divmod_step :: "num \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<times> 'a"
+  assumes divmod_def: "divmod m n = (numeral m div numeral n, numeral m mod numeral n)"
+    and divmod_step_def: "divmod_step l qr = (let (q, r) = qr
+    in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
+    else (2 * q, r))"
+    \<comment> \<open>These are conceptually definitions but force generated code
+    to be monomorphic wrt. particular instances of this class which
+    yields a significant speedup.\<close>
+begin
+
+lemma divmod_digit_1:
+  assumes "0 \<le> a" "0 < b" and "b \<le> a mod (2 * b)"
+  shows "2 * (a div (2 * b)) + 1 = a div b" (is "?P")
+    and "a mod (2 * b) - b = a mod b" (is "?Q")
+proof -
+  from assms mod_less_eq_dividend [of a "2 * b"] have "b \<le> a"
+    by (auto intro: trans)
+  with \<open>0 < b\<close> have "0 < a div b" by (auto intro: div_positive)
+  then have [simp]: "1 \<le> a div b" by (simp add: discrete)
+  with \<open>0 < b\<close> have mod_less: "a mod b < b" by (simp add: pos_mod_bound)
+  define w where "w = a div b mod 2"
+  then have w_exhaust: "w = 0 \<or> w = 1" by auto
+  have mod_w: "a mod (2 * b) = a mod b + b * w"
+    by (simp add: w_def mod_mult2_eq ac_simps)
+  from assms w_exhaust have "w = 1"
+    by (auto simp add: mod_w) (insert mod_less, auto)
+  with mod_w have mod: "a mod (2 * b) = a mod b + b" by simp
+  have "2 * (a div (2 * b)) = a div b - w"
+    by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps)
+  with \<open>w = 1\<close> have div: "2 * (a div (2 * b)) = a div b - 1" by simp
+  then show ?P and ?Q
+    by (simp_all add: div mod add_implies_diff [symmetric])
+qed
+
+lemma divmod_digit_0:
+  assumes "0 < b" and "a mod (2 * b) < b"
+  shows "2 * (a div (2 * b)) = a div b" (is "?P")
+    and "a mod (2 * b) = a mod b" (is "?Q")
+proof -
+  define w where "w = a div b mod 2"
+  then have w_exhaust: "w = 0 \<or> w = 1" by auto
+  have mod_w: "a mod (2 * b) = a mod b + b * w"
+    by (simp add: w_def mod_mult2_eq ac_simps)
+  moreover have "b \<le> a mod b + b"
+  proof -
+    from \<open>0 < b\<close> pos_mod_sign have "0 \<le> a mod b" by blast
+    then have "0 + b \<le> a mod b + b" by (rule add_right_mono)
+    then show ?thesis by simp
+  qed
+  moreover note assms w_exhaust
+  ultimately have "w = 0" by auto
+  with mod_w have mod: "a mod (2 * b) = a mod b" by simp
+  have "2 * (a div (2 * b)) = a div b - w"
+    by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps)
+  with \<open>w = 0\<close> have div: "2 * (a div (2 * b)) = a div b" by simp
+  then show ?P and ?Q
+    by (simp_all add: div mod)
+qed
+
+lemma fst_divmod:
+  "fst (divmod m n) = numeral m div numeral n"
+  by (simp add: divmod_def)
+
+lemma snd_divmod:
+  "snd (divmod m n) = numeral m mod numeral n"
+  by (simp add: divmod_def)
+
+text \<open>
+  This is a formulation of one step (referring to one digit position)
+  in school-method division: compare the dividend at the current
+  digit position with the remainder from previous division steps
+  and evaluate accordingly.
+\<close>
+
+lemma divmod_step_eq [simp]:
+  "divmod_step l (q, r) = (if numeral l \<le> r
+    then (2 * q + 1, r - numeral l) else (2 * q, r))"
+  by (simp add: divmod_step_def)
+
+text \<open>
+  This is a formulation of school-method division.
+  If the divisor is smaller than the dividend, terminate.
+  If not, shift the dividend to the right until termination
+  occurs and then reiterate single division steps in the
+  opposite direction.
+\<close>
+
+lemma divmod_divmod_step:
+  "divmod m n = (if m < n then (0, numeral m)
+    else divmod_step n (divmod m (Num.Bit0 n)))"
+proof (cases "m < n")
+  case True then have "numeral m < numeral n" by simp
+  then show ?thesis
+    by (simp add: prod_eq_iff div_less mod_less fst_divmod snd_divmod)
+next
+  case False
+  have "divmod m n =
+    divmod_step n (numeral m div (2 * numeral n),
+      numeral m mod (2 * numeral n))"
+  proof (cases "numeral n \<le> numeral m mod (2 * numeral n)")
+    case True
+    with divmod_step_eq
+      have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
+        (2 * (numeral m div (2 * numeral n)) + 1, numeral m mod (2 * numeral n) - numeral n)"
+        by simp
+    moreover from True divmod_digit_1 [of "numeral m" "numeral n"]
+      have "2 * (numeral m div (2 * numeral n)) + 1 = numeral m div numeral n"
+      and "numeral m mod (2 * numeral n) - numeral n = numeral m mod numeral n"
+      by simp_all
+    ultimately show ?thesis by (simp only: divmod_def)
+  next
+    case False then have *: "numeral m mod (2 * numeral n) < numeral n"
+      by (simp add: not_le)
+    with divmod_step_eq
+      have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
+        (2 * (numeral m div (2 * numeral n)), numeral m mod (2 * numeral n))"
+        by auto
+    moreover from * divmod_digit_0 [of "numeral n" "numeral m"]
+      have "2 * (numeral m div (2 * numeral n)) = numeral m div numeral n"
+      and "numeral m mod (2 * numeral n) = numeral m mod numeral n"
+      by (simp_all only: zero_less_numeral)
+    ultimately show ?thesis by (simp only: divmod_def)
+  qed
+  then have "divmod m n =
+    divmod_step n (numeral m div numeral (Num.Bit0 n),
+      numeral m mod numeral (Num.Bit0 n))"
+    by (simp only: numeral.simps distrib mult_1)
+  then have "divmod m n = divmod_step n (divmod m (Num.Bit0 n))"
+    by (simp add: divmod_def)
+  with False show ?thesis by simp
+qed
+
+text \<open>The division rewrite proper -- first, trivial results involving \<open>1\<close>\<close>
+
+lemma divmod_trivial [simp]:
+  "divmod Num.One Num.One = (numeral Num.One, 0)"
+  "divmod (Num.Bit0 m) Num.One = (numeral (Num.Bit0 m), 0)"
+  "divmod (Num.Bit1 m) Num.One = (numeral (Num.Bit1 m), 0)"
+  "divmod num.One (num.Bit0 n) = (0, Numeral1)"
+  "divmod num.One (num.Bit1 n) = (0, Numeral1)"
+  using divmod_divmod_step [of "Num.One"] by (simp_all add: divmod_def)
+
+text \<open>Division by an even number is a right-shift\<close>
+
+lemma divmod_cancel [simp]:
+  "divmod (Num.Bit0 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r))" (is ?P)
+  "divmod (Num.Bit1 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r + 1))" (is ?Q)
+proof -
+  have *: "\<And>q. numeral (Num.Bit0 q) = 2 * numeral q"
+    "\<And>q. numeral (Num.Bit1 q) = 2 * numeral q + 1"
+    by (simp_all only: numeral_mult numeral.simps distrib) simp_all
+  have "1 div 2 = 0" "1 mod 2 = 1" by (auto intro: div_less mod_less)
+  then show ?P and ?Q
+    by (simp_all add: fst_divmod snd_divmod prod_eq_iff split_def * [of m] * [of n] mod_mult_mult1
+      div_mult2_eq [of _ _ 2] mod_mult2_eq [of _ _ 2]
+      add.commute del: numeral_times_numeral)
+qed
+
+text \<open>The really hard work\<close>
+
+lemma divmod_steps [simp]:
+  "divmod (num.Bit0 m) (num.Bit1 n) =
+      (if m \<le> n then (0, numeral (num.Bit0 m))
+       else divmod_step (num.Bit1 n)
+             (divmod (num.Bit0 m)
+               (num.Bit0 (num.Bit1 n))))"
+  "divmod (num.Bit1 m) (num.Bit1 n) =
+      (if m < n then (0, numeral (num.Bit1 m))
+       else divmod_step (num.Bit1 n)
+             (divmod (num.Bit1 m)
+               (num.Bit0 (num.Bit1 n))))"
+  by (simp_all add: divmod_divmod_step)
+
+lemmas divmod_algorithm_code = divmod_step_eq divmod_trivial divmod_cancel divmod_steps  
+
+text \<open>Special case: divisibility\<close>
+
+definition divides_aux :: "'a \<times> 'a \<Rightarrow> bool"
+where
+  "divides_aux qr \<longleftrightarrow> snd qr = 0"
+
+lemma divides_aux_eq [simp]:
+  "divides_aux (q, r) \<longleftrightarrow> r = 0"
+  by (simp add: divides_aux_def)
+
+lemma dvd_numeral_simp [simp]:
+  "numeral m dvd numeral n \<longleftrightarrow> divides_aux (divmod n m)"
+  by (simp add: divmod_def mod_eq_0_iff_dvd)
+
+text \<open>Generic computation of quotient and remainder\<close>  
+
+lemma numeral_div_numeral [simp]: 
+  "numeral k div numeral l = fst (divmod k l)"
+  by (simp add: fst_divmod)
+
+lemma numeral_mod_numeral [simp]: 
+  "numeral k mod numeral l = snd (divmod k l)"
+  by (simp add: snd_divmod)
+
+lemma one_div_numeral [simp]:
+  "1 div numeral n = fst (divmod num.One n)"
+  by (simp add: fst_divmod)
+
+lemma one_mod_numeral [simp]:
+  "1 mod numeral n = snd (divmod num.One n)"
+  by (simp add: snd_divmod)
+
+text \<open>Computing congruences modulo \<open>2 ^ q\<close>\<close>
+
+lemma cong_exp_iff_simps:
+  "numeral n mod numeral Num.One = 0
+    \<longleftrightarrow> True"
+  "numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) = 0
+    \<longleftrightarrow> numeral n mod numeral q = 0"
+  "numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) = 0
+    \<longleftrightarrow> False"
+  "numeral m mod numeral Num.One = (numeral n mod numeral Num.One)
+    \<longleftrightarrow> True"
+  "numeral Num.One mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
+    \<longleftrightarrow> True"
+  "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
+    \<longleftrightarrow> False"
+  "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
+    \<longleftrightarrow> (numeral n mod numeral q) = 0"
+  "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
+    \<longleftrightarrow> False"
+  "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
+    \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)"
+  "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
+    \<longleftrightarrow> False"
+  "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
+    \<longleftrightarrow> (numeral m mod numeral q) = 0"
+  "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
+    \<longleftrightarrow> False"
+  "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
+    \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)"
+  by (auto simp add: case_prod_beta dest: arg_cong [of _ _ even])
+
+end
+
+hide_fact (open) div_less mod_less mod_less_eq_dividend mod_mult2_eq div_mult2_eq
+
+instantiation nat :: unique_euclidean_semiring_numeral
+begin
+
+definition divmod_nat :: "num \<Rightarrow> num \<Rightarrow> nat \<times> nat"
+where
+  divmod'_nat_def: "divmod_nat m n = (numeral m div numeral n, numeral m mod numeral n)"
+
+definition divmod_step_nat :: "num \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"
+where
+  "divmod_step_nat l qr = (let (q, r) = qr
+    in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
+    else (2 * q, r))"
+
+instance by standard
+  (auto simp add: divmod'_nat_def divmod_step_nat_def div_greater_zero_iff div_mult2_eq mod_mult2_eq)
+
+end
+
+declare divmod_algorithm_code [where ?'a = nat, code]
+
+lemma Suc_0_div_numeral [simp]:
+  fixes k l :: num
+  shows "Suc 0 div numeral k = fst (divmod Num.One k)"
+  by (simp_all add: fst_divmod)
+
+lemma Suc_0_mod_numeral [simp]:
+  fixes k l :: num
+  shows "Suc 0 mod numeral k = snd (divmod Num.One k)"
+  by (simp_all add: snd_divmod)
+
+instantiation int :: unique_euclidean_semiring_numeral
+begin
+
+definition divmod_int :: "num \<Rightarrow> num \<Rightarrow> int \<times> int"
+where
+  "divmod_int m n = (numeral m div numeral n, numeral m mod numeral n)"
+
+definition divmod_step_int :: "num \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int"
+where
+  "divmod_step_int l qr = (let (q, r) = qr
+    in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
+    else (2 * q, r))"
+
+instance
+  by standard (auto intro: zmod_le_nonneg_dividend simp add: divmod_int_def divmod_step_int_def
+    pos_imp_zdiv_pos_iff zmod_zmult2_eq zdiv_zmult2_eq)
+
+end
+
+declare divmod_algorithm_code [where ?'a = int, code]
+
+context
+begin
+  
+qualified definition adjust_div :: "int \<times> int \<Rightarrow> int"
+where
+  "adjust_div qr = (let (q, r) = qr in q + of_bool (r \<noteq> 0))"
+
+qualified lemma adjust_div_eq [simp, code]:
+  "adjust_div (q, r) = q + of_bool (r \<noteq> 0)"
+  by (simp add: adjust_div_def)
+
+qualified definition adjust_mod :: "int \<Rightarrow> int \<Rightarrow> int"
+where
+  [simp]: "adjust_mod l r = (if r = 0 then 0 else l - r)"
+
+lemma minus_numeral_div_numeral [simp]:
+  "- numeral m div numeral n = - (adjust_div (divmod m n) :: int)"
+proof -
+  have "int (fst (divmod m n)) = fst (divmod m n)"
+    by (simp only: fst_divmod divide_int_def) auto
+  then show ?thesis
+    by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def)
+qed
+
+lemma minus_numeral_mod_numeral [simp]:
+  "- numeral m mod numeral n = adjust_mod (numeral n) (snd (divmod m n) :: int)"
+proof (cases "snd (divmod m n) = (0::int)")
+  case True
+  then show ?thesis
+    by (simp add: mod_eq_0_iff_dvd divides_aux_def)
+next
+  case False
+  then have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
+    by (simp only: snd_divmod modulo_int_def) auto
+  then show ?thesis
+    by (simp add: divides_aux_def adjust_div_def)
+      (simp add: divides_aux_def modulo_int_def)
+qed
+
+lemma numeral_div_minus_numeral [simp]:
+  "numeral m div - numeral n = - (adjust_div (divmod m n) :: int)"
+proof -
+  have "int (fst (divmod m n)) = fst (divmod m n)"
+    by (simp only: fst_divmod divide_int_def) auto
+  then show ?thesis
+    by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def)
+qed
+  
+lemma numeral_mod_minus_numeral [simp]:
+  "numeral m mod - numeral n = - adjust_mod (numeral n) (snd (divmod m n) :: int)"
+proof (cases "snd (divmod m n) = (0::int)")
+  case True
+  then show ?thesis
+    by (simp add: mod_eq_0_iff_dvd divides_aux_def)
+next
+  case False
+  then have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
+    by (simp only: snd_divmod modulo_int_def) auto
+  then show ?thesis
+    by (simp add: divides_aux_def adjust_div_def)
+      (simp add: divides_aux_def modulo_int_def)
+qed
+
+lemma minus_one_div_numeral [simp]:
+  "- 1 div numeral n = - (adjust_div (divmod Num.One n) :: int)"
+  using minus_numeral_div_numeral [of Num.One n] by simp  
+
+lemma minus_one_mod_numeral [simp]:
+  "- 1 mod numeral n = adjust_mod (numeral n) (snd (divmod Num.One n) :: int)"
+  using minus_numeral_mod_numeral [of Num.One n] by simp
+
+lemma one_div_minus_numeral [simp]:
+  "1 div - numeral n = - (adjust_div (divmod Num.One n) :: int)"
+  using numeral_div_minus_numeral [of Num.One n] by simp
+  
+lemma one_mod_minus_numeral [simp]:
+  "1 mod - numeral n = - adjust_mod (numeral n) (snd (divmod Num.One n) :: int)"
+  using numeral_mod_minus_numeral [of Num.One n] by simp
+
+end
+
+lemma div_positive_int:
+  "k div l > 0" if "k \<ge> l" and "l > 0" for k l :: int
+  using that div_positive [of l k] by blast
+
+
 subsubsection \<open>Dedicated simproc for calculation\<close>
 
 text \<open>
@@ -1262,6 +1242,27 @@
 
 subsubsection \<open>Code generation\<close>
 
+definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat"
+  where "divmod_nat m n = (m div n, m mod n)"
+
+lemma fst_divmod_nat [simp]:
+  "fst (divmod_nat m n) = m div n"
+  by (simp add: divmod_nat_def)
+
+lemma snd_divmod_nat [simp]:
+  "snd (divmod_nat m n) = m mod n"
+  by (simp add: divmod_nat_def)
+
+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 [code]:
+  "m div n = fst (divmod_nat m n)"
+  "m mod n = snd (divmod_nat m n)"
+  by simp_all
+
 lemma [code]:
   fixes k :: int
   shows 
@@ -1286,10 +1287,8 @@
 code_identifier
   code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
 
-declare minus_div_mult_eq_mod [symmetric, nitpick_unfold]
 
-
-subsubsection \<open>Lemmas of doubtful value\<close>
+subsection \<open>Lemmas of doubtful value\<close>
 
 lemma div_geq:
   "m div n = Suc ((m - n) div n)" if "0 < n" and " \<not> m < n" for m n :: nat
diff -r 8b284d24f434 -r a8660a39e304 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Tue May 22 18:14:29 2018 +0000
+++ b/src/HOL/Rings.thy	Wed May 23 07:13:11 2018 +0000
@@ -1682,6 +1682,10 @@
 lemma minus_mod_eq_mult_div: "a - a mod b = b * (a div b)"
   by (rule add_implies_diff [symmetric]) (fact mult_div_mod_eq)
 
+lemma [nitpick_unfold]:
+  "a mod b = a - a div b * b"
+  by (fact minus_div_mult_eq_mod [symmetric])
+
 end