author  lcp 
Thu, 07 Oct 1993 10:48:16 +0100  
changeset 37  cebe01deba80 
parent 30  d49df4181f0d 
child 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 

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

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

163 
by (rtac Ord_is_Transset 1); 

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

165 
ORELSE etac InterD 1)); 

166 
val Ord_Inter = result(); 

167 

168 
val jmemA::prems = goal Ord.thy 

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

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

171 
by (etac RepFunE 1); 

172 
by (etac ssubst 1); 

173 
by (eresolve_tac prems 1); 

174 
val Ord_INT = result(); 

175 

176 

30  177 
(*** < is 'less than' for ordinals ***) 
178 

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

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

181 
val ltI = result(); 

182 

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

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

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

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

187 
val ltE = result(); 

188 

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

190 
by (etac ltE 1); 

191 
by (assume_tac 1); 

192 
val ltD = result(); 

193 

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

195 
by (fast_tac ZF_cs 1); 

196 
val not_lt0 = result(); 

197 

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

199 
val lt0E = standard (not_lt0 RS notE); 

200 

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

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

203 
val lt_trans = result(); 

204 

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

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

207 
val lt_anti_sym = result(); 

208 

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

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

211 

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

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

214 

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

216 

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

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

219 
val le_iff = result(); 

220 

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

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

223 
val leI = result(); 

224 

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

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

227 
val le_eqI = result(); 

228 

229 
val le_refl = refl RS le_eqI; 

230 

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

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

233 
by (etac prem 1); 

234 
val leCI = result(); 

235 

236 
val major::prems = goal Ord.thy 

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

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

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

240 
val leE = result(); 

241 

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

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

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

245 
val le_asym = result(); 

246 

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

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

249 
val le0_iff = result(); 

250 

251 
val le0D = standard (le0_iff RS iffD1); 

252 

253 
val lt_cs = 

254 
ZF_cs addSIs [le_refl, leCI] 

255 
addSDs [le0D] 

256 
addSEs [lt_anti_refl, lt0E, leE]; 

257 

258 

0  259 
(*** Natural Deduction rules for Memrel ***) 
260 

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

262 
by (fast_tac ZF_cs 1); 

263 
val Memrel_iff = result(); 

264 

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

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

267 
val MemrelI = result(); 

268 

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

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

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

272 
\ ] ==> P"; 

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

274 
by (etac conjE 1); 

275 
by (rtac minor 1); 

276 
by (REPEAT (assume_tac 1)); 

277 
val MemrelE = result(); 

278 

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

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

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

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

283 
etac disjI1, 

284 
etac bexE, 

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

286 
etac MemrelE, 

287 
etac bspec, 

288 
REPEAT o assume_tac]); 

289 
val wf_Memrel = result(); 

290 

291 
(*** Transfinite induction ***) 

292 

293 
(*Epsilon induction over a transitive set*) 

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

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

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

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

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

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

300 
by (resolve_tac prems 1); 

301 
by (assume_tac 1); 

302 
by (cut_facts_tac prems 1); 

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

304 
val Transset_induct = result(); 

305 

306 
(*Induction over an ordinal*) 

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

308 

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

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

311 
"[ Ord(i); \ 

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

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

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

315 
by (rtac indhyp 1); 

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

317 
by (REPEAT (assume_tac 1)); 

318 
val trans_induct = result(); 

319 

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

321 
fun trans_ind_tac a prems i = 

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

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

324 
ares_tac prems i]; 

325 

326 

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

328 

329 
(*Finds contradictions for the following proof*) 

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

331 

30  332 
(** Proving that < is a linear ordering on the ordinals **) 
0  333 

334 
val prems = goal Ord.thy 

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

336 
by (trans_ind_tac "i" prems 1); 

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

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

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

340 
ORELSE ball_tac 1 

341 
ORELSE eresolve_tac [impE,disjE,allE] 1 

342 
ORELSE hyp_subst_tac 1 

343 
ORELSE Ord_trans_tac 1)); 

344 
val Ord_linear_lemma = result(); 

345 

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

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

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

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

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

352 
val Ord_linear_lt = result(); 

0  353 

354 
val prems = goal Ord.thy 

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

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

358 
val Ord_linear_le = result(); 

359 

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

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

362 
val le_imp_not_lt = result(); 

0  363 

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

366 
by (REPEAT (SOMEGOAL assume_tac)); 

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

368 
val not_lt_imp_le = result(); 

0  369 

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

372 
val not_lt_iff_le = result(); 

0  373 

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

376 
val not_le_iff_lt = result(); 

377 

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

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

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

381 
val Ord_0_le = result(); 

0  382 

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

386 
by (fast_tac lt_cs 1); 

387 
val Ord_0_lt = result(); 

0  388 

30  389 
(*** Results about lessthan or equals ***) 
390 

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

0  392 

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

395 
by (assume_tac 1); 

396 
by (assume_tac 1); 

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

398 
val subset_imp_le = result(); 

0  399 

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

402 
by (fast_tac ZF_cs 2); 

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

404 
val le_imp_subset = result(); 

0  405 

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

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

409 
val le_subset_iff = result(); 

410 

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

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

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

414 
val le_succ_iff = result(); 

0  415 

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

418 
val lt_trans1 = result(); 

0  419 

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

422 
val lt_trans2 = result(); 

423 

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

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

426 
val le_trans = result(); 

0  427 

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

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

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

432 
val succ_leI = result(); 

0  433 

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

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

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

438 
val succ_leE = result(); 

0  439 

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

442 
val succ_le_iff = result(); 

0  443 

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

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

445 

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

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

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

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

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

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

453 
val Un_least_lt = result(); 

0  454 

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

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

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

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

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

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

462 
val Int_greatest_lt = result(); 

0  463 

464 
(*** Results about limits ***) 

465 

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

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

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

469 
val Ord_Union = result(); 

470 

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

472 
by (rtac Ord_Union 1); 

473 
by (etac RepFunE 1); 

474 
by (etac ssubst 1); 

475 
by (eresolve_tac prems 1); 

476 
val Ord_UN = result(); 

477 

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

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

483 
val UN_least_le = result(); 

0  484 

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

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

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

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

490 
val UN_succ_least_lt = result(); 

491 

492 
val prems = goal Ord.thy 

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

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

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

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

497 
val UN_upper_le = result(); 

0  498 

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

30  500 
by (fast_tac (eq_cs addEs [Ord_trans]) 1); 
0  501 
val Ord_equality = result(); 
502 

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

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

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

506 
val Ord_Union_subset = result(); 