--- 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
--- 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