Added the constant "curry".
authorskalberg
Mon Sep 15 12:27:13 2003 +0200 (2003-09-15)
changeset 14189de58f4d939e1
parent 14188 f471cd4c7282
child 14190 609c072edf90
Added the constant "curry".
src/HOL/Product_Type.thy
     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