author | lcp |
Fri, 23 Dec 1994 16:29:53 +0100 | |
changeset 828 | 03d7bfa70289 |
parent 803 | 4c8333ab3eae |
child 853 | a4b286dfdd6f |
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) *) |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
34 |
bind_thm ("Vfrom_mono", (Vfrom_mono_lemma RS spec RS mp)); |
0 | 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 |
|
803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
88 |
bind_thm ("A_into_Vfrom", A_subset_Vfrom RS subsetD); |
488 | 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 |
|
803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
247 |
bind_thm ("Sigma_subset_VLimit", |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
248 |
[Sigma_mono, product_VLimit] MRS subset_trans); |
484 | 249 |
|
803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
250 |
bind_thm ("nat_subset_VLimit", |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
251 |
[nat_le_Limit RS le_imp_subset, i_subset_Vfrom] MRS subset_trans); |
484 | 252 |
|
488 | 253 |
goal Univ.thy "!!i. [| n: nat; Limit(i) |] ==> n : Vfrom(A,i)"; |
516 | 254 |
by (REPEAT (ares_tac [nat_subset_VLimit RS subsetD] 1)); |
760 | 255 |
qed "nat_into_VLimit"; |
484 | 256 |
|
257 |
(** Closure under disjoint union **) |
|
258 |
||
803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
259 |
bind_thm ("zero_in_VLimit", Limit_has_0 RS ltD RS zero_in_Vfrom); |
484 | 260 |
|
261 |
goal Univ.thy "!!i. Limit(i) ==> 1 : Vfrom(A,i)"; |
|
516 | 262 |
by (REPEAT (ares_tac [nat_into_VLimit, nat_0I, nat_succI] 1)); |
760 | 263 |
qed "one_in_VLimit"; |
484 | 264 |
|
265 |
goalw Univ.thy [Inl_def] |
|
266 |
"!!A a. [| a: Vfrom(A,i); Limit(i) |] ==> Inl(a) : Vfrom(A,i)"; |
|
516 | 267 |
by (REPEAT (ares_tac [zero_in_VLimit, Pair_in_VLimit] 1)); |
760 | 268 |
qed "Inl_in_VLimit"; |
484 | 269 |
|
270 |
goalw Univ.thy [Inr_def] |
|
271 |
"!!A b. [| b: Vfrom(A,i); Limit(i) |] ==> Inr(b) : Vfrom(A,i)"; |
|
516 | 272 |
by (REPEAT (ares_tac [one_in_VLimit, Pair_in_VLimit] 1)); |
760 | 273 |
qed "Inr_in_VLimit"; |
484 | 274 |
|
275 |
goal Univ.thy "!!i. Limit(i) ==> Vfrom(C,i)+Vfrom(C,i) <= Vfrom(C,i)"; |
|
516 | 276 |
by (fast_tac (sum_cs addSIs [Inl_in_VLimit, Inr_in_VLimit]) 1); |
760 | 277 |
qed "sum_VLimit"; |
484 | 278 |
|
803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
279 |
bind_thm ("sum_subset_VLimit", [sum_mono, sum_VLimit] MRS subset_trans); |
484 | 280 |
|
0 | 281 |
|
282 |
||
283 |
(*** Properties assuming Transset(A) ***) |
|
284 |
||
285 |
goal Univ.thy "!!i A. Transset(A) ==> Transset(Vfrom(A,i))"; |
|
286 |
by (eps_ind_tac "i" 1); |
|
287 |
by (rtac (Vfrom RS ssubst) 1); |
|
288 |
by (fast_tac (ZF_cs addSIs [Transset_Union_family, Transset_Un, |
|
289 |
Transset_Pow]) 1); |
|
760 | 290 |
qed "Transset_Vfrom"; |
0 | 291 |
|
292 |
goal Univ.thy "!!A i. Transset(A) ==> Vfrom(A, succ(i)) = Pow(Vfrom(A,i))"; |
|
293 |
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
|
294 |
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
|
295 |
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
|
296 |
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
|
297 |
by (etac (Transset_Vfrom RS (Transset_iff_Pow RS iffD1)) 1); |
760 | 298 |
qed "Transset_Vfrom_succ"; |
0 | 299 |
|
435 | 300 |
goalw Ordinal.thy [Pair_def,Transset_def] |
0 | 301 |
"!!C. [| <a,b> <= C; Transset(C) |] ==> a: C & b: C"; |
302 |
by (fast_tac ZF_cs 1); |
|
760 | 303 |
qed "Transset_Pair_subset"; |
0 | 304 |
|
305 |
goal Univ.thy |
|
306 |
"!!a b.[| <a,b> <= Vfrom(A,i); Transset(A); Limit(i) |] ==> \ |
|
307 |
\ <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
|
308 |
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
|
309 |
by (etac Transset_Vfrom 1); |
516 | 310 |
by (REPEAT (ares_tac [Pair_in_VLimit] 1)); |
760 | 311 |
qed "Transset_Pair_subset_VLimit"; |
0 | 312 |
|
313 |
||
314 |
(*** Closure under product/sum applied to elements -- thus Vfrom(A,i) |
|
315 |
is a model of simple type theory provided A is a transitive set |
|
316 |
and i is a limit ordinal |
|
317 |
***) |
|
318 |
||
187 | 319 |
(*General theorem for membership in Vfrom(A,i) when i is a limit ordinal*) |
320 |
val [aprem,bprem,limiti,step] = goal Univ.thy |
|
321 |
"[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); \ |
|
322 |
\ !!x y j. [| j<i; 1:j; x: Vfrom(A,j); y: Vfrom(A,j) \ |
|
323 |
\ |] ==> EX k. h(x,y): Vfrom(A,k) & k<i |] ==> \ |
|
324 |
\ h(a,b) : Vfrom(A,i)"; |
|
325 |
(*Infer that a, b occur at ordinals x,xa < i.*) |
|
326 |
by (rtac ([aprem,limiti] MRS Limit_VfromE) 1); |
|
327 |
by (rtac ([bprem,limiti] MRS Limit_VfromE) 1); |
|
828 | 328 |
by (res_inst_tac [("j1", "x Un xa Un 2")] (step RS exE) 1); |
187 | 329 |
by (DO_GOAL [etac conjE, etac Limit_VfromI, rtac limiti, atac] 5); |
330 |
by (etac (Vfrom_UnI2 RS Vfrom_UnI1) 4); |
|
331 |
by (etac (Vfrom_UnI1 RS Vfrom_UnI1) 3); |
|
332 |
by (rtac (succI1 RS UnI2) 2); |
|
333 |
by (REPEAT (ares_tac [limiti, Limit_has_0, Limit_has_succ, Un_least_lt] 1)); |
|
760 | 334 |
qed "in_VLimit"; |
0 | 335 |
|
336 |
(** products **) |
|
337 |
||
338 |
goal Univ.thy |
|
187 | 339 |
"!!A. [| a: Vfrom(A,j); b: Vfrom(A,j); Transset(A) |] ==> \ |
340 |
\ a*b : Vfrom(A, succ(succ(succ(j))))"; |
|
0 | 341 |
by (dtac Transset_Vfrom 1); |
342 |
by (rtac subset_mem_Vfrom 1); |
|
343 |
by (rewtac Transset_def); |
|
344 |
by (fast_tac (ZF_cs addIs [Pair_in_Vfrom]) 1); |
|
760 | 345 |
qed "prod_in_Vfrom"; |
0 | 346 |
|
347 |
val [aprem,bprem,limiti,transset] = goal Univ.thy |
|
348 |
"[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) |] ==> \ |
|
349 |
\ a*b : Vfrom(A,i)"; |
|
516 | 350 |
by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1); |
187 | 351 |
by (REPEAT (ares_tac [exI, conjI, prod_in_Vfrom, transset, |
352 |
limiti RS Limit_has_succ] 1)); |
|
760 | 353 |
qed "prod_in_VLimit"; |
0 | 354 |
|
355 |
(** Disjoint sums, aka Quine ordered pairs **) |
|
356 |
||
357 |
goalw Univ.thy [sum_def] |
|
187 | 358 |
"!!A. [| a: Vfrom(A,j); b: Vfrom(A,j); Transset(A); 1:j |] ==> \ |
359 |
\ a+b : Vfrom(A, succ(succ(succ(j))))"; |
|
0 | 360 |
by (dtac Transset_Vfrom 1); |
361 |
by (rtac subset_mem_Vfrom 1); |
|
362 |
by (rewtac Transset_def); |
|
363 |
by (fast_tac (ZF_cs addIs [zero_in_Vfrom, Pair_in_Vfrom, |
|
364 |
i_subset_Vfrom RS subsetD]) 1); |
|
760 | 365 |
qed "sum_in_Vfrom"; |
0 | 366 |
|
367 |
val [aprem,bprem,limiti,transset] = goal Univ.thy |
|
368 |
"[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) |] ==> \ |
|
369 |
\ a+b : Vfrom(A,i)"; |
|
516 | 370 |
by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1); |
187 | 371 |
by (REPEAT (ares_tac [exI, conjI, sum_in_Vfrom, transset, |
372 |
limiti RS Limit_has_succ] 1)); |
|
760 | 373 |
qed "sum_in_VLimit"; |
0 | 374 |
|
375 |
(** function space! **) |
|
376 |
||
377 |
goalw Univ.thy [Pi_def] |
|
187 | 378 |
"!!A. [| a: Vfrom(A,j); b: Vfrom(A,j); Transset(A) |] ==> \ |
379 |
\ a->b : Vfrom(A, succ(succ(succ(succ(j)))))"; |
|
0 | 380 |
by (dtac Transset_Vfrom 1); |
381 |
by (rtac subset_mem_Vfrom 1); |
|
382 |
by (rtac (Collect_subset RS subset_trans) 1); |
|
383 |
by (rtac (Vfrom RS ssubst) 1); |
|
384 |
by (rtac (subset_trans RS subset_trans) 1); |
|
385 |
by (rtac Un_upper2 3); |
|
386 |
by (rtac (succI1 RS UN_upper) 2); |
|
387 |
by (rtac Pow_mono 1); |
|
388 |
by (rewtac Transset_def); |
|
389 |
by (fast_tac (ZF_cs addIs [Pair_in_Vfrom]) 1); |
|
760 | 390 |
qed "fun_in_Vfrom"; |
0 | 391 |
|
392 |
val [aprem,bprem,limiti,transset] = goal Univ.thy |
|
393 |
"[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) |] ==> \ |
|
394 |
\ a->b : Vfrom(A,i)"; |
|
516 | 395 |
by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1); |
187 | 396 |
by (REPEAT (ares_tac [exI, conjI, fun_in_Vfrom, transset, |
397 |
limiti RS Limit_has_succ] 1)); |
|
760 | 398 |
qed "fun_in_VLimit"; |
0 | 399 |
|
400 |
||
401 |
(*** The set Vset(i) ***) |
|
402 |
||
403 |
goal Univ.thy "Vset(i) = (UN j:i. Pow(Vset(j)))"; |
|
404 |
by (rtac (Vfrom RS ssubst) 1); |
|
405 |
by (fast_tac eq_cs 1); |
|
760 | 406 |
qed "Vset"; |
0 | 407 |
|
408 |
val Vset_succ = Transset_0 RS Transset_Vfrom_succ; |
|
409 |
||
410 |
val Transset_Vset = Transset_0 RS Transset_Vfrom; |
|
411 |
||
412 |
(** Characterisation of the elements of Vset(i) **) |
|
413 |
||
27 | 414 |
val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. b : Vset(i) --> rank(b) < i"; |
0 | 415 |
by (rtac (ordi RS trans_induct) 1); |
416 |
by (rtac (Vset RS ssubst) 1); |
|
417 |
by (safe_tac ZF_cs); |
|
418 |
by (rtac (rank RS ssubst) 1); |
|
27 | 419 |
by (rtac UN_succ_least_lt 1); |
420 |
by (fast_tac ZF_cs 2); |
|
421 |
by (REPEAT (ares_tac [ltI] 1)); |
|
760 | 422 |
qed "Vset_rank_imp1"; |
0 | 423 |
|
27 | 424 |
(* [| Ord(i); x : Vset(i) |] ==> rank(x) < i *) |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
425 |
bind_thm ("VsetD", (Vset_rank_imp1 RS spec RS mp)); |
0 | 426 |
|
427 |
val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. rank(b) : i --> b : Vset(i)"; |
|
428 |
by (rtac (ordi RS trans_induct) 1); |
|
429 |
by (rtac allI 1); |
|
430 |
by (rtac (Vset RS ssubst) 1); |
|
27 | 431 |
by (fast_tac (ZF_cs addSIs [rank_lt RS ltD]) 1); |
760 | 432 |
qed "Vset_rank_imp2"; |
0 | 433 |
|
27 | 434 |
goal Univ.thy "!!x i. rank(x)<i ==> x : Vset(i)"; |
435 |
by (etac ltE 1); |
|
436 |
by (etac (Vset_rank_imp2 RS spec RS mp) 1); |
|
437 |
by (assume_tac 1); |
|
760 | 438 |
qed "VsetI"; |
0 | 439 |
|
27 | 440 |
goal Univ.thy "!!i. Ord(i) ==> b : Vset(i) <-> rank(b) < i"; |
0 | 441 |
by (rtac iffI 1); |
27 | 442 |
by (REPEAT (eresolve_tac [asm_rl, VsetD, VsetI] 1)); |
760 | 443 |
qed "Vset_Ord_rank_iff"; |
0 | 444 |
|
27 | 445 |
goal Univ.thy "b : Vset(a) <-> rank(b) < rank(a)"; |
0 | 446 |
by (rtac (Vfrom_rank_eq RS subst) 1); |
447 |
by (rtac (Ord_rank RS Vset_Ord_rank_iff) 1); |
|
760 | 448 |
qed "Vset_rank_iff"; |
0 | 449 |
|
450 |
goal Univ.thy "!!i. Ord(i) ==> rank(Vset(i)) = i"; |
|
451 |
by (rtac (rank RS ssubst) 1); |
|
452 |
by (rtac equalityI 1); |
|
453 |
by (safe_tac ZF_cs); |
|
828 | 454 |
by (EVERY' [rtac UN_I, |
0 | 455 |
etac (i_subset_Vfrom RS subsetD), |
456 |
etac (Ord_in_Ord RS rank_of_Ord RS ssubst), |
|
457 |
assume_tac, |
|
458 |
rtac succI1] 3); |
|
27 | 459 |
by (REPEAT (eresolve_tac [asm_rl, VsetD RS ltD, Ord_trans] 1)); |
760 | 460 |
qed "rank_Vset"; |
0 | 461 |
|
462 |
(** Lemmas for reasoning about sets in terms of their elements' ranks **) |
|
463 |
||
464 |
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
|
465 |
by (rtac subsetI 1); |
27 | 466 |
by (etac (rank_lt RS VsetI) 1); |
760 | 467 |
qed "arg_subset_Vset_rank"; |
0 | 468 |
|
469 |
val [iprem] = goal Univ.thy |
|
470 |
"[| !!i. Ord(i) ==> a Int Vset(i) <= b |] ==> a <= b"; |
|
27 | 471 |
by (rtac ([subset_refl, arg_subset_Vset_rank] MRS |
472 |
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
|
473 |
by (rtac (Ord_rank RS iprem) 1); |
760 | 474 |
qed "Int_Vset_subset"; |
0 | 475 |
|
476 |
(** Set up an environment for simplification **) |
|
477 |
||
478 |
val rank_rls = [rank_Inl, rank_Inr, rank_pair1, rank_pair2]; |
|
27 | 479 |
val rank_trans_rls = rank_rls @ (rank_rls RLN (2, [lt_trans])); |
0 | 480 |
|
481 |
val rank_ss = ZF_ss |
|
27 | 482 |
addsimps [case_Inl, case_Inr, VsetI] |
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
483 |
addsimps rank_trans_rls; |
0 | 484 |
|
485 |
(** Recursion over Vset levels! **) |
|
486 |
||
487 |
(*NOT SUITABLE FOR REWRITING: recursive!*) |
|
488 |
goalw Univ.thy [Vrec_def] "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))"; |
|
489 |
by (rtac (transrec RS ssubst) 1); |
|
27 | 490 |
by (simp_tac (ZF_ss addsimps [Ord_rank, Ord_succ, VsetD RS ltD RS beta, |
491 |
VsetI RS beta, le_refl]) 1); |
|
760 | 492 |
qed "Vrec"; |
0 | 493 |
|
494 |
(*This form avoids giant explosions in proofs. NOTE USE OF == *) |
|
495 |
val rew::prems = goal Univ.thy |
|
496 |
"[| !!x. h(x)==Vrec(x,H) |] ==> \ |
|
497 |
\ h(a) = H(a, lam x: Vset(rank(a)). h(x))"; |
|
498 |
by (rewtac rew); |
|
499 |
by (rtac Vrec 1); |
|
760 | 500 |
qed "def_Vrec"; |
0 | 501 |
|
502 |
||
503 |
(*** univ(A) ***) |
|
504 |
||
505 |
goalw Univ.thy [univ_def] "!!A B. A<=B ==> univ(A) <= univ(B)"; |
|
506 |
by (etac Vfrom_mono 1); |
|
507 |
by (rtac subset_refl 1); |
|
760 | 508 |
qed "univ_mono"; |
0 | 509 |
|
510 |
goalw Univ.thy [univ_def] "!!A. Transset(A) ==> Transset(univ(A))"; |
|
511 |
by (etac Transset_Vfrom 1); |
|
760 | 512 |
qed "Transset_univ"; |
0 | 513 |
|
514 |
(** univ(A) as a limit **) |
|
515 |
||
516 |
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
|
517 |
by (rtac (Limit_nat RS Limit_Vfrom_eq) 1); |
760 | 518 |
qed "univ_eq_UN"; |
0 | 519 |
|
520 |
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
|
521 |
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
|
522 |
by (etac (univ_eq_UN RS subst) 1); |
760 | 523 |
qed "subset_univ_eq_Int"; |
0 | 524 |
|
525 |
val [aprem, iprem] = goal Univ.thy |
|
526 |
"[| a <= univ(X); \ |
|
527 |
\ !!i. i:nat ==> a Int Vfrom(X,i) <= b \ |
|
528 |
\ |] ==> a <= b"; |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
529 |
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
|
530 |
by (rtac UN_least 1); |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
531 |
by (etac iprem 1); |
760 | 532 |
qed "univ_Int_Vfrom_subset"; |
0 | 533 |
|
534 |
val prems = goal Univ.thy |
|
535 |
"[| a <= univ(X); b <= univ(X); \ |
|
536 |
\ !!i. i:nat ==> a Int Vfrom(X,i) = b Int Vfrom(X,i) \ |
|
537 |
\ |] ==> a = b"; |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
538 |
by (rtac equalityI 1); |
0 | 539 |
by (ALLGOALS |
540 |
(resolve_tac (prems RL [univ_Int_Vfrom_subset]) THEN' |
|
541 |
eresolve_tac (prems RL [equalityD1,equalityD2] RL [subset_trans]) THEN' |
|
542 |
rtac Int_lower1)); |
|
760 | 543 |
qed "univ_Int_Vfrom_eq"; |
0 | 544 |
|
545 |
(** Closure properties **) |
|
546 |
||
547 |
goalw Univ.thy [univ_def] "0 : univ(A)"; |
|
548 |
by (rtac (nat_0I RS zero_in_Vfrom) 1); |
|
760 | 549 |
qed "zero_in_univ"; |
0 | 550 |
|
551 |
goalw Univ.thy [univ_def] "A <= univ(A)"; |
|
552 |
by (rtac A_subset_Vfrom 1); |
|
760 | 553 |
qed "A_subset_univ"; |
0 | 554 |
|
555 |
val A_into_univ = A_subset_univ RS subsetD; |
|
556 |
||
557 |
(** Closure under unordered and ordered pairs **) |
|
558 |
||
559 |
goalw Univ.thy [univ_def] "!!A a. a: univ(A) ==> {a} : univ(A)"; |
|
516 | 560 |
by (REPEAT (ares_tac [singleton_in_VLimit, Limit_nat] 1)); |
760 | 561 |
qed "singleton_in_univ"; |
0 | 562 |
|
563 |
goalw Univ.thy [univ_def] |
|
564 |
"!!A a. [| a: univ(A); b: univ(A) |] ==> {a,b} : univ(A)"; |
|
516 | 565 |
by (REPEAT (ares_tac [doubleton_in_VLimit, Limit_nat] 1)); |
760 | 566 |
qed "doubleton_in_univ"; |
0 | 567 |
|
568 |
goalw Univ.thy [univ_def] |
|
569 |
"!!A a. [| a: univ(A); b: univ(A) |] ==> <a,b> : univ(A)"; |
|
516 | 570 |
by (REPEAT (ares_tac [Pair_in_VLimit, Limit_nat] 1)); |
760 | 571 |
qed "Pair_in_univ"; |
0 | 572 |
|
484 | 573 |
goalw Univ.thy [univ_def] "univ(A)*univ(A) <= univ(A)"; |
516 | 574 |
by (rtac (Limit_nat RS product_VLimit) 1); |
760 | 575 |
qed "product_univ"; |
0 | 576 |
|
577 |
||
578 |
(** The natural numbers **) |
|
579 |
||
580 |
goalw Univ.thy [univ_def] "nat <= univ(A)"; |
|
581 |
by (rtac i_subset_Vfrom 1); |
|
760 | 582 |
qed "nat_subset_univ"; |
0 | 583 |
|
584 |
(* n:nat ==> n:univ(A) *) |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
585 |
bind_thm ("nat_into_univ", (nat_subset_univ RS subsetD)); |
0 | 586 |
|
587 |
(** instances for 1 and 2 **) |
|
588 |
||
484 | 589 |
goalw Univ.thy [univ_def] "1 : univ(A)"; |
516 | 590 |
by (rtac (Limit_nat RS one_in_VLimit) 1); |
760 | 591 |
qed "one_in_univ"; |
0 | 592 |
|
593 |
(*unused!*) |
|
828 | 594 |
goal Univ.thy "2 : univ(A)"; |
0 | 595 |
by (REPEAT (ares_tac [nat_into_univ, nat_0I, nat_succI] 1)); |
760 | 596 |
qed "two_in_univ"; |
0 | 597 |
|
598 |
goalw Univ.thy [bool_def] "bool <= univ(A)"; |
|
599 |
by (fast_tac (ZF_cs addSIs [zero_in_univ,one_in_univ]) 1); |
|
760 | 600 |
qed "bool_subset_univ"; |
0 | 601 |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
602 |
bind_thm ("bool_into_univ", (bool_subset_univ RS subsetD)); |
0 | 603 |
|
604 |
||
605 |
(** Closure under disjoint union **) |
|
606 |
||
484 | 607 |
goalw Univ.thy [univ_def] "!!A a. a: univ(A) ==> Inl(a) : univ(A)"; |
516 | 608 |
by (etac (Limit_nat RSN (2,Inl_in_VLimit)) 1); |
760 | 609 |
qed "Inl_in_univ"; |
0 | 610 |
|
484 | 611 |
goalw Univ.thy [univ_def] "!!A b. b: univ(A) ==> Inr(b) : univ(A)"; |
516 | 612 |
by (etac (Limit_nat RSN (2,Inr_in_VLimit)) 1); |
760 | 613 |
qed "Inr_in_univ"; |
0 | 614 |
|
484 | 615 |
goalw Univ.thy [univ_def] "univ(C)+univ(C) <= univ(C)"; |
516 | 616 |
by (rtac (Limit_nat RS sum_VLimit) 1); |
760 | 617 |
qed "sum_univ"; |
0 | 618 |
|
803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
619 |
bind_thm ("sum_subset_univ", [sum_mono, sum_univ] MRS subset_trans); |
484 | 620 |
|
621 |
||
0 | 622 |
(** Closure under binary union -- use Un_least **) |
623 |
(** Closure under Collect -- use (Collect_subset RS subset_trans) **) |
|
624 |
(** Closure under RepFun -- use RepFun_subset **) |
|
803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
625 |
|
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
626 |
|
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
627 |
(*** Finite Branching Closure Properties ***) |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
628 |
|
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
629 |
(** Closure under finite powerset **) |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
630 |
|
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
631 |
goal Univ.thy |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
632 |
"!!i. [| b: Fin(Vfrom(A,i)); Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j<i"; |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
633 |
by (eresolve_tac [Fin_induct] 1); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
634 |
by (fast_tac (ZF_cs addSDs [Limit_has_0]) 1); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
635 |
by (safe_tac ZF_cs); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
636 |
by (eresolve_tac [Limit_VfromE] 1); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
637 |
by (assume_tac 1); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
638 |
by (res_inst_tac [("x", "xa Un j")] exI 1); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
639 |
by (best_tac (ZF_cs addIs [subset_refl RS Vfrom_mono RS subsetD, |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
640 |
Un_least_lt]) 1); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
641 |
val Fin_Vfrom_lemma = result(); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
642 |
|
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
643 |
goal Univ.thy "!!i. Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)"; |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
644 |
by (rtac subsetI 1); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
645 |
by (dresolve_tac [Fin_Vfrom_lemma] 1); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
646 |
by (safe_tac ZF_cs); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
647 |
by (resolve_tac [Vfrom RS ssubst] 1); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
648 |
by (fast_tac (ZF_cs addSDs [ltD]) 1); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
649 |
val Fin_VLimit = result(); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
650 |
|
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
651 |
bind_thm ("Fin_subset_VLimit", [Fin_mono, Fin_VLimit] MRS subset_trans); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
652 |
|
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
653 |
goalw Univ.thy [univ_def] "Fin(univ(A)) <= univ(A)"; |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
654 |
by (rtac (Limit_nat RS Fin_VLimit) 1); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
655 |
val Fin_univ = result(); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
656 |
|
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
657 |
(** Closure under finite powers (functions from a fixed natural number) **) |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
658 |
|
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
659 |
goal Univ.thy |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
660 |
"!!i. [| n: nat; Limit(i) |] ==> n -> Vfrom(A,i) <= Vfrom(A,i)"; |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
661 |
by (eresolve_tac [nat_fun_subset_Fin RS subset_trans] 1); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
662 |
by (REPEAT (ares_tac [Fin_subset_VLimit, Sigma_subset_VLimit, |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
663 |
nat_subset_VLimit, subset_refl] 1)); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
664 |
val nat_fun_VLimit = result(); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
665 |
|
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
666 |
bind_thm ("nat_fun_subset_VLimit", [Pi_mono, nat_fun_VLimit] MRS subset_trans); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
667 |
|
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
668 |
goalw Univ.thy [univ_def] "!!i. n: nat ==> n -> univ(A) <= univ(A)"; |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
669 |
by (etac (Limit_nat RSN (2,nat_fun_VLimit)) 1); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
670 |
val nat_fun_univ = result(); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
671 |
|
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
672 |
|
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
673 |
(** Closure under finite function space **) |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
674 |
|
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
675 |
(*General but seldom-used version; normally the domain is fixed*) |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
676 |
goal Univ.thy |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
677 |
"!!i. Limit(i) ==> Vfrom(A,i) -||> Vfrom(A,i) <= Vfrom(A,i)"; |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
678 |
by (resolve_tac [FiniteFun.dom_subset RS subset_trans] 1); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
679 |
by (REPEAT (ares_tac [Fin_subset_VLimit, Sigma_subset_VLimit, subset_refl] 1)); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
680 |
val FiniteFun_VLimit1 = result(); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
681 |
|
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
682 |
goalw Univ.thy [univ_def] "univ(A) -||> univ(A) <= univ(A)"; |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
683 |
by (rtac (Limit_nat RS FiniteFun_VLimit1) 1); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
684 |
val FiniteFun_univ1 = result(); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
685 |
|
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
686 |
(*Version for a fixed domain*) |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
687 |
goal Univ.thy |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
688 |
"!!i. [| W <= Vfrom(A,i); Limit(i) |] ==> W -||> Vfrom(A,i) <= Vfrom(A,i)"; |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
689 |
by (eresolve_tac [subset_refl RSN (2, FiniteFun_mono) RS subset_trans] 1); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
690 |
by (eresolve_tac [FiniteFun_VLimit1] 1); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
691 |
val FiniteFun_VLimit = result(); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
692 |
|
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
693 |
goalw Univ.thy [univ_def] |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
694 |
"!!W. W <= univ(A) ==> W -||> univ(A) <= univ(A)"; |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
695 |
by (etac (Limit_nat RSN (2, FiniteFun_VLimit)) 1); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
696 |
val FiniteFun_univ = result(); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
697 |
|
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
698 |
goal Univ.thy |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
699 |
"!!W. [| f: W -||> univ(A); W <= univ(A) |] ==> f : univ(A)"; |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
700 |
by (eresolve_tac [FiniteFun_univ RS subsetD] 1); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
701 |
by (assume_tac 1); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
702 |
val FiniteFun_in_univ = result(); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
703 |
|
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
704 |
(*Remove <= from the rule above*) |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
705 |
val FiniteFun_in_univ' = subsetI RSN (2, FiniteFun_in_univ); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
706 |
|
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
707 |