193 by (rtac (major RS trans_induct) 1); |
193 by (rtac (major RS trans_induct) 1); |
194 by (rtac (rank RS ssubst) 1); |
194 by (rtac (rank RS ssubst) 1); |
195 by (asm_simp_tac (ZF_ss addsimps [Ord_equality]) 1); |
195 by (asm_simp_tac (ZF_ss addsimps [Ord_equality]) 1); |
196 val rank_of_Ord = result(); |
196 val rank_of_Ord = result(); |
197 |
197 |
198 val [prem] = goal Epsilon.thy "a:b ==> rank(a) : rank(b)"; |
198 goal Epsilon.thy "!!a b. a:b ==> rank(a) < rank(b)"; |
199 by (res_inst_tac [("a1","b")] (rank RS ssubst) 1); |
199 by (res_inst_tac [("a1","b")] (rank RS ssubst) 1); |
200 by (rtac (prem RS UN_I) 1); |
200 be (UN_I RS ltI) 1; |
201 by (rtac succI1 1); |
201 by (rtac succI1 1); |
|
202 by (REPEAT (ares_tac [Ord_UN, Ord_succ, Ord_rank] 1)); |
202 val rank_lt = result(); |
203 val rank_lt = result(); |
203 |
204 |
204 val [major] = goal Epsilon.thy "a: eclose(b) ==> rank(a) : rank(b)"; |
205 val [major] = goal Epsilon.thy "a: eclose(b) ==> rank(a) < rank(b)"; |
205 by (rtac (major RS eclose_induct_down) 1); |
206 by (rtac (major RS eclose_induct_down) 1); |
206 by (etac rank_lt 1); |
207 by (etac rank_lt 1); |
207 by (etac (rank_lt RS Ord_trans) 1); |
208 by (etac (rank_lt RS lt_trans) 1); |
208 by (assume_tac 1); |
209 by (assume_tac 1); |
209 by (rtac Ord_rank 1); |
|
210 val eclose_rank_lt = result(); |
210 val eclose_rank_lt = result(); |
211 |
211 |
212 goal Epsilon.thy "!!a b. a<=b ==> rank(a) <= rank(b)"; |
212 goal Epsilon.thy "!!a b. a<=b ==> rank(a) le rank(b)"; |
|
213 by (rtac subset_imp_le 1); |
213 by (rtac (rank RS ssubst) 1); |
214 by (rtac (rank RS ssubst) 1); |
214 by (rtac (rank RS ssubst) 1); |
215 by (rtac (rank RS ssubst) 1); |
215 by (etac UN_mono 1); |
216 by (etac UN_mono 1); |
216 by (rtac subset_refl 1); |
217 by (REPEAT (resolve_tac [subset_refl, Ord_rank] 1)); |
217 val rank_mono = result(); |
218 val rank_mono = result(); |
218 |
219 |
219 goal Epsilon.thy "rank(Pow(a)) = succ(rank(a))"; |
220 goal Epsilon.thy "rank(Pow(a)) = succ(rank(a))"; |
220 by (rtac (rank RS trans) 1); |
221 by (rtac (rank RS trans) 1); |
221 by (rtac equalityI 1); |
222 by (rtac le_asym 1); |
222 by (fast_tac ZF_cs 2); |
223 by (DO_GOAL [rtac (Ord_rank RS Ord_succ RS UN_least_le), |
223 by (rtac UN_least 1); |
224 etac (PowD RS rank_mono RS succ_leI)] 1); |
224 by (etac (PowD RS rank_mono RS Ord_succ_mono) 1); |
225 by (DO_GOAL [rtac ([Pow_top, le_refl] MRS UN_upper_le), |
225 by (rtac Ord_rank 1); |
226 REPEAT o rtac (Ord_rank RS Ord_succ)] 1); |
226 by (rtac Ord_rank 1); |
|
227 val rank_Pow = result(); |
227 val rank_Pow = result(); |
228 |
228 |
229 goal Epsilon.thy "rank(0) = 0"; |
229 goal Epsilon.thy "rank(0) = 0"; |
230 by (rtac (rank RS trans) 1); |
230 by (rtac (rank RS trans) 1); |
231 by (fast_tac (ZF_cs addSIs [equalityI]) 1); |
231 by (fast_tac (ZF_cs addSIs [equalityI]) 1); |
234 goal Epsilon.thy "rank(succ(x)) = succ(rank(x))"; |
234 goal Epsilon.thy "rank(succ(x)) = succ(rank(x))"; |
235 by (rtac (rank RS trans) 1); |
235 by (rtac (rank RS trans) 1); |
236 by (rtac ([UN_least, succI1 RS UN_upper] MRS equalityI) 1); |
236 by (rtac ([UN_least, succI1 RS UN_upper] MRS equalityI) 1); |
237 by (etac succE 1); |
237 by (etac succE 1); |
238 by (fast_tac ZF_cs 1); |
238 by (fast_tac ZF_cs 1); |
239 by (REPEAT (ares_tac [Ord_succ_mono,Ord_rank,OrdmemD,rank_lt] 1)); |
239 be (rank_lt RS leI RS succ_leI RS le_imp_subset) 1; |
240 val rank_succ = result(); |
240 val rank_succ = result(); |
241 |
241 |
242 goal Epsilon.thy "rank(Union(A)) = (UN x:A. rank(x))"; |
242 goal Epsilon.thy "rank(Union(A)) = (UN x:A. rank(x))"; |
243 by (rtac equalityI 1); |
243 by (rtac equalityI 1); |
244 by (rtac (rank_mono RS UN_least) 2); |
244 by (rtac (rank_mono RS le_imp_subset RS UN_least) 2); |
245 by (etac Union_upper 2); |
245 by (etac Union_upper 2); |
246 by (rtac (rank RS ssubst) 1); |
246 by (rtac (rank RS ssubst) 1); |
247 by (rtac UN_least 1); |
247 by (rtac UN_least 1); |
248 by (etac UnionE 1); |
248 by (etac UnionE 1); |
249 by (rtac subset_trans 1); |
249 by (rtac subset_trans 1); |
250 by (etac (RepFunI RS Union_upper) 2); |
250 by (etac (RepFunI RS Union_upper) 2); |
251 by (etac (rank_lt RS Ord_succ_subsetI) 1); |
251 by (etac (rank_lt RS succ_leI RS le_imp_subset) 1); |
252 by (rtac Ord_rank 1); |
|
253 val rank_Union = result(); |
252 val rank_Union = result(); |
254 |
253 |
255 goal Epsilon.thy "rank(eclose(a)) = rank(a)"; |
254 goal Epsilon.thy "rank(eclose(a)) = rank(a)"; |
256 by (rtac equalityI 1); |
255 by (rtac le_asym 1); |
257 by (rtac (arg_subset_eclose RS rank_mono) 2); |
256 by (rtac (arg_subset_eclose RS rank_mono) 2); |
258 by (res_inst_tac [("a1","eclose(a)")] (rank RS ssubst) 1); |
257 by (res_inst_tac [("a1","eclose(a)")] (rank RS ssubst) 1); |
259 by (rtac UN_least 1); |
258 by (rtac (Ord_rank RS UN_least_le) 1); |
260 by (etac ([eclose_rank_lt, Ord_rank] MRS Ord_succ_subsetI) 1); |
259 by (etac (eclose_rank_lt RS succ_leI) 1); |
261 val rank_eclose = result(); |
260 val rank_eclose = result(); |
262 |
261 |
263 (* [| i: j; j: rank(a) |] ==> i: rank(a) *) |
262 goalw Epsilon.thy [Pair_def] "rank(a) < rank(<a,b>)"; |
264 val rank_trans = Ord_rank RSN (3, Ord_trans); |
263 by (rtac (consI1 RS rank_lt RS lt_trans) 1); |
265 |
|
266 goalw Epsilon.thy [Pair_def] "rank(a) : rank(<a,b>)"; |
|
267 by (rtac (consI1 RS rank_lt RS Ord_trans) 1); |
|
268 by (rtac (consI1 RS consI2 RS rank_lt) 1); |
264 by (rtac (consI1 RS consI2 RS rank_lt) 1); |
269 by (rtac Ord_rank 1); |
|
270 val rank_pair1 = result(); |
265 val rank_pair1 = result(); |
271 |
266 |
272 goalw Epsilon.thy [Pair_def] "rank(b) : rank(<a,b>)"; |
267 goalw Epsilon.thy [Pair_def] "rank(b) < rank(<a,b>)"; |
273 by (rtac (consI1 RS consI2 RS rank_lt RS Ord_trans) 1); |
268 by (rtac (consI1 RS consI2 RS rank_lt RS lt_trans) 1); |
274 by (rtac (consI1 RS consI2 RS rank_lt) 1); |
269 by (rtac (consI1 RS consI2 RS rank_lt) 1); |
275 by (rtac Ord_rank 1); |
|
276 val rank_pair2 = result(); |
270 val rank_pair2 = result(); |
277 |
271 |
278 goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inl_def] "rank(a) : rank(Inl(a))"; |
272 goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inl_def] "rank(a) < rank(Inl(a))"; |
279 by (rtac rank_pair2 1); |
273 by (rtac rank_pair2 1); |
280 val rank_Inl = result(); |
274 val rank_Inl = result(); |
281 |
275 |
282 goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inr_def] "rank(a) : rank(Inr(a))"; |
276 goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inr_def] "rank(a) < rank(Inr(a))"; |
283 by (rtac rank_pair2 1); |
277 by (rtac rank_pair2 1); |
284 val rank_Inr = result(); |
278 val rank_Inr = result(); |
285 |
|
286 val [major] = goal Epsilon.thy "i: rank(a) ==> (EX x:a. i<=rank(x))"; |
|
287 by (resolve_tac ([major] RL [rank RS subst] RL [UN_E]) 1); |
|
288 by (rtac bexI 1); |
|
289 by (etac member_succD 1); |
|
290 by (rtac Ord_rank 1); |
|
291 by (assume_tac 1); |
|
292 val rank_implies_mem = result(); |
|
293 |
|
294 |
279 |
295 (*** Corollaries of leastness ***) |
280 (*** Corollaries of leastness ***) |
296 |
281 |
297 goal Epsilon.thy "!!A B. A:B ==> eclose(A)<=eclose(B)"; |
282 goal Epsilon.thy "!!A B. A:B ==> eclose(A)<=eclose(B)"; |
298 by (rtac (Transset_eclose RS eclose_least) 1); |
283 by (rtac (Transset_eclose RS eclose_least) 1); |