inj_apply_equality: new
authorlcp
Fri Dec 23 16:28:26 1994 +0100 (1994-12-23)
changeset 826190974c664a3
parent 825 76d9575950f2
child 827 aa332949ce1a
inj_apply_equality: new
src/ZF/Perm.ML
     1.1 --- a/src/ZF/Perm.ML	Fri Dec 23 16:27:45 1994 +0100
     1.2 +++ b/src/ZF/Perm.ML	Fri Dec 23 16:28:26 1994 +0100
     1.3 @@ -63,6 +63,10 @@
     1.4  by (fast_tac ZF_cs 1);
     1.5  qed "inj_equality";
     1.6  
     1.7 +goalw thy [inj_def] "!!A B f. [| f:inj(A,B);  a:A;  b:A;  f`a=f`b |] ==> a=b";
     1.8 +by (fast_tac ZF_cs 1);
     1.9 +val inj_apply_equality = result();
    1.10 +
    1.11  (** A function with a left inverse is an injection **)
    1.12  
    1.13  val prems = goal Perm.thy
    1.14 @@ -122,6 +126,10 @@
    1.15  by (assume_tac 1);
    1.16  qed "id_type";
    1.17  
    1.18 +goalw Perm.thy [id_def] "!!A x. x:A ==> id(A)`x = x";
    1.19 +by (asm_simp_tac ZF_ss 1);
    1.20 +val id_conv = result();
    1.21 +
    1.22  val [prem] = goalw Perm.thy [id_def] "A<=B ==> id(A) <= id(B)";
    1.23  by (rtac (prem RS lam_mono) 1);
    1.24  qed "id_mono";