163 by (rtac (jmemA RS RepFunI RS Ord_Inter) 1); |
170 by (rtac (jmemA RS RepFunI RS Ord_Inter) 1); |
164 by (etac RepFunE 1); |
171 by (etac RepFunE 1); |
165 by (etac ssubst 1); |
172 by (etac ssubst 1); |
166 by (eresolve_tac prems 1); |
173 by (eresolve_tac prems 1); |
167 val Ord_INT = result(); |
174 val Ord_INT = result(); |
|
175 |
|
176 |
|
177 (*** < is 'less than' for ordinals ***) |
|
178 |
|
179 goalw Ord.thy [lt_def] "!!i j. [| i:j; Ord(j) |] ==> i<j"; |
|
180 by (REPEAT (ares_tac [conjI] 1)); |
|
181 val ltI = result(); |
|
182 |
|
183 val major::prems = goalw Ord.thy [lt_def] |
|
184 "[| i<j; [| i:j; Ord(i); Ord(j) |] ==> P |] ==> P"; |
|
185 by (rtac (major RS conjE) 1); |
|
186 by (REPEAT (ares_tac (prems@[Ord_in_Ord]) 1)); |
|
187 val ltE = result(); |
|
188 |
|
189 goal Ord.thy "!!i j. i<j ==> i:j"; |
|
190 by (etac ltE 1); |
|
191 by (assume_tac 1); |
|
192 val ltD = result(); |
|
193 |
|
194 goalw Ord.thy [lt_def] "~ i<0"; |
|
195 by (fast_tac ZF_cs 1); |
|
196 val not_lt0 = result(); |
|
197 |
|
198 (* i<0 ==> R *) |
|
199 val lt0E = standard (not_lt0 RS notE); |
|
200 |
|
201 goal Ord.thy "!!i j k. [| i<j; j<k |] ==> i<k"; |
|
202 by (fast_tac (ZF_cs addSIs [ltI] addSEs [ltE, Ord_trans]) 1); |
|
203 val lt_trans = result(); |
|
204 |
|
205 goalw Ord.thy [lt_def] "!!i j. [| i<j; j<i |] ==> P"; |
|
206 by (REPEAT (eresolve_tac [asm_rl, conjE, mem_anti_sym] 1)); |
|
207 val lt_anti_sym = result(); |
|
208 |
|
209 val lt_anti_refl = prove_goal Ord.thy "i<i ==> P" |
|
210 (fn [major]=> [ (rtac (major RS (major RS lt_anti_sym)) 1) ]); |
|
211 |
|
212 val lt_not_refl = prove_goal Ord.thy "~ i<i" |
|
213 (fn _=> [ (rtac notI 1), (etac lt_anti_refl 1) ]); |
|
214 |
|
215 (** le is less than or equals; recall i le j abbrevs i<succ(j) !! **) |
|
216 |
|
217 goalw Ord.thy [lt_def] "i le j <-> i<j | (i=j & Ord(j))"; |
|
218 by (fast_tac (ZF_cs addSIs [Ord_succ] addSDs [Ord_succD]) 1); |
|
219 val le_iff = result(); |
|
220 |
|
221 goal Ord.thy "!!i j. i<j ==> i le j"; |
|
222 by (asm_simp_tac (ZF_ss addsimps [le_iff]) 1); |
|
223 val leI = result(); |
|
224 |
|
225 goal Ord.thy "!!i. [| i=j; Ord(j) |] ==> i le j"; |
|
226 by (asm_simp_tac (ZF_ss addsimps [le_iff]) 1); |
|
227 val le_eqI = result(); |
|
228 |
|
229 val le_refl = refl RS le_eqI; |
|
230 |
|
231 val [prem] = goal Ord.thy "(~ (i=j & Ord(j)) ==> i<j) ==> i le j"; |
|
232 by (rtac (disjCI RS (le_iff RS iffD2)) 1); |
|
233 by (etac prem 1); |
|
234 val leCI = result(); |
|
235 |
|
236 val major::prems = goal Ord.thy |
|
237 "[| i le j; i<j ==> P; [| i=j; Ord(j) |] ==> P |] ==> P"; |
|
238 by (rtac (major RS (le_iff RS iffD1 RS disjE)) 1); |
|
239 by (DEPTH_SOLVE (ares_tac prems 1 ORELSE etac conjE 1)); |
|
240 val leE = result(); |
|
241 |
|
242 goal Ord.thy "!!i j. [| i le j; j le i |] ==> i=j"; |
|
243 by (asm_full_simp_tac (ZF_ss addsimps [le_iff]) 1); |
|
244 by (fast_tac (ZF_cs addEs [lt_anti_sym]) 1); |
|
245 val le_asym = result(); |
|
246 |
|
247 goal Ord.thy "i le 0 <-> i=0"; |
|
248 by (fast_tac (ZF_cs addSIs [Ord_0 RS le_refl] addSEs [leE, lt0E]) 1); |
|
249 val le0_iff = result(); |
|
250 |
|
251 val le0D = standard (le0_iff RS iffD1); |
|
252 |
|
253 val lt_cs = |
|
254 ZF_cs addSIs [le_refl, leCI] |
|
255 addSDs [le0D] |
|
256 addSEs [lt_anti_refl, lt0E, leE]; |
168 |
257 |
169 |
258 |
170 (*** Natural Deduction rules for Memrel ***) |
259 (*** Natural Deduction rules for Memrel ***) |
171 |
260 |
172 goalw Ord.thy [Memrel_def] "<a,b> : Memrel(A) <-> a:b & a:A & b:A"; |
261 goalw Ord.thy [Memrel_def] "<a,b> : Memrel(A) <-> a:b & a:A & b:A"; |
252 ORELSE eresolve_tac [impE,disjE,allE] 1 |
341 ORELSE eresolve_tac [impE,disjE,allE] 1 |
253 ORELSE hyp_subst_tac 1 |
342 ORELSE hyp_subst_tac 1 |
254 ORELSE Ord_trans_tac 1)); |
343 ORELSE Ord_trans_tac 1)); |
255 val Ord_linear_lemma = result(); |
344 val Ord_linear_lemma = result(); |
256 |
345 |
257 val ordi::ordj::prems = goal Ord.thy |
346 (*The trichotomy law for ordinals!*) |
258 "[| Ord(i); Ord(j); i:j ==> P; i=j ==> P; j:i ==> P |] \ |
347 val ordi::ordj::prems = goalw Ord.thy [lt_def] |
259 \ ==> P"; |
348 "[| Ord(i); Ord(j); i<j ==> P; i=j ==> P; j<i ==> P |] ==> P"; |
260 by (rtac (ordi RS Ord_linear_lemma RS spec RS impE) 1); |
349 by (rtac ([ordi,ordj] MRS (Ord_linear_lemma RS spec RS impE)) 1); |
261 by (rtac ordj 1); |
350 by (REPEAT (FIRSTGOAL (etac disjE))); |
262 by (REPEAT (eresolve_tac (prems@[asm_rl,disjE]) 1)); |
351 by (DEPTH_SOLVE (ares_tac ([ordi,ordj,conjI] @ prems) 1)); |
263 val Ord_linear = result(); |
352 val Ord_linear_lt = result(); |
264 |
353 |
265 val prems = goal Ord.thy |
354 val prems = goal Ord.thy |
266 "[| Ord(i); Ord(j); i<=j ==> P; j<=i ==> P |] \ |
355 "[| Ord(i); Ord(j); i le j ==> P; j le i ==> P |] ==> P"; |
267 \ ==> P"; |
356 by (res_inst_tac [("i","i"),("j","j")] Ord_linear_lt 1); |
268 by (res_inst_tac [("i","i"),("j","j")] Ord_linear 1); |
357 by (DEPTH_SOLVE (ares_tac ([leI,le_eqI] @ prems) 1)); |
269 by (DEPTH_SOLVE (ares_tac (prems@[subset_refl]) 1 |
358 val Ord_linear_le = result(); |
270 ORELSE eresolve_tac [asm_rl,OrdmemD,ssubst] 1)); |
359 |
271 val Ord_subset = result(); |
360 goal Ord.thy "!!i j. j le i ==> ~ i<j"; |
272 |
361 by (fast_tac (lt_cs addEs [lt_anti_sym]) 1); |
273 goal Ord.thy "!!i j. [| j<=i; ~ i<=j; Ord(i); Ord(j) |] ==> j:i"; |
362 val le_imp_not_lt = result(); |
274 by (etac Ord_linear 1); |
363 |
275 by (REPEAT (ares_tac [subset_refl] 1 |
364 goal Ord.thy "!!i j. [| ~ i<j; Ord(i); Ord(j) |] ==> j le i"; |
276 ORELSE eresolve_tac [notE,OrdmemD,ssubst] 1)); |
365 by (res_inst_tac [("i","i"),("j","j")] Ord_linear_le 1); |
277 val Ord_member = result(); |
366 by (REPEAT (SOMEGOAL assume_tac)); |
278 |
367 by (fast_tac (lt_cs addEs [lt_anti_sym]) 1); |
279 val [prem] = goal Ord.thy "Ord(i) ==> 0: succ(i)"; |
368 val not_lt_imp_le = result(); |
280 by (rtac (empty_subsetI RS Ord_member) 1); |
369 |
281 by (fast_tac ZF_cs 1); |
370 goal Ord.thy "!!i j. [| Ord(i); Ord(j) |] ==> ~ i<j <-> j le i"; |
282 by (rtac (prem RS Ord_succ) 1); |
371 by (REPEAT (ares_tac [iffI, le_imp_not_lt, not_lt_imp_le] 1)); |
|
372 val not_lt_iff_le = result(); |
|
373 |
|
374 goal Ord.thy "!!i j. [| Ord(i); Ord(j) |] ==> ~ i le j <-> j<i"; |
|
375 by (asm_simp_tac (ZF_ss addsimps [not_lt_iff_le RS iff_sym]) 1); |
|
376 val not_le_iff_lt = result(); |
|
377 |
|
378 goal Ord.thy "!!i. Ord(i) ==> 0 le i"; |
|
379 by (etac (not_lt_iff_le RS iffD1) 1); |
|
380 by (REPEAT (resolve_tac [Ord_0, not_lt0] 1)); |
|
381 val Ord_0_le = result(); |
|
382 |
|
383 goal Ord.thy "!!i. [| Ord(i); ~ i=0 |] ==> 0<i"; |
|
384 by (etac (not_le_iff_lt RS iffD1) 1); |
283 by (rtac Ord_0 1); |
385 by (rtac Ord_0 1); |
284 val Ord_0_in_succ = result(); |
386 by (fast_tac lt_cs 1); |
285 |
387 val Ord_0_lt = result(); |
286 goal Ord.thy "!!i j. [| Ord(i); Ord(j) |] ==> j:i <-> j<=i & ~(i<=j)"; |
388 |
287 by (rtac iffI 1); |
389 (*** Results about less-than or equals ***) |
288 by (rtac conjI 1); |
390 |
289 by (etac OrdmemD 1); |
391 (** For ordinals, j<=i (subset) implies j le i (less-than or equals) **) |
290 by (rtac (mem_anti_refl RS notI) 2); |
392 |
291 by (etac subsetD 2); |
393 goal Ord.thy "!!i j. [| j<=i; Ord(i); Ord(j) |] ==> j le i"; |
292 by (REPEAT (eresolve_tac [asm_rl, conjE, Ord_member] 1)); |
394 by (rtac (not_lt_iff_le RS iffD1) 1); |
293 val Ord_member_iff = result(); |
395 by (assume_tac 1); |
294 |
396 by (assume_tac 1); |
295 goal Ord.thy "!!i. Ord(i) ==> 0:i <-> ~ i=0"; |
397 by (fast_tac (ZF_cs addEs [ltE, mem_anti_refl]) 1); |
296 by (etac (Ord_0 RSN (2,Ord_member_iff) RS iff_trans) 1); |
398 val subset_imp_le = result(); |
297 by (fast_tac eq_cs 1); |
399 |
298 val Ord_0_member_iff = result(); |
400 goal Ord.thy "!!i j. i le j ==> i<=j"; |
299 |
401 by (etac leE 1); |
300 (** For ordinals, i: succ(j) means 'less-than or equals' **) |
402 by (fast_tac ZF_cs 2); |
301 |
403 by (fast_tac (subset_cs addIs [OrdmemD] addEs [ltE]) 1); |
302 goal Ord.thy "!!i j. [| j<=i; Ord(i); Ord(j) |] ==> j : succ(i)"; |
404 val le_imp_subset = result(); |
303 by (rtac Ord_member 1); |
405 |
304 by (REPEAT (ares_tac [Ord_succ] 3)); |
406 goal Ord.thy "j le i <-> j<=i & Ord(i) & Ord(j)"; |
305 by (rtac (mem_anti_refl RS notI) 2); |
407 by (fast_tac (ZF_cs addSEs [subset_imp_le, le_imp_subset] |
306 by (etac subsetD 2); |
408 addEs [ltE, make_elim Ord_succD]) 1); |
307 by (ALLGOALS (fast_tac ZF_cs)); |
409 val le_subset_iff = result(); |
308 val member_succI = result(); |
410 |
309 |
411 goal Ord.thy "i le succ(j) <-> i le j | i=succ(j) & Ord(i)"; |
310 (*Recall Ord_succ_subsetI, namely [| i:j; Ord(j) |] ==> succ(i) <= j *) |
412 by (simp_tac (ZF_ss addsimps [le_iff]) 1); |
311 goalw Ord.thy [Transset_def,Ord_def] |
413 by (fast_tac (ZF_cs addIs [Ord_succ] addDs [Ord_succD]) 1); |
312 "!!i j. [| i : succ(j); Ord(j) |] ==> i<=j"; |
414 val le_succ_iff = result(); |
313 by (fast_tac ZF_cs 1); |
415 |
314 val member_succD = result(); |
416 goal Ord.thy "!!i j. [| i le j; j<k |] ==> i<k"; |
315 |
417 by (fast_tac (ZF_cs addEs [leE, lt_trans]) 1); |
316 goal Ord.thy "!!i j. [| Ord(i); Ord(j) |] ==> j:succ(i) <-> j<=i"; |
418 val lt_trans1 = result(); |
317 by (fast_tac (subset_cs addSEs [member_succI, member_succD]) 1); |
419 |
318 val member_succ_iff = result(); |
420 goal Ord.thy "!!i j. [| i<j; j le k |] ==> i<k"; |
319 |
421 by (fast_tac (ZF_cs addEs [leE, lt_trans]) 1); |
320 goal Ord.thy |
422 val lt_trans2 = result(); |
321 "!!i j. [| Ord(i); Ord(j) |] ==> i<=succ(j) <-> i<=j | i=succ(j)"; |
423 |
322 by (asm_simp_tac (ZF_ss addsimps [member_succ_iff RS iff_sym, Ord_succ]) 1); |
424 goal Ord.thy "!!i j. [| i le j; j le k |] ==> i le k"; |
323 by (fast_tac ZF_cs 1); |
425 by (REPEAT (ares_tac [lt_trans1] 1)); |
324 val subset_succ_iff = result(); |
426 val le_trans = result(); |
325 |
427 |
326 goal Ord.thy "!!i j. [| i:succ(j); j:k; Ord(k) |] ==> i:k"; |
428 goal Ord.thy "!!i j. i<j ==> succ(i) le j"; |
327 by (fast_tac (ZF_cs addEs [Ord_trans]) 1); |
429 by (rtac (not_lt_iff_le RS iffD1) 1); |
328 val Ord_trans1 = result(); |
430 by (fast_tac (lt_cs addEs [lt_anti_sym]) 3); |
329 |
431 by (ALLGOALS (fast_tac (ZF_cs addEs [ltE] addIs [Ord_succ]))); |
330 goal Ord.thy "!!i j. [| i:j; j:succ(k); Ord(k) |] ==> i:k"; |
432 val succ_leI = result(); |
331 by (fast_tac (ZF_cs addEs [Ord_trans]) 1); |
433 |
332 val Ord_trans2 = result(); |
434 goal Ord.thy "!!i j. succ(i) le j ==> i<j"; |
333 |
435 by (rtac (not_le_iff_lt RS iffD1) 1); |
334 goal Ord.thy "!!i jk. [| i:j; j<=k; Ord(k) |] ==> i:k"; |
436 by (fast_tac (lt_cs addEs [lt_anti_sym]) 3); |
335 by (fast_tac (ZF_cs addEs [Ord_trans]) 1); |
437 by (ALLGOALS (fast_tac (ZF_cs addEs [ltE, make_elim Ord_succD]))); |
336 val Ord_transsub2 = result(); |
438 val succ_leE = result(); |
337 |
439 |
338 goal Ord.thy "!!i j. [| i:j; Ord(j) |] ==> succ(i) : succ(j)"; |
440 goal Ord.thy "succ(i) le j <-> i<j"; |
339 by (rtac member_succI 1); |
441 by (REPEAT (ares_tac [iffI,succ_leI,succ_leE] 1)); |
340 by (REPEAT (ares_tac [subsetI,Ord_succ,Ord_in_Ord] 1 |
442 val succ_le_iff = result(); |
341 ORELSE eresolve_tac [succE,Ord_trans,ssubst] 1)); |
|
342 val succ_mem_succI = result(); |
|
343 |
|
344 goal Ord.thy "!!i j. [| succ(i) : succ(j); Ord(j) |] ==> i:j"; |
|
345 by (REPEAT (eresolve_tac [asm_rl, make_elim member_succD, succ_subsetE] 1)); |
|
346 val succ_mem_succE = result(); |
|
347 |
|
348 goal Ord.thy "!!i j. Ord(j) ==> succ(i) : succ(j) <-> i:j"; |
|
349 by (REPEAT (ares_tac [iffI,succ_mem_succI,succ_mem_succE] 1)); |
|
350 val succ_mem_succ_iff = result(); |
|
351 |
|
352 goal Ord.thy "!!i j. [| i<=j; Ord(i); Ord(j) |] ==> succ(i) <= succ(j)"; |
|
353 by (rtac (member_succI RS succ_mem_succI RS member_succD) 1); |
|
354 by (REPEAT (ares_tac [Ord_succ] 1)); |
|
355 val Ord_succ_mono = result(); |
|
356 |
443 |
357 (** Union and Intersection **) |
444 (** Union and Intersection **) |
358 |
445 |
359 goal Ord.thy "!!i j k. [| i:k; j:k; Ord(k) |] ==> i Un j : k"; |
446 (*Replacing k by succ(k') yields the similar rule for le!*) |
360 by (res_inst_tac [("i","i"),("j","j")] Ord_subset 1); |
447 goal Ord.thy "!!i j k. [| i<k; j<k |] ==> i Un j < k"; |
361 by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1)); |
448 by (res_inst_tac [("i","i"),("j","j")] Ord_linear_le 1); |
362 by (asm_simp_tac (ZF_ss addsimps [subset_Un_iff RS iffD1]) 1); |
449 by (rtac (Un_commute RS ssubst) 4); |
363 by (rtac (Un_commute RS ssubst) 1); |
450 by (asm_full_simp_tac (ZF_ss addsimps [le_subset_iff, subset_Un_iff]) 4); |
364 by (asm_simp_tac (ZF_ss addsimps [subset_Un_iff RS iffD1]) 1); |
451 by (asm_full_simp_tac (ZF_ss addsimps [le_subset_iff, subset_Un_iff]) 3); |
365 val Ord_member_UnI = result(); |
452 by (REPEAT (eresolve_tac [asm_rl, ltE] 1)); |
366 |
453 val Un_least_lt = result(); |
367 goal Ord.thy "!!i j k. [| i:k; j:k; Ord(k) |] ==> i Int j : k"; |
454 |
368 by (res_inst_tac [("i","i"),("j","j")] Ord_subset 1); |
455 (*Replacing k by succ(k') yields the similar rule for le!*) |
369 by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1)); |
456 goal Ord.thy "!!i j k. [| i<k; j<k |] ==> i Int j < k"; |
370 by (asm_simp_tac (ZF_ss addsimps [subset_Int_iff RS iffD1]) 1); |
457 by (res_inst_tac [("i","i"),("j","j")] Ord_linear_le 1); |
371 by (rtac (Int_commute RS ssubst) 1); |
458 by (rtac (Int_commute RS ssubst) 4); |
372 by (asm_simp_tac (ZF_ss addsimps [subset_Int_iff RS iffD1]) 1); |
459 by (asm_full_simp_tac (ZF_ss addsimps [le_subset_iff, subset_Int_iff]) 4); |
373 val Ord_member_IntI = result(); |
460 by (asm_full_simp_tac (ZF_ss addsimps [le_subset_iff, subset_Int_iff]) 3); |
374 |
461 by (REPEAT (eresolve_tac [asm_rl, ltE] 1)); |
|
462 val Int_greatest_lt = result(); |
375 |
463 |
376 (*** Results about limits ***) |
464 (*** Results about limits ***) |
377 |
465 |
378 val prems = goal Ord.thy "[| !!i. i:A ==> Ord(i) |] ==> Ord(Union(A))"; |
466 val prems = goal Ord.thy "[| !!i. i:A ==> Ord(i) |] ==> Ord(Union(A))"; |
379 by (rtac (Ord_is_Transset RS Transset_Union_family RS OrdI) 1); |
467 by (rtac (Ord_is_Transset RS Transset_Union_family RS OrdI) 1); |
385 by (etac RepFunE 1); |
473 by (etac RepFunE 1); |
386 by (etac ssubst 1); |
474 by (etac ssubst 1); |
387 by (eresolve_tac prems 1); |
475 by (eresolve_tac prems 1); |
388 val Ord_UN = result(); |
476 val Ord_UN = result(); |
389 |
477 |
390 (*The upper bound must be a successor ordinal -- |
478 (* No < version; consider (UN i:nat.i)=nat *) |
391 consider that (UN i:nat.i)=nat although nat is an upper bound of each i*) |
|
392 val [ordi,limit] = goal Ord.thy |
479 val [ordi,limit] = goal Ord.thy |
393 "[| Ord(i); !!y. y:A ==> f(y): succ(i) |] ==> (UN y:A. f(y)) : succ(i)"; |
480 "[| Ord(i); !!x. x:A ==> b(x) le i |] ==> (UN x:A. b(x)) le i"; |
394 by (rtac (member_succD RS UN_least RS member_succI) 1); |
481 by (rtac (le_imp_subset RS UN_least RS subset_imp_le) 1); |
395 by (REPEAT (ares_tac [ordi, Ord_UN, ordi RS Ord_succ RS Ord_in_Ord, |
482 by (REPEAT (ares_tac [ordi, Ord_UN, limit] 1 ORELSE etac (limit RS ltE) 1)); |
396 limit] 1)); |
483 val UN_least_le = result(); |
397 val sup_least = result(); |
484 |
398 |
485 val [jlti,limit] = goal Ord.thy |
399 val [jmemi,ordi,limit] = goal Ord.thy |
486 "[| j<i; !!x. x:A ==> b(x)<j |] ==> (UN x:A. succ(b(x))) < i"; |
400 "[| j: i; Ord(i); !!y. y:A ==> f(y): j |] ==> (UN y:A. succ(f(y))) : i"; |
487 by (rtac (jlti RS ltE) 1); |
401 by (cut_facts_tac [jmemi RS (ordi RS Ord_in_Ord)] 1); |
488 by (rtac (UN_least_le RS lt_trans2) 1); |
402 by (rtac (sup_least RS Ord_trans2) 1); |
489 by (REPEAT (ares_tac [jlti, succ_leI, limit] 1)); |
403 by (REPEAT (ares_tac [jmemi, ordi, succ_mem_succI, limit] 1)); |
490 val UN_succ_least_lt = result(); |
404 val sup_least2 = result(); |
491 |
|
492 val prems = goal Ord.thy |
|
493 "[| a: A; i le b(a); !!x. x:A ==> Ord(b(x)) |] ==> i le (UN x:A. b(x))"; |
|
494 by (resolve_tac (prems RL [ltE]) 1); |
|
495 by (rtac (le_imp_subset RS subset_trans RS subset_imp_le) 1); |
|
496 by (REPEAT (ares_tac (prems @ [UN_upper, Ord_UN]) 1)); |
|
497 val UN_upper_le = result(); |
405 |
498 |
406 goal Ord.thy "!!i. Ord(i) ==> (UN y:i. succ(y)) = i"; |
499 goal Ord.thy "!!i. Ord(i) ==> (UN y:i. succ(y)) = i"; |
407 by (fast_tac (eq_cs addSEs [Ord_trans1]) 1); |
500 by (fast_tac (eq_cs addEs [Ord_trans]) 1); |
408 val Ord_equality = result(); |
501 val Ord_equality = result(); |
409 |
502 |
410 (*Holds for all transitive sets, not just ordinals*) |
503 (*Holds for all transitive sets, not just ordinals*) |
411 goal Ord.thy "!!i. Ord(i) ==> Union(i) <= i"; |
504 goal Ord.thy "!!i. Ord(i) ==> Union(i) <= i"; |
412 by (fast_tac (ZF_cs addSEs [Ord_trans]) 1); |
505 by (fast_tac (ZF_cs addSEs [Ord_trans]) 1); |