src/ZF/Perm.ML
changeset 826 190974c664a3
parent 791 354a56e923ff
child 862 ce99db6728ba
equal deleted inserted replaced
825:76d9575950f2 826:190974c664a3
    61     "!!f A B. [| <a,b>:f;  <c,b>:f;  f: inj(A,B) |] ==> a=c";
    61     "!!f A B. [| <a,b>:f;  <c,b>:f;  f: inj(A,B) |] ==> a=c";
    62 by (REPEAT (eresolve_tac [asm_rl, Pair_mem_PiE, CollectE] 1));
    62 by (REPEAT (eresolve_tac [asm_rl, Pair_mem_PiE, CollectE] 1));
    63 by (fast_tac ZF_cs 1);
    63 by (fast_tac ZF_cs 1);
    64 qed "inj_equality";
    64 qed "inj_equality";
    65 
    65 
       
    66 goalw thy [inj_def] "!!A B f. [| f:inj(A,B);  a:A;  b:A;  f`a=f`b |] ==> a=b";
       
    67 by (fast_tac ZF_cs 1);
       
    68 val inj_apply_equality = result();
       
    69 
    66 (** A function with a left inverse is an injection **)
    70 (** A function with a left inverse is an injection **)
    67 
    71 
    68 val prems = goal Perm.thy
    72 val prems = goal Perm.thy
    69     "[| f: A->B;  !!x. x:A ==> d(f`x)=x |] ==> f: inj(A,B)";
    73     "[| f: A->B;  !!x. x:A ==> d(f`x)=x |] ==> f: inj(A,B)";
    70 by (asm_simp_tac (ZF_ss addsimps ([inj_def] @ prems)) 1);
    74 by (asm_simp_tac (ZF_ss addsimps ([inj_def] @ prems)) 1);
   119 
   123 
   120 goalw Perm.thy [id_def] "id(A) : A->A";  
   124 goalw Perm.thy [id_def] "id(A) : A->A";  
   121 by (rtac lam_type 1);
   125 by (rtac lam_type 1);
   122 by (assume_tac 1);
   126 by (assume_tac 1);
   123 qed "id_type";
   127 qed "id_type";
       
   128 
       
   129 goalw Perm.thy [id_def] "!!A x. x:A ==> id(A)`x = x";
       
   130 by (asm_simp_tac ZF_ss 1);
       
   131 val id_conv = result();
   124 
   132 
   125 val [prem] = goalw Perm.thy [id_def] "A<=B ==> id(A) <= id(B)";
   133 val [prem] = goalw Perm.thy [id_def] "A<=B ==> id(A) <= id(B)";
   126 by (rtac (prem RS lam_mono) 1);
   134 by (rtac (prem RS lam_mono) 1);
   127 qed "id_mono";
   135 qed "id_mono";
   128 
   136