# HG changeset patch
# User paulson
# Date 1013593508 -3600
# Node ID 6288ebcb16233115ab5c79c9e5d90f70f327bf54
# Parent  5d18148e9059ae6bcb1011bf78977a047b64b8a8
new function lemmas

diff -r 5d18148e9059 -r 6288ebcb1623 src/ZF/func.ML
--- a/src/ZF/func.ML	Wed Feb 13 10:44:39 2002 +0100
+++ b/src/ZF/func.ML	Wed Feb 13 10:45:08 2002 +0100
@@ -23,16 +23,11 @@
 by (asm_full_simp_tac (FOL_ss addsimps [Pi_iff]) 1);
 qed "fun_is_function";
 
-(**Two "destruct" rules for Pi **)
-
+(*Functions are relations*)
 Goalw [Pi_def] "f: Pi(A,B) ==> f <= Sigma(A,B)";  
 by (Blast_tac 1);
 qed "fun_is_rel";
 
-Goal "[| f: Pi(A,B);  a:A |] ==> EX! y. <a,y>: f";  
-by (blast_tac (claset() addSDs [Pi_iff_old RS iffD1]) 1);
-qed "fun_unique_Pair";
-
 val prems = Goalw [Pi_def]
     "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==> Pi(A,B) = Pi(A',B')";
 by (simp_tac (FOL_ss addsimps prems addcongs [Sigma_cong]) 1);
@@ -72,10 +67,15 @@
 by (blast_tac (claset() addDs [apply_equality]) 1);
 qed "Pi_memberD";
 
+Goal "[| function(f);  a : domain(f)|] ==> <a,f`a>: f";
+by (asm_full_simp_tac (simpset() addsimps [function_def, apply_def]) 1); 
+by (rtac theI2 1);
+by Auto_tac;  
+qed "function_apply_Pair";
+
 Goal "[| f: Pi(A,B);  a:A |] ==> <a,f`a>: f";
-by (rtac (fun_unique_Pair RS ex1E) 1);
-by (resolve_tac [apply_equality RS ssubst] 3);
-by (REPEAT (assume_tac 1));
+by (asm_full_simp_tac (simpset() addsimps [Pi_iff]) 1); 
+by (blast_tac (claset() addIs [function_apply_Pair]) 1); 
 qed "apply_Pair";
 
 (*Conclusion is flexible -- use res_inst_tac or else apply_funtype below!*)