src/HOL/Product_Type.thy
changeset 22744 5cbe966d67a2
parent 22577 1a08fce38565
child 22838 466599ecf610
     1.1 --- a/src/HOL/Product_Type.thy	Fri Apr 20 11:21:41 2007 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Fri Apr 20 11:21:42 2007 +0200
     1.3 @@ -104,10 +104,10 @@
     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:    "split == (%c p. c (fst p) (snd p))"
     1.8 -  curry_def:    "curry == (%c x y. c (Pair x y))"
     1.9 -  prod_fun_def: "prod_fun f g == split (%x y. Pair (f x) (g y))"
    1.10 -  Sigma_def:    "Sigma A B == UN x:A. UN y:B x. {Pair x y}"
    1.11 +  split_def [code func]:    "split == (%c p. c (fst p) (snd p))"
    1.12 +  curry_def [code func]:    "curry == (%c x y. c (Pair x y))"
    1.13 +  prod_fun_def [code func]: "prod_fun f g == split (%x y. Pair (f x) (g y))"
    1.14 +  Sigma_def [code func]:    "Sigma A B == UN x:A. UN y:B x. {Pair x y}"
    1.15  
    1.16  abbreviation
    1.17    Times :: "['a set, 'b set] => ('a * 'b) set"
    1.18 @@ -599,17 +599,22 @@
    1.19    done
    1.20  
    1.21  
    1.22 -constdefs
    1.23 -  upd_fst :: "('a => 'c) => 'a * 'b => 'c * 'b"
    1.24 - "upd_fst f == prod_fun f id"
    1.25 +definition
    1.26 +  upd_fst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b"
    1.27 +where
    1.28 +  "upd_fst f = prod_fun f id"
    1.29  
    1.30 -  upd_snd :: "('b => 'c) => 'a * 'b => 'a * 'c"
    1.31 - "upd_snd f == prod_fun id f"
    1.32 +definition
    1.33 +  upd_snd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'c"
    1.34 +where
    1.35 +  "upd_snd f = prod_fun id f"
    1.36  
    1.37 -lemma upd_fst_conv [simp]: "upd_fst f (x,y) = (f x,y)" 
    1.38 +lemma upd_fst_conv [simp, code func]:
    1.39 +  "upd_fst f (x, y) = (f x, y)" 
    1.40    by (simp add: upd_fst_def)
    1.41  
    1.42 -lemma upd_snd_conv [simp]: "upd_snd f (x,y) = (x,f y)" 
    1.43 +lemma upd_snd_conv [simp, code func]:
    1.44 +  "upd_snd f (x, y) = (x, f y)" 
    1.45    by (simp add: upd_snd_def)
    1.46  
    1.47  text {*