author | lcp |
Thu, 30 Sep 1993 10:26:38 +0100 | |
changeset 15 | 6c6d2f6e3185 |
parent 6 | 8ce8c4d13d4d |
child 30 | d49df4181f0d |
permissions | -rw-r--r-- |
0 | 1 |
(* Title: ZF/ordinal.thy |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1993 University of Cambridge |
|
5 |
||
6 |
For ordinal.thy. Ordinals in Zermelo-Fraenkel Set Theory |
|
7 |
*) |
|
8 |
||
9 |
open Ord; |
|
10 |
||
11 |
(*** Rules for Transset ***) |
|
12 |
||
13 |
(** Two neat characterisations of Transset **) |
|
14 |
||
15 |
goalw Ord.thy [Transset_def] "Transset(A) <-> A<=Pow(A)"; |
|
16 |
by (fast_tac ZF_cs 1); |
|
17 |
val Transset_iff_Pow = result(); |
|
18 |
||
19 |
goalw Ord.thy [Transset_def] "Transset(A) <-> Union(succ(A)) = A"; |
|
20 |
by (fast_tac (eq_cs addSEs [equalityE]) 1); |
|
21 |
val Transset_iff_Union_succ = result(); |
|
22 |
||
23 |
(** Consequences of downwards closure **) |
|
24 |
||
25 |
goalw Ord.thy [Transset_def] |
|
26 |
"!!C a b. [| Transset(C); {a,b}: C |] ==> a:C & b: C"; |
|
27 |
by (fast_tac ZF_cs 1); |
|
28 |
val Transset_doubleton_D = result(); |
|
29 |
||
30 |
val [prem1,prem2] = goalw Ord.thy [Pair_def] |
|
31 |
"[| Transset(C); <a,b>: C |] ==> a:C & b: C"; |
|
32 |
by (cut_facts_tac [prem2] 1); |
|
33 |
by (fast_tac (ZF_cs addSDs [prem1 RS Transset_doubleton_D]) 1); |
|
34 |
val Transset_Pair_D = result(); |
|
35 |
||
36 |
val prem1::prems = goal Ord.thy |
|
37 |
"[| Transset(C); A*B <= C; b: B |] ==> A <= C"; |
|
38 |
by (cut_facts_tac prems 1); |
|
39 |
by (fast_tac (ZF_cs addSDs [prem1 RS Transset_Pair_D]) 1); |
|
40 |
val Transset_includes_domain = result(); |
|
41 |
||
42 |
val prem1::prems = goal Ord.thy |
|
43 |
"[| Transset(C); A*B <= C; a: A |] ==> B <= C"; |
|
44 |
by (cut_facts_tac prems 1); |
|
45 |
by (fast_tac (ZF_cs addSDs [prem1 RS Transset_Pair_D]) 1); |
|
46 |
val Transset_includes_range = result(); |
|
47 |
||
48 |
val [prem1,prem2] = goalw (merge_theories(Ord.thy,Sum.thy)) [sum_def] |
|
49 |
"[| Transset(C); A+B <= C |] ==> A <= C & B <= C"; |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
50 |
by (rtac (prem2 RS (Un_subset_iff RS iffD1) RS conjE) 1); |
0 | 51 |
by (REPEAT (etac (prem1 RS Transset_includes_range) 1 |
52 |
ORELSE resolve_tac [conjI, singletonI] 1)); |
|
53 |
val Transset_includes_summands = result(); |
|
54 |
||
55 |
val [prem] = goalw (merge_theories(Ord.thy,Sum.thy)) [sum_def] |
|
56 |
"Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)"; |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
57 |
by (rtac (Int_Un_distrib RS ssubst) 1); |
0 | 58 |
by (fast_tac (ZF_cs addSDs [prem RS Transset_Pair_D]) 1); |
59 |
val Transset_sum_Int_subset = result(); |
|
60 |
||
61 |
(** Closure properties **) |
|
62 |
||
63 |
goalw Ord.thy [Transset_def] "Transset(0)"; |
|
64 |
by (fast_tac ZF_cs 1); |
|
65 |
val Transset_0 = result(); |
|
66 |
||
67 |
goalw Ord.thy [Transset_def] |
|
68 |
"!!i j. [| Transset(i); Transset(j) |] ==> Transset(i Un j)"; |
|
69 |
by (fast_tac ZF_cs 1); |
|
70 |
val Transset_Un = result(); |
|
71 |
||
72 |
goalw Ord.thy [Transset_def] |
|
73 |
"!!i j. [| Transset(i); Transset(j) |] ==> Transset(i Int j)"; |
|
74 |
by (fast_tac ZF_cs 1); |
|
75 |
val Transset_Int = result(); |
|
76 |
||
77 |
goalw Ord.thy [Transset_def] "!!i. Transset(i) ==> Transset(succ(i))"; |
|
78 |
by (fast_tac ZF_cs 1); |
|
79 |
val Transset_succ = result(); |
|
80 |
||
81 |
goalw Ord.thy [Transset_def] "!!i. Transset(i) ==> Transset(Pow(i))"; |
|
82 |
by (fast_tac ZF_cs 1); |
|
83 |
val Transset_Pow = result(); |
|
84 |
||
85 |
goalw Ord.thy [Transset_def] "!!A. Transset(A) ==> Transset(Union(A))"; |
|
86 |
by (fast_tac ZF_cs 1); |
|
87 |
val Transset_Union = result(); |
|
88 |
||
89 |
val [Transprem] = goalw Ord.thy [Transset_def] |
|
90 |
"[| !!i. i:A ==> Transset(i) |] ==> Transset(Union(A))"; |
|
91 |
by (fast_tac (ZF_cs addEs [Transprem RS bspec RS subsetD]) 1); |
|
92 |
val Transset_Union_family = result(); |
|
93 |
||
94 |
val [prem,Transprem] = goalw Ord.thy [Transset_def] |
|
95 |
"[| j:A; !!i. i:A ==> Transset(i) |] ==> Transset(Inter(A))"; |
|
96 |
by (cut_facts_tac [prem] 1); |
|
97 |
by (fast_tac (ZF_cs addEs [Transprem RS bspec RS subsetD]) 1); |
|
98 |
val Transset_Inter_family = result(); |
|
99 |
||
100 |
(*** Natural Deduction rules for Ord ***) |
|
101 |
||
102 |
val prems = goalw Ord.thy [Ord_def] |
|
103 |
"[| Transset(i); !!x. x:i ==> Transset(x) |] ==> Ord(i) "; |
|
104 |
by (REPEAT (ares_tac (prems@[ballI,conjI]) 1)); |
|
105 |
val OrdI = result(); |
|
106 |
||
107 |
val [major] = goalw Ord.thy [Ord_def] |
|
108 |
"Ord(i) ==> Transset(i)"; |
|
109 |
by (rtac (major RS conjunct1) 1); |
|
110 |
val Ord_is_Transset = result(); |
|
111 |
||
112 |
val [major,minor] = goalw Ord.thy [Ord_def] |
|
113 |
"[| Ord(i); j:i |] ==> Transset(j) "; |
|
114 |
by (rtac (minor RS (major RS conjunct2 RS bspec)) 1); |
|
115 |
val Ord_contains_Transset = result(); |
|
116 |
||
117 |
(*** Lemmas for ordinals ***) |
|
118 |
||
119 |
goalw Ord.thy [Ord_def,Transset_def] "!!i j. [| Ord(i); j:i |] ==> Ord(j) "; |
|
120 |
by (fast_tac ZF_cs 1); |
|
121 |
val Ord_in_Ord = result(); |
|
122 |
||
123 |
goal Ord.thy "!!i j. [| Ord(i); Transset(j); j<=i |] ==> Ord(j)"; |
|
124 |
by (REPEAT (ares_tac [OrdI] 1 |
|
125 |
ORELSE eresolve_tac [Ord_contains_Transset, subsetD] 1)); |
|
126 |
val Ord_subset_Ord = result(); |
|
127 |
||
128 |
goalw Ord.thy [Ord_def,Transset_def] "!!i j. [| j:i; Ord(i) |] ==> j<=i"; |
|
129 |
by (fast_tac ZF_cs 1); |
|
130 |
val OrdmemD = result(); |
|
131 |
||
132 |
goal Ord.thy "!!i j k. [| i:j; j:k; Ord(k) |] ==> i:k"; |
|
133 |
by (REPEAT (ares_tac [OrdmemD RS subsetD] 1)); |
|
134 |
val Ord_trans = result(); |
|
135 |
||
136 |
goal Ord.thy "!!i j. [| i:j; Ord(j) |] ==> succ(i) <= j"; |
|
137 |
by (REPEAT (ares_tac [OrdmemD RSN (2,succ_subsetI)] 1)); |
|
138 |
val Ord_succ_subsetI = result(); |
|
139 |
||
140 |
||
141 |
(*** The construction of ordinals: 0, succ, Union ***) |
|
142 |
||
143 |
goal Ord.thy "Ord(0)"; |
|
144 |
by (REPEAT (ares_tac [OrdI,Transset_0] 1 ORELSE etac emptyE 1)); |
|
145 |
val Ord_0 = result(); |
|
146 |
||
147 |
goal Ord.thy "!!i. Ord(i) ==> Ord(succ(i))"; |
|
148 |
by (REPEAT (ares_tac [OrdI,Transset_succ] 1 |
|
149 |
ORELSE eresolve_tac [succE,ssubst,Ord_is_Transset, |
|
150 |
Ord_contains_Transset] 1)); |
|
151 |
val Ord_succ = result(); |
|
152 |
||
153 |
val nonempty::prems = goal Ord.thy |
|
154 |
"[| j:A; !!i. i:A ==> Ord(i) |] ==> Ord(Inter(A))"; |
|
155 |
by (rtac (nonempty RS Transset_Inter_family RS OrdI) 1); |
|
156 |
by (rtac Ord_is_Transset 1); |
|
157 |
by (REPEAT (ares_tac ([Ord_contains_Transset,nonempty]@prems) 1 |
|
158 |
ORELSE etac InterD 1)); |
|
159 |
val Ord_Inter = result(); |
|
160 |
||
161 |
val jmemA::prems = goal Ord.thy |
|
162 |
"[| j:A; !!x. x:A ==> Ord(B(x)) |] ==> Ord(INT x:A. B(x))"; |
|
163 |
by (rtac (jmemA RS RepFunI RS Ord_Inter) 1); |
|
164 |
by (etac RepFunE 1); |
|
165 |
by (etac ssubst 1); |
|
166 |
by (eresolve_tac prems 1); |
|
167 |
val Ord_INT = result(); |
|
168 |
||
169 |
||
170 |
(*** Natural Deduction rules for Memrel ***) |
|
171 |
||
172 |
goalw Ord.thy [Memrel_def] "<a,b> : Memrel(A) <-> a:b & a:A & b:A"; |
|
173 |
by (fast_tac ZF_cs 1); |
|
174 |
val Memrel_iff = result(); |
|
175 |
||
176 |
val prems = goal Ord.thy "[| a: b; a: A; b: A |] ==> <a,b> : Memrel(A)"; |
|
177 |
by (REPEAT (resolve_tac (prems@[conjI, Memrel_iff RS iffD2]) 1)); |
|
178 |
val MemrelI = result(); |
|
179 |
||
180 |
val [major,minor] = goal Ord.thy |
|
181 |
"[| <a,b> : Memrel(A); \ |
|
182 |
\ [| a: A; b: A; a:b |] ==> P \ |
|
183 |
\ |] ==> P"; |
|
184 |
by (rtac (major RS (Memrel_iff RS iffD1) RS conjE) 1); |
|
185 |
by (etac conjE 1); |
|
186 |
by (rtac minor 1); |
|
187 |
by (REPEAT (assume_tac 1)); |
|
188 |
val MemrelE = result(); |
|
189 |
||
190 |
(*The membership relation (as a set) is well-founded. |
|
191 |
Proof idea: show A<=B by applying the foundation axiom to A-B *) |
|
192 |
goalw Ord.thy [wf_def] "wf(Memrel(A))"; |
|
193 |
by (EVERY1 [rtac (foundation RS disjE RS allI), |
|
194 |
etac disjI1, |
|
195 |
etac bexE, |
|
196 |
rtac (impI RS allI RS bexI RS disjI2), |
|
197 |
etac MemrelE, |
|
198 |
etac bspec, |
|
199 |
REPEAT o assume_tac]); |
|
200 |
val wf_Memrel = result(); |
|
201 |
||
202 |
(*** Transfinite induction ***) |
|
203 |
||
204 |
(*Epsilon induction over a transitive set*) |
|
205 |
val major::prems = goalw Ord.thy [Transset_def] |
|
206 |
"[| i: k; Transset(k); \ |
|
207 |
\ !!x.[| x: k; ALL y:x. P(y) |] ==> P(x) \ |
|
208 |
\ |] ==> P(i)"; |
|
209 |
by (rtac (major RS (wf_Memrel RS wf_induct2)) 1); |
|
210 |
by (fast_tac (ZF_cs addEs [MemrelE]) 1); |
|
211 |
by (resolve_tac prems 1); |
|
212 |
by (assume_tac 1); |
|
213 |
by (cut_facts_tac prems 1); |
|
214 |
by (fast_tac (ZF_cs addIs [MemrelI]) 1); |
|
215 |
val Transset_induct = result(); |
|
216 |
||
217 |
(*Induction over an ordinal*) |
|
218 |
val Ord_induct = Ord_is_Transset RSN (2, Transset_induct); |
|
219 |
||
220 |
(*Induction over the class of ordinals -- a useful corollary of Ord_induct*) |
|
221 |
val [major,indhyp] = goal Ord.thy |
|
222 |
"[| Ord(i); \ |
|
223 |
\ !!x.[| Ord(x); ALL y:x. P(y) |] ==> P(x) \ |
|
224 |
\ |] ==> P(i)"; |
|
225 |
by (rtac (major RS Ord_succ RS (succI1 RS Ord_induct)) 1); |
|
226 |
by (rtac indhyp 1); |
|
227 |
by (rtac (major RS Ord_succ RS Ord_in_Ord) 1); |
|
228 |
by (REPEAT (assume_tac 1)); |
|
229 |
val trans_induct = result(); |
|
230 |
||
231 |
(*Perform induction on i, then prove the Ord(i) subgoal using prems. *) |
|
232 |
fun trans_ind_tac a prems i = |
|
233 |
EVERY [res_inst_tac [("i",a)] trans_induct i, |
|
234 |
rename_last_tac a ["1"] (i+1), |
|
235 |
ares_tac prems i]; |
|
236 |
||
237 |
||
238 |
(*** Fundamental properties of the epsilon ordering (< on ordinals) ***) |
|
239 |
||
240 |
(*Finds contradictions for the following proof*) |
|
241 |
val Ord_trans_tac = EVERY' [etac notE, etac Ord_trans, REPEAT o atac]; |
|
242 |
||
243 |
(** Proving that "member" is a linear ordering on the ordinals **) |
|
244 |
||
245 |
val prems = goal Ord.thy |
|
246 |
"Ord(i) ==> (ALL j. Ord(j) --> i:j | i=j | j:i)"; |
|
247 |
by (trans_ind_tac "i" prems 1); |
|
248 |
by (rtac (impI RS allI) 1); |
|
249 |
by (trans_ind_tac "j" [] 1); |
|
250 |
by (DEPTH_SOLVE (swap_res_tac [disjCI,equalityI,subsetI] 1 |
|
251 |
ORELSE ball_tac 1 |
|
252 |
ORELSE eresolve_tac [impE,disjE,allE] 1 |
|
253 |
ORELSE hyp_subst_tac 1 |
|
254 |
ORELSE Ord_trans_tac 1)); |
|
255 |
val Ord_linear_lemma = result(); |
|
256 |
||
257 |
val ordi::ordj::prems = goal Ord.thy |
|
258 |
"[| Ord(i); Ord(j); i:j ==> P; i=j ==> P; j:i ==> P |] \ |
|
259 |
\ ==> P"; |
|
260 |
by (rtac (ordi RS Ord_linear_lemma RS spec RS impE) 1); |
|
261 |
by (rtac ordj 1); |
|
262 |
by (REPEAT (eresolve_tac (prems@[asm_rl,disjE]) 1)); |
|
263 |
val Ord_linear = result(); |
|
264 |
||
265 |
val prems = goal Ord.thy |
|
266 |
"[| Ord(i); Ord(j); i<=j ==> P; j<=i ==> P |] \ |
|
267 |
\ ==> P"; |
|
268 |
by (res_inst_tac [("i","i"),("j","j")] Ord_linear 1); |
|
269 |
by (DEPTH_SOLVE (ares_tac (prems@[subset_refl]) 1 |
|
270 |
ORELSE eresolve_tac [asm_rl,OrdmemD,ssubst] 1)); |
|
271 |
val Ord_subset = result(); |
|
272 |
||
273 |
goal Ord.thy "!!i j. [| j<=i; ~ i<=j; Ord(i); Ord(j) |] ==> j:i"; |
|
274 |
by (etac Ord_linear 1); |
|
275 |
by (REPEAT (ares_tac [subset_refl] 1 |
|
276 |
ORELSE eresolve_tac [notE,OrdmemD,ssubst] 1)); |
|
277 |
val Ord_member = result(); |
|
278 |
||
279 |
val [prem] = goal Ord.thy "Ord(i) ==> 0: succ(i)"; |
|
280 |
by (rtac (empty_subsetI RS Ord_member) 1); |
|
281 |
by (fast_tac ZF_cs 1); |
|
282 |
by (rtac (prem RS Ord_succ) 1); |
|
283 |
by (rtac Ord_0 1); |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
284 |
val Ord_0_in_succ = result(); |
0 | 285 |
|
286 |
goal Ord.thy "!!i j. [| Ord(i); Ord(j) |] ==> j:i <-> j<=i & ~(i<=j)"; |
|
287 |
by (rtac iffI 1); |
|
288 |
by (rtac conjI 1); |
|
289 |
by (etac OrdmemD 1); |
|
290 |
by (rtac (mem_anti_refl RS notI) 2); |
|
291 |
by (etac subsetD 2); |
|
292 |
by (REPEAT (eresolve_tac [asm_rl, conjE, Ord_member] 1)); |
|
293 |
val Ord_member_iff = result(); |
|
294 |
||
295 |
goal Ord.thy "!!i. Ord(i) ==> 0:i <-> ~ i=0"; |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
296 |
by (etac (Ord_0 RSN (2,Ord_member_iff) RS iff_trans) 1); |
0 | 297 |
by (fast_tac eq_cs 1); |
298 |
val Ord_0_member_iff = result(); |
|
299 |
||
300 |
(** For ordinals, i: succ(j) means 'less-than or equals' **) |
|
301 |
||
302 |
goal Ord.thy "!!i j. [| j<=i; Ord(i); Ord(j) |] ==> j : succ(i)"; |
|
303 |
by (rtac Ord_member 1); |
|
304 |
by (REPEAT (ares_tac [Ord_succ] 3)); |
|
305 |
by (rtac (mem_anti_refl RS notI) 2); |
|
306 |
by (etac subsetD 2); |
|
307 |
by (ALLGOALS (fast_tac ZF_cs)); |
|
308 |
val member_succI = result(); |
|
309 |
||
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
310 |
(*Recall Ord_succ_subsetI, namely [| i:j; Ord(j) |] ==> succ(i) <= j *) |
0 | 311 |
goalw Ord.thy [Transset_def,Ord_def] |
312 |
"!!i j. [| i : succ(j); Ord(j) |] ==> i<=j"; |
|
313 |
by (fast_tac ZF_cs 1); |
|
314 |
val member_succD = result(); |
|
315 |
||
316 |
goal Ord.thy "!!i j. [| Ord(i); Ord(j) |] ==> j:succ(i) <-> j<=i"; |
|
317 |
by (fast_tac (subset_cs addSEs [member_succI, member_succD]) 1); |
|
318 |
val member_succ_iff = result(); |
|
319 |
||
320 |
goal Ord.thy |
|
321 |
"!!i j. [| Ord(i); Ord(j) |] ==> i<=succ(j) <-> i<=j | i=succ(j)"; |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
322 |
by (asm_simp_tac (ZF_ss addsimps [member_succ_iff RS iff_sym, Ord_succ]) 1); |
0 | 323 |
by (fast_tac ZF_cs 1); |
324 |
val subset_succ_iff = result(); |
|
325 |
||
326 |
goal Ord.thy "!!i j. [| i:succ(j); j:k; Ord(k) |] ==> i:k"; |
|
327 |
by (fast_tac (ZF_cs addEs [Ord_trans]) 1); |
|
328 |
val Ord_trans1 = result(); |
|
329 |
||
330 |
goal Ord.thy "!!i j. [| i:j; j:succ(k); Ord(k) |] ==> i:k"; |
|
331 |
by (fast_tac (ZF_cs addEs [Ord_trans]) 1); |
|
332 |
val Ord_trans2 = result(); |
|
333 |
||
334 |
goal Ord.thy "!!i jk. [| i:j; j<=k; Ord(k) |] ==> i:k"; |
|
335 |
by (fast_tac (ZF_cs addEs [Ord_trans]) 1); |
|
336 |
val Ord_transsub2 = result(); |
|
337 |
||
338 |
goal Ord.thy "!!i j. [| i:j; Ord(j) |] ==> succ(i) : succ(j)"; |
|
339 |
by (rtac member_succI 1); |
|
340 |
by (REPEAT (ares_tac [subsetI,Ord_succ,Ord_in_Ord] 1 |
|
341 |
ORELSE eresolve_tac [succE,Ord_trans,ssubst] 1)); |
|
342 |
val succ_mem_succI = result(); |
|
343 |
||
344 |
goal Ord.thy "!!i j. [| succ(i) : succ(j); Ord(j) |] ==> i:j"; |
|
345 |
by (REPEAT (eresolve_tac [asm_rl, make_elim member_succD, succ_subsetE] 1)); |
|
346 |
val succ_mem_succE = result(); |
|
347 |
||
348 |
goal Ord.thy "!!i j. Ord(j) ==> succ(i) : succ(j) <-> i:j"; |
|
349 |
by (REPEAT (ares_tac [iffI,succ_mem_succI,succ_mem_succE] 1)); |
|
350 |
val succ_mem_succ_iff = result(); |
|
351 |
||
352 |
goal Ord.thy "!!i j. [| i<=j; Ord(i); Ord(j) |] ==> succ(i) <= succ(j)"; |
|
353 |
by (rtac (member_succI RS succ_mem_succI RS member_succD) 1); |
|
354 |
by (REPEAT (ares_tac [Ord_succ] 1)); |
|
355 |
val Ord_succ_mono = result(); |
|
356 |
||
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
357 |
(** Union and Intersection **) |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
358 |
|
0 | 359 |
goal Ord.thy "!!i j k. [| i:k; j:k; Ord(k) |] ==> i Un j : k"; |
360 |
by (res_inst_tac [("i","i"),("j","j")] Ord_subset 1); |
|
361 |
by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1)); |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
362 |
by (asm_simp_tac (ZF_ss addsimps [subset_Un_iff RS iffD1]) 1); |
0 | 363 |
by (rtac (Un_commute RS ssubst) 1); |
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
364 |
by (asm_simp_tac (ZF_ss addsimps [subset_Un_iff RS iffD1]) 1); |
0 | 365 |
val Ord_member_UnI = result(); |
366 |
||
367 |
goal Ord.thy "!!i j k. [| i:k; j:k; Ord(k) |] ==> i Int j : k"; |
|
368 |
by (res_inst_tac [("i","i"),("j","j")] Ord_subset 1); |
|
369 |
by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1)); |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
370 |
by (asm_simp_tac (ZF_ss addsimps [subset_Int_iff RS iffD1]) 1); |
0 | 371 |
by (rtac (Int_commute RS ssubst) 1); |
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
372 |
by (asm_simp_tac (ZF_ss addsimps [subset_Int_iff RS iffD1]) 1); |
0 | 373 |
val Ord_member_IntI = result(); |
374 |
||
375 |
||
376 |
(*** Results about limits ***) |
|
377 |
||
378 |
val prems = goal Ord.thy "[| !!i. i:A ==> Ord(i) |] ==> Ord(Union(A))"; |
|
379 |
by (rtac (Ord_is_Transset RS Transset_Union_family RS OrdI) 1); |
|
380 |
by (REPEAT (etac UnionE 1 ORELSE ares_tac ([Ord_contains_Transset]@prems) 1)); |
|
381 |
val Ord_Union = result(); |
|
382 |
||
383 |
val prems = goal Ord.thy "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(UN x:A. B(x))"; |
|
384 |
by (rtac Ord_Union 1); |
|
385 |
by (etac RepFunE 1); |
|
386 |
by (etac ssubst 1); |
|
387 |
by (eresolve_tac prems 1); |
|
388 |
val Ord_UN = result(); |
|
389 |
||
390 |
(*The upper bound must be a successor ordinal -- |
|
391 |
consider that (UN i:nat.i)=nat although nat is an upper bound of each i*) |
|
392 |
val [ordi,limit] = goal Ord.thy |
|
393 |
"[| Ord(i); !!y. y:A ==> f(y): succ(i) |] ==> (UN y:A. f(y)) : succ(i)"; |
|
394 |
by (rtac (member_succD RS UN_least RS member_succI) 1); |
|
395 |
by (REPEAT (ares_tac [ordi, Ord_UN, ordi RS Ord_succ RS Ord_in_Ord, |
|
396 |
limit] 1)); |
|
397 |
val sup_least = result(); |
|
398 |
||
399 |
val [jmemi,ordi,limit] = goal Ord.thy |
|
400 |
"[| j: i; Ord(i); !!y. y:A ==> f(y): j |] ==> (UN y:A. succ(f(y))) : i"; |
|
401 |
by (cut_facts_tac [jmemi RS (ordi RS Ord_in_Ord)] 1); |
|
402 |
by (rtac (sup_least RS Ord_trans2) 1); |
|
403 |
by (REPEAT (ares_tac [jmemi, ordi, succ_mem_succI, limit] 1)); |
|
404 |
val sup_least2 = result(); |
|
405 |
||
406 |
goal Ord.thy "!!i. Ord(i) ==> (UN y:i. succ(y)) = i"; |
|
407 |
by (fast_tac (eq_cs addSEs [Ord_trans1]) 1); |
|
408 |
val Ord_equality = result(); |
|
409 |
||
410 |
(*Holds for all transitive sets, not just ordinals*) |
|
411 |
goal Ord.thy "!!i. Ord(i) ==> Union(i) <= i"; |
|
412 |
by (fast_tac (ZF_cs addSEs [Ord_trans]) 1); |
|
413 |
val Ord_Union_subset = result(); |