author  lcp 
Fri, 17 Sep 1993 16:16:38 +0200  
changeset 6  8ce8c4d13d4d 
parent 0  a5a9c433f639 
child 14  1c0926788772 
permissions  rwrr 
0  1 
(* Title: ZF/ordinal.thy 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1993 University of Cambridge 

5 

6 
For ordinal.thy. Ordinals in ZermeloFraenkel Set Theory 

7 
*) 

8 

9 
open Ord; 

10 

11 
(*** Rules for Transset ***) 

12 

13 
(** Two neat characterisations of Transset **) 

14 

15 
goalw Ord.thy [Transset_def] "Transset(A) <> A<=Pow(A)"; 

16 
by (fast_tac ZF_cs 1); 

17 
val Transset_iff_Pow = result(); 

18 

19 
goalw Ord.thy [Transset_def] "Transset(A) <> Union(succ(A)) = A"; 

20 
by (fast_tac (eq_cs addSEs [equalityE]) 1); 

21 
val Transset_iff_Union_succ = result(); 

22 

23 
(** Consequences of downwards closure **) 

24 

25 
goalw Ord.thy [Transset_def] 

26 
"!!C a b. [ Transset(C); {a,b}: C ] ==> a:C & b: C"; 

27 
by (fast_tac ZF_cs 1); 

28 
val Transset_doubleton_D = result(); 

29 

30 
val [prem1,prem2] = goalw Ord.thy [Pair_def] 

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

32 
by (cut_facts_tac [prem2] 1); 

33 
by (fast_tac (ZF_cs addSDs [prem1 RS Transset_doubleton_D]) 1); 

34 
val Transset_Pair_D = result(); 

35 

36 
val prem1::prems = goal Ord.thy 

37 
"[ Transset(C); A*B <= C; b: B ] ==> A <= C"; 

38 
by (cut_facts_tac prems 1); 

39 
by (fast_tac (ZF_cs addSDs [prem1 RS Transset_Pair_D]) 1); 

40 
val Transset_includes_domain = result(); 

41 

42 
val prem1::prems = goal Ord.thy 

43 
"[ Transset(C); A*B <= C; a: A ] ==> B <= C"; 

44 
by (cut_facts_tac prems 1); 

45 
by (fast_tac (ZF_cs addSDs [prem1 RS Transset_Pair_D]) 1); 

46 
val Transset_includes_range = result(); 

47 

48 
val [prem1,prem2] = goalw (merge_theories(Ord.thy,Sum.thy)) [sum_def] 

49 
"[ Transset(C); A+B <= C ] ==> A <= C & B <= C"; 

50 
br (prem2 RS (Un_subset_iff RS iffD1) RS conjE) 1; 

51 
by (REPEAT (etac (prem1 RS Transset_includes_range) 1 

52 
ORELSE resolve_tac [conjI, singletonI] 1)); 

53 
val Transset_includes_summands = result(); 

54 

55 
val [prem] = goalw (merge_theories(Ord.thy,Sum.thy)) [sum_def] 

56 
"Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)"; 

57 
br (Int_Un_distrib RS ssubst) 1; 

58 
by (fast_tac (ZF_cs addSDs [prem RS Transset_Pair_D]) 1); 

59 
val Transset_sum_Int_subset = result(); 

60 

61 
(** Closure properties **) 

62 

63 
goalw Ord.thy [Transset_def] "Transset(0)"; 

64 
by (fast_tac ZF_cs 1); 

65 
val Transset_0 = result(); 

66 

67 
goalw Ord.thy [Transset_def] 

68 
"!!i j. [ Transset(i); Transset(j) ] ==> Transset(i Un j)"; 

69 
by (fast_tac ZF_cs 1); 

70 
val Transset_Un = result(); 

71 

72 
goalw Ord.thy [Transset_def] 

73 
"!!i j. [ Transset(i); Transset(j) ] ==> Transset(i Int j)"; 

74 
by (fast_tac ZF_cs 1); 

75 
val Transset_Int = result(); 

76 

77 
goalw Ord.thy [Transset_def] "!!i. Transset(i) ==> Transset(succ(i))"; 

78 
by (fast_tac ZF_cs 1); 

79 
val Transset_succ = result(); 

80 

81 
goalw Ord.thy [Transset_def] "!!i. Transset(i) ==> Transset(Pow(i))"; 

82 
by (fast_tac ZF_cs 1); 

83 
val Transset_Pow = result(); 

84 

85 
goalw Ord.thy [Transset_def] "!!A. Transset(A) ==> Transset(Union(A))"; 

86 
by (fast_tac ZF_cs 1); 

87 
val Transset_Union = result(); 

88 

89 
val [Transprem] = goalw Ord.thy [Transset_def] 

90 
"[ !!i. i:A ==> Transset(i) ] ==> Transset(Union(A))"; 

91 
by (fast_tac (ZF_cs addEs [Transprem RS bspec RS subsetD]) 1); 

92 
val Transset_Union_family = result(); 

93 

94 
val [prem,Transprem] = goalw Ord.thy [Transset_def] 

95 
"[ j:A; !!i. i:A ==> Transset(i) ] ==> Transset(Inter(A))"; 

96 
by (cut_facts_tac [prem] 1); 

97 
by (fast_tac (ZF_cs addEs [Transprem RS bspec RS subsetD]) 1); 

98 
val Transset_Inter_family = result(); 

99 

100 
(*** Natural Deduction rules for Ord ***) 

101 

102 
val prems = goalw Ord.thy [Ord_def] 

103 
"[ Transset(i); !!x. x:i ==> Transset(x) ] ==> Ord(i) "; 

104 
by (REPEAT (ares_tac (prems@[ballI,conjI]) 1)); 

105 
val OrdI = result(); 

106 

107 
val [major] = goalw Ord.thy [Ord_def] 

108 
"Ord(i) ==> Transset(i)"; 

109 
by (rtac (major RS conjunct1) 1); 

110 
val Ord_is_Transset = result(); 

111 

112 
val [major,minor] = goalw Ord.thy [Ord_def] 

113 
"[ Ord(i); j:i ] ==> Transset(j) "; 

114 
by (rtac (minor RS (major RS conjunct2 RS bspec)) 1); 

115 
val Ord_contains_Transset = result(); 

116 

117 
(*** Lemmas for ordinals ***) 

118 

119 
goalw Ord.thy [Ord_def,Transset_def] "!!i j. [ Ord(i); j:i ] ==> Ord(j) "; 

120 
by (fast_tac ZF_cs 1); 

121 
val Ord_in_Ord = result(); 

122 

123 
goal Ord.thy "!!i j. [ Ord(i); Transset(j); j<=i ] ==> Ord(j)"; 

124 
by (REPEAT (ares_tac [OrdI] 1 

125 
ORELSE eresolve_tac [Ord_contains_Transset, subsetD] 1)); 

126 
val Ord_subset_Ord = result(); 

127 

128 
goalw Ord.thy [Ord_def,Transset_def] "!!i j. [ j:i; Ord(i) ] ==> j<=i"; 

129 
by (fast_tac ZF_cs 1); 

130 
val OrdmemD = result(); 

131 

132 
goal Ord.thy "!!i j k. [ i:j; j:k; Ord(k) ] ==> i:k"; 

133 
by (REPEAT (ares_tac [OrdmemD RS subsetD] 1)); 

134 
val Ord_trans = result(); 

135 

136 
goal Ord.thy "!!i j. [ i:j; Ord(j) ] ==> succ(i) <= j"; 

137 
by (REPEAT (ares_tac [OrdmemD RSN (2,succ_subsetI)] 1)); 

138 
val Ord_succ_subsetI = result(); 

139 

140 

141 
(*** The construction of ordinals: 0, succ, Union ***) 

142 

143 
goal Ord.thy "Ord(0)"; 

144 
by (REPEAT (ares_tac [OrdI,Transset_0] 1 ORELSE etac emptyE 1)); 

145 
val Ord_0 = result(); 

146 

147 
goal Ord.thy "!!i. Ord(i) ==> Ord(succ(i))"; 

148 
by (REPEAT (ares_tac [OrdI,Transset_succ] 1 

149 
ORELSE eresolve_tac [succE,ssubst,Ord_is_Transset, 

150 
Ord_contains_Transset] 1)); 

151 
val Ord_succ = result(); 

152 

153 
val nonempty::prems = goal Ord.thy 

154 
"[ j:A; !!i. i:A ==> Ord(i) ] ==> Ord(Inter(A))"; 

155 
by (rtac (nonempty RS Transset_Inter_family RS OrdI) 1); 

156 
by (rtac Ord_is_Transset 1); 

157 
by (REPEAT (ares_tac ([Ord_contains_Transset,nonempty]@prems) 1 

158 
ORELSE etac InterD 1)); 

159 
val Ord_Inter = result(); 

160 

161 
val jmemA::prems = goal Ord.thy 

162 
"[ j:A; !!x. x:A ==> Ord(B(x)) ] ==> Ord(INT x:A. B(x))"; 

163 
by (rtac (jmemA RS RepFunI RS Ord_Inter) 1); 

164 
by (etac RepFunE 1); 

165 
by (etac ssubst 1); 

166 
by (eresolve_tac prems 1); 

167 
val Ord_INT = result(); 

168 

169 

170 
(*** Natural Deduction rules for Memrel ***) 

171 

172 
goalw Ord.thy [Memrel_def] "<a,b> : Memrel(A) <> a:b & a:A & b:A"; 

173 
by (fast_tac ZF_cs 1); 

174 
val Memrel_iff = result(); 

175 

176 
val prems = goal Ord.thy "[ a: b; a: A; b: A ] ==> <a,b> : Memrel(A)"; 

177 
by (REPEAT (resolve_tac (prems@[conjI, Memrel_iff RS iffD2]) 1)); 

178 
val MemrelI = result(); 

179 

180 
val [major,minor] = goal Ord.thy 

181 
"[ <a,b> : Memrel(A); \ 

182 
\ [ a: A; b: A; a:b ] ==> P \ 

183 
\ ] ==> P"; 

184 
by (rtac (major RS (Memrel_iff RS iffD1) RS conjE) 1); 

185 
by (etac conjE 1); 

186 
by (rtac minor 1); 

187 
by (REPEAT (assume_tac 1)); 

188 
val MemrelE = result(); 

189 

190 
(*The membership relation (as a set) is wellfounded. 

191 
Proof idea: show A<=B by applying the foundation axiom to AB *) 

192 
goalw Ord.thy [wf_def] "wf(Memrel(A))"; 

193 
by (EVERY1 [rtac (foundation RS disjE RS allI), 

194 
etac disjI1, 

195 
etac bexE, 

196 
rtac (impI RS allI RS bexI RS disjI2), 

197 
etac MemrelE, 

198 
etac bspec, 

199 
REPEAT o assume_tac]); 

200 
val wf_Memrel = result(); 

201 

202 
(*** Transfinite induction ***) 

203 

204 
(*Epsilon induction over a transitive set*) 

205 
val major::prems = goalw Ord.thy [Transset_def] 

206 
"[ i: k; Transset(k); \ 

207 
\ !!x.[ x: k; ALL y:x. P(y) ] ==> P(x) \ 

208 
\ ] ==> P(i)"; 

209 
by (rtac (major RS (wf_Memrel RS wf_induct2)) 1); 

210 
by (fast_tac (ZF_cs addEs [MemrelE]) 1); 

211 
by (resolve_tac prems 1); 

212 
by (assume_tac 1); 

213 
by (cut_facts_tac prems 1); 

214 
by (fast_tac (ZF_cs addIs [MemrelI]) 1); 

215 
val Transset_induct = result(); 

216 

217 
(*Induction over an ordinal*) 

218 
val Ord_induct = Ord_is_Transset RSN (2, Transset_induct); 

219 

220 
(*Induction over the class of ordinals  a useful corollary of Ord_induct*) 

221 
val [major,indhyp] = goal Ord.thy 

222 
"[ Ord(i); \ 

223 
\ !!x.[ Ord(x); ALL y:x. P(y) ] ==> P(x) \ 

224 
\ ] ==> P(i)"; 

225 
by (rtac (major RS Ord_succ RS (succI1 RS Ord_induct)) 1); 

226 
by (rtac indhyp 1); 

227 
by (rtac (major RS Ord_succ RS Ord_in_Ord) 1); 

228 
by (REPEAT (assume_tac 1)); 

229 
val trans_induct = result(); 

230 

231 
(*Perform induction on i, then prove the Ord(i) subgoal using prems. *) 

232 
fun trans_ind_tac a prems i = 

233 
EVERY [res_inst_tac [("i",a)] trans_induct i, 

234 
rename_last_tac a ["1"] (i+1), 

235 
ares_tac prems i]; 

236 

237 

238 
(*** Fundamental properties of the epsilon ordering (< on ordinals) ***) 

239 

240 
(*Finds contradictions for the following proof*) 

241 
val Ord_trans_tac = EVERY' [etac notE, etac Ord_trans, REPEAT o atac]; 

242 

243 
(** Proving that "member" is a linear ordering on the ordinals **) 

244 

245 
val prems = goal Ord.thy 

246 
"Ord(i) ==> (ALL j. Ord(j) > i:j  i=j  j:i)"; 

247 
by (trans_ind_tac "i" prems 1); 

248 
by (rtac (impI RS allI) 1); 

249 
by (trans_ind_tac "j" [] 1); 

250 
by (DEPTH_SOLVE (swap_res_tac [disjCI,equalityI,subsetI] 1 

251 
ORELSE ball_tac 1 

252 
ORELSE eresolve_tac [impE,disjE,allE] 1 

253 
ORELSE hyp_subst_tac 1 

254 
ORELSE Ord_trans_tac 1)); 

255 
val Ord_linear_lemma = result(); 

256 

257 
val ordi::ordj::prems = goal Ord.thy 

258 
"[ Ord(i); Ord(j); i:j ==> P; i=j ==> P; j:i ==> P ] \ 

259 
\ ==> P"; 

260 
by (rtac (ordi RS Ord_linear_lemma RS spec RS impE) 1); 

261 
by (rtac ordj 1); 

262 
by (REPEAT (eresolve_tac (prems@[asm_rl,disjE]) 1)); 

263 
val Ord_linear = result(); 

264 

265 
val prems = goal Ord.thy 

266 
"[ Ord(i); Ord(j); i<=j ==> P; j<=i ==> P ] \ 

267 
\ ==> P"; 

268 
by (res_inst_tac [("i","i"),("j","j")] Ord_linear 1); 

269 
by (DEPTH_SOLVE (ares_tac (prems@[subset_refl]) 1 

270 
ORELSE eresolve_tac [asm_rl,OrdmemD,ssubst] 1)); 

271 
val Ord_subset = result(); 

272 

273 
goal Ord.thy "!!i j. [ j<=i; ~ i<=j; Ord(i); Ord(j) ] ==> j:i"; 

274 
by (etac Ord_linear 1); 

275 
by (REPEAT (ares_tac [subset_refl] 1 

276 
ORELSE eresolve_tac [notE,OrdmemD,ssubst] 1)); 

277 
val Ord_member = result(); 

278 

279 
val [prem] = goal Ord.thy "Ord(i) ==> 0: succ(i)"; 

280 
by (rtac (empty_subsetI RS Ord_member) 1); 

281 
by (fast_tac ZF_cs 1); 

282 
by (rtac (prem RS Ord_succ) 1); 

283 
by (rtac Ord_0 1); 

284 
val Ord_0_mem_succ = result(); 

285 

286 
goal Ord.thy "!!i j. [ Ord(i); Ord(j) ] ==> j:i <> j<=i & ~(i<=j)"; 

287 
by (rtac iffI 1); 

288 
by (rtac conjI 1); 

289 
by (etac OrdmemD 1); 

290 
by (rtac (mem_anti_refl RS notI) 2); 

291 
by (etac subsetD 2); 

292 
by (REPEAT (eresolve_tac [asm_rl, conjE, Ord_member] 1)); 

293 
val Ord_member_iff = result(); 

294 

295 
goal Ord.thy "!!i. Ord(i) ==> 0:i <> ~ i=0"; 

296 
be (Ord_0 RSN (2,Ord_member_iff) RS iff_trans) 1; 

297 
by (fast_tac eq_cs 1); 

298 
val Ord_0_member_iff = result(); 

299 

300 
(** For ordinals, i: succ(j) means 'lessthan or equals' **) 

301 

302 
goal Ord.thy "!!i j. [ j<=i; Ord(i); Ord(j) ] ==> j : succ(i)"; 

303 
by (rtac Ord_member 1); 

304 
by (REPEAT (ares_tac [Ord_succ] 3)); 

305 
by (rtac (mem_anti_refl RS notI) 2); 

306 
by (etac subsetD 2); 

307 
by (ALLGOALS (fast_tac ZF_cs)); 

308 
val member_succI = result(); 

309 

310 
goalw Ord.thy [Transset_def,Ord_def] 

311 
"!!i j. [ i : succ(j); Ord(j) ] ==> i<=j"; 

312 
by (fast_tac ZF_cs 1); 

313 
val member_succD = result(); 

314 

315 
goal Ord.thy "!!i j. [ Ord(i); Ord(j) ] ==> j:succ(i) <> j<=i"; 

316 
by (fast_tac (subset_cs addSEs [member_succI, member_succD]) 1); 

317 
val member_succ_iff = result(); 

318 

319 
goal Ord.thy 

320 
"!!i j. [ Ord(i); Ord(j) ] ==> i<=succ(j) <> i<=j  i=succ(j)"; 

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

321 
by (asm_simp_tac (ZF_ss addsimps [member_succ_iff RS iff_sym, Ord_succ]) 1); 
0  322 
by (fast_tac ZF_cs 1); 
323 
val subset_succ_iff = result(); 

324 

325 
goal Ord.thy "!!i j. [ i:succ(j); j:k; Ord(k) ] ==> i:k"; 

326 
by (fast_tac (ZF_cs addEs [Ord_trans]) 1); 

327 
val Ord_trans1 = result(); 

328 

329 
goal Ord.thy "!!i j. [ i:j; j:succ(k); Ord(k) ] ==> i:k"; 

330 
by (fast_tac (ZF_cs addEs [Ord_trans]) 1); 

331 
val Ord_trans2 = result(); 

332 

333 
goal Ord.thy "!!i jk. [ i:j; j<=k; Ord(k) ] ==> i:k"; 

334 
by (fast_tac (ZF_cs addEs [Ord_trans]) 1); 

335 
val Ord_transsub2 = result(); 

336 

337 
goal Ord.thy "!!i j. [ i:j; Ord(j) ] ==> succ(i) : succ(j)"; 

338 
by (rtac member_succI 1); 

339 
by (REPEAT (ares_tac [subsetI,Ord_succ,Ord_in_Ord] 1 

340 
ORELSE eresolve_tac [succE,Ord_trans,ssubst] 1)); 

341 
val succ_mem_succI = result(); 

342 

343 
goal Ord.thy "!!i j. [ succ(i) : succ(j); Ord(j) ] ==> i:j"; 

344 
by (REPEAT (eresolve_tac [asm_rl, make_elim member_succD, succ_subsetE] 1)); 

345 
val succ_mem_succE = result(); 

346 

347 
goal Ord.thy "!!i j. Ord(j) ==> succ(i) : succ(j) <> i:j"; 

348 
by (REPEAT (ares_tac [iffI,succ_mem_succI,succ_mem_succE] 1)); 

349 
val succ_mem_succ_iff = result(); 

350 

351 
goal Ord.thy "!!i j. [ i<=j; Ord(i); Ord(j) ] ==> succ(i) <= succ(j)"; 

352 
by (rtac (member_succI RS succ_mem_succI RS member_succD) 1); 

353 
by (REPEAT (ares_tac [Ord_succ] 1)); 

354 
val Ord_succ_mono = result(); 

355 

356 
goal Ord.thy "!!i j k. [ i:k; j:k; Ord(k) ] ==> i Un j : k"; 

357 
by (res_inst_tac [("i","i"),("j","j")] Ord_subset 1); 

358 
by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1)); 

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

359 
by (asm_simp_tac (ZF_ss addsimps [subset_Un_iff RS iffD1]) 1); 
0  360 
by (rtac (Un_commute RS ssubst) 1); 
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

361 
by (asm_simp_tac (ZF_ss addsimps [subset_Un_iff RS iffD1]) 1); 
0  362 
val Ord_member_UnI = result(); 
363 

364 
goal Ord.thy "!!i j k. [ i:k; j:k; Ord(k) ] ==> i Int j : k"; 

365 
by (res_inst_tac [("i","i"),("j","j")] Ord_subset 1); 

366 
by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1)); 

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

367 
by (asm_simp_tac (ZF_ss addsimps [subset_Int_iff RS iffD1]) 1); 
0  368 
by (rtac (Int_commute RS ssubst) 1); 
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

369 
by (asm_simp_tac (ZF_ss addsimps [subset_Int_iff RS iffD1]) 1); 
0  370 
val Ord_member_IntI = result(); 
371 

372 

373 
(*** Results about limits ***) 

374 

375 
val prems = goal Ord.thy "[ !!i. i:A ==> Ord(i) ] ==> Ord(Union(A))"; 

376 
by (rtac (Ord_is_Transset RS Transset_Union_family RS OrdI) 1); 

377 
by (REPEAT (etac UnionE 1 ORELSE ares_tac ([Ord_contains_Transset]@prems) 1)); 

378 
val Ord_Union = result(); 

379 

380 
val prems = goal Ord.thy "[ !!x. x:A ==> Ord(B(x)) ] ==> Ord(UN x:A. B(x))"; 

381 
by (rtac Ord_Union 1); 

382 
by (etac RepFunE 1); 

383 
by (etac ssubst 1); 

384 
by (eresolve_tac prems 1); 

385 
val Ord_UN = result(); 

386 

387 
(*The upper bound must be a successor ordinal  

388 
consider that (UN i:nat.i)=nat although nat is an upper bound of each i*) 

389 
val [ordi,limit] = goal Ord.thy 

390 
"[ Ord(i); !!y. y:A ==> f(y): succ(i) ] ==> (UN y:A. f(y)) : succ(i)"; 

391 
by (rtac (member_succD RS UN_least RS member_succI) 1); 

392 
by (REPEAT (ares_tac [ordi, Ord_UN, ordi RS Ord_succ RS Ord_in_Ord, 

393 
limit] 1)); 

394 
val sup_least = result(); 

395 

396 
val [jmemi,ordi,limit] = goal Ord.thy 

397 
"[ j: i; Ord(i); !!y. y:A ==> f(y): j ] ==> (UN y:A. succ(f(y))) : i"; 

398 
by (cut_facts_tac [jmemi RS (ordi RS Ord_in_Ord)] 1); 

399 
by (rtac (sup_least RS Ord_trans2) 1); 

400 
by (REPEAT (ares_tac [jmemi, ordi, succ_mem_succI, limit] 1)); 

401 
val sup_least2 = result(); 

402 

403 
goal Ord.thy "!!i. Ord(i) ==> (UN y:i. succ(y)) = i"; 

404 
by (fast_tac (eq_cs addSEs [Ord_trans1]) 1); 

405 
val Ord_equality = result(); 

406 

407 
(*Holds for all transitive sets, not just ordinals*) 

408 
goal Ord.thy "!!i. Ord(i) ==> Union(i) <= i"; 

409 
by (fast_tac (ZF_cs addSEs [Ord_trans]) 1); 

410 
val Ord_Union_subset = result(); 