# HG changeset patch
# User haftmann
# Date 1252652726 -7200
# Node ID fdbfa0e35e786df6d3565d568af3b5fa5bcf895b
# Parent  4d4ee06e9420713aa84a7e5c9d5c2f5255c480af# Parent  c83dab2c598885590fad1cec796c29f6d6bc6b54
merged

diff -r 4d4ee06e9420 -r fdbfa0e35e78 src/HOL/Fact.thy
--- a/src/HOL/Fact.thy	Thu Sep 10 16:16:18 2009 +0200
+++ b/src/HOL/Fact.thy	Fri Sep 11 09:05:26 2009 +0200
@@ -8,7 +8,7 @@
 header{*Factorial Function*}
 
 theory Fact
-imports NatTransfer
+imports Nat_Transfer
 begin
 
 class fact =
diff -r 4d4ee06e9420 -r fdbfa0e35e78 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Thu Sep 10 16:16:18 2009 +0200
+++ b/src/HOL/Fun.thy	Fri Sep 11 09:05:26 2009 +0200
@@ -7,6 +7,7 @@
 
 theory Fun
 imports Complete_Lattice
+uses ("Tools/transfer.ML")
 begin
 
 text{*As a simplification rule, it replaces all function equalities by
@@ -568,6 +569,16 @@
 *}
 
 
+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 4d4ee06e9420 -r fdbfa0e35e78 src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Thu Sep 10 16:16:18 2009 +0200
+++ b/src/HOL/IntDiv.thy	Fri Sep 11 09:05:26 2009 +0200
@@ -1102,20 +1102,6 @@
   thus ?thesis by simp
 qed
 
-
-theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
-apply (simp split add: split_nat)
-apply (rule iffI)
-apply (erule exE)
-apply (rule_tac x = "int x" in exI)
-apply simp
-apply (erule exE)
-apply (rule_tac x = "nat x" in exI)
-apply (erule conjE)
-apply (erule_tac x = "nat x" in allE)
-apply simp
-done
-
 theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
 proof -
   have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y"
diff -r 4d4ee06e9420 -r fdbfa0e35e78 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Sep 10 16:16:18 2009 +0200
+++ b/src/HOL/IsaMakefile	Fri Sep 11 09:05:26 2009 +0200
@@ -291,7 +291,7 @@
   Log.thy \
   Lubs.thy \
   MacLaurin.thy \
-  NatTransfer.thy \
+  Nat_Transfer.thy \
   NthRoot.thy \
   SEQ.thy \
   Series.thy \
@@ -306,7 +306,7 @@
   Real.thy \
   RealVector.thy \
   Tools/float_syntax.ML \
-  Tools/transfer_data.ML \
+  Tools/transfer.ML \
   Tools/Qelim/ferrante_rackoff_data.ML \
   Tools/Qelim/ferrante_rackoff.ML \
   Tools/Qelim/langford_data.ML \
@@ -901,7 +901,7 @@
   ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy		\
   ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy \
   ex/Sudoku.thy ex/Tarski.thy \
-  ex/Termination.thy ex/Unification.thy ex/document/root.bib		\
+  ex/Termination.thy ex/Transfer_Ex.thy ex/Unification.thy ex/document/root.bib		\
   ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy \
   ex/Predicate_Compile.thy ex/predicate_compile.ML ex/Predicate_Compile_ex.thy
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
diff -r 4d4ee06e9420 -r fdbfa0e35e78 src/HOL/NatTransfer.thy
--- a/src/HOL/NatTransfer.thy	Thu Sep 10 16:16:18 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,537 +0,0 @@
-(*  Title:      HOL/Library/NatTransfer.thy
-    Authors:    Jeremy Avigad and Amine Chaieb
-
-    Sets up transfer from nats to ints and
-    back.
-*)
-
-
-header {* NatTransfer *}
-
-theory NatTransfer
-imports Main Parity
-uses ("Tools/transfer_data.ML")
-begin
-
-subsection {* A transfer Method between isomorphic domains*}
-
-definition TransferMorphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
-  where "TransferMorphism a B = True"
-
-use "Tools/transfer_data.ML"
-
-setup TransferData.setup
-
-
-subsection {* Set up transfer from nat to int *}
-
-(* set up transfer direction *)
-
-lemma TransferMorphism_nat_int: "TransferMorphism nat (op <= (0::int))"
-  by (simp add: TransferMorphism_def)
-
-declare TransferMorphism_nat_int[transfer
-  add mode: manual
-  return: nat_0_le
-  labels: natint
-]
-
-(* basic functions and relations *)
-
-lemma transfer_nat_int_numerals:
-    "(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:
-    "(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 nat_div_distrib nat_mod_distrib 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:
-    "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 even_nat_def)
-
-declare TransferMorphism_nat_int[transfer add return:
-  transfer_nat_int_numerals
-  transfer_nat_int_functions
-  transfer_nat_int_function_closures
-  transfer_nat_int_relations
-]
-
-
-(* first-order quantifiers *)
-
-lemma transfer_nat_int_quantifiers:
-    "(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)
-
-(* should we restrict these? *)
-lemma all_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
-    (ALL x. Q x \<longrightarrow> P x) = (ALL x. Q x \<longrightarrow> P' x)"
-  by auto
-
-lemma ex_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
-    (EX x. Q x \<and> P x) = (EX x. Q x \<and> P' x)"
-  by auto
-
-declare TransferMorphism_nat_int[transfer add
-  return: transfer_nat_int_quantifiers
-  cong: all_cong ex_cong]
-
-
-(* if *)
-
-lemma nat_if_cong: "(if P then (nat x) else (nat y)) =
-    nat (if P then x else y)"
-  by auto
-
-declare TransferMorphism_nat_int [transfer add return: nat_if_cong]
-
-
-(* operations with sets *)
-
-definition
-  nat_set :: "int set \<Rightarrow> bool"
-where
-  "nat_set S = (ALL x:S. x >= 0)"
-
-lemma transfer_nat_int_set_functions:
-    "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! *)
-  apply (rule card_image [symmetric])
-  apply (auto simp add: inj_on_def image_def)
-  apply (rule_tac x = "int x" in bexI)
-  apply auto
-  apply (rule_tac x = "int x" in bexI)
-  apply auto
-  apply (rule_tac x = "int x" in bexI)
-  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? *)
-  unfolding nat_set_def apply auto
-done
-
-lemma transfer_nat_int_set_relations:
-    "(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 expand_set_eq 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: "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>
-    {(x::int). x >= 0 & P x} = {x. x >= 0 & P' x}"
-  by auto
-
-declare TransferMorphism_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
-]
-
-
-(* setsum and setprod *)
-
-(* this handles the case where the *domain* of f is nat *)
-lemma transfer_nat_int_sum_prod:
-    "setsum f A = setsum (%x. f (nat x)) (int ` A)"
-    "setprod f A = setprod (%x. f (nat x)) (int ` A)"
-  apply (subst setsum_reindex)
-  apply (unfold inj_on_def, auto)
-  apply (subst setprod_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:
-    "setsum f A = nat(setsum (%x. int (f x)) A)"
-    "setprod f A = nat(setprod (%x. int (f x)) A)"
-  apply (subst int_setsum [symmetric])
-  apply auto
-  apply (subst int_setprod [symmetric])
-  apply auto
-done
-
-lemma transfer_nat_int_sum_prod_closure:
-    "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setsum f A >= 0"
-    "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0"
-  unfolding nat_set_def
-  apply (rule setsum_nonneg)
-  apply auto
-  apply (rule setprod_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> setsum f A >= 0"
-    "(!!x. x : A  ==> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0"
-  unfolding nat_set_def simp_implies_def
-  apply (rule setsum_nonneg)
-  apply auto
-  apply (rule setprod_nonneg)
-  apply auto
-done
-*)
-
-(* Making A = B in this lemma doesn't work. Why not?
-   Also, why aren't setsum_cong and setprod_cong enough,
-   with the previously mentioned rule turned on? *)
-
-lemma transfer_nat_int_sum_prod_cong:
-    "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
-      setsum f A = setsum g B"
-    "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
-      setprod f A = setprod g B"
-  unfolding nat_set_def
-  apply (subst setsum_cong, assumption)
-  apply auto [2]
-  apply (subst setprod_cong, assumption, auto)
-done
-
-declare TransferMorphism_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]
-
-(* 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 *)
-
-lemma TransferMorphism_int_nat: "TransferMorphism int (UNIV :: nat set)"
-  by (simp add: TransferMorphism_def)
-
-declare TransferMorphism_int_nat[transfer add
-  mode: manual
-(*  labels: int-nat *)
-  return: nat_int
-]
-
-
-(* basic functions and relations *)
-
-definition
-  is_nat :: "int \<Rightarrow> bool"
-where
-  "is_nat x = (x >= 0)"
-
-lemma transfer_int_nat_numerals:
-    "0 = int 0"
-    "1 = int 1"
-    "2 = int 2"
-    "3 = int 3"
-  by auto
-
-lemma transfer_int_nat_functions:
-    "(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: int_mult tsub_def int_power zdiv_int zmod_int)
-
-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"
-    "is_nat 3"
-    "is_nat (int z)"
-  by (simp_all only: is_nat_def transfer_nat_int_function_closures)
-
-lemma transfer_int_nat_relations:
-    "(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)"
-    "(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)
-
-declare TransferMorphism_int_nat[transfer add return:
-  transfer_int_nat_numerals
-  transfer_int_nat_functions
-  transfer_int_nat_function_closures
-  transfer_int_nat_relations
-  UNIV_apply
-]
-
-
-(* first-order quantifiers *)
-
-lemma transfer_int_nat_quantifiers:
-    "(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 TransferMorphism_int_nat[transfer add
-  return: transfer_int_nat_quantifiers]
-
-
-(* if *)
-
-lemma int_if_cong: "(if P then (int x) else (int y)) =
-    int (if P then x else y)"
-  by auto
-
-declare TransferMorphism_int_nat [transfer add return: int_if_cong]
-
-
-
-(* operations with sets *)
-
-lemma transfer_int_nat_set_functions:
-    "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:
-    "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"
-  by (simp_all only: transfer_nat_int_set_function_closures is_nat_def)
-
-lemma transfer_int_nat_set_relations:
-    "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: "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>
-    {(x::nat). P x} = {x. P' x}"
-  by auto
-
-declare TransferMorphism_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
-]
-
-
-(* setsum and setprod *)
-
-(* this handles the case where the *domain* of f is int *)
-lemma transfer_int_nat_sum_prod:
-    "nat_set A \<Longrightarrow> setsum f A = setsum (%x. f (int x)) (nat ` A)"
-    "nat_set A \<Longrightarrow> setprod f A = setprod (%x. f (int x)) (nat ` A)"
-  apply (subst setsum_reindex)
-  apply (unfold inj_on_def nat_set_def, auto simp add: eq_nat_nat_iff)
-  apply (subst setprod_reindex)
-  apply (unfold inj_on_def nat_set_def o_def, auto simp add: eq_nat_nat_iff
-            cong: setprod_cong)
-done
-
-(* this handles the case where the *range* of f is int *)
-lemma transfer_int_nat_sum_prod2:
-    "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow> setsum f A = int(setsum (%x. nat (f x)) A)"
-    "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow>
-      setprod f A = int(setprod (%x. nat (f x)) A)"
-  unfolding is_nat_def
-  apply (subst int_setsum, auto)
-  apply (subst int_setprod, auto simp add: cong: setprod_cong)
-done
-
-declare TransferMorphism_int_nat[transfer add
-  return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
-  cong: setsum_cong setprod_cong]
-
-
-subsection {* Test it out *}
-
-(* nat to int *)
-
-lemma ex1: "(x::nat) + y = y + x"
-  by auto
-
-thm ex1 [transferred]
-
-lemma ex2: "(a::nat) div b * b + a mod b = a"
-  by (rule mod_div_equality)
-
-thm ex2 [transferred]
-
-lemma ex3: "ALL (x::nat). ALL y. EX z. z >= x + y"
-  by auto
-
-thm ex3 [transferred natint]
-
-lemma ex4: "(x::nat) >= y \<Longrightarrow> (x - y) + y = x"
-  by auto
-
-thm ex4 [transferred]
-
-lemma ex5: "(2::nat) * (SUM i <= n. i) = n * (n + 1)"
-  by (induct n rule: nat_induct, auto)
-
-thm ex5 [transferred]
-
-theorem ex6: "0 <= (n::int) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
-  by (rule ex5 [transferred])
-
-thm ex6 [transferred]
-
-thm ex5 [transferred, transferred]
-
-end
diff -r 4d4ee06e9420 -r fdbfa0e35e78 src/HOL/Nat_Transfer.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nat_Transfer.thy	Fri Sep 11 09:05:26 2009 +0200
@@ -0,0 +1,484 @@
+
+(* Authors: Jeremy Avigad and Amine Chaieb *)
+
+header {* Sets up transfer from nats to ints and back. *}
+
+theory Nat_Transfer
+imports Main Parity
+begin
+
+subsection {* Set up transfer from nat to int *}
+
+(* set up transfer direction *)
+
+lemma TransferMorphism_nat_int: "TransferMorphism nat (op <= (0::int))"
+  by (simp add: TransferMorphism_def)
+
+declare TransferMorphism_nat_int[transfer
+  add mode: manual
+  return: nat_0_le
+  labels: natint
+]
+
+(* basic functions and relations *)
+
+lemma transfer_nat_int_numerals:
+    "(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:
+    "(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 nat_div_distrib nat_mod_distrib 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:
+    "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)
+
+declare TransferMorphism_nat_int[transfer add return:
+  transfer_nat_int_numerals
+  transfer_nat_int_functions
+  transfer_nat_int_function_closures
+  transfer_nat_int_relations
+]
+
+
+(* first-order quantifiers *)
+
+lemma transfer_nat_int_quantifiers:
+    "(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)
+
+(* should we restrict these? *)
+lemma all_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
+    (ALL x. Q x \<longrightarrow> P x) = (ALL x. Q x \<longrightarrow> P' x)"
+  by auto
+
+lemma ex_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
+    (EX x. Q x \<and> P x) = (EX x. Q x \<and> P' x)"
+  by auto
+
+declare TransferMorphism_nat_int[transfer add
+  return: transfer_nat_int_quantifiers
+  cong: all_cong ex_cong]
+
+
+(* if *)
+
+lemma nat_if_cong: "(if P then (nat x) else (nat y)) =
+    nat (if P then x else y)"
+  by auto
+
+declare TransferMorphism_nat_int [transfer add return: nat_if_cong]
+
+
+(* operations with sets *)
+
+definition
+  nat_set :: "int set \<Rightarrow> bool"
+where
+  "nat_set S = (ALL x:S. x >= 0)"
+
+lemma transfer_nat_int_set_functions:
+    "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! *)
+  apply (rule card_image [symmetric])
+  apply (auto simp add: inj_on_def image_def)
+  apply (rule_tac x = "int x" in bexI)
+  apply auto
+  apply (rule_tac x = "int x" in bexI)
+  apply auto
+  apply (rule_tac x = "int x" in bexI)
+  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? *)
+  unfolding nat_set_def apply auto
+done
+
+lemma transfer_nat_int_set_relations:
+    "(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 expand_set_eq 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: "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>
+    {(x::int). x >= 0 & P x} = {x. x >= 0 & P' x}"
+  by auto
+
+declare TransferMorphism_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
+]
+
+
+(* setsum and setprod *)
+
+(* this handles the case where the *domain* of f is nat *)
+lemma transfer_nat_int_sum_prod:
+    "setsum f A = setsum (%x. f (nat x)) (int ` A)"
+    "setprod f A = setprod (%x. f (nat x)) (int ` A)"
+  apply (subst setsum_reindex)
+  apply (unfold inj_on_def, auto)
+  apply (subst setprod_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:
+    "setsum f A = nat(setsum (%x. int (f x)) A)"
+    "setprod f A = nat(setprod (%x. int (f x)) A)"
+  apply (subst int_setsum [symmetric])
+  apply auto
+  apply (subst int_setprod [symmetric])
+  apply auto
+done
+
+lemma transfer_nat_int_sum_prod_closure:
+    "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setsum f A >= 0"
+    "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0"
+  unfolding nat_set_def
+  apply (rule setsum_nonneg)
+  apply auto
+  apply (rule setprod_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> setsum f A >= 0"
+    "(!!x. x : A  ==> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0"
+  unfolding nat_set_def simp_implies_def
+  apply (rule setsum_nonneg)
+  apply auto
+  apply (rule setprod_nonneg)
+  apply auto
+done
+*)
+
+(* Making A = B in this lemma doesn't work. Why not?
+   Also, why aren't setsum_cong and setprod_cong enough,
+   with the previously mentioned rule turned on? *)
+
+lemma transfer_nat_int_sum_prod_cong:
+    "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
+      setsum f A = setsum g B"
+    "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
+      setprod f A = setprod g B"
+  unfolding nat_set_def
+  apply (subst setsum_cong, assumption)
+  apply auto [2]
+  apply (subst setprod_cong, assumption, auto)
+done
+
+declare TransferMorphism_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]
+
+(* 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 *)
+
+lemma TransferMorphism_int_nat: "TransferMorphism int (UNIV :: nat set)"
+  by (simp add: TransferMorphism_def)
+
+declare TransferMorphism_int_nat[transfer add
+  mode: manual
+(*  labels: int-nat *)
+  return: nat_int
+]
+
+
+(* basic functions and relations *)
+
+definition
+  is_nat :: "int \<Rightarrow> bool"
+where
+  "is_nat x = (x >= 0)"
+
+lemma transfer_int_nat_numerals:
+    "0 = int 0"
+    "1 = int 1"
+    "2 = int 2"
+    "3 = int 3"
+  by auto
+
+lemma transfer_int_nat_functions:
+    "(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: int_mult tsub_def int_power zdiv_int zmod_int)
+
+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"
+    "is_nat 3"
+    "is_nat (int z)"
+  by (simp_all only: is_nat_def transfer_nat_int_function_closures)
+
+lemma transfer_int_nat_relations:
+    "(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)"
+    "(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)
+
+declare TransferMorphism_int_nat[transfer add return:
+  transfer_int_nat_numerals
+  transfer_int_nat_functions
+  transfer_int_nat_function_closures
+  transfer_int_nat_relations
+  UNIV_apply
+]
+
+
+(* first-order quantifiers *)
+
+lemma transfer_int_nat_quantifiers:
+    "(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 TransferMorphism_int_nat[transfer add
+  return: transfer_int_nat_quantifiers]
+
+
+(* if *)
+
+lemma int_if_cong: "(if P then (int x) else (int y)) =
+    int (if P then x else y)"
+  by auto
+
+declare TransferMorphism_int_nat [transfer add return: int_if_cong]
+
+
+
+(* operations with sets *)
+
+lemma transfer_int_nat_set_functions:
+    "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:
+    "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"
+  by (simp_all only: transfer_nat_int_set_function_closures is_nat_def)
+
+lemma transfer_int_nat_set_relations:
+    "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: "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>
+    {(x::nat). P x} = {x. P' x}"
+  by auto
+
+declare TransferMorphism_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
+]
+
+
+(* setsum and setprod *)
+
+(* this handles the case where the *domain* of f is int *)
+lemma transfer_int_nat_sum_prod:
+    "nat_set A \<Longrightarrow> setsum f A = setsum (%x. f (int x)) (nat ` A)"
+    "nat_set A \<Longrightarrow> setprod f A = setprod (%x. f (int x)) (nat ` A)"
+  apply (subst setsum_reindex)
+  apply (unfold inj_on_def nat_set_def, auto simp add: eq_nat_nat_iff)
+  apply (subst setprod_reindex)
+  apply (unfold inj_on_def nat_set_def o_def, auto simp add: eq_nat_nat_iff
+            cong: setprod_cong)
+done
+
+(* this handles the case where the *range* of f is int *)
+lemma transfer_int_nat_sum_prod2:
+    "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow> setsum f A = int(setsum (%x. nat (f x)) A)"
+    "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow>
+      setprod f A = int(setprod (%x. nat (f x)) A)"
+  unfolding is_nat_def
+  apply (subst int_setsum, auto)
+  apply (subst int_setprod, auto simp add: cong: setprod_cong)
+done
+
+declare TransferMorphism_int_nat[transfer add
+  return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
+  cong: setsum_cong setprod_cong]
+
+end
diff -r 4d4ee06e9420 -r fdbfa0e35e78 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Thu Sep 10 16:16:18 2009 +0200
+++ b/src/HOL/Presburger.thy	Fri Sep 11 09:05:26 2009 +0200
@@ -382,15 +382,22 @@
 
 lemma uminus_dvd_conv: "(d dvd (t::int)) \<equiv> (-d dvd t)" "(d dvd (t::int)) \<equiv> (d dvd -t)"
   by simp_all
+
 text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*}
-lemma all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))"
+
+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::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
-  apply (auto split add: split_nat)
-  apply (rule_tac x="int x" in exI, simp)
-  apply (rule_tac x = "nat x" in exI,erule_tac x = "nat x" in allE, simp)
-  done
+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))"
diff -r 4d4ee06e9420 -r fdbfa0e35e78 src/HOL/Tools/transfer.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/transfer.ML	Fri Sep 11 09:05:26 2009 +0200
@@ -0,0 +1,241 @@
+(*  Author:     Amine Chaieb, University of Cambridge, 2009
+                Jeremy Avigad, Carnegie Mellon University
+*)
+
+signature TRANSFER =
+sig
+  type data
+  type entry
+  val get: Proof.context -> data
+  val del: attribute
+  val setup: theory -> theory
+end;
+
+structure Transfer : TRANSFER =
+struct
+
+val eq_thm = Thm.eq_thm;
+
+type entry = {inj : thm list, emb : thm list, ret : thm list, cong : thm list,
+  guess : bool, hints : string list}; 
+type data = simpset * (thm * entry) list;
+
+structure Data = GenericDataFun
+(
+  type T = data;
+  val empty = (HOL_ss, []);
+  val extend  = I;
+  fun merge _ ((ss1, e1), (ss2, e2)) =
+    (merge_ss (ss1, ss2), AList.merge eq_thm (K true) (e1, e2));
+);
+
+val get = Data.get o Context.Proof;
+
+fun del_data key = apsnd (remove (eq_fst eq_thm) (key, []));
+
+val del = Thm.declaration_attribute (Data.map o del_data);
+val add_ss = Thm.declaration_attribute 
+   (fn th => Data.map (fn (ss,data) => (ss addsimps [th], data)));
+
+val del_ss = Thm.declaration_attribute 
+   (fn th => Data.map (fn (ss,data) => (ss delsimps [th], data)));
+
+val transM_pat = (Thm.dest_arg1 o Thm.dest_arg o cprop_of) @{thm TransferMorphism_def};
+
+fun merge_update eq m (k,v) [] = [(k,v)]
+  | merge_update eq m (k,v) ((k',v')::al) = 
+           if eq (k,k') then (k',m (v,v')):: al else (k',v') :: merge_update eq m (k,v) al
+
+fun C f x y = f y x
+
+fun simpset_of_entry injonly {inj = inj, emb = emb, ret = ret, cong = cg, guess = g, hints = hints} = 
+ HOL_ss addsimps inj addsimps (if injonly then [] else emb@ret) addcongs cg;
+
+fun basic_transfer_rule injonly a0 D0 e leave ctxt0 th = 
+ let 
+  val ([a,D], ctxt) = apfst (map Drule.dest_term o snd) (Variable.import true (map Drule.mk_term [a0, D0]) ctxt0)
+  val (aT,bT) = 
+     let val T = typ_of (ctyp_of_term a) 
+     in (Term.range_type T, Term.domain_type T)
+     end
+  val ctxt' = (Variable.declare_term (term_of a) o Variable.declare_term (term_of D) o Variable.declare_thm th) ctxt
+  val ns = filter (fn i => Type.could_unify (snd i, aT) andalso not (fst (fst i) mem_string leave)) (Term.add_vars (prop_of th) [])
+  val (ins, ctxt'') = Variable.variant_fixes (map (fst o fst) ns) ctxt'
+  val cns = map ((cterm_of o ProofContext.theory_of) ctxt'' o Var) ns
+  val cfis = map ((cterm_of o ProofContext.theory_of) ctxt'' o (fn n => Free (n, bT))) ins
+  val cis = map (Thm.capply a) cfis
+  val (hs,ctxt''') = Assumption.add_assumes (map (fn ct => Thm.capply @{cterm "Trueprop"} (Thm.capply D ct)) cfis) ctxt''
+  val th1 = Drule.cterm_instantiate (cns~~ cis) th
+  val th2 = fold (C implies_elim) hs (fold_rev implies_intr (map cprop_of hs) th1)
+  val th3 = Simplifier.asm_full_simplify (Simplifier.context ctxt''' (simpset_of_entry injonly e)) 
+                                         (fold_rev implies_intr (map cprop_of hs) th2)
+in hd (Variable.export ctxt''' ctxt0 [th3]) end;
+
+local
+fun transfer_ruleh a D leave ctxt th = 
+ let val (ss,al) = get ctxt
+     val a0 = cterm_of (ProofContext.theory_of ctxt) a
+     val D0 = cterm_of (ProofContext.theory_of ctxt) D
+     fun h (th', e) = let val (a',D') = (Thm.dest_binop o Thm.dest_arg o cprop_of) th' 
+                 in if a0 aconvc a' andalso D0 aconvc D' then SOME e else NONE
+                 end
+ in case get_first h al of
+      SOME e => basic_transfer_rule false a0 D0 e leave ctxt th
+    | NONE => error "Transfer: corresponding instance not found in context-data"
+ end
+in fun transfer_rule (a,D) leave (gctxt,th) = 
+   (gctxt, transfer_ruleh a D leave (Context.proof_of gctxt) th)
+end;
+
+fun  splits P [] = []
+   | splits P (xxs as (x::xs)) = 
+    let val pss = filter (P x) xxs
+        val qss = filter_out (P x) xxs
+    in if null pss then [qss] else if null qss then [pss] else pss:: splits P qss
+    end
+
+fun all_transfers leave (gctxt,th) = 
+ let 
+  val ctxt = Context.proof_of gctxt
+  val tys = map snd (Term.add_vars (prop_of th) [])
+  val _ = if null tys then error "transfer: Unable to guess instance" else ()
+  val tyss = splits (curry Type.could_unify) tys 
+  val get_ty = typ_of o ctyp_of_term o fst o Thm.dest_binop o Thm.dest_arg o cprop_of
+  val get_aD = Thm.dest_binop o Thm.dest_arg o cprop_of
+  val insts = 
+    map_filter (fn tys => 
+          get_first (fn (k,ss) => if Type.could_unify (hd tys, range_type (get_ty k)) 
+                                  then SOME (get_aD k, ss) 
+                                  else NONE) (snd (get ctxt))) tyss
+  val _ = if null insts then error "Transfer guesser: there were no possible instances, use direction: in order to provide a direction" else ()
+  val ths = map  (fn ((a,D),e) => basic_transfer_rule false a D e leave ctxt th) insts
+  val cth = Conjunction.intr_balanced ths
+ in (gctxt, cth)
+ end;
+
+fun transfer_rule_by_hint ls leave (gctxt,th) = 
+ let 
+  val ctxt = Context.proof_of gctxt
+  val get_aD = Thm.dest_binop o Thm.dest_arg o cprop_of
+  val insts = 
+    map_filter (fn (k,e) => if exists (fn l => l mem_string (#hints e)) ls 
+          then SOME (get_aD k, e) else NONE)
+        (snd (get ctxt))
+  val _ = if null insts then error "Transfer: No labels provided are stored in the context" else ()
+  val ths = map  (fn ((a,D),e) => basic_transfer_rule false a D e leave ctxt th) insts
+  val cth = Conjunction.intr_balanced ths
+ in (gctxt, cth)
+ end;
+
+
+fun transferred_attribute ls NONE leave = 
+         if null ls then all_transfers leave else transfer_rule_by_hint ls leave
+  | transferred_attribute _ (SOME (a,D)) leave = transfer_rule (a,D) leave
+
+                                                    (* Add data to the context *)
+fun gen_merge_entries {inj = inj0, emb = emb0, ret = ret0, cong = cg0, guess = g0, hints = hints0}
+                      ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1}, 
+                       {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2})
+ = 
+ let fun h xs0 xs ys = subtract Thm.eq_thm xs0 (merge Thm.eq_thm (xs,ys)) in
+ {inj = h inj0 inj1 inj2, emb = h emb0 emb1 emb2, 
+  ret = h ret0 ret1 ret2, cong = h cg0 cg1 cg2, guess = g1 andalso g2,
+  hints = subtract (op = : string*string -> bool) hints0 
+            (hints1 union_string hints2)}
+ end;
+
+local
+ val h = curry (merge Thm.eq_thm)
+in
+fun merge_entries ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1}, 
+                   {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2}) = 
+    {inj = h inj1 inj2, emb = h emb1 emb2, ret = h ret1 ret2, cong = h cg1 cg2, guess = g1 andalso g2, hints = hints1 union_string hints2}
+end; 
+
+fun add ((inja,injd), (emba,embd), (reta,retd), (cga,cgd), g, (hintsa, hintsd)) =
+  Thm.declaration_attribute (fn key => fn context => context |> Data.map
+   (fn (ss, al) => 
+     let
+      val _ = ((let val _ = Thm.match (transM_pat, (Thm.dest_arg o cprop_of) key) 
+                in 0 end) 
+                handle MATCH => error "Attribute expected Theorem of the form : TransferMorphism A a B b")
+      val e0 = {inj = inja, emb = emba, ret = reta, cong = cga, guess = g, hints = hintsa}
+      val ed = {inj = injd, emb = embd, ret = retd, cong = cgd, guess = g, hints = hintsd}
+      val entry = 
+        if g then 
+         let val (a0,D0) = (Thm.dest_binop o Thm.dest_arg o cprop_of) key
+             val ctxt0 = ProofContext.init (Thm.theory_of_thm key)
+             val inj' = if null inja then #inj (case AList.lookup eq_thm al key of SOME e => e | NONE => error "Transfer: can not generate return rules on the fly, either add injectivity axiom or force manual mode with mode: manual") 
+                        else inja
+             val ret' = merge Thm.eq_thm (reta,  map (fn th => basic_transfer_rule true a0 D0 {inj = inj', emb = [], ret = [], cong = cga, guess = g, hints = hintsa} [] ctxt0 th RS sym) emba)
+         in {inj = inja, emb = emba, ret = ret', cong = cga, guess = g, hints = hintsa} end 
+        else e0
+    in (ss, merge_update eq_thm (gen_merge_entries ed) (key, entry) al)
+    end));
+
+
+
+(* concrete syntax *)
+
+local
+
+fun keyword k = Scan.lift (Args.$$$ k) >> K ()
+fun keywordC k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
+
+val congN = "cong"
+val injN = "inj"
+val embedN = "embed"
+val returnN = "return"
+val addN = "add"
+val delN = "del"
+val modeN = "mode"
+val automaticN = "automatic"
+val manualN = "manual"
+val directionN = "direction"
+val labelsN = "labels"
+val leavingN = "leaving"
+
+val any_keyword = keywordC congN || keywordC injN || keywordC embedN || keywordC returnN || keywordC directionN || keywordC modeN || keywordC delN || keywordC labelsN || keywordC leavingN
+
+val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat
+val terms = thms >> map Drule.dest_term
+val types = thms >> (Logic.dest_type o HOLogic.dest_Trueprop o prop_of o hd) 
+val name = Scan.lift Args.name
+val names = Scan.repeat (Scan.unless any_keyword name)
+fun optional scan = Scan.optional scan []
+fun optional2 scan = Scan.optional scan ([],[])
+
+val mode = keywordC modeN |-- ((Scan.lift (Args.$$$ manualN) >> K false) || (Scan.lift (Args.$$$ automaticN) >> K true))
+val inj = (keywordC injN |-- thms) -- optional (keywordC delN |-- thms)
+val embed = (keywordC embedN |-- thms) -- optional (keywordC delN |-- thms)
+val return = (keywordC returnN |-- thms) -- optional (keywordC delN |-- thms)
+val cong = (keywordC congN |-- thms) -- optional (keywordC delN |-- thms)
+val addscan = Scan.unless any_keyword (keyword addN)
+val labels = (keywordC labelsN |-- names) -- optional (keywordC delN |-- names)
+val entry = Scan.optional mode true -- optional2 inj -- optional2 embed -- optional2 return -- optional2 cong -- optional2 labels
+
+val transf_add = addscan |-- entry
+in
+
+val install_att_syntax =
+  (Scan.lift (Args.$$$ delN >> K del) ||
+    transf_add
+    >> (fn (((((g, inj), embed), ret), cg), hints) => add (inj, embed, ret, cg, g, hints)))
+
+val transferred_att_syntax = (optional names -- Scan.option (keywordC directionN |-- (Args.term -- Args.term))
+  -- optional (keywordC leavingN |-- names) >> (fn ((hints, aD),leave) => transferred_attribute hints aD leave));
+
+end;
+
+
+(* theory setup *)
+
+val setup =
+  Attrib.setup @{binding transfer} install_att_syntax
+    "Installs transfer data" #>
+  Attrib.setup @{binding transfer_simps} (Attrib.add_del add_ss del_ss)
+    "simp rules for transfer" #>
+  Attrib.setup @{binding transferred} transferred_att_syntax
+    "Transfers theorems";
+
+end;
diff -r 4d4ee06e9420 -r fdbfa0e35e78 src/HOL/Tools/transfer_data.ML
--- a/src/HOL/Tools/transfer_data.ML	Thu Sep 10 16:16:18 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,243 +0,0 @@
-(*  Title:      Tools/transfer.ML
-    Author:     Amine Chaieb, University of Cambridge, 2009
-                Jeremy Avigad, Carnegie Mellon University
-*)
-
-signature TRANSFER_DATA =
-sig
-  type data
-  type entry
-  val get: Proof.context -> data
-  val del: attribute
-  val add: attribute 
-  val setup: theory -> theory
-end;
-
-structure TransferData (* : TRANSFER_DATA*) =
-struct
-type entry = {inj : thm list , emb : thm list , ret : thm list , cong : thm list, guess : bool, hints : string list}; 
-type data = simpset * (thm * entry) list;
-
-val eq_key = Thm.eq_thm;
-fun eq_data arg = eq_fst eq_key arg;
-
-structure Data = GenericDataFun
-(
-  type T = data;
-  val empty = (HOL_ss, []);
-  val extend  = I;
-  fun merge _ ((ss, e), (ss', e')) =
-    (merge_ss (ss, ss'), AList.merge eq_key (K true) (e, e'));
-);
-
-val get = Data.get o Context.Proof;
-
-fun del_data key = apsnd (remove eq_data (key, []));
-
-val del = Thm.declaration_attribute (Data.map o del_data);
-val add_ss = Thm.declaration_attribute 
-   (fn th => Data.map (fn (ss,data) => (ss addsimps [th], data)));
-
-val del_ss = Thm.declaration_attribute 
-   (fn th => Data.map (fn (ss,data) => (ss delsimps [th], data)));
-
-val transM_pat = (Thm.dest_arg1 o Thm.dest_arg o cprop_of) @{thm TransferMorphism_def};
-
-fun merge_update eq m (k,v) [] = [(k,v)]
-  | merge_update eq m (k,v) ((k',v')::al) = 
-           if eq (k,k') then (k',m (v,v')):: al else (k',v') :: merge_update eq m (k,v) al
-
-fun C f x y = f y x
-
-fun simpset_of_entry injonly {inj = inj, emb = emb, ret = ret, cong = cg, guess = g, hints = hints} = 
- HOL_ss addsimps inj addsimps (if injonly then [] else emb@ret) addcongs cg;
-
-fun basic_transfer_rule injonly a0 D0 e leave ctxt0 th = 
- let 
-  val ([a,D], ctxt) = apfst (map Drule.dest_term o snd) (Variable.import true (map Drule.mk_term [a0, D0]) ctxt0)
-  val (aT,bT) = 
-     let val T = typ_of (ctyp_of_term a) 
-     in (Term.range_type T, Term.domain_type T)
-     end
-  val ctxt' = (Variable.declare_term (term_of a) o Variable.declare_term (term_of D) o Variable.declare_thm th) ctxt
-  val ns = filter (fn i => Type.could_unify (snd i, aT) andalso not (fst (fst i) mem_string leave)) (Term.add_vars (prop_of th) [])
-  val (ins, ctxt'') = Variable.variant_fixes (map (fst o fst) ns) ctxt'
-  val cns = map ((cterm_of o ProofContext.theory_of) ctxt'' o Var) ns
-  val cfis = map ((cterm_of o ProofContext.theory_of) ctxt'' o (fn n => Free (n, bT))) ins
-  val cis = map (Thm.capply a) cfis
-  val (hs,ctxt''') = Assumption.add_assumes (map (fn ct => Thm.capply @{cterm "Trueprop"} (Thm.capply D ct)) cfis) ctxt''
-  val th1 = Drule.cterm_instantiate (cns~~ cis) th
-  val th2 = fold (C implies_elim) hs (fold_rev implies_intr (map cprop_of hs) th1)
-  val th3 = Simplifier.asm_full_simplify (Simplifier.context ctxt''' (simpset_of_entry injonly e)) 
-                                         (fold_rev implies_intr (map cprop_of hs) th2)
-in hd (Variable.export ctxt''' ctxt0 [th3]) end;
-
-local
-fun transfer_ruleh a D leave ctxt th = 
- let val (ss,al) = get ctxt
-     val a0 = cterm_of (ProofContext.theory_of ctxt) a
-     val D0 = cterm_of (ProofContext.theory_of ctxt) D
-     fun h (th', e) = let val (a',D') = (Thm.dest_binop o Thm.dest_arg o cprop_of) th' 
-                 in if a0 aconvc a' andalso D0 aconvc D' then SOME e else NONE
-                 end
- in case get_first h al of
-      SOME e => basic_transfer_rule false a0 D0 e leave ctxt th
-    | NONE => error "Transfer: corresponding instance not found in context-data"
- end
-in fun transfer_rule (a,D) leave (gctxt,th) = 
-   (gctxt, transfer_ruleh a D leave (Context.proof_of gctxt) th)
-end;
-
-fun  splits P [] = []
-   | splits P (xxs as (x::xs)) = 
-    let val pss = filter (P x) xxs
-        val qss = filter_out (P x) xxs
-    in if null pss then [qss] else if null qss then [pss] else pss:: splits P qss
-    end
-
-fun all_transfers leave (gctxt,th) = 
- let 
-  val ctxt = Context.proof_of gctxt
-  val tys = map snd (Term.add_vars (prop_of th) [])
-  val _ = if null tys then error "transfer: Unable to guess instance" else ()
-  val tyss = splits (curry Type.could_unify) tys 
-  val get_ty = typ_of o ctyp_of_term o fst o Thm.dest_binop o Thm.dest_arg o cprop_of
-  val get_aD = Thm.dest_binop o Thm.dest_arg o cprop_of
-  val insts = 
-    map_filter (fn tys => 
-          get_first (fn (k,ss) => if Type.could_unify (hd tys, range_type (get_ty k)) 
-                                  then SOME (get_aD k, ss) 
-                                  else NONE) (snd (get ctxt))) tyss
-  val _ = if null insts then error "Transfer guesser: there were no possible instances, use direction: in order to provide a direction" else ()
-  val ths = map  (fn ((a,D),e) => basic_transfer_rule false a D e leave ctxt th) insts
-  val cth = Conjunction.intr_balanced ths
- in (gctxt, cth)
- end;
-
-fun transfer_rule_by_hint ls leave (gctxt,th) = 
- let 
-  val ctxt = Context.proof_of gctxt
-  val get_aD = Thm.dest_binop o Thm.dest_arg o cprop_of
-  val insts = 
-    map_filter (fn (k,e) => if exists (fn l => l mem_string (#hints e)) ls 
-			    then SOME (get_aD k, e) else NONE)
-        (snd (get ctxt))
-  val _ = if null insts then error "Transfer: No labels provided are stored in the context" else ()
-  val ths = map  (fn ((a,D),e) => basic_transfer_rule false a D e leave ctxt th) insts
-  val cth = Conjunction.intr_balanced ths
- in (gctxt, cth)
- end;
-
-
-fun transferred_attribute ls NONE leave = 
-         if null ls then all_transfers leave else transfer_rule_by_hint ls leave
-  | transferred_attribute _ (SOME (a,D)) leave = transfer_rule (a,D) leave
-
-                                                    (* Add data to the context *)
-fun gen_merge_entries {inj = inj0, emb = emb0, ret = ret0, cong = cg0, guess = g0, hints = hints0}
-                      ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1}, 
-                       {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2})
- = 
- let fun h xs0 xs ys = subtract Thm.eq_thm xs0 (merge Thm.eq_thm (xs,ys)) in
- {inj = h inj0 inj1 inj2, emb = h emb0 emb1 emb2, 
-  ret = h ret0 ret1 ret2, cong = h cg0 cg1 cg2, guess = g1 andalso g2,
-  hints = subtract (op = : string*string -> bool) hints0 
-            (hints1 union_string hints2)}
- end;
-
-local
- val h = curry (merge Thm.eq_thm)
-in
-fun merge_entries ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1}, 
-                   {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2}) = 
-    {inj = h inj1 inj2, emb = h emb1 emb2, ret = h ret1 ret2, cong = h cg1 cg2, guess = g1 andalso g2, hints = hints1 union_string hints2}
-end; 
-
-fun add ((inja,injd), (emba,embd), (reta,retd), (cga,cgd), g, (hintsa, hintsd)) =
-  Thm.declaration_attribute (fn key => fn context => context |> Data.map
-   (fn (ss, al) => 
-     let
-      val _ = ((let val _ = Thm.match (transM_pat, (Thm.dest_arg o cprop_of) key) 
-                in 0 end) 
-                handle MATCH => error "Attribute expected Theorem of the form : TransferMorphism A a B b")
-      val e0 = {inj = inja, emb = emba, ret = reta, cong = cga, guess = g, hints = hintsa}
-      val ed = {inj = injd, emb = embd, ret = retd, cong = cgd, guess = g, hints = hintsd}
-      val entry = 
-        if g then 
-         let val (a0,D0) = (Thm.dest_binop o Thm.dest_arg o cprop_of) key
-             val ctxt0 = ProofContext.init (Thm.theory_of_thm key)
-             val inj' = if null inja then #inj (case AList.lookup eq_key al key of SOME e => e | NONE => error "Transfer: can not generate return rules on the fly, either add injectivity axiom or force manual mode with mode: manual") 
-                        else inja
-             val ret' = merge Thm.eq_thm (reta,  map (fn th => basic_transfer_rule true a0 D0 {inj = inj', emb = [], ret = [], cong = cga, guess = g, hints = hintsa} [] ctxt0 th RS sym) emba)
-         in {inj = inja, emb = emba, ret = ret', cong = cga, guess = g, hints = hintsa} end 
-        else e0
-    in (ss, merge_update eq_key (gen_merge_entries ed) (key, entry) al)
-    end));
-
-
-
-(* concrete syntax *)
-
-local
-
-fun keyword k = Scan.lift (Args.$$$ k) >> K ()
-fun keywordC k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
-
-val congN = "cong"
-val injN = "inj"
-val embedN = "embed"
-val returnN = "return"
-val addN = "add"
-val delN = "del"
-val modeN = "mode"
-val automaticN = "automatic"
-val manualN = "manual"
-val directionN = "direction"
-val labelsN = "labels"
-val leavingN = "leaving"
-
-val any_keyword = keywordC congN || keywordC injN || keywordC embedN || keywordC returnN || keywordC directionN || keywordC modeN || keywordC delN || keywordC labelsN || keywordC leavingN
-
-val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat
-val terms = thms >> map Drule.dest_term
-val types = thms >> (Logic.dest_type o HOLogic.dest_Trueprop o prop_of o hd) 
-val name = Scan.lift Args.name
-val names = Scan.repeat (Scan.unless any_keyword name)
-fun optional scan = Scan.optional scan []
-fun optional2 scan = Scan.optional scan ([],[])
-
-val mode = keywordC modeN |-- ((Scan.lift (Args.$$$ manualN) >> K false) || (Scan.lift (Args.$$$ automaticN) >> K true))
-val inj = (keywordC injN |-- thms) -- optional (keywordC delN |-- thms)
-val embed = (keywordC embedN |-- thms) -- optional (keywordC delN |-- thms)
-val return = (keywordC returnN |-- thms) -- optional (keywordC delN |-- thms)
-val cong = (keywordC congN |-- thms) -- optional (keywordC delN |-- thms)
-val addscan = Scan.unless any_keyword (keyword addN)
-val labels = (keywordC labelsN |-- names) -- optional (keywordC delN |-- names)
-val entry = Scan.optional mode true -- optional2 inj -- optional2 embed -- optional2 return -- optional2 cong -- optional2 labels
-
-val transf_add = addscan |-- entry
-in
-
-val install_att_syntax =
-  (Scan.lift (Args.$$$ delN >> K del) ||
-    transf_add
-    >> (fn (((((g, inj), embed), ret), cg), hints) => add (inj, embed, ret, cg, g, hints)))
-
-val transferred_att_syntax = (optional names -- Scan.option (keywordC directionN |-- (Args.term -- Args.term))
-  -- optional (keywordC leavingN |-- names) >> (fn ((hints, aD),leave) => transferred_attribute hints aD leave));
-
-end;
-
-
-(* theory setup *)
-
-
-val setup =
-  Attrib.setup @{binding transfer} install_att_syntax
-    "Installs transfer data" #>
-  Attrib.setup @{binding transfer_simps} (Attrib.add_del add_ss del_ss)
-    "simp rules for transfer" #>
-  Attrib.setup @{binding transferred} transferred_att_syntax
-    "Transfers theorems";
-
-end;
diff -r 4d4ee06e9420 -r fdbfa0e35e78 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Thu Sep 10 16:16:18 2009 +0200
+++ b/src/HOL/ex/ROOT.ML	Fri Sep 11 09:05:26 2009 +0200
@@ -60,6 +60,7 @@
   "BinEx",
   "Sqrt",
   "Sqrt_Script",
+  "Transfer_Ex",
   "Arithmetic_Series_Complex",
   "HarmonicSeries",
   "Refute_Examples",
diff -r 4d4ee06e9420 -r fdbfa0e35e78 src/HOL/ex/Transfer_Ex.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Transfer_Ex.thy	Fri Sep 11 09:05:26 2009 +0200
@@ -0,0 +1,42 @@
+
+header {* Various examples for transfer procedure *}
+
+theory Transfer_Ex
+imports Complex_Main
+begin
+
+(* nat to int *)
+
+lemma ex1: "(x::nat) + y = y + x"
+  by auto
+
+thm ex1 [transferred]
+
+lemma ex2: "(a::nat) div b * b + a mod b = a"
+  by (rule mod_div_equality)
+
+thm ex2 [transferred]
+
+lemma ex3: "ALL (x::nat). ALL y. EX z. z >= x + y"
+  by auto
+
+thm ex3 [transferred natint]
+
+lemma ex4: "(x::nat) >= y \<Longrightarrow> (x - y) + y = x"
+  by auto
+
+thm ex4 [transferred]
+
+lemma ex5: "(2::nat) * (SUM i <= n. i) = n * (n + 1)"
+  by (induct n rule: nat_induct, auto)
+
+thm ex5 [transferred]
+
+theorem ex6: "0 <= (n::int) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
+  by (rule ex5 [transferred])
+
+thm ex6 [transferred]
+
+thm ex5 [transferred, transferred]
+
+end
\ No newline at end of file