# HG changeset patch
# User paulson
# Date 893677666 -7200
# Node ID aa5ea943f8e397e613ea3467ac33ef66dded86c5
# Parent  ee3317896a4734ccd5062f5b54ea7a03ba473b89
New proof of apply_equality and new thm Pi_image_cons

diff -r ee3317896a47 -r aa5ea943f8e3 src/ZF/func.ML
--- a/src/ZF/func.ML	Fri Apr 24 16:18:39 1998 +0200
+++ b/src/ZF/func.ML	Mon Apr 27 13:47:46 1998 +0200
@@ -75,10 +75,13 @@
 by (Blast_tac 1);
 qed "apply_equality2";
 
-goalw ZF.thy [apply_def] "!!a b f. [| <a,b>: f;  f: Pi(A,B) |] ==> f`a = b";
-by (rtac the_equality 1);
-by (rtac apply_equality2 2);
-by (REPEAT (assume_tac 1));
+goalw ZF.thy [apply_def, function_def]
+     "!!a b f. [| <a,b>: f;  function(f) |] ==> f`a = b";
+by (blast_tac (claset() addIs [the_equality]) 1);
+qed "function_apply_equality";
+
+goalw ZF.thy [Pi_def] "!!a b f. [| <a,b>: f;  f: Pi(A,B) |] ==> f`a = b";
+by (blast_tac (claset() addIs [function_apply_equality]) 1);
 qed "apply_equality";
 
 (*Applying a function outside its domain yields 0*)
@@ -250,6 +253,10 @@
                               addcongs [RepFun_cong]) 1);
 qed "image_fun";
 
+goal thy "!!f. [| f: Pi(A,B);  x: A |] ==> f `` cons(x,y) = cons(f`x, f``y)";
+by (blast_tac (claset() addDs [apply_equality, apply_Pair]) 1);
+qed "Pi_image_cons";
+
 
 (*** properties of "restrict" ***)