author  lcp 
Tue, 26 Jul 1994 13:21:20 +0200  
changeset 484  70b789956bd3 
parent 435  ca5356bd315a 
child 488  52f7447d4f1b 
permissions  rwrr 
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); 
0  15 
val Vfrom = result(); 
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); 

31 
val Vfrom_mono_lemma = result(); 

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); 
0  44 
val Vfrom_rank_subset1 = result(); 
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); 

61 
val Vfrom_rank_subset2 = result(); 

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); 

67 
val Vfrom_rank_eq = result(); 

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); 

75 
val zero_in_Vfrom = result(); 

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); 

81 
val i_subset_Vfrom = result(); 

82 

83 
goal Univ.thy "A <= Vfrom(A,i)"; 

84 
by (rtac (Vfrom RS ssubst) 1); 

85 
by (rtac Un_upper1 1); 

86 
val A_subset_Vfrom = result(); 

87 

88 
goal Univ.thy "!!A a i. a <= Vfrom(A,i) ==> a: Vfrom(A,succ(i))"; 

89 
by (rtac (Vfrom RS ssubst) 1); 

90 
by (fast_tac ZF_cs 1); 

91 
val subset_mem_Vfrom = result(); 

92 

93 
(** Finite sets and ordered pairs **) 

94 

95 
goal Univ.thy "!!a. a: Vfrom(A,i) ==> {a} : Vfrom(A,succ(i))"; 

96 
by (rtac subset_mem_Vfrom 1); 

97 
by (safe_tac ZF_cs); 

98 
val singleton_in_Vfrom = result(); 

99 

100 
goal Univ.thy 

101 
"!!A. [ a: Vfrom(A,i); b: Vfrom(A,i) ] ==> {a,b} : Vfrom(A,succ(i))"; 

102 
by (rtac subset_mem_Vfrom 1); 

103 
by (safe_tac ZF_cs); 

104 
val doubleton_in_Vfrom = result(); 

105 

106 
goalw Univ.thy [Pair_def] 

107 
"!!A. [ a: Vfrom(A,i); b: Vfrom(A,i) ] ==> \ 

108 
\ <a,b> : Vfrom(A,succ(succ(i)))"; 

109 
by (REPEAT (ares_tac [doubleton_in_Vfrom] 1)); 

110 
val Pair_in_Vfrom = result(); 

111 

112 
val [prem] = goal Univ.thy 

113 
"a<=Vfrom(A,i) ==> succ(a) : Vfrom(A,succ(succ(i)))"; 

114 
by (REPEAT (resolve_tac [subset_mem_Vfrom, succ_subsetI] 1)); 

115 
by (rtac (Vfrom_mono RSN (2,subset_trans)) 2); 

116 
by (REPEAT (resolve_tac [prem, subset_refl, subset_succI] 1)); 

117 
val succ_in_Vfrom = result(); 

118 

119 
(*** 0, successor and limit equations fof Vfrom ***) 

120 

121 
goal Univ.thy "Vfrom(A,0) = A"; 

122 
by (rtac (Vfrom RS ssubst) 1); 

123 
by (fast_tac eq_cs 1); 

124 
val Vfrom_0 = result(); 

125 

126 
goal Univ.thy "!!i. Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))"; 

127 
by (rtac (Vfrom RS trans) 1); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

128 
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

129 
(2, equalityI RS subst_context)) 1); 
0  130 
by (rtac UN_least 1); 
131 
by (rtac (subset_refl RS Vfrom_mono RS Pow_mono) 1); 

27  132 
by (etac (ltI RS le_imp_subset) 1); 
133 
by (etac Ord_succ 1); 

0  134 
val Vfrom_succ_lemma = result(); 
135 

136 
goal Univ.thy "Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))"; 

137 
by (res_inst_tac [("x1", "succ(i)")] (Vfrom_rank_eq RS subst) 1); 

138 
by (res_inst_tac [("x1", "i")] (Vfrom_rank_eq RS subst) 1); 

139 
by (rtac (rank_succ RS ssubst) 1); 

140 
by (rtac (Ord_rank RS Vfrom_succ_lemma) 1); 

141 
val Vfrom_succ = result(); 

142 

143 
(*The premise distinguishes this from Vfrom(A,0); allowing X=0 forces 

144 
the conclusion to be Vfrom(A,Union(X)) = A Un (UN y:X. Vfrom(A,y)) *) 

145 
val [prem] = goal Univ.thy "y:X ==> Vfrom(A,Union(X)) = (UN y:X. Vfrom(A,y))"; 

146 
by (rtac (Vfrom RS ssubst) 1); 

147 
by (rtac equalityI 1); 

148 
(*first inclusion*) 

149 
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

150 
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

151 
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

152 
by (rtac UN_least 1); 
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

153 
by (etac UnionE 1); 
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

154 
by (rtac subset_trans 1); 
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

155 
by (etac UN_upper 2); 
0  156 
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

157 
by (etac ([UN_upper, Un_upper2] MRS subset_trans) 1); 
0  158 
(*opposite inclusion*) 
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

159 
by (rtac UN_least 1); 
0  160 
by (rtac (Vfrom RS ssubst) 1); 
161 
by (fast_tac ZF_cs 1); 

162 
val Vfrom_Union = result(); 

163 

164 
goal Univ.thy "!!i. Ord(i) ==> i=0  (EX j. i=succ(j))  Limit(i)"; 

27  165 
by (fast_tac (ZF_cs addSIs [non_succ_LimitI, Ord_0_lt]) 1); 
0  166 
val Ord_cases_lemma = result(); 
167 

168 
val major::prems = goal Univ.thy 

169 
"[ Ord(i); \ 

170 
\ i=0 ==> P; \ 

171 
\ !!j. i=succ(j) ==> P; \ 

172 
\ Limit(i) ==> P \ 

173 
\ ] ==> P"; 

174 
by (cut_facts_tac [major RS Ord_cases_lemma] 1); 

175 
by (REPEAT (eresolve_tac (prems@[disjE, exE]) 1)); 

176 
val Ord_cases = result(); 

177 

178 

179 
(*** Vfrom applied to Limit ordinals ***) 

180 

181 
(*NB. limit ordinals are nonempty; 

182 
Vfrom(A,0) = A = A Un (UN y:0. Vfrom(A,y)) *) 

183 
val [limiti] = goal Univ.thy 

184 
"Limit(i) ==> Vfrom(A,i) = (UN y:i. Vfrom(A,y))"; 

27  185 
by (rtac (limiti RS (Limit_has_0 RS ltD) RS Vfrom_Union RS subst) 1); 
0  186 
by (rtac (limiti RS Limit_Union_eq RS ssubst) 1); 
187 
by (rtac refl 1); 

188 
val Limit_Vfrom_eq = result(); 

189 

27  190 
goal Univ.thy "!!a. [ a: Vfrom(A,j); Limit(i); j<i ] ==> a : Vfrom(A,i)"; 
191 
by (rtac (Limit_Vfrom_eq RS equalityD2 RS subsetD) 1); 

192 
by (REPEAT (ares_tac [ltD RS UN_I] 1)); 

193 
val Limit_VfromI = result(); 

194 

195 
val prems = goal Univ.thy 

196 
"[ a: Vfrom(A,i); Limit(i); \ 

197 
\ !!x. [ x<i; a: Vfrom(A,x) ] ==> R \ 

198 
\ ] ==> R"; 

199 
by (rtac (Limit_Vfrom_eq RS equalityD1 RS subsetD RS UN_E) 1); 

200 
by (REPEAT (ares_tac (prems @ [ltI, Limit_is_Ord]) 1)); 

201 
val Limit_VfromE = result(); 

0  202 

484  203 
val zero_in_Vfrom_Limit = Limit_has_0 RS ltD RS zero_in_Vfrom; 
204 

0  205 
val [major,limiti] = goal Univ.thy 
206 
"[ a: Vfrom(A,i); Limit(i) ] ==> {a} : Vfrom(A,i)"; 

27  207 
by (rtac ([major,limiti] MRS Limit_VfromE) 1); 
208 
by (etac ([singleton_in_Vfrom, limiti] MRS Limit_VfromI) 1); 

0  209 
by (etac (limiti RS Limit_has_succ) 1); 
484  210 
val singleton_in_Vfrom_Limit = result(); 
0  211 

212 
val Vfrom_UnI1 = Un_upper1 RS (subset_refl RS Vfrom_mono RS subsetD) 

213 
and Vfrom_UnI2 = Un_upper2 RS (subset_refl RS Vfrom_mono RS subsetD); 

214 

215 
(*Hard work is finding a single j:i such that {a,b}<=Vfrom(A,j)*) 

216 
val [aprem,bprem,limiti] = goal Univ.thy 

217 
"[ a: Vfrom(A,i); b: Vfrom(A,i); Limit(i) ] ==> \ 

218 
\ {a,b} : Vfrom(A,i)"; 

27  219 
by (rtac ([aprem,limiti] MRS Limit_VfromE) 1); 
220 
by (rtac ([bprem,limiti] MRS Limit_VfromE) 1); 

221 
by (rtac ([doubleton_in_Vfrom, limiti] MRS Limit_VfromI) 1); 

222 
by (etac Vfrom_UnI1 1); 

223 
by (etac Vfrom_UnI2 1); 

224 
by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt] 1)); 

484  225 
val doubleton_in_Vfrom_Limit = result(); 
0  226 

227 
val [aprem,bprem,limiti] = goal Univ.thy 

228 
"[ a: Vfrom(A,i); b: Vfrom(A,i); Limit(i) ] ==> \ 

229 
\ <a,b> : Vfrom(A,i)"; 

230 
(*Infer that a, b occur at ordinals x,xa < i.*) 

27  231 
by (rtac ([aprem,limiti] MRS Limit_VfromE) 1); 
232 
by (rtac ([bprem,limiti] MRS Limit_VfromE) 1); 

233 
by (rtac ([Pair_in_Vfrom, limiti] MRS Limit_VfromI) 1); 

0  234 
(*Infer that succ(succ(x Un xa)) < i *) 
27  235 
by (etac Vfrom_UnI1 1); 
236 
by (etac Vfrom_UnI2 1); 

237 
by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt] 1)); 

484  238 
val Pair_in_Vfrom_Limit = result(); 
239 

240 
goal Univ.thy "!!i. Limit(i) ==> Vfrom(A,i)*Vfrom(A,i) <= Vfrom(A,i)"; 

241 
by (REPEAT (ares_tac [subsetI,Pair_in_Vfrom_Limit] 1 

242 
ORELSE eresolve_tac [SigmaE, ssubst] 1)); 

243 
val product_Vfrom_Limit = result(); 

244 

245 
val Sigma_subset_Vfrom_Limit = 

246 
[Sigma_mono, product_Vfrom_Limit] MRS subset_trans > standard; 

247 

248 
val nat_subset_Vfrom_Limit = 

249 
[nat_le_Limit RS le_imp_subset, i_subset_Vfrom] MRS subset_trans 

250 
> standard; 

251 

252 
val nat_into_Vfrom_Limit = standard (nat_subset_Vfrom_Limit RS subsetD); 

253 

254 
(** Closure under disjoint union **) 

255 

256 
val zero_in_Vfrom_Limit = Limit_has_0 RS ltD RS zero_in_Vfrom > standard; 

257 

258 
goal Univ.thy "!!i. Limit(i) ==> 1 : Vfrom(A,i)"; 

259 
by (REPEAT (ares_tac [nat_into_Vfrom_Limit, nat_0I, nat_succI] 1)); 

260 
val one_in_Vfrom_Limit = result(); 

261 

262 
goalw Univ.thy [Inl_def] 

263 
"!!A a. [ a: Vfrom(A,i); Limit(i) ] ==> Inl(a) : Vfrom(A,i)"; 

264 
by (REPEAT (ares_tac [zero_in_Vfrom_Limit, Pair_in_Vfrom_Limit] 1)); 

265 
val Inl_in_Vfrom_Limit = result(); 

266 

267 
goalw Univ.thy [Inr_def] 

268 
"!!A b. [ b: Vfrom(A,i); Limit(i) ] ==> Inr(b) : Vfrom(A,i)"; 

269 
by (REPEAT (ares_tac [one_in_Vfrom_Limit, Pair_in_Vfrom_Limit] 1)); 

270 
val Inr_in_Vfrom_Limit = result(); 

271 

272 
goal Univ.thy "!!i. Limit(i) ==> Vfrom(C,i)+Vfrom(C,i) <= Vfrom(C,i)"; 

273 
by (fast_tac (sum_cs addSIs [Inl_in_Vfrom_Limit, Inr_in_Vfrom_Limit]) 1); 

274 
val sum_Vfrom_Limit = result(); 

275 

276 
val sum_subset_Vfrom_Limit = 

277 
[sum_mono, sum_Vfrom_Limit] MRS subset_trans > standard; 

278 

279 

280 
(** Closure under finite powerset **) 

281 

282 
goal Univ.thy 

283 
"!!i. [ b: Fin(Vfrom(A,i)); Limit(i) ] ==> EX j. b <= Vfrom(A,j) & j<i"; 

284 
by (eresolve_tac [Fin_induct] 1); 

285 
by (fast_tac (ZF_cs addSDs [Limit_has_0]) 1); 

286 
by (safe_tac ZF_cs); 

287 
by (eresolve_tac [Limit_VfromE] 1); 

288 
by (assume_tac 1); 

289 
by (res_inst_tac [("x", "xa Un j")] exI 1); 

290 
by (best_tac (ZF_cs addIs [subset_refl RS Vfrom_mono RS subsetD, 

291 
Un_least_lt]) 1); 

292 
val Fin_Vfrom_lemma = result(); 

293 

294 
goal Univ.thy "!!i. Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)"; 

295 
by (rtac subsetI 1); 

296 
by (dresolve_tac [Fin_Vfrom_lemma] 1); 

297 
by (safe_tac ZF_cs); 

298 
by (resolve_tac [Vfrom RS ssubst] 1); 

299 
by (fast_tac (ZF_cs addSDs [ltD]) 1); 

300 
val Fin_Vfrom_Limit = result(); 

301 

302 
val Fin_subset_Vfrom_Limit = 

303 
[Fin_mono, Fin_Vfrom_Limit] MRS subset_trans > standard; 

304 

305 
goal Univ.thy "!!i. [ n: nat; Limit(i) ] ==> n > Vfrom(A,i) <= Vfrom(A,i)"; 

306 
by (eresolve_tac [nat_fun_subset_Fin RS subset_trans] 1); 

307 
by (REPEAT (ares_tac [Fin_subset_Vfrom_Limit, Sigma_subset_Vfrom_Limit, 

308 
nat_subset_Vfrom_Limit, subset_refl] 1)); 

309 
val nat_fun_Vfrom_Limit = result(); 

310 

311 
val nat_fun_subset_Vfrom_Limit = 

312 
[Pi_mono, nat_fun_Vfrom_Limit] MRS subset_trans > standard; 

313 

0  314 

315 

316 
(*** Properties assuming Transset(A) ***) 

317 

318 
goal Univ.thy "!!i A. Transset(A) ==> Transset(Vfrom(A,i))"; 

319 
by (eps_ind_tac "i" 1); 

320 
by (rtac (Vfrom RS ssubst) 1); 

321 
by (fast_tac (ZF_cs addSIs [Transset_Union_family, Transset_Un, 

322 
Transset_Pow]) 1); 

323 
val Transset_Vfrom = result(); 

324 

325 
goal Univ.thy "!!A i. Transset(A) ==> Vfrom(A, succ(i)) = Pow(Vfrom(A,i))"; 

326 
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

327 
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

328 
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

329 
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

330 
by (etac (Transset_Vfrom RS (Transset_iff_Pow RS iffD1)) 1); 
0  331 
val Transset_Vfrom_succ = result(); 
332 

435  333 
goalw Ordinal.thy [Pair_def,Transset_def] 
0  334 
"!!C. [ <a,b> <= C; Transset(C) ] ==> a: C & b: C"; 
335 
by (fast_tac ZF_cs 1); 

336 
val Transset_Pair_subset = result(); 

337 

338 
goal Univ.thy 

339 
"!!a b.[ <a,b> <= Vfrom(A,i); Transset(A); Limit(i) ] ==> \ 

340 
\ <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

341 
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

342 
by (etac Transset_Vfrom 1); 
484  343 
by (REPEAT (ares_tac [Pair_in_Vfrom_Limit] 1)); 
344 
val Transset_Pair_subset_Vfrom_Limit = result(); 

0  345 

346 

347 
(*** Closure under product/sum applied to elements  thus Vfrom(A,i) 

348 
is a model of simple type theory provided A is a transitive set 

349 
and i is a limit ordinal 

350 
***) 

351 

187  352 
(*General theorem for membership in Vfrom(A,i) when i is a limit ordinal*) 
353 
val [aprem,bprem,limiti,step] = goal Univ.thy 

354 
"[ a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); \ 

355 
\ !!x y j. [ j<i; 1:j; x: Vfrom(A,j); y: Vfrom(A,j) \ 

356 
\ ] ==> EX k. h(x,y): Vfrom(A,k) & k<i ] ==> \ 

357 
\ h(a,b) : Vfrom(A,i)"; 

358 
(*Infer that a, b occur at ordinals x,xa < i.*) 

359 
by (rtac ([aprem,limiti] MRS Limit_VfromE) 1); 

360 
by (rtac ([bprem,limiti] MRS Limit_VfromE) 1); 

361 
by (res_inst_tac [("j1", "x Un xa Un succ(1)")] (step RS exE) 1); 

362 
by (DO_GOAL [etac conjE, etac Limit_VfromI, rtac limiti, atac] 5); 

363 
by (etac (Vfrom_UnI2 RS Vfrom_UnI1) 4); 

364 
by (etac (Vfrom_UnI1 RS Vfrom_UnI1) 3); 

365 
by (rtac (succI1 RS UnI2) 2); 

366 
by (REPEAT (ares_tac [limiti, Limit_has_0, Limit_has_succ, Un_least_lt] 1)); 

484  367 
val in_Vfrom_Limit = result(); 
0  368 

369 
(** products **) 

370 

371 
goal Univ.thy 

187  372 
"!!A. [ a: Vfrom(A,j); b: Vfrom(A,j); Transset(A) ] ==> \ 
373 
\ a*b : Vfrom(A, succ(succ(succ(j))))"; 

0  374 
by (dtac Transset_Vfrom 1); 
375 
by (rtac subset_mem_Vfrom 1); 

376 
by (rewtac Transset_def); 

377 
by (fast_tac (ZF_cs addIs [Pair_in_Vfrom]) 1); 

378 
val prod_in_Vfrom = result(); 

379 

380 
val [aprem,bprem,limiti,transset] = goal Univ.thy 

381 
"[ a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) ] ==> \ 

382 
\ a*b : Vfrom(A,i)"; 

484  383 
by (rtac ([aprem,bprem,limiti] MRS in_Vfrom_Limit) 1); 
187  384 
by (REPEAT (ares_tac [exI, conjI, prod_in_Vfrom, transset, 
385 
limiti RS Limit_has_succ] 1)); 

484  386 
val prod_in_Vfrom_Limit = result(); 
0  387 

388 
(** Disjoint sums, aka Quine ordered pairs **) 

389 

390 
goalw Univ.thy [sum_def] 

187  391 
"!!A. [ a: Vfrom(A,j); b: Vfrom(A,j); Transset(A); 1:j ] ==> \ 
392 
\ a+b : Vfrom(A, succ(succ(succ(j))))"; 

0  393 
by (dtac Transset_Vfrom 1); 
394 
by (rtac subset_mem_Vfrom 1); 

395 
by (rewtac Transset_def); 

396 
by (fast_tac (ZF_cs addIs [zero_in_Vfrom, Pair_in_Vfrom, 

397 
i_subset_Vfrom RS subsetD]) 1); 

398 
val sum_in_Vfrom = result(); 

399 

400 
val [aprem,bprem,limiti,transset] = goal Univ.thy 

401 
"[ a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) ] ==> \ 

402 
\ a+b : Vfrom(A,i)"; 

484  403 
by (rtac ([aprem,bprem,limiti] MRS in_Vfrom_Limit) 1); 
187  404 
by (REPEAT (ares_tac [exI, conjI, sum_in_Vfrom, transset, 
405 
limiti RS Limit_has_succ] 1)); 

484  406 
val sum_in_Vfrom_Limit = result(); 
0  407 

408 
(** function space! **) 

409 

410 
goalw Univ.thy [Pi_def] 

187  411 
"!!A. [ a: Vfrom(A,j); b: Vfrom(A,j); Transset(A) ] ==> \ 
412 
\ a>b : Vfrom(A, succ(succ(succ(succ(j)))))"; 

0  413 
by (dtac Transset_Vfrom 1); 
414 
by (rtac subset_mem_Vfrom 1); 

415 
by (rtac (Collect_subset RS subset_trans) 1); 

416 
by (rtac (Vfrom RS ssubst) 1); 

417 
by (rtac (subset_trans RS subset_trans) 1); 

418 
by (rtac Un_upper2 3); 

419 
by (rtac (succI1 RS UN_upper) 2); 

420 
by (rtac Pow_mono 1); 

421 
by (rewtac Transset_def); 

422 
by (fast_tac (ZF_cs addIs [Pair_in_Vfrom]) 1); 

423 
val fun_in_Vfrom = result(); 

424 

425 
val [aprem,bprem,limiti,transset] = goal Univ.thy 

426 
"[ a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) ] ==> \ 

427 
\ a>b : Vfrom(A,i)"; 

484  428 
by (rtac ([aprem,bprem,limiti] MRS in_Vfrom_Limit) 1); 
187  429 
by (REPEAT (ares_tac [exI, conjI, fun_in_Vfrom, transset, 
430 
limiti RS Limit_has_succ] 1)); 

484  431 
val fun_in_Vfrom_Limit = result(); 
0  432 

433 

434 
(*** The set Vset(i) ***) 

435 

436 
goal Univ.thy "Vset(i) = (UN j:i. Pow(Vset(j)))"; 

437 
by (rtac (Vfrom RS ssubst) 1); 

438 
by (fast_tac eq_cs 1); 

439 
val Vset = result(); 

440 

441 
val Vset_succ = Transset_0 RS Transset_Vfrom_succ; 

442 

443 
val Transset_Vset = Transset_0 RS Transset_Vfrom; 

444 

445 
(** Characterisation of the elements of Vset(i) **) 

446 

27  447 
val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. b : Vset(i) > rank(b) < i"; 
0  448 
by (rtac (ordi RS trans_induct) 1); 
449 
by (rtac (Vset RS ssubst) 1); 

450 
by (safe_tac ZF_cs); 

451 
by (rtac (rank RS ssubst) 1); 

27  452 
by (rtac UN_succ_least_lt 1); 
453 
by (fast_tac ZF_cs 2); 

454 
by (REPEAT (ares_tac [ltI] 1)); 

0  455 
val Vset_rank_imp1 = result(); 
456 

27  457 
(* [ Ord(i); x : Vset(i) ] ==> rank(x) < i *) 
458 
val VsetD = standard (Vset_rank_imp1 RS spec RS mp); 

0  459 

460 
val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. rank(b) : i > b : Vset(i)"; 

461 
by (rtac (ordi RS trans_induct) 1); 

462 
by (rtac allI 1); 

463 
by (rtac (Vset RS ssubst) 1); 

27  464 
by (fast_tac (ZF_cs addSIs [rank_lt RS ltD]) 1); 
0  465 
val Vset_rank_imp2 = result(); 
466 

27  467 
goal Univ.thy "!!x i. rank(x)<i ==> x : Vset(i)"; 
468 
by (etac ltE 1); 

469 
by (etac (Vset_rank_imp2 RS spec RS mp) 1); 

470 
by (assume_tac 1); 

471 
val VsetI = result(); 

0  472 

27  473 
goal Univ.thy "!!i. Ord(i) ==> b : Vset(i) <> rank(b) < i"; 
0  474 
by (rtac iffI 1); 
27  475 
by (REPEAT (eresolve_tac [asm_rl, VsetD, VsetI] 1)); 
0  476 
val Vset_Ord_rank_iff = result(); 
477 

27  478 
goal Univ.thy "b : Vset(a) <> rank(b) < rank(a)"; 
0  479 
by (rtac (Vfrom_rank_eq RS subst) 1); 
480 
by (rtac (Ord_rank RS Vset_Ord_rank_iff) 1); 

481 
val Vset_rank_iff = result(); 

482 

483 
goal Univ.thy "!!i. Ord(i) ==> rank(Vset(i)) = i"; 

484 
by (rtac (rank RS ssubst) 1); 

485 
by (rtac equalityI 1); 

486 
by (safe_tac ZF_cs); 

487 
by (EVERY' [wtac UN_I, 

488 
etac (i_subset_Vfrom RS subsetD), 

489 
etac (Ord_in_Ord RS rank_of_Ord RS ssubst), 

490 
assume_tac, 

491 
rtac succI1] 3); 

27  492 
by (REPEAT (eresolve_tac [asm_rl, VsetD RS ltD, Ord_trans] 1)); 
0  493 
val rank_Vset = result(); 
494 

495 
(** Lemmas for reasoning about sets in terms of their elements' ranks **) 

496 

497 
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

498 
by (rtac subsetI 1); 
27  499 
by (etac (rank_lt RS VsetI) 1); 
0  500 
val arg_subset_Vset_rank = result(); 
501 

502 
val [iprem] = goal Univ.thy 

503 
"[ !!i. Ord(i) ==> a Int Vset(i) <= b ] ==> a <= b"; 

27  504 
by (rtac ([subset_refl, arg_subset_Vset_rank] MRS 
505 
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

506 
by (rtac (Ord_rank RS iprem) 1); 
0  507 
val Int_Vset_subset = result(); 
508 

509 
(** Set up an environment for simplification **) 

510 

511 
val rank_rls = [rank_Inl, rank_Inr, rank_pair1, rank_pair2]; 

27  512 
val rank_trans_rls = rank_rls @ (rank_rls RLN (2, [lt_trans])); 
0  513 

514 
val rank_ss = ZF_ss 

27  515 
addsimps [case_Inl, case_Inr, VsetI] 
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

516 
addsimps rank_trans_rls; 
0  517 

518 
(** Recursion over Vset levels! **) 

519 

520 
(*NOT SUITABLE FOR REWRITING: recursive!*) 

521 
goalw Univ.thy [Vrec_def] "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))"; 

522 
by (rtac (transrec RS ssubst) 1); 

27  523 
by (simp_tac (ZF_ss addsimps [Ord_rank, Ord_succ, VsetD RS ltD RS beta, 
524 
VsetI RS beta, le_refl]) 1); 

0  525 
val Vrec = result(); 
526 

527 
(*This form avoids giant explosions in proofs. NOTE USE OF == *) 

528 
val rew::prems = goal Univ.thy 

529 
"[ !!x. h(x)==Vrec(x,H) ] ==> \ 

530 
\ h(a) = H(a, lam x: Vset(rank(a)). h(x))"; 

531 
by (rewtac rew); 

532 
by (rtac Vrec 1); 

533 
val def_Vrec = result(); 

534 

535 

536 
(*** univ(A) ***) 

537 

538 
goalw Univ.thy [univ_def] "!!A B. A<=B ==> univ(A) <= univ(B)"; 

539 
by (etac Vfrom_mono 1); 

540 
by (rtac subset_refl 1); 

541 
val univ_mono = result(); 

542 

543 
goalw Univ.thy [univ_def] "!!A. Transset(A) ==> Transset(univ(A))"; 

544 
by (etac Transset_Vfrom 1); 

545 
val Transset_univ = result(); 

546 

547 
(** univ(A) as a limit **) 

548 

549 
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

550 
by (rtac (Limit_nat RS Limit_Vfrom_eq) 1); 
0  551 
val univ_eq_UN = result(); 
552 

553 
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

554 
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

555 
by (etac (univ_eq_UN RS subst) 1); 
0  556 
val subset_univ_eq_Int = result(); 
557 

558 
val [aprem, iprem] = goal Univ.thy 

559 
"[ a <= univ(X); \ 

560 
\ !!i. i:nat ==> a Int Vfrom(X,i) <= b \ 

561 
\ ] ==> a <= b"; 

15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

562 
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

563 
by (rtac UN_least 1); 
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

564 
by (etac iprem 1); 
0  565 
val univ_Int_Vfrom_subset = result(); 
566 

567 
val prems = goal Univ.thy 

568 
"[ a <= univ(X); b <= univ(X); \ 

569 
\ !!i. i:nat ==> a Int Vfrom(X,i) = b Int Vfrom(X,i) \ 

570 
\ ] ==> a = b"; 

15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

571 
by (rtac equalityI 1); 
0  572 
by (ALLGOALS 
573 
(resolve_tac (prems RL [univ_Int_Vfrom_subset]) THEN' 

574 
eresolve_tac (prems RL [equalityD1,equalityD2] RL [subset_trans]) THEN' 

575 
rtac Int_lower1)); 

576 
val univ_Int_Vfrom_eq = result(); 

577 

578 
(** Closure properties **) 

579 

580 
goalw Univ.thy [univ_def] "0 : univ(A)"; 

581 
by (rtac (nat_0I RS zero_in_Vfrom) 1); 

582 
val zero_in_univ = result(); 

583 

584 
goalw Univ.thy [univ_def] "A <= univ(A)"; 

585 
by (rtac A_subset_Vfrom 1); 

586 
val A_subset_univ = result(); 

587 

588 
val A_into_univ = A_subset_univ RS subsetD; 

589 

590 
(** Closure under unordered and ordered pairs **) 

591 

592 
goalw Univ.thy [univ_def] "!!A a. a: univ(A) ==> {a} : univ(A)"; 

484  593 
by (REPEAT (ares_tac [singleton_in_Vfrom_Limit, Limit_nat] 1)); 
0  594 
val singleton_in_univ = result(); 
595 

596 
goalw Univ.thy [univ_def] 

597 
"!!A a. [ a: univ(A); b: univ(A) ] ==> {a,b} : univ(A)"; 

484  598 
by (REPEAT (ares_tac [doubleton_in_Vfrom_Limit, Limit_nat] 1)); 
0  599 
val doubleton_in_univ = result(); 
600 

601 
goalw Univ.thy [univ_def] 

602 
"!!A a. [ a: univ(A); b: univ(A) ] ==> <a,b> : univ(A)"; 

484  603 
by (REPEAT (ares_tac [Pair_in_Vfrom_Limit, Limit_nat] 1)); 
0  604 
val Pair_in_univ = result(); 
605 

484  606 
goalw Univ.thy [univ_def] "univ(A)*univ(A) <= univ(A)"; 
607 
by (rtac (Limit_nat RS product_Vfrom_Limit) 1); 

0  608 
val product_univ = result(); 
609 

484  610 
val Sigma_subset_univ = 
611 
[Sigma_mono, product_univ] MRS subset_trans > standard; 

0  612 

613 
goalw Univ.thy [univ_def] 

614 
"!!a b.[ <a,b> <= univ(A); Transset(A) ] ==> <a,b> : univ(A)"; 

484  615 
by (etac Transset_Pair_subset_Vfrom_Limit 1); 
0  616 
by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1)); 
617 
val Transset_Pair_subset_univ = result(); 

618 

619 

620 
(** The natural numbers **) 

621 

622 
goalw Univ.thy [univ_def] "nat <= univ(A)"; 

623 
by (rtac i_subset_Vfrom 1); 

624 
val nat_subset_univ = result(); 

625 

626 
(* n:nat ==> n:univ(A) *) 

627 
val nat_into_univ = standard (nat_subset_univ RS subsetD); 

628 

629 
(** instances for 1 and 2 **) 

630 

484  631 
goalw Univ.thy [univ_def] "1 : univ(A)"; 
632 
by (rtac (Limit_nat RS one_in_Vfrom_Limit) 1); 

0  633 
val one_in_univ = result(); 
634 

635 
(*unused!*) 

27  636 
goal Univ.thy "succ(1) : univ(A)"; 
0  637 
by (REPEAT (ares_tac [nat_into_univ, nat_0I, nat_succI] 1)); 
638 
val two_in_univ = result(); 

639 

640 
goalw Univ.thy [bool_def] "bool <= univ(A)"; 

641 
by (fast_tac (ZF_cs addSIs [zero_in_univ,one_in_univ]) 1); 

642 
val bool_subset_univ = result(); 

643 

644 
val bool_into_univ = standard (bool_subset_univ RS subsetD); 

645 

646 

647 
(** Closure under disjoint union **) 

648 

484  649 
goalw Univ.thy [univ_def] "!!A a. a: univ(A) ==> Inl(a) : univ(A)"; 
650 
by (etac (Limit_nat RSN (2,Inl_in_Vfrom_Limit)) 1); 

0  651 
val Inl_in_univ = result(); 
652 

484  653 
goalw Univ.thy [univ_def] "!!A b. b: univ(A) ==> Inr(b) : univ(A)"; 
654 
by (etac (Limit_nat RSN (2,Inr_in_Vfrom_Limit)) 1); 

0  655 
val Inr_in_univ = result(); 
656 

484  657 
goalw Univ.thy [univ_def] "univ(C)+univ(C) <= univ(C)"; 
658 
by (rtac (Limit_nat RS sum_Vfrom_Limit) 1); 

0  659 
val sum_univ = result(); 
660 

484  661 
val sum_subset_univ = [sum_mono, sum_univ] MRS subset_trans > standard; 
662 

663 

664 
(** Closure under finite powerset **) 

665 

666 
goalw Univ.thy [univ_def] "Fin(univ(A)) <= univ(A)"; 

667 
by (rtac (Limit_nat RS Fin_Vfrom_Limit) 1); 

668 
val Fin_univ = result(); 

0  669 

484  670 
val Fin_subset_univ = [Fin_mono, Fin_univ] MRS subset_trans > standard; 
671 

672 
goalw Univ.thy [univ_def] "!!i. n: nat ==> n > univ(A) <= univ(A)"; 

673 
by (etac (Limit_nat RSN (2,nat_fun_Vfrom_Limit)) 1); 

674 
val nat_fun_univ = result(); 

675 

676 
val nat_fun_subset_univ = [Pi_mono, nat_fun_univ] MRS subset_trans > standard; 

677 

678 
goal Univ.thy "!!f. [ f: n > B; B <= univ(A); n : nat ] ==> f : univ(A)"; 

679 
by (REPEAT (ares_tac [nat_fun_subset_univ RS subsetD] 1)); 

680 
val nat_fun_into_univ = result(); 

0  681 

682 
(** Closure under binary union  use Un_least **) 

683 
(** Closure under Collect  use (Collect_subset RS subset_trans) **) 

684 
(** Closure under RepFun  use RepFun_subset **) 