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