|
1 (* Title: ZF/perm.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1991 University of Cambridge |
|
5 |
|
6 For perm.thy. The theory underlying permutation groups |
|
7 -- Composition of relations, the identity relation |
|
8 -- Injections, surjections, bijections |
|
9 -- Lemmas for the Schroeder-Bernstein Theorem |
|
10 *) |
|
11 |
|
12 open Perm; |
|
13 |
|
14 (** Surjective function space **) |
|
15 |
|
16 goalw Perm.thy [surj_def] "!!f A B. f: surj(A,B) ==> f: A->B"; |
|
17 by (etac CollectD1 1); |
|
18 val surj_is_fun = result(); |
|
19 |
|
20 goalw Perm.thy [surj_def] "!!f A B. f : Pi(A,B) ==> f: surj(A,range(f))"; |
|
21 by (fast_tac (ZF_cs addIs [apply_equality] |
|
22 addEs [range_of_fun,domain_type]) 1); |
|
23 val fun_is_surj = result(); |
|
24 |
|
25 goalw Perm.thy [surj_def] "!!f A B. f: surj(A,B) ==> range(f)=B"; |
|
26 by (best_tac (ZF_cs addIs [equalityI,apply_Pair] addEs [range_type]) 1); |
|
27 val surj_range = result(); |
|
28 |
|
29 |
|
30 (** Injective function space **) |
|
31 |
|
32 goalw Perm.thy [inj_def] "!!f A B. f: inj(A,B) ==> f: A->B"; |
|
33 by (etac CollectD1 1); |
|
34 val inj_is_fun = result(); |
|
35 |
|
36 goalw Perm.thy [inj_def] |
|
37 "!!f A B. [| <a,b>:f; <c,b>:f; f: inj(A,B) |] ==> a=c"; |
|
38 by (REPEAT (eresolve_tac [asm_rl, Pair_mem_PiE, CollectE] 1)); |
|
39 by (fast_tac ZF_cs 1); |
|
40 val inj_equality = result(); |
|
41 |
|
42 (** Bijections -- simple lemmas but no intro/elim rules -- use unfolding **) |
|
43 |
|
44 goalw Perm.thy [bij_def] "!!f A B. f: bij(A,B) ==> f: inj(A,B)"; |
|
45 by (etac IntD1 1); |
|
46 val bij_is_inj = result(); |
|
47 |
|
48 goalw Perm.thy [bij_def] "!!f A B. f: bij(A,B) ==> f: surj(A,B)"; |
|
49 by (etac IntD2 1); |
|
50 val bij_is_surj = result(); |
|
51 |
|
52 (* f: bij(A,B) ==> f: A->B *) |
|
53 val bij_is_fun = standard (bij_is_inj RS inj_is_fun); |
|
54 |
|
55 (** Identity function **) |
|
56 |
|
57 val [prem] = goalw Perm.thy [id_def] "a:A ==> <a,a> : id(A)"; |
|
58 by (rtac (prem RS lamI) 1); |
|
59 val idI = result(); |
|
60 |
|
61 val major::prems = goalw Perm.thy [id_def] |
|
62 "[| p: id(A); !!x.[| x:A; p=<x,x> |] ==> P \ |
|
63 \ |] ==> P"; |
|
64 by (rtac (major RS lamE) 1); |
|
65 by (REPEAT (ares_tac prems 1)); |
|
66 val idE = result(); |
|
67 |
|
68 goalw Perm.thy [id_def] "id(A) : A->A"; |
|
69 by (rtac lam_type 1); |
|
70 by (assume_tac 1); |
|
71 val id_type = result(); |
|
72 |
|
73 val [prem] = goalw Perm.thy [id_def] "A<=B ==> id(A) <= id(B)"; |
|
74 by (rtac (prem RS lam_mono) 1); |
|
75 val id_mono = result(); |
|
76 |
|
77 goalw Perm.thy [inj_def,id_def] "id(A): inj(A,A)"; |
|
78 by (REPEAT (ares_tac [CollectI,lam_type] 1)); |
|
79 by (SIMP_TAC ZF_ss 1); |
|
80 val id_inj = result(); |
|
81 |
|
82 goalw Perm.thy [id_def,surj_def] "id(A): surj(A,A)"; |
|
83 by (fast_tac (ZF_cs addIs [lam_type,beta]) 1); |
|
84 val id_surj = result(); |
|
85 |
|
86 goalw Perm.thy [bij_def] "id(A): bij(A,A)"; |
|
87 by (fast_tac (ZF_cs addIs [id_inj,id_surj]) 1); |
|
88 val id_bij = result(); |
|
89 |
|
90 |
|
91 (** Converse of a relation **) |
|
92 |
|
93 val [prem] = goal Perm.thy "f: inj(A,B) ==> converse(f) : range(f)->A"; |
|
94 by (rtac (prem RS inj_is_fun RS PiE) 1); |
|
95 by (rtac (converse_type RS PiI) 1); |
|
96 by (fast_tac ZF_cs 1); |
|
97 by (fast_tac (ZF_cs addEs [prem RSN (3,inj_equality)]) 1); |
|
98 by flexflex_tac; |
|
99 val inj_converse_fun = result(); |
|
100 |
|
101 val prems = goalw Perm.thy [surj_def] |
|
102 "f: inj(A,B) ==> converse(f): surj(range(f), A)"; |
|
103 by (fast_tac (ZF_cs addIs (prems@[inj_converse_fun,apply_Pair,apply_equality, |
|
104 converseI,inj_is_fun])) 1); |
|
105 val inj_converse_surj = result(); |
|
106 |
|
107 (*The premises are equivalent to saying that f is injective...*) |
|
108 val prems = goal Perm.thy |
|
109 "[| f: A->B; converse(f): C->A; a: A |] ==> converse(f)`(f`a) = a"; |
|
110 by (fast_tac (ZF_cs addIs (prems@[apply_Pair,apply_equality,converseI])) 1); |
|
111 val left_inverse_lemma = result(); |
|
112 |
|
113 val prems = goal Perm.thy |
|
114 "[| f: inj(A,B); a: A |] ==> converse(f)`(f`a) = a"; |
|
115 by (fast_tac (ZF_cs addIs (prems@ |
|
116 [left_inverse_lemma,inj_converse_fun,inj_is_fun])) 1); |
|
117 val left_inverse = result(); |
|
118 |
|
119 val prems = goal Perm.thy |
|
120 "[| f: A->B; converse(f): C->A; b: C |] ==> f`(converse(f)`b) = b"; |
|
121 by (rtac (apply_Pair RS (converseD RS apply_equality)) 1); |
|
122 by (REPEAT (resolve_tac prems 1)); |
|
123 val right_inverse_lemma = result(); |
|
124 |
|
125 val prems = goal Perm.thy |
|
126 "[| f: inj(A,B); b: range(f) |] ==> f`(converse(f)`b) = b"; |
|
127 by (rtac right_inverse_lemma 1); |
|
128 by (REPEAT (resolve_tac (prems@ [inj_converse_fun,inj_is_fun]) 1)); |
|
129 val right_inverse = result(); |
|
130 |
|
131 val prems = goal Perm.thy |
|
132 "f: inj(A,B) ==> converse(f): inj(range(f), A)"; |
|
133 bw inj_def; (*rewrite subgoal but not prems!!*) |
|
134 by (cut_facts_tac prems 1); |
|
135 by (safe_tac ZF_cs); |
|
136 (*apply f to both sides and simplify using right_inverse |
|
137 -- could also use etac[subst_context RS box_equals] in this proof *) |
|
138 by (rtac simp_equals 2); |
|
139 by (REPEAT (eresolve_tac [inj_converse_fun, right_inverse RS sym, ssubst] 1 |
|
140 ORELSE ares_tac [refl,rangeI] 1)); |
|
141 val inj_converse_inj = result(); |
|
142 |
|
143 goalw Perm.thy [bij_def] "!!f A B. f: bij(A,B) ==> converse(f): bij(B,A)"; |
|
144 by (etac IntE 1); |
|
145 by (eresolve_tac [(surj_range RS subst)] 1); |
|
146 by (rtac IntI 1); |
|
147 by (etac inj_converse_inj 1); |
|
148 by (etac inj_converse_surj 1); |
|
149 val bij_converse_bij = result(); |
|
150 |
|
151 |
|
152 (** Composition of two relations **) |
|
153 |
|
154 (*The inductive definition package could derive these theorems for R o S*) |
|
155 |
|
156 goalw Perm.thy [comp_def] "!!r s. [| <a,b>:s; <b,c>:r |] ==> <a,c> : r O s"; |
|
157 by (fast_tac ZF_cs 1); |
|
158 val compI = result(); |
|
159 |
|
160 val prems = goalw Perm.thy [comp_def] |
|
161 "[| xz : r O s; \ |
|
162 \ !!x y z. [| xz=<x,z>; <x,y>:s; <y,z>:r |] ==> P \ |
|
163 \ |] ==> P"; |
|
164 by (cut_facts_tac prems 1); |
|
165 by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1 ORELSE ares_tac prems 1)); |
|
166 val compE = result(); |
|
167 |
|
168 val compEpair = |
|
169 rule_by_tactic (REPEAT_FIRST (etac Pair_inject ORELSE' bound_hyp_subst_tac) |
|
170 THEN prune_params_tac) |
|
171 (read_instantiate [("xz","<a,c>")] compE); |
|
172 |
|
173 val comp_cs = ZF_cs addIs [compI,idI] addSEs [compE,idE]; |
|
174 |
|
175 (** Domain and Range -- see Suppes, section 3.1 **) |
|
176 |
|
177 (*Boyer et al., Set Theory in First-Order Logic, JAR 2 (1986), 287-327*) |
|
178 goal Perm.thy "range(r O s) <= range(r)"; |
|
179 by (fast_tac comp_cs 1); |
|
180 val range_comp = result(); |
|
181 |
|
182 goal Perm.thy "!!r s. domain(r) <= range(s) ==> range(r O s) = range(r)"; |
|
183 by (rtac (range_comp RS equalityI) 1); |
|
184 by (fast_tac comp_cs 1); |
|
185 val range_comp_eq = result(); |
|
186 |
|
187 goal Perm.thy "domain(r O s) <= domain(s)"; |
|
188 by (fast_tac comp_cs 1); |
|
189 val domain_comp = result(); |
|
190 |
|
191 goal Perm.thy "!!r s. range(s) <= domain(r) ==> domain(r O s) = domain(s)"; |
|
192 by (rtac (domain_comp RS equalityI) 1); |
|
193 by (fast_tac comp_cs 1); |
|
194 val domain_comp_eq = result(); |
|
195 |
|
196 (** Other results **) |
|
197 |
|
198 goal Perm.thy "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)"; |
|
199 by (fast_tac comp_cs 1); |
|
200 val comp_mono = result(); |
|
201 |
|
202 (*composition preserves relations*) |
|
203 goal Perm.thy "!!r s. [| s<=A*B; r<=B*C |] ==> (r O s) <= A*C"; |
|
204 by (fast_tac comp_cs 1); |
|
205 val comp_rel = result(); |
|
206 |
|
207 (*associative law for composition*) |
|
208 goal Perm.thy "(r O s) O t = r O (s O t)"; |
|
209 by (fast_tac (comp_cs addIs [equalityI]) 1); |
|
210 val comp_assoc = result(); |
|
211 |
|
212 (*left identity of composition; provable inclusions are |
|
213 id(A) O r <= r |
|
214 and [| r<=A*B; B<=C |] ==> r <= id(C) O r *) |
|
215 goal Perm.thy "!!r A B. r<=A*B ==> id(B) O r = r"; |
|
216 by (fast_tac (comp_cs addIs [equalityI]) 1); |
|
217 val left_comp_id = result(); |
|
218 |
|
219 (*right identity of composition; provable inclusions are |
|
220 r O id(A) <= r |
|
221 and [| r<=A*B; A<=C |] ==> r <= r O id(C) *) |
|
222 goal Perm.thy "!!r A B. r<=A*B ==> r O id(A) = r"; |
|
223 by (fast_tac (comp_cs addIs [equalityI]) 1); |
|
224 val right_comp_id = result(); |
|
225 |
|
226 |
|
227 (** Composition preserves functions, injections, and surjections **) |
|
228 |
|
229 goal Perm.thy "!!f g. [| g: A->B; f: B->C |] ==> (f O g) : A->C"; |
|
230 by (REPEAT (ares_tac [PiI,comp_rel,ex1I,compI] 1 |
|
231 ORELSE eresolve_tac [fun_is_rel,apply_Pair,apply_type] 1)); |
|
232 by (fast_tac (comp_cs addDs [apply_equality]) 1); |
|
233 val comp_func = result(); |
|
234 |
|
235 goal Perm.thy "!!f g. [| g: A->B; f: B->C; a:A |] ==> (f O g)`a = f`(g`a)"; |
|
236 by (REPEAT (ares_tac [comp_func,apply_equality,compI, |
|
237 apply_Pair,apply_type] 1)); |
|
238 val comp_func_apply = result(); |
|
239 |
|
240 goalw Perm.thy [inj_def] |
|
241 "!!f g. [| g: inj(A,B); f: inj(B,C) |] ==> (f O g) : inj(A,C)"; |
|
242 by (REPEAT (eresolve_tac [bspec RS bspec RS mp, box_equals] 1 |
|
243 ORELSE step_tac (ZF_cs addSIs [comp_func,apply_type,comp_func_apply]) 1)); |
|
244 val comp_inj = result(); |
|
245 |
|
246 goalw Perm.thy [surj_def] |
|
247 "!!f g. [| g: surj(A,B); f: surj(B,C) |] ==> (f O g) : surj(A,C)"; |
|
248 by (best_tac (ZF_cs addSIs [comp_func,comp_func_apply]) 1); |
|
249 val comp_surj = result(); |
|
250 |
|
251 goalw Perm.thy [bij_def] |
|
252 "!!f g. [| g: bij(A,B); f: bij(B,C) |] ==> (f O g) : bij(A,C)"; |
|
253 by (fast_tac (ZF_cs addIs [comp_inj,comp_surj]) 1); |
|
254 val comp_bij = result(); |
|
255 |
|
256 |
|
257 (** Dual properties of inj and surj -- useful for proofs from |
|
258 D Pastre. Automatic theorem proving in set theory. |
|
259 Artificial Intelligence, 10:1--27, 1978. **) |
|
260 |
|
261 goalw Perm.thy [inj_def] |
|
262 "!!f g. [| (f O g): inj(A,C); g: A->B; f: B->C |] ==> g: inj(A,B)"; |
|
263 by (safe_tac comp_cs); |
|
264 by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1)); |
|
265 by (ASM_SIMP_TAC (ZF_ss addrews [comp_func_apply]) 1); |
|
266 val comp_mem_injD1 = result(); |
|
267 |
|
268 goalw Perm.thy [inj_def,surj_def] |
|
269 "!!f g. [| (f O g): inj(A,C); g: surj(A,B); f: B->C |] ==> f: inj(B,C)"; |
|
270 by (safe_tac comp_cs); |
|
271 by (res_inst_tac [("x1", "x")] (bspec RS bexE) 1); |
|
272 by (eres_inst_tac [("x1", "w")] (bspec RS bexE) 3); |
|
273 by (REPEAT (assume_tac 1)); |
|
274 by (safe_tac (comp_cs addSIs ZF_congs)); |
|
275 by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1)); |
|
276 by (ASM_SIMP_TAC (ZF_ss addrews [comp_func_apply]) 1); |
|
277 val comp_mem_injD2 = result(); |
|
278 |
|
279 goalw Perm.thy [surj_def] |
|
280 "!!f g. [| (f O g): surj(A,C); g: A->B; f: B->C |] ==> f: surj(B,C)"; |
|
281 by (fast_tac (comp_cs addSIs [comp_func_apply RS sym, apply_type]) 1); |
|
282 val comp_mem_surjD1 = result(); |
|
283 |
|
284 goal Perm.thy |
|
285 "!!f g. [| (f O g)`a = c; g: A->B; f: B->C; a:A |] ==> f`(g`a) = c"; |
|
286 by (REPEAT (ares_tac [comp_func_apply RS sym RS trans] 1)); |
|
287 val comp_func_applyD = result(); |
|
288 |
|
289 goalw Perm.thy [inj_def,surj_def] |
|
290 "!!f g. [| (f O g): surj(A,C); g: A->B; f: inj(B,C) |] ==> g: surj(A,B)"; |
|
291 by (safe_tac comp_cs); |
|
292 by (eres_inst_tac [("x1", "f`y")] (bspec RS bexE) 1); |
|
293 by (REPEAT (ares_tac [apply_type] 1 ORELSE dtac comp_func_applyD 1)); |
|
294 by (best_tac (comp_cs addSIs [apply_type]) 1); |
|
295 val comp_mem_surjD2 = result(); |
|
296 |
|
297 |
|
298 (** inverses of composition **) |
|
299 |
|
300 (*left inverse of composition; one inclusion is |
|
301 f: A->B ==> id(A) <= converse(f) O f *) |
|
302 val [prem] = goal Perm.thy |
|
303 "f: inj(A,B) ==> converse(f) O f = id(A)"; |
|
304 val injfD = prem RSN (3,inj_equality); |
|
305 by (cut_facts_tac [prem RS inj_is_fun] 1); |
|
306 by (fast_tac (comp_cs addIs [equalityI,apply_Pair] |
|
307 addEs [domain_type, make_elim injfD]) 1); |
|
308 val left_comp_inverse = result(); |
|
309 |
|
310 (*right inverse of composition; one inclusion is |
|
311 f: A->B ==> f O converse(f) <= id(B) *) |
|
312 val [prem] = goalw Perm.thy [surj_def] |
|
313 "f: surj(A,B) ==> f O converse(f) = id(B)"; |
|
314 val appfD = (prem RS CollectD1) RSN (3,apply_equality2); |
|
315 by (cut_facts_tac [prem] 1); |
|
316 by (rtac equalityI 1); |
|
317 by (best_tac (comp_cs addEs [domain_type, range_type, make_elim appfD]) 1); |
|
318 by (best_tac (comp_cs addIs [apply_Pair]) 1); |
|
319 val right_comp_inverse = result(); |
|
320 |
|
321 (*Injective case applies converse(f) to both sides then simplifies |
|
322 using left_inverse_lemma*) |
|
323 goalw Perm.thy [bij_def,inj_def,surj_def] |
|
324 "!!f A B. [| converse(f): B->A; f: A->B |] ==> f : bij(A,B)"; |
|
325 val cf_cong = read_instantiate_sg (sign_of Perm.thy) |
|
326 [("t","%x.?f`x")] subst_context; |
|
327 by (fast_tac (ZF_cs addIs [left_inverse_lemma, right_inverse_lemma, apply_type] |
|
328 addEs [cf_cong RS box_equals]) 1); |
|
329 val invertible_imp_bijective = result(); |
|
330 |
|
331 (** Unions of functions -- cf similar theorems on func.ML **) |
|
332 |
|
333 goal Perm.thy "converse(r Un s) = converse(r) Un converse(s)"; |
|
334 by (rtac equalityI 1); |
|
335 by (DEPTH_SOLVE_1 |
|
336 (resolve_tac [Un_least,converse_mono, Un_upper1,Un_upper2] 2)); |
|
337 by (fast_tac ZF_cs 1); |
|
338 val converse_of_Un = result(); |
|
339 |
|
340 goalw Perm.thy [surj_def] |
|
341 "!!f g. [| f: surj(A,B); g: surj(C,D); A Int C = 0 |] ==> \ |
|
342 \ (f Un g) : surj(A Un C, B Un D)"; |
|
343 by (DEPTH_SOLVE_1 (eresolve_tac [fun_disjoint_apply1, fun_disjoint_apply2] 1 |
|
344 ORELSE ball_tac 1 |
|
345 ORELSE (rtac trans 1 THEN atac 2) |
|
346 ORELSE step_tac (ZF_cs addIs [fun_disjoint_Un]) 1)); |
|
347 val surj_disjoint_Un = result(); |
|
348 |
|
349 (*A simple, high-level proof; the version for injections follows from it, |
|
350 using f:inj(A,B)<->f:bij(A,range(f)) *) |
|
351 goal Perm.thy |
|
352 "!!f g. [| f: bij(A,B); g: bij(C,D); A Int C = 0; B Int D = 0 |] ==> \ |
|
353 \ (f Un g) : bij(A Un C, B Un D)"; |
|
354 by (rtac invertible_imp_bijective 1); |
|
355 by (rtac (converse_of_Un RS ssubst) 1); |
|
356 by (REPEAT (ares_tac [fun_disjoint_Un, bij_is_fun, bij_converse_bij] 1)); |
|
357 val bij_disjoint_Un = result(); |
|
358 |
|
359 |
|
360 (** Restrictions as surjections and bijections *) |
|
361 |
|
362 val prems = goalw Perm.thy [surj_def] |
|
363 "f: Pi(A,B) ==> f: surj(A, f``A)"; |
|
364 val rls = apply_equality :: (prems RL [apply_Pair,Pi_type]); |
|
365 by (fast_tac (ZF_cs addIs rls) 1); |
|
366 val surj_image = result(); |
|
367 |
|
368 goal Perm.thy |
|
369 "!!f. [| f: Pi(C,B); A<=C |] ==> restrict(f,A)``A = f``A"; |
|
370 by (rtac equalityI 1); |
|
371 by (SELECT_GOAL (rewtac restrict_def) 2); |
|
372 by (REPEAT (eresolve_tac [imageE, apply_equality RS subst] 2 |
|
373 ORELSE ares_tac [subsetI,lamI,imageI] 2)); |
|
374 by (REPEAT (ares_tac [image_mono,restrict_subset,subset_refl] 1)); |
|
375 val restrict_image = result(); |
|
376 |
|
377 goalw Perm.thy [inj_def] |
|
378 "!!f. [| f: inj(A,B); C<=A |] ==> restrict(f,C): inj(C,B)"; |
|
379 by (safe_tac (ZF_cs addSEs [restrict_type2])); |
|
380 by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp, subsetD, |
|
381 box_equals, restrict] 1)); |
|
382 val restrict_inj = result(); |
|
383 |
|
384 val prems = goal Perm.thy |
|
385 "[| f: Pi(A,B); C<=A |] ==> restrict(f,C): surj(C, f``C)"; |
|
386 by (rtac (restrict_image RS subst) 1); |
|
387 by (rtac (restrict_type2 RS surj_image) 3); |
|
388 by (REPEAT (resolve_tac prems 1)); |
|
389 val restrict_surj = result(); |
|
390 |
|
391 goalw Perm.thy [inj_def,bij_def] |
|
392 "!!f. [| f: inj(A,B); C<=A |] ==> restrict(f,C): bij(C, f``C)"; |
|
393 by (safe_tac ZF_cs); |
|
394 by (REPEAT (eresolve_tac [bspec RS bspec RS mp, subsetD, |
|
395 box_equals, restrict] 1 |
|
396 ORELSE ares_tac [surj_is_fun,restrict_surj] 1)); |
|
397 val restrict_bij = result(); |
|
398 |
|
399 |
|
400 (*** Lemmas for Ramsey's Theorem ***) |
|
401 |
|
402 goalw Perm.thy [inj_def] "!!f. [| f: inj(A,B); B<=D |] ==> f: inj(A,D)"; |
|
403 by (fast_tac (ZF_cs addSEs [fun_weaken_type]) 1); |
|
404 val inj_weaken_type = result(); |
|
405 |
|
406 val [major] = goal Perm.thy |
|
407 "[| f: inj(succ(m), A) |] ==> restrict(f,m) : inj(m, A-{f`m})"; |
|
408 by (rtac (major RS restrict_bij RS bij_is_inj RS inj_weaken_type) 1); |
|
409 by (fast_tac ZF_cs 1); |
|
410 by (cut_facts_tac [major] 1); |
|
411 by (rewtac inj_def); |
|
412 by (safe_tac ZF_cs); |
|
413 by (etac range_type 1); |
|
414 by (assume_tac 1); |
|
415 by (dtac apply_equality 1); |
|
416 by (assume_tac 1); |
|
417 by (res_inst_tac [("a","m")] mem_anti_refl 1); |
|
418 by (fast_tac ZF_cs 1); |
|
419 val inj_succ_restrict = result(); |
|
420 |
|
421 goalw Perm.thy [inj_def] |
|
422 "!!f. [| f: inj(A,B); ~ a:A; ~ b:B |] ==> \ |
|
423 \ cons(<a,b>,f) : inj(cons(a,A), cons(b,B))"; |
|
424 (*cannot use safe_tac: must preserve the implication*) |
|
425 by (etac CollectE 1); |
|
426 by (rtac CollectI 1); |
|
427 by (etac fun_extend 1); |
|
428 by (REPEAT (ares_tac [ballI] 1)); |
|
429 by (REPEAT_FIRST (eresolve_tac [consE,ssubst])); |
|
430 (*Assumption ALL w:A. ALL x:A. f`w = f`x --> w=x makes ASM_SIMP_TAC loop!*) |
|
431 by (ALLGOALS (SIMP_TAC (ZF_ss addrews [fun_extend_apply2,fun_extend_apply1]))); |
|
432 by (ALLGOALS (fast_tac (ZF_cs addIs [apply_type]))); |
|
433 val inj_extend = result(); |