# HG changeset patch
# User haftmann
# Date 1507494502 -7200
# Node ID 212a3334e7da8d1380fd9b0f8e0c00aa5b3e7416
# Parent  93c6632ddf44976fdb594ee28b2a38b6cfe3f8bd
more fundamental definition of div and mod on int

diff -r 93c6632ddf44 -r 212a3334e7da src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Divides.thy	Sun Oct 08 22:28:22 2017 +0200
@@ -326,12 +326,6 @@
   "m mod n = snd (divmod_nat m n)"
   by simp_all
 
-
-subsection \<open>Division on @{typ int}\<close>
-
-context
-begin
-
 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)"
@@ -377,31 +371,6 @@
 apply (blast intro: unique_quotient)
 done
 
-end
-
-instantiation int :: "{idom_modulo, normalization_semidom}"
-begin
-
-definition normalize_int :: "int \<Rightarrow> int"
-  where [simp]: "normalize = (abs :: int \<Rightarrow> int)"
-
-definition unit_factor_int :: "int \<Rightarrow> int"
-  where [simp]: "unit_factor = (sgn :: int \<Rightarrow> int)"
-
-definition divide_int :: "int \<Rightarrow> int \<Rightarrow> int"
-  where "k div l = (if l = 0 \<or> k = 0 then 0
-    else if k > 0 \<and> l > 0 \<or> k < 0 \<and> l < 0
-      then int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
-      else
-        if l dvd k then - int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
-        else - int (Suc (nat \<bar>k\<bar> div nat \<bar>l\<bar>)))"
-
-definition modulo_int :: "int \<Rightarrow> int \<Rightarrow> int"
-  where "k mod l = (if l = 0 then k else if l dvd k then 0
-    else if k > 0 \<and> l > 0 \<or> k < 0 \<and> l < 0
-      then sgn l * int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)
-      else sgn l * (\<bar>l\<bar> - int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)))"
-
 lemma eucl_rel_int:
   "eucl_rel_int k l (k div l, k mod l)"
 proof (cases k rule: int_cases3)
@@ -433,42 +402,21 @@
   using unique_quotient [of k l] unique_remainder [of k l]
   by auto
 
-instance proof
-  fix k l :: int
-  show "k div l * l + k mod l = k"
-    using eucl_rel_int [of k l]
-    unfolding eucl_rel_int_iff by (simp add: ac_simps)
-next
-  fix k :: int show "k div 0 = 0"
-    by (rule div_int_unique, simp add: eucl_rel_int_iff)
-next
-  fix k l :: int
-  assume "l \<noteq> 0"
-  then show "k * l div l = k"
-    by (auto simp add: eucl_rel_int_iff ac_simps intro: div_int_unique [of _ _ _ 0])
-qed (auto simp add: sgn_mult mult_sgn_abs abs_eq_iff')
-
-end
-
-lemma is_unit_int:
-  "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
-  by auto
-
-lemma zdiv_int:
-  "int (a div b) = int a div int b"
-  by (simp add: divide_int_def)
-
-lemma zmod_int:
-  "int (a mod b) = int a mod int b"
-  by (simp add: modulo_int_def int_dvd_iff)
-
 lemma div_abs_eq_div_nat:
   "\<bar>k\<bar> div \<bar>l\<bar> = int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)"
   by (simp add: divide_int_def)
 
 lemma mod_abs_eq_div_nat:
   "\<bar>k\<bar> mod \<bar>l\<bar> = int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)"
-  by (simp add: modulo_int_def dvd_int_unfold_dvd_nat)
+  by (simp add: modulo_int_def)
+
+lemma zdiv_int:
+  "int (a div b) = int a div int b"
+  by (simp add: divide_int_def sgn_1_pos)
+
+lemma zmod_int:
+  "int (a mod b) = int a mod int b"
+  by (simp add: modulo_int_def sgn_1_pos)
 
 lemma div_sgn_abs_cancel:
   fixes k l v :: int
@@ -493,7 +441,7 @@
 next
   case False
   with assms have "(sgn k * \<bar>k\<bar>) div (sgn l * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>"
-    by (simp add: div_sgn_abs_cancel)
+    using div_sgn_abs_cancel [of l k l] by simp
   then show ?thesis
     by (simp add: sgn_mult_abs)
 qed
@@ -502,12 +450,14 @@
   fixes k l :: int
   assumes "l dvd k"
   shows "k div l = (sgn k * sgn l) * (\<bar>k\<bar> div \<bar>l\<bar>)"
-proof (cases "k = 0")
+proof (cases "k = 0 \<or> l = 0")
   case True
   then show ?thesis
-    by simp
+    by auto
 next
   case False
+  then have "k \<noteq> 0" and "l \<noteq> 0"
+    by auto
   show ?thesis
   proof (cases "sgn l = sgn k")
     case True
@@ -515,9 +465,12 @@
       by (simp add: div_eq_sgn_abs)
   next
     case False
-    with \<open>k \<noteq> 0\<close> assms show ?thesis
+    with \<open>k \<noteq> 0\<close> \<open>l \<noteq> 0\<close>
+    have "sgn l * sgn k = - 1"
+      by (simp add: sgn_if split: if_splits)
+    with assms show ?thesis
       unfolding divide_int_def [of k l]
-        by (auto simp add: zdiv_int)
+      by (auto simp add: zdiv_int ac_simps)
   qed
 qed
 
@@ -529,59 +482,14 @@
   using assms
   by (simp only: divide_int_def [of k l], auto simp add: not_less zdiv_int)
   
-lemma sgn_mod:
-  fixes k l :: int
-  assumes "l \<noteq> 0" "\<not> l dvd k"
-  shows "sgn (k mod l) = sgn l"
-proof -
-  from \<open>\<not> l dvd k\<close>
-  have "k mod l \<noteq> 0"
-    by (simp add: dvd_eq_mod_eq_0)
-  show ?thesis
-    using \<open>l \<noteq> 0\<close> \<open>\<not> l dvd k\<close>
-    unfolding modulo_int_def [of k l]
-    by (auto simp add: sgn_1_pos sgn_1_neg mod_greater_zero_iff_not_dvd nat_dvd_iff not_less
-      zless_nat_eq_int_zless [symmetric] elim: nonpos_int_cases)
-qed
-
-lemma abs_mod_less:
-  fixes k l :: int
-  assumes "l \<noteq> 0"
-  shows "\<bar>k mod l\<bar> < \<bar>l\<bar>"
-  using assms unfolding modulo_int_def [of k l]
-  by (auto simp add: not_less int_dvd_iff mod_greater_zero_iff_not_dvd elim: pos_int_cases neg_int_cases nonneg_int_cases nonpos_int_cases)
-
-instantiation int :: unique_euclidean_ring
-begin
-
-definition [simp]:
-  "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
-
-definition [simp]:
-  "uniqueness_constraint_int (k :: int) l \<longleftrightarrow> unit_factor k = unit_factor l"
-  
-instance proof
-  fix l q r:: int
-  assume "uniqueness_constraint r l"
-    and "euclidean_size r < euclidean_size l"
-  then have "sgn r = sgn l" and "\<bar>r\<bar> < \<bar>l\<bar>"
-    by simp_all
-  then have "eucl_rel_int (q * l + r) l (q, r)"
-    by (rule eucl_rel_int_remainderI) simp
-  then show "(q * l + r) div l = q"
-    by (rule div_int_unique)
-qed (use mult_le_mono2 [of 1] in \<open>auto simp add: abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib\<close>)
-
-end
-
 text\<open>Basic laws about division and remainder\<close>
 
 lemma pos_mod_conj: "(0::int) < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b"
   using eucl_rel_int [of a b]
   by (auto simp add: eucl_rel_int_iff prod_eq_iff)
 
-lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1]
-   and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2]
+lemmas pos_mod_sign = pos_mod_conj [THEN conjunct1]
+   and pos_mod_bound = pos_mod_conj [THEN conjunct2]
 
 lemma neg_mod_conj: "b < (0::int) \<Longrightarrow> a mod b \<le> 0 \<and> b < a mod b"
   using eucl_rel_int [of a b]
@@ -631,39 +539,6 @@
 
 text\<open>There is no \<open>mod_neg_pos_trivial\<close>.\<close>
 
-instance int :: ring_parity
-proof
-  fix k l :: int
-  show "k mod 2 = 1" if "\<not> 2 dvd k"
-  proof (rule order_antisym)
-    have "0 \<le> k mod 2" and "k mod 2 < 2"
-      by auto
-    moreover have "k mod 2 \<noteq> 0"
-      using that by (simp add: dvd_eq_mod_eq_0)
-    ultimately have "0 < k mod 2"
-      by (simp only: less_le) simp
-    then show "1 \<le> k mod 2"
-      by simp
-    from \<open>k mod 2 < 2\<close> show "k mod 2 \<le> 1"
-      by (simp only: less_le) simp
-  qed
-qed (simp_all add: dvd_eq_mod_eq_0 divide_int_def)
-
-lemma even_diff_iff [simp]:
-  "even (k - l) \<longleftrightarrow> even (k + l)" for k l :: int
-  using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
-
-lemma even_abs_add_iff [simp]:
-  "even (\<bar>k\<bar> + l) \<longleftrightarrow> even (k + l)" for k l :: int
-  by (cases "k \<ge> 0") (simp_all add: ac_simps)
-
-lemma even_add_abs_iff [simp]:
-  "even (k + \<bar>l\<bar>) \<longleftrightarrow> even (k + l)" for k l :: int
-  using even_abs_add_iff [of l k] by (simp add: ac_simps)
-
-lemma even_nat_iff: "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
-  by (simp add: even_of_nat [of "nat k", where ?'a = int, symmetric])
-
 
 subsubsection \<open>Laws for div and mod with Unary Minus\<close>
 
@@ -697,14 +572,14 @@
   by (simp add: mod_eq_0_iff_dvd)
 
 lemma zdiv_zminus2_eq_if:
-     "b \<noteq> (0::int)
+  "b \<noteq> (0::int)
       ==> a div (-b) =
           (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
-by (simp add: zdiv_zminus1_eq_if div_minus_right)
+  by (auto simp add: zdiv_zminus1_eq_if div_minus_right)
 
 lemma zmod_zminus2_eq_if:
-     "a mod (-b::int) = (if a mod b = 0 then 0 else  (a mod b) - b)"
-by (simp add: zmod_zminus1_eq_if mod_minus_right)
+  "a mod (-b::int) = (if a mod b = 0 then 0 else  (a mod b) - b)"
+  by (auto simp add: zmod_zminus1_eq_if mod_minus_right)
 
 
 subsubsection \<open>Monotonicity in the First Argument (Dividend)\<close>
@@ -1161,11 +1036,17 @@
 
 lemma minus_numeral_mod_numeral [simp]:
   "- numeral m mod numeral n = adjust_mod (numeral n) (snd (divmod m n) :: int)"
-proof -
-  have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
-    using that by (simp only: snd_divmod modulo_int_def) auto
+proof (cases "snd (divmod m n) = (0::int)")
+  case True
   then show ?thesis
-    by (auto simp add: split_def Let_def adjust_div_def divides_aux_def modulo_int_def)
+    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]:
@@ -1179,11 +1060,17 @@
   
 lemma numeral_mod_minus_numeral [simp]:
   "numeral m mod - numeral n = - adjust_mod (numeral n) (snd (divmod m n) :: int)"
-proof -
-  have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
-    using that by (simp only: snd_divmod modulo_int_def) auto
+proof (cases "snd (divmod m n) = (0::int)")
+  case True
   then show ?thesis
-    by (auto simp add: split_def Let_def adjust_div_def divides_aux_def modulo_int_def)
+    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]:
@@ -1461,6 +1348,10 @@
 lemma even_int_iff [simp]: "even (int n) \<longleftrightarrow> even n"
   by (fact even_of_nat)
 
+lemma is_unit_int:
+  "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
+  by auto
+
 text \<open>Tool setup\<close>
 
 declare transfer_morphism_int_nat [transfer add return: even_int_iff]
diff -r 93c6632ddf44 -r 212a3334e7da src/HOL/Euclidean_Division.thy
--- a/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:22 2017 +0200
@@ -704,7 +704,7 @@
 
 subsection \<open>Euclidean division on @{typ nat}\<close>
 
-instantiation nat :: unique_euclidean_semiring
+instantiation nat :: normalization_semidom
 begin
 
 definition normalize_nat :: "nat \<Rightarrow> nat"
@@ -718,15 +718,23 @@
   "unit_factor (Suc n) = 1"
   by (simp_all add: unit_factor_nat_def)
 
+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})"
+
+instance
+  by standard (auto simp add: divide_nat_def ac_simps unit_factor_nat_def intro: Max_eqI)
+
+end
+
+instantiation nat :: unique_euclidean_semiring
+begin
+
 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))"
 
@@ -757,15 +765,11 @@
     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"
@@ -805,7 +809,7 @@
     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)
+qed simp_all
 
 end
 
@@ -1329,6 +1333,186 @@
 qed
 
 
+subsection \<open>Euclidean division on @{typ int}\<close>
+
+instantiation int :: normalization_semidom
+begin
+
+definition normalize_int :: "int \<Rightarrow> int"
+  where [simp]: "normalize = (abs :: int \<Rightarrow> int)"
+
+definition unit_factor_int :: "int \<Rightarrow> int"
+  where [simp]: "unit_factor = (sgn :: int \<Rightarrow> int)"
+
+definition divide_int :: "int \<Rightarrow> int \<Rightarrow> int"
+  where "k div l = (if l = 0 then 0
+    else if sgn k = sgn l
+      then int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
+      else - int (nat \<bar>k\<bar> div nat \<bar>l\<bar> + of_bool (\<not> l dvd k)))"
+
+lemma divide_int_unfold:
+  "(sgn k * int m) div (sgn l * int n) =
+   (if sgn l = 0 \<or> sgn k = 0 \<or> n = 0 then 0
+    else if sgn k = sgn l
+      then int (m div n)
+      else - int (m div n + of_bool (\<not> n dvd m)))"
+  by (auto simp add: divide_int_def sgn_0_0 sgn_1_pos sgn_mult abs_mult
+    nat_mult_distrib dvd_int_iff)
+
+instance proof
+  fix k :: int show "k div 0 = 0"
+  by (simp add: divide_int_def)
+next
+  fix k l :: int
+  assume "l \<noteq> 0"
+  obtain n m and s t where k: "k = sgn s * int n" and l: "l = sgn t * int m" 
+    by (blast intro: int_sgnE elim: that)
+  then have "k * l = sgn (s * t) * int (n * m)"
+    by (simp add: ac_simps sgn_mult)
+  with k l \<open>l \<noteq> 0\<close> show "k * l div l = k"
+    by (simp only: divide_int_unfold)
+      (auto simp add: algebra_simps sgn_mult sgn_1_pos sgn_0_0)
+qed (auto simp add: sgn_mult mult_sgn_abs abs_eq_iff')
+
+end
+
+instantiation int :: unique_euclidean_ring
+begin
+
+definition euclidean_size_int :: "int \<Rightarrow> nat"
+  where [simp]: "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
+
+definition uniqueness_constraint_int :: "int \<Rightarrow> int \<Rightarrow> bool"
+  where [simp]: "uniqueness_constraint_int k l \<longleftrightarrow> unit_factor k = unit_factor l"
+
+definition modulo_int :: "int \<Rightarrow> int \<Rightarrow> int"
+  where "k mod l = (if l = 0 then k
+    else if sgn k = sgn l
+      then sgn l * int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)
+      else sgn l * (\<bar>l\<bar> * of_bool (\<not> l dvd k) - int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)))"
+
+lemma modulo_int_unfold:
+  "(sgn k * int m) mod (sgn l * int n) =
+   (if sgn l = 0 \<or> sgn k = 0 \<or> n = 0 then sgn k * int m
+    else if sgn k = sgn l
+      then sgn l * int (m mod n)
+      else sgn l * (int (n * of_bool (\<not> n dvd m)) - int (m mod n)))"
+  by (auto simp add: modulo_int_def sgn_0_0 sgn_1_pos sgn_mult abs_mult
+    nat_mult_distrib dvd_int_iff)
+
+lemma abs_mod_less:
+  "\<bar>k mod l\<bar> < \<bar>l\<bar>" if "l \<noteq> 0" for k l :: int
+proof -
+  obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m" 
+    by (blast intro: int_sgnE elim: that)
+  with that show ?thesis
+    by (simp add: modulo_int_unfold sgn_0_0 sgn_1_pos sgn_1_neg
+      abs_mult mod_greater_zero_iff_not_dvd)
+qed
+
+lemma sgn_mod:
+  "sgn (k mod l) = sgn l" if "l \<noteq> 0" "\<not> l dvd k" for k l :: int
+proof -
+  obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m" 
+    by (blast intro: int_sgnE elim: that)
+  with that show ?thesis
+    by (simp add: modulo_int_unfold sgn_0_0 sgn_1_pos sgn_1_neg
+      sgn_mult mod_eq_0_iff_dvd int_dvd_iff)
+qed
+
+instance proof
+  fix k l :: int
+  obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m" 
+    by (blast intro: int_sgnE elim: that)
+  then show "k div l * l + k mod l = k"
+    by (auto simp add: divide_int_unfold modulo_int_unfold algebra_simps dest!: sgn_not_eq_imp)
+       (simp_all add: of_nat_mult [symmetric] of_nat_add [symmetric]
+         distrib_left [symmetric] minus_mult_right
+         del: of_nat_mult minus_mult_right [symmetric])
+next
+  fix l q r :: int
+  obtain n m and s t
+     where l: "l = sgn s * int n" and q: "q = sgn t * int m"
+    by (blast intro: int_sgnE elim: that)
+  assume \<open>l \<noteq> 0\<close>
+  with l have "s \<noteq> 0" and "n > 0"
+    by (simp_all add: sgn_0_0)
+  assume "uniqueness_constraint r l"
+  moreover have "r = sgn r * \<bar>r\<bar>"
+    by (simp add: sgn_mult_abs)
+  moreover define u where "u = nat \<bar>r\<bar>"
+  ultimately have "r = sgn l * int u"
+    by simp
+  with l \<open>n > 0\<close> have r: "r = sgn s * int u"
+    by (simp add: sgn_mult)
+  assume "euclidean_size r < euclidean_size l"
+  with l r \<open>s \<noteq> 0\<close> have "u < n"
+    by (simp add: abs_mult)
+  show "(q * l + r) div l = q"
+  proof (cases "q = 0 \<or> r = 0")
+    case True
+    then show ?thesis
+    proof
+      assume "q = 0"
+      then show ?thesis
+        using l r \<open>u < n\<close> by (simp add: divide_int_unfold)
+    next
+      assume "r = 0"
+      from \<open>r = 0\<close> have *: "q * l + r = sgn (t * s) * int (n * m)"
+        using q l by (simp add: ac_simps sgn_mult)
+      from \<open>s \<noteq> 0\<close> \<open>n > 0\<close> show ?thesis
+        by (simp only: *, simp only: q l divide_int_unfold)
+          (auto simp add: sgn_mult sgn_0_0 sgn_1_pos)
+    qed
+  next
+    case False
+    with q r have "t \<noteq> 0" and "m > 0" and "s \<noteq> 0" and "u > 0"
+      by (simp_all add: sgn_0_0)
+    moreover from \<open>0 < m\<close> \<open>u < n\<close> have "u \<le> m * n"
+      using mult_le_less_imp_less [of 1 m u n] by simp
+    ultimately have *: "q * l + r = sgn (s * t)
+      * int (if t < 0 then m * n - u else m * n + u)"
+      using l q r
+      by (simp add: sgn_mult algebra_simps of_nat_diff)
+    have "(m * n - u) div n = m - 1" if "u > 0"
+      using \<open>0 < m\<close> \<open>u < n\<close> that
+      by (auto intro: div_nat_eqI simp add: algebra_simps)
+    moreover have "n dvd m * n - u \<longleftrightarrow> n dvd u"
+      using \<open>u \<le> m * n\<close> dvd_diffD1 [of n "m * n" u]
+      by auto
+    ultimately show ?thesis
+      using \<open>s \<noteq> 0\<close> \<open>m > 0\<close> \<open>u > 0\<close> \<open>u < n\<close> \<open>u \<le> m * n\<close>
+      by (simp only: *, simp only: l q divide_int_unfold)
+        (auto simp add: sgn_mult sgn_0_0 sgn_1_pos algebra_simps dest: dvd_imp_le)
+  qed
+qed (use mult_le_mono2 [of 1] in \<open>auto simp add: abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib\<close>)
+
+end
+
+lemma pos_mod_bound [simp]:
+  "k mod l < l" if "l > 0" for k l :: int
+proof -
+  obtain m and s where "k = sgn s * int m"
+    by (blast intro: int_sgnE elim: that)
+  moreover from that obtain n where "l = sgn 1 * int n"
+    by (cases l) auto
+  ultimately show ?thesis
+    using that by (simp only: modulo_int_unfold)
+      (simp add: mod_greater_zero_iff_not_dvd)
+qed
+
+lemma pos_mod_sign [simp]:
+  "0 \<le> k mod l" if "l > 0" for k l :: int
+proof -
+  obtain m and s where "k = sgn s * int m"
+    by (blast intro: int_sgnE elim: that)
+  moreover from that obtain n where "l = sgn 1 * int n"
+    by (cases l) auto
+  ultimately show ?thesis
+    using that by (simp only: modulo_int_unfold) simp
+qed
+
+
 subsection \<open>Code generation\<close>
 
 code_identifier
diff -r 93c6632ddf44 -r 212a3334e7da src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/GCD.thy	Sun Oct 08 22:28:22 2017 +0200
@@ -2017,11 +2017,11 @@
 lemma gcd_non_0_int: "y > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
   for x y :: int
   apply (frule_tac b = y and a = x in pos_mod_sign)
-  apply (simp del: pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib)
+  apply (simp del: Euclidean_Division.pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib)
   apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric] zmod_zminus1_eq_if)
   apply (frule_tac a = x in pos_mod_bound)
   apply (subst (1 2) gcd.commute)
-  apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat nat_le_eq_zle)
+  apply (simp del: Euclidean_Division.pos_mod_bound add: nat_diff_distrib gcd_diff2_nat nat_le_eq_zle)
   done
 
 lemma gcd_red_int: "gcd x y = gcd y (x mod y)"
diff -r 93c6632ddf44 -r 212a3334e7da src/HOL/Int.thy
--- a/src/HOL/Int.thy	Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Int.thy	Sun Oct 08 22:28:22 2017 +0200
@@ -255,6 +255,10 @@
 lemma of_int_power [simp]: "of_int (z ^ n) = of_int z ^ n"
   by (induct n) simp_all
 
+lemma of_int_of_bool [simp]:
+  "of_int (of_bool P) = of_bool P"
+  by auto
+
 end
 
 context ring_char_0
@@ -548,6 +552,10 @@
 lemma diff_nat_numeral [simp]: "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')"
   by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)
 
+lemma nat_of_bool [simp]:
+  "nat (of_bool P) = of_bool P"
+  by auto
+
 
 text \<open>For termination proofs:\<close>
 lemma measure_function_int[measure_function]: "is_measure (nat \<circ> abs)" ..
@@ -668,6 +676,31 @@
   \<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close>
   by (fact Let_neg_numeral) \<comment> \<open>FIXME drop\<close>
 
+lemma sgn_mult_dvd_iff [simp]:
+  "sgn r * l dvd k \<longleftrightarrow> l dvd k \<and> (r = 0 \<longrightarrow> k = 0)" for k l r :: int
+  by (cases r rule: int_cases3) auto
+
+lemma mult_sgn_dvd_iff [simp]:
+  "l * sgn r dvd k \<longleftrightarrow> l dvd k \<and> (r = 0 \<longrightarrow> k = 0)" for k l r :: int
+  using sgn_mult_dvd_iff [of r l k] by (simp add: ac_simps)
+
+lemma dvd_sgn_mult_iff [simp]:
+  "l dvd sgn r * k \<longleftrightarrow> l dvd k \<or> r = 0" for k l r :: int
+  by (cases r rule: int_cases3) simp_all
+
+lemma dvd_mult_sgn_iff [simp]:
+  "l dvd k * sgn r \<longleftrightarrow> l dvd k \<or> r = 0" for k l r :: int
+  using dvd_sgn_mult_iff [of l r k] by (simp add: ac_simps)
+
+lemma int_sgnE:
+  fixes k :: int
+  obtains n and l where "k = sgn l * int n"
+proof -
+  have "k = sgn k * int (nat \<bar>k\<bar>)"
+    by (simp add: sgn_mult_abs)
+  then show ?thesis ..
+qed
+
 text \<open>Unfold \<open>min\<close> and \<open>max\<close> on numerals.\<close>
 
 lemmas max_number_of [simp] =
@@ -1629,19 +1662,10 @@
   shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)"
     (is "?lhs \<longleftrightarrow> ?rhs")
 proof -
-  from assms obtain k where "d = a * k" by (rule dvdE)
-  show ?thesis
-  proof
-    assume ?lhs
-    then obtain l where "x + t = a * l" by (rule dvdE)
-    then have "x = a * l - t" by simp
-    with \<open>d = a * k\<close> show ?rhs by simp
-  next
-    assume ?rhs
-    then obtain l where "x + c * d + t = a * l" by (rule dvdE)
-    then have "x = a * l - c * d - t" by simp
-    with \<open>d = a * k\<close> show ?lhs by simp
-  qed
+  from assms have "a dvd (x + t) \<longleftrightarrow> a dvd ((x + t) + c * d)"
+    by (simp add: dvd_add_left_iff)
+  then show ?thesis
+    by (simp add: ac_simps)
 qed
 
 
diff -r 93c6632ddf44 -r 212a3334e7da src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Nat.thy	Sun Oct 08 22:28:22 2017 +0200
@@ -1676,6 +1676,10 @@
     by (simp add: add.commute)
 qed
 
+lemma of_nat_of_bool [simp]:
+  "of_nat (of_bool P) = of_bool P"
+  by auto
+
 end
 
 declare of_nat_code [code]
@@ -1764,6 +1768,10 @@
 lemma abs_of_nat [simp]: "\<bar>of_nat n\<bar> = of_nat n"
   unfolding abs_if by auto
 
+lemma sgn_of_nat [simp]:
+  "sgn (of_nat n) = of_bool (n > 0)"
+  by simp
+
 end
 
 lemma of_nat_id [simp]: "of_nat n = n"
diff -r 93c6632ddf44 -r 212a3334e7da src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Parity.thy	Sun Oct 08 22:28:22 2017 +0200
@@ -483,4 +483,40 @@
 
 end
 
+
+subsection \<open>Instance for @{typ int}\<close>
+
+instance int :: ring_parity
+proof
+  fix k l :: int
+  show "k mod 2 = 1" if "\<not> 2 dvd k"
+  proof (rule order_antisym)
+    have "0 \<le> k mod 2" and "k mod 2 < 2"
+      by auto
+    moreover have "k mod 2 \<noteq> 0"
+      using that by (simp add: dvd_eq_mod_eq_0)
+    ultimately have "0 < k mod 2"
+      by (simp only: less_le) simp
+    then show "1 \<le> k mod 2"
+      by simp
+    from \<open>k mod 2 < 2\<close> show "k mod 2 \<le> 1"
+      by (simp only: less_le) simp
+  qed
+qed (simp_all add: dvd_eq_mod_eq_0 divide_int_def)
+
+lemma even_diff_iff [simp]:
+  "even (k - l) \<longleftrightarrow> even (k + l)" for k l :: int
+  using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
+
+lemma even_abs_add_iff [simp]:
+  "even (\<bar>k\<bar> + l) \<longleftrightarrow> even (k + l)" for k l :: int
+  by (cases "k \<ge> 0") (simp_all add: ac_simps)
+
+lemma even_add_abs_iff [simp]:
+  "even (k + \<bar>l\<bar>) \<longleftrightarrow> even (k + l)" for k l :: int
+  using even_abs_add_iff [of l k] by (simp add: ac_simps)
+
+lemma even_nat_iff: "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
+  by (simp add: even_of_nat [of "nat k", where ?'a = int, symmetric])
+
 end
diff -r 93c6632ddf44 -r 212a3334e7da src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Rings.thy	Sun Oct 08 22:28:22 2017 +0200
@@ -118,6 +118,13 @@
 end
 
 class semiring_1 = zero_neq_one + semiring_0 + monoid_mult
+begin
+
+lemma (in semiring_1) of_bool_conj:
+  "of_bool (P \<and> Q) = of_bool P * of_bool Q"
+  by auto
+
+end
 
 text \<open>Abstract divisibility\<close>
 
@@ -2319,6 +2326,10 @@
     by (auto simp add: abs_mult)
 qed
 
+lemma sgn_not_eq_imp:
+  "sgn a = - sgn b" if "sgn b \<noteq> sgn a" and "sgn a \<noteq> 0" and "sgn b \<noteq> 0"
+  using that by (cases "a < 0") (auto simp add: sgn_0_0 sgn_1_pos sgn_1_neg)
+
 lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k"
   by (simp add: abs_if)