# HG changeset patch
# User haftmann
# Date 1256812896 -3600
# Node ID ddd97d9dfbfbae93e328bda94a3d193c2f59e7af
# Parent  dfda7461950926ff3e0155c15df7fafabd65688a
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly

diff -r dfda74619509 -r ddd97d9dfbfb src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Thu Oct 29 08:14:39 2009 +0100
+++ b/src/HOL/Code_Numeral.thy	Thu Oct 29 11:41:36 2009 +0100
@@ -3,7 +3,7 @@
 header {* Type of target language numerals *}
 
 theory Code_Numeral
-imports Nat_Numeral Divides
+imports Nat_Numeral Nat_Transfer Divides
 begin
 
 text {*
diff -r dfda74619509 -r ddd97d9dfbfb src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu Oct 29 08:14:39 2009 +0100
+++ b/src/HOL/Divides.thy	Thu Oct 29 11:41:36 2009 +0100
@@ -6,7 +6,7 @@
 header {* The division operators div and mod *}
 
 theory Divides
-imports Nat_Numeral
+imports Nat_Numeral Nat_Transfer
 uses
   "~~/src/Provers/Arith/assoc_fold.ML"
   "~~/src/Provers/Arith/cancel_numerals.ML"
diff -r dfda74619509 -r ddd97d9dfbfb src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Thu Oct 29 08:14:39 2009 +0100
+++ b/src/HOL/Fun.thy	Thu Oct 29 11:41:36 2009 +0100
@@ -7,7 +7,6 @@
 
 theory Fun
 imports Complete_Lattice
-uses ("Tools/transfer.ML")
 begin
 
 text{*As a simplification rule, it replaces all function equalities by
@@ -604,16 +603,6 @@
 *}
 
 
-subsection {* Generic transfer procedure *}
-
-definition TransferMorphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
-  where "TransferMorphism a B \<longleftrightarrow> True"
-
-use "Tools/transfer.ML"
-
-setup Transfer.setup
-
-
 subsection {* Code generator setup *}
 
 types_code
diff -r dfda74619509 -r ddd97d9dfbfb src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Thu Oct 29 08:14:39 2009 +0100
+++ b/src/HOL/GCD.thy	Thu Oct 29 11:41:36 2009 +0100
@@ -28,7 +28,7 @@
 header {* GCD *}
 
 theory GCD
-imports Fact
+imports Fact Parity
 begin
 
 declare One_nat_def [simp del]
diff -r dfda74619509 -r ddd97d9dfbfb src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Thu Oct 29 08:14:39 2009 +0100
+++ b/src/HOL/IntDiv.thy	Thu Oct 29 11:41:36 2009 +0100
@@ -1024,139 +1024,16 @@
 lemmas zdvd_iff_zmod_eq_0_number_of [simp] =
   dvd_eq_mod_eq_0 [of "number_of x::int" "number_of y::int", standard]
 
-lemma zdvd_anti_sym:
-    "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
-  apply (simp add: dvd_def, auto)
-  apply (simp add: mult_assoc zero_less_mult_iff zmult_eq_1_iff)
-  done
-
-lemma zdvd_dvd_eq: assumes "a \<noteq> 0" and "(a::int) dvd b" and "b dvd a" 
-  shows "\<bar>a\<bar> = \<bar>b\<bar>"
-proof-
-  from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast 
-  from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast 
-  from k k' have "a = a*k*k'" by simp
-  with mult_cancel_left1[where c="a" and b="k*k'"]
-  have kk':"k*k' = 1" using `a\<noteq>0` by (simp add: mult_assoc)
-  hence "k = 1 \<and> k' = 1 \<or> k = -1 \<and> k' = -1" by (simp add: zmult_eq_1_iff)
-  thus ?thesis using k k' by auto
-qed
-
-lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
-  apply (subgoal_tac "m = n + (m - n)")
-   apply (erule ssubst)
-   apply (blast intro: dvd_add, simp)
-  done
-
-lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
-apply (rule iffI)
- apply (erule_tac [2] dvd_add)
- apply (subgoal_tac "n = (n + k * m) - k * m")
-  apply (erule ssubst)
-  apply (erule dvd_diff)
-  apply(simp_all)
-done
-
 lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"
   by (rule dvd_mod) (* TODO: remove *)
 
 lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
   by (rule dvd_mod_imp_dvd) (* TODO: remove *)
 
-lemma dvd_imp_le_int: "(i::int) ~= 0 ==> d dvd i ==> abs d <= abs i"
-apply(auto simp:abs_if)
-   apply(clarsimp simp:dvd_def mult_less_0_iff)
-  using mult_le_cancel_left_neg[of _ "-1::int"]
-  apply(clarsimp simp:dvd_def mult_less_0_iff)
- apply(clarsimp simp:dvd_def mult_less_0_iff
-         minus_mult_right simp del: mult_minus_right)
-apply(clarsimp simp:dvd_def mult_less_0_iff)
-done
-
-lemma zdvd_not_zless: "0 < m ==> m < n ==> \<not> n dvd (m::int)"
-  apply (auto elim!: dvdE)
-  apply (subgoal_tac "0 < n")
-   prefer 2
-   apply (blast intro: order_less_trans)
-  apply (simp add: zero_less_mult_iff)
-  done
-
 lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)"
   using zmod_zdiv_equality[where a="m" and b="n"]
   by (simp add: algebra_simps)
 
-lemma zdvd_mult_div_cancel:"(n::int) dvd m \<Longrightarrow> n * (m div n) = m"
-apply (subgoal_tac "m mod n = 0")
- apply (simp add: zmult_div_cancel)
-apply (simp only: dvd_eq_mod_eq_0)
-done
-
-lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \<noteq> (0::int)"
-  shows "m dvd n"
-proof-
-  from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast
-  {assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp
-    with h have False by (simp add: mult_assoc)}
-  hence "n = m * h" by blast
-  thus ?thesis by simp
-qed
-
-theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
-proof -
-  have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y"
-  proof -
-    fix k
-    assume A: "int y = int x * k"
-    then show "x dvd y" proof (cases k)
-      case (1 n) with A have "y = x * n" by (simp add: zmult_int)
-      then show ?thesis ..
-    next
-      case (2 n) with A have "int y = int x * (- int (Suc n))" by simp
-      also have "\<dots> = - (int x * int (Suc n))" by (simp only: mult_minus_right)
-      also have "\<dots> = - int (x * Suc n)" by (simp only: zmult_int)
-      finally have "- int (x * Suc n) = int y" ..
-      then show ?thesis by (simp only: negative_eq_positive) auto
-    qed
-  qed
-  then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left int_mult)
-qed
-
-lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
-proof
-  assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp
-  hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)
-  hence "nat \<bar>x\<bar> = 1"  by simp
-  thus "\<bar>x\<bar> = 1" by (cases "x < 0", auto)
-next
-  assume "\<bar>x\<bar>=1" thus "x dvd 1" 
-    by(cases "x < 0",simp_all add: minus_equation_iff dvd_eq_mod_eq_0)
-qed
-lemma zdvd_mult_cancel1: 
-  assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)"
-proof
-  assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m" 
-    by (cases "n >0", auto simp add: minus_dvd_iff minus_equation_iff)
-next
-  assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp
-  from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
-qed
-
-lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
-  unfolding zdvd_int by (cases "z \<ge> 0") simp_all
-
-lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
-  unfolding zdvd_int by (cases "z \<ge> 0") simp_all
-
-lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
-  by (auto simp add: dvd_int_iff)
-
-lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
-  apply (rule_tac z=n in int_cases)
-  apply (auto simp add: dvd_int_iff)
-  apply (rule_tac z=z in int_cases)
-  apply (auto simp add: dvd_imp_le)
-  done
-
 lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m"
 apply (induct "y", auto)
 apply (rule zmod_zmult1_eq [THEN trans])
@@ -1182,6 +1059,12 @@
 lemma abs_div: "(y::int) dvd x \<Longrightarrow> abs (x div y) = abs x div abs y"
 by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)
 
+lemma zdvd_mult_div_cancel:"(n::int) dvd m \<Longrightarrow> n * (m div n) = m"
+apply (subgoal_tac "m mod n = 0")
+ apply (simp add: zmult_div_cancel)
+apply (simp only: dvd_eq_mod_eq_0)
+done
+
 text{*Suggested by Matthias Daum*}
 lemma int_power_div_base:
      "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)"
@@ -1349,6 +1232,43 @@
 declare dvd_eq_mod_eq_0_number_of [simp]
 
 
+subsection {* Transfer setup *}
+
+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 TransferMorphism_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 TransferMorphism_int_nat[transfer add return:
+  transfer_int_nat_functions
+  transfer_int_nat_function_closures
+]
+
+
 subsection {* Code generation *}
 
 definition pdivmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
diff -r dfda74619509 -r ddd97d9dfbfb src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Oct 29 08:14:39 2009 +0100
+++ b/src/HOL/IsaMakefile	Thu Oct 29 11:41:36 2009 +0100
@@ -223,7 +223,6 @@
   Tools/sat_funcs.ML \
   Tools/sat_solver.ML \
   Tools/split_rule.ML \
-  Tools/transfer.ML \
   Tools/typecopy.ML \
   Tools/typedef_codegen.ML \
   Tools/typedef.ML \
@@ -255,6 +254,7 @@
   Main.thy \
   Map.thy \
   Nat_Numeral.thy \
+  Nat_Transfer.thy \
   Presburger.thy \
   Predicate_Compile.thy \
   Quickcheck.thy \
@@ -276,6 +276,7 @@
   Tools/Groebner_Basis/misc.ML \
   Tools/Groebner_Basis/normalizer.ML \
   Tools/Groebner_Basis/normalizer_data.ML \
+  Tools/choice_specification.ML \
   Tools/int_arith.ML \
   Tools/list_code.ML \
   Tools/meson.ML \
@@ -299,7 +300,6 @@
   Tools/Qelim/presburger.ML \
   Tools/Qelim/qelim.ML \
   Tools/recdef.ML \
-  Tools/choice_specification.ML \
   Tools/res_atp.ML \
   Tools/res_axioms.ML \
   Tools/res_clause.ML \
@@ -307,6 +307,7 @@
   Tools/res_reconstruct.ML \
   Tools/string_code.ML \
   Tools/string_syntax.ML \
+  Tools/transfer.ML \
   Tools/TFL/casesplit.ML \
   Tools/TFL/dcterm.ML \
   Tools/TFL/post.ML \
@@ -334,7 +335,6 @@
   Log.thy \
   Lubs.thy \
   MacLaurin.thy \
-  Nat_Transfer.thy \
   NthRoot.thy \
   PReal.thy \
   Parity.thy \
diff -r dfda74619509 -r ddd97d9dfbfb src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Oct 29 08:14:39 2009 +0100
+++ b/src/HOL/List.thy	Thu Oct 29 11:41:36 2009 +0100
@@ -3587,8 +3587,8 @@
 by (blast intro: listrel.intros)
 
 lemma listrel_Cons:
-     "listrel r `` {x#xs} = set_Cons (r``{x}) (listrel r `` {xs})";
-by (auto simp add: set_Cons_def intro: listrel.intros) 
+     "listrel r `` {x#xs} = set_Cons (r``{x}) (listrel r `` {xs})"
+by (auto simp add: set_Cons_def intro: listrel.intros)
 
 
 subsection {* Size function *}
@@ -3615,6 +3615,45 @@
 by (induct xs) force+
 
 
+subsection {* Transfer *}
+
+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: "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:
+  "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";
+*)
+
+
 subsection {* Code generator *}
 
 subsubsection {* Setup *}
@@ -4017,5 +4056,4 @@
   "list_ex P [i..j] = (~ all_from_to_int (%x. ~P x) i j)"
 by(simp add: all_from_to_int_iff_ball list_ex_iff)
 
-
 end
diff -r dfda74619509 -r ddd97d9dfbfb src/HOL/Nat_Transfer.thy
--- a/src/HOL/Nat_Transfer.thy	Thu Oct 29 08:14:39 2009 +0100
+++ b/src/HOL/Nat_Transfer.thy	Thu Oct 29 11:41:36 2009 +0100
@@ -1,15 +1,26 @@
 
 (* Authors: Jeremy Avigad and Amine Chaieb *)
 
-header {* Sets up transfer from nats to ints and back. *}
+header {* Generic transfer machinery;  specific transfer from nats to ints and back. *}
 
 theory Nat_Transfer
-imports Main Parity
+imports Nat_Numeral
+uses ("Tools/transfer.ML")
 begin
 
+subsection {* Generic transfer machinery *}
+
+definition TransferMorphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
+  where "TransferMorphism a B \<longleftrightarrow> True"
+
+use "Tools/transfer.ML"
+
+setup Transfer.setup
+
+
 subsection {* Set up transfer from nat to int *}
 
-(* set up transfer direction *)
+text {* set up transfer direction *}
 
 lemma TransferMorphism_nat_int: "TransferMorphism nat (op <= (0::int))"
   by (simp add: TransferMorphism_def)
@@ -20,7 +31,7 @@
   labels: natint
 ]
 
-(* basic functions and relations *)
+text {* basic functions and relations *}
 
 lemma transfer_nat_int_numerals:
     "(0::nat) = nat 0"
@@ -43,31 +54,20 @@
     "(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 nat_div_distrib nat_mod_distrib tsub_def)
+      nat_power_eq tsub_def)
 
 lemma transfer_nat_int_function_closures:
     "(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"
-    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
-    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
     "(0::int) >= 0"
     "(1::int) >= 0"
     "(2::int) >= 0"
     "(3::int) >= 0"
     "int z >= 0"
   apply (auto simp add: zero_le_mult_iff tsub_def)
-  apply (case_tac "y = 0")
-  apply auto
-  apply (subst pos_imp_zdiv_nonneg_iff, auto)
-  apply (case_tac "y = 0")
-  apply force
-  apply (rule pos_mod_sign)
-  apply arith
 done
 
 lemma transfer_nat_int_relations:
@@ -89,7 +89,21 @@
 ]
 
 
-(* first-order quantifiers *)
+text {* first-order quantifiers *}
+
+lemma all_nat: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x\<ge>0. P (nat x))"
+  by (simp split add: split_nat)
+
+lemma ex_nat: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> P (nat x))"
+proof
+  assume "\<exists>x. P x"
+  then obtain x where "P x" ..
+  then have "int x \<ge> 0 \<and> P (nat (int x))" by simp
+  then show "\<exists>x\<ge>0. P (nat x)" ..
+next
+  assume "\<exists>x\<ge>0. P (nat x)"
+  then show "\<exists>x. P x" by auto
+qed
 
 lemma transfer_nat_int_quantifiers:
     "(ALL (x::nat). P x) = (ALL (x::int). x >= 0 \<longrightarrow> P (nat x))"
@@ -110,7 +124,7 @@
   cong: all_cong ex_cong]
 
 
-(* if *)
+text {* if *}
 
 lemma nat_if_cong: "(if P then (nat x) else (nat y)) =
     nat (if P then x else y)"
@@ -119,7 +133,7 @@
 declare TransferMorphism_nat_int [transfer add return: nat_if_cong]
 
 
-(* operations with sets *)
+text {* operations with sets *}
 
 definition
   nat_set :: "int set \<Rightarrow> bool"
@@ -132,8 +146,6 @@
     "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! *)
   apply (rule card_image [symmetric])
   apply (auto simp add: inj_on_def image_def)
   apply (rule_tac x = "int x" in bexI)
@@ -144,17 +156,12 @@
   apply auto
   apply (rule_tac x = "int x" in exI)
   apply auto
-  apply (rule_tac x = "int x" in bexI)
-  apply auto
-  apply (rule_tac x = "int x" in bexI)
-  apply auto
 done
 
 lemma transfer_nat_int_set_function_closures:
     "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)"
-    "x >= 0 \<Longrightarrow> nat_set {x..y}"
     "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? *)
@@ -167,7 +174,6 @@
     "(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)
@@ -194,7 +200,7 @@
 ]
 
 
-(* setsum and setprod *)
+text {* setsum and setprod *}
 
 (* this handles the case where the *domain* of f is nat *)
 lemma transfer_nat_int_sum_prod:
@@ -262,52 +268,10 @@
     transfer_nat_int_sum_prod_closure
   cong: transfer_nat_int_sum_prod_cong]
 
-(* lists *)
-
-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";
-
-thm nat_0_le;
-
-lemma transfer_nat_int_list_return_embed: "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:
-  "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";
-*)
-
-
-
 
 subsection {* Set up transfer from int to nat *}
 
-(* set up transfer direction *)
+text {* set up transfer direction *}
 
 lemma TransferMorphism_int_nat: "TransferMorphism int (UNIV :: nat set)"
   by (simp add: TransferMorphism_def)
@@ -319,7 +283,11 @@
 ]
 
 
-(* basic functions and relations *)
+text {* basic functions and relations *}
+
+lemma UNIV_apply:
+  "UNIV x = True"
+  by (simp add: top_fun_eq top_bool_eq)
 
 definition
   is_nat :: "int \<Rightarrow> bool"
@@ -338,17 +306,13 @@
     "(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: int_mult tsub_def int_power zdiv_int zmod_int)
+  by (auto simp add: int_mult tsub_def int_power)
 
 lemma transfer_int_nat_function_closures:
     "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 x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
-    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
     "is_nat 0"
     "is_nat 1"
     "is_nat 2"
@@ -361,12 +325,7 @@
     "(int x < int y) = (x < y)"
     "(int x <= int y) = (x <= y)"
     "(int x dvd int y) = (x dvd y)"
-    "(even (int x)) = (even x)"
-  by (auto simp add: zdvd_int even_nat_def)
-
-lemma UNIV_apply:
-  "UNIV x = True"
-  by (simp add: top_fun_eq top_bool_eq)
+  by (auto simp add: zdvd_int)
 
 declare TransferMorphism_int_nat[transfer add return:
   transfer_int_nat_numerals
@@ -377,7 +336,7 @@
 ]
 
 
-(* first-order quantifiers *)
+text {* first-order quantifiers *}
 
 lemma transfer_int_nat_quantifiers:
     "(ALL (x::int) >= 0. P x) = (ALL (x::nat). P (int x))"
@@ -392,7 +351,7 @@
   return: transfer_int_nat_quantifiers]
 
 
-(* if *)
+text {* if *}
 
 lemma int_if_cong: "(if P then (int x) else (int y)) =
     int (if P then x else y)"
@@ -402,7 +361,7 @@
 
 
 
-(* operations with sets *)
+text {* operations with sets *}
 
 lemma transfer_int_nat_set_functions:
     "nat_set A \<Longrightarrow> card A = card (nat ` A)"
@@ -410,7 +369,6 @@
     "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
@@ -421,7 +379,6 @@
     "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)"
-    "is_nat x \<Longrightarrow> nat_set {x..y}"
     "nat_set {x. x >= 0 & P x}"
     "nat_set (int ` C)"
     "nat_set A \<Longrightarrow> x : A \<Longrightarrow> is_nat x"
@@ -454,7 +411,7 @@
 ]
 
 
-(* setsum and setprod *)
+text {* setsum and setprod *}
 
 (* this handles the case where the *domain* of f is int *)
 lemma transfer_int_nat_sum_prod:
diff -r dfda74619509 -r ddd97d9dfbfb src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Thu Oct 29 08:14:39 2009 +0100
+++ b/src/HOL/Parity.thy	Thu Oct 29 11:41:36 2009 +0100
@@ -28,6 +28,13 @@
 
 end
 
+lemma transfer_int_nat_relations:
+  "even (int x) \<longleftrightarrow> even x"
+  by (simp add: even_nat_def)
+
+declare TransferMorphism_int_nat[transfer add return:
+  transfer_int_nat_relations
+]
 
 lemma even_zero_int[simp]: "even (0::int)" by presburger
 
@@ -310,6 +317,8 @@
 
 subsection {* General Lemmas About Division *}
 
+(*FIXME move to Divides.thy*)
+
 lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1" 
 apply (induct "m")
 apply (simp_all add: mod_Suc)
diff -r dfda74619509 -r ddd97d9dfbfb src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Thu Oct 29 08:14:39 2009 +0100
+++ b/src/HOL/Presburger.thy	Thu Oct 29 11:41:36 2009 +0100
@@ -385,20 +385,6 @@
 
 text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*}
 
-lemma all_nat: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x\<ge>0. P (nat x))"
-  by (simp split add: split_nat)
-
-lemma ex_nat: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> P (nat x))"
-proof
-  assume "\<exists>x. P x"
-  then obtain x where "P x" ..
-  then have "int x \<ge> 0 \<and> P (nat (int x))" by simp
-  then show "\<exists>x\<ge>0. P (nat x)" ..
-next
-  assume "\<exists>x\<ge>0. P (nat x)"
-  then show "\<exists>x. P x" by auto
-qed
-
 lemma zdiff_int_split: "P (int (x - y)) =
   ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
   by (case_tac "y \<le> x", simp_all add: zdiff_int)
diff -r dfda74619509 -r ddd97d9dfbfb src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Thu Oct 29 08:14:39 2009 +0100
+++ b/src/HOL/SetInterval.thy	Thu Oct 29 11:41:36 2009 +0100
@@ -9,7 +9,7 @@
 header {* Set intervals *}
 
 theory SetInterval
-imports Int
+imports Int Nat_Transfer
 begin
 
 context ord
@@ -1150,4 +1150,41 @@
   "\<Prod>i\<le>n. t" == "CONST setprod (\<lambda>i. t) {..n}"
   "\<Prod>i<n. t" == "CONST setprod (\<lambda>i. t) {..<n}"
 
+subsection {* Transfer setup *}
+
+lemma transfer_nat_int_set_functions:
+    "{..n} = nat ` {0..int n}"
+    "{m..n} = nat ` {int m..int n}"  (* need all variants of these! *)
+  apply (auto simp add: image_def)
+  apply (rule_tac x = "int x" in bexI)
+  apply auto
+  apply (rule_tac x = "int x" in bexI)
+  apply auto
+  done
+
+lemma transfer_nat_int_set_function_closures:
+    "x >= 0 \<Longrightarrow> nat_set {x..y}"
+  by (simp add: nat_set_def)
+
+declare TransferMorphism_nat_int[transfer add
+  return: transfer_nat_int_set_functions
+    transfer_nat_int_set_function_closures
+]
+
+lemma transfer_int_nat_set_functions:
+    "is_nat m \<Longrightarrow> is_nat n \<Longrightarrow> {m..n} = int ` {nat m..nat n}"
+  by (simp 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:
+    "is_nat x \<Longrightarrow> nat_set {x..y}"
+  by (simp only: transfer_nat_int_set_function_closures is_nat_def)
+
+declare TransferMorphism_int_nat[transfer add
+  return: transfer_int_nat_set_functions
+    transfer_int_nat_set_function_closures
+]
+
 end