src/HOL/Product_Type.thy
 changeset 14189 de58f4d939e1 parent 14101 d25c23e46173 child 14190 609c072edf90
```     1.1 --- a/src/HOL/Product_Type.thy	Mon Sep 15 12:16:34 2003 +0200
1.2 +++ b/src/HOL/Product_Type.thy	Mon Sep 15 12:27:13 2003 +0200
1.3 @@ -91,6 +91,7 @@
1.4    fst      :: "'a * 'b => 'a"
1.5    snd      :: "'a * 'b => 'b"
1.6    split    :: "[['a, 'b] => 'c, 'a * 'b] => 'c"
1.7 +  curry    :: "['a * 'b => 'c, 'a, 'b] => 'c"
1.8    prod_fun :: "['a => 'b, 'c => 'd, 'a * 'c] => 'b * 'd"
1.9    Pair     :: "['a, 'b] => 'a * 'b"
1.10    Sigma    :: "['a set, 'a => 'b set] => ('a * 'b) set"
1.11 @@ -141,6 +142,7 @@
1.12    fst_def:      "fst p == THE a. EX b. p = (a, b)"
1.13    snd_def:      "snd p == THE b. EX a. p = (a, b)"
1.14    split_def:    "split == (%c p. c (fst p) (snd p))"
1.15 +  curry_def:    "curry == (%c x y. c (x,y))"
1.16    prod_fun_def: "prod_fun f g == split(%x y.(f(x), g(y)))"
1.17    Sigma_def:    "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
1.18
1.19 @@ -265,6 +267,24 @@
1.20    -- {* @{text "[iff]"} is not a good idea because it makes @{text blast} loop *}
1.21    by fast
1.22
1.23 +lemma curry_split [simp]: "curry (split f) = f"
1.24 +  by (simp add: curry_def split_def)
1.25 +
1.26 +lemma split_curry [simp]: "split (curry f) = f"
1.27 +  by (simp add: curry_def split_def)
1.28 +
1.29 +lemma curryI [intro!]: "f (a,b) ==> curry f a b"
1.30 +  by (simp add: curry_def)
1.31 +
1.32 +lemma curryD [dest]: "curry f a b ==> f (a,b)"
1.33 +  by (simp add: curry_def)
1.34 +
1.35 +lemma curryE [elim!]: "[| curry f a b ; f (a,b) ==> Q |] ==> Q"
1.36 +  by (simp add: curry_def)
1.37 +
1.38 +lemma curry_conv [simp]: "curry f a b = f (a,b)"
1.39 +  by (simp add: curry_def)
1.40 +
1.41  lemma prod_induct [induct type: *]: "!!x. (!!a b. P (a, b)) ==> P x"
1.42    by fast
1.43
```