equal
deleted
inserted
replaced
154 |
154 |
155 |
155 |
156 (*** Converse of a function ***) |
156 (*** Converse of a function ***) |
157 |
157 |
158 goalw Perm.thy [inj_def] "!!f. f: inj(A,B) ==> converse(f) : range(f)->A"; |
158 goalw Perm.thy [inj_def] "!!f. f: inj(A,B) ==> converse(f) : range(f)->A"; |
159 by (asm_simp_tac |
159 by (asm_simp_tac (ZF_ss addsimps [Pi_iff, function_def]) 1); |
160 (ZF_ss addsimps [Pi_iff, function_def, |
|
161 domain_converse, converse_iff]) 1); |
|
162 by (eresolve_tac [CollectE] 1); |
160 by (eresolve_tac [CollectE] 1); |
163 by (asm_simp_tac (ZF_ss addsimps [apply_iff]) 1); |
161 by (asm_simp_tac (ZF_ss addsimps [apply_iff]) 1); |
164 by (fast_tac (ZF_cs addDs [fun_is_rel]) 1); |
162 by (fast_tac (ZF_cs addDs [fun_is_rel]) 1); |
165 qed "inj_converse_fun"; |
163 qed "inj_converse_fun"; |
166 |
164 |