42 Goalw [WO1_def] "[| WO1; ALL B:A. EX C:D(B). P(C,B) |] \ |
42 Goalw [WO1_def] "[| WO1; ALL B:A. EX C:D(B). P(C,B) |] \ |
43 \ ==> EX f. ALL B:A. P(f`B,B)"; |
43 \ ==> EX f. ALL B:A. P(f`B,B)"; |
44 by (eres_inst_tac [("x","Union({{C:D(B). P(C,B)}. B:A})")] allE 1); |
44 by (eres_inst_tac [("x","Union({{C:D(B). P(C,B)}. B:A})")] allE 1); |
45 by (etac exE 1); |
45 by (etac exE 1); |
46 by (dtac ex_choice_fun 1); |
46 by (dtac ex_choice_fun 1); |
47 by (fast_tac (claset() addEs [RepFunE, sym RS equals0D]) 1); |
47 by (fast_tac (claset() addEs [sym RS equals0E]) 1); |
48 by (etac exE 1); |
48 by (etac exE 1); |
49 by (res_inst_tac [("x","lam x:A. f`{C:D(x). P(C,x)}")] exI 1); |
49 by (res_inst_tac [("x","lam x:A. f`{C:D(x). P(C,x)}")] exI 1); |
50 by (Asm_full_simp_tac 1); |
50 by (Asm_full_simp_tac 1); |
51 by (fast_tac (claset() addSDs [RepFunI RSN (2, apply_type)] |
51 by (fast_tac (claset() addSDs [RepFunI RSN (2, apply_type)] |
52 addSEs [CollectD2]) 1); |
52 addSEs [CollectD2]) 1); |
67 THEN (assume_tac 2)); |
67 THEN (assume_tac 2)); |
68 by (fast_tac (claset() addSEs [well_ord_cardinal_eqpoll]) 1); |
68 by (fast_tac (claset() addSEs [well_ord_cardinal_eqpoll]) 1); |
69 val lemma2_1 = result(); |
69 val lemma2_1 = result(); |
70 |
70 |
71 Goal "f : bij(D+D, B) ==> {{f`Inl(i), f`Inr(i)}. i:D} : Pow(Pow(B))"; |
71 Goal "f : bij(D+D, B) ==> {{f`Inl(i), f`Inr(i)}. i:D} : Pow(Pow(B))"; |
72 by (fast_tac (claset() addSIs [InlI, InrI] |
72 by (fast_tac (claset() addSEs [bij_is_fun RS apply_type]) 1); |
73 addSEs [RepFunE, bij_is_fun RS apply_type]) 1); |
|
74 val lemma2_2 = result(); |
73 val lemma2_2 = result(); |
75 |
74 |
76 Goal "[| f:inj(A,B); f`a = f`b; a:A; b:A |] ==> a=b"; |
75 Goal "[| f:inj(A,B); f`a = f`b; a:A; b:A |] ==> a=b"; |
77 by (rtac inj_equality 1); |
76 by (rtac inj_equality 1); |
78 by (TRYALL (fast_tac (claset() addSEs [inj_is_fun RS apply_Pair] addEs [subst]))); |
77 by (TRYALL (fast_tac (claset() addSEs [inj_is_fun RS apply_Pair] addEs [subst]))); |
79 val lemma = result(); |
78 val lemma = result(); |
80 |
79 |
81 Goalw AC_aux_defs |
80 Goalw AC_aux_defs |
82 "f : bij(D+D, B) ==> \ |
81 "f : bij(D+D, B) ==> pairwise_disjoint({{f`Inl(i), f`Inr(i)}. i:D})"; |
83 \ pairwise_disjoint({{f`Inl(i), f`Inr(i)}. i:D})"; |
82 by (blast_tac (claset() addDs [bij_is_inj RS lemma]) 1); |
84 by (fast_tac (claset() addSEs [RepFunE, not_emptyE] |
|
85 addDs [bij_is_inj RS lemma, Inl_iff RS iffD1, |
|
86 Inr_iff RS iffD1, Inl_Inr_iff RS iffD1 RS FalseE, |
|
87 Inr_Inl_iff RS iffD1 RS FalseE] |
|
88 addSIs [InlI, InrI]) 1); |
|
89 val lemma2_3 = result(); |
83 val lemma2_3 = result(); |
90 |
84 |
91 val [major, minor] = goalw thy AC_aux_defs |
85 val [major, minor] = goalw thy AC_aux_defs |
92 "[| f : bij(D+D, B); 1 le n |] ==> \ |
86 "[| f : bij(D+D, B); 1 le n |] ==> \ |
93 \ sets_of_size_between({{f`Inl(i), f`Inr(i)}. i:D}, 2, succ(n))"; |
87 \ sets_of_size_between({{f`Inl(i), f`Inr(i)}. i:D}, 2, succ(n))"; |
94 by (rewtac succ_def); |
88 by (rewtac succ_def); |
95 by (fast_tac (claset() |
89 by (fast_tac (claset() |
96 addSIs [cons_lepoll_cong, minor, lepoll_refl, InlI, InrI] |
90 addSIs [cons_lepoll_cong, minor, lepoll_refl] |
97 addIs [singleton_eqpoll_1 RS eqpoll_imp_lepoll RS lepoll_trans, |
91 addIs [singleton_eqpoll_1 RS eqpoll_imp_lepoll RS lepoll_trans, |
98 le_imp_subset RS subset_imp_lepoll] |
92 le_imp_subset RS subset_imp_lepoll] |
99 addDs [major RS bij_is_inj RS lemma, Inl_Inr_iff RS iffD1 RS FalseE] |
93 addDs [major RS bij_is_inj RS lemma] |
100 addSEs [RepFunE, not_emptyE, mem_irrefl]) 1); |
94 addSEs [mem_irrefl]) 1); |
101 val lemma2_4 = result(); |
95 val lemma2_4 = result(); |
102 |
96 |
103 Goalw [bij_def, surj_def] |
97 Goalw [bij_def, surj_def] |
104 "f : bij(D+D, B) ==> Union({{f`Inl(i), f`Inr(i)}. i:D})=B"; |
98 "f : bij(D+D, B) ==> Union({{f`Inl(i), f`Inr(i)}. i:D})=B"; |
105 by (fast_tac (claset() addSEs [inj_is_fun RS apply_type]) 1); |
99 by (fast_tac (claset() addSEs [inj_is_fun RS apply_type]) 1); |