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