src/HOL/Product_Type.thy
changeset 24162 8dfd5dd65d82
parent 23247 b99dce43d252
child 24286 7619080e49f0
     1.1 --- a/src/HOL/Product_Type.thy	Tue Aug 07 09:38:43 2007 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Tue Aug 07 09:38:44 2007 +0200
     1.3 @@ -104,9 +104,9 @@
     1.4    Pair_def:     "Pair a b == Abs_Prod (Pair_Rep a b)"
     1.5    fst_def:      "fst p == THE a. EX b. p = Pair a b"
     1.6    snd_def:      "snd p == THE b. EX a. p = Pair a b"
     1.7 -  split_def [code func]:    "split == (%c p. c (fst p) (snd p))"
     1.8 -  curry_def [code func]:    "curry == (%c x y. c (Pair x y))"
     1.9 -  prod_fun_def [code func]: "prod_fun f g == split (%x y. Pair (f x) (g y))"
    1.10 +  split_def:    "split == (%c p. c (fst p) (snd p))"
    1.11 +  curry_def:    "curry == (%c x y. c (Pair x y))"
    1.12 +  prod_fun_def: "prod_fun f g == split (%x y. Pair (f x) (g y))"
    1.13    Sigma_def [code func]:    "Sigma A B == UN x:A. UN y:B x. {Pair x y}"
    1.14  
    1.15  abbreviation
    1.16 @@ -337,7 +337,7 @@
    1.17  lemma curryE: "[| curry f a b ; f (a,b) ==> Q |] ==> Q"
    1.18    by (simp add: curry_def)
    1.19  
    1.20 -lemma curry_conv [simp]: "curry f a b = f (a,b)"
    1.21 +lemma curry_conv [simp, code func]: "curry f a b = f (a,b)"
    1.22    by (simp add: curry_def)
    1.23  
    1.24  lemma prod_induct [induct type: *]: "!!x. (!!a b. P (a, b)) ==> P x"
    1.25 @@ -346,7 +346,7 @@
    1.26  lemma split_paired_Ex [simp]: "(EX x. P x) = (EX a b. P (a, b))"
    1.27    by fast
    1.28  
    1.29 -lemma split_conv [simp]: "split c (a, b) = c a b"
    1.30 +lemma split_conv [simp, code func]: "split c (a, b) = c a b"
    1.31    by (simp add: split_def)
    1.32  
    1.33  lemmas split = split_conv  -- {* for backwards compatibility *}
    1.34 @@ -569,7 +569,7 @@
    1.35    functions.
    1.36  *}
    1.37  
    1.38 -lemma prod_fun [simp]: "prod_fun f g (a, b) = (f a, g b)"
    1.39 +lemma prod_fun [simp, code func]: "prod_fun f g (a, b) = (f a, g b)"
    1.40    by (simp add: prod_fun_def)
    1.41  
    1.42  lemma prod_fun_compose: "prod_fun (f1 o f2) (g1 o g2) = (prod_fun f1 g1 o prod_fun f2 g2)"
    1.43 @@ -754,6 +754,8 @@
    1.44    internal_split :: "('a => 'b => 'c) => 'a * 'b => 'c"
    1.45    "internal_split == split"
    1.46  
    1.47 +lemmas [code func del] = internal_split_def
    1.48 +
    1.49  lemma internal_split_conv: "internal_split c (a, b) = c a b"
    1.50    by (simp only: internal_split_def split_conv)
    1.51  
    1.52 @@ -908,7 +910,6 @@
    1.53  
    1.54    Codegen.add_codegen "let_codegen" let_codegen
    1.55    #> Codegen.add_codegen "split_codegen" split_codegen
    1.56 -  #> CodegenPackage.add_appconst ("Let", CodegenPackage.appgen_let)
    1.57  
    1.58  end
    1.59  *}