67 |
67 |
68 (* used in : AC10-AC15.ML AC16WO4.ML WO6WO1.ML *) |
68 (* used in : AC10-AC15.ML AC16WO4.ML WO6WO1.ML *) |
69 (*I don't know where to put this one.*) |
69 (*I don't know where to put this one.*) |
70 goal Cardinal.thy |
70 goal Cardinal.thy |
71 "!!m A B. [| A lepoll succ(m); B<=A; B~=0 |] ==> A-B lepoll m"; |
71 "!!m A B. [| A lepoll succ(m); B<=A; B~=0 |] ==> A-B lepoll m"; |
72 by (resolve_tac [not_emptyE] 1 THEN (atac 1)); |
72 by (resolve_tac [not_emptyE] 1 THEN (assume_tac 1)); |
73 by (forward_tac [singleton_subsetI] 1); |
73 by (forward_tac [singleton_subsetI] 1); |
74 by (forward_tac [subsetD] 1 THEN (atac 1)); |
74 by (forward_tac [subsetD] 1 THEN (assume_tac 1)); |
75 by (res_inst_tac [("A2","A")] |
75 by (res_inst_tac [("A2","A")] |
76 (Diff_sing_lepoll RSN (2, subset_imp_lepoll RS lepoll_trans)) 1 |
76 (Diff_sing_lepoll RSN (2, subset_imp_lepoll RS lepoll_trans)) 1 |
77 THEN (REPEAT (atac 2))); |
77 THEN (REPEAT (assume_tac 2))); |
78 by (fast_tac ZF_cs 1); |
78 by (fast_tac ZF_cs 1); |
79 val Diff_lepoll = result(); |
79 val Diff_lepoll = result(); |
80 |
80 |
81 (* ********************************************************************** *) |
81 (* ********************************************************************** *) |
82 (* lemmas concerning lepoll and eqpoll relations *) |
82 (* lemmas concerning lepoll and eqpoll relations *) |
89 (* lemma for ordertype_Int *) |
89 (* lemma for ordertype_Int *) |
90 goalw Cardinal.thy [rvimage_def] "rvimage(A,id(A),r) = r Int A*A"; |
90 goalw Cardinal.thy [rvimage_def] "rvimage(A,id(A),r) = r Int A*A"; |
91 by (resolve_tac [equalityI] 1); |
91 by (resolve_tac [equalityI] 1); |
92 by (step_tac ZF_cs 1); |
92 by (step_tac ZF_cs 1); |
93 by (dres_inst_tac [("P","%a. <id(A)`xb,a>:r")] (id_conv RS subst) 1 |
93 by (dres_inst_tac [("P","%a. <id(A)`xb,a>:r")] (id_conv RS subst) 1 |
94 THEN (atac 1)); |
94 THEN (assume_tac 1)); |
95 by (dres_inst_tac [("P","%a. <a,ya>:r")] (id_conv RS subst) 1 |
95 by (dres_inst_tac [("P","%a. <a,ya>:r")] (id_conv RS subst) 1 |
96 THEN (REPEAT (atac 1))); |
96 THEN (REPEAT (assume_tac 1))); |
97 by (fast_tac (ZF_cs addIs [id_conv RS ssubst]) 1); |
97 by (fast_tac (ZF_cs addIs [id_conv RS ssubst]) 1); |
98 val rvimage_id = result(); |
98 val rvimage_id = result(); |
99 |
99 |
100 (* used only in Hartog.ML *) |
100 (* used only in Hartog.ML *) |
101 goal Cardinal.thy |
101 goal Cardinal.thy |
136 |
136 |
137 goal thy "A*B=0 <-> A=0 | B=0"; |
137 goal thy "A*B=0 <-> A=0 | B=0"; |
138 by (fast_tac (ZF_cs addSIs [equals0I] addEs [equals0D]) 1); |
138 by (fast_tac (ZF_cs addSIs [equals0I] addEs [equals0D]) 1); |
139 val Sigma_empty_iff = result(); |
139 val Sigma_empty_iff = result(); |
140 |
140 |
|
141 goalw thy [Finite_def] "!!n. n:nat ==> Finite(n)"; |
|
142 by (fast_tac (AC_cs addSIs [eqpoll_refl]) 1); |
|
143 val nat_into_Finite = result(); |
|
144 |
|
145 goalw thy [Finite_def] "~Finite(nat)"; |
|
146 by (fast_tac (AC_cs addSDs [eqpoll_imp_lepoll] |
|
147 addIs [Ord_nat RSN (2, ltI) RS lt_not_lepoll RS notE]) 1); |
|
148 val nat_not_Finite = result(); |
|
149 |
|
150 val le_imp_lepoll = le_imp_subset RS subset_imp_lepoll; |
|
151 |
|
152 (* ********************************************************************** *) |
|
153 (* Another elimination rule for EX! *) |
|
154 (* ********************************************************************** *) |
|
155 |
|
156 goal thy "!!x. [| EX! x. P(x); P(x); P(y) |] ==> x=y"; |
|
157 by (eresolve_tac [ex1E] 1); |
|
158 by (res_inst_tac [("b","xa")] (sym RSN (2, trans)) 1); |
|
159 by (fast_tac AC_cs 1); |
|
160 by (fast_tac AC_cs 1); |
|
161 val ex1_two_eq = result(); |
|
162 |
|
163 (* ********************************************************************** *) |
|
164 (* image of a surjection *) |
|
165 (* ********************************************************************** *) |
|
166 |
|
167 goalw thy [surj_def] "!!f. f : surj(A, B) ==> f``A = B"; |
|
168 by (eresolve_tac [CollectE] 1); |
|
169 by (resolve_tac [subset_refl RSN (2, image_fun) RS ssubst] 1 THEN (assume_tac 1)); |
|
170 by (fast_tac (AC_cs addSEs [RepFunE, apply_type] |
|
171 addSIs [RepFunI] addIs [equalityI]) 1); |
|
172 val surj_image_eq = result(); |
|
173 |
|
174 |
|
175 goal thy "!!y. succ(x) lepoll y ==> y ~= 0"; |
|
176 by (fast_tac (ZF_cs addSDs [lepoll_0_is_0]) 1); |
|
177 val succ_lepoll_imp_not_empty = result(); |
|
178 |
|
179 goal thy "!!x. x eqpoll succ(n) ==> x ~= 0"; |
|
180 by (fast_tac (AC_cs addSEs [eqpoll_sym RS eqpoll_0_is_0 RS succ_neq_0]) 1); |
|
181 val eqpoll_succ_imp_not_empty = result(); |
|
182 |