14 AC12_def, AC13_def, AC14_def, AC15_def, AC16_def, |
14 AC12_def, AC13_def, AC14_def, AC15_def, AC16_def, |
15 AC17_def, AC18_def, AC19_def]; |
15 AC17_def, AC18_def, AC19_def]; |
16 |
16 |
17 val AC_aux_defs = [pairwise_disjoint_def, sets_of_size_between_def]; |
17 val AC_aux_defs = [pairwise_disjoint_def, sets_of_size_between_def]; |
18 |
18 |
19 val AC_cs = OrdQuant_cs; |
|
20 val AC_ss = OrdQuant_ss; |
|
21 |
|
22 (* ******************************************** *) |
19 (* ******************************************** *) |
23 |
20 |
24 (* Theorems analogous to ones presented in "ZF/Ordinal.ML" *) |
21 (* Theorems analogous to ones presented in "ZF/Ordinal.ML" *) |
25 |
22 |
26 (* lemma for nat_le_imp_lepoll *) |
23 (* lemma for nat_le_imp_lepoll *) |
27 val [prem] = goalw Cardinal.thy [lepoll_def] |
24 val [prem] = goalw Cardinal.thy [lepoll_def] |
28 "m:nat ==> ALL n: nat. m le n --> m lepoll n"; |
25 "m:nat ==> ALL n: nat. m le n --> m lepoll n"; |
29 by (nat_ind_tac "m" [prem] 1); |
26 by (nat_ind_tac "m" [prem] 1); |
30 by (fast_tac (ZF_cs addSIs [le_imp_subset RS id_subset_inj]) 1); |
27 by (fast_tac (!claset addSIs [le_imp_subset RS id_subset_inj]) 1); |
31 by (rtac ballI 1); |
28 by (rtac ballI 1); |
32 by (eres_inst_tac [("n","n")] natE 1); |
29 by (eres_inst_tac [("n","n")] natE 1); |
33 by (asm_simp_tac (ZF_ss addsimps [inj_def, succI1 RS Pi_empty2]) 1); |
30 by (asm_simp_tac (!simpset addsimps [inj_def, succI1 RS Pi_empty2]) 1); |
34 by (fast_tac (ZF_cs addSDs [le0D]) 1); |
31 by (fast_tac (!claset addSIs [le_imp_subset RS id_subset_inj]) 1); |
35 by (fast_tac (ZF_cs addSIs [le_imp_subset RS id_subset_inj]) 1); |
|
36 val nat_le_imp_lepoll_lemma = result(); |
32 val nat_le_imp_lepoll_lemma = result(); |
37 |
33 |
38 (* used in : AC10-AC15.ML WO1-WO6.ML WO6WO1.ML*) |
34 (* used in : AC10-AC15.ML WO1-WO6.ML WO6WO1.ML*) |
39 val nat_le_imp_lepoll = nat_le_imp_lepoll_lemma RS bspec RS mp |> standard; |
35 val nat_le_imp_lepoll = nat_le_imp_lepoll_lemma RS bspec RS mp |> standard; |
40 |
36 |
41 (* ********************************************************************** *) |
37 (* ********************************************************************** *) |
42 (* lemmas concerning FOL and pure ZF theory *) |
38 (* lemmas concerning FOL and pure ZF theory *) |
43 (* ********************************************************************** *) |
39 (* ********************************************************************** *) |
44 |
40 |
45 goal thy "!!X. (A->X)=0 ==> X=0"; |
41 goal thy "!!X. (A->X)=0 ==> X=0"; |
46 by (fast_tac (ZF_cs addSIs [equals0I] addEs [lam_type RSN (2, equals0D)]) 1); |
42 by (fast_tac (!claset addSIs [equals0I] addEs [lam_type RSN (2, equals0D)]) 1); |
47 val fun_space_emptyD = result(); |
43 val fun_space_emptyD = result(); |
48 |
44 |
49 (* used only in WO1_DC.ML *) |
45 (* used only in WO1_DC.ML *) |
50 (*Note simpler proof*) |
46 (*Note simpler proof*) |
51 goal ZF.thy "!!A f g. [| ALL x:A. f`x=g`x; f:Df->Cf; g:Dg->Cg; \ |
47 goal upair.thy "!!A f g. [| ALL x:A. f`x=g`x; f:Df->Cf; g:Dg->Cg; \ |
52 \ A<=Df; A<=Dg |] ==> f``A=g``A"; |
48 \ A<=Df; A<=Dg |] ==> f``A=g``A"; |
53 by (asm_simp_tac (ZF_ss addsimps [image_fun]) 1); |
49 by (asm_simp_tac (!simpset addsimps [image_fun]) 1); |
54 val images_eq = result(); |
50 val images_eq = result(); |
55 |
51 |
56 (* used in : AC10-AC15.ML AC16WO4.ML WO6WO1.ML *) |
52 (* used in : AC10-AC15.ML AC16WO4.ML WO6WO1.ML *) |
57 (*I don't know where to put this one.*) |
53 (*I don't know where to put this one.*) |
58 goal Cardinal.thy |
54 goal Cardinal.thy |
61 by (forward_tac [singleton_subsetI] 1); |
57 by (forward_tac [singleton_subsetI] 1); |
62 by (forward_tac [subsetD] 1 THEN (assume_tac 1)); |
58 by (forward_tac [subsetD] 1 THEN (assume_tac 1)); |
63 by (res_inst_tac [("A2","A")] |
59 by (res_inst_tac [("A2","A")] |
64 (Diff_sing_lepoll RSN (2, subset_imp_lepoll RS lepoll_trans)) 1 |
60 (Diff_sing_lepoll RSN (2, subset_imp_lepoll RS lepoll_trans)) 1 |
65 THEN (REPEAT (assume_tac 2))); |
61 THEN (REPEAT (assume_tac 2))); |
66 by (fast_tac ZF_cs 1); |
62 by (Fast_tac 1); |
67 val Diff_lepoll = result(); |
63 val Diff_lepoll = result(); |
68 |
64 |
69 (* ********************************************************************** *) |
65 (* ********************************************************************** *) |
70 (* lemmas concerning lepoll and eqpoll relations *) |
66 (* lemmas concerning lepoll and eqpoll relations *) |
71 (* ********************************************************************** *) |
67 (* ********************************************************************** *) |
75 (* ********************************************************************** *) |
71 (* ********************************************************************** *) |
76 |
72 |
77 (* lemma for ordertype_Int *) |
73 (* lemma for ordertype_Int *) |
78 goalw Cardinal.thy [rvimage_def] "rvimage(A,id(A),r) = r Int A*A"; |
74 goalw Cardinal.thy [rvimage_def] "rvimage(A,id(A),r) = r Int A*A"; |
79 by (rtac equalityI 1); |
75 by (rtac equalityI 1); |
80 by (step_tac ZF_cs 1); |
76 by (Step_tac 1); |
81 by (dres_inst_tac [("P","%a. <id(A)`xb,a>:r")] (id_conv RS subst) 1 |
77 by (dres_inst_tac [("P","%a. <id(A)`xb,a>:r")] (id_conv RS subst) 1 |
82 THEN (assume_tac 1)); |
78 THEN (assume_tac 1)); |
83 by (dres_inst_tac [("P","%a. <a,ya>:r")] (id_conv RS subst) 1 |
79 by (dres_inst_tac [("P","%a. <a,ya>:r")] (id_conv RS subst) 1 |
84 THEN (REPEAT (assume_tac 1))); |
80 THEN (REPEAT (assume_tac 1))); |
85 by (fast_tac (ZF_cs addIs [id_conv RS ssubst]) 1); |
81 by (fast_tac (!claset addIs [id_conv RS ssubst]) 1); |
86 val rvimage_id = result(); |
82 val rvimage_id = result(); |
87 |
83 |
88 (* used only in Hartog.ML *) |
84 (* used only in Hartog.ML *) |
89 goal Cardinal.thy |
85 goal Cardinal.thy |
90 "!!A r. well_ord(A,r) ==> ordertype(A, r Int A*A) = ordertype(A,r)"; |
86 "!!A r. well_ord(A,r) ==> ordertype(A, r Int A*A) = ordertype(A,r)"; |
94 val ordertype_Int = result(); |
90 val ordertype_Int = result(); |
95 |
91 |
96 (* used only in AC16_lemmas.ML *) |
92 (* used only in AC16_lemmas.ML *) |
97 goalw CardinalArith.thy [InfCard_def] |
93 goalw CardinalArith.thy [InfCard_def] |
98 "!!i. [| ~Finite(i); Card(i) |] ==> InfCard(i)"; |
94 "!!i. [| ~Finite(i); Card(i) |] ==> InfCard(i)"; |
99 by (asm_simp_tac (ZF_ss addsimps [Card_is_Ord RS nat_le_infinite_Ord]) 1); |
95 by (asm_simp_tac (!simpset addsimps [Card_is_Ord RS nat_le_infinite_Ord]) 1); |
100 val Inf_Card_is_InfCard = result(); |
96 val Inf_Card_is_InfCard = result(); |
101 |
97 |
102 goal thy "(THE z. {x}={z}) = x"; |
98 goal thy "(THE z. {x}={z}) = x"; |
103 by (fast_tac (AC_cs addSIs [the_equality] |
99 by (fast_tac (!claset addSIs [the_equality] |
104 addSEs [singleton_eq_iff RS iffD1 RS sym]) 1); |
100 addSEs [singleton_eq_iff RS iffD1 RS sym]) 1); |
105 val the_element = result(); |
101 val the_element = result(); |
106 |
102 |
107 goal thy "(lam x:A. {x}) : bij(A, {{x}. x:A})"; |
103 goal thy "(lam x:A. {x}) : bij(A, {{x}. x:A})"; |
108 by (res_inst_tac [("d","%z. THE x. z={x}")] lam_bijective 1); |
104 by (res_inst_tac [("d","%z. THE x. z={x}")] lam_bijective 1); |
109 by (TRYALL (eresolve_tac [RepFunI, RepFunE])); |
105 by (TRYALL (eresolve_tac [RepFunI, RepFunE])); |
110 by (REPEAT (asm_full_simp_tac (AC_ss addsimps [the_element]) 1)); |
106 by (REPEAT (asm_full_simp_tac (!simpset addsimps [the_element]) 1)); |
111 val lam_sing_bij = result(); |
107 val lam_sing_bij = result(); |
112 |
108 |
113 val [major,minor] = goal thy |
109 val [major,minor] = goal thy |
114 "[| f : Pi(A,B); (!!x. x:A ==> B(x)<=C(x)) |] ==> f : Pi(A,C)"; |
110 "[| f : Pi(A,B); (!!x. x:A ==> B(x)<=C(x)) |] ==> f : Pi(A,C)"; |
115 by (fast_tac (AC_cs addSIs [major RS Pi_type, minor RS subsetD, |
111 by (fast_tac (!claset addSIs [major RS Pi_type, minor RS subsetD, |
116 major RS apply_type]) 1); |
112 major RS apply_type]) 1); |
117 val Pi_weaken_type = result(); |
113 val Pi_weaken_type = result(); |
118 |
114 |
119 val [major, minor] = goalw thy [inj_def] |
115 val [major, minor] = goalw thy [inj_def] |
120 "[| f:inj(A, B); (!!a. a:A ==> f`a : C) |] ==> f:inj(A,C)"; |
116 "[| f:inj(A, B); (!!a. a:A ==> f`a : C) |] ==> f:inj(A,C)"; |
121 by (fast_tac (AC_cs addSEs [minor] |
117 by (fast_tac (!claset addSEs [minor] |
122 addSIs [major RS CollectD1 RS Pi_type, major RS CollectD2]) 1); |
118 addSIs [major RS CollectD1 RS Pi_type, major RS CollectD2]) 1); |
123 val inj_strengthen_type = result(); |
119 val inj_strengthen_type = result(); |
124 |
120 |
125 goal thy "A*B=0 <-> A=0 | B=0"; |
121 goal thy "A*B=0 <-> A=0 | B=0"; |
126 by (fast_tac (ZF_cs addSIs [equals0I] addEs [equals0D]) 1); |
122 by (fast_tac (!claset addSIs [equals0I] addEs [equals0D]) 1); |
127 val Sigma_empty_iff = result(); |
123 val Sigma_empty_iff = result(); |
128 |
124 |
129 goalw thy [Finite_def] "!!n. n:nat ==> Finite(n)"; |
125 goalw thy [Finite_def] "!!n. n:nat ==> Finite(n)"; |
130 by (fast_tac (AC_cs addSIs [eqpoll_refl]) 1); |
126 by (fast_tac (!claset addSIs [eqpoll_refl]) 1); |
131 val nat_into_Finite = result(); |
127 val nat_into_Finite = result(); |
132 |
128 |
133 goalw thy [Finite_def] "~Finite(nat)"; |
129 goalw thy [Finite_def] "~Finite(nat)"; |
134 by (fast_tac (AC_cs addSDs [eqpoll_imp_lepoll] |
130 by (fast_tac (!claset addSDs [eqpoll_imp_lepoll] |
135 addIs [Ord_nat RSN (2, ltI) RS lt_not_lepoll RS notE]) 1); |
131 addIs [Ord_nat RSN (2, ltI) RS lt_not_lepoll RS notE]) 1); |
136 val nat_not_Finite = result(); |
132 val nat_not_Finite = result(); |
137 |
133 |
138 val le_imp_lepoll = le_imp_subset RS subset_imp_lepoll; |
134 val le_imp_lepoll = le_imp_subset RS subset_imp_lepoll; |
139 |
135 |
142 (* ********************************************************************** *) |
138 (* ********************************************************************** *) |
143 |
139 |
144 goal thy "!!x. [| EX! x. P(x); P(x); P(y) |] ==> x=y"; |
140 goal thy "!!x. [| EX! x. P(x); P(x); P(y) |] ==> x=y"; |
145 by (etac ex1E 1); |
141 by (etac ex1E 1); |
146 by (res_inst_tac [("b","xa")] (sym RSN (2, trans)) 1); |
142 by (res_inst_tac [("b","xa")] (sym RSN (2, trans)) 1); |
147 by (fast_tac AC_cs 1); |
143 by (Fast_tac 1); |
148 by (fast_tac AC_cs 1); |
144 by (Fast_tac 1); |
149 val ex1_two_eq = result(); |
145 val ex1_two_eq = result(); |
150 |
146 |
151 (* ********************************************************************** *) |
147 (* ********************************************************************** *) |
152 (* image of a surjection *) |
148 (* image of a surjection *) |
153 (* ********************************************************************** *) |
149 (* ********************************************************************** *) |
154 |
150 |
155 goalw thy [surj_def] "!!f. f : surj(A, B) ==> f``A = B"; |
151 goalw thy [surj_def] "!!f. f : surj(A, B) ==> f``A = B"; |
156 by (etac CollectE 1); |
152 by (etac CollectE 1); |
157 by (resolve_tac [subset_refl RSN (2, image_fun) RS ssubst] 1 THEN (assume_tac 1)); |
153 by (resolve_tac [subset_refl RSN (2, image_fun) RS ssubst] 1 THEN (assume_tac 1)); |
158 by (fast_tac (AC_cs addSEs [RepFunE, apply_type] |
154 by (fast_tac (!claset addSEs [RepFunE, apply_type] |
159 addSIs [RepFunI] addIs [equalityI]) 1); |
155 addSIs [RepFunI] addIs [equalityI]) 1); |
160 val surj_image_eq = result(); |
156 val surj_image_eq = result(); |
161 |
157 |
162 |
158 |
163 goal thy "!!y. succ(x) lepoll y ==> y ~= 0"; |
159 goal thy "!!y. succ(x) lepoll y ==> y ~= 0"; |
164 by (fast_tac (ZF_cs addSDs [lepoll_0_is_0]) 1); |
160 by (fast_tac (!claset addSDs [lepoll_0_is_0]) 1); |
165 val succ_lepoll_imp_not_empty = result(); |
161 val succ_lepoll_imp_not_empty = result(); |
166 |
162 |
167 goal thy "!!x. x eqpoll succ(n) ==> x ~= 0"; |
163 goal thy "!!x. x eqpoll succ(n) ==> x ~= 0"; |
168 by (fast_tac (AC_cs addSEs [eqpoll_sym RS eqpoll_0_is_0 RS succ_neq_0]) 1); |
164 by (fast_tac (!claset addSEs [eqpoll_sym RS eqpoll_0_is_0 RS succ_neq_0]) 1); |
169 val eqpoll_succ_imp_not_empty = result(); |
165 val eqpoll_succ_imp_not_empty = result(); |
170 |
166 |