equal
deleted
inserted
replaced
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 |