99 addSEs [RepFunE, not_emptyE, mem_irrefl]) 1); |
99 addSEs [RepFunE, not_emptyE, mem_irrefl]) 1); |
100 val lemma2_4 = result(); |
100 val lemma2_4 = result(); |
101 |
101 |
102 goalw thy [bij_def, surj_def] |
102 goalw thy [bij_def, surj_def] |
103 "!!f. f : bij(D+D, B) ==> Union({{f`Inl(i), f`Inr(i)}. i:D})=B"; |
103 "!!f. f : bij(D+D, B) ==> Union({{f`Inl(i), f`Inr(i)}. i:D})=B"; |
104 by (fast_tac (!claset addSEs [inj_is_fun RS apply_type, CollectE, sumE] |
104 by (fast_tac (!claset addSEs [inj_is_fun RS apply_type]) 1); |
105 addSIs [InlI, InrI, equalityI]) 1); |
|
106 val lemma2_5 = result(); |
105 val lemma2_5 = result(); |
107 |
106 |
108 goal thy "!!A. [| WO1; ~Finite(B); 1 le n |] \ |
107 goal thy "!!A. [| WO1; ~Finite(B); 1 le n |] \ |
109 \ ==> EX C:Pow(Pow(B)). pairwise_disjoint(C) & \ |
108 \ ==> EX C:Pow(Pow(B)). pairwise_disjoint(C) & \ |
110 \ sets_of_size_between(C, 2, succ(n)) & \ |
109 \ sets_of_size_between(C, 2, succ(n)) & \ |