author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 186  320f6bdb593a 
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"; 

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

50 
by (rtac (prem2 RS (Un_subset_iff RS iffD1) RS conjE) 1); 
0  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)"; 

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

57 
by (rtac (Int_Un_distrib RS ssubst) 1); 
0  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 

30  123 
(* Ord(succ(j)) ==> Ord(j) *) 
124 
val Ord_succD = succI1 RSN (2, Ord_in_Ord); 

125 

0  126 
goal Ord.thy "!!i j. [ Ord(i); Transset(j); j<=i ] ==> Ord(j)"; 
127 
by (REPEAT (ares_tac [OrdI] 1 

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

129 
val Ord_subset_Ord = result(); 

130 

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

132 
by (fast_tac ZF_cs 1); 

133 
val OrdmemD = result(); 

134 

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

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

137 
val Ord_trans = result(); 

138 

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

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

141 
val Ord_succ_subsetI = result(); 

142 

143 

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

145 

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

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

148 
val Ord_0 = result(); 

149 

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

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

152 
ORELSE eresolve_tac [succE,ssubst,Ord_is_Transset, 

153 
Ord_contains_Transset] 1)); 

154 
val Ord_succ = result(); 

155 

30  156 
goal Ord.thy "Ord(succ(i)) <> Ord(i)"; 
157 
by (fast_tac (ZF_cs addIs [Ord_succ] addDs [Ord_succD]) 1); 

158 
val Ord_succ_iff = result(); 

159 

186  160 
goalw Ord.thy [Ord_def] "!!i j. [ Ord(i); Ord(j) ] ==> Ord(i Un j)"; 
161 
by (fast_tac (ZF_cs addSIs [Transset_Un]) 1); 

162 
val Ord_Un = result(); 

163 

164 
goalw Ord.thy [Ord_def] "!!i j. [ Ord(i); Ord(j) ] ==> Ord(i Int j)"; 

165 
by (fast_tac (ZF_cs addSIs [Transset_Int]) 1); 

166 
val Ord_Int = result(); 

167 

0  168 
val nonempty::prems = goal Ord.thy 
169 
"[ j:A; !!i. i:A ==> Ord(i) ] ==> Ord(Inter(A))"; 

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

171 
by (rtac Ord_is_Transset 1); 

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

173 
ORELSE etac InterD 1)); 

174 
val Ord_Inter = result(); 

175 

176 
val jmemA::prems = goal Ord.thy 

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

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

179 
by (etac RepFunE 1); 

180 
by (etac ssubst 1); 

181 
by (eresolve_tac prems 1); 

182 
val Ord_INT = result(); 

183 

184 

30  185 
(*** < is 'less than' for ordinals ***) 
186 

187 
goalw Ord.thy [lt_def] "!!i j. [ i:j; Ord(j) ] ==> i<j"; 

188 
by (REPEAT (ares_tac [conjI] 1)); 

189 
val ltI = result(); 

190 

191 
val major::prems = goalw Ord.thy [lt_def] 

192 
"[ i<j; [ i:j; Ord(i); Ord(j) ] ==> P ] ==> P"; 

193 
by (rtac (major RS conjE) 1); 

194 
by (REPEAT (ares_tac (prems@[Ord_in_Ord]) 1)); 

195 
val ltE = result(); 

196 

197 
goal Ord.thy "!!i j. i<j ==> i:j"; 

198 
by (etac ltE 1); 

199 
by (assume_tac 1); 

200 
val ltD = result(); 

201 

202 
goalw Ord.thy [lt_def] "~ i<0"; 

203 
by (fast_tac ZF_cs 1); 

204 
val not_lt0 = result(); 

205 

206 
(* i<0 ==> R *) 

207 
val lt0E = standard (not_lt0 RS notE); 

208 

209 
goal Ord.thy "!!i j k. [ i<j; j<k ] ==> i<k"; 

210 
by (fast_tac (ZF_cs addSIs [ltI] addSEs [ltE, Ord_trans]) 1); 

211 
val lt_trans = result(); 

212 

213 
goalw Ord.thy [lt_def] "!!i j. [ i<j; j<i ] ==> P"; 

214 
by (REPEAT (eresolve_tac [asm_rl, conjE, mem_anti_sym] 1)); 

215 
val lt_anti_sym = result(); 

216 

217 
val lt_anti_refl = prove_goal Ord.thy "i<i ==> P" 

218 
(fn [major]=> [ (rtac (major RS (major RS lt_anti_sym)) 1) ]); 

219 

220 
val lt_not_refl = prove_goal Ord.thy "~ i<i" 

221 
(fn _=> [ (rtac notI 1), (etac lt_anti_refl 1) ]); 

222 

223 
(** le is less than or equals; recall i le j abbrevs i<succ(j) !! **) 

224 

225 
goalw Ord.thy [lt_def] "i le j <> i<j  (i=j & Ord(j))"; 

226 
by (fast_tac (ZF_cs addSIs [Ord_succ] addSDs [Ord_succD]) 1); 

227 
val le_iff = result(); 

228 

229 
goal Ord.thy "!!i j. i<j ==> i le j"; 

230 
by (asm_simp_tac (ZF_ss addsimps [le_iff]) 1); 

231 
val leI = result(); 

232 

233 
goal Ord.thy "!!i. [ i=j; Ord(j) ] ==> i le j"; 

234 
by (asm_simp_tac (ZF_ss addsimps [le_iff]) 1); 

235 
val le_eqI = result(); 

236 

237 
val le_refl = refl RS le_eqI; 

238 

239 
val [prem] = goal Ord.thy "(~ (i=j & Ord(j)) ==> i<j) ==> i le j"; 

240 
by (rtac (disjCI RS (le_iff RS iffD2)) 1); 

241 
by (etac prem 1); 

242 
val leCI = result(); 

243 

244 
val major::prems = goal Ord.thy 

245 
"[ i le j; i<j ==> P; [ i=j; Ord(j) ] ==> P ] ==> P"; 

246 
by (rtac (major RS (le_iff RS iffD1 RS disjE)) 1); 

247 
by (DEPTH_SOLVE (ares_tac prems 1 ORELSE etac conjE 1)); 

248 
val leE = result(); 

249 

250 
goal Ord.thy "!!i j. [ i le j; j le i ] ==> i=j"; 

251 
by (asm_full_simp_tac (ZF_ss addsimps [le_iff]) 1); 

252 
by (fast_tac (ZF_cs addEs [lt_anti_sym]) 1); 

253 
val le_asym = result(); 

254 

255 
goal Ord.thy "i le 0 <> i=0"; 

256 
by (fast_tac (ZF_cs addSIs [Ord_0 RS le_refl] addSEs [leE, lt0E]) 1); 

257 
val le0_iff = result(); 

258 

259 
val le0D = standard (le0_iff RS iffD1); 

260 

261 
val lt_cs = 

262 
ZF_cs addSIs [le_refl, leCI] 

263 
addSDs [le0D] 

264 
addSEs [lt_anti_refl, lt0E, leE]; 

265 

266 

0  267 
(*** Natural Deduction rules for Memrel ***) 
268 

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

270 
by (fast_tac ZF_cs 1); 

271 
val Memrel_iff = result(); 

272 

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

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

275 
val MemrelI = result(); 

276 

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

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

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

280 
\ ] ==> P"; 

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

282 
by (etac conjE 1); 

283 
by (rtac minor 1); 

284 
by (REPEAT (assume_tac 1)); 

285 
val MemrelE = result(); 

286 

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

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

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

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

291 
etac disjI1, 

292 
etac bexE, 

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

294 
etac MemrelE, 

295 
etac bspec, 

296 
REPEAT o assume_tac]); 

297 
val wf_Memrel = result(); 

298 

299 
(*** Transfinite induction ***) 

300 

301 
(*Epsilon induction over a transitive set*) 

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

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

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

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

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

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

308 
by (resolve_tac prems 1); 

309 
by (assume_tac 1); 

310 
by (cut_facts_tac prems 1); 

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

312 
val Transset_induct = result(); 

313 

314 
(*Induction over an ordinal*) 

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

316 

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

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

319 
"[ Ord(i); \ 

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

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

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

323 
by (rtac indhyp 1); 

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

325 
by (REPEAT (assume_tac 1)); 

326 
val trans_induct = result(); 

327 

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

329 
fun trans_ind_tac a prems i = 

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

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

332 
ares_tac prems i]; 

333 

334 

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

336 

337 
(*Finds contradictions for the following proof*) 

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

339 

30  340 
(** Proving that < is a linear ordering on the ordinals **) 
0  341 

342 
val prems = goal Ord.thy 

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

344 
by (trans_ind_tac "i" prems 1); 

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

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

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

348 
ORELSE ball_tac 1 

349 
ORELSE eresolve_tac [impE,disjE,allE] 1 

350 
ORELSE hyp_subst_tac 1 

351 
ORELSE Ord_trans_tac 1)); 

352 
val Ord_linear_lemma = result(); 

353 

30  354 
(*The trichotomy law for ordinals!*) 
355 
val ordi::ordj::prems = goalw Ord.thy [lt_def] 

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

357 
by (rtac ([ordi,ordj] MRS (Ord_linear_lemma RS spec RS impE)) 1); 

358 
by (REPEAT (FIRSTGOAL (etac disjE))); 

359 
by (DEPTH_SOLVE (ares_tac ([ordi,ordj,conjI] @ prems) 1)); 

360 
val Ord_linear_lt = result(); 

0  361 

362 
val prems = goal Ord.thy 

30  363 
"[ Ord(i); Ord(j); i le j ==> P; j le i ==> P ] ==> P"; 
364 
by (res_inst_tac [("i","i"),("j","j")] Ord_linear_lt 1); 

365 
by (DEPTH_SOLVE (ares_tac ([leI,le_eqI] @ prems) 1)); 

366 
val Ord_linear_le = result(); 

367 

368 
goal Ord.thy "!!i j. j le i ==> ~ i<j"; 

369 
by (fast_tac (lt_cs addEs [lt_anti_sym]) 1); 

370 
val le_imp_not_lt = result(); 

0  371 

30  372 
goal Ord.thy "!!i j. [ ~ i<j; Ord(i); Ord(j) ] ==> j le i"; 
373 
by (res_inst_tac [("i","i"),("j","j")] Ord_linear_le 1); 

374 
by (REPEAT (SOMEGOAL assume_tac)); 

375 
by (fast_tac (lt_cs addEs [lt_anti_sym]) 1); 

376 
val not_lt_imp_le = result(); 

0  377 

30  378 
goal Ord.thy "!!i j. [ Ord(i); Ord(j) ] ==> ~ i<j <> j le i"; 
379 
by (REPEAT (ares_tac [iffI, le_imp_not_lt, not_lt_imp_le] 1)); 

380 
val not_lt_iff_le = result(); 

0  381 

30  382 
goal Ord.thy "!!i j. [ Ord(i); Ord(j) ] ==> ~ i le j <> j<i"; 
383 
by (asm_simp_tac (ZF_ss addsimps [not_lt_iff_le RS iff_sym]) 1); 

384 
val not_le_iff_lt = result(); 

385 

386 
goal Ord.thy "!!i. Ord(i) ==> 0 le i"; 

387 
by (etac (not_lt_iff_le RS iffD1) 1); 

388 
by (REPEAT (resolve_tac [Ord_0, not_lt0] 1)); 

389 
val Ord_0_le = result(); 

0  390 

37  391 
goal Ord.thy "!!i. [ Ord(i); i~=0 ] ==> 0<i"; 
30  392 
by (etac (not_le_iff_lt RS iffD1) 1); 
393 
by (rtac Ord_0 1); 

394 
by (fast_tac lt_cs 1); 

395 
val Ord_0_lt = result(); 

0  396 

30  397 
(*** Results about lessthan or equals ***) 
398 

399 
(** For ordinals, j<=i (subset) implies j le i (lessthan or equals) **) 

0  400 

30  401 
goal Ord.thy "!!i j. [ j<=i; Ord(i); Ord(j) ] ==> j le i"; 
402 
by (rtac (not_lt_iff_le RS iffD1) 1); 

403 
by (assume_tac 1); 

404 
by (assume_tac 1); 

405 
by (fast_tac (ZF_cs addEs [ltE, mem_anti_refl]) 1); 

406 
val subset_imp_le = result(); 

0  407 

30  408 
goal Ord.thy "!!i j. i le j ==> i<=j"; 
409 
by (etac leE 1); 

410 
by (fast_tac ZF_cs 2); 

411 
by (fast_tac (subset_cs addIs [OrdmemD] addEs [ltE]) 1); 

412 
val le_imp_subset = result(); 

0  413 

30  414 
goal Ord.thy "j le i <> j<=i & Ord(i) & Ord(j)"; 
415 
by (fast_tac (ZF_cs addSEs [subset_imp_le, le_imp_subset] 

416 
addEs [ltE, make_elim Ord_succD]) 1); 

417 
val le_subset_iff = result(); 

418 

419 
goal Ord.thy "i le succ(j) <> i le j  i=succ(j) & Ord(i)"; 

420 
by (simp_tac (ZF_ss addsimps [le_iff]) 1); 

421 
by (fast_tac (ZF_cs addIs [Ord_succ] addDs [Ord_succD]) 1); 

422 
val le_succ_iff = result(); 

0  423 

30  424 
goal Ord.thy "!!i j. [ i le j; j<k ] ==> i<k"; 
425 
by (fast_tac (ZF_cs addEs [leE, lt_trans]) 1); 

426 
val lt_trans1 = result(); 

0  427 

30  428 
goal Ord.thy "!!i j. [ i<j; j le k ] ==> i<k"; 
429 
by (fast_tac (ZF_cs addEs [leE, lt_trans]) 1); 

430 
val lt_trans2 = result(); 

431 

432 
goal Ord.thy "!!i j. [ i le j; j le k ] ==> i le k"; 

433 
by (REPEAT (ares_tac [lt_trans1] 1)); 

434 
val le_trans = result(); 

0  435 

30  436 
goal Ord.thy "!!i j. i<j ==> succ(i) le j"; 
437 
by (rtac (not_lt_iff_le RS iffD1) 1); 

438 
by (fast_tac (lt_cs addEs [lt_anti_sym]) 3); 

439 
by (ALLGOALS (fast_tac (ZF_cs addEs [ltE] addIs [Ord_succ]))); 

440 
val succ_leI = result(); 

0  441 

30  442 
goal Ord.thy "!!i j. succ(i) le j ==> i<j"; 
443 
by (rtac (not_le_iff_lt RS iffD1) 1); 

444 
by (fast_tac (lt_cs addEs [lt_anti_sym]) 3); 

445 
by (ALLGOALS (fast_tac (ZF_cs addEs [ltE, make_elim Ord_succD]))); 

446 
val succ_leE = result(); 

0  447 

30  448 
goal Ord.thy "succ(i) le j <> i<j"; 
449 
by (REPEAT (ares_tac [iffI,succ_leI,succ_leE] 1)); 

450 
val succ_le_iff = result(); 

0  451 

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

452 
(** Union and Intersection **) 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

453 

186  454 
goal Ord.thy "!!i j. [ Ord(i); Ord(j) ] ==> i le i Un j"; 
455 
by (rtac (Un_upper1 RS subset_imp_le) 1); 

456 
by (REPEAT (ares_tac [Ord_Un] 1)); 

457 
val Un_upper1_le = result(); 

458 

459 
goal Ord.thy "!!i j. [ Ord(i); Ord(j) ] ==> j le i Un j"; 

460 
by (rtac (Un_upper2 RS subset_imp_le) 1); 

461 
by (REPEAT (ares_tac [Ord_Un] 1)); 

462 
val Un_upper2_le = result(); 

463 

30  464 
(*Replacing k by succ(k') yields the similar rule for le!*) 
465 
goal Ord.thy "!!i j k. [ i<k; j<k ] ==> i Un j < k"; 

466 
by (res_inst_tac [("i","i"),("j","j")] Ord_linear_le 1); 

467 
by (rtac (Un_commute RS ssubst) 4); 

468 
by (asm_full_simp_tac (ZF_ss addsimps [le_subset_iff, subset_Un_iff]) 4); 

469 
by (asm_full_simp_tac (ZF_ss addsimps [le_subset_iff, subset_Un_iff]) 3); 

470 
by (REPEAT (eresolve_tac [asm_rl, ltE] 1)); 

471 
val Un_least_lt = result(); 

0  472 

30  473 
(*Replacing k by succ(k') yields the similar rule for le!*) 
474 
goal Ord.thy "!!i j k. [ i<k; j<k ] ==> i Int j < k"; 

475 
by (res_inst_tac [("i","i"),("j","j")] Ord_linear_le 1); 

476 
by (rtac (Int_commute RS ssubst) 4); 

477 
by (asm_full_simp_tac (ZF_ss addsimps [le_subset_iff, subset_Int_iff]) 4); 

478 
by (asm_full_simp_tac (ZF_ss addsimps [le_subset_iff, subset_Int_iff]) 3); 

479 
by (REPEAT (eresolve_tac [asm_rl, ltE] 1)); 

480 
val Int_greatest_lt = result(); 

0  481 

482 
(*** Results about limits ***) 

483 

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

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

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

487 
val Ord_Union = result(); 

488 

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

490 
by (rtac Ord_Union 1); 

491 
by (etac RepFunE 1); 

492 
by (etac ssubst 1); 

493 
by (eresolve_tac prems 1); 

494 
val Ord_UN = result(); 

495 

30  496 
(* No < version; consider (UN i:nat.i)=nat *) 
0  497 
val [ordi,limit] = goal Ord.thy 
30  498 
"[ Ord(i); !!x. x:A ==> b(x) le i ] ==> (UN x:A. b(x)) le i"; 
499 
by (rtac (le_imp_subset RS UN_least RS subset_imp_le) 1); 

500 
by (REPEAT (ares_tac [ordi, Ord_UN, limit] 1 ORELSE etac (limit RS ltE) 1)); 

501 
val UN_least_le = result(); 

0  502 

30  503 
val [jlti,limit] = goal Ord.thy 
504 
"[ j<i; !!x. x:A ==> b(x)<j ] ==> (UN x:A. succ(b(x))) < i"; 

505 
by (rtac (jlti RS ltE) 1); 

506 
by (rtac (UN_least_le RS lt_trans2) 1); 

507 
by (REPEAT (ares_tac [jlti, succ_leI, limit] 1)); 

508 
val UN_succ_least_lt = result(); 

509 

510 
val prems = goal Ord.thy 

511 
"[ a: A; i le b(a); !!x. x:A ==> Ord(b(x)) ] ==> i le (UN x:A. b(x))"; 

512 
by (resolve_tac (prems RL [ltE]) 1); 

513 
by (rtac (le_imp_subset RS subset_trans RS subset_imp_le) 1); 

514 
by (REPEAT (ares_tac (prems @ [UN_upper, Ord_UN]) 1)); 

515 
val UN_upper_le = result(); 

0  516 

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

30  518 
by (fast_tac (eq_cs addEs [Ord_trans]) 1); 
0  519 
val Ord_equality = result(); 
520 

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

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

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

524 
val Ord_Union_subset = result(); 