1 (* Title: ZF/Ordinal.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 Ordinals in Zermelo-Fraenkel Set Theory |
|
7 *) |
|
8 |
|
9 (*** Rules for Transset ***) |
|
10 |
|
11 (** Three neat characterisations of Transset **) |
|
12 |
|
13 Goalw [Transset_def] "Transset(A) <-> A<=Pow(A)"; |
|
14 by (Blast_tac 1); |
|
15 qed "Transset_iff_Pow"; |
|
16 |
|
17 Goalw [Transset_def] "Transset(A) <-> Union(succ(A)) = A"; |
|
18 by (blast_tac (claset() addSEs [equalityE]) 1); |
|
19 qed "Transset_iff_Union_succ"; |
|
20 |
|
21 Goalw [Transset_def] "Transset(A) <-> Union(A) <= A"; |
|
22 by (Blast_tac 1); |
|
23 qed "Transset_iff_Union_subset"; |
|
24 |
|
25 (** Consequences of downwards closure **) |
|
26 |
|
27 Goalw [Transset_def] |
|
28 "[| Transset(C); {a,b}: C |] ==> a:C & b: C"; |
|
29 by (Blast_tac 1); |
|
30 qed "Transset_doubleton_D"; |
|
31 |
|
32 val [prem1,prem2] = goalw (the_context ()) [Pair_def] |
|
33 "[| Transset(C); <a,b>: C |] ==> a:C & b: C"; |
|
34 by (cut_facts_tac [prem2] 1); |
|
35 by (blast_tac (claset() addSDs [prem1 RS Transset_doubleton_D]) 1); |
|
36 qed "Transset_Pair_D"; |
|
37 |
|
38 val prem1::prems = goal (the_context ()) |
|
39 "[| Transset(C); A*B <= C; b: B |] ==> A <= C"; |
|
40 by (cut_facts_tac prems 1); |
|
41 by (blast_tac (claset() addSDs [prem1 RS Transset_Pair_D]) 1); |
|
42 qed "Transset_includes_domain"; |
|
43 |
|
44 val prem1::prems = goal (the_context ()) |
|
45 "[| Transset(C); A*B <= C; a: A |] ==> B <= C"; |
|
46 by (cut_facts_tac prems 1); |
|
47 by (blast_tac (claset() addSDs [prem1 RS Transset_Pair_D]) 1); |
|
48 qed "Transset_includes_range"; |
|
49 |
|
50 (** Closure properties **) |
|
51 |
|
52 Goalw [Transset_def] "Transset(0)"; |
|
53 by (Blast_tac 1); |
|
54 qed "Transset_0"; |
|
55 |
|
56 Goalw [Transset_def] |
|
57 "[| Transset(i); Transset(j) |] ==> Transset(i Un j)"; |
|
58 by (Blast_tac 1); |
|
59 qed "Transset_Un"; |
|
60 |
|
61 Goalw [Transset_def] |
|
62 "[| Transset(i); Transset(j) |] ==> Transset(i Int j)"; |
|
63 by (Blast_tac 1); |
|
64 qed "Transset_Int"; |
|
65 |
|
66 Goalw [Transset_def] "Transset(i) ==> Transset(succ(i))"; |
|
67 by (Blast_tac 1); |
|
68 qed "Transset_succ"; |
|
69 |
|
70 Goalw [Transset_def] "Transset(i) ==> Transset(Pow(i))"; |
|
71 by (Blast_tac 1); |
|
72 qed "Transset_Pow"; |
|
73 |
|
74 Goalw [Transset_def] "Transset(A) ==> Transset(Union(A))"; |
|
75 by (Blast_tac 1); |
|
76 qed "Transset_Union"; |
|
77 |
|
78 val [Transprem] = Goalw [Transset_def] |
|
79 "[| !!i. i:A ==> Transset(i) |] ==> Transset(Union(A))"; |
|
80 by (blast_tac (claset() addDs [Transprem RS bspec RS subsetD]) 1); |
|
81 qed "Transset_Union_family"; |
|
82 |
|
83 val [prem,Transprem] = Goalw [Transset_def] |
|
84 "[| j:A; !!i. i:A ==> Transset(i) |] ==> Transset(Inter(A))"; |
|
85 by (cut_facts_tac [prem] 1); |
|
86 by (blast_tac (claset() addDs [Transprem RS bspec RS subsetD]) 1); |
|
87 qed "Transset_Inter_family"; |
|
88 |
|
89 (*** Natural Deduction rules for Ord ***) |
|
90 |
|
91 val prems = Goalw [Ord_def] |
|
92 "[| Transset(i); !!x. x:i ==> Transset(x) |] ==> Ord(i)"; |
|
93 by (REPEAT (ares_tac (prems@[ballI,conjI]) 1)); |
|
94 qed "OrdI"; |
|
95 |
|
96 Goalw [Ord_def] "Ord(i) ==> Transset(i)"; |
|
97 by (Blast_tac 1); |
|
98 qed "Ord_is_Transset"; |
|
99 |
|
100 Goalw [Ord_def] |
|
101 "[| Ord(i); j:i |] ==> Transset(j) "; |
|
102 by (Blast_tac 1); |
|
103 qed "Ord_contains_Transset"; |
|
104 |
|
105 (*** Lemmas for ordinals ***) |
|
106 |
|
107 Goalw [Ord_def,Transset_def] "[| Ord(i); j:i |] ==> Ord(j)"; |
|
108 by (Blast_tac 1); |
|
109 qed "Ord_in_Ord"; |
|
110 |
|
111 (* Ord(succ(j)) ==> Ord(j) *) |
|
112 bind_thm ("Ord_succD", succI1 RSN (2, Ord_in_Ord)); |
|
113 |
|
114 AddSDs [Ord_succD]; |
|
115 |
|
116 Goal "[| Ord(i); Transset(j); j<=i |] ==> Ord(j)"; |
|
117 by (REPEAT (ares_tac [OrdI] 1 |
|
118 ORELSE eresolve_tac [Ord_contains_Transset, subsetD] 1)); |
|
119 qed "Ord_subset_Ord"; |
|
120 |
|
121 Goalw [Ord_def,Transset_def] "[| j:i; Ord(i) |] ==> j<=i"; |
|
122 by (Blast_tac 1); |
|
123 qed "OrdmemD"; |
|
124 |
|
125 Goal "[| i:j; j:k; Ord(k) |] ==> i:k"; |
|
126 by (REPEAT (ares_tac [OrdmemD RS subsetD] 1)); |
|
127 qed "Ord_trans"; |
|
128 |
|
129 Goal "[| i:j; Ord(j) |] ==> succ(i) <= j"; |
|
130 by (REPEAT (ares_tac [OrdmemD RSN (2,succ_subsetI)] 1)); |
|
131 qed "Ord_succ_subsetI"; |
|
132 |
|
133 |
|
134 (*** The construction of ordinals: 0, succ, Union ***) |
|
135 |
|
136 Goal "Ord(0)"; |
|
137 by (REPEAT (ares_tac [OrdI,Transset_0] 1 ORELSE etac emptyE 1)); |
|
138 qed "Ord_0"; |
|
139 |
|
140 Goal "Ord(i) ==> Ord(succ(i))"; |
|
141 by (REPEAT (ares_tac [OrdI,Transset_succ] 1 |
|
142 ORELSE eresolve_tac [succE,ssubst,Ord_is_Transset, |
|
143 Ord_contains_Transset] 1)); |
|
144 qed "Ord_succ"; |
|
145 |
|
146 bind_thm ("Ord_1", Ord_0 RS Ord_succ); |
|
147 |
|
148 Goal "Ord(succ(i)) <-> Ord(i)"; |
|
149 by (blast_tac (claset() addIs [Ord_succ]) 1); |
|
150 qed "Ord_succ_iff"; |
|
151 |
|
152 Addsimps [Ord_0, Ord_succ_iff]; |
|
153 AddSIs [Ord_0, Ord_succ]; |
|
154 AddTCs [Ord_0, Ord_succ]; |
|
155 |
|
156 Goalw [Ord_def] "[| Ord(i); Ord(j) |] ==> Ord(i Un j)"; |
|
157 by (blast_tac (claset() addSIs [Transset_Un]) 1); |
|
158 qed "Ord_Un"; |
|
159 |
|
160 Goalw [Ord_def] "[| Ord(i); Ord(j) |] ==> Ord(i Int j)"; |
|
161 by (blast_tac (claset() addSIs [Transset_Int]) 1); |
|
162 qed "Ord_Int"; |
|
163 AddTCs [Ord_Un, Ord_Int]; |
|
164 |
|
165 val nonempty::prems = Goal |
|
166 "[| j:A; !!i. i:A ==> Ord(i) |] ==> Ord(Inter(A))"; |
|
167 by (rtac (nonempty RS Transset_Inter_family RS OrdI) 1); |
|
168 by (rtac Ord_is_Transset 1); |
|
169 by (REPEAT (ares_tac ([Ord_contains_Transset,nonempty]@prems) 1 |
|
170 ORELSE etac InterD 1)); |
|
171 qed "Ord_Inter"; |
|
172 |
|
173 val jmemA::prems = Goal |
|
174 "[| j:A; !!x. x:A ==> Ord(B(x)) |] ==> Ord(INT x:A. B(x))"; |
|
175 by (rtac (jmemA RS RepFunI RS Ord_Inter) 1); |
|
176 by (etac RepFunE 1); |
|
177 by (etac ssubst 1); |
|
178 by (eresolve_tac prems 1); |
|
179 qed "Ord_INT"; |
|
180 |
|
181 (*There is no set of all ordinals, for then it would contain itself*) |
|
182 Goal "~ (ALL i. i:X <-> Ord(i))"; |
|
183 by (rtac notI 1); |
|
184 by (forw_inst_tac [("x", "X")] spec 1); |
|
185 by (safe_tac (claset() addSEs [mem_irrefl])); |
|
186 by (swap_res_tac [Ord_is_Transset RSN (2,OrdI)] 1); |
|
187 by (Blast_tac 2); |
|
188 by (rewtac Transset_def); |
|
189 by Safe_tac; |
|
190 by (Asm_full_simp_tac 1); |
|
191 by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1)); |
|
192 qed "ON_class"; |
|
193 |
|
194 (*** < is 'less than' for ordinals ***) |
|
195 |
|
196 Goalw [lt_def] "[| i:j; Ord(j) |] ==> i<j"; |
|
197 by (REPEAT (ares_tac [conjI] 1)); |
|
198 qed "ltI"; |
|
199 |
|
200 val major::prems = Goalw [lt_def] |
|
201 "[| i<j; [| i:j; Ord(i); Ord(j) |] ==> P |] ==> P"; |
|
202 by (rtac (major RS conjE) 1); |
|
203 by (REPEAT (ares_tac (prems@[Ord_in_Ord]) 1)); |
|
204 qed "ltE"; |
|
205 |
|
206 Goal "i<j ==> i:j"; |
|
207 by (etac ltE 1); |
|
208 by (assume_tac 1); |
|
209 qed "ltD"; |
|
210 |
|
211 Goalw [lt_def] "~ i<0"; |
|
212 by (Blast_tac 1); |
|
213 qed "not_lt0"; |
|
214 |
|
215 Addsimps [not_lt0]; |
|
216 |
|
217 Goal "j<i ==> Ord(j)"; |
|
218 by (etac ltE 1 THEN assume_tac 1); |
|
219 qed "lt_Ord"; |
|
220 |
|
221 Goal "j<i ==> Ord(i)"; |
|
222 by (etac ltE 1 THEN assume_tac 1); |
|
223 qed "lt_Ord2"; |
|
224 |
|
225 (* "ja le j ==> Ord(j)" *) |
|
226 bind_thm ("le_Ord2", lt_Ord2 RS Ord_succD); |
|
227 |
|
228 (* i<0 ==> R *) |
|
229 bind_thm ("lt0E", not_lt0 RS notE); |
|
230 |
|
231 Goal "[| i<j; j<k |] ==> i<k"; |
|
232 by (blast_tac (claset() addSIs [ltI] addSEs [ltE] addIs [Ord_trans]) 1); |
|
233 qed "lt_trans"; |
|
234 |
|
235 Goalw [lt_def] "i<j ==> ~ (j<i)"; |
|
236 by (blast_tac (claset() addEs [mem_asym]) 1); |
|
237 qed "lt_not_sym"; |
|
238 |
|
239 (* [| i<j; ~P ==> j<i |] ==> P *) |
|
240 bind_thm ("lt_asym", lt_not_sym RS swap); |
|
241 |
|
242 val [major]= goal (the_context ()) "i<i ==> P"; |
|
243 by (rtac (major RS (major RS lt_asym)) 1) ; |
|
244 qed "lt_irrefl"; |
|
245 |
|
246 Goal "~ i<i"; |
|
247 by (rtac notI 1); |
|
248 by (etac lt_irrefl 1) ; |
|
249 qed "lt_not_refl"; |
|
250 |
|
251 AddSEs [lt_irrefl, lt0E]; |
|
252 |
|
253 (** le is less than or equals; recall i le j abbrevs i<succ(j) !! **) |
|
254 |
|
255 Goalw [lt_def] "i le j <-> i<j | (i=j & Ord(j))"; |
|
256 by (Blast_tac 1); |
|
257 qed "le_iff"; |
|
258 |
|
259 (*Equivalently, i<j ==> i < succ(j)*) |
|
260 Goal "i<j ==> i le j"; |
|
261 by (asm_simp_tac (simpset() addsimps [le_iff]) 1); |
|
262 qed "leI"; |
|
263 |
|
264 Goal "[| i=j; Ord(j) |] ==> i le j"; |
|
265 by (asm_simp_tac (simpset() addsimps [le_iff]) 1); |
|
266 qed "le_eqI"; |
|
267 |
|
268 bind_thm ("le_refl", refl RS le_eqI); |
|
269 |
|
270 Goal "i le i <-> Ord(i)"; |
|
271 by (asm_simp_tac (simpset() addsimps [lt_not_refl, le_iff]) 1); |
|
272 qed "le_refl_iff"; |
|
273 |
|
274 AddIffs [le_refl_iff]; |
|
275 |
|
276 val [prem] = Goal "(~ (i=j & Ord(j)) ==> i<j) ==> i le j"; |
|
277 by (rtac (disjCI RS (le_iff RS iffD2)) 1); |
|
278 by (etac prem 1); |
|
279 qed "leCI"; |
|
280 |
|
281 val major::prems = Goal |
|
282 "[| i le j; i<j ==> P; [| i=j; Ord(j) |] ==> P |] ==> P"; |
|
283 by (rtac (major RS (le_iff RS iffD1 RS disjE)) 1); |
|
284 by (DEPTH_SOLVE (ares_tac prems 1 ORELSE etac conjE 1)); |
|
285 qed "leE"; |
|
286 |
|
287 Goal "[| i le j; j le i |] ==> i=j"; |
|
288 by (asm_full_simp_tac (simpset() addsimps [le_iff]) 1); |
|
289 by (blast_tac (claset() addEs [lt_asym]) 1); |
|
290 qed "le_anti_sym"; |
|
291 |
|
292 Goal "i le 0 <-> i=0"; |
|
293 by (blast_tac (claset() addSEs [leE]) 1); |
|
294 qed "le0_iff"; |
|
295 |
|
296 bind_thm ("le0D", le0_iff RS iffD1); |
|
297 |
|
298 AddSDs [le0D]; |
|
299 Addsimps [le0_iff]; |
|
300 |
|
301 val le_cs = claset() addSIs [leCI] addSEs [leE] addEs [lt_asym]; |
|
302 |
|
303 |
|
304 (*** Natural Deduction rules for Memrel ***) |
|
305 |
|
306 Goalw [Memrel_def] "<a,b> : Memrel(A) <-> a:b & a:A & b:A"; |
|
307 by (Blast_tac 1); |
|
308 qed "Memrel_iff"; |
|
309 Addsimps [Memrel_iff]; |
|
310 (*MemrelI/E give better speed than AddIffs here*) |
|
311 |
|
312 Goal "[| a: b; a: A; b: A |] ==> <a,b> : Memrel(A)"; |
|
313 by Auto_tac; |
|
314 qed "MemrelI"; |
|
315 |
|
316 val [major,minor] = Goal |
|
317 "[| <a,b> : Memrel(A); \ |
|
318 \ [| a: A; b: A; a:b |] ==> P \ |
|
319 \ |] ==> P"; |
|
320 by (rtac (major RS (Memrel_iff RS iffD1) RS conjE) 1); |
|
321 by (etac conjE 1); |
|
322 by (rtac minor 1); |
|
323 by (REPEAT (assume_tac 1)); |
|
324 qed "MemrelE"; |
|
325 |
|
326 AddSIs [MemrelI]; |
|
327 AddSEs [MemrelE]; |
|
328 |
|
329 Goalw [Memrel_def] "Memrel(A) <= A*A"; |
|
330 by (Blast_tac 1); |
|
331 qed "Memrel_type"; |
|
332 |
|
333 Goalw [Memrel_def] "A<=B ==> Memrel(A) <= Memrel(B)"; |
|
334 by (Blast_tac 1); |
|
335 qed "Memrel_mono"; |
|
336 |
|
337 Goalw [Memrel_def] "Memrel(0) = 0"; |
|
338 by (Blast_tac 1); |
|
339 qed "Memrel_0"; |
|
340 |
|
341 Goalw [Memrel_def] "Memrel(1) = 0"; |
|
342 by (Blast_tac 1); |
|
343 qed "Memrel_1"; |
|
344 |
|
345 Addsimps [Memrel_0, Memrel_1]; |
|
346 |
|
347 (*The membership relation (as a set) is well-founded. |
|
348 Proof idea: show A<=B by applying the foundation axiom to A-B *) |
|
349 Goalw [wf_def] "wf(Memrel(A))"; |
|
350 by (EVERY1 [rtac (foundation RS disjE RS allI), |
|
351 etac disjI1, |
|
352 etac bexE, |
|
353 rtac (impI RS allI RS bexI RS disjI2), |
|
354 etac MemrelE, |
|
355 etac bspec, |
|
356 REPEAT o assume_tac]); |
|
357 qed "wf_Memrel"; |
|
358 |
|
359 (*Transset(i) does not suffice, though ALL j:i.Transset(j) does*) |
|
360 Goalw [Ord_def, Transset_def, trans_def] |
|
361 "Ord(i) ==> trans(Memrel(i))"; |
|
362 by (Blast_tac 1); |
|
363 qed "trans_Memrel"; |
|
364 |
|
365 (*If Transset(A) then Memrel(A) internalizes the membership relation below A*) |
|
366 Goalw [Transset_def] |
|
367 "Transset(A) ==> <a,b> : Memrel(A) <-> a:b & b:A"; |
|
368 by (Blast_tac 1); |
|
369 qed "Transset_Memrel_iff"; |
|
370 |
|
371 |
|
372 (*** Transfinite induction ***) |
|
373 |
|
374 (*Epsilon induction over a transitive set*) |
|
375 val major::prems = Goalw [Transset_def] |
|
376 "[| i: k; Transset(k); \ |
|
377 \ !!x.[| x: k; ALL y:x. P(y) |] ==> P(x) \ |
|
378 \ |] ==> P(i)"; |
|
379 by (rtac (major RS (wf_Memrel RS wf_induct2)) 1); |
|
380 by (Blast_tac 1); |
|
381 by (resolve_tac prems 1); |
|
382 by (assume_tac 1); |
|
383 by (cut_facts_tac prems 1); |
|
384 by (Blast_tac 1); |
|
385 qed "Transset_induct"; |
|
386 |
|
387 (*Induction over an ordinal*) |
|
388 bind_thm ("Ord_induct", Ord_is_Transset RSN (2, Transset_induct)); |
|
389 |
|
390 (*Induction over the class of ordinals -- a useful corollary of Ord_induct*) |
|
391 val [major,indhyp] = Goal |
|
392 "[| Ord(i); \ |
|
393 \ !!x.[| Ord(x); ALL y:x. P(y) |] ==> P(x) \ |
|
394 \ |] ==> P(i)"; |
|
395 by (rtac (major RS Ord_succ RS (succI1 RS Ord_induct)) 1); |
|
396 by (rtac indhyp 1); |
|
397 by (rtac (major RS Ord_succ RS Ord_in_Ord) 1); |
|
398 by (REPEAT (assume_tac 1)); |
|
399 qed "trans_induct"; |
|
400 |
|
401 (*Perform induction on i, then prove the Ord(i) subgoal using prems. *) |
|
402 fun trans_ind_tac a prems i = |
|
403 EVERY [res_inst_tac [("i",a)] trans_induct i, |
|
404 rename_last_tac a ["1"] (i+1), |
|
405 ares_tac prems i]; |
|
406 |
|
407 |
|
408 (*** Fundamental properties of the epsilon ordering (< on ordinals) ***) |
|
409 |
|
410 (*Finds contradictions for the following proof*) |
|
411 val Ord_trans_tac = EVERY' [etac notE, etac Ord_trans, REPEAT o atac]; |
|
412 |
|
413 (** Proving that < is a linear ordering on the ordinals **) |
|
414 |
|
415 Goal "Ord(i) ==> (ALL j. Ord(j) --> i:j | i=j | j:i)"; |
|
416 by (etac trans_induct 1); |
|
417 by (rtac (impI RS allI) 1); |
|
418 by (trans_ind_tac "j" [] 1); |
|
419 by (DEPTH_SOLVE (Step_tac 1 ORELSE Ord_trans_tac 1)); |
|
420 qed_spec_mp "Ord_linear"; |
|
421 |
|
422 (*The trichotomy law for ordinals!*) |
|
423 val ordi::ordj::prems = Goalw [lt_def] |
|
424 "[| Ord(i); Ord(j); i<j ==> P; i=j ==> P; j<i ==> P |] ==> P"; |
|
425 by (rtac ([ordi,ordj] MRS Ord_linear RS disjE) 1); |
|
426 by (etac disjE 2); |
|
427 by (DEPTH_SOLVE (ares_tac ([ordi,ordj,conjI] @ prems) 1)); |
|
428 qed "Ord_linear_lt"; |
|
429 |
|
430 val prems = Goal |
|
431 "[| Ord(i); Ord(j); i<j ==> P; j le i ==> P |] ==> P"; |
|
432 by (res_inst_tac [("i","i"),("j","j")] Ord_linear_lt 1); |
|
433 by (DEPTH_SOLVE (ares_tac ([leI, sym RS le_eqI] @ prems) 1)); |
|
434 qed "Ord_linear2"; |
|
435 |
|
436 val prems = Goal |
|
437 "[| Ord(i); Ord(j); i le j ==> P; j le i ==> P |] ==> P"; |
|
438 by (res_inst_tac [("i","i"),("j","j")] Ord_linear_lt 1); |
|
439 by (DEPTH_SOLVE (ares_tac ([leI,le_eqI] @ prems) 1)); |
|
440 qed "Ord_linear_le"; |
|
441 |
|
442 Goal "j le i ==> ~ i<j"; |
|
443 by (blast_tac le_cs 1); |
|
444 qed "le_imp_not_lt"; |
|
445 |
|
446 Goal "[| ~ i<j; Ord(i); Ord(j) |] ==> j le i"; |
|
447 by (res_inst_tac [("i","i"),("j","j")] Ord_linear2 1); |
|
448 by (REPEAT (SOMEGOAL assume_tac)); |
|
449 by (blast_tac le_cs 1); |
|
450 qed "not_lt_imp_le"; |
|
451 |
|
452 (** Some rewrite rules for <, le **) |
|
453 |
|
454 Goalw [lt_def] "Ord(j) ==> i:j <-> i<j"; |
|
455 by (Blast_tac 1); |
|
456 qed "Ord_mem_iff_lt"; |
|
457 |
|
458 Goal "[| Ord(i); Ord(j) |] ==> ~ i<j <-> j le i"; |
|
459 by (REPEAT (ares_tac [iffI, le_imp_not_lt, not_lt_imp_le] 1)); |
|
460 qed "not_lt_iff_le"; |
|
461 |
|
462 Goal "[| Ord(i); Ord(j) |] ==> ~ i le j <-> j<i"; |
|
463 by (asm_simp_tac (simpset() addsimps [not_lt_iff_le RS iff_sym]) 1); |
|
464 qed "not_le_iff_lt"; |
|
465 |
|
466 (*This is identical to 0<succ(i) *) |
|
467 Goal "Ord(i) ==> 0 le i"; |
|
468 by (etac (not_lt_iff_le RS iffD1) 1); |
|
469 by (REPEAT (resolve_tac [Ord_0, not_lt0] 1)); |
|
470 qed "Ord_0_le"; |
|
471 |
|
472 Goal "[| Ord(i); i~=0 |] ==> 0<i"; |
|
473 by (etac (not_le_iff_lt RS iffD1) 1); |
|
474 by (rtac Ord_0 1); |
|
475 by (Blast_tac 1); |
|
476 qed "Ord_0_lt"; |
|
477 |
|
478 Goal "Ord(i) ==> i~=0 <-> 0<i"; |
|
479 by (blast_tac (claset() addIs [Ord_0_lt]) 1); |
|
480 qed "Ord_0_lt_iff"; |
|
481 |
|
482 |
|
483 (*** Results about less-than or equals ***) |
|
484 |
|
485 (** For ordinals, j<=i (subset) implies j le i (less-than or equals) **) |
|
486 |
|
487 Goal "0 le succ(x) <-> Ord(x)"; |
|
488 by (blast_tac (claset() addIs [Ord_0_le] addEs [ltE]) 1); |
|
489 qed "zero_le_succ_iff"; |
|
490 AddIffs [zero_le_succ_iff]; |
|
491 |
|
492 Goal "[| j<=i; Ord(i); Ord(j) |] ==> j le i"; |
|
493 by (rtac (not_lt_iff_le RS iffD1) 1); |
|
494 by (assume_tac 1); |
|
495 by (assume_tac 1); |
|
496 by (blast_tac (claset() addEs [ltE, mem_irrefl]) 1); |
|
497 qed "subset_imp_le"; |
|
498 |
|
499 Goal "i le j ==> i<=j"; |
|
500 by (etac leE 1); |
|
501 by (Blast_tac 2); |
|
502 by (blast_tac (subset_cs addIs [OrdmemD] addEs [ltE]) 1); |
|
503 qed "le_imp_subset"; |
|
504 |
|
505 Goal "j le i <-> j<=i & Ord(i) & Ord(j)"; |
|
506 by (blast_tac (claset() addDs [subset_imp_le, le_imp_subset] addEs [ltE]) 1); |
|
507 qed "le_subset_iff"; |
|
508 |
|
509 Goal "i le succ(j) <-> i le j | i=succ(j) & Ord(i)"; |
|
510 by (simp_tac (simpset() addsimps [le_iff]) 1); |
|
511 by (Blast_tac 1); |
|
512 qed "le_succ_iff"; |
|
513 |
|
514 (*Just a variant of subset_imp_le*) |
|
515 val [ordi,ordj,minor] = Goal |
|
516 "[| Ord(i); Ord(j); !!x. x<j ==> x<i |] ==> j le i"; |
|
517 by (REPEAT_FIRST (ares_tac [notI RS not_lt_imp_le, ordi, ordj])); |
|
518 by (etac (minor RS lt_irrefl) 1); |
|
519 qed "all_lt_imp_le"; |
|
520 |
|
521 (** Transitive laws **) |
|
522 |
|
523 Goal "[| i le j; j<k |] ==> i<k"; |
|
524 by (blast_tac (claset() addSEs [leE] addIs [lt_trans]) 1); |
|
525 qed "lt_trans1"; |
|
526 |
|
527 Goal "[| i<j; j le k |] ==> i<k"; |
|
528 by (blast_tac (claset() addSEs [leE] addIs [lt_trans]) 1); |
|
529 qed "lt_trans2"; |
|
530 |
|
531 Goal "[| i le j; j le k |] ==> i le k"; |
|
532 by (REPEAT (ares_tac [lt_trans1] 1)); |
|
533 qed "le_trans"; |
|
534 |
|
535 Goal "i<j ==> succ(i) le j"; |
|
536 by (rtac (not_lt_iff_le RS iffD1) 1); |
|
537 by (blast_tac le_cs 3); |
|
538 by (ALLGOALS (blast_tac (claset() addEs [ltE]))); |
|
539 qed "succ_leI"; |
|
540 |
|
541 (*Identical to succ(i) < succ(j) ==> i<j *) |
|
542 Goal "succ(i) le j ==> i<j"; |
|
543 by (rtac (not_le_iff_lt RS iffD1) 1); |
|
544 by (blast_tac le_cs 3); |
|
545 by (ALLGOALS (blast_tac (claset() addEs [ltE]))); |
|
546 qed "succ_leE"; |
|
547 |
|
548 Goal "succ(i) le j <-> i<j"; |
|
549 by (REPEAT (ares_tac [iffI,succ_leI,succ_leE] 1)); |
|
550 qed "succ_le_iff"; |
|
551 AddIffs [succ_le_iff]; |
|
552 |
|
553 Goal "succ(i) le succ(j) ==> i le j"; |
|
554 by (blast_tac (claset() addSDs [succ_leE]) 1); |
|
555 qed "succ_le_imp_le"; |
|
556 |
|
557 Goal "[| i <= j; j<k; Ord(i) |] ==> i<k"; |
|
558 by (resolve_tac [subset_imp_le RS lt_trans1] 1); |
|
559 by (REPEAT (eresolve_tac [asm_rl, ltE] 1)); |
|
560 qed "lt_subset_trans"; |
|
561 |
|
562 (** Union and Intersection **) |
|
563 |
|
564 Goal "[| Ord(i); Ord(j) |] ==> i le i Un j"; |
|
565 by (rtac (Un_upper1 RS subset_imp_le) 1); |
|
566 by (REPEAT (ares_tac [Ord_Un] 1)); |
|
567 qed "Un_upper1_le"; |
|
568 |
|
569 Goal "[| Ord(i); Ord(j) |] ==> j le i Un j"; |
|
570 by (rtac (Un_upper2 RS subset_imp_le) 1); |
|
571 by (REPEAT (ares_tac [Ord_Un] 1)); |
|
572 qed "Un_upper2_le"; |
|
573 |
|
574 (*Replacing k by succ(k') yields the similar rule for le!*) |
|
575 Goal "[| i<k; j<k |] ==> i Un j < k"; |
|
576 by (res_inst_tac [("i","i"),("j","j")] Ord_linear_le 1); |
|
577 by (stac Un_commute 4); |
|
578 by (asm_full_simp_tac (simpset() addsimps [le_subset_iff, subset_Un_iff]) 4); |
|
579 by (asm_full_simp_tac (simpset() addsimps [le_subset_iff, subset_Un_iff]) 3); |
|
580 by (REPEAT (eresolve_tac [asm_rl, ltE] 1)); |
|
581 qed "Un_least_lt"; |
|
582 |
|
583 Goal "[| Ord(i); Ord(j) |] ==> i Un j < k <-> i<k & j<k"; |
|
584 by (safe_tac (claset() addSIs [Un_least_lt])); |
|
585 by (rtac (Un_upper2_le RS lt_trans1) 2); |
|
586 by (rtac (Un_upper1_le RS lt_trans1) 1); |
|
587 by (REPEAT_SOME assume_tac); |
|
588 qed "Un_least_lt_iff"; |
|
589 |
|
590 val [ordi,ordj,ordk] = goal (the_context ()) |
|
591 "[| Ord(i); Ord(j); Ord(k) |] ==> i Un j : k <-> i:k & j:k"; |
|
592 by (cut_inst_tac [("k","k")] ([ordi,ordj] MRS Un_least_lt_iff) 1); |
|
593 by (asm_full_simp_tac (simpset() addsimps [lt_def,ordi,ordj,ordk]) 1); |
|
594 qed "Un_least_mem_iff"; |
|
595 |
|
596 (*Replacing k by succ(k') yields the similar rule for le!*) |
|
597 Goal "[| i<k; j<k |] ==> i Int j < k"; |
|
598 by (res_inst_tac [("i","i"),("j","j")] Ord_linear_le 1); |
|
599 by (stac Int_commute 4); |
|
600 by (asm_full_simp_tac (simpset() addsimps [le_subset_iff, subset_Int_iff]) 4); |
|
601 by (asm_full_simp_tac (simpset() addsimps [le_subset_iff, subset_Int_iff]) 3); |
|
602 by (REPEAT (eresolve_tac [asm_rl, ltE] 1)); |
|
603 qed "Int_greatest_lt"; |
|
604 |
|
605 (*FIXME: the Intersection duals are missing!*) |
|
606 |
|
607 |
|
608 (*** Results about limits ***) |
|
609 |
|
610 val prems = Goal "[| !!i. i:A ==> Ord(i) |] ==> Ord(Union(A))"; |
|
611 by (rtac (Ord_is_Transset RS Transset_Union_family RS OrdI) 1); |
|
612 by (REPEAT (etac UnionE 1 ORELSE ares_tac ([Ord_contains_Transset]@prems) 1)); |
|
613 qed "Ord_Union"; |
|
614 |
|
615 val prems = Goal |
|
616 "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(UN x:A. B(x))"; |
|
617 by (rtac Ord_Union 1); |
|
618 by (etac RepFunE 1); |
|
619 by (etac ssubst 1); |
|
620 by (eresolve_tac prems 1); |
|
621 qed "Ord_UN"; |
|
622 |
|
623 (* No < version; consider (UN i:nat.i)=nat *) |
|
624 val [ordi,limit] = Goal |
|
625 "[| Ord(i); !!x. x:A ==> b(x) le i |] ==> (UN x:A. b(x)) le i"; |
|
626 by (rtac (le_imp_subset RS UN_least RS subset_imp_le) 1); |
|
627 by (REPEAT (ares_tac [ordi, Ord_UN, limit] 1 ORELSE etac (limit RS ltE) 1)); |
|
628 qed "UN_least_le"; |
|
629 |
|
630 val [jlti,limit] = Goal |
|
631 "[| j<i; !!x. x:A ==> b(x)<j |] ==> (UN x:A. succ(b(x))) < i"; |
|
632 by (rtac (jlti RS ltE) 1); |
|
633 by (rtac (UN_least_le RS lt_trans2) 1); |
|
634 by (REPEAT (ares_tac [jlti, succ_leI, limit] 1)); |
|
635 qed "UN_succ_least_lt"; |
|
636 |
|
637 Goal "[| a: A; i le b(a); Ord(UN x:A. b(x)) |] ==> i le (UN x:A. b(x))"; |
|
638 by (ftac ltD 1); |
|
639 by (rtac (le_imp_subset RS subset_trans RS subset_imp_le) 1); |
|
640 by (REPEAT (ares_tac [lt_Ord, UN_upper] 1)); |
|
641 qed "UN_upper_le"; |
|
642 |
|
643 val [leprem] = Goal |
|
644 "[| !!x. x:A ==> c(x) le d(x) |] ==> (UN x:A. c(x)) le (UN x:A. d(x))"; |
|
645 by (rtac UN_least_le 1); |
|
646 by (rtac UN_upper_le 2); |
|
647 by (etac leprem 3); |
|
648 by (ALLGOALS (asm_simp_tac (simpset() addsimps [Ord_UN, leprem RS le_Ord2]))); |
|
649 qed "le_implies_UN_le_UN"; |
|
650 |
|
651 Goal "Ord(i) ==> (UN y:i. succ(y)) = i"; |
|
652 by (blast_tac (claset() addIs [Ord_trans]) 1); |
|
653 qed "Ord_equality"; |
|
654 |
|
655 (*Holds for all transitive sets, not just ordinals*) |
|
656 Goal "Ord(i) ==> Union(i) <= i"; |
|
657 by (blast_tac (claset() addIs [Ord_trans]) 1); |
|
658 qed "Ord_Union_subset"; |
|
659 |
|
660 |
|
661 (*** Limit ordinals -- general properties ***) |
|
662 |
|
663 Goalw [Limit_def] "Limit(i) ==> Union(i) = i"; |
|
664 by (fast_tac (claset() addSIs [ltI] addSEs [ltE] addEs [Ord_trans]) 1); |
|
665 qed "Limit_Union_eq"; |
|
666 |
|
667 Goalw [Limit_def] "Limit(i) ==> Ord(i)"; |
|
668 by (etac conjunct1 1); |
|
669 qed "Limit_is_Ord"; |
|
670 |
|
671 Goalw [Limit_def] "Limit(i) ==> 0 < i"; |
|
672 by (etac (conjunct2 RS conjunct1) 1); |
|
673 qed "Limit_has_0"; |
|
674 |
|
675 Goalw [Limit_def] "[| Limit(i); j<i |] ==> succ(j) < i"; |
|
676 by (Blast_tac 1); |
|
677 qed "Limit_has_succ"; |
|
678 |
|
679 Goalw [Limit_def] |
|
680 "[| 0<i; ALL y. succ(y) ~= i |] ==> Limit(i)"; |
|
681 by (safe_tac subset_cs); |
|
682 by (rtac (not_le_iff_lt RS iffD1) 2); |
|
683 by (blast_tac le_cs 4); |
|
684 by (REPEAT (eresolve_tac [asm_rl, ltE, Ord_succ] 1)); |
|
685 qed "non_succ_LimitI"; |
|
686 |
|
687 Goal "Limit(succ(i)) ==> P"; |
|
688 by (rtac lt_irrefl 1); |
|
689 by (rtac Limit_has_succ 1); |
|
690 by (assume_tac 1); |
|
691 by (etac (Limit_is_Ord RS Ord_succD RS le_refl) 1); |
|
692 qed "succ_LimitE"; |
|
693 AddSEs [succ_LimitE]; |
|
694 |
|
695 Goal "~ Limit(succ(i))"; |
|
696 by (Blast_tac 1); |
|
697 qed "not_succ_Limit"; |
|
698 Addsimps [not_succ_Limit]; |
|
699 |
|
700 Goal "[| Limit(i); i le succ(j) |] ==> i le j"; |
|
701 by (blast_tac (claset() addSEs [leE]) 1); |
|
702 qed "Limit_le_succD"; |
|
703 |
|
704 (** Traditional 3-way case analysis on ordinals **) |
|
705 |
|
706 Goal "Ord(i) ==> i=0 | (EX j. Ord(j) & i=succ(j)) | Limit(i)"; |
|
707 by (blast_tac (claset() addSIs [non_succ_LimitI, Ord_0_lt]) 1); |
|
708 qed "Ord_cases_disj"; |
|
709 |
|
710 val major::prems = Goal |
|
711 "[| Ord(i); \ |
|
712 \ i=0 ==> P; \ |
|
713 \ !!j. [| Ord(j); i=succ(j) |] ==> P; \ |
|
714 \ Limit(i) ==> P \ |
|
715 \ |] ==> P"; |
|
716 by (cut_facts_tac [major RS Ord_cases_disj] 1); |
|
717 by (REPEAT (eresolve_tac (prems@[asm_rl, disjE, exE, conjE]) 1)); |
|
718 qed "Ord_cases"; |
|
719 |
|
720 val major::prems = Goal |
|
721 "[| Ord(i); \ |
|
722 \ P(0); \ |
|
723 \ !!x. [| Ord(x); P(x) |] ==> P(succ(x)); \ |
|
724 \ !!x. [| Limit(x); ALL y:x. P(y) |] ==> P(x) \ |
|
725 \ |] ==> P(i)"; |
|
726 by (resolve_tac [major RS trans_induct] 1); |
|
727 by (etac Ord_cases 1); |
|
728 by (ALLGOALS (blast_tac (claset() addIs prems))); |
|
729 qed "trans_induct3"; |
|