1.1 --- a/src/ZF/func.ML	Wed Feb 13 10:44:39 2002 +0100
     1.2 +++ b/src/ZF/func.ML	Wed Feb 13 10:45:08 2002 +0100
     1.3 @@ -23,16 +23,11 @@
     1.4  by (asm_full_simp_tac (FOL_ss addsimps [Pi_iff]) 1);
     1.5  qed "fun_is_function";
     1.6  
     1.7 -(**Two "destruct" rules for Pi **)
     1.8 -
     1.9 +(*Functions are relations*)
    1.10  Goalw [Pi_def] "f: Pi(A,B) ==> f <= Sigma(A,B)";  
    1.11  by (Blast_tac 1);
    1.12  qed "fun_is_rel";
    1.13  
    1.14 -Goal "[| f: Pi(A,B);  a:A |] ==> EX! y. <a,y>: f";  
    1.15 -by (blast_tac (claset() addSDs [Pi_iff_old RS iffD1]) 1);
    1.16 -qed "fun_unique_Pair";
    1.17 -
    1.18  val prems = Goalw [Pi_def]
    1.19      "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==> Pi(A,B) = Pi(A',B')";
    1.20  by (simp_tac (FOL_ss addsimps prems addcongs [Sigma_cong]) 1);
    1.21 @@ -72,10 +67,15 @@
    1.22  by (blast_tac (claset() addDs [apply_equality]) 1);
    1.23  qed "Pi_memberD";
    1.24  
    1.25 +Goal "[| function(f);  a : domain(f)|] ==> <a,f`a>: f";
    1.26 +by (asm_full_simp_tac (simpset() addsimps [function_def, apply_def]) 1); 
    1.27 +by (rtac theI2 1);
    1.28 +by Auto_tac;  
    1.29 +qed "function_apply_Pair";
    1.30 +
    1.31  Goal "[| f: Pi(A,B);  a:A |] ==> <a,f`a>: f";
    1.32 -by (rtac (fun_unique_Pair RS ex1E) 1);
    1.33 -by (resolve_tac [apply_equality RS ssubst] 3);
    1.34 -by (REPEAT (assume_tac 1));
    1.35 +by (asm_full_simp_tac (simpset() addsimps [Pi_iff]) 1); 
    1.36 +by (blast_tac (claset() addIs [function_apply_Pair]) 1); 
    1.37  qed "apply_Pair";
    1.38  
    1.39  (*Conclusion is flexible -- use res_inst_tac or else apply_funtype below!*)