# HG changeset patch
# User haftmann
# Date 1507494502 -7200
# Node ID 0b12755ccbb2c3e39e8b4eb6a1f4719a7ed1118b
# Parent  212a3334e7da8d1380fd9b0f8e0c00aa5b3e7416
euclidean rings need no normalization

diff -r 212a3334e7da -r 0b12755ccbb2 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Code_Numeral.thy	Sun Oct 08 22:28:22 2017 +0200
@@ -220,36 +220,15 @@
   "of_nat (nat_of_integer k) = max 0 k"
   by transfer auto
 
-instantiation integer :: normalization_semidom
+instantiation integer :: unique_euclidean_ring
 begin
 
-lift_definition normalize_integer :: "integer \<Rightarrow> integer"
-  is "normalize :: int \<Rightarrow> int"
-  .
-
-declare normalize_integer.rep_eq [simp]
-
-lift_definition unit_factor_integer :: "integer \<Rightarrow> integer"
-  is "unit_factor :: int \<Rightarrow> int"
-  .
-
-declare unit_factor_integer.rep_eq [simp]
-
 lift_definition divide_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
   is "divide :: int \<Rightarrow> int \<Rightarrow> int"
   .
 
 declare divide_integer.rep_eq [simp]
-  
-instance
-  by (standard; transfer)
-    (auto simp add: mult_sgn_abs sgn_mult abs_eq_iff')
 
-end
-
-instantiation integer :: unique_euclidean_ring
-begin
-  
 lift_definition modulo_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
   is "modulo :: int \<Rightarrow> int \<Rightarrow> int"
   .
@@ -279,7 +258,7 @@
   by (simp add: fun_eq_iff nat_of_integer.rep_eq)
 
 lemma [code]:
-  "uniqueness_constraint (k :: integer) l \<longleftrightarrow> unit_factor k = unit_factor l"
+  "uniqueness_constraint (k :: integer) l \<longleftrightarrow> sgn k = sgn l"
   by (simp add: integer_eq_iff)
 
 instance integer :: ring_parity
@@ -458,14 +437,6 @@
   "Neg m * Neg n = Pos (m * n)"
   by simp_all
 
-lemma normalize_integer_code [code]:
-  "normalize = (abs :: integer \<Rightarrow> integer)"
-  by transfer simp
-
-lemma unit_factor_integer_code [code]:
-  "unit_factor = (sgn :: integer \<Rightarrow> integer)"
-  by transfer simp
-
 definition divmod_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer \<times> integer"
 where
   "divmod_integer k l = (k div l, k mod l)"
@@ -880,18 +851,6 @@
 instantiation natural :: unique_euclidean_semiring
 begin
 
-lift_definition normalize_natural :: "natural \<Rightarrow> natural"
-  is "normalize :: nat \<Rightarrow> nat"
-  .
-
-declare normalize_natural.rep_eq [simp]
-
-lift_definition unit_factor_natural :: "natural \<Rightarrow> natural"
-  is "unit_factor :: nat \<Rightarrow> nat"
-  .
-
-declare unit_factor_natural.rep_eq [simp]
-
 lift_definition divide_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
   is "divide :: nat \<Rightarrow> nat \<Rightarrow> nat"
   .
@@ -1068,31 +1027,6 @@
   "integer_of_natural (m * n) = integer_of_natural m * integer_of_natural n"
   by transfer simp
 
-lemma [code]:
-  "normalize n = n" for n :: natural
-  by transfer simp
-
-lemma [code]:
-  "unit_factor n = of_bool (n \<noteq> 0)" for n :: natural
-proof (cases "n = 0")
-  case True
-  then show ?thesis
-    by simp
-next
-  case False
-  then have "unit_factor n = 1"
-  proof transfer
-    fix n :: nat
-    assume "n \<noteq> 0"
-    then obtain m where "n = Suc m"
-      by (cases n) auto
-    then show "unit_factor n = 1"
-      by simp
-  qed
-  with False show ?thesis
-    by simp
-qed
-
 lemma [code abstract]:
   "integer_of_natural (m div n) = integer_of_natural m div integer_of_natural n"
   by transfer (simp add: zdiv_int)
diff -r 212a3334e7da -r 0b12755ccbb2 src/HOL/Computational_Algebra/Euclidean_Algorithm.thy
--- a/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Sun Oct 08 22:28:22 2017 +0200
@@ -9,10 +9,26 @@
 begin
 
 subsection \<open>Generic construction of the (simple) euclidean algorithm\<close>
-  
-context euclidean_semiring
+
+class normalization_euclidean_semiring = euclidean_semiring + normalization_semidom
 begin
 
+lemma euclidean_size_normalize [simp]:
+  "euclidean_size (normalize a) = euclidean_size a"
+proof (cases "a = 0")
+  case True
+  then show ?thesis
+    by simp
+next
+  case [simp]: False
+  have "euclidean_size (normalize a) \<le> euclidean_size (normalize a * unit_factor a)"
+    by (rule size_mult_mono) simp
+  moreover have "euclidean_size a \<le> euclidean_size (a * (1 div unit_factor a))"
+    by (rule size_mult_mono) simp
+  ultimately show ?thesis
+    by simp
+qed
+
 context
 begin
 
@@ -282,7 +298,7 @@
   
 subsection \<open>The (simple) euclidean algorithm as gcd computation\<close>
   
-class euclidean_semiring_gcd = euclidean_semiring + gcd + Gcd +
+class euclidean_semiring_gcd = normalization_euclidean_semiring + gcd + Gcd +
   assumes gcd_eucl: "Euclidean_Algorithm.gcd = GCD.gcd"
     and lcm_eucl: "Euclidean_Algorithm.lcm = GCD.lcm"
   assumes Gcd_eucl: "Euclidean_Algorithm.Gcd = GCD.Gcd"
@@ -400,7 +416,7 @@
 end
 
 lemma factorial_euclidean_semiring_gcdI:
-  "OFCLASS('a::{factorial_semiring_gcd, euclidean_semiring}, euclidean_semiring_gcd_class)"
+  "OFCLASS('a::{factorial_semiring_gcd, normalization_euclidean_semiring}, euclidean_semiring_gcd_class)"
 proof
   interpret semiring_Gcd 1 0 times
     Euclidean_Algorithm.gcd Euclidean_Algorithm.lcm
@@ -502,7 +518,7 @@
         also have "r' - r' div r * r = r' mod r" using div_mult_mod_eq [of r' r]
           by (simp add: algebra_simps)
         finally show "(s' - r' div r * s) * a + (t' - r' div r * t) * b = r' mod r" .
-      qed (auto simp: gcd_mod_right algebra_simps minus_mod_eq_div_mult [symmetric] gcd.commute)
+      qed (auto simp: algebra_simps minus_mod_eq_div_mult [symmetric] gcd.commute)
       finally show ?thesis .
     qed
   qed
@@ -552,6 +568,8 @@
 
 subsection \<open>Typical instances\<close>
 
+instance nat :: normalization_euclidean_semiring ..
+
 instance nat :: euclidean_semiring_gcd
 proof
   interpret semiring_Gcd 1 0 times
@@ -584,6 +602,8 @@
     by (simp add: fun_eq_iff Euclidean_Algorithm.Gcd_def semiring_Gcd_class.Gcd_Lcm)
 qed
 
+instance int :: normalization_euclidean_semiring ..
+
 instance int :: euclidean_ring_gcd
 proof
   interpret semiring_Gcd 1 0 times
diff -r 212a3334e7da -r 0b12755ccbb2 src/HOL/Computational_Algebra/Field_as_Ring.thy
--- a/src/HOL/Computational_Algebra/Field_as_Ring.thy	Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Computational_Algebra/Field_as_Ring.thy	Sun Oct 08 22:28:22 2017 +0200
@@ -24,7 +24,7 @@
 
 end
 
-instantiation real :: unique_euclidean_ring
+instantiation real :: "{unique_euclidean_ring, normalization_euclidean_semiring}"
 begin
 
 definition [simp]: "normalize_real = (normalize_field :: real \<Rightarrow> _)"
@@ -55,7 +55,7 @@
 
 end
 
-instantiation rat :: unique_euclidean_ring
+instantiation rat :: "{unique_euclidean_ring, normalization_euclidean_semiring}"
 begin
 
 definition [simp]: "normalize_rat = (normalize_field :: rat \<Rightarrow> _)"
@@ -86,7 +86,7 @@
 
 end
 
-instantiation complex :: unique_euclidean_ring
+instantiation complex :: "{unique_euclidean_ring, normalization_euclidean_semiring}"
 begin
 
 definition [simp]: "normalize_complex = (normalize_field :: complex \<Rightarrow> _)"
diff -r 212a3334e7da -r 0b12755ccbb2 src/HOL/Computational_Algebra/Formal_Power_Series.thy
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Sun Oct 08 22:28:22 2017 +0200
@@ -1425,6 +1425,8 @@
 
 end
 
+instance fps :: (field) normalization_euclidean_semiring ..
+
 instantiation fps :: (field) euclidean_ring_gcd
 begin
 definition fps_gcd_def: "(gcd :: 'a fps \<Rightarrow> _) = Euclidean_Algorithm.gcd"
diff -r 212a3334e7da -r 0b12755ccbb2 src/HOL/Computational_Algebra/Polynomial_Factorial.thy
--- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Sun Oct 08 22:28:22 2017 +0200
@@ -416,14 +416,12 @@
 begin
 
 interpretation field_poly: 
-  unique_euclidean_ring where zero = "0 :: 'a :: field poly"
-    and one = 1 and plus = plus
-    and uminus = uminus and minus = minus
+  normalization_euclidean_semiring where zero = "0 :: 'a :: field poly"
+    and one = 1 and plus = plus and minus = minus
     and times = times
     and normalize = "\<lambda>p. smult (inverse (lead_coeff p)) p"
     and unit_factor = "\<lambda>p. [:lead_coeff p:]"
     and euclidean_size = "\<lambda>p. if p = 0 then 0 else 2 ^ degree p"
-    and uniqueness_constraint = top
     and divide = divide and modulo = modulo
   rewrites "dvd.dvd (times :: 'a poly \<Rightarrow> _) = Rings.dvd"
     and "comm_monoid_mult.prod_mset times 1 = prod_mset"
@@ -438,9 +436,9 @@
     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
-    (\<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"
+  show "class.normalization_euclidean_semiring divide plus minus (0 :: 'a poly) times 1
+    modulo (\<lambda>p. if p = 0 then 0 else 2 ^ degree p)
+    (\<lambda>p. [:lead_coeff p:]) (\<lambda>p. smult (inverse (lead_coeff p)) p)"
   proof (standard, fold dvd_dict)
     fix p :: "'a poly"
     show "[:lead_coeff p:] * smult (inverse (lead_coeff p)) p = p"
@@ -453,23 +451,6 @@
     fix p :: "'a poly" assume "p \<noteq> 0"
     then show "is_unit [:lead_coeff p:]"
       by (simp add: is_unit_pCons_iff)
-  next
-    fix p q s :: "'a poly" assume "s \<noteq> 0"
-    moreover assume "(if p = 0 then (0::nat) else 2 ^ degree p) < (if q = 0 then 0 else 2 ^ degree q)"
-    ultimately show "(if p * s = 0 then (0::nat) else 2 ^ degree (p * s)) < (if q * s = 0 then 0 else 2 ^ degree (q * s))"
-      by (auto simp add: degree_mult_eq)
-  next
-    fix p q r :: "'a poly"
-    assume "p \<noteq> 0"
-    with eucl_rel_poly [of r p] have "eucl_rel_poly (r + q * p) p (q + r div p, r mod p)"
-      by (simp add: eucl_rel_poly_iff distrib_right)
-    then have "(r + q * p) div p = q + r div p"
-      by (rule div_poly_eq)
-    moreover assume "(if r = 0 then (0::nat) else 2 ^ degree r)
-      < (if p = 0 then 0 else 2 ^ degree p)"
-    ultimately show "(q * p + r) div p = q"
-      using \<open>p \<noteq> 0\<close>
-      by (cases "r = 0") (simp_all add: div_poly_less ac_simps)
   qed (auto simp: lead_coeff_mult Rings.div_mult_mod_eq intro!: degree_mod_less' degree_mult_right_le)
 qed
 
@@ -758,7 +739,7 @@
 
 end
 
-instantiation poly :: ("{field,factorial_ring_gcd}") unique_euclidean_ring
+instantiation poly :: ("{field,factorial_ring_gcd}") "{unique_euclidean_ring, normalization_euclidean_semiring}"
 begin
 
 definition euclidean_size_poly :: "'a poly \<Rightarrow> nat"
@@ -783,9 +764,8 @@
 
 end
 
-instance poly :: ("{field,factorial_ring_gcd}") euclidean_ring_gcd
-  by (rule euclidean_ring_gcd_class.intro, rule factorial_euclidean_semiring_gcdI)
-    standard
+instance poly :: ("{field, normalization_euclidean_semiring, factorial_ring_gcd}") euclidean_ring_gcd
+  by (rule euclidean_ring_gcd_class.intro, rule factorial_euclidean_semiring_gcdI) standard
 
   
 subsection \<open>Polynomial GCD\<close>
diff -r 212a3334e7da -r 0b12755ccbb2 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
@@ -6,7 +6,7 @@
 section \<open>More on quotient and remainder\<close>
 
 theory Divides
-imports Parity Nat_Transfer
+imports Parity
 begin
 
 subsection \<open>Numeral division with a pragmatic type class\<close>
@@ -273,7 +273,7 @@
 hide_fact (open) div_less mod_less mod_less_eq_dividend mod_mult2_eq div_mult2_eq
 
 
-subsection \<open>Division on @{typ nat}\<close>
+subsection \<open>More on division\<close>
 
 instantiation nat :: unique_euclidean_semiring_numeral
 begin
@@ -1094,6 +1094,24 @@
 
 subsubsection \<open>Further properties\<close>
 
+lemma div_int_pos_iff:
+  "k div l \<ge> 0 \<longleftrightarrow> k = 0 \<or> l = 0 \<or> k \<ge> 0 \<and> l \<ge> 0
+    \<or> k < 0 \<and> l < 0"
+  for k l :: int
+  apply (cases "k = 0 \<or> l = 0")
+   apply (auto simp add: pos_imp_zdiv_nonneg_iff neg_imp_zdiv_nonneg_iff)
+  apply (rule ccontr)
+  apply (simp add: neg_imp_zdiv_nonneg_iff)
+  done
+
+lemma mod_int_pos_iff:
+  "k mod l \<ge> 0 \<longleftrightarrow> l dvd k \<or> l = 0 \<and> k \<ge> 0 \<or> l > 0"
+  for k l :: int
+  apply (cases "l > 0")
+   apply (simp_all add: dvd_eq_mod_eq_0)
+  apply (use neg_mod_conj [of l k] in \<open>auto simp add: le_less not_less\<close>)
+  done
+
 text \<open>Simplify expresions in which div and mod combine numerical constants\<close>
 
 lemma int_div_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a div b = q"
@@ -1139,42 +1157,6 @@
 apply (simp add: nat_eq_iff zmod_int)
 done
 
-text  \<open>transfer setup\<close>
-
-lemma transfer_nat_int_functions:
-    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
-    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
-  by (auto simp add: nat_div_distrib nat_mod_distrib)
-
-lemma transfer_nat_int_function_closures:
-    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
-    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
-  apply (cases "y = 0")
-  apply (auto simp add: pos_imp_zdiv_nonneg_iff)
-  apply (cases "y = 0")
-  apply auto
-done
-
-declare transfer_morphism_nat_int [transfer add return:
-  transfer_nat_int_functions
-  transfer_nat_int_function_closures
-]
-
-lemma transfer_int_nat_functions:
-    "(int x) div (int y) = int (x div y)"
-    "(int x) mod (int y) = int (x mod y)"
-  by (auto simp add: zdiv_int zmod_int)
-
-lemma transfer_int_nat_function_closures:
-    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
-    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
-  by (simp_all only: is_nat_def transfer_nat_int_function_closures)
-
-declare transfer_morphism_int_nat [transfer add return:
-  transfer_int_nat_functions
-  transfer_int_nat_function_closures
-]
-
 text\<open>Suggested by Matthias Daum\<close>
 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")
@@ -1352,8 +1334,4 @@
   "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]
-
 end
diff -r 212a3334e7da -r 0b12755ccbb2 src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Enum.thy	Sun Oct 08 22:28:22 2017 +0200
@@ -712,7 +712,7 @@
   "x dvd y \<longleftrightarrow> x = a\<^sub>2 \<or> y = a\<^sub>1"
   by (auto simp add: dvd_def times_finite_2_def split: finite_2.splits)
 
-instantiation finite_2 :: unique_euclidean_semiring begin
+instantiation finite_2 :: "{normalization_semidom, unique_euclidean_semiring}" begin
 definition [simp]: "normalize = (id :: finite_2 \<Rightarrow> _)"
 definition [simp]: "unit_factor = (id :: finite_2 \<Rightarrow> _)"
 definition [simp]: "euclidean_size x = (case x of a\<^sub>1 \<Rightarrow> 0 | a\<^sub>2 \<Rightarrow> 1)"
@@ -864,7 +864,7 @@
   "x dvd y \<longleftrightarrow> x = a\<^sub>2 \<or> x = a\<^sub>3 \<or> y = a\<^sub>1"
   by (cases x) (auto simp add: dvd_def times_finite_3_def split: finite_3.splits)
 
-instantiation finite_3 :: unique_euclidean_semiring begin
+instantiation finite_3 :: "{normalization_semidom, unique_euclidean_semiring}" begin
 definition [simp]: "normalize x = (case x of a\<^sub>3 \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> x)"
 definition [simp]: "unit_factor = (id :: finite_3 \<Rightarrow> _)"
 definition [simp]: "euclidean_size x = (case x of a\<^sub>1 \<Rightarrow> 0 | _ \<Rightarrow> 1)"
diff -r 212a3334e7da -r 0b12755ccbb2 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
@@ -3,15 +3,15 @@
     Author:     Florian Haftmann, TU Muenchen
 *)
 
-section \<open>Uniquely determined division in euclidean (semi)rings\<close>
+section \<open>Division in euclidean (semi)rings\<close>
 
 theory Euclidean_Division
-  imports Nat_Transfer Lattices_Big
+  imports Int Lattices_Big
 begin
 
 subsection \<open>Euclidean (semi)rings with explicit division and remainder\<close>
   
-class euclidean_semiring = semidom_modulo + normalization_semidom + 
+class euclidean_semiring = semidom_modulo + 
   fixes euclidean_size :: "'a \<Rightarrow> nat"
   assumes size_0 [simp]: "euclidean_size 0 = 0"
   assumes mod_size_less: 
@@ -23,22 +23,6 @@
 lemma size_mult_mono': "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (b * a)"
   by (subst mult.commute) (rule size_mult_mono)
 
-lemma euclidean_size_normalize [simp]:
-  "euclidean_size (normalize a) = euclidean_size a"
-proof (cases "a = 0")
-  case True
-  then show ?thesis
-    by simp
-next
-  case [simp]: False
-  have "euclidean_size (normalize a) \<le> euclidean_size (normalize a * unit_factor a)"
-    by (rule size_mult_mono) simp
-  moreover have "euclidean_size a \<le> euclidean_size (a * (1 div unit_factor a))"
-    by (rule size_mult_mono) simp
-  ultimately show ?thesis
-    by simp
-qed
-
 lemma dvd_euclidean_size_eq_imp_dvd:
   assumes "a \<noteq> 0" and "euclidean_size a = euclidean_size b"
     and "b dvd a" 
diff -r 212a3334e7da -r 0b12755ccbb2 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Main.thy	Sun Oct 08 22:28:22 2017 +0200
@@ -6,7 +6,16 @@
 \<close>
 
 theory Main
-imports Predicate_Compile Quickcheck_Narrowing Extraction Nunchaku BNF_Greatest_Fixpoint Filter Conditionally_Complete_Lattices Binomial GCD
+  imports
+    Predicate_Compile
+    Quickcheck_Narrowing 
+    Extraction
+    Nunchaku
+    BNF_Greatest_Fixpoint Filter
+    Conditionally_Complete_Lattices
+    Binomial
+    GCD
+    Nat_Transfer
 begin
 
 text \<open>
diff -r 212a3334e7da -r 0b12755ccbb2 src/HOL/Nat_Transfer.thy
--- a/src/HOL/Nat_Transfer.thy	Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Nat_Transfer.thy	Sun Oct 08 22:28:22 2017 +0200
@@ -3,7 +3,7 @@
 section \<open>Generic transfer machinery;  specific transfer from nats to ints and back.\<close>
 
 theory Nat_Transfer
-imports Int
+imports Int Divides
 begin
 
 subsection \<open>Generic transfer machinery\<close>
@@ -21,7 +21,8 @@
 
 text \<open>set up transfer direction\<close>
 
-lemma transfer_morphism_nat_int: "transfer_morphism nat (op <= (0::int))" ..
+lemma transfer_morphism_nat_int [no_atp]:
+  "transfer_morphism nat (op <= (0::int))" ..
 
 declare transfer_morphism_nat_int [transfer add
   mode: manual
@@ -31,7 +32,7 @@
 
 text \<open>basic functions and relations\<close>
 
-lemma transfer_nat_int_numerals [transfer key: transfer_morphism_nat_int]:
+lemma transfer_nat_int_numerals [no_atp, transfer key: transfer_morphism_nat_int]:
     "(0::nat) = nat 0"
     "(1::nat) = nat 1"
     "(2::nat) = nat 2"
@@ -46,15 +47,17 @@
 lemma tsub_eq: "x >= y \<Longrightarrow> tsub x y = x - y"
   by (simp add: tsub_def)
 
-lemma transfer_nat_int_functions [transfer key: transfer_morphism_nat_int]:
+lemma transfer_nat_int_functions [no_atp, transfer key: transfer_morphism_nat_int]:
     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) + (nat y) = nat (x + y)"
     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) * (nat y) = nat (x * y)"
     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) - (nat y) = nat (tsub x y)"
     "(x::int) >= 0 \<Longrightarrow> (nat x)^n = nat (x^n)"
+    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
+    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
   by (auto simp add: eq_nat_nat_iff nat_mult_distrib
-      nat_power_eq tsub_def)
+      nat_power_eq tsub_def nat_div_distrib nat_mod_distrib)
 
-lemma transfer_nat_int_function_closures [transfer key: transfer_morphism_nat_int]:
+lemma transfer_nat_int_function_closures [no_atp, transfer key: transfer_morphism_nat_int]:
     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x + y >= 0"
     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x * y >= 0"
     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> tsub x y >= 0"
@@ -64,9 +67,16 @@
     "(2::int) >= 0"
     "(3::int) >= 0"
     "int z >= 0"
-  by (auto simp add: zero_le_mult_iff tsub_def)
+    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
+    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
+            apply (auto simp add: zero_le_mult_iff tsub_def pos_imp_zdiv_nonneg_iff)
+   apply (cases "y = 0")
+    apply (auto simp add: pos_imp_zdiv_nonneg_iff)
+  apply (cases "y = 0")
+   apply auto
+  done
 
-lemma transfer_nat_int_relations [transfer key: transfer_morphism_nat_int]:
+lemma transfer_nat_int_relations [no_atp, transfer key: transfer_morphism_nat_int]:
     "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
       (nat (x::int) = nat y) = (x = y)"
     "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
@@ -94,7 +104,7 @@
   then show "\<exists>x. P x" by auto
 qed
 
-lemma transfer_nat_int_quantifiers [transfer key: transfer_morphism_nat_int]:
+lemma transfer_nat_int_quantifiers [no_atp, transfer key: transfer_morphism_nat_int]:
     "(ALL (x::nat). P x) = (ALL (x::int). x >= 0 \<longrightarrow> P (nat x))"
     "(EX (x::nat). P x) = (EX (x::int). x >= 0 & P (nat x))"
   by (rule all_nat, rule ex_nat)
@@ -126,7 +136,7 @@
 where
   "nat_set S = (ALL x:S. x >= 0)"
 
-lemma transfer_nat_int_set_functions:
+lemma transfer_nat_int_set_functions [no_atp]:
     "card A = card (int ` A)"
     "{} = nat ` ({}::int set)"
     "A Un B = nat ` (int ` A Un int ` B)"
@@ -144,7 +154,7 @@
   apply auto
 done
 
-lemma transfer_nat_int_set_function_closures:
+lemma transfer_nat_int_set_function_closures [no_atp]:
     "nat_set {}"
     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
@@ -154,7 +164,7 @@
   unfolding nat_set_def apply auto
 done
 
-lemma transfer_nat_int_set_relations:
+lemma transfer_nat_int_set_relations [no_atp]:
     "(finite A) = (finite (int ` A))"
     "(x : A) = (int x : int ` A)"
     "(A = B) = (int ` A = int ` B)"
@@ -169,11 +179,11 @@
   apply (drule_tac x = "int x" in spec, auto)
 done
 
-lemma transfer_nat_int_set_return_embed: "nat_set A \<Longrightarrow>
+lemma transfer_nat_int_set_return_embed [no_atp]: "nat_set A \<Longrightarrow>
     (int ` nat ` A = A)"
   by (auto simp add: nat_set_def image_def)
 
-lemma transfer_nat_int_set_cong: "(!!x. x >= 0 \<Longrightarrow> P x = P' x) \<Longrightarrow>
+lemma transfer_nat_int_set_cong [no_atp]: "(!!x. x >= 0 \<Longrightarrow> P x = P' x) \<Longrightarrow>
     {(x::int). x >= 0 & P x} = {x. x >= 0 & P' x}"
   by auto
 
@@ -189,7 +199,7 @@
 text \<open>sum and prod\<close>
 
 (* this handles the case where the *domain* of f is nat *)
-lemma transfer_nat_int_sum_prod:
+lemma transfer_nat_int_sum_prod [no_atp]:
     "sum f A = sum (%x. f (nat x)) (int ` A)"
     "prod f A = prod (%x. f (nat x)) (int ` A)"
   apply (subst sum.reindex)
@@ -199,14 +209,14 @@
 done
 
 (* this handles the case where the *range* of f is nat *)
-lemma transfer_nat_int_sum_prod2:
+lemma transfer_nat_int_sum_prod2 [no_atp]:
     "sum f A = nat(sum (%x. int (f x)) A)"
     "prod f A = nat(prod (%x. int (f x)) A)"
   apply (simp only: int_sum [symmetric] nat_int)
   apply (simp only: int_prod [symmetric] nat_int)
   done
 
-lemma transfer_nat_int_sum_prod_closure:
+lemma transfer_nat_int_sum_prod_closure [no_atp]:
     "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> sum f A >= 0"
     "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> prod f A >= 0"
   unfolding nat_set_def
@@ -236,7 +246,7 @@
    Also, why aren't sum.cong and prod.cong enough,
    with the previously mentioned rule turned on? *)
 
-lemma transfer_nat_int_sum_prod_cong:
+lemma transfer_nat_int_sum_prod_cong [no_atp]:
     "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
       sum f A = sum g B"
     "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
@@ -257,7 +267,7 @@
 
 text \<open>set up transfer direction\<close>
 
-lemma transfer_morphism_int_nat: "transfer_morphism int (\<lambda>n. True)" ..
+lemma transfer_morphism_int_nat [no_atp]: "transfer_morphism int (\<lambda>n. True)" ..
 
 declare transfer_morphism_int_nat [transfer add
   mode: manual
@@ -273,21 +283,23 @@
 where
   "is_nat x = (x >= 0)"
 
-lemma transfer_int_nat_numerals:
+lemma transfer_int_nat_numerals [no_atp]:
     "0 = int 0"
     "1 = int 1"
     "2 = int 2"
     "3 = int 3"
   by auto
 
-lemma transfer_int_nat_functions:
+lemma transfer_int_nat_functions [no_atp]:
     "(int x) + (int y) = int (x + y)"
     "(int x) * (int y) = int (x * y)"
     "tsub (int x) (int y) = int (x - y)"
     "(int x)^n = int (x^n)"
-  by (auto simp add: tsub_def)
+    "(int x) div (int y) = int (x div y)"
+    "(int x) mod (int y) = int (x mod y)"
+  by (auto simp add: zdiv_int zmod_int tsub_def)
 
-lemma transfer_int_nat_function_closures:
+lemma transfer_int_nat_function_closures [no_atp]:
     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x + y)"
     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x * y)"
     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (tsub x y)"
@@ -297,9 +309,11 @@
     "is_nat 2"
     "is_nat 3"
     "is_nat (int z)"
+    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
+    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
   by (simp_all only: is_nat_def transfer_nat_int_function_closures)
 
-lemma transfer_int_nat_relations:
+lemma transfer_int_nat_relations [no_atp]:
     "(int x = int y) = (x = y)"
     "(int x < int y) = (x < y)"
     "(int x <= int y) = (x <= y)"
@@ -316,7 +330,7 @@
 
 text \<open>first-order quantifiers\<close>
 
-lemma transfer_int_nat_quantifiers:
+lemma transfer_int_nat_quantifiers [no_atp]:
     "(ALL (x::int) >= 0. P x) = (ALL (x::nat). P (int x))"
     "(EX (x::int) >= 0. P x) = (EX (x::nat). P (int x))"
   apply (subst all_nat)
@@ -341,7 +355,7 @@
 
 text \<open>operations with sets\<close>
 
-lemma transfer_int_nat_set_functions:
+lemma transfer_int_nat_set_functions [no_atp]:
     "nat_set A \<Longrightarrow> card A = card (nat ` A)"
     "{} = int ` ({}::nat set)"
     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Un B = int ` (nat ` A Un nat ` B)"
@@ -353,7 +367,7 @@
           transfer_nat_int_set_return_embed nat_0_le
           cong: transfer_nat_int_set_cong)
 
-lemma transfer_int_nat_set_function_closures:
+lemma transfer_int_nat_set_function_closures [no_atp]:
     "nat_set {}"
     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
@@ -362,7 +376,7 @@
     "nat_set A \<Longrightarrow> x : A \<Longrightarrow> is_nat x"
   by (simp_all only: transfer_nat_int_set_function_closures is_nat_def)
 
-lemma transfer_int_nat_set_relations:
+lemma transfer_int_nat_set_relations [no_atp]:
     "nat_set A \<Longrightarrow> finite A = finite (nat ` A)"
     "is_nat x \<Longrightarrow> nat_set A \<Longrightarrow> (x : A) = (nat x : nat ` A)"
     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A = B) = (nat ` A = nat ` B)"
@@ -371,12 +385,12 @@
   by (simp_all only: is_nat_def transfer_nat_int_set_relations
     transfer_nat_int_set_return_embed nat_0_le)
 
-lemma transfer_int_nat_set_return_embed: "nat ` int ` A = A"
+lemma transfer_int_nat_set_return_embed [no_atp]: "nat ` int ` A = A"
   by (simp only: transfer_nat_int_set_relations
     transfer_nat_int_set_function_closures
     transfer_nat_int_set_return_embed nat_0_le)
 
-lemma transfer_int_nat_set_cong: "(!!x. P x = P' x) \<Longrightarrow>
+lemma transfer_int_nat_set_cong [no_atp]: "(!!x. P x = P' x) \<Longrightarrow>
     {(x::nat). P x} = {x. P' x}"
   by auto
 
@@ -392,7 +406,7 @@
 text \<open>sum and prod\<close>
 
 (* this handles the case where the *domain* of f is int *)
-lemma transfer_int_nat_sum_prod:
+lemma transfer_int_nat_sum_prod [no_atp]:
     "nat_set A \<Longrightarrow> sum f A = sum (%x. f (int x)) (nat ` A)"
     "nat_set A \<Longrightarrow> prod f A = prod (%x. f (int x)) (nat ` A)"
   apply (subst sum.reindex)
@@ -403,7 +417,7 @@
 done
 
 (* this handles the case where the *range* of f is int *)
-lemma transfer_int_nat_sum_prod2:
+lemma transfer_int_nat_sum_prod2 [no_atp]:
     "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow> sum f A = int(sum (%x. nat (f x)) A)"
     "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow>
       prod f A = int(prod (%x. nat (f x)) A)"
@@ -414,4 +428,6 @@
   return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
   cong: sum.cong prod.cong]
 
+declare transfer_morphism_int_nat [transfer add return: even_int_iff]
+
 end
diff -r 212a3334e7da -r 0b12755ccbb2 src/HOL/Number_Theory/Cong.thy
--- a/src/HOL/Number_Theory/Cong.thy	Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Number_Theory/Cong.thy	Sun Oct 08 22:28:22 2017 +0200
@@ -86,8 +86,7 @@
   "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> m \<ge> 0 \<Longrightarrow> [nat x = nat y] (mod (nat m)) \<longleftrightarrow> [x = y] (mod m)"
   for x y m :: int
   unfolding cong_int_def cong_nat_def
-  by (metis Divides.transfer_int_nat_functions(2) nat_0_le nat_mod_distrib)
-
+  by (metis int_nat_eq nat_mod_distrib zmod_int)
 
 declare transfer_morphism_nat_int [transfer add return: transfer_nat_int_cong]
 
diff -r 212a3334e7da -r 0b12755ccbb2 src/HOL/Number_Theory/Gauss.thy
--- a/src/HOL/Number_Theory/Gauss.thy	Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Number_Theory/Gauss.thy	Sun Oct 08 22:28:22 2017 +0200
@@ -196,7 +196,8 @@
   moreover have "int y = 0 \<or> 0 < int y" for y
     by linarith
   ultimately show "0 < x mod int p"
-    by (metis (no_types) B_greater_zero Divides.transfer_int_nat_functions(2) zero_less_imp_eq_int)
+    using B_greater_zero [of x]
+    by (auto simp add: mod_int_pos_iff intro: neq_le_trans)
 qed
 
 lemma F_subset: "F \<subseteq> {x. 0 < x \<and> x \<le> ((int p - 1) div 2)}"
diff -r 212a3334e7da -r 0b12755ccbb2 src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Number_Theory/Residues.thy	Sun Oct 08 22:28:22 2017 +0200
@@ -365,8 +365,7 @@
     done
   finally have "fact (p - 1) mod p = \<ominus> \<one>" .
   then show ?thesis
-    by (metis of_nat_fact Divides.transfer_int_nat_functions(2)
-        cong_int_def res_neg_eq res_one_eq)
+    by (simp add: cong_int_def res_neg_eq res_one_eq zmod_int)
 qed
 
 lemma wilson_theorem:
diff -r 212a3334e7da -r 0b12755ccbb2 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/SMT.thy	Sun Oct 08 22:28:22 2017 +0200
@@ -124,8 +124,14 @@
 lemma int_nat_nneg: "\<forall>i. i \<ge> 0 \<longrightarrow> int (nat i) = i" by simp
 lemma int_nat_neg: "\<forall>i. i < 0 \<longrightarrow> int (nat i) = 0" by simp
 
-lemmas nat_zero_as_int = transfer_nat_int_numerals(1)
-lemmas nat_one_as_int = transfer_nat_int_numerals(2)
+lemma nat_zero_as_int:
+  "0 = nat 0"
+  by simp
+
+lemma nat_one_as_int:
+  "1 = nat 1"
+  by simp
+
 lemma nat_numeral_as_int: "numeral = (\<lambda>i. nat (numeral i))" by simp
 lemma nat_less_as_int: "op < = (\<lambda>a b. int a < int b)" by simp
 lemma nat_leq_as_int: "op \<le> = (\<lambda>a b. int a \<le> int b)" by simp