# HG changeset patch
# User haftmann
# Date 1509433863 0
# Node ID 0230af0f3c590e728a27df19c8c5add4563e881a
# Parent  826a5fd4d36c490f29536a5eea83139ac7c357bf
removed ancient nat-int transfer

diff -r 826a5fd4d36c -r 0230af0f3c59 NEWS
--- a/NEWS	Mon Oct 30 19:29:06 2017 +0000
+++ b/NEWS	Tue Oct 31 07:11:03 2017 +0000
@@ -66,6 +66,8 @@
 * Class linordered_semiring_1 covers zero_less_one also, ruling out
 pathologic instances. Minor INCOMPATIBILITY.
 
+* Removed nat-int transfer machinery.  Rare INCOMPATIBILITY.
+
 
 *** System ***
 
diff -r 826a5fd4d36c -r 0230af0f3c59 src/HOL/Decision_Procs/Conversions.thy
--- a/src/HOL/Decision_Procs/Conversions.thy	Mon Oct 30 19:29:06 2017 +0000
+++ b/src/HOL/Decision_Procs/Conversions.thy	Tue Oct 31 07:11:03 2017 +0000
@@ -93,7 +93,7 @@
 ML \<open>
 fun nat_conv i = (case strip_app i of
     (@{const_name zero_class.zero}, []) => @{thm nat_0 [meta]}
-  | (@{const_name one_class.one}, []) => @{thm transfer_nat_int_numerals(2) [meta, symmetric]}
+  | (@{const_name one_class.one}, []) => @{thm nat_one_as_int [meta, symmetric]}
   | (@{const_name numeral}, [b]) => inst [] [b] @{thm nat_numeral [meta]}
   | (@{const_name uminus}, [b]) => (case strip_app b of
       (@{const_name one_class.one}, []) => @{thm nat_minus1_eq [meta]}
diff -r 826a5fd4d36c -r 0230af0f3c59 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Mon Oct 30 19:29:06 2017 +0000
+++ b/src/HOL/Main.thy	Tue Oct 31 07:11:03 2017 +0000
@@ -15,7 +15,6 @@
     Conditionally_Complete_Lattices
     Binomial
     GCD
-    Nat_Transfer
 begin
 
 text \<open>
diff -r 826a5fd4d36c -r 0230af0f3c59 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Oct 30 19:29:06 2017 +0000
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Tue Oct 31 07:11:03 2017 +0000
@@ -268,7 +268,6 @@
  @{const_name Meson.skolem},
  @{const_name ATP.fequal},
  @{const_name ATP.fEx},
- @{const_name transfer_morphism},
  @{const_name enum_prod_inst.enum_all_prod},
  @{const_name enum_prod_inst.enum_ex_prod},
  @{const_name Quickcheck_Random.catch_match},
diff -r 826a5fd4d36c -r 0230af0f3c59 src/HOL/Nat_Transfer.thy
--- a/src/HOL/Nat_Transfer.thy	Mon Oct 30 19:29:06 2017 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,464 +0,0 @@
-(* Authors: Jeremy Avigad and Amine Chaieb *)
-
-section \<open>Generic transfer machinery;  specific transfer from nats to ints and back.\<close>
-
-theory Nat_Transfer
-imports List GCD
-begin
-
-subsection \<open>Generic transfer machinery\<close>
-
-definition transfer_morphism:: "('b \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool"
-  where "transfer_morphism f A \<longleftrightarrow> True"
-
-lemma transfer_morphismI[intro]: "transfer_morphism f A"
-  by (simp add: transfer_morphism_def)
-
-ML_file "Tools/legacy_transfer.ML"
-
-
-subsection \<open>Set up transfer from nat to int\<close>
-
-text \<open>set up transfer direction\<close>
-
-lemma transfer_morphism_nat_int [no_atp]:
-  "transfer_morphism nat (op <= (0::int))" ..
-
-declare transfer_morphism_nat_int [transfer add
-  mode: manual
-  return: nat_0_le
-  labels: nat_int
-]
-
-text \<open>basic functions and relations\<close>
-
-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"
-    "(3::nat) = nat 3"
-  by auto
-
-definition
-  tsub :: "int \<Rightarrow> int \<Rightarrow> int"
-where
-  "tsub x y = (if x >= y then x - y else 0)"
-
-lemma tsub_eq: "x >= y \<Longrightarrow> tsub x y = x - y"
-  by (simp add: tsub_def)
-
-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_div_distrib nat_mod_distrib)
-
-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"
-    "(x::int) >= 0 \<Longrightarrow> x^n >= 0"
-    "(0::int) >= 0"
-    "(1::int) >= 0"
-    "(2::int) >= 0"
-    "(3::int) >= 0"
-    "int z >= 0"
-    "(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 [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>
-      (nat (x::int) < nat y) = (x < y)"
-    "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
-      (nat (x::int) <= nat y) = (x <= y)"
-    "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
-      (nat (x::int) dvd nat y) = (x dvd y)"
-  by (auto simp add: zdvd_int)
-
-
-text \<open>first-order quantifiers\<close>
-
-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)
-
-declare transfer_morphism_nat_int [transfer add
-  cong: all_cong ex_cong]
-
-
-text \<open>if\<close>
-
-lemma nat_if_cong [transfer key: transfer_morphism_nat_int]:
-  "(if P then (nat x) else (nat y)) = nat (if P then x else y)"
-  by auto
-
-
-text \<open>operations with sets\<close>
-
-definition
-  nat_set :: "int set \<Rightarrow> bool"
-where
-  "nat_set S = (ALL x:S. x >= 0)"
-
-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)"
-    "A Int B = nat ` (int ` A Int int ` B)"
-    "{x. P x} = nat ` {x. x >= 0 & P(nat x)}"
-    "{..n} = nat ` {0..int n}"
-    "{m..n} = nat ` {int m..int n}"  (* need all variants of these! *)
-  by (rule card_image [symmetric])
-    (auto simp add: inj_on_def image_def intro: bexI [of _ "int x" for x] exI [of _ "int x" for x])
-
-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)"
-    "nat_set {x. x >= 0 & P x}"
-    "nat_set (int ` C)"
-    "nat_set A \<Longrightarrow> x : A \<Longrightarrow> x >= 0" (* does it hurt to turn this on? *)
-    "x >= 0 \<Longrightarrow> nat_set {x..y}"
-  unfolding nat_set_def apply auto
-done
-
-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)"
-    "(A < B) = (int ` A < int ` B)"
-    "(A <= B) = (int ` A <= int ` B)"
-  apply (rule iffI)
-  apply (erule finite_imageI)
-  apply (erule finite_imageD)
-  apply (auto simp add: image_def set_eq_iff inj_on_def)
-  apply (drule_tac x = "int x" in spec, auto)
-  apply (drule_tac x = "int x" in spec, auto)
-  apply (drule_tac x = "int x" in spec, auto)
-done
-
-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 [no_atp]: "(!!x. x >= 0 \<Longrightarrow> P x = P' x) \<Longrightarrow>
-    {(x::int). x >= 0 & P x} = {x. x >= 0 & P' x}"
-  by auto
-
-declare transfer_morphism_nat_int [transfer add
-  return: transfer_nat_int_set_functions
-    transfer_nat_int_set_function_closures
-    transfer_nat_int_set_relations
-    transfer_nat_int_set_return_embed
-  cong: transfer_nat_int_set_cong
-]
-
-
-text \<open>sum and prod\<close>
-
-(* this handles the case where the *domain* of f is nat *)
-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)
-  apply (unfold inj_on_def, auto)
-  apply (subst prod.reindex)
-  apply (unfold inj_on_def o_def, auto)
-done
-
-(* this handles the case where the *range* of f is nat *)
-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 [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
-  apply (rule sum_nonneg)
-  apply auto
-  apply (rule prod_nonneg)
-  apply auto
-done
-
-(* this version doesn't work, even with nat_set A \<Longrightarrow>
-      x : A \<Longrightarrow> x >= 0 turned on. Why not?
-
-  also: what does =simp=> do?
-
-lemma transfer_nat_int_sum_prod_closure:
-    "(!!x. x : A  ==> f x >= (0::int)) \<Longrightarrow> sum f A >= 0"
-    "(!!x. x : A  ==> f x >= (0::int)) \<Longrightarrow> prod f A >= 0"
-  unfolding nat_set_def simp_implies_def
-  apply (rule sum_nonneg)
-  apply auto
-  apply (rule prod_nonneg)
-  apply auto
-done
-*)
-
-(* Making A = B in this lemma doesn't work. Why not?
-   Also, why aren't sum.cong and prod.cong enough,
-   with the previously mentioned rule turned on? *)
-
-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>
-      prod f A = prod g B"
-  unfolding nat_set_def
-  apply (subst sum.cong, assumption)
-  apply auto [2]
-  apply (subst prod.cong, assumption, auto)
-done
-
-declare transfer_morphism_nat_int [transfer add
-  return: transfer_nat_int_sum_prod transfer_nat_int_sum_prod2
-    transfer_nat_int_sum_prod_closure
-  cong: transfer_nat_int_sum_prod_cong]
-
-
-subsection \<open>Set up transfer from int to nat\<close>
-
-text \<open>set up transfer direction\<close>
-
-lemma transfer_morphism_int_nat [no_atp]: "transfer_morphism int (\<lambda>n. True)" ..
-
-declare transfer_morphism_int_nat [transfer add
-  mode: manual
-  return: nat_int
-  labels: int_nat
-]
-
-
-text \<open>basic functions and relations\<close>
-
-definition
-  is_nat :: "int \<Rightarrow> bool"
-where
-  "is_nat x = (x >= 0)"
-
-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 [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)"
-    "(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 [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)"
-    "is_nat x \<Longrightarrow> is_nat (x^n)"
-    "is_nat 0"
-    "is_nat 1"
-    "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 [no_atp]:
-    "(int x = int y) = (x = y)"
-    "(int x < int y) = (x < y)"
-    "(int x <= int y) = (x <= y)"
-    "(int x dvd int y) = (x dvd y)"
-  by (auto simp add: zdvd_int)
-
-declare transfer_morphism_int_nat [transfer add return:
-  transfer_int_nat_numerals
-  transfer_int_nat_functions
-  transfer_int_nat_function_closures
-  transfer_int_nat_relations
-]
-
-
-text \<open>first-order quantifiers\<close>
-
-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)
-  apply auto [1]
-  apply (subst ex_nat)
-  apply auto
-done
-
-declare transfer_morphism_int_nat [transfer add
-  return: transfer_int_nat_quantifiers]
-
-
-text \<open>if\<close>
-
-lemma int_if_cong: "(if P then (int x) else (int y)) =
-    int (if P then x else y)"
-  by auto
-
-declare transfer_morphism_int_nat [transfer add return: int_if_cong]
-
-
-
-text \<open>operations with sets\<close>
-
-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)"
-    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Int B = int ` (nat ` A Int nat ` B)"
-    "{x. x >= 0 & P x} = int ` {x. P(int x)}"
-    "is_nat m \<Longrightarrow> is_nat n \<Longrightarrow> {m..n} = int ` {nat m..nat n}"
-       (* need all variants of these! *)
-  by (simp_all only: is_nat_def transfer_nat_int_set_functions
-          transfer_nat_int_set_function_closures
-          transfer_nat_int_set_return_embed nat_0_le
-          cong: transfer_nat_int_set_cong)
-
-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)"
-    "nat_set {x. x >= 0 & P x}"
-    "nat_set (int ` C)"
-    "nat_set A \<Longrightarrow> x : A \<Longrightarrow> is_nat x"
-    "is_nat x \<Longrightarrow> nat_set {x..y}"
-  by (simp_all only: transfer_nat_int_set_function_closures is_nat_def)
-
-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)"
-    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A < B) = (nat ` A < nat ` B)"
-    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A <= B) = (nat ` A <= nat ` B)"
-  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 [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 [no_atp]: "(!!x. P x = P' x) \<Longrightarrow>
-    {(x::nat). P x} = {x. P' x}"
-  by auto
-
-declare transfer_morphism_int_nat [transfer add
-  return: transfer_int_nat_set_functions
-    transfer_int_nat_set_function_closures
-    transfer_int_nat_set_relations
-    transfer_int_nat_set_return_embed
-  cong: transfer_int_nat_set_cong
-]
-
-
-text \<open>sum and prod\<close>
-
-(* this handles the case where the *domain* of f is int *)
-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)
-  apply (unfold inj_on_def nat_set_def, auto simp add: eq_nat_nat_iff)
-  apply (subst prod.reindex)
-  apply (unfold inj_on_def nat_set_def o_def, auto simp add: eq_nat_nat_iff
-            cong: prod.cong)
-done
-
-(* this handles the case where the *range* of f is int *)
-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)"
-  unfolding is_nat_def
-  by (subst int_sum) auto
-
-declare transfer_morphism_int_nat [transfer add
-  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]
-
-lemma transfer_nat_int_gcd [no_atp]:
-  "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
-  "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> lcm (nat x) (nat y) = nat (lcm x y)"
-  for x y :: int
-  unfolding gcd_int_def lcm_int_def by auto
-
-lemma transfer_nat_int_gcd_closures [no_atp]:
-  "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> gcd x y \<ge> 0"
-  "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> lcm x y \<ge> 0"
-  for x y :: int
-  by (auto simp add: gcd_int_def lcm_int_def)
-
-declare transfer_morphism_nat_int
-  [transfer add return: transfer_nat_int_gcd transfer_nat_int_gcd_closures]
-
-lemma transfer_int_nat_gcd [no_atp]:
-  "gcd (int x) (int y) = int (gcd x y)"
-  "lcm (int x) (int y) = int (lcm x y)"
-  by (auto simp: gcd_int_def lcm_int_def)
-
-lemma transfer_int_nat_gcd_closures [no_atp]:
-  "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> gcd x y >= 0"
-  "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0"
-  by (auto simp: gcd_int_def lcm_int_def)
-
-declare transfer_morphism_int_nat
-  [transfer add return: transfer_int_nat_gcd transfer_int_nat_gcd_closures]
-
-definition embed_list :: "nat list \<Rightarrow> int list" where
-"embed_list l = map int l"
-
-definition nat_list :: "int list \<Rightarrow> bool" where
-"nat_list l = nat_set (set l)"
-
-definition return_list :: "int list \<Rightarrow> nat list" where
-"return_list l = map nat l"
-
-lemma transfer_nat_int_list_return_embed [no_atp]:
-  "nat_list l \<longrightarrow> embed_list (return_list l) = l"
-  unfolding embed_list_def return_list_def nat_list_def nat_set_def
-  apply (induct l)
-  apply auto
-done
-
-lemma transfer_nat_int_list_functions [no_atp]:
-  "l @ m = return_list (embed_list l @ embed_list m)"
-  "[] = return_list []"
-  unfolding return_list_def embed_list_def
-  apply auto
-  apply (induct l, auto)
-  apply (induct m, auto)
-done
-
-(*
-lemma transfer_nat_int_fold1: "fold f l x =
-    fold (%x. f (nat x)) (embed_list l) x";
-*)
-
-end
diff -r 826a5fd4d36c -r 0230af0f3c59 src/HOL/Number_Theory/Cong.thy
--- a/src/HOL/Number_Theory/Cong.thy	Mon Oct 30 19:29:06 2017 +0000
+++ b/src/HOL/Number_Theory/Cong.thy	Tue Oct 31 07:11:03 2017 +0000
@@ -161,54 +161,56 @@
 
 subsection \<open>Congruences on @{typ nat} and @{typ int}\<close>
 
-lemma transfer_nat_int_cong:
-  "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
-  by (auto simp add: cong_def nat_mod_distrib [symmetric])
-     (metis eq_nat_nat_iff le_less mod_by_0 pos_mod_conj)
-
-declare transfer_morphism_nat_int [transfer add return: transfer_nat_int_cong]
-
 lemma cong_int_iff:
   "[int m = int q] (mod int n) \<longleftrightarrow> [m = q] (mod n)"
   by (simp add: cong_def of_nat_mod [symmetric])
 
-lemma transfer_int_nat_cong:
-  "[int x = int y] (mod (int m)) = [x = y] (mod m)"
-  by (fact cong_int_iff)
-
-declare transfer_morphism_int_nat [transfer add return: transfer_int_nat_cong]
-
 lemma cong_Suc_0 [simp, presburger]:
   "[m = n] (mod Suc 0)"
   using cong_1 [of m n] by simp
 
-lemma cong_diff_aux_int:
-  "[a = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow>
-    a \<ge> c \<Longrightarrow> b \<ge> d \<Longrightarrow> [tsub a c = tsub b d] (mod m)"
-  for a b c d :: int
-  by (metis cong_diff tsub_eq)
-
 lemma cong_diff_nat:
   "[a - c = b - d] (mod m)" if "[a = b] (mod m)" "[c = d] (mod m)"
-    and "a \<ge> c" "b \<ge> d" for a b c d m :: nat 
-  using that by (rule cong_diff_aux_int [transferred])
-
-lemma cong_diff_iff_cong_0_aux_int: "a \<ge> b \<Longrightarrow> [tsub a b = 0] (mod m) = [a = b] (mod m)"
-  for a b :: int
-  by (subst tsub_eq, assumption, rule cong_diff_iff_cong_0)
+    and "a \<ge> c" "b \<ge> d" for a b c d m :: nat
+proof -
+  have "[c + (a - c) = d + (b - d)] (mod m)"
+    using that by simp
+  with \<open>[c = d] (mod m)\<close> have "[c + (a - c) = c + (b - d)] (mod m)"
+    using mod_add_cong by (auto simp add: cong_def) fastforce
+  then show ?thesis
+    by (simp add: cong_def nat_mod_eq_iff)
+qed
 
 lemma cong_diff_iff_cong_0_nat:
-  fixes a b :: nat
-  assumes "a \<ge> b"
-  shows "[a - b = 0] (mod m) = [a = b] (mod m)"
-  using assms by (rule cong_diff_iff_cong_0_aux_int [transferred])
+  "[a - b = 0] (mod m) \<longleftrightarrow> [a = b] (mod m)" if "a \<ge> b" for a b :: nat
+  using that by (auto simp add: cong_def le_imp_diff_is_add dest: nat_mod_eq_lemma)
 
-lemma cong_altdef_nat: "a \<ge> b \<Longrightarrow> [a = b] (mod m) \<longleftrightarrow> m dvd (a - b)"
+lemma cong_diff_iff_cong_0_nat':
+  "[nat \<bar>int a - int b\<bar> = 0] (mod m) \<longleftrightarrow> [a = b] (mod m)"
+proof (cases "b \<le> a")
+  case True
+  then show ?thesis
+    by (simp add: nat_diff_distrib' cong_diff_iff_cong_0_nat [of b a m])
+next
+  case False
+  then have "a \<le> b"
+    by simp
+  then show ?thesis
+    by (simp add: nat_diff_distrib' cong_diff_iff_cong_0_nat [of a b m])
+      (auto simp add: cong_def)
+qed
+
+lemma cong_altdef_nat:
+  "a \<ge> b \<Longrightarrow> [a = b] (mod m) \<longleftrightarrow> m dvd (a - b)"
   for a b :: nat
   by (simp add: cong_0_iff [symmetric] cong_diff_iff_cong_0_nat)
 
-lemma cong_altdef_int: "[a = b] (mod m) \<longleftrightarrow> m dvd (a - b)"
+lemma cong_altdef_nat':
+  "[a = b] (mod m) \<longleftrightarrow> m dvd nat \<bar>int a - int b\<bar>"
+  by (simp add: cong_0_iff [symmetric] cong_diff_iff_cong_0_nat')
+
+lemma cong_altdef_int:
+  "[a = b] (mod m) \<longleftrightarrow> m dvd (a - b)"
   for a b :: int
   by (simp add: cong_0_iff [symmetric] cong_diff_iff_cong_0)
 
@@ -224,31 +226,47 @@
   apply (auto simp add: field_simps)
   done
 
-lemma cong_mult_rcancel_int: "coprime k m \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
-  for a k m :: int
-  by (metis cong_altdef_int left_diff_distrib coprime_dvd_mult_iff gcd.commute)
-
-lemma cong_mult_rcancel_nat: "coprime k m \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
-  for a k m :: nat
-  by (metis cong_mult_rcancel_int [transferred])
+lemma cong_mult_rcancel_int:
+  "[a * k = b * k] (mod m) \<longleftrightarrow> [a = b] (mod m)"
+  if "coprime k m" for a k m :: int
+  by (metis that cong_altdef_int left_diff_distrib coprime_dvd_mult_iff gcd.commute)
 
-lemma cong_mult_lcancel_nat: "coprime k m \<Longrightarrow> [k * a = k * b ] (mod m) = [a = b] (mod m)"
-  for a k m :: nat
-  by (simp add: mult.commute cong_mult_rcancel_nat)
+lemma cong_mult_rcancel_nat:
+  "[a * k = b * k] (mod m) \<longleftrightarrow> [a = b] (mod m)"
+  if "coprime k m" for a k m :: nat
+proof -
+  have "[a * k = b * k] (mod m) \<longleftrightarrow> m dvd nat \<bar>int (a * k) - int (b * k)\<bar>"
+    by (simp add: cong_altdef_nat')
+  also have "\<dots> \<longleftrightarrow> m dvd nat \<bar>(int a - int b) * int k\<bar>"
+    by (simp add: algebra_simps)
+  also have "\<dots> \<longleftrightarrow> m dvd nat \<bar>int a - int b\<bar> * k"
+    by (simp add: abs_mult nat_times_as_int)
+  also have "\<dots> \<longleftrightarrow> m dvd nat \<bar>int a - int b\<bar>"
+    by (rule coprime_dvd_mult_iff) (use \<open>coprime k m\<close> in \<open>simp add: ac_simps\<close>)
+  also have "\<dots> \<longleftrightarrow> [a = b] (mod m)"
+    by (simp add: cong_altdef_nat')
+  finally show ?thesis .
+qed
 
-lemma cong_mult_lcancel_int: "coprime k m \<Longrightarrow> [k * a = k * b] (mod m) = [a = b] (mod m)"
-  for a k m :: int
-  by (simp add: mult.commute cong_mult_rcancel_int)
+lemma cong_mult_lcancel_int:
+  "[k * a = k * b] (mod m) = [a = b] (mod m)"
+  if "coprime k m" for a k m :: int
+  using that by (simp add: cong_mult_rcancel_int ac_simps)
+
+lemma cong_mult_lcancel_nat:
+  "[k * a = k * b] (mod m) = [a = b] (mod m)"
+  if "coprime k m" for a k m :: nat
+  using that by (simp add: cong_mult_rcancel_nat ac_simps)
 
 lemma coprime_cong_mult_int:
   "[a = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n \<Longrightarrow> [a = b] (mod m * n)"
   for a b :: int
-  by (metis divides_mult cong_altdef_int)
+  by (simp add: cong_altdef_int divides_mult)
 
 lemma coprime_cong_mult_nat:
   "[a = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n \<Longrightarrow> [a = b] (mod m * n)"
   for a b :: nat
-  by (metis coprime_cong_mult_int [transferred])
+  by (simp add: cong_altdef_nat' divides_mult)
 
 lemma cong_less_imp_eq_nat: "0 \<le> a \<Longrightarrow> a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b"
   for a b :: nat
@@ -292,14 +310,14 @@
     by (metis cong_def mult.commute nat_mod_eq_iff) 
 qed
 
+lemma cong_gcd_eq_nat: "[a = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
+  for a b :: nat
+  by (auto simp add: cong_def) (metis gcd_red_nat)
+
 lemma cong_gcd_eq_int: "[a = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
   for a b :: int
   by (auto simp add: cong_def) (metis gcd_red_int)
 
-lemma cong_gcd_eq_nat: "[a = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
-  for a b :: nat
-  by (metis cong_gcd_eq_int [transferred])
-
 lemma cong_imp_coprime_nat: "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
   for a b :: nat
   by (auto simp add: cong_gcd_eq_nat)
diff -r 826a5fd4d36c -r 0230af0f3c59 src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Mon Oct 30 19:29:06 2017 +0000
+++ b/src/HOL/Number_Theory/Residues.thy	Tue Oct 31 07:11:03 2017 +0000
@@ -291,8 +291,8 @@
 next
   case False
   with assms show ?thesis
-    using residues.euler_theorem [of "int m" "int a"] transfer_int_nat_cong
-    by (auto simp add: residues_def gcd_int_def) force
+    using residues.euler_theorem [of "int m" "int a"] cong_int_iff
+    by (auto simp add: residues_def gcd_int_def) fastforce
 qed
 
 lemma fermat_theorem:
diff -r 826a5fd4d36c -r 0230af0f3c59 src/HOL/ROOT
--- a/src/HOL/ROOT	Mon Oct 30 19:29:06 2017 +0000
+++ b/src/HOL/ROOT	Tue Oct 31 07:11:03 2017 +0000
@@ -590,7 +590,6 @@
     Termination
     ThreeDivides
     Transfer_Debug
-    Transfer_Ex
     Transfer_Int_Nat
     Transitive_Closure_Table_Ex
     Tree23
diff -r 826a5fd4d36c -r 0230af0f3c59 src/HOL/ex/Transfer_Ex.thy
--- a/src/HOL/ex/Transfer_Ex.thy	Mon Oct 30 19:29:06 2017 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,65 +0,0 @@
-
-section \<open>Various examples for transfer procedure\<close>
-
-theory Transfer_Ex
-imports Main Transfer_Int_Nat
-begin
-
-lemma ex1: "(x::nat) + y = y + x"
-  by auto
-
-lemma "0 \<le> (y::int) \<Longrightarrow> 0 \<le> (x::int) \<Longrightarrow> x + y = y + x"
-  by (fact ex1 [transferred])
-
-(* Using new transfer package *)
-lemma "0 \<le> (x::int) \<Longrightarrow> 0 \<le> (y::int) \<Longrightarrow> x + y = y + x"
-  by (fact ex1 [untransferred])
-
-lemma ex2: "(a::nat) div b * b + a mod b = a"
-  by (rule div_mult_mod_eq)
-
-lemma "0 \<le> (b::int) \<Longrightarrow> 0 \<le> (a::int) \<Longrightarrow> a div b * b + a mod b = a"
-  by (fact ex2 [transferred])
-
-(* Using new transfer package *)
-lemma "0 \<le> (a::int) \<Longrightarrow> 0 \<le> (b::int) \<Longrightarrow> a div b * b + a mod b = a"
-  by (fact ex2 [untransferred])
-
-lemma ex3: "ALL (x::nat). ALL y. EX z. z >= x + y"
-  by auto
-
-lemma "\<forall>x\<ge>0::int. \<forall>y\<ge>0. \<exists>z\<ge>0. x + y \<le> z"
-  by (fact ex3 [transferred nat_int])
-
-(* Using new transfer package *)
-lemma "\<forall>x::int\<in>{0..}. \<forall>y\<in>{0..}. \<exists>z\<in>{0..}. x + y \<le> z"
-  by (fact ex3 [untransferred])
-
-lemma ex4: "(x::nat) >= y \<Longrightarrow> (x - y) + y = x"
-  by auto
-
-lemma "0 \<le> (x::int) \<Longrightarrow> 0 \<le> (y::int) \<Longrightarrow> y \<le> x \<Longrightarrow> tsub x y + y = x"
-  by (fact ex4 [transferred])
-
-(* Using new transfer package *)
-lemma "0 \<le> (y::int) \<Longrightarrow> 0 \<le> (x::int) \<Longrightarrow> y \<le> x \<Longrightarrow> tsub x y + y = x"
-  by (fact ex4 [untransferred])
-
-lemma ex5: "(2::nat) * \<Sum>{..n} = n * (n + 1)"
-  by (induct n rule: nat_induct, auto)
-
-lemma "0 \<le> (n::int) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
-  by (fact ex5 [transferred])
-
-(* Using new transfer package *)
-lemma "0 \<le> (n::int) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
-  by (fact ex5 [untransferred])
-
-lemma "0 \<le> (n::nat) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
-  by (fact ex5 [transferred, transferred])
-
-(* Using new transfer package *)
-lemma "0 \<le> (n::nat) \<Longrightarrow> 2 * \<Sum>{..n} = n * (n + 1)"
-  by (fact ex5 [untransferred, Transfer.transferred])
-
-end
diff -r 826a5fd4d36c -r 0230af0f3c59 src/HOL/ex/Transfer_Int_Nat.thy
--- a/src/HOL/ex/Transfer_Int_Nat.thy	Mon Oct 30 19:29:06 2017 +0000
+++ b/src/HOL/ex/Transfer_Int_Nat.thy	Tue Oct 31 07:11:03 2017 +0000
@@ -39,13 +39,16 @@
   unfolding rel_fun_def ZN_def by simp
 
 lemma ZN_mult [transfer_rule]: "(ZN ===> ZN ===> ZN) (op *) (op *)"
-  unfolding rel_fun_def ZN_def by (simp add: of_nat_mult)
+  unfolding rel_fun_def ZN_def by simp
+
+definition tsub :: "int \<Rightarrow> int \<Rightarrow> int"
+  where "tsub k l = max 0 (k - l)"
 
 lemma ZN_diff [transfer_rule]: "(ZN ===> ZN ===> ZN) tsub (op -)"
-  unfolding rel_fun_def ZN_def tsub_def by (simp add: of_nat_diff)
+  unfolding rel_fun_def ZN_def by (auto simp add: of_nat_diff tsub_def)
 
 lemma ZN_power [transfer_rule]: "(ZN ===> op = ===> ZN) (op ^) (op ^)"
-  unfolding rel_fun_def ZN_def by (simp add: of_nat_power)
+  unfolding rel_fun_def ZN_def by simp
 
 lemma ZN_nat_id [transfer_rule]: "(ZN ===> op =) nat id"
   unfolding rel_fun_def ZN_def by simp
@@ -92,7 +95,7 @@
   unfolding rel_fun_def ZN_def by (simp add: zmod_int)
 
 lemma ZN_gcd [transfer_rule]: "(ZN ===> ZN ===> ZN) gcd gcd"
-  unfolding rel_fun_def ZN_def by (simp add: transfer_int_nat_gcd)
+  unfolding rel_fun_def ZN_def by (simp add: gcd_int_def)
 
 lemma ZN_atMost [transfer_rule]:
   "(ZN ===> rel_set ZN) (atLeastAtMost 0) atMost"