# HG changeset patch
# User haftmann
# Date 1252588987 -7200
# Node ID 4ccd84fb19d343054fca6709dc8526db55e5438d
# Parent  bf781ef40c8193b3ecc4318ccb776325607e475c
early bootstrap of generic transfer procedure

diff -r bf781ef40c81 -r 4ccd84fb19d3 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Thu Sep 10 14:07:58 2009 +0200
+++ b/src/HOL/Fun.thy	Thu Sep 10 15:23:07 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 bf781ef40c81 -r 4ccd84fb19d3 src/HOL/NatTransfer.thy
--- a/src/HOL/NatTransfer.thy	Thu Sep 10 14:07:58 2009 +0200
+++ b/src/HOL/NatTransfer.thy	Thu Sep 10 15:23:07 2009 +0200
@@ -1,28 +1,12 @@
-(*  Title:      HOL/Library/NatTransfer.thy
-    Authors:    Jeremy Avigad and Amine Chaieb
 
-    Sets up transfer from nats to ints and
-    back.
-*)
+(* Authors: Jeremy Avigad and Amine Chaieb *)
 
-
-header {* NatTransfer *}
+header {* Sets up transfer from nats to ints and back. *}
 
 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 *)
@@ -497,41 +481,4 @@
   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