# HG changeset patch
# User skalberg
# Date 1063621633 -7200
# Node ID de58f4d939e1020ad8674c099ed33dd63a98e360
# Parent  f471cd4c7282c5334d31f8537aeb94cb8f5f50ce
Added the constant "curry".

diff -r f471cd4c7282 -r de58f4d939e1 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Mon Sep 15 12:16:34 2003 +0200
+++ b/src/HOL/Product_Type.thy	Mon Sep 15 12:27:13 2003 +0200
@@ -91,6 +91,7 @@
   fst      :: "'a * 'b => 'a"
   snd      :: "'a * 'b => 'b"
   split    :: "[['a, 'b] => 'c, 'a * 'b] => 'c"
+  curry    :: "['a * 'b => 'c, 'a, 'b] => 'c"
   prod_fun :: "['a => 'b, 'c => 'd, 'a * 'c] => 'b * 'd"
   Pair     :: "['a, 'b] => 'a * 'b"
   Sigma    :: "['a set, 'a => 'b set] => ('a * 'b) set"
@@ -141,6 +142,7 @@
   fst_def:      "fst p == THE a. EX b. p = (a, b)"
   snd_def:      "snd p == THE b. EX a. p = (a, b)"
   split_def:    "split == (%c p. c (fst p) (snd p))"
+  curry_def:    "curry == (%c x y. c (x,y))"
   prod_fun_def: "prod_fun f g == split(%x y.(f(x), g(y)))"
   Sigma_def:    "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
 
@@ -265,6 +267,24 @@
   -- {* @{text "[iff]"} is not a good idea because it makes @{text blast} loop *}
   by fast
 
+lemma curry_split [simp]: "curry (split f) = f"
+  by (simp add: curry_def split_def)
+
+lemma split_curry [simp]: "split (curry f) = f"
+  by (simp add: curry_def split_def)
+
+lemma curryI [intro!]: "f (a,b) ==> curry f a b"
+  by (simp add: curry_def)
+
+lemma curryD [dest]: "curry f a b ==> f (a,b)"
+  by (simp add: curry_def)
+
+lemma curryE [elim!]: "[| curry f a b ; f (a,b) ==> Q |] ==> Q"
+  by (simp add: curry_def)
+
+lemma curry_conv [simp]: "curry f a b = f (a,b)"
+  by (simp add: curry_def)
+
 lemma prod_induct [induct type: *]: "!!x. (!!a b. P (a, b)) ==> P x"
   by fast