equal
deleted
inserted
replaced
295 by (eres_inst_tac [("x","B - {xa}")] allE 1); |
295 by (eres_inst_tac [("x","B - {xa}")] allE 1); |
296 by (etac impE 1); |
296 by (etac impE 1); |
297 by (asm_full_simp_tac (!simpset addsimps [add_succ]) 1); |
297 by (asm_full_simp_tac (!simpset addsimps [add_succ]) 1); |
298 by (fast_tac (!claset addSIs [Diff_sing_eqpoll, lepoll_Diff_sing]) 1); |
298 by (fast_tac (!claset addSIs [Diff_sing_eqpoll, lepoll_Diff_sing]) 1); |
299 by (res_inst_tac [("P","%z. z lepoll m")] subst 1 THEN (assume_tac 2)); |
299 by (res_inst_tac [("P","%z. z lepoll m")] subst 1 THEN (assume_tac 2)); |
300 by (fast_tac (!claset addSIs [equalityI]) 1); |
300 by (Fast_tac 1); |
301 val eqpoll_sum_imp_Diff_lepoll_lemma = result(); |
301 val eqpoll_sum_imp_Diff_lepoll_lemma = result(); |
302 |
302 |
303 goal thy "!!k. [| A eqpoll succ(k #+ m); B<=A; succ(k) lepoll B; \ |
303 goal thy "!!k. [| A eqpoll succ(k #+ m); B<=A; succ(k) lepoll B; \ |
304 \ k:nat; m:nat |] \ |
304 \ k:nat; m:nat |] \ |
305 \ ==> A-B lepoll m"; |
305 \ ==> A-B lepoll m"; |
327 by (etac impE 1); |
327 by (etac impE 1); |
328 by (fast_tac (!claset addSIs [Diff_sing_eqpoll, |
328 by (fast_tac (!claset addSIs [Diff_sing_eqpoll, |
329 eqpoll_sym RSN (2, Diff_sing_eqpoll) RS eqpoll_sym] |
329 eqpoll_sym RSN (2, Diff_sing_eqpoll) RS eqpoll_sym] |
330 addss (!simpset addsimps [add_succ])) 1); |
330 addss (!simpset addsimps [add_succ])) 1); |
331 by (res_inst_tac [("P","%z. z eqpoll m")] subst 1 THEN (assume_tac 2)); |
331 by (res_inst_tac [("P","%z. z eqpoll m")] subst 1 THEN (assume_tac 2)); |
332 by (fast_tac (!claset addSIs [equalityI]) 1); |
332 by (Fast_tac 1); |
333 val eqpoll_sum_imp_Diff_eqpoll_lemma = result(); |
333 val eqpoll_sum_imp_Diff_eqpoll_lemma = result(); |
334 |
334 |
335 goal thy "!!k. [| A eqpoll succ(k #+ m); B<=A; succ(k) eqpoll B; \ |
335 goal thy "!!k. [| A eqpoll succ(k #+ m); B<=A; succ(k) eqpoll B; \ |
336 \ k:nat; m:nat |] \ |
336 \ k:nat; m:nat |] \ |
337 \ ==> A-B eqpoll m"; |
337 \ ==> A-B eqpoll m"; |
345 (* back to the second part *) |
345 (* back to the second part *) |
346 (* ********************************************************************** *) |
346 (* ********************************************************************** *) |
347 |
347 |
348 goal thy "!!w. [| x Int y = 0; w <= x Un y |] \ |
348 goal thy "!!w. [| x Int y = 0; w <= x Un y |] \ |
349 \ ==> w Int (x - {u}) = w - cons(u, w Int y)"; |
349 \ ==> w Int (x - {u}) = w - cons(u, w Int y)"; |
350 by (fast_tac (!claset addSIs [equalityI] addEs [equals0D]) 1); |
350 by (fast_tac (!claset addEs [equals0D]) 1); |
351 val w_Int_eq_w_Diff = result(); |
351 val w_Int_eq_w_Diff = result(); |
352 |
352 |
353 goal thy "!!w. [| w:{v:s_u(u, t_n, succ(l), y). a <= v}; \ |
353 goal thy "!!w. [| w:{v:s_u(u, t_n, succ(l), y). a <= v}; \ |
354 \ l eqpoll a; t_n <= {v:Pow(x Un y). v eqpoll succ(succ(l) #+ m)}; \ |
354 \ l eqpoll a; t_n <= {v:Pow(x Un y). v eqpoll succ(succ(l) #+ m)}; \ |
355 \ m:nat; l:nat; x Int y = 0; u : x; \ |
355 \ m:nat; l:nat; x Int y = 0; u : x; \ |
438 (* LL can be well ordered *) |
438 (* LL can be well ordered *) |
439 (* ********************************************************************** *) |
439 (* ********************************************************************** *) |
440 |
440 |
441 goal thy "{x:Pow(X). x lepoll 0} = {0}"; |
441 goal thy "{x:Pow(X). x lepoll 0} = {0}"; |
442 by (fast_tac (!claset addSDs [lepoll_0_is_0] |
442 by (fast_tac (!claset addSDs [lepoll_0_is_0] |
443 addSIs [lepoll_refl, equalityI]) 1); |
443 addSIs [lepoll_refl]) 1); |
444 val subsets_lepoll_0_eq_unit = result(); |
444 val subsets_lepoll_0_eq_unit = result(); |
445 |
445 |
446 goal thy "!!X. [| well_ord(X, R); ~Finite(X); n:nat |] \ |
446 goal thy "!!X. [| well_ord(X, R); ~Finite(X); n:nat |] \ |
447 \ ==> EX S. well_ord({Y: Pow(X) . Y eqpoll succ(n)}, S)"; |
447 \ ==> EX S. well_ord({Y: Pow(X) . Y eqpoll succ(n)}, S)"; |
448 by (resolve_tac [well_ord_infinite_subsets_eqpoll_X |
448 by (resolve_tac [well_ord_infinite_subsets_eqpoll_X |
451 by (fast_tac (!claset addSEs [bij_is_inj RS well_ord_rvimage]) 1); |
451 by (fast_tac (!claset addSEs [bij_is_inj RS well_ord_rvimage]) 1); |
452 val well_ord_subsets_eqpoll_n = result(); |
452 val well_ord_subsets_eqpoll_n = result(); |
453 |
453 |
454 goal thy "!!n. n:nat ==> {z:Pow(y). z lepoll succ(n)} = \ |
454 goal thy "!!n. n:nat ==> {z:Pow(y). z lepoll succ(n)} = \ |
455 \ {z:Pow(y). z lepoll n} Un {z:Pow(y). z eqpoll succ(n)}"; |
455 \ {z:Pow(y). z lepoll n} Un {z:Pow(y). z eqpoll succ(n)}"; |
456 by (fast_tac (!claset addIs [le_refl, leI, |
456 by (fast_tac (!claset addIs [le_refl, leI, le_imp_lepoll] |
457 le_imp_lepoll, equalityI] |
|
458 addSDs [lepoll_succ_disj] |
457 addSDs [lepoll_succ_disj] |
459 addSEs [nat_into_Ord, lepoll_trans, eqpoll_imp_lepoll]) 1); |
458 addSEs [nat_into_Ord, lepoll_trans, eqpoll_imp_lepoll]) 1); |
460 val subsets_lepoll_succ = result(); |
459 val subsets_lepoll_succ = result(); |
461 |
460 |
462 goal thy "!!n. n:nat ==> \ |
461 goal thy "!!n. n:nat ==> \ |
474 "tot_ord({a},0)"; |
473 "tot_ord({a},0)"; |
475 by (Simp_tac 1); |
474 by (Simp_tac 1); |
476 val tot_ord_unit = result(); |
475 val tot_ord_unit = result(); |
477 |
476 |
478 goalw thy [wf_on_def, wf_def] "wf[{a}](0)"; |
477 goalw thy [wf_on_def, wf_def] "wf[{a}](0)"; |
479 by (fast_tac (!claset addSIs [equalityI]) 1); |
478 by (Fast_tac 1); |
480 val wf_on_unit = result(); |
479 val wf_on_unit = result(); |
481 |
480 |
482 goalw thy [well_ord_def] "well_ord({a},0)"; |
481 goalw thy [well_ord_def] "well_ord({a},0)"; |
483 by (simp_tac (!simpset addsimps [tot_ord_unit, wf_on_unit]) 1); |
482 by (simp_tac (!simpset addsimps [tot_ord_unit, wf_on_unit]) 1); |
484 val well_ord_unit = result(); |
483 val well_ord_unit = result(); |