author | clasohm |
Wed, 07 Dec 1994 13:12:04 +0100 | |
changeset 760 | f0200e91b272 |
parent 537 | 3a84f846e649 |
child 782 | 200a16083201 |
permissions | -rw-r--r-- |
435 | 1 |
(* Title: ZF/Univ |
0 | 2 |
ID: $Id$ |
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
435 | 4 |
Copyright 1994 University of Cambridge |
0 | 5 |
|
6 |
The cumulative hierarchy and a small universe for recursive types |
|
7 |
*) |
|
8 |
||
9 |
open Univ; |
|
10 |
||
11 |
(*NOT SUITABLE FOR REWRITING -- RECURSIVE!*) |
|
12 |
goal Univ.thy "Vfrom(A,i) = A Un (UN j:i. Pow(Vfrom(A,j)))"; |
|
13 |
by (rtac (Vfrom_def RS def_transrec RS ssubst) 1); |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
14 |
by (simp_tac ZF_ss 1); |
760 | 15 |
qed "Vfrom"; |
0 | 16 |
|
17 |
(** Monotonicity **) |
|
18 |
||
19 |
goal Univ.thy "!!A B. A<=B ==> ALL j. i<=j --> Vfrom(A,i) <= Vfrom(B,j)"; |
|
20 |
by (eps_ind_tac "i" 1); |
|
21 |
by (rtac (impI RS allI) 1); |
|
22 |
by (rtac (Vfrom RS ssubst) 1); |
|
23 |
by (rtac (Vfrom RS ssubst) 1); |
|
24 |
by (etac Un_mono 1); |
|
25 |
by (rtac UN_mono 1); |
|
26 |
by (assume_tac 1); |
|
27 |
by (rtac Pow_mono 1); |
|
28 |
by (etac (bspec RS spec RS mp) 1); |
|
29 |
by (assume_tac 1); |
|
30 |
by (rtac subset_refl 1); |
|
760 | 31 |
qed "Vfrom_mono_lemma"; |
0 | 32 |
|
33 |
(* [| A<=B; i<=x |] ==> Vfrom(A,i) <= Vfrom(B,x) *) |
|
34 |
val Vfrom_mono = standard (Vfrom_mono_lemma RS spec RS mp); |
|
35 |
||
36 |
||
37 |
(** A fundamental equality: Vfrom does not require ordinals! **) |
|
38 |
||
39 |
goal Univ.thy "Vfrom(A,x) <= Vfrom(A,rank(x))"; |
|
40 |
by (eps_ind_tac "x" 1); |
|
41 |
by (rtac (Vfrom RS ssubst) 1); |
|
42 |
by (rtac (Vfrom RS ssubst) 1); |
|
27 | 43 |
by (fast_tac (ZF_cs addSIs [rank_lt RS ltD]) 1); |
760 | 44 |
qed "Vfrom_rank_subset1"; |
0 | 45 |
|
46 |
goal Univ.thy "Vfrom(A,rank(x)) <= Vfrom(A,x)"; |
|
47 |
by (eps_ind_tac "x" 1); |
|
48 |
by (rtac (Vfrom RS ssubst) 1); |
|
49 |
by (rtac (Vfrom RS ssubst) 1); |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
50 |
by (rtac (subset_refl RS Un_mono) 1); |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
51 |
by (rtac UN_least 1); |
27 | 52 |
(*expand rank(x1) = (UN y:x1. succ(rank(y))) in assumptions*) |
53 |
by (etac (rank RS equalityD1 RS subsetD RS UN_E) 1); |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
54 |
by (rtac subset_trans 1); |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
55 |
by (etac UN_upper 2); |
27 | 56 |
by (rtac (subset_refl RS Vfrom_mono RS subset_trans RS Pow_mono) 1); |
57 |
by (etac (ltI RS le_imp_subset) 1); |
|
58 |
by (rtac (Ord_rank RS Ord_succ) 1); |
|
0 | 59 |
by (etac bspec 1); |
60 |
by (assume_tac 1); |
|
760 | 61 |
qed "Vfrom_rank_subset2"; |
0 | 62 |
|
63 |
goal Univ.thy "Vfrom(A,rank(x)) = Vfrom(A,x)"; |
|
64 |
by (rtac equalityI 1); |
|
65 |
by (rtac Vfrom_rank_subset2 1); |
|
66 |
by (rtac Vfrom_rank_subset1 1); |
|
760 | 67 |
qed "Vfrom_rank_eq"; |
0 | 68 |
|
69 |
||
70 |
(*** Basic closure properties ***) |
|
71 |
||
72 |
goal Univ.thy "!!x y. y:x ==> 0 : Vfrom(A,x)"; |
|
73 |
by (rtac (Vfrom RS ssubst) 1); |
|
74 |
by (fast_tac ZF_cs 1); |
|
760 | 75 |
qed "zero_in_Vfrom"; |
0 | 76 |
|
77 |
goal Univ.thy "i <= Vfrom(A,i)"; |
|
78 |
by (eps_ind_tac "i" 1); |
|
79 |
by (rtac (Vfrom RS ssubst) 1); |
|
80 |
by (fast_tac ZF_cs 1); |
|
760 | 81 |
qed "i_subset_Vfrom"; |
0 | 82 |
|
83 |
goal Univ.thy "A <= Vfrom(A,i)"; |
|
84 |
by (rtac (Vfrom RS ssubst) 1); |
|
85 |
by (rtac Un_upper1 1); |
|
760 | 86 |
qed "A_subset_Vfrom"; |
0 | 87 |
|
488 | 88 |
val A_into_Vfrom = A_subset_Vfrom RS subsetD |> standard; |
89 |
||
0 | 90 |
goal Univ.thy "!!A a i. a <= Vfrom(A,i) ==> a: Vfrom(A,succ(i))"; |
91 |
by (rtac (Vfrom RS ssubst) 1); |
|
92 |
by (fast_tac ZF_cs 1); |
|
760 | 93 |
qed "subset_mem_Vfrom"; |
0 | 94 |
|
95 |
(** Finite sets and ordered pairs **) |
|
96 |
||
97 |
goal Univ.thy "!!a. a: Vfrom(A,i) ==> {a} : Vfrom(A,succ(i))"; |
|
98 |
by (rtac subset_mem_Vfrom 1); |
|
99 |
by (safe_tac ZF_cs); |
|
760 | 100 |
qed "singleton_in_Vfrom"; |
0 | 101 |
|
102 |
goal Univ.thy |
|
103 |
"!!A. [| a: Vfrom(A,i); b: Vfrom(A,i) |] ==> {a,b} : Vfrom(A,succ(i))"; |
|
104 |
by (rtac subset_mem_Vfrom 1); |
|
105 |
by (safe_tac ZF_cs); |
|
760 | 106 |
qed "doubleton_in_Vfrom"; |
0 | 107 |
|
108 |
goalw Univ.thy [Pair_def] |
|
109 |
"!!A. [| a: Vfrom(A,i); b: Vfrom(A,i) |] ==> \ |
|
110 |
\ <a,b> : Vfrom(A,succ(succ(i)))"; |
|
111 |
by (REPEAT (ares_tac [doubleton_in_Vfrom] 1)); |
|
760 | 112 |
qed "Pair_in_Vfrom"; |
0 | 113 |
|
114 |
val [prem] = goal Univ.thy |
|
115 |
"a<=Vfrom(A,i) ==> succ(a) : Vfrom(A,succ(succ(i)))"; |
|
116 |
by (REPEAT (resolve_tac [subset_mem_Vfrom, succ_subsetI] 1)); |
|
117 |
by (rtac (Vfrom_mono RSN (2,subset_trans)) 2); |
|
118 |
by (REPEAT (resolve_tac [prem, subset_refl, subset_succI] 1)); |
|
760 | 119 |
qed "succ_in_Vfrom"; |
0 | 120 |
|
121 |
(*** 0, successor and limit equations fof Vfrom ***) |
|
122 |
||
123 |
goal Univ.thy "Vfrom(A,0) = A"; |
|
124 |
by (rtac (Vfrom RS ssubst) 1); |
|
125 |
by (fast_tac eq_cs 1); |
|
760 | 126 |
qed "Vfrom_0"; |
0 | 127 |
|
128 |
goal Univ.thy "!!i. Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))"; |
|
129 |
by (rtac (Vfrom RS trans) 1); |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
130 |
by (rtac (succI1 RS RepFunI RS Union_upper RSN |
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
131 |
(2, equalityI RS subst_context)) 1); |
0 | 132 |
by (rtac UN_least 1); |
133 |
by (rtac (subset_refl RS Vfrom_mono RS Pow_mono) 1); |
|
27 | 134 |
by (etac (ltI RS le_imp_subset) 1); |
135 |
by (etac Ord_succ 1); |
|
760 | 136 |
qed "Vfrom_succ_lemma"; |
0 | 137 |
|
138 |
goal Univ.thy "Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))"; |
|
139 |
by (res_inst_tac [("x1", "succ(i)")] (Vfrom_rank_eq RS subst) 1); |
|
140 |
by (res_inst_tac [("x1", "i")] (Vfrom_rank_eq RS subst) 1); |
|
141 |
by (rtac (rank_succ RS ssubst) 1); |
|
142 |
by (rtac (Ord_rank RS Vfrom_succ_lemma) 1); |
|
760 | 143 |
qed "Vfrom_succ"; |
0 | 144 |
|
145 |
(*The premise distinguishes this from Vfrom(A,0); allowing X=0 forces |
|
146 |
the conclusion to be Vfrom(A,Union(X)) = A Un (UN y:X. Vfrom(A,y)) *) |
|
147 |
val [prem] = goal Univ.thy "y:X ==> Vfrom(A,Union(X)) = (UN y:X. Vfrom(A,y))"; |
|
148 |
by (rtac (Vfrom RS ssubst) 1); |
|
149 |
by (rtac equalityI 1); |
|
150 |
(*first inclusion*) |
|
151 |
by (rtac Un_least 1); |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
152 |
by (rtac (A_subset_Vfrom RS subset_trans) 1); |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
153 |
by (rtac (prem RS UN_upper) 1); |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
154 |
by (rtac UN_least 1); |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
155 |
by (etac UnionE 1); |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
156 |
by (rtac subset_trans 1); |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
157 |
by (etac UN_upper 2); |
0 | 158 |
by (rtac (Vfrom RS ssubst) 1); |
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
159 |
by (etac ([UN_upper, Un_upper2] MRS subset_trans) 1); |
0 | 160 |
(*opposite inclusion*) |
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
161 |
by (rtac UN_least 1); |
0 | 162 |
by (rtac (Vfrom RS ssubst) 1); |
163 |
by (fast_tac ZF_cs 1); |
|
760 | 164 |
qed "Vfrom_Union"; |
0 | 165 |
|
166 |
goal Univ.thy "!!i. Ord(i) ==> i=0 | (EX j. i=succ(j)) | Limit(i)"; |
|
27 | 167 |
by (fast_tac (ZF_cs addSIs [non_succ_LimitI, Ord_0_lt]) 1); |
760 | 168 |
qed "Ord_cases_lemma"; |
0 | 169 |
|
170 |
val major::prems = goal Univ.thy |
|
171 |
"[| Ord(i); \ |
|
172 |
\ i=0 ==> P; \ |
|
173 |
\ !!j. i=succ(j) ==> P; \ |
|
174 |
\ Limit(i) ==> P \ |
|
175 |
\ |] ==> P"; |
|
176 |
by (cut_facts_tac [major RS Ord_cases_lemma] 1); |
|
177 |
by (REPEAT (eresolve_tac (prems@[disjE, exE]) 1)); |
|
760 | 178 |
qed "Ord_cases"; |
0 | 179 |
|
180 |
||
181 |
(*** Vfrom applied to Limit ordinals ***) |
|
182 |
||
183 |
(*NB. limit ordinals are non-empty; |
|
184 |
Vfrom(A,0) = A = A Un (UN y:0. Vfrom(A,y)) *) |
|
185 |
val [limiti] = goal Univ.thy |
|
186 |
"Limit(i) ==> Vfrom(A,i) = (UN y:i. Vfrom(A,y))"; |
|
27 | 187 |
by (rtac (limiti RS (Limit_has_0 RS ltD) RS Vfrom_Union RS subst) 1); |
0 | 188 |
by (rtac (limiti RS Limit_Union_eq RS ssubst) 1); |
189 |
by (rtac refl 1); |
|
760 | 190 |
qed "Limit_Vfrom_eq"; |
0 | 191 |
|
27 | 192 |
goal Univ.thy "!!a. [| a: Vfrom(A,j); Limit(i); j<i |] ==> a : Vfrom(A,i)"; |
193 |
by (rtac (Limit_Vfrom_eq RS equalityD2 RS subsetD) 1); |
|
194 |
by (REPEAT (ares_tac [ltD RS UN_I] 1)); |
|
760 | 195 |
qed "Limit_VfromI"; |
27 | 196 |
|
197 |
val prems = goal Univ.thy |
|
198 |
"[| a: Vfrom(A,i); Limit(i); \ |
|
199 |
\ !!x. [| x<i; a: Vfrom(A,x) |] ==> R \ |
|
200 |
\ |] ==> R"; |
|
201 |
by (rtac (Limit_Vfrom_eq RS equalityD1 RS subsetD RS UN_E) 1); |
|
202 |
by (REPEAT (ares_tac (prems @ [ltI, Limit_is_Ord]) 1)); |
|
760 | 203 |
qed "Limit_VfromE"; |
0 | 204 |
|
516 | 205 |
val zero_in_VLimit = Limit_has_0 RS ltD RS zero_in_Vfrom; |
484 | 206 |
|
0 | 207 |
val [major,limiti] = goal Univ.thy |
208 |
"[| a: Vfrom(A,i); Limit(i) |] ==> {a} : Vfrom(A,i)"; |
|
27 | 209 |
by (rtac ([major,limiti] MRS Limit_VfromE) 1); |
210 |
by (etac ([singleton_in_Vfrom, limiti] MRS Limit_VfromI) 1); |
|
0 | 211 |
by (etac (limiti RS Limit_has_succ) 1); |
760 | 212 |
qed "singleton_in_VLimit"; |
0 | 213 |
|
214 |
val Vfrom_UnI1 = Un_upper1 RS (subset_refl RS Vfrom_mono RS subsetD) |
|
215 |
and Vfrom_UnI2 = Un_upper2 RS (subset_refl RS Vfrom_mono RS subsetD); |
|
216 |
||
217 |
(*Hard work is finding a single j:i such that {a,b}<=Vfrom(A,j)*) |
|
218 |
val [aprem,bprem,limiti] = goal Univ.thy |
|
219 |
"[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i) |] ==> \ |
|
220 |
\ {a,b} : Vfrom(A,i)"; |
|
27 | 221 |
by (rtac ([aprem,limiti] MRS Limit_VfromE) 1); |
222 |
by (rtac ([bprem,limiti] MRS Limit_VfromE) 1); |
|
223 |
by (rtac ([doubleton_in_Vfrom, limiti] MRS Limit_VfromI) 1); |
|
224 |
by (etac Vfrom_UnI1 1); |
|
225 |
by (etac Vfrom_UnI2 1); |
|
226 |
by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt] 1)); |
|
760 | 227 |
qed "doubleton_in_VLimit"; |
0 | 228 |
|
229 |
val [aprem,bprem,limiti] = goal Univ.thy |
|
230 |
"[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i) |] ==> \ |
|
231 |
\ <a,b> : Vfrom(A,i)"; |
|
232 |
(*Infer that a, b occur at ordinals x,xa < i.*) |
|
27 | 233 |
by (rtac ([aprem,limiti] MRS Limit_VfromE) 1); |
234 |
by (rtac ([bprem,limiti] MRS Limit_VfromE) 1); |
|
235 |
by (rtac ([Pair_in_Vfrom, limiti] MRS Limit_VfromI) 1); |
|
0 | 236 |
(*Infer that succ(succ(x Un xa)) < i *) |
27 | 237 |
by (etac Vfrom_UnI1 1); |
238 |
by (etac Vfrom_UnI2 1); |
|
239 |
by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt] 1)); |
|
760 | 240 |
qed "Pair_in_VLimit"; |
484 | 241 |
|
242 |
goal Univ.thy "!!i. Limit(i) ==> Vfrom(A,i)*Vfrom(A,i) <= Vfrom(A,i)"; |
|
516 | 243 |
by (REPEAT (ares_tac [subsetI,Pair_in_VLimit] 1 |
484 | 244 |
ORELSE eresolve_tac [SigmaE, ssubst] 1)); |
760 | 245 |
qed "product_VLimit"; |
484 | 246 |
|
516 | 247 |
val Sigma_subset_VLimit = |
248 |
[Sigma_mono, product_VLimit] MRS subset_trans |> standard; |
|
484 | 249 |
|
516 | 250 |
val nat_subset_VLimit = |
484 | 251 |
[nat_le_Limit RS le_imp_subset, i_subset_Vfrom] MRS subset_trans |
252 |
|> standard; |
|
253 |
||
488 | 254 |
goal Univ.thy "!!i. [| n: nat; Limit(i) |] ==> n : Vfrom(A,i)"; |
516 | 255 |
by (REPEAT (ares_tac [nat_subset_VLimit RS subsetD] 1)); |
760 | 256 |
qed "nat_into_VLimit"; |
484 | 257 |
|
258 |
(** Closure under disjoint union **) |
|
259 |
||
516 | 260 |
val zero_in_VLimit = Limit_has_0 RS ltD RS zero_in_Vfrom |> standard; |
484 | 261 |
|
262 |
goal Univ.thy "!!i. Limit(i) ==> 1 : Vfrom(A,i)"; |
|
516 | 263 |
by (REPEAT (ares_tac [nat_into_VLimit, nat_0I, nat_succI] 1)); |
760 | 264 |
qed "one_in_VLimit"; |
484 | 265 |
|
266 |
goalw Univ.thy [Inl_def] |
|
267 |
"!!A a. [| a: Vfrom(A,i); Limit(i) |] ==> Inl(a) : Vfrom(A,i)"; |
|
516 | 268 |
by (REPEAT (ares_tac [zero_in_VLimit, Pair_in_VLimit] 1)); |
760 | 269 |
qed "Inl_in_VLimit"; |
484 | 270 |
|
271 |
goalw Univ.thy [Inr_def] |
|
272 |
"!!A b. [| b: Vfrom(A,i); Limit(i) |] ==> Inr(b) : Vfrom(A,i)"; |
|
516 | 273 |
by (REPEAT (ares_tac [one_in_VLimit, Pair_in_VLimit] 1)); |
760 | 274 |
qed "Inr_in_VLimit"; |
484 | 275 |
|
276 |
goal Univ.thy "!!i. Limit(i) ==> Vfrom(C,i)+Vfrom(C,i) <= Vfrom(C,i)"; |
|
516 | 277 |
by (fast_tac (sum_cs addSIs [Inl_in_VLimit, Inr_in_VLimit]) 1); |
760 | 278 |
qed "sum_VLimit"; |
484 | 279 |
|
516 | 280 |
val sum_subset_VLimit = |
281 |
[sum_mono, sum_VLimit] MRS subset_trans |> standard; |
|
484 | 282 |
|
0 | 283 |
|
284 |
||
285 |
(*** Properties assuming Transset(A) ***) |
|
286 |
||
287 |
goal Univ.thy "!!i A. Transset(A) ==> Transset(Vfrom(A,i))"; |
|
288 |
by (eps_ind_tac "i" 1); |
|
289 |
by (rtac (Vfrom RS ssubst) 1); |
|
290 |
by (fast_tac (ZF_cs addSIs [Transset_Union_family, Transset_Un, |
|
291 |
Transset_Pow]) 1); |
|
760 | 292 |
qed "Transset_Vfrom"; |
0 | 293 |
|
294 |
goal Univ.thy "!!A i. Transset(A) ==> Vfrom(A, succ(i)) = Pow(Vfrom(A,i))"; |
|
295 |
by (rtac (Vfrom_succ RS trans) 1); |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
296 |
by (rtac (Un_upper2 RSN (2,equalityI)) 1); |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
297 |
by (rtac (subset_refl RSN (2,Un_least)) 1); |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
298 |
by (rtac (A_subset_Vfrom RS subset_trans) 1); |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
299 |
by (etac (Transset_Vfrom RS (Transset_iff_Pow RS iffD1)) 1); |
760 | 300 |
qed "Transset_Vfrom_succ"; |
0 | 301 |
|
435 | 302 |
goalw Ordinal.thy [Pair_def,Transset_def] |
0 | 303 |
"!!C. [| <a,b> <= C; Transset(C) |] ==> a: C & b: C"; |
304 |
by (fast_tac ZF_cs 1); |
|
760 | 305 |
qed "Transset_Pair_subset"; |
0 | 306 |
|
307 |
goal Univ.thy |
|
308 |
"!!a b.[| <a,b> <= Vfrom(A,i); Transset(A); Limit(i) |] ==> \ |
|
309 |
\ <a,b> : Vfrom(A,i)"; |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
310 |
by (etac (Transset_Pair_subset RS conjE) 1); |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
311 |
by (etac Transset_Vfrom 1); |
516 | 312 |
by (REPEAT (ares_tac [Pair_in_VLimit] 1)); |
760 | 313 |
qed "Transset_Pair_subset_VLimit"; |
0 | 314 |
|
315 |
||
316 |
(*** Closure under product/sum applied to elements -- thus Vfrom(A,i) |
|
317 |
is a model of simple type theory provided A is a transitive set |
|
318 |
and i is a limit ordinal |
|
319 |
***) |
|
320 |
||
187 | 321 |
(*General theorem for membership in Vfrom(A,i) when i is a limit ordinal*) |
322 |
val [aprem,bprem,limiti,step] = goal Univ.thy |
|
323 |
"[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); \ |
|
324 |
\ !!x y j. [| j<i; 1:j; x: Vfrom(A,j); y: Vfrom(A,j) \ |
|
325 |
\ |] ==> EX k. h(x,y): Vfrom(A,k) & k<i |] ==> \ |
|
326 |
\ h(a,b) : Vfrom(A,i)"; |
|
327 |
(*Infer that a, b occur at ordinals x,xa < i.*) |
|
328 |
by (rtac ([aprem,limiti] MRS Limit_VfromE) 1); |
|
329 |
by (rtac ([bprem,limiti] MRS Limit_VfromE) 1); |
|
330 |
by (res_inst_tac [("j1", "x Un xa Un succ(1)")] (step RS exE) 1); |
|
331 |
by (DO_GOAL [etac conjE, etac Limit_VfromI, rtac limiti, atac] 5); |
|
332 |
by (etac (Vfrom_UnI2 RS Vfrom_UnI1) 4); |
|
333 |
by (etac (Vfrom_UnI1 RS Vfrom_UnI1) 3); |
|
334 |
by (rtac (succI1 RS UnI2) 2); |
|
335 |
by (REPEAT (ares_tac [limiti, Limit_has_0, Limit_has_succ, Un_least_lt] 1)); |
|
760 | 336 |
qed "in_VLimit"; |
0 | 337 |
|
338 |
(** products **) |
|
339 |
||
340 |
goal Univ.thy |
|
187 | 341 |
"!!A. [| a: Vfrom(A,j); b: Vfrom(A,j); Transset(A) |] ==> \ |
342 |
\ a*b : Vfrom(A, succ(succ(succ(j))))"; |
|
0 | 343 |
by (dtac Transset_Vfrom 1); |
344 |
by (rtac subset_mem_Vfrom 1); |
|
345 |
by (rewtac Transset_def); |
|
346 |
by (fast_tac (ZF_cs addIs [Pair_in_Vfrom]) 1); |
|
760 | 347 |
qed "prod_in_Vfrom"; |
0 | 348 |
|
349 |
val [aprem,bprem,limiti,transset] = goal Univ.thy |
|
350 |
"[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) |] ==> \ |
|
351 |
\ a*b : Vfrom(A,i)"; |
|
516 | 352 |
by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1); |
187 | 353 |
by (REPEAT (ares_tac [exI, conjI, prod_in_Vfrom, transset, |
354 |
limiti RS Limit_has_succ] 1)); |
|
760 | 355 |
qed "prod_in_VLimit"; |
0 | 356 |
|
357 |
(** Disjoint sums, aka Quine ordered pairs **) |
|
358 |
||
359 |
goalw Univ.thy [sum_def] |
|
187 | 360 |
"!!A. [| a: Vfrom(A,j); b: Vfrom(A,j); Transset(A); 1:j |] ==> \ |
361 |
\ a+b : Vfrom(A, succ(succ(succ(j))))"; |
|
0 | 362 |
by (dtac Transset_Vfrom 1); |
363 |
by (rtac subset_mem_Vfrom 1); |
|
364 |
by (rewtac Transset_def); |
|
365 |
by (fast_tac (ZF_cs addIs [zero_in_Vfrom, Pair_in_Vfrom, |
|
366 |
i_subset_Vfrom RS subsetD]) 1); |
|
760 | 367 |
qed "sum_in_Vfrom"; |
0 | 368 |
|
369 |
val [aprem,bprem,limiti,transset] = goal Univ.thy |
|
370 |
"[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) |] ==> \ |
|
371 |
\ a+b : Vfrom(A,i)"; |
|
516 | 372 |
by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1); |
187 | 373 |
by (REPEAT (ares_tac [exI, conjI, sum_in_Vfrom, transset, |
374 |
limiti RS Limit_has_succ] 1)); |
|
760 | 375 |
qed "sum_in_VLimit"; |
0 | 376 |
|
377 |
(** function space! **) |
|
378 |
||
379 |
goalw Univ.thy [Pi_def] |
|
187 | 380 |
"!!A. [| a: Vfrom(A,j); b: Vfrom(A,j); Transset(A) |] ==> \ |
381 |
\ a->b : Vfrom(A, succ(succ(succ(succ(j)))))"; |
|
0 | 382 |
by (dtac Transset_Vfrom 1); |
383 |
by (rtac subset_mem_Vfrom 1); |
|
384 |
by (rtac (Collect_subset RS subset_trans) 1); |
|
385 |
by (rtac (Vfrom RS ssubst) 1); |
|
386 |
by (rtac (subset_trans RS subset_trans) 1); |
|
387 |
by (rtac Un_upper2 3); |
|
388 |
by (rtac (succI1 RS UN_upper) 2); |
|
389 |
by (rtac Pow_mono 1); |
|
390 |
by (rewtac Transset_def); |
|
391 |
by (fast_tac (ZF_cs addIs [Pair_in_Vfrom]) 1); |
|
760 | 392 |
qed "fun_in_Vfrom"; |
0 | 393 |
|
394 |
val [aprem,bprem,limiti,transset] = goal Univ.thy |
|
395 |
"[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) |] ==> \ |
|
396 |
\ a->b : Vfrom(A,i)"; |
|
516 | 397 |
by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1); |
187 | 398 |
by (REPEAT (ares_tac [exI, conjI, fun_in_Vfrom, transset, |
399 |
limiti RS Limit_has_succ] 1)); |
|
760 | 400 |
qed "fun_in_VLimit"; |
0 | 401 |
|
402 |
||
403 |
(*** The set Vset(i) ***) |
|
404 |
||
405 |
goal Univ.thy "Vset(i) = (UN j:i. Pow(Vset(j)))"; |
|
406 |
by (rtac (Vfrom RS ssubst) 1); |
|
407 |
by (fast_tac eq_cs 1); |
|
760 | 408 |
qed "Vset"; |
0 | 409 |
|
410 |
val Vset_succ = Transset_0 RS Transset_Vfrom_succ; |
|
411 |
||
412 |
val Transset_Vset = Transset_0 RS Transset_Vfrom; |
|
413 |
||
414 |
(** Characterisation of the elements of Vset(i) **) |
|
415 |
||
27 | 416 |
val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. b : Vset(i) --> rank(b) < i"; |
0 | 417 |
by (rtac (ordi RS trans_induct) 1); |
418 |
by (rtac (Vset RS ssubst) 1); |
|
419 |
by (safe_tac ZF_cs); |
|
420 |
by (rtac (rank RS ssubst) 1); |
|
27 | 421 |
by (rtac UN_succ_least_lt 1); |
422 |
by (fast_tac ZF_cs 2); |
|
423 |
by (REPEAT (ares_tac [ltI] 1)); |
|
760 | 424 |
qed "Vset_rank_imp1"; |
0 | 425 |
|
27 | 426 |
(* [| Ord(i); x : Vset(i) |] ==> rank(x) < i *) |
427 |
val VsetD = standard (Vset_rank_imp1 RS spec RS mp); |
|
0 | 428 |
|
429 |
val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. rank(b) : i --> b : Vset(i)"; |
|
430 |
by (rtac (ordi RS trans_induct) 1); |
|
431 |
by (rtac allI 1); |
|
432 |
by (rtac (Vset RS ssubst) 1); |
|
27 | 433 |
by (fast_tac (ZF_cs addSIs [rank_lt RS ltD]) 1); |
760 | 434 |
qed "Vset_rank_imp2"; |
0 | 435 |
|
27 | 436 |
goal Univ.thy "!!x i. rank(x)<i ==> x : Vset(i)"; |
437 |
by (etac ltE 1); |
|
438 |
by (etac (Vset_rank_imp2 RS spec RS mp) 1); |
|
439 |
by (assume_tac 1); |
|
760 | 440 |
qed "VsetI"; |
0 | 441 |
|
27 | 442 |
goal Univ.thy "!!i. Ord(i) ==> b : Vset(i) <-> rank(b) < i"; |
0 | 443 |
by (rtac iffI 1); |
27 | 444 |
by (REPEAT (eresolve_tac [asm_rl, VsetD, VsetI] 1)); |
760 | 445 |
qed "Vset_Ord_rank_iff"; |
0 | 446 |
|
27 | 447 |
goal Univ.thy "b : Vset(a) <-> rank(b) < rank(a)"; |
0 | 448 |
by (rtac (Vfrom_rank_eq RS subst) 1); |
449 |
by (rtac (Ord_rank RS Vset_Ord_rank_iff) 1); |
|
760 | 450 |
qed "Vset_rank_iff"; |
0 | 451 |
|
452 |
goal Univ.thy "!!i. Ord(i) ==> rank(Vset(i)) = i"; |
|
453 |
by (rtac (rank RS ssubst) 1); |
|
454 |
by (rtac equalityI 1); |
|
455 |
by (safe_tac ZF_cs); |
|
456 |
by (EVERY' [wtac UN_I, |
|
457 |
etac (i_subset_Vfrom RS subsetD), |
|
458 |
etac (Ord_in_Ord RS rank_of_Ord RS ssubst), |
|
459 |
assume_tac, |
|
460 |
rtac succI1] 3); |
|
27 | 461 |
by (REPEAT (eresolve_tac [asm_rl, VsetD RS ltD, Ord_trans] 1)); |
760 | 462 |
qed "rank_Vset"; |
0 | 463 |
|
464 |
(** Lemmas for reasoning about sets in terms of their elements' ranks **) |
|
465 |
||
466 |
goal Univ.thy "a <= Vset(rank(a))"; |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
467 |
by (rtac subsetI 1); |
27 | 468 |
by (etac (rank_lt RS VsetI) 1); |
760 | 469 |
qed "arg_subset_Vset_rank"; |
0 | 470 |
|
471 |
val [iprem] = goal Univ.thy |
|
472 |
"[| !!i. Ord(i) ==> a Int Vset(i) <= b |] ==> a <= b"; |
|
27 | 473 |
by (rtac ([subset_refl, arg_subset_Vset_rank] MRS |
474 |
Int_greatest RS subset_trans) 1); |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
475 |
by (rtac (Ord_rank RS iprem) 1); |
760 | 476 |
qed "Int_Vset_subset"; |
0 | 477 |
|
478 |
(** Set up an environment for simplification **) |
|
479 |
||
480 |
val rank_rls = [rank_Inl, rank_Inr, rank_pair1, rank_pair2]; |
|
27 | 481 |
val rank_trans_rls = rank_rls @ (rank_rls RLN (2, [lt_trans])); |
0 | 482 |
|
483 |
val rank_ss = ZF_ss |
|
27 | 484 |
addsimps [case_Inl, case_Inr, VsetI] |
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
485 |
addsimps rank_trans_rls; |
0 | 486 |
|
487 |
(** Recursion over Vset levels! **) |
|
488 |
||
489 |
(*NOT SUITABLE FOR REWRITING: recursive!*) |
|
490 |
goalw Univ.thy [Vrec_def] "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))"; |
|
491 |
by (rtac (transrec RS ssubst) 1); |
|
27 | 492 |
by (simp_tac (ZF_ss addsimps [Ord_rank, Ord_succ, VsetD RS ltD RS beta, |
493 |
VsetI RS beta, le_refl]) 1); |
|
760 | 494 |
qed "Vrec"; |
0 | 495 |
|
496 |
(*This form avoids giant explosions in proofs. NOTE USE OF == *) |
|
497 |
val rew::prems = goal Univ.thy |
|
498 |
"[| !!x. h(x)==Vrec(x,H) |] ==> \ |
|
499 |
\ h(a) = H(a, lam x: Vset(rank(a)). h(x))"; |
|
500 |
by (rewtac rew); |
|
501 |
by (rtac Vrec 1); |
|
760 | 502 |
qed "def_Vrec"; |
0 | 503 |
|
504 |
||
505 |
(*** univ(A) ***) |
|
506 |
||
507 |
goalw Univ.thy [univ_def] "!!A B. A<=B ==> univ(A) <= univ(B)"; |
|
508 |
by (etac Vfrom_mono 1); |
|
509 |
by (rtac subset_refl 1); |
|
760 | 510 |
qed "univ_mono"; |
0 | 511 |
|
512 |
goalw Univ.thy [univ_def] "!!A. Transset(A) ==> Transset(univ(A))"; |
|
513 |
by (etac Transset_Vfrom 1); |
|
760 | 514 |
qed "Transset_univ"; |
0 | 515 |
|
516 |
(** univ(A) as a limit **) |
|
517 |
||
518 |
goalw Univ.thy [univ_def] "univ(A) = (UN i:nat. Vfrom(A,i))"; |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
519 |
by (rtac (Limit_nat RS Limit_Vfrom_eq) 1); |
760 | 520 |
qed "univ_eq_UN"; |
0 | 521 |
|
522 |
goal Univ.thy "!!c. c <= univ(A) ==> c = (UN i:nat. c Int Vfrom(A,i))"; |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
523 |
by (rtac (subset_UN_iff_eq RS iffD1) 1); |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
524 |
by (etac (univ_eq_UN RS subst) 1); |
760 | 525 |
qed "subset_univ_eq_Int"; |
0 | 526 |
|
527 |
val [aprem, iprem] = goal Univ.thy |
|
528 |
"[| a <= univ(X); \ |
|
529 |
\ !!i. i:nat ==> a Int Vfrom(X,i) <= b \ |
|
530 |
\ |] ==> a <= b"; |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
531 |
by (rtac (aprem RS subset_univ_eq_Int RS ssubst) 1); |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
532 |
by (rtac UN_least 1); |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
533 |
by (etac iprem 1); |
760 | 534 |
qed "univ_Int_Vfrom_subset"; |
0 | 535 |
|
536 |
val prems = goal Univ.thy |
|
537 |
"[| a <= univ(X); b <= univ(X); \ |
|
538 |
\ !!i. i:nat ==> a Int Vfrom(X,i) = b Int Vfrom(X,i) \ |
|
539 |
\ |] ==> a = b"; |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
540 |
by (rtac equalityI 1); |
0 | 541 |
by (ALLGOALS |
542 |
(resolve_tac (prems RL [univ_Int_Vfrom_subset]) THEN' |
|
543 |
eresolve_tac (prems RL [equalityD1,equalityD2] RL [subset_trans]) THEN' |
|
544 |
rtac Int_lower1)); |
|
760 | 545 |
qed "univ_Int_Vfrom_eq"; |
0 | 546 |
|
547 |
(** Closure properties **) |
|
548 |
||
549 |
goalw Univ.thy [univ_def] "0 : univ(A)"; |
|
550 |
by (rtac (nat_0I RS zero_in_Vfrom) 1); |
|
760 | 551 |
qed "zero_in_univ"; |
0 | 552 |
|
553 |
goalw Univ.thy [univ_def] "A <= univ(A)"; |
|
554 |
by (rtac A_subset_Vfrom 1); |
|
760 | 555 |
qed "A_subset_univ"; |
0 | 556 |
|
557 |
val A_into_univ = A_subset_univ RS subsetD; |
|
558 |
||
559 |
(** Closure under unordered and ordered pairs **) |
|
560 |
||
561 |
goalw Univ.thy [univ_def] "!!A a. a: univ(A) ==> {a} : univ(A)"; |
|
516 | 562 |
by (REPEAT (ares_tac [singleton_in_VLimit, Limit_nat] 1)); |
760 | 563 |
qed "singleton_in_univ"; |
0 | 564 |
|
565 |
goalw Univ.thy [univ_def] |
|
566 |
"!!A a. [| a: univ(A); b: univ(A) |] ==> {a,b} : univ(A)"; |
|
516 | 567 |
by (REPEAT (ares_tac [doubleton_in_VLimit, Limit_nat] 1)); |
760 | 568 |
qed "doubleton_in_univ"; |
0 | 569 |
|
570 |
goalw Univ.thy [univ_def] |
|
571 |
"!!A a. [| a: univ(A); b: univ(A) |] ==> <a,b> : univ(A)"; |
|
516 | 572 |
by (REPEAT (ares_tac [Pair_in_VLimit, Limit_nat] 1)); |
760 | 573 |
qed "Pair_in_univ"; |
0 | 574 |
|
484 | 575 |
goalw Univ.thy [univ_def] "univ(A)*univ(A) <= univ(A)"; |
516 | 576 |
by (rtac (Limit_nat RS product_VLimit) 1); |
760 | 577 |
qed "product_univ"; |
0 | 578 |
|
579 |
||
580 |
(** The natural numbers **) |
|
581 |
||
582 |
goalw Univ.thy [univ_def] "nat <= univ(A)"; |
|
583 |
by (rtac i_subset_Vfrom 1); |
|
760 | 584 |
qed "nat_subset_univ"; |
0 | 585 |
|
586 |
(* n:nat ==> n:univ(A) *) |
|
587 |
val nat_into_univ = standard (nat_subset_univ RS subsetD); |
|
588 |
||
589 |
(** instances for 1 and 2 **) |
|
590 |
||
484 | 591 |
goalw Univ.thy [univ_def] "1 : univ(A)"; |
516 | 592 |
by (rtac (Limit_nat RS one_in_VLimit) 1); |
760 | 593 |
qed "one_in_univ"; |
0 | 594 |
|
595 |
(*unused!*) |
|
27 | 596 |
goal Univ.thy "succ(1) : univ(A)"; |
0 | 597 |
by (REPEAT (ares_tac [nat_into_univ, nat_0I, nat_succI] 1)); |
760 | 598 |
qed "two_in_univ"; |
0 | 599 |
|
600 |
goalw Univ.thy [bool_def] "bool <= univ(A)"; |
|
601 |
by (fast_tac (ZF_cs addSIs [zero_in_univ,one_in_univ]) 1); |
|
760 | 602 |
qed "bool_subset_univ"; |
0 | 603 |
|
604 |
val bool_into_univ = standard (bool_subset_univ RS subsetD); |
|
605 |
||
606 |
||
607 |
(** Closure under disjoint union **) |
|
608 |
||
484 | 609 |
goalw Univ.thy [univ_def] "!!A a. a: univ(A) ==> Inl(a) : univ(A)"; |
516 | 610 |
by (etac (Limit_nat RSN (2,Inl_in_VLimit)) 1); |
760 | 611 |
qed "Inl_in_univ"; |
0 | 612 |
|
484 | 613 |
goalw Univ.thy [univ_def] "!!A b. b: univ(A) ==> Inr(b) : univ(A)"; |
516 | 614 |
by (etac (Limit_nat RSN (2,Inr_in_VLimit)) 1); |
760 | 615 |
qed "Inr_in_univ"; |
0 | 616 |
|
484 | 617 |
goalw Univ.thy [univ_def] "univ(C)+univ(C) <= univ(C)"; |
516 | 618 |
by (rtac (Limit_nat RS sum_VLimit) 1); |
760 | 619 |
qed "sum_univ"; |
0 | 620 |
|
484 | 621 |
val sum_subset_univ = [sum_mono, sum_univ] MRS subset_trans |> standard; |
622 |
||
623 |
||
0 | 624 |
(** Closure under binary union -- use Un_least **) |
625 |
(** Closure under Collect -- use (Collect_subset RS subset_trans) **) |
|
626 |
(** Closure under RepFun -- use RepFun_subset **) |