56 by (rtac (subset_refl RS Vfrom_mono RS subset_trans RS Pow_mono) 1); |
56 by (rtac (subset_refl RS Vfrom_mono RS subset_trans RS Pow_mono) 1); |
57 by (etac (ltI RS le_imp_subset) 1); |
57 by (etac (ltI RS le_imp_subset) 1); |
58 by (rtac (Ord_rank RS Ord_succ) 1); |
58 by (rtac (Ord_rank RS Ord_succ) 1); |
59 by (etac bspec 1); |
59 by (etac bspec 1); |
60 by (assume_tac 1); |
60 by (assume_tac 1); |
61 val Vfrom_rank_subset2 = result(); |
61 qed "Vfrom_rank_subset2"; |
62 |
62 |
63 goal Univ.thy "Vfrom(A,rank(x)) = Vfrom(A,x)"; |
63 goal Univ.thy "Vfrom(A,rank(x)) = Vfrom(A,x)"; |
64 by (rtac equalityI 1); |
64 by (rtac equalityI 1); |
65 by (rtac Vfrom_rank_subset2 1); |
65 by (rtac Vfrom_rank_subset2 1); |
66 by (rtac Vfrom_rank_subset1 1); |
66 by (rtac Vfrom_rank_subset1 1); |
67 val Vfrom_rank_eq = result(); |
67 qed "Vfrom_rank_eq"; |
68 |
68 |
69 |
69 |
70 (*** Basic closure properties ***) |
70 (*** Basic closure properties ***) |
71 |
71 |
72 goal Univ.thy "!!x y. y:x ==> 0 : Vfrom(A,x)"; |
72 goal Univ.thy "!!x y. y:x ==> 0 : Vfrom(A,x)"; |
73 by (rtac (Vfrom RS ssubst) 1); |
73 by (rtac (Vfrom RS ssubst) 1); |
74 by (fast_tac ZF_cs 1); |
74 by (fast_tac ZF_cs 1); |
75 val zero_in_Vfrom = result(); |
75 qed "zero_in_Vfrom"; |
76 |
76 |
77 goal Univ.thy "i <= Vfrom(A,i)"; |
77 goal Univ.thy "i <= Vfrom(A,i)"; |
78 by (eps_ind_tac "i" 1); |
78 by (eps_ind_tac "i" 1); |
79 by (rtac (Vfrom RS ssubst) 1); |
79 by (rtac (Vfrom RS ssubst) 1); |
80 by (fast_tac ZF_cs 1); |
80 by (fast_tac ZF_cs 1); |
81 val i_subset_Vfrom = result(); |
81 qed "i_subset_Vfrom"; |
82 |
82 |
83 goal Univ.thy "A <= Vfrom(A,i)"; |
83 goal Univ.thy "A <= Vfrom(A,i)"; |
84 by (rtac (Vfrom RS ssubst) 1); |
84 by (rtac (Vfrom RS ssubst) 1); |
85 by (rtac Un_upper1 1); |
85 by (rtac Un_upper1 1); |
86 val A_subset_Vfrom = result(); |
86 qed "A_subset_Vfrom"; |
87 |
87 |
88 val A_into_Vfrom = A_subset_Vfrom RS subsetD |> standard; |
88 val A_into_Vfrom = A_subset_Vfrom RS subsetD |> standard; |
89 |
89 |
90 goal Univ.thy "!!A a i. a <= Vfrom(A,i) ==> a: Vfrom(A,succ(i))"; |
90 goal Univ.thy "!!A a i. a <= Vfrom(A,i) ==> a: Vfrom(A,succ(i))"; |
91 by (rtac (Vfrom RS ssubst) 1); |
91 by (rtac (Vfrom RS ssubst) 1); |
92 by (fast_tac ZF_cs 1); |
92 by (fast_tac ZF_cs 1); |
93 val subset_mem_Vfrom = result(); |
93 qed "subset_mem_Vfrom"; |
94 |
94 |
95 (** Finite sets and ordered pairs **) |
95 (** Finite sets and ordered pairs **) |
96 |
96 |
97 goal Univ.thy "!!a. a: Vfrom(A,i) ==> {a} : Vfrom(A,succ(i))"; |
97 goal Univ.thy "!!a. a: Vfrom(A,i) ==> {a} : Vfrom(A,succ(i))"; |
98 by (rtac subset_mem_Vfrom 1); |
98 by (rtac subset_mem_Vfrom 1); |
99 by (safe_tac ZF_cs); |
99 by (safe_tac ZF_cs); |
100 val singleton_in_Vfrom = result(); |
100 qed "singleton_in_Vfrom"; |
101 |
101 |
102 goal Univ.thy |
102 goal Univ.thy |
103 "!!A. [| a: Vfrom(A,i); b: Vfrom(A,i) |] ==> {a,b} : Vfrom(A,succ(i))"; |
103 "!!A. [| a: Vfrom(A,i); b: Vfrom(A,i) |] ==> {a,b} : Vfrom(A,succ(i))"; |
104 by (rtac subset_mem_Vfrom 1); |
104 by (rtac subset_mem_Vfrom 1); |
105 by (safe_tac ZF_cs); |
105 by (safe_tac ZF_cs); |
106 val doubleton_in_Vfrom = result(); |
106 qed "doubleton_in_Vfrom"; |
107 |
107 |
108 goalw Univ.thy [Pair_def] |
108 goalw Univ.thy [Pair_def] |
109 "!!A. [| a: Vfrom(A,i); b: Vfrom(A,i) |] ==> \ |
109 "!!A. [| a: Vfrom(A,i); b: Vfrom(A,i) |] ==> \ |
110 \ <a,b> : Vfrom(A,succ(succ(i)))"; |
110 \ <a,b> : Vfrom(A,succ(succ(i)))"; |
111 by (REPEAT (ares_tac [doubleton_in_Vfrom] 1)); |
111 by (REPEAT (ares_tac [doubleton_in_Vfrom] 1)); |
112 val Pair_in_Vfrom = result(); |
112 qed "Pair_in_Vfrom"; |
113 |
113 |
114 val [prem] = goal Univ.thy |
114 val [prem] = goal Univ.thy |
115 "a<=Vfrom(A,i) ==> succ(a) : Vfrom(A,succ(succ(i)))"; |
115 "a<=Vfrom(A,i) ==> succ(a) : Vfrom(A,succ(succ(i)))"; |
116 by (REPEAT (resolve_tac [subset_mem_Vfrom, succ_subsetI] 1)); |
116 by (REPEAT (resolve_tac [subset_mem_Vfrom, succ_subsetI] 1)); |
117 by (rtac (Vfrom_mono RSN (2,subset_trans)) 2); |
117 by (rtac (Vfrom_mono RSN (2,subset_trans)) 2); |
118 by (REPEAT (resolve_tac [prem, subset_refl, subset_succI] 1)); |
118 by (REPEAT (resolve_tac [prem, subset_refl, subset_succI] 1)); |
119 val succ_in_Vfrom = result(); |
119 qed "succ_in_Vfrom"; |
120 |
120 |
121 (*** 0, successor and limit equations fof Vfrom ***) |
121 (*** 0, successor and limit equations fof Vfrom ***) |
122 |
122 |
123 goal Univ.thy "Vfrom(A,0) = A"; |
123 goal Univ.thy "Vfrom(A,0) = A"; |
124 by (rtac (Vfrom RS ssubst) 1); |
124 by (rtac (Vfrom RS ssubst) 1); |
125 by (fast_tac eq_cs 1); |
125 by (fast_tac eq_cs 1); |
126 val Vfrom_0 = result(); |
126 qed "Vfrom_0"; |
127 |
127 |
128 goal Univ.thy "!!i. Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))"; |
128 goal Univ.thy "!!i. Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))"; |
129 by (rtac (Vfrom RS trans) 1); |
129 by (rtac (Vfrom RS trans) 1); |
130 by (rtac (succI1 RS RepFunI RS Union_upper RSN |
130 by (rtac (succI1 RS RepFunI RS Union_upper RSN |
131 (2, equalityI RS subst_context)) 1); |
131 (2, equalityI RS subst_context)) 1); |
132 by (rtac UN_least 1); |
132 by (rtac UN_least 1); |
133 by (rtac (subset_refl RS Vfrom_mono RS Pow_mono) 1); |
133 by (rtac (subset_refl RS Vfrom_mono RS Pow_mono) 1); |
134 by (etac (ltI RS le_imp_subset) 1); |
134 by (etac (ltI RS le_imp_subset) 1); |
135 by (etac Ord_succ 1); |
135 by (etac Ord_succ 1); |
136 val Vfrom_succ_lemma = result(); |
136 qed "Vfrom_succ_lemma"; |
137 |
137 |
138 goal Univ.thy "Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))"; |
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); |
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); |
140 by (res_inst_tac [("x1", "i")] (Vfrom_rank_eq RS subst) 1); |
141 by (rtac (rank_succ RS ssubst) 1); |
141 by (rtac (rank_succ RS ssubst) 1); |
142 by (rtac (Ord_rank RS Vfrom_succ_lemma) 1); |
142 by (rtac (Ord_rank RS Vfrom_succ_lemma) 1); |
143 val Vfrom_succ = result(); |
143 qed "Vfrom_succ"; |
144 |
144 |
145 (*The premise distinguishes this from Vfrom(A,0); allowing X=0 forces |
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)) *) |
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))"; |
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); |
148 by (rtac (Vfrom RS ssubst) 1); |
185 val [limiti] = goal Univ.thy |
185 val [limiti] = goal Univ.thy |
186 "Limit(i) ==> Vfrom(A,i) = (UN y:i. Vfrom(A,y))"; |
186 "Limit(i) ==> Vfrom(A,i) = (UN y:i. Vfrom(A,y))"; |
187 by (rtac (limiti RS (Limit_has_0 RS ltD) RS Vfrom_Union RS subst) 1); |
187 by (rtac (limiti RS (Limit_has_0 RS ltD) RS Vfrom_Union RS subst) 1); |
188 by (rtac (limiti RS Limit_Union_eq RS ssubst) 1); |
188 by (rtac (limiti RS Limit_Union_eq RS ssubst) 1); |
189 by (rtac refl 1); |
189 by (rtac refl 1); |
190 val Limit_Vfrom_eq = result(); |
190 qed "Limit_Vfrom_eq"; |
191 |
191 |
192 goal Univ.thy "!!a. [| a: Vfrom(A,j); Limit(i); j<i |] ==> a : Vfrom(A,i)"; |
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); |
193 by (rtac (Limit_Vfrom_eq RS equalityD2 RS subsetD) 1); |
194 by (REPEAT (ares_tac [ltD RS UN_I] 1)); |
194 by (REPEAT (ares_tac [ltD RS UN_I] 1)); |
195 val Limit_VfromI = result(); |
195 qed "Limit_VfromI"; |
196 |
196 |
197 val prems = goal Univ.thy |
197 val prems = goal Univ.thy |
198 "[| a: Vfrom(A,i); Limit(i); \ |
198 "[| a: Vfrom(A,i); Limit(i); \ |
199 \ !!x. [| x<i; a: Vfrom(A,x) |] ==> R \ |
199 \ !!x. [| x<i; a: Vfrom(A,x) |] ==> R \ |
200 \ |] ==> R"; |
200 \ |] ==> R"; |
201 by (rtac (Limit_Vfrom_eq RS equalityD1 RS subsetD RS UN_E) 1); |
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)); |
202 by (REPEAT (ares_tac (prems @ [ltI, Limit_is_Ord]) 1)); |
203 val Limit_VfromE = result(); |
203 qed "Limit_VfromE"; |
204 |
204 |
205 val zero_in_VLimit = Limit_has_0 RS ltD RS zero_in_Vfrom; |
205 val zero_in_VLimit = Limit_has_0 RS ltD RS zero_in_Vfrom; |
206 |
206 |
207 val [major,limiti] = goal Univ.thy |
207 val [major,limiti] = goal Univ.thy |
208 "[| a: Vfrom(A,i); Limit(i) |] ==> {a} : Vfrom(A,i)"; |
208 "[| a: Vfrom(A,i); Limit(i) |] ==> {a} : Vfrom(A,i)"; |
209 by (rtac ([major,limiti] MRS Limit_VfromE) 1); |
209 by (rtac ([major,limiti] MRS Limit_VfromE) 1); |
210 by (etac ([singleton_in_Vfrom, limiti] MRS Limit_VfromI) 1); |
210 by (etac ([singleton_in_Vfrom, limiti] MRS Limit_VfromI) 1); |
211 by (etac (limiti RS Limit_has_succ) 1); |
211 by (etac (limiti RS Limit_has_succ) 1); |
212 val singleton_in_VLimit = result(); |
212 qed "singleton_in_VLimit"; |
213 |
213 |
214 val Vfrom_UnI1 = Un_upper1 RS (subset_refl RS Vfrom_mono RS subsetD) |
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); |
215 and Vfrom_UnI2 = Un_upper2 RS (subset_refl RS Vfrom_mono RS subsetD); |
216 |
216 |
217 (*Hard work is finding a single j:i such that {a,b}<=Vfrom(A,j)*) |
217 (*Hard work is finding a single j:i such that {a,b}<=Vfrom(A,j)*) |
235 by (rtac ([Pair_in_Vfrom, limiti] MRS Limit_VfromI) 1); |
235 by (rtac ([Pair_in_Vfrom, limiti] MRS Limit_VfromI) 1); |
236 (*Infer that succ(succ(x Un xa)) < i *) |
236 (*Infer that succ(succ(x Un xa)) < i *) |
237 by (etac Vfrom_UnI1 1); |
237 by (etac Vfrom_UnI1 1); |
238 by (etac Vfrom_UnI2 1); |
238 by (etac Vfrom_UnI2 1); |
239 by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt] 1)); |
239 by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt] 1)); |
240 val Pair_in_VLimit = result(); |
240 qed "Pair_in_VLimit"; |
241 |
241 |
242 goal Univ.thy "!!i. Limit(i) ==> Vfrom(A,i)*Vfrom(A,i) <= Vfrom(A,i)"; |
242 goal Univ.thy "!!i. Limit(i) ==> Vfrom(A,i)*Vfrom(A,i) <= Vfrom(A,i)"; |
243 by (REPEAT (ares_tac [subsetI,Pair_in_VLimit] 1 |
243 by (REPEAT (ares_tac [subsetI,Pair_in_VLimit] 1 |
244 ORELSE eresolve_tac [SigmaE, ssubst] 1)); |
244 ORELSE eresolve_tac [SigmaE, ssubst] 1)); |
245 val product_VLimit = result(); |
245 qed "product_VLimit"; |
246 |
246 |
247 val Sigma_subset_VLimit = |
247 val Sigma_subset_VLimit = |
248 [Sigma_mono, product_VLimit] MRS subset_trans |> standard; |
248 [Sigma_mono, product_VLimit] MRS subset_trans |> standard; |
249 |
249 |
250 val nat_subset_VLimit = |
250 val nat_subset_VLimit = |
251 [nat_le_Limit RS le_imp_subset, i_subset_Vfrom] MRS subset_trans |
251 [nat_le_Limit RS le_imp_subset, i_subset_Vfrom] MRS subset_trans |
252 |> standard; |
252 |> standard; |
253 |
253 |
254 goal Univ.thy "!!i. [| n: nat; Limit(i) |] ==> n : Vfrom(A,i)"; |
254 goal Univ.thy "!!i. [| n: nat; Limit(i) |] ==> n : Vfrom(A,i)"; |
255 by (REPEAT (ares_tac [nat_subset_VLimit RS subsetD] 1)); |
255 by (REPEAT (ares_tac [nat_subset_VLimit RS subsetD] 1)); |
256 val nat_into_VLimit = result(); |
256 qed "nat_into_VLimit"; |
257 |
257 |
258 (** Closure under disjoint union **) |
258 (** Closure under disjoint union **) |
259 |
259 |
260 val zero_in_VLimit = Limit_has_0 RS ltD RS zero_in_Vfrom |> standard; |
260 val zero_in_VLimit = Limit_has_0 RS ltD RS zero_in_Vfrom |> standard; |
261 |
261 |
262 goal Univ.thy "!!i. Limit(i) ==> 1 : Vfrom(A,i)"; |
262 goal Univ.thy "!!i. Limit(i) ==> 1 : Vfrom(A,i)"; |
263 by (REPEAT (ares_tac [nat_into_VLimit, nat_0I, nat_succI] 1)); |
263 by (REPEAT (ares_tac [nat_into_VLimit, nat_0I, nat_succI] 1)); |
264 val one_in_VLimit = result(); |
264 qed "one_in_VLimit"; |
265 |
265 |
266 goalw Univ.thy [Inl_def] |
266 goalw Univ.thy [Inl_def] |
267 "!!A a. [| a: Vfrom(A,i); Limit(i) |] ==> Inl(a) : Vfrom(A,i)"; |
267 "!!A a. [| a: Vfrom(A,i); Limit(i) |] ==> Inl(a) : Vfrom(A,i)"; |
268 by (REPEAT (ares_tac [zero_in_VLimit, Pair_in_VLimit] 1)); |
268 by (REPEAT (ares_tac [zero_in_VLimit, Pair_in_VLimit] 1)); |
269 val Inl_in_VLimit = result(); |
269 qed "Inl_in_VLimit"; |
270 |
270 |
271 goalw Univ.thy [Inr_def] |
271 goalw Univ.thy [Inr_def] |
272 "!!A b. [| b: Vfrom(A,i); Limit(i) |] ==> Inr(b) : Vfrom(A,i)"; |
272 "!!A b. [| b: Vfrom(A,i); Limit(i) |] ==> Inr(b) : Vfrom(A,i)"; |
273 by (REPEAT (ares_tac [one_in_VLimit, Pair_in_VLimit] 1)); |
273 by (REPEAT (ares_tac [one_in_VLimit, Pair_in_VLimit] 1)); |
274 val Inr_in_VLimit = result(); |
274 qed "Inr_in_VLimit"; |
275 |
275 |
276 goal Univ.thy "!!i. Limit(i) ==> Vfrom(C,i)+Vfrom(C,i) <= Vfrom(C,i)"; |
276 goal Univ.thy "!!i. Limit(i) ==> Vfrom(C,i)+Vfrom(C,i) <= Vfrom(C,i)"; |
277 by (fast_tac (sum_cs addSIs [Inl_in_VLimit, Inr_in_VLimit]) 1); |
277 by (fast_tac (sum_cs addSIs [Inl_in_VLimit, Inr_in_VLimit]) 1); |
278 val sum_VLimit = result(); |
278 qed "sum_VLimit"; |
279 |
279 |
280 val sum_subset_VLimit = |
280 val sum_subset_VLimit = |
281 [sum_mono, sum_VLimit] MRS subset_trans |> standard; |
281 [sum_mono, sum_VLimit] MRS subset_trans |> standard; |
282 |
282 |
283 |
283 |
287 goal Univ.thy "!!i A. Transset(A) ==> Transset(Vfrom(A,i))"; |
287 goal Univ.thy "!!i A. Transset(A) ==> Transset(Vfrom(A,i))"; |
288 by (eps_ind_tac "i" 1); |
288 by (eps_ind_tac "i" 1); |
289 by (rtac (Vfrom RS ssubst) 1); |
289 by (rtac (Vfrom RS ssubst) 1); |
290 by (fast_tac (ZF_cs addSIs [Transset_Union_family, Transset_Un, |
290 by (fast_tac (ZF_cs addSIs [Transset_Union_family, Transset_Un, |
291 Transset_Pow]) 1); |
291 Transset_Pow]) 1); |
292 val Transset_Vfrom = result(); |
292 qed "Transset_Vfrom"; |
293 |
293 |
294 goal Univ.thy "!!A i. Transset(A) ==> Vfrom(A, succ(i)) = Pow(Vfrom(A,i))"; |
294 goal Univ.thy "!!A i. Transset(A) ==> Vfrom(A, succ(i)) = Pow(Vfrom(A,i))"; |
295 by (rtac (Vfrom_succ RS trans) 1); |
295 by (rtac (Vfrom_succ RS trans) 1); |
296 by (rtac (Un_upper2 RSN (2,equalityI)) 1); |
296 by (rtac (Un_upper2 RSN (2,equalityI)) 1); |
297 by (rtac (subset_refl RSN (2,Un_least)) 1); |
297 by (rtac (subset_refl RSN (2,Un_least)) 1); |
298 by (rtac (A_subset_Vfrom RS subset_trans) 1); |
298 by (rtac (A_subset_Vfrom RS subset_trans) 1); |
299 by (etac (Transset_Vfrom RS (Transset_iff_Pow RS iffD1)) 1); |
299 by (etac (Transset_Vfrom RS (Transset_iff_Pow RS iffD1)) 1); |
300 val Transset_Vfrom_succ = result(); |
300 qed "Transset_Vfrom_succ"; |
301 |
301 |
302 goalw Ordinal.thy [Pair_def,Transset_def] |
302 goalw Ordinal.thy [Pair_def,Transset_def] |
303 "!!C. [| <a,b> <= C; Transset(C) |] ==> a: C & b: C"; |
303 "!!C. [| <a,b> <= C; Transset(C) |] ==> a: C & b: C"; |
304 by (fast_tac ZF_cs 1); |
304 by (fast_tac ZF_cs 1); |
305 val Transset_Pair_subset = result(); |
305 qed "Transset_Pair_subset"; |
306 |
306 |
307 goal Univ.thy |
307 goal Univ.thy |
308 "!!a b.[| <a,b> <= Vfrom(A,i); Transset(A); Limit(i) |] ==> \ |
308 "!!a b.[| <a,b> <= Vfrom(A,i); Transset(A); Limit(i) |] ==> \ |
309 \ <a,b> : Vfrom(A,i)"; |
309 \ <a,b> : Vfrom(A,i)"; |
310 by (etac (Transset_Pair_subset RS conjE) 1); |
310 by (etac (Transset_Pair_subset RS conjE) 1); |
311 by (etac Transset_Vfrom 1); |
311 by (etac Transset_Vfrom 1); |
312 by (REPEAT (ares_tac [Pair_in_VLimit] 1)); |
312 by (REPEAT (ares_tac [Pair_in_VLimit] 1)); |
313 val Transset_Pair_subset_VLimit = result(); |
313 qed "Transset_Pair_subset_VLimit"; |
314 |
314 |
315 |
315 |
316 (*** Closure under product/sum applied to elements -- thus Vfrom(A,i) |
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 |
317 is a model of simple type theory provided A is a transitive set |
318 and i is a limit ordinal |
318 and i is a limit ordinal |
331 by (DO_GOAL [etac conjE, etac Limit_VfromI, rtac limiti, atac] 5); |
331 by (DO_GOAL [etac conjE, etac Limit_VfromI, rtac limiti, atac] 5); |
332 by (etac (Vfrom_UnI2 RS Vfrom_UnI1) 4); |
332 by (etac (Vfrom_UnI2 RS Vfrom_UnI1) 4); |
333 by (etac (Vfrom_UnI1 RS Vfrom_UnI1) 3); |
333 by (etac (Vfrom_UnI1 RS Vfrom_UnI1) 3); |
334 by (rtac (succI1 RS UnI2) 2); |
334 by (rtac (succI1 RS UnI2) 2); |
335 by (REPEAT (ares_tac [limiti, Limit_has_0, Limit_has_succ, Un_least_lt] 1)); |
335 by (REPEAT (ares_tac [limiti, Limit_has_0, Limit_has_succ, Un_least_lt] 1)); |
336 val in_VLimit = result(); |
336 qed "in_VLimit"; |
337 |
337 |
338 (** products **) |
338 (** products **) |
339 |
339 |
340 goal Univ.thy |
340 goal Univ.thy |
341 "!!A. [| a: Vfrom(A,j); b: Vfrom(A,j); Transset(A) |] ==> \ |
341 "!!A. [| a: Vfrom(A,j); b: Vfrom(A,j); Transset(A) |] ==> \ |
342 \ a*b : Vfrom(A, succ(succ(succ(j))))"; |
342 \ a*b : Vfrom(A, succ(succ(succ(j))))"; |
343 by (dtac Transset_Vfrom 1); |
343 by (dtac Transset_Vfrom 1); |
344 by (rtac subset_mem_Vfrom 1); |
344 by (rtac subset_mem_Vfrom 1); |
345 by (rewtac Transset_def); |
345 by (rewtac Transset_def); |
346 by (fast_tac (ZF_cs addIs [Pair_in_Vfrom]) 1); |
346 by (fast_tac (ZF_cs addIs [Pair_in_Vfrom]) 1); |
347 val prod_in_Vfrom = result(); |
347 qed "prod_in_Vfrom"; |
348 |
348 |
349 val [aprem,bprem,limiti,transset] = goal Univ.thy |
349 val [aprem,bprem,limiti,transset] = goal Univ.thy |
350 "[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) |] ==> \ |
350 "[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) |] ==> \ |
351 \ a*b : Vfrom(A,i)"; |
351 \ a*b : Vfrom(A,i)"; |
352 by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1); |
352 by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1); |
353 by (REPEAT (ares_tac [exI, conjI, prod_in_Vfrom, transset, |
353 by (REPEAT (ares_tac [exI, conjI, prod_in_Vfrom, transset, |
354 limiti RS Limit_has_succ] 1)); |
354 limiti RS Limit_has_succ] 1)); |
355 val prod_in_VLimit = result(); |
355 qed "prod_in_VLimit"; |
356 |
356 |
357 (** Disjoint sums, aka Quine ordered pairs **) |
357 (** Disjoint sums, aka Quine ordered pairs **) |
358 |
358 |
359 goalw Univ.thy [sum_def] |
359 goalw Univ.thy [sum_def] |
360 "!!A. [| a: Vfrom(A,j); b: Vfrom(A,j); Transset(A); 1:j |] ==> \ |
360 "!!A. [| a: Vfrom(A,j); b: Vfrom(A,j); Transset(A); 1:j |] ==> \ |
362 by (dtac Transset_Vfrom 1); |
362 by (dtac Transset_Vfrom 1); |
363 by (rtac subset_mem_Vfrom 1); |
363 by (rtac subset_mem_Vfrom 1); |
364 by (rewtac Transset_def); |
364 by (rewtac Transset_def); |
365 by (fast_tac (ZF_cs addIs [zero_in_Vfrom, Pair_in_Vfrom, |
365 by (fast_tac (ZF_cs addIs [zero_in_Vfrom, Pair_in_Vfrom, |
366 i_subset_Vfrom RS subsetD]) 1); |
366 i_subset_Vfrom RS subsetD]) 1); |
367 val sum_in_Vfrom = result(); |
367 qed "sum_in_Vfrom"; |
368 |
368 |
369 val [aprem,bprem,limiti,transset] = goal Univ.thy |
369 val [aprem,bprem,limiti,transset] = goal Univ.thy |
370 "[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) |] ==> \ |
370 "[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) |] ==> \ |
371 \ a+b : Vfrom(A,i)"; |
371 \ a+b : Vfrom(A,i)"; |
372 by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1); |
372 by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1); |
373 by (REPEAT (ares_tac [exI, conjI, sum_in_Vfrom, transset, |
373 by (REPEAT (ares_tac [exI, conjI, sum_in_Vfrom, transset, |
374 limiti RS Limit_has_succ] 1)); |
374 limiti RS Limit_has_succ] 1)); |
375 val sum_in_VLimit = result(); |
375 qed "sum_in_VLimit"; |
376 |
376 |
377 (** function space! **) |
377 (** function space! **) |
378 |
378 |
379 goalw Univ.thy [Pi_def] |
379 goalw Univ.thy [Pi_def] |
380 "!!A. [| a: Vfrom(A,j); b: Vfrom(A,j); Transset(A) |] ==> \ |
380 "!!A. [| a: Vfrom(A,j); b: Vfrom(A,j); Transset(A) |] ==> \ |
387 by (rtac Un_upper2 3); |
387 by (rtac Un_upper2 3); |
388 by (rtac (succI1 RS UN_upper) 2); |
388 by (rtac (succI1 RS UN_upper) 2); |
389 by (rtac Pow_mono 1); |
389 by (rtac Pow_mono 1); |
390 by (rewtac Transset_def); |
390 by (rewtac Transset_def); |
391 by (fast_tac (ZF_cs addIs [Pair_in_Vfrom]) 1); |
391 by (fast_tac (ZF_cs addIs [Pair_in_Vfrom]) 1); |
392 val fun_in_Vfrom = result(); |
392 qed "fun_in_Vfrom"; |
393 |
393 |
394 val [aprem,bprem,limiti,transset] = goal Univ.thy |
394 val [aprem,bprem,limiti,transset] = goal Univ.thy |
395 "[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) |] ==> \ |
395 "[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) |] ==> \ |
396 \ a->b : Vfrom(A,i)"; |
396 \ a->b : Vfrom(A,i)"; |
397 by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1); |
397 by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1); |
398 by (REPEAT (ares_tac [exI, conjI, fun_in_Vfrom, transset, |
398 by (REPEAT (ares_tac [exI, conjI, fun_in_Vfrom, transset, |
399 limiti RS Limit_has_succ] 1)); |
399 limiti RS Limit_has_succ] 1)); |
400 val fun_in_VLimit = result(); |
400 qed "fun_in_VLimit"; |
401 |
401 |
402 |
402 |
403 (*** The set Vset(i) ***) |
403 (*** The set Vset(i) ***) |
404 |
404 |
405 goal Univ.thy "Vset(i) = (UN j:i. Pow(Vset(j)))"; |
405 goal Univ.thy "Vset(i) = (UN j:i. Pow(Vset(j)))"; |
406 by (rtac (Vfrom RS ssubst) 1); |
406 by (rtac (Vfrom RS ssubst) 1); |
407 by (fast_tac eq_cs 1); |
407 by (fast_tac eq_cs 1); |
408 val Vset = result(); |
408 qed "Vset"; |
409 |
409 |
410 val Vset_succ = Transset_0 RS Transset_Vfrom_succ; |
410 val Vset_succ = Transset_0 RS Transset_Vfrom_succ; |
411 |
411 |
412 val Transset_Vset = Transset_0 RS Transset_Vfrom; |
412 val Transset_Vset = Transset_0 RS Transset_Vfrom; |
413 |
413 |
419 by (safe_tac ZF_cs); |
419 by (safe_tac ZF_cs); |
420 by (rtac (rank RS ssubst) 1); |
420 by (rtac (rank RS ssubst) 1); |
421 by (rtac UN_succ_least_lt 1); |
421 by (rtac UN_succ_least_lt 1); |
422 by (fast_tac ZF_cs 2); |
422 by (fast_tac ZF_cs 2); |
423 by (REPEAT (ares_tac [ltI] 1)); |
423 by (REPEAT (ares_tac [ltI] 1)); |
424 val Vset_rank_imp1 = result(); |
424 qed "Vset_rank_imp1"; |
425 |
425 |
426 (* [| Ord(i); x : Vset(i) |] ==> rank(x) < i *) |
426 (* [| Ord(i); x : Vset(i) |] ==> rank(x) < i *) |
427 val VsetD = standard (Vset_rank_imp1 RS spec RS mp); |
427 val VsetD = standard (Vset_rank_imp1 RS spec RS mp); |
428 |
428 |
429 val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. rank(b) : i --> b : Vset(i)"; |
429 val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. rank(b) : i --> b : Vset(i)"; |
430 by (rtac (ordi RS trans_induct) 1); |
430 by (rtac (ordi RS trans_induct) 1); |
431 by (rtac allI 1); |
431 by (rtac allI 1); |
432 by (rtac (Vset RS ssubst) 1); |
432 by (rtac (Vset RS ssubst) 1); |
433 by (fast_tac (ZF_cs addSIs [rank_lt RS ltD]) 1); |
433 by (fast_tac (ZF_cs addSIs [rank_lt RS ltD]) 1); |
434 val Vset_rank_imp2 = result(); |
434 qed "Vset_rank_imp2"; |
435 |
435 |
436 goal Univ.thy "!!x i. rank(x)<i ==> x : Vset(i)"; |
436 goal Univ.thy "!!x i. rank(x)<i ==> x : Vset(i)"; |
437 by (etac ltE 1); |
437 by (etac ltE 1); |
438 by (etac (Vset_rank_imp2 RS spec RS mp) 1); |
438 by (etac (Vset_rank_imp2 RS spec RS mp) 1); |
439 by (assume_tac 1); |
439 by (assume_tac 1); |
440 val VsetI = result(); |
440 qed "VsetI"; |
441 |
441 |
442 goal Univ.thy "!!i. Ord(i) ==> b : Vset(i) <-> rank(b) < i"; |
442 goal Univ.thy "!!i. Ord(i) ==> b : Vset(i) <-> rank(b) < i"; |
443 by (rtac iffI 1); |
443 by (rtac iffI 1); |
444 by (REPEAT (eresolve_tac [asm_rl, VsetD, VsetI] 1)); |
444 by (REPEAT (eresolve_tac [asm_rl, VsetD, VsetI] 1)); |
445 val Vset_Ord_rank_iff = result(); |
445 qed "Vset_Ord_rank_iff"; |
446 |
446 |
447 goal Univ.thy "b : Vset(a) <-> rank(b) < rank(a)"; |
447 goal Univ.thy "b : Vset(a) <-> rank(b) < rank(a)"; |
448 by (rtac (Vfrom_rank_eq RS subst) 1); |
448 by (rtac (Vfrom_rank_eq RS subst) 1); |
449 by (rtac (Ord_rank RS Vset_Ord_rank_iff) 1); |
449 by (rtac (Ord_rank RS Vset_Ord_rank_iff) 1); |
450 val Vset_rank_iff = result(); |
450 qed "Vset_rank_iff"; |
451 |
451 |
452 goal Univ.thy "!!i. Ord(i) ==> rank(Vset(i)) = i"; |
452 goal Univ.thy "!!i. Ord(i) ==> rank(Vset(i)) = i"; |
453 by (rtac (rank RS ssubst) 1); |
453 by (rtac (rank RS ssubst) 1); |
454 by (rtac equalityI 1); |
454 by (rtac equalityI 1); |
455 by (safe_tac ZF_cs); |
455 by (safe_tac ZF_cs); |
457 etac (i_subset_Vfrom RS subsetD), |
457 etac (i_subset_Vfrom RS subsetD), |
458 etac (Ord_in_Ord RS rank_of_Ord RS ssubst), |
458 etac (Ord_in_Ord RS rank_of_Ord RS ssubst), |
459 assume_tac, |
459 assume_tac, |
460 rtac succI1] 3); |
460 rtac succI1] 3); |
461 by (REPEAT (eresolve_tac [asm_rl, VsetD RS ltD, Ord_trans] 1)); |
461 by (REPEAT (eresolve_tac [asm_rl, VsetD RS ltD, Ord_trans] 1)); |
462 val rank_Vset = result(); |
462 qed "rank_Vset"; |
463 |
463 |
464 (** Lemmas for reasoning about sets in terms of their elements' ranks **) |
464 (** Lemmas for reasoning about sets in terms of their elements' ranks **) |
465 |
465 |
466 goal Univ.thy "a <= Vset(rank(a))"; |
466 goal Univ.thy "a <= Vset(rank(a))"; |
467 by (rtac subsetI 1); |
467 by (rtac subsetI 1); |
468 by (etac (rank_lt RS VsetI) 1); |
468 by (etac (rank_lt RS VsetI) 1); |
469 val arg_subset_Vset_rank = result(); |
469 qed "arg_subset_Vset_rank"; |
470 |
470 |
471 val [iprem] = goal Univ.thy |
471 val [iprem] = goal Univ.thy |
472 "[| !!i. Ord(i) ==> a Int Vset(i) <= b |] ==> a <= b"; |
472 "[| !!i. Ord(i) ==> a Int Vset(i) <= b |] ==> a <= b"; |
473 by (rtac ([subset_refl, arg_subset_Vset_rank] MRS |
473 by (rtac ([subset_refl, arg_subset_Vset_rank] MRS |
474 Int_greatest RS subset_trans) 1); |
474 Int_greatest RS subset_trans) 1); |
475 by (rtac (Ord_rank RS iprem) 1); |
475 by (rtac (Ord_rank RS iprem) 1); |
476 val Int_Vset_subset = result(); |
476 qed "Int_Vset_subset"; |
477 |
477 |
478 (** Set up an environment for simplification **) |
478 (** Set up an environment for simplification **) |
479 |
479 |
480 val rank_rls = [rank_Inl, rank_Inr, rank_pair1, rank_pair2]; |
480 val rank_rls = [rank_Inl, rank_Inr, rank_pair1, rank_pair2]; |
481 val rank_trans_rls = rank_rls @ (rank_rls RLN (2, [lt_trans])); |
481 val rank_trans_rls = rank_rls @ (rank_rls RLN (2, [lt_trans])); |
489 (*NOT SUITABLE FOR REWRITING: recursive!*) |
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))"; |
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); |
491 by (rtac (transrec RS ssubst) 1); |
492 by (simp_tac (ZF_ss addsimps [Ord_rank, Ord_succ, VsetD RS ltD RS beta, |
492 by (simp_tac (ZF_ss addsimps [Ord_rank, Ord_succ, VsetD RS ltD RS beta, |
493 VsetI RS beta, le_refl]) 1); |
493 VsetI RS beta, le_refl]) 1); |
494 val Vrec = result(); |
494 qed "Vrec"; |
495 |
495 |
496 (*This form avoids giant explosions in proofs. NOTE USE OF == *) |
496 (*This form avoids giant explosions in proofs. NOTE USE OF == *) |
497 val rew::prems = goal Univ.thy |
497 val rew::prems = goal Univ.thy |
498 "[| !!x. h(x)==Vrec(x,H) |] ==> \ |
498 "[| !!x. h(x)==Vrec(x,H) |] ==> \ |
499 \ h(a) = H(a, lam x: Vset(rank(a)). h(x))"; |
499 \ h(a) = H(a, lam x: Vset(rank(a)). h(x))"; |
500 by (rewtac rew); |
500 by (rewtac rew); |
501 by (rtac Vrec 1); |
501 by (rtac Vrec 1); |
502 val def_Vrec = result(); |
502 qed "def_Vrec"; |
503 |
503 |
504 |
504 |
505 (*** univ(A) ***) |
505 (*** univ(A) ***) |
506 |
506 |
507 goalw Univ.thy [univ_def] "!!A B. A<=B ==> univ(A) <= univ(B)"; |
507 goalw Univ.thy [univ_def] "!!A B. A<=B ==> univ(A) <= univ(B)"; |
508 by (etac Vfrom_mono 1); |
508 by (etac Vfrom_mono 1); |
509 by (rtac subset_refl 1); |
509 by (rtac subset_refl 1); |
510 val univ_mono = result(); |
510 qed "univ_mono"; |
511 |
511 |
512 goalw Univ.thy [univ_def] "!!A. Transset(A) ==> Transset(univ(A))"; |
512 goalw Univ.thy [univ_def] "!!A. Transset(A) ==> Transset(univ(A))"; |
513 by (etac Transset_Vfrom 1); |
513 by (etac Transset_Vfrom 1); |
514 val Transset_univ = result(); |
514 qed "Transset_univ"; |
515 |
515 |
516 (** univ(A) as a limit **) |
516 (** univ(A) as a limit **) |
517 |
517 |
518 goalw Univ.thy [univ_def] "univ(A) = (UN i:nat. Vfrom(A,i))"; |
518 goalw Univ.thy [univ_def] "univ(A) = (UN i:nat. Vfrom(A,i))"; |
519 by (rtac (Limit_nat RS Limit_Vfrom_eq) 1); |
519 by (rtac (Limit_nat RS Limit_Vfrom_eq) 1); |
520 val univ_eq_UN = result(); |
520 qed "univ_eq_UN"; |
521 |
521 |
522 goal Univ.thy "!!c. c <= univ(A) ==> c = (UN i:nat. c Int Vfrom(A,i))"; |
522 goal Univ.thy "!!c. c <= univ(A) ==> c = (UN i:nat. c Int Vfrom(A,i))"; |
523 by (rtac (subset_UN_iff_eq RS iffD1) 1); |
523 by (rtac (subset_UN_iff_eq RS iffD1) 1); |
524 by (etac (univ_eq_UN RS subst) 1); |
524 by (etac (univ_eq_UN RS subst) 1); |
525 val subset_univ_eq_Int = result(); |
525 qed "subset_univ_eq_Int"; |
526 |
526 |
527 val [aprem, iprem] = goal Univ.thy |
527 val [aprem, iprem] = goal Univ.thy |
528 "[| a <= univ(X); \ |
528 "[| a <= univ(X); \ |
529 \ !!i. i:nat ==> a Int Vfrom(X,i) <= b \ |
529 \ !!i. i:nat ==> a Int Vfrom(X,i) <= b \ |
530 \ |] ==> a <= b"; |
530 \ |] ==> a <= b"; |
531 by (rtac (aprem RS subset_univ_eq_Int RS ssubst) 1); |
531 by (rtac (aprem RS subset_univ_eq_Int RS ssubst) 1); |
532 by (rtac UN_least 1); |
532 by (rtac UN_least 1); |
533 by (etac iprem 1); |
533 by (etac iprem 1); |
534 val univ_Int_Vfrom_subset = result(); |
534 qed "univ_Int_Vfrom_subset"; |
535 |
535 |
536 val prems = goal Univ.thy |
536 val prems = goal Univ.thy |
537 "[| a <= univ(X); b <= univ(X); \ |
537 "[| a <= univ(X); b <= univ(X); \ |
538 \ !!i. i:nat ==> a Int Vfrom(X,i) = b Int Vfrom(X,i) \ |
538 \ !!i. i:nat ==> a Int Vfrom(X,i) = b Int Vfrom(X,i) \ |
539 \ |] ==> a = b"; |
539 \ |] ==> a = b"; |
540 by (rtac equalityI 1); |
540 by (rtac equalityI 1); |
541 by (ALLGOALS |
541 by (ALLGOALS |
542 (resolve_tac (prems RL [univ_Int_Vfrom_subset]) THEN' |
542 (resolve_tac (prems RL [univ_Int_Vfrom_subset]) THEN' |
543 eresolve_tac (prems RL [equalityD1,equalityD2] RL [subset_trans]) THEN' |
543 eresolve_tac (prems RL [equalityD1,equalityD2] RL [subset_trans]) THEN' |
544 rtac Int_lower1)); |
544 rtac Int_lower1)); |
545 val univ_Int_Vfrom_eq = result(); |
545 qed "univ_Int_Vfrom_eq"; |
546 |
546 |
547 (** Closure properties **) |
547 (** Closure properties **) |
548 |
548 |
549 goalw Univ.thy [univ_def] "0 : univ(A)"; |
549 goalw Univ.thy [univ_def] "0 : univ(A)"; |
550 by (rtac (nat_0I RS zero_in_Vfrom) 1); |
550 by (rtac (nat_0I RS zero_in_Vfrom) 1); |
551 val zero_in_univ = result(); |
551 qed "zero_in_univ"; |
552 |
552 |
553 goalw Univ.thy [univ_def] "A <= univ(A)"; |
553 goalw Univ.thy [univ_def] "A <= univ(A)"; |
554 by (rtac A_subset_Vfrom 1); |
554 by (rtac A_subset_Vfrom 1); |
555 val A_subset_univ = result(); |
555 qed "A_subset_univ"; |
556 |
556 |
557 val A_into_univ = A_subset_univ RS subsetD; |
557 val A_into_univ = A_subset_univ RS subsetD; |
558 |
558 |
559 (** Closure under unordered and ordered pairs **) |
559 (** Closure under unordered and ordered pairs **) |
560 |
560 |
561 goalw Univ.thy [univ_def] "!!A a. a: univ(A) ==> {a} : univ(A)"; |
561 goalw Univ.thy [univ_def] "!!A a. a: univ(A) ==> {a} : univ(A)"; |
562 by (REPEAT (ares_tac [singleton_in_VLimit, Limit_nat] 1)); |
562 by (REPEAT (ares_tac [singleton_in_VLimit, Limit_nat] 1)); |
563 val singleton_in_univ = result(); |
563 qed "singleton_in_univ"; |
564 |
564 |
565 goalw Univ.thy [univ_def] |
565 goalw Univ.thy [univ_def] |
566 "!!A a. [| a: univ(A); b: univ(A) |] ==> {a,b} : univ(A)"; |
566 "!!A a. [| a: univ(A); b: univ(A) |] ==> {a,b} : univ(A)"; |
567 by (REPEAT (ares_tac [doubleton_in_VLimit, Limit_nat] 1)); |
567 by (REPEAT (ares_tac [doubleton_in_VLimit, Limit_nat] 1)); |
568 val doubleton_in_univ = result(); |
568 qed "doubleton_in_univ"; |
569 |
569 |
570 goalw Univ.thy [univ_def] |
570 goalw Univ.thy [univ_def] |
571 "!!A a. [| a: univ(A); b: univ(A) |] ==> <a,b> : univ(A)"; |
571 "!!A a. [| a: univ(A); b: univ(A) |] ==> <a,b> : univ(A)"; |
572 by (REPEAT (ares_tac [Pair_in_VLimit, Limit_nat] 1)); |
572 by (REPEAT (ares_tac [Pair_in_VLimit, Limit_nat] 1)); |
573 val Pair_in_univ = result(); |
573 qed "Pair_in_univ"; |
574 |
574 |
575 goalw Univ.thy [univ_def] "univ(A)*univ(A) <= univ(A)"; |
575 goalw Univ.thy [univ_def] "univ(A)*univ(A) <= univ(A)"; |
576 by (rtac (Limit_nat RS product_VLimit) 1); |
576 by (rtac (Limit_nat RS product_VLimit) 1); |
577 val product_univ = result(); |
577 qed "product_univ"; |
578 |
578 |
579 |
579 |
580 (** The natural numbers **) |
580 (** The natural numbers **) |
581 |
581 |
582 goalw Univ.thy [univ_def] "nat <= univ(A)"; |
582 goalw Univ.thy [univ_def] "nat <= univ(A)"; |
583 by (rtac i_subset_Vfrom 1); |
583 by (rtac i_subset_Vfrom 1); |
584 val nat_subset_univ = result(); |
584 qed "nat_subset_univ"; |
585 |
585 |
586 (* n:nat ==> n:univ(A) *) |
586 (* n:nat ==> n:univ(A) *) |
587 val nat_into_univ = standard (nat_subset_univ RS subsetD); |
587 val nat_into_univ = standard (nat_subset_univ RS subsetD); |
588 |
588 |
589 (** instances for 1 and 2 **) |
589 (** instances for 1 and 2 **) |
590 |
590 |
591 goalw Univ.thy [univ_def] "1 : univ(A)"; |
591 goalw Univ.thy [univ_def] "1 : univ(A)"; |
592 by (rtac (Limit_nat RS one_in_VLimit) 1); |
592 by (rtac (Limit_nat RS one_in_VLimit) 1); |
593 val one_in_univ = result(); |
593 qed "one_in_univ"; |
594 |
594 |
595 (*unused!*) |
595 (*unused!*) |
596 goal Univ.thy "succ(1) : univ(A)"; |
596 goal Univ.thy "succ(1) : univ(A)"; |
597 by (REPEAT (ares_tac [nat_into_univ, nat_0I, nat_succI] 1)); |
597 by (REPEAT (ares_tac [nat_into_univ, nat_0I, nat_succI] 1)); |
598 val two_in_univ = result(); |
598 qed "two_in_univ"; |
599 |
599 |
600 goalw Univ.thy [bool_def] "bool <= univ(A)"; |
600 goalw Univ.thy [bool_def] "bool <= univ(A)"; |
601 by (fast_tac (ZF_cs addSIs [zero_in_univ,one_in_univ]) 1); |
601 by (fast_tac (ZF_cs addSIs [zero_in_univ,one_in_univ]) 1); |
602 val bool_subset_univ = result(); |
602 qed "bool_subset_univ"; |
603 |
603 |
604 val bool_into_univ = standard (bool_subset_univ RS subsetD); |
604 val bool_into_univ = standard (bool_subset_univ RS subsetD); |
605 |
605 |
606 |
606 |
607 (** Closure under disjoint union **) |
607 (** Closure under disjoint union **) |
608 |
608 |
609 goalw Univ.thy [univ_def] "!!A a. a: univ(A) ==> Inl(a) : univ(A)"; |
609 goalw Univ.thy [univ_def] "!!A a. a: univ(A) ==> Inl(a) : univ(A)"; |
610 by (etac (Limit_nat RSN (2,Inl_in_VLimit)) 1); |
610 by (etac (Limit_nat RSN (2,Inl_in_VLimit)) 1); |
611 val Inl_in_univ = result(); |
611 qed "Inl_in_univ"; |
612 |
612 |
613 goalw Univ.thy [univ_def] "!!A b. b: univ(A) ==> Inr(b) : univ(A)"; |
613 goalw Univ.thy [univ_def] "!!A b. b: univ(A) ==> Inr(b) : univ(A)"; |
614 by (etac (Limit_nat RSN (2,Inr_in_VLimit)) 1); |
614 by (etac (Limit_nat RSN (2,Inr_in_VLimit)) 1); |
615 val Inr_in_univ = result(); |
615 qed "Inr_in_univ"; |
616 |
616 |
617 goalw Univ.thy [univ_def] "univ(C)+univ(C) <= univ(C)"; |
617 goalw Univ.thy [univ_def] "univ(C)+univ(C) <= univ(C)"; |
618 by (rtac (Limit_nat RS sum_VLimit) 1); |
618 by (rtac (Limit_nat RS sum_VLimit) 1); |
619 val sum_univ = result(); |
619 qed "sum_univ"; |
620 |
620 |
621 val sum_subset_univ = [sum_mono, sum_univ] MRS subset_trans |> standard; |
621 val sum_subset_univ = [sum_mono, sum_univ] MRS subset_trans |> standard; |
622 |
622 |
623 |
623 |
624 (** Closure under binary union -- use Un_least **) |
624 (** Closure under binary union -- use Un_least **) |