equal
deleted
inserted
replaced
392 by (REPEAT (resolve_tac [ballI, impI] 1)); |
392 by (REPEAT (resolve_tac [ballI, impI] 1)); |
393 (** LEVEL 8 **) |
393 (** LEVEL 8 **) |
394 by (resolve_tac [w_Int_eqpoll_m RS eqpoll_m_not_empty RS not_emptyE] 1); |
394 by (resolve_tac [w_Int_eqpoll_m RS eqpoll_m_not_empty RS not_emptyE] 1); |
395 by (EVERY (map Blast_tac [4,3,2,1])); |
395 by (EVERY (map Blast_tac [4,3,2,1])); |
396 by (dresolve_tac [equalityD1 RS subsetD] 1 THEN (assume_tac 1)); |
396 by (dresolve_tac [equalityD1 RS subsetD] 1 THEN (assume_tac 1)); |
397 by (forward_tac [cons_cons_in] 1 THEN REPEAT (assume_tac 1)); |
397 by (ftac cons_cons_in 1 THEN REPEAT (assume_tac 1)); |
398 by (etac ex1_two_eq 1); |
398 by (etac ex1_two_eq 1); |
399 by (REPEAT (blast_tac |
399 by (REPEAT (blast_tac |
400 (claset() addDs [s_subset RS subsetD, in_s_imp_u_in]) 1)); |
400 (claset() addDs [s_subset RS subsetD, in_s_imp_u_in]) 1)); |
401 qed "subset_s_lepoll_w"; |
401 qed "subset_s_lepoll_w"; |
402 |
402 |
479 by (rewtac MM_def); |
479 by (rewtac MM_def); |
480 by (fast_tac (claset() addSDs [unique_superset1, includes RS subsetD]) 1); |
480 by (fast_tac (claset() addSDs [unique_superset1, includes RS subsetD]) 1); |
481 qed "the_in_MM_subset"; |
481 qed "the_in_MM_subset"; |
482 |
482 |
483 Goalw [GG_def] "v : LL ==> GG ` v <= x"; |
483 Goalw [GG_def] "v : LL ==> GG ` v <= x"; |
484 by (forward_tac [the_in_MM_subset] 1); |
484 by (ftac the_in_MM_subset 1); |
485 by (forward_tac [in_LL_eq_Int] 1); |
485 by (ftac in_LL_eq_Int 1); |
486 by (force_tac (claset() addEs [equalityE], simpset()) 1); |
486 by (force_tac (claset() addEs [equalityE], simpset()) 1); |
487 qed "GG_subset"; |
487 qed "GG_subset"; |
488 |
488 |
489 |
489 |
490 Goal "n:nat ==> EX z. z<=y & n eqpoll z"; |
490 Goal "n:nat ==> EX z. z<=y & n eqpoll z"; |
610 by (case_tac "Finite(A)" 1); |
610 by (case_tac "Finite(A)" 1); |
611 by (rtac lemma1 1 THEN REPEAT (assume_tac 1)); |
611 by (rtac lemma1 1 THEN REPEAT (assume_tac 1)); |
612 by (cut_facts_tac [lemma2] 1); |
612 by (cut_facts_tac [lemma2] 1); |
613 by (REPEAT (eresolve_tac [exE, conjE] 1)); |
613 by (REPEAT (eresolve_tac [exE, conjE] 1)); |
614 by (eres_inst_tac [("x","A Un y")] allE 1); |
614 by (eres_inst_tac [("x","A Un y")] allE 1); |
615 by (forward_tac [infinite_Un] 1 THEN (mp_tac 1)); |
615 by (ftac infinite_Un 1 THEN (mp_tac 1)); |
616 by (etac zero_lt_natE 1); by (assume_tac 1); |
616 by (etac zero_lt_natE 1); by (assume_tac 1); |
617 by (Clarify_tac 1); |
617 by (Clarify_tac 1); |
618 by (DEPTH_SOLVE (ares_tac [export conclusion] 1)); |
618 by (DEPTH_SOLVE (ares_tac [export conclusion] 1)); |
619 qed "AC16_WO4"; |
619 qed "AC16_WO4"; |