# HG changeset patch
# User haftmann
# Date 1507494501 -7200
# Node ID 1907167b60383c049804ec3b7f8069b4142a8990
# Parent  c3631f32dfeb81f1bcd5eccefde5d17116583c9f
elementary definition of division on natural numbers

diff -r c3631f32dfeb -r 1907167b6038 src/HOL/Computational_Algebra/Polynomial_Factorial.thy
--- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -15,7 +15,7 @@
 
 definition to_fract :: "'a :: idom \<Rightarrow> 'a fract"
   where "to_fract x = Fract x 1"
-  \<comment> \<open>FIXME: name \<open>of_idom\<close>, abbreviation\<close>
+  \<comment> \<open>FIXME: more idiomatic name, abbreviation\<close>
 
 lemma to_fract_0 [simp]: "to_fract 0 = 0"
   by (simp add: to_fract_def eq_fract Zero_fract_def)
@@ -438,8 +438,8 @@
     by (simp add: irreducible_dict)
   show "comm_semiring_1.prime_elem times 1 0 = prime_elem"
     by (simp add: prime_elem_dict)
-  show "class.unique_euclidean_ring divide plus minus (0 :: 'a poly) times 1 modulo
-    (\<lambda>p. [:lead_coeff p:]) (\<lambda>p. smult (inverse (lead_coeff p)) p)
+  show "class.unique_euclidean_ring divide plus minus (0 :: 'a poly) times 1
+    (\<lambda>p. [:lead_coeff p:]) (\<lambda>p. smult (inverse (lead_coeff p)) p) modulo
     (\<lambda>p. if p = 0 then 0 else 2 ^ degree p) uminus top"
   proof (standard, fold dvd_dict)
     fix p :: "'a poly"
diff -r c3631f32dfeb -r 1907167b6038 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Divides.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -9,95 +9,6 @@
 imports Parity
 begin
 
-subsection \<open>Parity\<close>
-
-class unique_euclidean_semiring_parity = unique_euclidean_semiring +
-  assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
-  assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1"
-  assumes zero_not_eq_two: "0 \<noteq> 2"
-begin
-
-lemma parity_cases [case_names even odd]:
-  assumes "a mod 2 = 0 \<Longrightarrow> P"
-  assumes "a mod 2 = 1 \<Longrightarrow> P"
-  shows P
-  using assms parity by blast
-
-lemma one_div_two_eq_zero [simp]:
-  "1 div 2 = 0"
-proof (cases "2 = 0")
-  case True then show ?thesis by simp
-next
-  case False
-  from div_mult_mod_eq have "1 div 2 * 2 + 1 mod 2 = 1" .
-  with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp
-  then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq del: mult_eq_0_iff)
-  then have "1 div 2 = 0 \<or> 2 = 0" by simp
-  with False show ?thesis by auto
-qed
-
-lemma not_mod_2_eq_0_eq_1 [simp]:
-  "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
-  by (cases a rule: parity_cases) simp_all
-
-lemma not_mod_2_eq_1_eq_0 [simp]:
-  "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
-  by (cases a rule: parity_cases) simp_all
-
-subclass semiring_parity
-proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1)
-  show "1 mod 2 = 1"
-    by (fact one_mod_two_eq_one)
-next
-  fix a b
-  assume "a mod 2 = 1"
-  moreover assume "b mod 2 = 1"
-  ultimately show "(a + b) mod 2 = 0"
-    using mod_add_eq [of a 2 b] by simp
-next
-  fix a b
-  assume "(a * b) mod 2 = 0"
-  then have "(a mod 2) * (b mod 2) mod 2 = 0"
-    by (simp add: mod_mult_eq)
-  then have "(a mod 2) * (b mod 2) = 0"
-    by (cases "a mod 2 = 0") simp_all
-  then show "a mod 2 = 0 \<or> b mod 2 = 0"
-    by (rule divisors_zero)
-next
-  fix a
-  assume "a mod 2 = 1"
-  then have "a = a div 2 * 2 + 1"
-    using div_mult_mod_eq [of a 2] by simp
-  then show "\<exists>b. a = b + 1" ..
-qed
-
-lemma even_iff_mod_2_eq_zero:
-  "even a \<longleftrightarrow> a mod 2 = 0"
-  by (fact dvd_eq_mod_eq_0)
-
-lemma odd_iff_mod_2_eq_one:
-  "odd a \<longleftrightarrow> a mod 2 = 1"
-  by (simp add: even_iff_mod_2_eq_zero)
-
-lemma even_succ_div_two [simp]:
-  "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
-  by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
-
-lemma odd_succ_div_two [simp]:
-  "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
-  by (auto elim!: oddE simp add: zero_not_eq_two [symmetric] add.assoc)
-
-lemma even_two_times_div_two:
-  "even a \<Longrightarrow> 2 * (a div 2) = a"
-  by (fact dvd_mult_div_cancel)
-
-lemma odd_two_times_div_two_succ [simp]:
-  "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
-  using mult_div_mod_eq [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
- 
-end
-
-
 subsection \<open>Numeral division with a pragmatic type class\<close>
 
 text \<open>
@@ -382,445 +293,11 @@
 
 end
 
+hide_fact (open) div_less mod_less mod_less_eq_dividend mod_mult2_eq div_mult2_eq
+
 
 subsection \<open>Division on @{typ nat}\<close>
 
-context
-begin
-
-text \<open>
-  We define @{const divide} and @{const modulo} on @{typ nat} by means
-  of a characteristic relation with two input arguments
-  @{term "m::nat"}, @{term "n::nat"} and two output arguments
-  @{term "q::nat"}(uotient) and @{term "r::nat"}(emainder).
-\<close>
-
-inductive eucl_rel_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat \<Rightarrow> bool"
-  where eucl_rel_nat_by0: "eucl_rel_nat m 0 (0, m)"
-  | eucl_rel_natI: "r < n \<Longrightarrow> m = q * n + r \<Longrightarrow> eucl_rel_nat m n (q, r)"
-
-text \<open>@{const eucl_rel_nat} is total:\<close>
-
-qualified lemma eucl_rel_nat_ex:
-  obtains q r where "eucl_rel_nat m n (q, r)"
-proof (cases "n = 0")
-  case True
-  with that eucl_rel_nat_by0 show thesis
-    by blast
-next
-  case False
-  have "\<exists>q r. m = q * n + r \<and> r < n"
-  proof (induct m)
-    case 0 with \<open>n \<noteq> 0\<close>
-    have "(0::nat) = 0 * n + 0 \<and> 0 < n" by simp
-    then show ?case by blast
-  next
-    case (Suc m) then obtain q' r'
-      where m: "m = q' * n + r'" and n: "r' < n" by auto
-    then show ?case proof (cases "Suc r' < n")
-      case True
-      from m n have "Suc m = q' * n + Suc r'" by simp
-      with True show ?thesis by blast
-    next
-      case False then have "n \<le> Suc r'"
-        by (simp add: not_less)
-      moreover from n have "Suc r' \<le> n"
-        by (simp add: Suc_le_eq)
-      ultimately have "n = Suc r'" by auto
-      with m have "Suc m = Suc q' * n + 0" by simp
-      with \<open>n \<noteq> 0\<close> show ?thesis by blast
-    qed
-  qed
-  with that \<open>n \<noteq> 0\<close> eucl_rel_natI show thesis
-    by blast
-qed
-
-text \<open>@{const eucl_rel_nat} is injective:\<close>
-
-qualified lemma eucl_rel_nat_unique_div:
-  assumes "eucl_rel_nat m n (q, r)"
-    and "eucl_rel_nat m n (q', r')"
-  shows "q = q'"
-proof (cases "n = 0")
-  case True with assms show ?thesis
-    by (auto elim: eucl_rel_nat.cases)
-next
-  case False
-  have *: "q' \<le> q" if "q' * n + r' = q * n + r" "r < n" for q r q' r' :: nat
-  proof (rule ccontr)
-    assume "\<not> q' \<le> q"
-    then have "q < q'"
-      by (simp add: not_le)
-    with that show False
-      by (auto simp add: less_iff_Suc_add algebra_simps)
-  qed
-  from \<open>n \<noteq> 0\<close> assms show ?thesis
-    by (auto intro: order_antisym elim: eucl_rel_nat.cases dest: * sym split: if_splits)
-qed
-
-qualified lemma eucl_rel_nat_unique_mod:
-  assumes "eucl_rel_nat m n (q, r)"
-    and "eucl_rel_nat m n (q', r')"
-  shows "r = r'"
-proof -
-  from assms have "q' = q"
-    by (auto intro: eucl_rel_nat_unique_div)
-  with assms show ?thesis
-    by (auto elim!: eucl_rel_nat.cases)
-qed
-
-text \<open>
-  We instantiate divisibility on the natural numbers by
-  means of @{const eucl_rel_nat}:
-\<close>
-
-qualified definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
-  "divmod_nat m n = (THE qr. eucl_rel_nat m n qr)"
-
-qualified lemma eucl_rel_nat_divmod_nat:
-  "eucl_rel_nat m n (divmod_nat m n)"
-proof -
-  from eucl_rel_nat_ex
-    obtain q r where rel: "eucl_rel_nat m n (q, r)" .
-  then show ?thesis
-    by (auto simp add: divmod_nat_def intro: theI
-      elim: eucl_rel_nat_unique_div eucl_rel_nat_unique_mod)
-qed
-
-qualified lemma divmod_nat_unique:
-  "divmod_nat m n = (q, r)" if "eucl_rel_nat m n (q, r)"
-  using that
-  by (auto simp add: divmod_nat_def intro: eucl_rel_nat_divmod_nat elim: eucl_rel_nat_unique_div eucl_rel_nat_unique_mod)
-
-qualified lemma divmod_nat_zero:
-  "divmod_nat m 0 = (0, m)"
-  by (rule divmod_nat_unique) (fact eucl_rel_nat_by0)
-
-qualified lemma divmod_nat_zero_left:
-  "divmod_nat 0 n = (0, 0)"
-  by (rule divmod_nat_unique) 
-    (cases n, auto intro: eucl_rel_nat_by0 eucl_rel_natI)
-
-qualified lemma divmod_nat_base:
-  "m < n \<Longrightarrow> divmod_nat m n = (0, m)"
-  by (rule divmod_nat_unique) 
-    (cases n, auto intro: eucl_rel_nat_by0 eucl_rel_natI)
-
-qualified lemma divmod_nat_step:
-  assumes "0 < n" and "n \<le> m"
-  shows "divmod_nat m n =
-    (Suc (fst (divmod_nat (m - n) n)), snd (divmod_nat (m - n) n))"
-proof (rule divmod_nat_unique)
-  have "eucl_rel_nat (m - n) n (divmod_nat (m - n) n)"
-    by (fact eucl_rel_nat_divmod_nat)
-  then show "eucl_rel_nat m n (Suc
-    (fst (divmod_nat (m - n) n)), snd (divmod_nat (m - n) n))"
-    using assms
-      by (auto split: if_splits intro: eucl_rel_natI elim!: eucl_rel_nat.cases simp add: algebra_simps)
-qed
-
-end
-
-instantiation nat :: "{semidom_modulo, normalization_semidom}"
-begin
-
-definition normalize_nat :: "nat \<Rightarrow> nat"
-  where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
-
-definition unit_factor_nat :: "nat \<Rightarrow> nat"
-  where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
-
-lemma unit_factor_simps [simp]:
-  "unit_factor 0 = (0::nat)"
-  "unit_factor (Suc n) = 1"
-  by (simp_all add: unit_factor_nat_def)
-
-definition divide_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-  where div_nat_def: "m div n = fst (Divides.divmod_nat m n)"
-
-definition modulo_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-  where mod_nat_def: "m mod n = snd (Divides.divmod_nat m n)"
-
-lemma fst_divmod_nat [simp]:
-  "fst (Divides.divmod_nat m n) = m div n"
-  by (simp add: div_nat_def)
-
-lemma snd_divmod_nat [simp]:
-  "snd (Divides.divmod_nat m n) = m mod n"
-  by (simp add: mod_nat_def)
-
-lemma divmod_nat_div_mod:
-  "Divides.divmod_nat m n = (m div n, m mod n)"
-  by (simp add: prod_eq_iff)
-
-lemma div_nat_unique:
-  assumes "eucl_rel_nat m n (q, r)"
-  shows "m div n = q"
-  using assms
-  by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
-
-lemma mod_nat_unique:
-  assumes "eucl_rel_nat m n (q, r)"
-  shows "m mod n = r"
-  using assms
-  by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
-
-lemma eucl_rel_nat: "eucl_rel_nat m n (m div n, m mod n)"
-  using Divides.eucl_rel_nat_divmod_nat
-  by (simp add: divmod_nat_div_mod)
-
-text \<open>The ''recursion'' equations for @{const divide} and @{const modulo}\<close>
-
-lemma div_less [simp]:
-  fixes m n :: nat
-  assumes "m < n"
-  shows "m div n = 0"
-  using assms Divides.divmod_nat_base by (simp add: prod_eq_iff)
-
-lemma le_div_geq:
-  fixes m n :: nat
-  assumes "0 < n" and "n \<le> m"
-  shows "m div n = Suc ((m - n) div n)"
-  using assms Divides.divmod_nat_step by (simp add: prod_eq_iff)
-
-lemma mod_less [simp]:
-  fixes m n :: nat
-  assumes "m < n"
-  shows "m mod n = m"
-  using assms Divides.divmod_nat_base by (simp add: prod_eq_iff)
-
-lemma le_mod_geq:
-  fixes m n :: nat
-  assumes "n \<le> m"
-  shows "m mod n = (m - n) mod n"
-  using assms Divides.divmod_nat_step by (cases "n = 0") (simp_all add: prod_eq_iff)
-
-lemma mod_less_divisor [simp]:
-  fixes m n :: nat
-  assumes "n > 0"
-  shows "m mod n < n"
-  using assms eucl_rel_nat [of m n]
-    by (auto elim: eucl_rel_nat.cases)
-
-lemma mod_le_divisor [simp]:
-  fixes m n :: nat
-  assumes "n > 0"
-  shows "m mod n \<le> n"
-  using assms eucl_rel_nat [of m n]
-    by (auto elim: eucl_rel_nat.cases)
-
-instance proof
-  fix m n :: nat
-  show "m div n * n + m mod n = m"
-    using eucl_rel_nat [of m n]
-    by (auto elim: eucl_rel_nat.cases)
-next
-  fix n :: nat show "n div 0 = 0"
-    by (simp add: div_nat_def Divides.divmod_nat_zero)
-next
-  fix m n :: nat
-  assume "n \<noteq> 0"
-  then show "m * n div n = m"
-    by (auto intro!: eucl_rel_natI div_nat_unique [of _ _ _ 0])
-qed (simp_all add: unit_factor_nat_def)
-
-end
-
-text \<open>Simproc for cancelling @{const divide} and @{const modulo}\<close>
-
-lemma (in semiring_modulo) cancel_div_mod_rules:
-  "((a div b) * b + a mod b) + c = a + c"
-  "(b * (a div b) + a mod b) + c = a + c"
-  by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
-
-ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
-
-ML \<open>
-structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
-(
-  val div_name = @{const_name divide};
-  val mod_name = @{const_name modulo};
-  val mk_binop = HOLogic.mk_binop;
-  val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
-  val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
-  fun mk_sum [] = HOLogic.zero
-    | mk_sum [t] = t
-    | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
-  fun dest_sum tm =
-    if HOLogic.is_zero tm then []
-    else
-      (case try HOLogic.dest_Suc tm of
-        SOME t => HOLogic.Suc_zero :: dest_sum t
-      | NONE =>
-          (case try dest_plus tm of
-            SOME (t, u) => dest_sum t @ dest_sum u
-          | NONE => [tm]));
-
-  val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
-
-  val prove_eq_sums = Arith_Data.prove_conv2 all_tac
-    (Arith_Data.simp_all_tac @{thms add_0_left add_0_right ac_simps})
-)
-\<close>
-
-simproc_setup cancel_div_mod_nat ("(m::nat) + n") =
-  \<open>K Cancel_Div_Mod_Nat.proc\<close>
-
-lemma div_by_Suc_0 [simp]:
-  "m div Suc 0 = m"
-  using div_by_1 [of m] by simp
-
-lemma mod_by_Suc_0 [simp]:
-  "m mod Suc 0 = 0"
-  using mod_by_1 [of m] by simp
-
-lemma mod_greater_zero_iff_not_dvd:
-  fixes m n :: nat
-  shows "m mod n > 0 \<longleftrightarrow> \<not> n dvd m"
-  by (simp add: dvd_eq_mod_eq_0)
-
-instantiation nat :: unique_euclidean_semiring
-begin
-
-definition [simp]:
-  "euclidean_size_nat = (id :: nat \<Rightarrow> nat)"
-
-definition [simp]:
-  "uniqueness_constraint_nat = (top :: nat \<Rightarrow> nat \<Rightarrow> bool)"
-
-instance proof
-  fix n q r :: nat
-  assume "euclidean_size r < euclidean_size n"
-  then have "n > r"
-    by simp_all
-  then have "eucl_rel_nat (q * n + r) n (q, r)"
-    by (rule eucl_rel_natI) rule
-  then show "(q * n + r) div n = q"
-    by (rule div_nat_unique)
-qed (use mult_le_mono2 [of 1] in \<open>simp_all\<close>)
-
-end
-  
-lemma divmod_nat_if [code]:
-  "Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
-    let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
-  by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
-
-lemma mod_Suc_eq [mod_simps]:
-  "Suc (m mod n) mod n = Suc m mod n"
-proof -
-  have "(m mod n + 1) mod n = (m + 1) mod n"
-    by (simp only: mod_simps)
-  then show ?thesis
-    by simp
-qed
-
-lemma mod_Suc_Suc_eq [mod_simps]:
-  "Suc (Suc (m mod n)) mod n = Suc (Suc m) mod n"
-proof -
-  have "(m mod n + 2) mod n = (m + 2) mod n"
-    by (simp only: mod_simps)
-  then show ?thesis
-    by simp
-qed
-
-
-subsubsection \<open>Quotient\<close>
-
-lemma div_geq: "0 < n \<Longrightarrow>  \<not> m < n \<Longrightarrow> m div n = Suc ((m - n) div n)"
-by (simp add: le_div_geq linorder_not_less)
-
-lemma div_if: "0 < n \<Longrightarrow> m div n = (if m < n then 0 else Suc ((m - n) div n))"
-by (simp add: div_geq)
-
-lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"
-by simp
-
-lemma div_mult_self1_is_m [simp]: "0<n ==> (n*m) div n = (m::nat)"
-by simp
-
-lemma div_positive:
-  fixes m n :: nat
-  assumes "n > 0"
-  assumes "m \<ge> n"
-  shows "m div n > 0"
-proof -
-  from \<open>m \<ge> n\<close> obtain q where "m = n + q"
-    by (auto simp add: le_iff_add)
-  with \<open>n > 0\<close> show ?thesis by (simp add: div_add_self1)
-qed
-
-lemma div_eq_0_iff: "(a div b::nat) = 0 \<longleftrightarrow> a < b \<or> b = 0"
-  by auto (metis div_positive less_numeral_extra(3) not_less)
-
-
-subsubsection \<open>Remainder\<close>
-
-lemma mod_Suc_le_divisor [simp]:
-  "m mod Suc n \<le> n"
-  using mod_less_divisor [of "Suc n" m] by arith
-
-lemma mod_less_eq_dividend [simp]:
-  fixes m n :: nat
-  shows "m mod n \<le> m"
-proof (rule add_leD2)
-  from div_mult_mod_eq have "m div n * n + m mod n = m" .
-  then show "m div n * n + m mod n \<le> m" by auto
-qed
-
-lemma mod_geq: "\<not> m < (n::nat) \<Longrightarrow> m mod n = (m - n) mod n"
-by (simp add: le_mod_geq linorder_not_less)
-
-lemma mod_if: "m mod (n::nat) = (if m < n then m else (m - n) mod n)"
-by (simp add: le_mod_geq)
-
-
-subsubsection \<open>Quotient and Remainder\<close>
-
-lemma div_mult1_eq:
-  "(a * b) div c = a * (b div c) + a * (b mod c) div (c::nat)"
-  by (cases "c = 0")
-     (auto simp add: algebra_simps distrib_left [symmetric]
-     intro!: div_nat_unique [of _ _ _ "(a * (b mod c)) mod c"] eucl_rel_natI)
-
-lemma eucl_rel_nat_add1_eq:
-  "eucl_rel_nat a c (aq, ar) \<Longrightarrow> eucl_rel_nat b c (bq, br)
-   \<Longrightarrow> eucl_rel_nat (a + b) c (aq + bq + (ar + br) div c, (ar + br) mod c)"
-  by (auto simp add: split_ifs algebra_simps elim!: eucl_rel_nat.cases intro: eucl_rel_nat_by0 eucl_rel_natI)
-
-(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
-lemma div_add1_eq:
-  "(a + b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
-by (blast intro: eucl_rel_nat_add1_eq [THEN div_nat_unique] eucl_rel_nat)
-
-lemma eucl_rel_nat_mult2_eq:
-  assumes "eucl_rel_nat a b (q, r)"
-  shows "eucl_rel_nat a (b * c) (q div c, b *(q mod c) + r)"
-proof (cases "c = 0")
-  case True
-  with assms show ?thesis
-    by (auto intro: eucl_rel_nat_by0 elim!: eucl_rel_nat.cases simp add: ac_simps)
-next
-  case False
-  { assume "r < b"
-    with False have "b * (q mod c) + r < b * c"
-      apply (cut_tac m = q and n = c in mod_less_divisor)
-      apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
-      apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst)
-      apply (simp add: add_mult_distrib2)
-      done
-    then have "r + b * (q mod c) < b * c"
-      by (simp add: ac_simps)
-  } with assms False show ?thesis
-    by (auto simp add: algebra_simps add_mult_distrib2 [symmetric] elim!: eucl_rel_nat.cases intro: eucl_rel_nat.intros)
-qed
-
-lemma div_mult2_eq: "a div (b * c) = (a div b) div (c::nat)"
-by (force simp add: eucl_rel_nat [THEN eucl_rel_nat_mult2_eq, THEN div_nat_unique])
-
-lemma mod_mult2_eq: "a mod (b * c) = b * (a div b mod c) + a mod (b::nat)"
-by (auto simp add: mult.commute eucl_rel_nat [THEN eucl_rel_nat_mult2_eq, THEN mod_nat_unique])
-
 instantiation nat :: unique_euclidean_semiring_numeral
 begin
 
@@ -834,370 +311,15 @@
     in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
     else (2 * q, r))"
 
-instance
-  by standard (auto intro: div_positive simp add: divmod'_nat_def divmod_step_nat_def mod_mult2_eq div_mult2_eq)
+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]
-  
 
-subsubsection \<open>Further Facts about Quotient and Remainder\<close>
-
-lemma div_le_mono:
-  fixes m n k :: nat
-  assumes "m \<le> n"
-  shows "m div k \<le> n div k"
-proof -
-  from assms obtain q where "n = m + q"
-    by (auto simp add: le_iff_add)
-  then show ?thesis
-    by (simp add: div_add1_eq [of m q k])
-qed
-
-(* Antimonotonicity of div in second argument *)
-lemma div_le_mono2: "!!m::nat. [| 0<m; m\<le>n |] ==> (k div n) \<le> (k div m)"
-apply (subgoal_tac "0<n")
- prefer 2 apply simp
-apply (induct_tac k rule: nat_less_induct)
-apply (rename_tac "k")
-apply (case_tac "k<n", simp)
-apply (subgoal_tac "~ (k<m) ")
- prefer 2 apply simp
-apply (simp add: div_geq)
-apply (subgoal_tac "(k-n) div n \<le> (k-m) div n")
- prefer 2
- apply (blast intro: div_le_mono diff_le_mono2)
-apply (rule le_trans, simp)
-apply (simp)
-done
-
-lemma div_le_dividend [simp]: "m div n \<le> (m::nat)"
-apply (case_tac "n=0", simp)
-apply (subgoal_tac "m div n \<le> m div 1", simp)
-apply (rule div_le_mono2)
-apply (simp_all (no_asm_simp))
-done
-
-(* Similar for "less than" *)
-lemma div_less_dividend [simp]:
-  "\<lbrakk>(1::nat) < n; 0 < m\<rbrakk> \<Longrightarrow> m div n < m"
-apply (induct m rule: nat_less_induct)
-apply (rename_tac "m")
-apply (case_tac "m<n", simp)
-apply (subgoal_tac "0<n")
- prefer 2 apply simp
-apply (simp add: div_geq)
-apply (case_tac "n<m")
- apply (subgoal_tac "(m-n) div n < (m-n) ")
-  apply (rule impI less_trans_Suc)+
-apply assumption
-  apply (simp_all)
-done
-
-text\<open>A fact for the mutilated chess board\<close>
-lemma mod_Suc: "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"
-apply (case_tac "n=0", simp)
-apply (induct "m" rule: nat_less_induct)
-apply (case_tac "Suc (na) <n")
-(* case Suc(na) < n *)
-apply (frule lessI [THEN less_trans], simp add: less_not_refl3)
-(* case n \<le> Suc(na) *)
-apply (simp add: linorder_not_less le_Suc_eq mod_geq)
-apply (auto simp add: Suc_diff_le le_mod_geq)
-done
-
-lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"
-by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
-
-lemmas mod_eq_0D [dest!] = mod_eq_0_iff [THEN iffD1]
-
-(*Loses information, namely we also have r<d provided d is nonzero*)
-lemma mod_eqD:
-  fixes m d r q :: nat
-  assumes "m mod d = r"
-  shows "\<exists>q. m = r + q * d"
-proof -
-  from div_mult_mod_eq obtain q where "q * d + m mod d = m" by blast
-  with assms have "m = r + q * d" by simp
-  then show ?thesis ..
-qed
-
-lemma split_div:
- "P(n div k :: nat) =
- ((k = 0 \<longrightarrow> P 0) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P i)))"
- (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
-proof
-  assume P: ?P
-  show ?Q
-  proof (cases)
-    assume "k = 0"
-    with P show ?Q by simp
-  next
-    assume not0: "k \<noteq> 0"
-    thus ?Q
-    proof (simp, intro allI impI)
-      fix i j
-      assume n: "n = k*i + j" and j: "j < k"
-      show "P i"
-      proof (cases)
-        assume "i = 0"
-        with n j P show "P i" by simp
-      next
-        assume "i \<noteq> 0"
-        with not0 n j P show "P i" by(simp add:ac_simps)
-      qed
-    qed
-  qed
-next
-  assume Q: ?Q
-  show ?P
-  proof (cases)
-    assume "k = 0"
-    with Q show ?P by simp
-  next
-    assume not0: "k \<noteq> 0"
-    with Q have R: ?R by simp
-    from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
-    show ?P by simp
-  qed
-qed
-
-lemma split_div_lemma:
-  assumes "0 < n"
-  shows "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> q = ((m::nat) div n)" (is "?lhs \<longleftrightarrow> ?rhs")
-proof
-  assume ?rhs
-  with minus_mod_eq_mult_div [symmetric] have nq: "n * q = m - (m mod n)" by simp
-  then have A: "n * q \<le> m" by simp
-  have "n - (m mod n) > 0" using mod_less_divisor assms by auto
-  then have "m < m + (n - (m mod n))" by simp
-  then have "m < n + (m - (m mod n))" by simp
-  with nq have "m < n + n * q" by simp
-  then have B: "m < n * Suc q" by simp
-  from A B show ?lhs ..
-next
-  assume P: ?lhs
-  then have "eucl_rel_nat m n (q, m - n * q)"
-    by (auto intro: eucl_rel_natI simp add: ac_simps)
-  then have "m div n = q"
-    by (rule div_nat_unique)
-  then show ?rhs by simp
-qed
-
-theorem split_div':
-  "P ((m::nat) div n) = ((n = 0 \<and> P 0) \<or>
-   (\<exists>q. (n * q \<le> m \<and> m < n * (Suc q)) \<and> P q))"
-  apply (cases "0 < n")
-  apply (simp only: add: split_div_lemma)
-  apply simp_all
-  done
-
-lemma split_mod:
- "P(n mod k :: nat) =
- ((k = 0 \<longrightarrow> P n) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P j)))"
- (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
-proof
-  assume P: ?P
-  show ?Q
-  proof (cases)
-    assume "k = 0"
-    with P show ?Q by simp
-  next
-    assume not0: "k \<noteq> 0"
-    thus ?Q
-    proof (simp, intro allI impI)
-      fix i j
-      assume "n = k*i + j" "j < k"
-      thus "P j" using not0 P by (simp add: ac_simps)
-    qed
-  qed
-next
-  assume Q: ?Q
-  show ?P
-  proof (cases)
-    assume "k = 0"
-    with Q show ?P by simp
-  next
-    assume not0: "k \<noteq> 0"
-    with Q have R: ?R by simp
-    from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
-    show ?P by simp
-  qed
-qed
-
-lemma div_eq_dividend_iff: "a \<noteq> 0 \<Longrightarrow> (a :: nat) div b = a \<longleftrightarrow> b = 1"
-  apply rule
-  apply (cases "b = 0")
-  apply simp_all
-  apply (metis (full_types) One_nat_def Suc_lessI div_less_dividend less_not_refl3)
-  done
-
-lemma (in field_char_0) of_nat_div:
-  "of_nat (m div n) = ((of_nat m - of_nat (m mod n)) / of_nat n)"
-proof -
-  have "of_nat (m div n) = ((of_nat (m div n * n + m mod n) - of_nat (m mod n)) / of_nat n :: 'a)"
-    unfolding of_nat_add by (cases "n = 0") simp_all
-  then show ?thesis
-    by simp
-qed
-
-
-subsubsection \<open>An ``induction'' law for modulus arithmetic.\<close>
-
-lemma mod_induct_0:
-  assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
-  and base: "P i" and i: "i<p"
-  shows "P 0"
-proof (rule ccontr)
-  assume contra: "\<not>(P 0)"
-  from i have p: "0<p" by simp
-  have "\<forall>k. 0<k \<longrightarrow> \<not> P (p-k)" (is "\<forall>k. ?A k")
-  proof
-    fix k
-    show "?A k"
-    proof (induct k)
-      show "?A 0" by simp  \<comment> "by contradiction"
-    next
-      fix n
-      assume ih: "?A n"
-      show "?A (Suc n)"
-      proof (clarsimp)
-        assume y: "P (p - Suc n)"
-        have n: "Suc n < p"
-        proof (rule ccontr)
-          assume "\<not>(Suc n < p)"
-          hence "p - Suc n = 0"
-            by simp
-          with y contra show "False"
-            by simp
-        qed
-        hence n2: "Suc (p - Suc n) = p-n" by arith
-        from p have "p - Suc n < p" by arith
-        with y step have z: "P ((Suc (p - Suc n)) mod p)"
-          by blast
-        show "False"
-        proof (cases "n=0")
-          case True
-          with z n2 contra show ?thesis by simp
-        next
-          case False
-          with p have "p-n < p" by arith
-          with z n2 False ih show ?thesis by simp
-        qed
-      qed
-    qed
-  qed
-  moreover
-  from i obtain k where "0<k \<and> i+k=p"
-    by (blast dest: less_imp_add_positive)
-  hence "0<k \<and> i=p-k" by auto
-  moreover
-  note base
-  ultimately
-  show "False" by blast
-qed
-
-lemma mod_induct:
-  assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
-  and base: "P i" and i: "i<p" and j: "j<p"
-  shows "P j"
-proof -
-  have "\<forall>j<p. P j"
-  proof
-    fix j
-    show "j<p \<longrightarrow> P j" (is "?A j")
-    proof (induct j)
-      from step base i show "?A 0"
-        by (auto elim: mod_induct_0)
-    next
-      fix k
-      assume ih: "?A k"
-      show "?A (Suc k)"
-      proof
-        assume suc: "Suc k < p"
-        hence k: "k<p" by simp
-        with ih have "P k" ..
-        with step k have "P (Suc k mod p)"
-          by blast
-        moreover
-        from suc have "Suc k mod p = Suc k"
-          by simp
-        ultimately
-        show "P (Suc k)" by simp
-      qed
-    qed
-  qed
-  with j show ?thesis by blast
-qed
-
-lemma div2_Suc_Suc [simp]: "Suc (Suc m) div 2 = Suc (m div 2)"
-  by (simp add: numeral_2_eq_2 le_div_geq)
-
-lemma mod2_Suc_Suc [simp]: "Suc (Suc m) mod 2 = m mod 2"
-  by (simp add: numeral_2_eq_2 le_mod_geq)
-
-lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
-by (simp add: mult_2 [symmetric])
-
-lemma mod2_gr_0 [simp]: "0 < (m::nat) mod 2 \<longleftrightarrow> m mod 2 = 1"
-proof -
-  { fix n :: nat have  "(n::nat) < 2 \<Longrightarrow> n = 0 \<or> n = 1" by (cases n) simp_all }
-  moreover have "m mod 2 < 2" by simp
-  ultimately have "m mod 2 = 0 \<or> m mod 2 = 1" .
-  then show ?thesis by auto
-qed
-
-text\<open>These lemmas collapse some needless occurrences of Suc:
-    at least three Sucs, since two and fewer are rewritten back to Suc again!
-    We already have some rules to simplify operands smaller than 3.\<close>
-
-lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"
-by (simp add: Suc3_eq_add_3)
-
-lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"
-by (simp add: Suc3_eq_add_3)
-
-lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"
-by (simp add: Suc3_eq_add_3)
-
-lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
-by (simp add: Suc3_eq_add_3)
-
-lemmas Suc_div_eq_add3_div_numeral [simp] = Suc_div_eq_add3_div [of _ "numeral v"] for v
-lemmas Suc_mod_eq_add3_mod_numeral [simp] = Suc_mod_eq_add3_mod [of _ "numeral v"] for v
-
-lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1"
-apply (induct "m")
-apply (simp_all add: mod_Suc)
-done
-
-declare Suc_times_mod_eq [of "numeral w", simp] for w
-
-lemma Suc_div_le_mono [simp]: "n div k \<le> (Suc n) div k"
-by (simp add: div_le_mono)
-
-lemma Suc_n_div_2_gt_zero [simp]: "(0::nat) < n ==> 0 < (n + 1) div 2"
-by (cases n) simp_all
-
-lemma div_2_gt_zero [simp]: assumes A: "(1::nat) < n" shows "0 < n div 2"
-proof -
-  from A have B: "0 < n - 1" and C: "n - 1 + 1 = n" by simp_all
-  from Suc_n_div_2_gt_zero [OF B] C show ?thesis by simp
-qed
-
-lemma mod_mult_self3' [simp]: "Suc (k * n + m) mod n = Suc m mod n"
-  using mod_mult_self3 [of k n "Suc m"] by simp
-
-lemma mod_Suc_eq_Suc_mod: "Suc m mod n = Suc (m mod n) mod n"
-apply (subst mod_Suc [of m])
-apply (subst mod_Suc [of "m mod n"], simp)
-done
-
-lemma mod_2_not_eq_zero_eq_one_nat:
-  fixes n :: nat
-  shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
-  by (fact not_mod_2_eq_0_eq_1)
+lemma odd_Suc_minus_one [simp]: "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
+  by (auto elim: oddE)
 
 lemma even_Suc_div_two [simp]:
   "even n \<Longrightarrow> Suc n div 2 = n div 2"
@@ -1245,6 +367,11 @@
   qed
 qed
 
+lemma mod_2_not_eq_zero_eq_one_nat:
+  fixes n :: nat
+  shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
+  by (fact not_mod_2_eq_0_eq_1)
+
 lemma Suc_0_div_numeral [simp]:
   fixes k l :: num
   shows "Suc 0 div numeral k = fst (divmod Num.One k)"
@@ -1255,6 +382,27 @@
   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
+
 
 subsection \<open>Division on @{typ int}\<close>
 
@@ -2225,7 +1373,7 @@
 lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
 apply (subgoal_tac "nat x div nat k < nat x")
  apply (simp add: nat_div_distrib [symmetric])
-apply (rule Divides.div_less_dividend, simp_all)
+apply (rule div_less_dividend, simp_all)
 done
 
 lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y mod n" and xy:"y \<le> x"
@@ -2258,11 +1406,12 @@
   thus  ?lhs by simp
 qed
 
+
 subsubsection \<open>Dedicated simproc for calculation\<close>
 
 text \<open>
   There is space for improvement here: the calculation itself
-  could be carried outside the logic, and a generic simproc
+  could be carried out outside the logic, and a generic simproc
   (simplifier setup) for generic calculation would be helpful. 
 \<close>
 
@@ -2348,4 +1497,39 @@
 
 declare minus_div_mult_eq_mod [symmetric, nitpick_unfold]
 
+
+subsubsection \<open>Lemmas of doubtful value\<close>
+
+lemma mod_mult_self3':
+  "Suc (k * n + m) mod n = Suc m mod n"
+  by (fact Suc_mod_mult_self3)
+
+lemma mod_Suc_eq_Suc_mod:
+  "Suc m mod n = Suc (m mod n) mod n"
+  by (simp add: mod_simps)
+
+lemma div_geq:
+  "m div n = Suc ((m - n) div n)" if "0 < n" and " \<not> m < n" for m n :: nat
+  by (rule le_div_geq) (use that in \<open>simp_all add: not_less\<close>)
+
+lemma mod_geq:
+  "m mod n = (m - n) mod n" if "\<not> m < n" for m n :: nat
+  by (rule le_mod_geq) (use that in \<open>simp add: not_less\<close>)
+
+lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"
+  by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
+
+lemmas mod_eq_0D [dest!] = mod_eq_0_iff [THEN iffD1]
+
+(*Loses information, namely we also have r<d provided d is nonzero*)
+lemma mod_eqD:
+  fixes m d r q :: nat
+  assumes "m mod d = r"
+  shows "\<exists>q. m = r + q * d"
+proof -
+  from div_mult_mod_eq obtain q where "q * d + m mod d = m" by blast
+  with assms have "m = r + q * d" by simp
+  then show ?thesis ..
+qed
+
 end
diff -r c3631f32dfeb -r 1907167b6038 src/HOL/Euclidean_Division.thy
--- a/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -6,9 +6,19 @@
 section \<open>Uniquely determined division in euclidean (semi)rings\<close>
 
 theory Euclidean_Division
-  imports Nat_Transfer
+  imports Nat_Transfer Lattices_Big
 begin
 
+subsection \<open>Prelude: simproc for cancelling @{const divide} and @{const modulo}\<close>
+
+lemma (in semiring_modulo) cancel_div_mod_rules:
+  "((a div b) * b + a mod b) + c = a + c"
+  "(b * (a div b) + a mod b) + c = a + c"
+  by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
+
+ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
+
+
 subsection \<open>Euclidean (semi)rings with explicit division and remainder\<close>
   
 class euclidean_semiring = semidom_modulo + normalization_semidom + 
@@ -639,4 +649,657 @@
 
 end
 
+
+subsection \<open>Euclidean division on @{typ nat}\<close>
+
+instantiation nat :: unique_euclidean_semiring
+begin
+
+definition normalize_nat :: "nat \<Rightarrow> nat"
+  where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
+
+definition unit_factor_nat :: "nat \<Rightarrow> nat"
+  where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
+
+lemma unit_factor_simps [simp]:
+  "unit_factor 0 = (0::nat)"
+  "unit_factor (Suc n) = 1"
+  by (simp_all add: unit_factor_nat_def)
+
+definition euclidean_size_nat :: "nat \<Rightarrow> nat"
+  where [simp]: "euclidean_size_nat = id"
+
+definition uniqueness_constraint_nat :: "nat \<Rightarrow> nat \<Rightarrow> bool"
+  where [simp]: "uniqueness_constraint_nat = \<top>"
+
+definition divide_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+  where "m div n = (if n = 0 then 0 else Max {k::nat. k * n \<le> m})"
+
+definition modulo_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+  where "m mod n = m - (m div n * (n::nat))"
+
+instance proof
+  fix m n :: nat
+  have ex: "\<exists>k. k * n \<le> l" for l :: nat
+    by (rule exI [of _ 0]) simp
+  have fin: "finite {k. k * n \<le> l}" if "n > 0" for l
+  proof -
+    from that have "{k. k * n \<le> l} \<subseteq> {k. k \<le> l}"
+      by (cases n) auto
+    then show ?thesis
+      by (rule finite_subset) simp
+  qed
+  have mult_div_unfold: "n * (m div n) = Max {l. l \<le> m \<and> n dvd l}"
+  proof (cases "n = 0")
+    case True
+    moreover have "{l. l = 0 \<and> l \<le> m} = {0::nat}"
+      by auto
+    ultimately show ?thesis
+      by simp
+  next
+    case False
+    with ex [of m] fin have "n * Max {k. k * n \<le> m} = Max (times n ` {k. k * n \<le> m})"
+      by (auto simp add: nat_mult_max_right intro: hom_Max_commute)
+    also have "times n ` {k. k * n \<le> m} = {l. l \<le> m \<and> n dvd l}"
+      by (auto simp add: ac_simps elim!: dvdE)
+    finally show ?thesis
+      using False by (simp add: divide_nat_def ac_simps)
+  qed
+  show "n div 0 = 0"
+    by (simp add: divide_nat_def)
+  have less_eq: "m div n * n \<le> m"
+    by (auto simp add: mult_div_unfold ac_simps intro: Max.boundedI)
+  then show "m div n * n + m mod n = m"
+    by (simp add: modulo_nat_def)
+  assume "n \<noteq> 0" 
+  show "m * n div n = m"
+    using \<open>n \<noteq> 0\<close> by (auto simp add: divide_nat_def ac_simps intro: Max_eqI)
+  show "euclidean_size (m mod n) < euclidean_size n"
+  proof -
+    have "m < Suc (m div n) * n"
+    proof (rule ccontr)
+      assume "\<not> m < Suc (m div n) * n"
+      then have "Suc (m div n) * n \<le> m"
+        by (simp add: not_less)
+      moreover from \<open>n \<noteq> 0\<close> have "Max {k. k * n \<le> m} < Suc (m div n)"
+        by (simp add: divide_nat_def)
+      with \<open>n \<noteq> 0\<close> ex fin have "\<And>k. k * n \<le> m \<Longrightarrow> k < Suc (m div n)"
+        by auto
+      ultimately have "Suc (m div n) < Suc (m div n)"
+        by blast
+      then show False
+        by simp
+    qed
+    with \<open>n \<noteq> 0\<close> show ?thesis
+      by (simp add: modulo_nat_def)
+  qed
+  show "euclidean_size m \<le> euclidean_size (m * n)"
+    using \<open>n \<noteq> 0\<close> by (cases n) simp_all
+  fix q r :: nat
+  show "(q * n + r) div n = q" if "euclidean_size r < euclidean_size n"
+  proof -
+    from that have "r < n"
+      by simp
+    have "k \<le> q" if "k * n \<le> q * n + r" for k
+    proof (rule ccontr)
+      assume "\<not> k \<le> q"
+      then have "q < k"
+        by simp
+      then obtain l where "k = Suc (q + l)"
+        by (auto simp add: less_iff_Suc_add)
+      with \<open>r < n\<close> that show False
+        by (simp add: algebra_simps)
+    qed
+    with \<open>n \<noteq> 0\<close> ex fin show ?thesis
+      by (auto simp add: divide_nat_def Max_eq_iff)
+  qed
+qed (simp_all add: unit_factor_nat_def)
+
 end
+
+text \<open>Tool support\<close>
+
+ML \<open>
+structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
+(
+  val div_name = @{const_name divide};
+  val mod_name = @{const_name modulo};
+  val mk_binop = HOLogic.mk_binop;
+  val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
+  val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
+  fun mk_sum [] = HOLogic.zero
+    | mk_sum [t] = t
+    | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
+  fun dest_sum tm =
+    if HOLogic.is_zero tm then []
+    else
+      (case try HOLogic.dest_Suc tm of
+        SOME t => HOLogic.Suc_zero :: dest_sum t
+      | NONE =>
+          (case try dest_plus tm of
+            SOME (t, u) => dest_sum t @ dest_sum u
+          | NONE => [tm]));
+
+  val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
+
+  val prove_eq_sums = Arith_Data.prove_conv2 all_tac
+    (Arith_Data.simp_all_tac @{thms add_0_left add_0_right ac_simps})
+)
+\<close>
+
+simproc_setup cancel_div_mod_nat ("(m::nat) + n") =
+  \<open>K Cancel_Div_Mod_Nat.proc\<close>
+
+lemma div_nat_eqI:
+  "m div n = q" if "n * q \<le> m" and "m < n * Suc q" for m n q :: nat
+  by (rule div_eqI [of _ "m - n * q"]) (use that in \<open>simp_all add: algebra_simps\<close>)
+
+lemma mod_nat_eqI:
+  "m mod n = r" if "r < n" and "r \<le> m" and "n dvd m - r" for m n r :: nat
+  by (rule mod_eqI [of _ _ "(m - r) div n"]) (use that in \<open>simp_all add: algebra_simps\<close>)
+
+lemma div_mult_self_is_m [simp]:
+  "m * n div n = m" if "n > 0" for m n :: nat
+  using that by simp
+
+lemma div_mult_self1_is_m [simp]:
+  "n * m div n = m" if "n > 0" for m n :: nat
+  using that by simp
+
+lemma mod_less_divisor [simp]:
+  "m mod n < n" if "n > 0" for m n :: nat
+  using mod_size_less [of n m] that by simp
+
+lemma mod_le_divisor [simp]:
+  "m mod n \<le> n" if "n > 0" for m n :: nat
+  using that by (auto simp add: le_less)
+
+lemma div_times_less_eq_dividend [simp]:
+  "m div n * n \<le> m" for m n :: nat
+  by (simp add: minus_mod_eq_div_mult [symmetric])
+
+lemma times_div_less_eq_dividend [simp]:
+  "n * (m div n) \<le> m" for m n :: nat
+  using div_times_less_eq_dividend [of m n]
+  by (simp add: ac_simps)
+
+lemma dividend_less_div_times:
+  "m < n + (m div n) * n" if "0 < n" for m n :: nat
+proof -
+  from that have "m mod n < n"
+    by simp
+  then show ?thesis
+    by (simp add: minus_mod_eq_div_mult [symmetric])
+qed
+
+lemma dividend_less_times_div:
+  "m < n + n * (m div n)" if "0 < n" for m n :: nat
+  using dividend_less_div_times [of n m] that
+  by (simp add: ac_simps)
+
+lemma mod_Suc_le_divisor [simp]:
+  "m mod Suc n \<le> n"
+  using mod_less_divisor [of "Suc n" m] by arith
+
+lemma mod_less_eq_dividend [simp]:
+  "m mod n \<le> m" for m n :: nat
+proof (rule add_leD2)
+  from div_mult_mod_eq have "m div n * n + m mod n = m" .
+  then show "m div n * n + m mod n \<le> m" by auto
+qed
+
+lemma
+  div_less [simp]: "m div n = 0"
+  and mod_less [simp]: "m mod n = m"
+  if "m < n" for m n :: nat
+  using that by (auto intro: div_eqI mod_eqI) 
+
+lemma le_div_geq:
+  "m div n = Suc ((m - n) div n)" if "0 < n" and "n \<le> m" for m n :: nat
+proof -
+  from \<open>n \<le> m\<close> obtain q where "m = n + q"
+    by (auto simp add: le_iff_add)
+  with \<open>0 < n\<close> show ?thesis
+    by (simp add: div_add_self1)
+qed
+
+lemma le_mod_geq:
+  "m mod n = (m - n) mod n" if "n \<le> m" for m n :: nat
+proof -
+  from \<open>n \<le> m\<close> obtain q where "m = n + q"
+    by (auto simp add: le_iff_add)
+  then show ?thesis
+    by simp
+qed
+
+lemma div_if:
+  "m div n = (if m < n \<or> n = 0 then 0 else Suc ((m - n) div n))"
+  by (simp add: le_div_geq)
+
+lemma mod_if:
+  "m mod n = (if m < n then m else (m - n) mod n)" for m n :: nat
+  by (simp add: le_mod_geq)
+
+lemma div_eq_0_iff:
+  "m div n = 0 \<longleftrightarrow> m < n \<or> n = 0" for m n :: nat
+  by (simp add: div_if)
+
+lemma div_greater_zero_iff:
+  "m div n > 0 \<longleftrightarrow> n \<le> m \<and> n > 0" for m n :: nat
+  using div_eq_0_iff [of m n] by auto
+
+lemma mod_greater_zero_iff_not_dvd:
+  "m mod n > 0 \<longleftrightarrow> \<not> n dvd m" for m n :: nat
+  by (simp add: dvd_eq_mod_eq_0)
+
+lemma div_by_Suc_0 [simp]:
+  "m div Suc 0 = m"
+  using div_by_1 [of m] by simp
+
+lemma mod_by_Suc_0 [simp]:
+  "m mod Suc 0 = 0"
+  using mod_by_1 [of m] by simp
+
+lemma div2_Suc_Suc [simp]:
+  "Suc (Suc m) div 2 = Suc (m div 2)"
+  by (simp add: numeral_2_eq_2 le_div_geq)
+
+lemma Suc_n_div_2_gt_zero [simp]:
+  "0 < Suc n div 2" if "n > 0" for n :: nat
+  using that by (cases n) simp_all
+
+lemma div_2_gt_zero [simp]:
+  "0 < n div 2" if "Suc 0 < n" for n :: nat
+  using that Suc_n_div_2_gt_zero [of "n - 1"] by simp
+
+lemma mod2_Suc_Suc [simp]:
+  "Suc (Suc m) mod 2 = m mod 2"
+  by (simp add: numeral_2_eq_2 le_mod_geq)
+
+lemma add_self_div_2 [simp]:
+  "(m + m) div 2 = m" for m :: nat
+  by (simp add: mult_2 [symmetric])
+
+lemma add_self_mod_2 [simp]:
+  "(m + m) mod 2 = 0" for m :: nat
+  by (simp add: mult_2 [symmetric])
+
+lemma mod2_gr_0 [simp]:
+  "0 < m mod 2 \<longleftrightarrow> m mod 2 = 1" for m :: nat
+proof -
+  have "m mod 2 < 2"
+    by (rule mod_less_divisor) simp
+  then have "m mod 2 = 0 \<or> m mod 2 = 1"
+    by arith
+  then show ?thesis
+    by auto     
+qed
+
+lemma mod_Suc_eq [mod_simps]:
+  "Suc (m mod n) mod n = Suc m mod n"
+proof -
+  have "(m mod n + 1) mod n = (m + 1) mod n"
+    by (simp only: mod_simps)
+  then show ?thesis
+    by simp
+qed
+
+lemma mod_Suc_Suc_eq [mod_simps]:
+  "Suc (Suc (m mod n)) mod n = Suc (Suc m) mod n"
+proof -
+  have "(m mod n + 2) mod n = (m + 2) mod n"
+    by (simp only: mod_simps)
+  then show ?thesis
+    by simp
+qed
+
+lemma
+  Suc_mod_mult_self1 [simp]: "Suc (m + k * n) mod n = Suc m mod n"
+  and Suc_mod_mult_self2 [simp]: "Suc (m + n * k) mod n = Suc m mod n"
+  and Suc_mod_mult_self3 [simp]: "Suc (k * n + m) mod n = Suc m mod n"
+  and Suc_mod_mult_self4 [simp]: "Suc (n * k + m) mod n = Suc m mod n"
+  by (subst mod_Suc_eq [symmetric], simp add: mod_simps)+
+
+lemma div_mult1_eq: -- \<open>TODO: Generalization candidate\<close>
+  "(a * b) div c = a * (b div c) + a * (b mod c) div c" for a b c :: nat
+  apply (cases "c = 0")
+   apply simp
+  apply (rule div_eqI [of _ "(a * (b mod c)) mod c"])
+     apply (auto simp add: algebra_simps distrib_left [symmetric])
+  done
+
+lemma div_add1_eq: -- \<open>NOT suitable for rewriting: the RHS has an instance of the LHS\<close>
+   -- \<open>TODO: Generalization candidate\<close>
+  "(a + b) div c = a div c + b div c + ((a mod c + b mod c) div c)" for a b c :: nat
+  apply (cases "c = 0")
+   apply simp
+  apply (rule div_eqI [of _ "(a mod c + b mod c) mod c"])
+  apply (auto simp add: algebra_simps)
+  done
+
+context
+  fixes m n q :: nat
+begin
+
+private lemma eucl_rel_mult2:
+  "m mod n + n * (m div n mod q) < n * q"
+  if "n > 0" and "q > 0"
+proof -
+  from \<open>n > 0\<close> have "m mod n < n"
+    by (rule mod_less_divisor)
+  from \<open>q > 0\<close> have "m div n mod q < q"
+    by (rule mod_less_divisor)
+  then obtain s where "q = Suc (m div n mod q + s)"
+    by (blast dest: less_imp_Suc_add)
+  moreover have "m mod n + n * (m div n mod q) < n * Suc (m div n mod q + s)"
+    using \<open>m mod n < n\<close> by (simp add: add_mult_distrib2)
+  ultimately show ?thesis
+    by simp
+qed
+
+lemma div_mult2_eq:
+  "m div (n * q) = (m div n) div q"
+proof (cases "n = 0 \<or> q = 0")
+  case True
+  then show ?thesis
+    by auto
+next
+  case False
+  with eucl_rel_mult2 show ?thesis
+    by (auto intro: div_eqI [of _ "n * (m div n mod q) + m mod n"]
+      simp add: algebra_simps add_mult_distrib2 [symmetric])
+qed
+
+lemma mod_mult2_eq:
+  "m mod (n * q) = n * (m div n mod q) + m mod n"
+proof (cases "n = 0 \<or> q = 0")
+  case True
+  then show ?thesis
+    by auto
+next
+  case False
+  with eucl_rel_mult2 show ?thesis
+    by (auto intro: mod_eqI [of _ _ "(m div n) div q"]
+      simp add: algebra_simps add_mult_distrib2 [symmetric])
+qed
+
+end
+
+lemma div_le_mono:
+  "m div k \<le> n div k" if "m \<le> n" for m n k :: nat
+proof -
+  from that obtain q where "n = m + q"
+    by (auto simp add: le_iff_add)
+  then show ?thesis
+    by (simp add: div_add1_eq [of m q k])
+qed
+
+text \<open>Antimonotonicity of @{const divide} in second argument\<close>
+
+lemma div_le_mono2:
+  "k div n \<le> k div m" if "0 < m" and "m \<le> n" for m n k :: nat
+using that proof (induct k arbitrary: m rule: less_induct)
+  case (less k)
+  show ?case
+  proof (cases "n \<le> k")
+    case False
+    then show ?thesis
+      by simp
+  next
+    case True
+    have "(k - n) div n \<le> (k - m) div n"
+      using less.prems
+      by (blast intro: div_le_mono diff_le_mono2)
+    also have "\<dots> \<le> (k - m) div m"
+      using \<open>n \<le> k\<close> less.prems less.hyps [of "k - m" m]
+      by simp
+    finally show ?thesis
+      using \<open>n \<le> k\<close> less.prems
+      by (simp add: le_div_geq)
+  qed
+qed
+
+lemma div_le_dividend [simp]:
+  "m div n \<le> m" for m n :: nat
+  using div_le_mono2 [of 1 n m] by (cases "n = 0") simp_all
+
+lemma div_less_dividend [simp]:
+  "m div n < m" if "1 < n" and "0 < m" for m n :: nat
+using that proof (induct m rule: less_induct)
+  case (less m)
+  show ?case
+  proof (cases "n < m")
+    case False
+    with less show ?thesis
+      by (cases "n = m") simp_all
+  next
+    case True
+    then show ?thesis
+      using less.hyps [of "m - n"] less.prems
+      by (simp add: le_div_geq)
+  qed
+qed
+
+lemma div_eq_dividend_iff:
+  "m div n = m \<longleftrightarrow> n = 1" if "m > 0" for m n :: nat
+proof
+  assume "n = 1"
+  then show "m div n = m"
+    by simp
+next
+  assume P: "m div n = m"
+  show "n = 1"
+  proof (rule ccontr)
+    have "n \<noteq> 0"
+      by (rule ccontr) (use that P in auto)
+    moreover assume "n \<noteq> 1"
+    ultimately have "n > 1"
+      by simp
+    with that have "m div n < m"
+      by simp
+    with P show False
+      by simp
+  qed
+qed
+
+lemma less_mult_imp_div_less:
+  "m div n < i" if "m < i * n" for m n i :: nat
+proof -
+  from that have "i * n > 0"
+    by (cases "i * n = 0") simp_all
+  then have "i > 0" and "n > 0"
+    by simp_all
+  have "m div n * n \<le> m"
+    by simp
+  then have "m div n * n < i * n"
+    using that by (rule le_less_trans)
+  with \<open>n > 0\<close> show ?thesis
+    by simp
+qed
+
+text \<open>A fact for the mutilated chess board\<close>
+
+lemma mod_Suc:
+  "Suc m mod n = (if Suc (m mod n) = n then 0 else Suc (m mod n))" (is "_ = ?rhs")
+proof (cases "n = 0")
+  case True
+  then show ?thesis
+    by simp
+next
+  case False
+  have "Suc m mod n = Suc (m mod n) mod n"
+    by (simp add: mod_simps)
+  also have "\<dots> = ?rhs"
+    using False by (auto intro!: mod_nat_eqI intro: neq_le_trans simp add: Suc_le_eq)
+  finally show ?thesis .
+qed
+
+lemma Suc_times_mod_eq:
+  "Suc (m * n) mod m = 1" if "Suc 0 < m"
+  using that by (simp add: mod_Suc)
+
+lemma Suc_times_numeral_mod_eq [simp]:
+  "Suc (numeral k * n) mod numeral k = 1" if "numeral k \<noteq> (1::nat)"
+  by (rule Suc_times_mod_eq) (use that in simp)
+
+lemma Suc_div_le_mono [simp]:
+  "m div n \<le> Suc m div n"
+  by (simp add: div_le_mono)
+
+text \<open>These lemmas collapse some needless occurrences of Suc:
+  at least three Sucs, since two and fewer are rewritten back to Suc again!
+  We already have some rules to simplify operands smaller than 3.\<close>
+
+lemma div_Suc_eq_div_add3 [simp]:
+  "m div Suc (Suc (Suc n)) = m div (3 + n)"
+  by (simp add: Suc3_eq_add_3)
+
+lemma mod_Suc_eq_mod_add3 [simp]:
+  "m mod Suc (Suc (Suc n)) = m mod (3 + n)"
+  by (simp add: Suc3_eq_add_3)
+
+lemma Suc_div_eq_add3_div:
+  "Suc (Suc (Suc m)) div n = (3 + m) div n"
+  by (simp add: Suc3_eq_add_3)
+
+lemma Suc_mod_eq_add3_mod:
+  "Suc (Suc (Suc m)) mod n = (3 + m) mod n"
+  by (simp add: Suc3_eq_add_3)
+
+lemmas Suc_div_eq_add3_div_numeral [simp] =
+  Suc_div_eq_add3_div [of _ "numeral v"] for v
+
+lemmas Suc_mod_eq_add3_mod_numeral [simp] =
+  Suc_mod_eq_add3_mod [of _ "numeral v"] for v
+
+lemma (in field_char_0) of_nat_div:
+  "of_nat (m div n) = ((of_nat m - of_nat (m mod n)) / of_nat n)"
+proof -
+  have "of_nat (m div n) = ((of_nat (m div n * n + m mod n) - of_nat (m mod n)) / of_nat n :: 'a)"
+    unfolding of_nat_add by (cases "n = 0") simp_all
+  then show ?thesis
+    by simp
+qed
+
+text \<open>An ``induction'' law for modulus arithmetic.\<close>
+
+lemma mod_induct [consumes 3, case_names step]:
+  "P m" if "P n" and "n < p" and "m < p"
+    and step: "\<And>n. n < p \<Longrightarrow> P n \<Longrightarrow> P (Suc n mod p)"
+using \<open>m < p\<close> proof (induct m)
+  case 0
+  show ?case
+  proof (rule ccontr)
+    assume "\<not> P 0"
+    from \<open>n < p\<close> have "0 < p"
+      by simp
+    from \<open>n < p\<close> obtain m where "0 < m" and "p = n + m"
+      by (blast dest: less_imp_add_positive)
+    with \<open>P n\<close> have "P (p - m)"
+      by simp
+    moreover have "\<not> P (p - m)"
+    using \<open>0 < m\<close> proof (induct m)
+      case 0
+      then show ?case
+        by simp
+    next
+      case (Suc m)
+      show ?case
+      proof
+        assume P: "P (p - Suc m)"
+        with \<open>\<not> P 0\<close> have "Suc m < p"
+          by (auto intro: ccontr) 
+        then have "Suc (p - Suc m) = p - m"
+          by arith
+        moreover from \<open>0 < p\<close> have "p - Suc m < p"
+          by arith
+        with P step have "P ((Suc (p - Suc m)) mod p)"
+          by blast
+        ultimately show False
+          using \<open>\<not> P 0\<close> Suc.hyps by (cases "m = 0") simp_all
+      qed
+    qed
+    ultimately show False
+      by blast
+  qed
+next
+  case (Suc m)
+  then have "m < p" and mod: "Suc m mod p = Suc m"
+    by simp_all
+  from \<open>m < p\<close> have "P m"
+    by (rule Suc.hyps)
+  with \<open>m < p\<close> have "P (Suc m mod p)"
+    by (rule step)
+  with mod show ?case
+    by simp
+qed
+
+lemma split_div:
+  "P (m div n) \<longleftrightarrow> (n = 0 \<longrightarrow> P 0) \<and> (n \<noteq> 0 \<longrightarrow>
+     (\<forall>i j. j < n \<longrightarrow> m = n * i + j \<longrightarrow> P i))"
+     (is "?P = ?Q") for m n :: nat
+proof (cases "n = 0")
+  case True
+  then show ?thesis
+    by simp
+next
+  case False
+  show ?thesis
+  proof
+    assume ?P
+    with False show ?Q
+      by auto
+  next
+    assume ?Q
+    with False have *: "\<And>i j. j < n \<Longrightarrow> m = n * i + j \<Longrightarrow> P i"
+      by simp
+    with False show ?P
+      by (auto intro: * [of "m mod n"])
+  qed
+qed
+
+lemma split_div':
+  "P (m div n) \<longleftrightarrow> n = 0 \<and> P 0 \<or> (\<exists>q. (n * q \<le> m \<and> m < n * Suc q) \<and> P q)"
+proof (cases "n = 0")
+  case True
+  then show ?thesis
+    by simp
+next
+  case False
+  then have "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> m div n = q" for q
+    by (auto intro: div_nat_eqI dividend_less_times_div)
+  then show ?thesis
+    by auto
+qed
+
+lemma split_mod:
+  "P (m mod n) \<longleftrightarrow> (n = 0 \<longrightarrow> P m) \<and> (n \<noteq> 0 \<longrightarrow>
+     (\<forall>i j. j < n \<longrightarrow> m = n * i + j \<longrightarrow> P j))"
+     (is "?P \<longleftrightarrow> ?Q") for m n :: nat
+proof (cases "n = 0")
+  case True
+  then show ?thesis
+    by simp
+next
+  case False
+  show ?thesis
+  proof
+    assume ?P
+    with False show ?Q
+      by auto
+  next
+    assume ?Q
+    with False have *: "\<And>i j. j < n \<Longrightarrow> m = n * i + j \<Longrightarrow> P j"
+      by simp
+    with False show ?P
+      by (auto intro: * [of _ "m div n"])
+  qed
+qed
+
+
+subsection \<open>Code generation\<close>
+
+code_identifier
+  code_module Euclidean_Division \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
+
+end
diff -r c3631f32dfeb -r 1907167b6038 src/HOL/Library/Code_Target_Nat.thy
--- a/src/HOL/Library/Code_Target_Nat.thy	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Library/Code_Target_Nat.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -95,7 +95,7 @@
 
 lemma [code]:
   "Divides.divmod_nat m n = (m div n, m mod n)"
-  by (fact divmod_nat_div_mod)
+  by (fact divmod_nat_def)
 
 lemma [code]:
   "divmod m n = map_prod nat_of_integer nat_of_integer (divmod m n)"
@@ -130,7 +130,7 @@
 proof -
   from div_mult_mod_eq have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp
   show ?thesis
-    by (simp add: Let_def divmod_nat_div_mod of_nat_add [symmetric])
+    by (simp add: Let_def divmod_nat_def of_nat_add [symmetric])
       (simp add: * mult.commute of_nat_mult add.commute)
 qed
 
diff -r c3631f32dfeb -r 1907167b6038 src/HOL/Library/RBT_Impl.thy
--- a/src/HOL/Library/RBT_Impl.thy	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Library/RBT_Impl.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -1169,7 +1169,7 @@
           apfst (Branch B t1 k v) (rbtreeify_g n' kvs')
       else case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
           apfst (Branch B t1 k v) (rbtreeify_f n' kvs'))"
-by (subst rbtreeify_f.simps) (simp only: Let_def divmod_nat_div_mod prod.case)
+by (subst rbtreeify_f.simps) (simp only: Let_def divmod_nat_def prod.case)
 
 lemma rbtreeify_g_code [code]:
   "rbtreeify_g n kvs =
@@ -1180,7 +1180,7 @@
           apfst (Branch B t1 k v) (rbtreeify_g n' kvs')
       else case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
           apfst (Branch B t1 k v) (rbtreeify_g n' kvs'))"
-by(subst rbtreeify_g.simps)(simp only: Let_def divmod_nat_div_mod prod.case)
+by(subst rbtreeify_g.simps)(simp only: Let_def divmod_nat_def prod.case)
 
 lemma Suc_double_half: "Suc (2 * n) div 2 = n"
 by simp
diff -r c3631f32dfeb -r 1907167b6038 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Parity.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -101,6 +101,92 @@
 
 end
 
+class unique_euclidean_semiring_parity = unique_euclidean_semiring +
+  assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
+  assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1"
+  assumes zero_not_eq_two: "0 \<noteq> 2"
+begin
+
+lemma parity_cases [case_names even odd]:
+  assumes "a mod 2 = 0 \<Longrightarrow> P"
+  assumes "a mod 2 = 1 \<Longrightarrow> P"
+  shows P
+  using assms parity by blast
+
+lemma one_div_two_eq_zero [simp]:
+  "1 div 2 = 0"
+proof (cases "2 = 0")
+  case True then show ?thesis by simp
+next
+  case False
+  from div_mult_mod_eq have "1 div 2 * 2 + 1 mod 2 = 1" .
+  with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp
+  then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq del: mult_eq_0_iff)
+  then have "1 div 2 = 0 \<or> 2 = 0" by simp
+  with False show ?thesis by auto
+qed
+
+lemma not_mod_2_eq_0_eq_1 [simp]:
+  "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
+  by (cases a rule: parity_cases) simp_all
+
+lemma not_mod_2_eq_1_eq_0 [simp]:
+  "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
+  by (cases a rule: parity_cases) simp_all
+
+subclass semiring_parity
+proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1)
+  show "1 mod 2 = 1"
+    by (fact one_mod_two_eq_one)
+next
+  fix a b
+  assume "a mod 2 = 1"
+  moreover assume "b mod 2 = 1"
+  ultimately show "(a + b) mod 2 = 0"
+    using mod_add_eq [of a 2 b] by simp
+next
+  fix a b
+  assume "(a * b) mod 2 = 0"
+  then have "(a mod 2) * (b mod 2) mod 2 = 0"
+    by (simp add: mod_mult_eq)
+  then have "(a mod 2) * (b mod 2) = 0"
+    by (cases "a mod 2 = 0") simp_all
+  then show "a mod 2 = 0 \<or> b mod 2 = 0"
+    by (rule divisors_zero)
+next
+  fix a
+  assume "a mod 2 = 1"
+  then have "a = a div 2 * 2 + 1"
+    using div_mult_mod_eq [of a 2] by simp
+  then show "\<exists>b. a = b + 1" ..
+qed
+
+lemma even_iff_mod_2_eq_zero:
+  "even a \<longleftrightarrow> a mod 2 = 0"
+  by (fact dvd_eq_mod_eq_0)
+
+lemma odd_iff_mod_2_eq_one:
+  "odd a \<longleftrightarrow> a mod 2 = 1"
+  by (simp add: even_iff_mod_2_eq_zero)
+
+lemma even_succ_div_two [simp]:
+  "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
+  by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
+
+lemma odd_succ_div_two [simp]:
+  "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
+  by (auto elim!: oddE simp add: zero_not_eq_two [symmetric] add.assoc)
+
+lemma even_two_times_div_two:
+  "even a \<Longrightarrow> 2 * (a div 2) = a"
+  by (fact dvd_mult_div_cancel)
+
+lemma odd_two_times_div_two_succ [simp]:
+  "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
+  using mult_div_mod_eq [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
+ 
+end
+
 
 subsection \<open>Instances for @{typ nat} and @{typ int}\<close>
 
@@ -190,9 +276,6 @@
   for k l :: int
   using even_abs_add_iff [of l k] by (simp add: ac_simps)
 
-lemma odd_Suc_minus_one [simp]: "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
-  by (auto elim: oddE)
-
 instance int :: ring_parity
 proof
   show "\<not> 2 dvd (1 :: int)"
diff -r c3631f32dfeb -r 1907167b6038 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Rings.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -1620,6 +1620,10 @@
   shows "c dvd a"
   using assms dvd_mod_iff [of c b a] by simp
 
+lemma dvd_minus_mod [simp]:
+  "b dvd a - a mod b"
+  by (simp add: minus_mod_eq_div_mult)
+
 end
 
 class idom_modulo = idom + semidom_modulo
diff -r c3631f32dfeb -r 1907167b6038 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Word/Word.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -2024,7 +2024,7 @@
 
 lemmas le_unat_uoi = unat_le [THEN word_unat.Abs_inverse]
 
-lemmas thd = refl [THEN [2] split_div_lemma [THEN iffD2], THEN conjunct1]
+lemmas thd = times_div_less_eq_dividend
 
 lemmas uno_simps [THEN le_unat_uoi] = mod_le_divisor div_le_dividend dtle
 
@@ -3724,7 +3724,7 @@
 lemmas length_word_rsplit_exp_size' = refl [THEN length_word_rsplit_exp_size]
 
 (* alternative proof of word_rcat_rsplit *)
-lemmas tdle = iffD2 [OF split_div_lemma refl, THEN conjunct1]
+lemmas tdle = times_div_less_eq_dividend
 lemmas dtle = xtr4 [OF tdle mult.commute]
 
 lemma word_rcat_rsplit: "word_rcat (word_rsplit w) = w"
@@ -3734,7 +3734,7 @@
     apply (simp_all add: word_size
       refl [THEN length_word_rsplit_size [simplified not_less [symmetric], simplified]])
    apply safe
-   apply (erule xtr7, rule len_gt_0 [THEN dtle])+
+   apply (erule xtr7, rule dtle)+
   done
 
 lemma size_word_rsplit_rcat_size:
diff -r c3631f32dfeb -r 1907167b6038 src/HOL/Word/Word_Miscellaneous.thy
--- a/src/HOL/Word/Word_Miscellaneous.thy	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Word/Word_Miscellaneous.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -304,8 +304,8 @@
 lemmas pl_pl_mm' = add.commute [THEN [2] trans, THEN pl_pl_mm]
 
 lemmas dme = div_mult_mod_eq
-lemmas dtle = xtr3 [OF dme [symmetric] le_add1]
-lemmas th2 = order_trans [OF order_refl [THEN [2] mult_le_mono] dtle]
+lemmas dtle = div_times_less_eq_dividend
+lemmas th2 = order_trans [OF order_refl [THEN [2] mult_le_mono] div_times_less_eq_dividend]
 
 lemma td_gal: "0 < c \<Longrightarrow> a \<ge> b * c \<longleftrightarrow> a div c \<ge> b"
   for a b c :: nat
@@ -316,15 +316,13 @@
 
 lemmas td_gal_lt = td_gal [simplified not_less [symmetric], simplified]
 
-lemma div_mult_le: "a div b * b \<le> a"
-  for a b :: nat
-  by (fact dtle)
+lemmas div_mult_le = div_times_less_eq_dividend 
 
-lemmas sdl = split_div_lemma [THEN iffD1, symmetric]
+lemmas sdl = div_nat_eqI
 
 lemma given_quot: "f > 0 \<Longrightarrow> (f * l + (f - 1)) div f = l"
   for f l :: nat
-  by (rule sdl, assumption) (simp (no_asm))
+  by (rule div_nat_eqI) (simp_all)
 
 lemma given_quot_alt: "f > 0 \<Longrightarrow> (l * f + f - Suc 0) div f = l"
   for f l :: nat