New proof of apply_equality and new thm Pi_image_cons
authorpaulson
Mon Apr 27 13:47:46 1998 +0200 (1998-04-27)
changeset 4829aa5ea943f8e3
parent 4828 ee3317896a47
child 4830 bd73675adbed
New proof of apply_equality and new thm Pi_image_cons
src/ZF/func.ML
     1.1 --- a/src/ZF/func.ML	Fri Apr 24 16:18:39 1998 +0200
     1.2 +++ b/src/ZF/func.ML	Mon Apr 27 13:47:46 1998 +0200
     1.3 @@ -75,10 +75,13 @@
     1.4  by (Blast_tac 1);
     1.5  qed "apply_equality2";
     1.6  
     1.7 -goalw ZF.thy [apply_def] "!!a b f. [| <a,b>: f;  f: Pi(A,B) |] ==> f`a = b";
     1.8 -by (rtac the_equality 1);
     1.9 -by (rtac apply_equality2 2);
    1.10 -by (REPEAT (assume_tac 1));
    1.11 +goalw ZF.thy [apply_def, function_def]
    1.12 +     "!!a b f. [| <a,b>: f;  function(f) |] ==> f`a = b";
    1.13 +by (blast_tac (claset() addIs [the_equality]) 1);
    1.14 +qed "function_apply_equality";
    1.15 +
    1.16 +goalw ZF.thy [Pi_def] "!!a b f. [| <a,b>: f;  f: Pi(A,B) |] ==> f`a = b";
    1.17 +by (blast_tac (claset() addIs [function_apply_equality]) 1);
    1.18  qed "apply_equality";
    1.19  
    1.20  (*Applying a function outside its domain yields 0*)
    1.21 @@ -250,6 +253,10 @@
    1.22                                addcongs [RepFun_cong]) 1);
    1.23  qed "image_fun";
    1.24  
    1.25 +goal thy "!!f. [| f: Pi(A,B);  x: A |] ==> f `` cons(x,y) = cons(f`x, f``y)";
    1.26 +by (blast_tac (claset() addDs [apply_equality, apply_Pair]) 1);
    1.27 +qed "Pi_image_cons";
    1.28 +
    1.29  
    1.30  (*** properties of "restrict" ***)
    1.31