1.1 --- a/src/HOL/Fun.thy	Thu Sep 10 14:07:58 2009 +0200
     1.2 +++ b/src/HOL/Fun.thy	Thu Sep 10 15:23:07 2009 +0200
     1.3 @@ -7,6 +7,7 @@
     1.4  
     1.5  theory Fun
     1.6  imports Complete_Lattice
     1.7 +uses ("Tools/transfer.ML")
     1.8  begin
     1.9  
    1.10  text{*As a simplification rule, it replaces all function equalities by
    1.11 @@ -568,6 +569,16 @@
    1.12  *}
    1.13  
    1.14  
    1.15 +subsection {* Generic transfer procedure *}
    1.16 +
    1.17 +definition TransferMorphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
    1.18 +  where "TransferMorphism a B \<longleftrightarrow> True"
    1.19 +
    1.20 +use "Tools/transfer.ML"
    1.21 +
    1.22 +setup Transfer.setup
    1.23 +
    1.24 +
    1.25  subsection {* Code generator setup *}
    1.26  
    1.27  types_code

     2.1 --- a/src/HOL/NatTransfer.thy	Thu Sep 10 14:07:58 2009 +0200
     2.2 +++ b/src/HOL/NatTransfer.thy	Thu Sep 10 15:23:07 2009 +0200
     2.3 @@ -1,28 +1,12 @@
     2.4 -(*  Title:      HOL/Library/NatTransfer.thy
     2.5 -    Authors:    Jeremy Avigad and Amine Chaieb
     2.6  
     2.7 -    Sets up transfer from nats to ints and
     2.8 -    back.
     2.9 -*)
    2.10 +(* Authors: Jeremy Avigad and Amine Chaieb *)
    2.11  
    2.12 -
    2.13 -header {* NatTransfer *}
    2.14 +header {* Sets up transfer from nats to ints and back. *}
    2.15  
    2.16  theory NatTransfer
    2.17  imports Main Parity
    2.18 -uses ("Tools/transfer_data.ML")
    2.19  begin
    2.20  
    2.21 -subsection {* A transfer Method between isomorphic domains*}
    2.22 -
    2.23 -definition TransferMorphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
    2.24 -  where "TransferMorphism a B = True"
    2.25 -
    2.26 -use "Tools/transfer_data.ML"
    2.27 -
    2.28 -setup TransferData.setup
    2.29 -
    2.30 -
    2.31  subsection {* Set up transfer from nat to int *}
    2.32  
    2.33  (* set up transfer direction *)
    2.34 @@ -497,41 +481,4 @@
    2.35    return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
    2.36    cong: setsum_cong setprod_cong]
    2.37  
    2.38 -
    2.39 -subsection {* Test it out *}
    2.40 -
    2.41 -(* nat to int *)
    2.42 -
    2.43 -lemma ex1: "(x::nat) + y = y + x"
    2.44 -  by auto
    2.45 -
    2.46 -thm ex1 [transferred]
    2.47 -
    2.48 -lemma ex2: "(a::nat) div b * b + a mod b = a"
    2.49 -  by (rule mod_div_equality)
    2.50 -
    2.51 -thm ex2 [transferred]
    2.52 -
    2.53 -lemma ex3: "ALL (x::nat). ALL y. EX z. z >= x + y"
    2.54 -  by auto
    2.55 -
    2.56 -thm ex3 [transferred natint]
    2.57 -
    2.58 -lemma ex4: "(x::nat) >= y \<Longrightarrow> (x - y) + y = x"
    2.59 -  by auto
    2.60 -
    2.61 -thm ex4 [transferred]
    2.62 -
    2.63 -lemma ex5: "(2::nat) * (SUM i <= n. i) = n * (n + 1)"
    2.64 -  by (induct n rule: nat_induct, auto)
    2.65 -
    2.66 -thm ex5 [transferred]
    2.67 -
    2.68 -theorem ex6: "0 <= (n::int) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
    2.69 -  by (rule ex5 [transferred])
    2.70 -
    2.71 -thm ex6 [transferred]
    2.72 -
    2.73 -thm ex5 [transferred, transferred]
    2.74 -
    2.75  end