author  lcp 
Thu, 30 Sep 1993 10:10:21 +0100  
changeset 14  1c0926788772 
parent 6  8ce8c4d13d4d 
child 27  0e152fe9571e 
permissions  rwrr 
0  1 
(* Title: ZF/univ 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1992 University of Cambridge 

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

43 
by (fast_tac (ZF_cs addSIs [rank_lt]) 1); 

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

14
1c0926788772
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); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

51 
by (rtac UN_least 1); 
0  52 
by (etac (rank_implies_mem RS bexE) 1); 
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

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

54 
by (etac UN_upper 2); 
0  55 
by (etac (subset_refl RS Vfrom_mono RS subset_trans RS Pow_mono) 1); 
56 
by (etac bspec 1); 

57 
by (assume_tac 1); 

58 
val Vfrom_rank_subset2 = result(); 

59 

60 
goal Univ.thy "Vfrom(A,rank(x)) = Vfrom(A,x)"; 

61 
by (rtac equalityI 1); 

62 
by (rtac Vfrom_rank_subset2 1); 

63 
by (rtac Vfrom_rank_subset1 1); 

64 
val Vfrom_rank_eq = result(); 

65 

66 

67 
(*** Basic closure properties ***) 

68 

69 
goal Univ.thy "!!x y. y:x ==> 0 : Vfrom(A,x)"; 

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

71 
by (fast_tac ZF_cs 1); 

72 
val zero_in_Vfrom = result(); 

73 

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

75 
by (eps_ind_tac "i" 1); 

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

77 
by (fast_tac ZF_cs 1); 

78 
val i_subset_Vfrom = result(); 

79 

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

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

82 
by (rtac Un_upper1 1); 

83 
val A_subset_Vfrom = result(); 

84 

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

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

87 
by (fast_tac ZF_cs 1); 

88 
val subset_mem_Vfrom = result(); 

89 

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

91 

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

93 
by (rtac subset_mem_Vfrom 1); 

94 
by (safe_tac ZF_cs); 

95 
val singleton_in_Vfrom = result(); 

96 

97 
goal Univ.thy 

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

99 
by (rtac subset_mem_Vfrom 1); 

100 
by (safe_tac ZF_cs); 

101 
val doubleton_in_Vfrom = result(); 

102 

103 
goalw Univ.thy [Pair_def] 

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

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

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

107 
val Pair_in_Vfrom = result(); 

108 

109 
val [prem] = goal Univ.thy 

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

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

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

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

114 
val succ_in_Vfrom = result(); 

115 

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

117 

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

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

120 
by (fast_tac eq_cs 1); 

121 
val Vfrom_0 = result(); 

122 

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

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

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

125 
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

126 
(2, equalityI RS subst_context)) 1); 
0  127 
by (rtac UN_least 1); 
128 
by (rtac (subset_refl RS Vfrom_mono RS Pow_mono) 1); 

129 
by (etac member_succD 1); 

130 
by (assume_tac 1); 

131 
val Vfrom_succ_lemma = result(); 

132 

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

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

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

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

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

138 
val Vfrom_succ = result(); 

139 

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

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

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

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

144 
by (rtac equalityI 1); 

145 
(*first inclusion*) 

146 
by (rtac Un_least 1); 

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

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

148 
by (rtac (prem RS UN_upper) 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

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

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

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

152 
by (etac UN_upper 2); 
0  153 
by (rtac (Vfrom RS ssubst) 1); 
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

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

156 
by (rtac UN_least 1); 
0  157 
by (rtac (Vfrom RS ssubst) 1); 
158 
by (fast_tac ZF_cs 1); 

159 
val Vfrom_Union = result(); 

160 

161 
(*** Limit ordinals  general properties ***) 

162 

163 
goalw Univ.thy [Limit_def] "!!i. Limit(i) ==> Union(i) = i"; 

164 
by (fast_tac (eq_cs addEs [Ord_trans]) 1); 

165 
val Limit_Union_eq = result(); 

166 

167 
goalw Univ.thy [Limit_def] "!!i. Limit(i) ==> Ord(i)"; 

168 
by (etac conjunct1 1); 

169 
val Limit_is_Ord = result(); 

170 

171 
goalw Univ.thy [Limit_def] "!!i. Limit(i) ==> 0 : i"; 

172 
by (fast_tac ZF_cs 1); 

173 
val Limit_has_0 = result(); 

174 

175 
goalw Univ.thy [Limit_def] "!!i. [ Limit(i); j:i ] ==> succ(j) : i"; 

176 
by (fast_tac ZF_cs 1); 

177 
val Limit_has_succ = result(); 

178 

179 
goalw Univ.thy [Limit_def] "Limit(nat)"; 

180 
by (REPEAT (ares_tac [conjI, ballI, nat_0I, nat_succI, Ord_nat] 1)); 

181 
val Limit_nat = result(); 

182 

183 
goalw Univ.thy [Limit_def] 

184 
"!!i. [ Ord(i); 0:i; ALL y. ~ succ(y)=i ] ==> Limit(i)"; 

185 
by (safe_tac subset_cs); 

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

186 
by (rtac Ord_member 1); 
0  187 
by (REPEAT_FIRST (eresolve_tac [asm_rl, Ord_in_Ord RS Ord_succ] 
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

188 
ORELSE' dtac Ord_succ_subsetI )); 
0  189 
by (fast_tac (subset_cs addSIs [equalityI]) 1); 
190 
val non_succ_LimitI = result(); 

191 

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

193 
by (fast_tac (ZF_cs addSIs [non_succ_LimitI, Ord_0_member_iff RS iffD2]) 1); 

194 
val Ord_cases_lemma = result(); 

195 

196 
val major::prems = goal Univ.thy 

197 
"[ Ord(i); \ 

198 
\ i=0 ==> P; \ 

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

200 
\ Limit(i) ==> P \ 

201 
\ ] ==> P"; 

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

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

204 
val Ord_cases = result(); 

205 

206 

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

208 

209 
(*NB. limit ordinals are nonempty; 

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

211 
val [limiti] = goal Univ.thy 

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

213 
by (rtac (limiti RS Limit_has_0 RS Vfrom_Union RS subst) 1); 

214 
by (rtac (limiti RS Limit_Union_eq RS ssubst) 1); 

215 
by (rtac refl 1); 

216 
val Limit_Vfrom_eq = result(); 

217 

218 
val Limit_VfromE = standard (Limit_Vfrom_eq RS equalityD1 RS subsetD RS UN_E); 

219 

220 
val [major,limiti] = goal Univ.thy 

221 
"[ a: Vfrom(A,i); Limit(i) ] ==> {a} : Vfrom(A,i)"; 

222 
by (rtac (limiti RS Limit_VfromE) 1); 

223 
by (rtac major 1); 

224 
by (rtac (limiti RS Limit_Vfrom_eq RS ssubst) 1); 

225 
by (rtac UN_I 1); 

226 
by (etac singleton_in_Vfrom 2); 

227 
by (etac (limiti RS Limit_has_succ) 1); 

228 
val singleton_in_Vfrom_limit = result(); 

229 

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

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

232 

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

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

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

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

237 
by (rtac (aprem RS (limiti RS Limit_VfromE)) 1); 

238 
by (rtac (bprem RS (limiti RS Limit_VfromE)) 1); 

239 
by (rtac (limiti RS Limit_Vfrom_eq RS ssubst) 1); 

240 
by (rtac UN_I 1); 

241 
by (rtac doubleton_in_Vfrom 2); 

242 
by (etac Vfrom_UnI1 2); 

243 
by (etac Vfrom_UnI2 2); 

244 
by (REPEAT (ares_tac[limiti, Limit_has_succ, Ord_member_UnI, Limit_is_Ord] 1)); 

245 
val doubleton_in_Vfrom_limit = result(); 

246 

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

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

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

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

251 
by (rtac (aprem RS (limiti RS Limit_VfromE)) 1); 

252 
by (rtac (bprem RS (limiti RS Limit_VfromE)) 1); 

253 
by (rtac (limiti RS Limit_Vfrom_eq RS ssubst) 1); 

254 
by (rtac UN_I 1); 

255 
by (rtac Pair_in_Vfrom 2); 

256 
(*Infer that succ(succ(x Un xa)) < i *) 

257 
by (etac Vfrom_UnI1 2); 

258 
by (etac Vfrom_UnI2 2); 

259 
by (REPEAT (ares_tac[limiti, Limit_has_succ, Ord_member_UnI, Limit_is_Ord] 1)); 

260 
val Pair_in_Vfrom_limit = result(); 

261 

262 

263 
(*** Properties assuming Transset(A) ***) 

264 

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

266 
by (eps_ind_tac "i" 1); 

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

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

269 
Transset_Pow]) 1); 

270 
val Transset_Vfrom = result(); 

271 

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

273 
by (rtac (Vfrom_succ RS trans) 1); 

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

274 
by (rtac (Un_upper2 RSN (2,equalityI)) 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

275 
by (rtac (subset_refl RSN (2,Un_least)) 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

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

277 
by (etac (Transset_Vfrom RS (Transset_iff_Pow RS iffD1)) 1); 
0  278 
val Transset_Vfrom_succ = result(); 
279 

280 
goalw Ord.thy [Pair_def,Transset_def] 

281 
"!!C. [ <a,b> <= C; Transset(C) ] ==> a: C & b: C"; 

282 
by (fast_tac ZF_cs 1); 

283 
val Transset_Pair_subset = result(); 

284 

285 
goal Univ.thy 

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

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

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

288 
by (etac (Transset_Pair_subset RS conjE) 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

289 
by (etac Transset_Vfrom 1); 
0  290 
by (REPEAT (ares_tac [Pair_in_Vfrom_limit] 1)); 
291 
val Transset_Pair_subset_Vfrom_limit = result(); 

292 

293 

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

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

296 
and i is a limit ordinal 

297 
***) 

298 

299 
(*There are three nearly identical proofs below  needs a general theorem 

300 
for proving ...a...b : Vfrom(A,i) where i is a limit ordinal*) 

301 

302 
(** products **) 

303 

304 
goal Univ.thy 

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

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

307 
by (dtac Transset_Vfrom 1); 

308 
by (rtac subset_mem_Vfrom 1); 

309 
by (rewtac Transset_def); 

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

311 
val prod_in_Vfrom = result(); 

312 

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

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

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

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

317 
by (rtac (aprem RS (limiti RS Limit_VfromE)) 1); 

318 
by (rtac (bprem RS (limiti RS Limit_VfromE)) 1); 

319 
by (rtac (limiti RS Limit_Vfrom_eq RS ssubst) 1); 

320 
by (rtac UN_I 1); 

321 
by (rtac prod_in_Vfrom 2); 

322 
(*Infer that succ(succ(succ(x Un xa))) < i *) 

323 
by (etac (Vfrom_UnI1 RS Vfrom_UnI2) 2); 

324 
by (etac (Vfrom_UnI2 RS Vfrom_UnI2) 2); 

325 
by (REPEAT (ares_tac [limiti RS Limit_has_succ, 

326 
Ord_member_UnI, limiti RS Limit_is_Ord, transset] 1)); 

327 
val prod_in_Vfrom_limit = result(); 

328 

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

330 

331 
goalw Univ.thy [sum_def] 

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

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

334 
by (dtac Transset_Vfrom 1); 

335 
by (rtac subset_mem_Vfrom 1); 

336 
by (rewtac Transset_def); 

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

338 
i_subset_Vfrom RS subsetD]) 1); 

339 
val sum_in_Vfrom = result(); 

340 

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

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

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

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

345 
by (rtac (aprem RS (limiti RS Limit_VfromE)) 1); 

346 
by (rtac (bprem RS (limiti RS Limit_VfromE)) 1); 

347 
by (rtac (limiti RS Limit_Vfrom_eq RS ssubst) 1); 

348 
by (rtac UN_I 1); 

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

349 
by (rtac sum_in_Vfrom 2); 
0  350 
by (rtac (succI1 RS UnI1) 5); 
351 
(*Infer that succ(succ(succ(x Un xa))) < i *) 

352 
by (etac (Vfrom_UnI1 RS Vfrom_UnI2) 2); 

353 
by (etac (Vfrom_UnI2 RS Vfrom_UnI2) 2); 

354 
by (REPEAT (ares_tac [limiti RS Limit_has_0, 

355 
limiti RS Limit_has_succ, 

356 
Ord_member_UnI, limiti RS Limit_is_Ord, transset] 1)); 

357 
val sum_in_Vfrom_limit = result(); 

358 

359 
(** function space! **) 

360 

361 
goalw Univ.thy [Pi_def] 

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

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

364 
by (dtac Transset_Vfrom 1); 

365 
by (rtac subset_mem_Vfrom 1); 

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

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

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

369 
by (rtac Un_upper2 3); 

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

371 
by (rtac Pow_mono 1); 

372 
by (rewtac Transset_def); 

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

374 
val fun_in_Vfrom = result(); 

375 

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

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

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

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

380 
by (rtac (aprem RS (limiti RS Limit_VfromE)) 1); 

381 
by (rtac (bprem RS (limiti RS Limit_VfromE)) 1); 

382 
by (rtac (limiti RS Limit_Vfrom_eq RS ssubst) 1); 

383 
by (rtac UN_I 1); 

384 
by (rtac fun_in_Vfrom 2); 

385 
(*Infer that succ(succ(succ(x Un xa))) < i *) 

386 
by (etac (Vfrom_UnI1 RS Vfrom_UnI2) 2); 

387 
by (etac (Vfrom_UnI2 RS Vfrom_UnI2) 2); 

388 
by (REPEAT (ares_tac [limiti RS Limit_has_succ, 

389 
Ord_member_UnI, limiti RS Limit_is_Ord, transset] 1)); 

390 
val fun_in_Vfrom_limit = result(); 

391 

392 

393 
(*** The set Vset(i) ***) 

394 

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

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

397 
by (fast_tac eq_cs 1); 

398 
val Vset = result(); 

399 

400 
val Vset_succ = Transset_0 RS Transset_Vfrom_succ; 

401 

402 
val Transset_Vset = Transset_0 RS Transset_Vfrom; 

403 

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

405 

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

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

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

409 
by (safe_tac ZF_cs); 

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

411 
by (rtac sup_least2 1); 

412 
by (assume_tac 1); 

413 
by (assume_tac 1); 

414 
by (fast_tac ZF_cs 1); 

415 
val Vset_rank_imp1 = result(); 

416 

417 
(* [ Ord(i); x : Vset(i) ] ==> rank(x) : i *) 

418 
val Vset_D = standard (Vset_rank_imp1 RS spec RS mp); 

419 

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

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

422 
by (rtac allI 1); 

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

424 
by (fast_tac (ZF_cs addSIs [rank_lt]) 1); 

425 
val Vset_rank_imp2 = result(); 

426 

427 
(* [ Ord(i); rank(x) : i ] ==> x : Vset(i) *) 

428 
val VsetI = standard (Vset_rank_imp2 RS spec RS mp); 

429 

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

431 
by (rtac iffI 1); 

432 
by (etac (ordi RS Vset_D) 1); 

433 
by (etac (ordi RS VsetI) 1); 

434 
val Vset_Ord_rank_iff = result(); 

435 

436 
goal Univ.thy "b : Vset(a) <> rank(b) : rank(a)"; 

437 
by (rtac (Vfrom_rank_eq RS subst) 1); 

438 
by (rtac (Ord_rank RS Vset_Ord_rank_iff) 1); 

439 
val Vset_rank_iff = result(); 

440 

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

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

443 
by (rtac equalityI 1); 

444 
by (safe_tac ZF_cs); 

445 
by (EVERY' [rtac UN_I, 

446 
etac (i_subset_Vfrom RS subsetD), 

447 
etac (Ord_in_Ord RS rank_of_Ord RS ssubst), 

448 
assume_tac, 

449 
rtac succI1] 3); 

450 
by (REPEAT (eresolve_tac [asm_rl,Vset_D,Ord_trans] 1)); 

451 
val rank_Vset = result(); 

452 

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

454 

455 
(* rank(x) : rank(a) ==> x : Vset(rank(a)) *) 

456 
val Vset_rankI = Ord_rank RS VsetI; 

457 

458 
goal Univ.thy "a <= Vset(rank(a))"; 

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

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

460 
by (etac (rank_lt RS Vset_rankI) 1); 
0  461 
val arg_subset_Vset_rank = result(); 
462 

463 
val [iprem] = goal Univ.thy 

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

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

465 
by (rtac ([subset_refl, arg_subset_Vset_rank] MRS Int_greatest RS subset_trans) 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

466 
by (rtac (Ord_rank RS iprem) 1); 
0  467 
val Int_Vset_subset = result(); 
468 

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

470 

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

472 
val rank_trans_rls = rank_rls @ (rank_rls RLN (2, [rank_trans])); 

473 

474 
val rank_ss = ZF_ss 

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

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

476 
addsimps rank_trans_rls; 
0  477 

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

479 

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

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

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

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

483 
by (simp_tac (ZF_ss addsimps [Ord_rank, Ord_succ, Vset_D RS beta, 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

484 
VsetI RS beta]) 1); 
0  485 
val Vrec = result(); 
486 

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

488 
val rew::prems = goal Univ.thy 

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

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

491 
by (rewtac rew); 

492 
by (rtac Vrec 1); 

493 
val def_Vrec = result(); 

494 

495 

496 
(*** univ(A) ***) 

497 

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

499 
by (etac Vfrom_mono 1); 

500 
by (rtac subset_refl 1); 

501 
val univ_mono = result(); 

502 

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

504 
by (etac Transset_Vfrom 1); 

505 
val Transset_univ = result(); 

506 

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

508 

509 
goalw Univ.thy [univ_def] "univ(A) = (UN i:nat. Vfrom(A,i))"; 

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

510 
by (rtac (Limit_nat RS Limit_Vfrom_eq) 1); 
0  511 
val univ_eq_UN = result(); 
512 

513 
goal Univ.thy "!!c. c <= univ(A) ==> c = (UN i:nat. c Int Vfrom(A,i))"; 

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

514 
by (rtac (subset_UN_iff_eq RS iffD1) 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

515 
by (etac (univ_eq_UN RS subst) 1); 
0  516 
val subset_univ_eq_Int = result(); 
517 

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

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

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

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

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

522 
by (rtac (aprem RS subset_univ_eq_Int RS ssubst) 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

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

524 
by (etac iprem 1); 
0  525 
val univ_Int_Vfrom_subset = result(); 
526 

527 
val prems = goal Univ.thy 

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

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

530 
\ ] ==> a = b"; 

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

531 
by (rtac equalityI 1); 
0  532 
by (ALLGOALS 
533 
(resolve_tac (prems RL [univ_Int_Vfrom_subset]) THEN' 

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

535 
rtac Int_lower1)); 

536 
val univ_Int_Vfrom_eq = result(); 

537 

538 
(** Closure properties **) 

539 

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

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

542 
val zero_in_univ = result(); 

543 

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

545 
by (rtac A_subset_Vfrom 1); 

546 
val A_subset_univ = result(); 

547 

548 
val A_into_univ = A_subset_univ RS subsetD; 

549 

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

551 

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

553 
by (rtac singleton_in_Vfrom_limit 1); 

554 
by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1)); 

555 
val singleton_in_univ = result(); 

556 

557 
goalw Univ.thy [univ_def] 

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

559 
by (rtac doubleton_in_Vfrom_limit 1); 

560 
by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1)); 

561 
val doubleton_in_univ = result(); 

562 

563 
goalw Univ.thy [univ_def] 

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

565 
by (rtac Pair_in_Vfrom_limit 1); 

566 
by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1)); 

567 
val Pair_in_univ = result(); 

568 

569 
goal Univ.thy "univ(A)*univ(A) <= univ(A)"; 

570 
by (REPEAT (ares_tac [subsetI,Pair_in_univ] 1 

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

572 
val product_univ = result(); 

573 

574 
val Sigma_subset_univ = standard 

575 
(Sigma_mono RS (product_univ RSN (2,subset_trans))); 

576 

577 
goalw Univ.thy [univ_def] 

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

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

579 
by (etac Transset_Pair_subset_Vfrom_limit 1); 
0  580 
by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1)); 
581 
val Transset_Pair_subset_univ = result(); 

582 

583 

584 
(** The natural numbers **) 

585 

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

587 
by (rtac i_subset_Vfrom 1); 

588 
val nat_subset_univ = result(); 

589 

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

591 
val nat_into_univ = standard (nat_subset_univ RS subsetD); 

592 

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

594 

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

595 
goal Univ.thy "1 : univ(A)"; 
0  596 
by (REPEAT (ares_tac [nat_into_univ, nat_0I, nat_succI] 1)); 
597 
val one_in_univ = result(); 

598 

599 
(*unused!*) 

600 
goal Univ.thy "succ(succ(0)) : univ(A)"; 

601 
by (REPEAT (ares_tac [nat_into_univ, nat_0I, nat_succI] 1)); 

602 
val two_in_univ = result(); 

603 

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

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

606 
val bool_subset_univ = result(); 

607 

608 
val bool_into_univ = standard (bool_subset_univ RS subsetD); 

609 

610 

611 
(** Closure under disjoint union **) 

612 

613 
goalw Univ.thy [Inl_def] "!!A a. a: univ(A) ==> Inl(a) : univ(A)"; 

614 
by (REPEAT (ares_tac [zero_in_univ,Pair_in_univ] 1)); 

615 
val Inl_in_univ = result(); 

616 

617 
goalw Univ.thy [Inr_def] "!!A b. b: univ(A) ==> Inr(b) : univ(A)"; 

618 
by (REPEAT (ares_tac [one_in_univ, Pair_in_univ] 1)); 

619 
val Inr_in_univ = result(); 

620 

621 
goal Univ.thy "univ(C)+univ(C) <= univ(C)"; 

622 
by (REPEAT (ares_tac [subsetI,Inl_in_univ,Inr_in_univ] 1 

623 
ORELSE eresolve_tac [sumE, ssubst] 1)); 

624 
val sum_univ = result(); 

625 

626 
val sum_subset_univ = standard 

627 
(sum_mono RS (sum_univ RSN (2,subset_trans))); 

628 

629 

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

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

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

633 

634 