author  paulson 
Wed, 05 Jun 2002 15:34:55 +0200  
changeset 13203  fac77a839aa2 
parent 13185  da61bfa0a391 
child 13217  bc5dc2392578 
permissions  rwrr 
1478  1 
(* Title: ZF/epsilon.thy 
0  2 
ID: $Id$ 
1478  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1993 University of Cambridge 
5 

6 
Epsilon induction and recursion 

7 
*) 

8 

13164  9 
theory Epsilon = Nat + mono: 
10 

2469  11 
constdefs 
13164  12 
eclose :: "i=>i" 
2469  13 
"eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))" 
0  14 

13164  15 
transrec :: "[i, [i,i]=>i] =>i" 
2469  16 
"transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)" 
17 

13164  18 
rank :: "i=>i" 
2469  19 
"rank(a) == transrec(a, %x f. UN y:x. succ(f`y))" 
20 

13164  21 
transrec2 :: "[i, i, [i,i]=>i] =>i" 
2469  22 
"transrec2(k, a, b) == 
23 
transrec(k, 

24 
%i r. if(i=0, a, 

25 
if(EX j. i=succ(j), 

26 
b(THE j. i=succ(j), r`(THE j. i=succ(j))), 

27 
UN j<i. r`j)))" 

28 

13164  29 
recursor :: "[i, [i,i]=>i, i]=>i" 
30 
"recursor(a,b,k) == transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))" 

31 

32 
rec :: "[i, i, [i,i]=>i]=>i" 

33 
"rec(k,a,b) == recursor(a,b,k)" 

34 

35 

36 
(*** Basic closure properties ***) 

37 

38 
lemma arg_subset_eclose: "A <= eclose(A)" 

39 
apply (unfold eclose_def) 

40 
apply (rule nat_rec_0 [THEN equalityD2, THEN subset_trans]) 

41 
apply (rule nat_0I [THEN UN_upper]) 

42 
done 

43 

44 
lemmas arg_into_eclose = arg_subset_eclose [THEN subsetD, standard] 

45 

46 
lemma Transset_eclose: "Transset(eclose(A))" 

47 
apply (unfold eclose_def Transset_def) 

48 
apply (rule subsetI [THEN ballI]) 

49 
apply (erule UN_E) 

50 
apply (rule nat_succI [THEN UN_I], assumption) 

51 
apply (erule nat_rec_succ [THEN ssubst]) 

52 
apply (erule UnionI, assumption) 

53 
done 

54 

55 
(* x : eclose(A) ==> x <= eclose(A) *) 

56 
lemmas eclose_subset = 

57 
Transset_eclose [unfolded Transset_def, THEN bspec, standard] 

58 

59 
(* [ A : eclose(B); c : A ] ==> c : eclose(B) *) 

60 
lemmas ecloseD = eclose_subset [THEN subsetD, standard] 

61 

62 
lemmas arg_in_eclose_sing = arg_subset_eclose [THEN singleton_subsetD] 

63 
lemmas arg_into_eclose_sing = arg_in_eclose_sing [THEN ecloseD, standard] 

64 

65 
(* This is epsiloninduction for eclose(A); see also eclose_induct_down... 

66 
[ a: eclose(A); !!x. [ x: eclose(A); ALL y:x. P(y) ] ==> P(x) 

67 
] ==> P(a) 

68 
*) 

13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset

69 
lemmas eclose_induct = 
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset

70 
Transset_induct [OF _ Transset_eclose, induct set: eclose] 
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset

71 

13164  72 

73 
(*Epsilon induction*) 

74 
lemma eps_induct: 

75 
"[ !!x. ALL y:x. P(y) ==> P(x) ] ==> P(a)" 

76 
by (rule arg_in_eclose_sing [THEN eclose_induct], blast) 

77 

78 

79 
(*** Leastness of eclose ***) 

80 

81 
(** eclose(A) is the least transitive set including A as a subset. **) 

82 

83 
lemma eclose_least_lemma: 

84 
"[ Transset(X); A<=X; n: nat ] ==> nat_rec(n, A, %m r. Union(r)) <= X" 

85 
apply (unfold Transset_def) 

86 
apply (erule nat_induct) 

87 
apply (simp add: nat_rec_0) 

88 
apply (simp add: nat_rec_succ, blast) 

89 
done 

90 

91 
lemma eclose_least: 

92 
"[ Transset(X); A<=X ] ==> eclose(A) <= X" 

93 
apply (unfold eclose_def) 

94 
apply (rule eclose_least_lemma [THEN UN_least], assumption+) 

95 
done 

96 

97 
(*COMPLETELY DIFFERENT induction principle from eclose_induct!!*) 

98 
lemma eclose_induct_down: 

99 
"[ a: eclose(b); 

100 
!!y. [ y: b ] ==> P(y); 

101 
!!y z. [ y: eclose(b); P(y); z: y ] ==> P(z) 

102 
] ==> P(a)" 

103 
apply (rule eclose_least [THEN subsetD, THEN CollectD2, of "eclose(b)"]) 

104 
prefer 3 apply assumption 

105 
apply (unfold Transset_def) 

106 
apply (blast intro: ecloseD) 

107 
apply (blast intro: arg_subset_eclose [THEN subsetD]) 

108 
done 

109 

13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset

110 
(*fixed up for induct method*) 
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset

111 
lemmas eclose_induct_down = eclose_induct_down [consumes 1] 
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset

112 

13164  113 
lemma Transset_eclose_eq_arg: "Transset(X) ==> eclose(X) = X" 
114 
apply (erule equalityI [OF eclose_least arg_subset_eclose]) 

115 
apply (rule subset_refl) 

116 
done 

117 

118 

119 
(*** Epsilon recursion ***) 

120 

121 
(*Unused...*) 

122 
lemma mem_eclose_trans: "[ A: eclose(B); B: eclose(C) ] ==> A: eclose(C)" 

123 
by (rule eclose_least [OF Transset_eclose eclose_subset, THEN subsetD], 

124 
assumption+) 

125 

126 
(*Variant of the previous lemma in a useable form for the sequel*) 

127 
lemma mem_eclose_sing_trans: 

128 
"[ A: eclose({B}); B: eclose({C}) ] ==> A: eclose({C})" 

129 
by (rule eclose_least [OF Transset_eclose singleton_subsetI, THEN subsetD], 

130 
assumption+) 

131 

132 
lemma under_Memrel: "[ Transset(i); j:i ] ==> Memrel(i)``{j} = j" 

133 
by (unfold Transset_def, blast) 

134 

135 
(* j : eclose(A) ==> Memrel(eclose(A)) `` j = j *) 

136 
lemmas under_Memrel_eclose = Transset_eclose [THEN under_Memrel, standard] 

137 

138 
lemmas wfrec_ssubst = wf_Memrel [THEN wfrec, THEN ssubst] 

139 

140 
lemma wfrec_eclose_eq: 

141 
"[ k:eclose({j}); j:eclose({i}) ] ==> 

142 
wfrec(Memrel(eclose({i})), k, H) = wfrec(Memrel(eclose({j})), k, H)" 

143 
apply (erule eclose_induct) 

144 
apply (rule wfrec_ssubst) 

145 
apply (rule wfrec_ssubst) 

146 
apply (simp add: under_Memrel_eclose mem_eclose_sing_trans [of _ j i]) 

147 
done 

148 

149 
lemma wfrec_eclose_eq2: 

150 
"k: i ==> wfrec(Memrel(eclose({i})),k,H) = wfrec(Memrel(eclose({k})),k,H)" 

151 
apply (rule arg_in_eclose_sing [THEN wfrec_eclose_eq]) 

152 
apply (erule arg_into_eclose_sing) 

153 
done 

154 

155 
lemma transrec: "transrec(a,H) = H(a, lam x:a. transrec(x,H))" 

156 
apply (unfold transrec_def) 

157 
apply (rule wfrec_ssubst) 

158 
apply (simp add: wfrec_eclose_eq2 arg_in_eclose_sing under_Memrel_eclose) 

159 
done 

160 

161 
(*Avoids explosions in proofs; resolve it with a metalevel definition.*) 

162 
lemma def_transrec: 

163 
"[ !!x. f(x)==transrec(x,H) ] ==> f(a) = H(a, lam x:a. f(x))" 

164 
apply simp 

165 
apply (rule transrec) 

166 
done 

167 

168 
lemma transrec_type: 

169 
"[ !!x u. [ x:eclose({a}); u: Pi(x,B) ] ==> H(x,u) : B(x) ] 

170 
==> transrec(a,H) : B(a)" 

171 
apply (rule_tac i = "a" in arg_in_eclose_sing [THEN eclose_induct]) 

172 
apply (subst transrec) 

173 
apply (simp add: lam_type) 

174 
done 

175 

176 
lemma eclose_sing_Ord: "Ord(i) ==> eclose({i}) <= succ(i)" 

177 
apply (erule Ord_is_Transset [THEN Transset_succ, THEN eclose_least]) 

178 
apply (rule succI1 [THEN singleton_subsetI]) 

179 
done 

180 

181 
lemma Ord_transrec_type: 

182 
assumes jini: "j: i" 

183 
and ordi: "Ord(i)" 

184 
and minor: " !!x u. [ x: i; u: Pi(x,B) ] ==> H(x,u) : B(x)" 

185 
shows "transrec(j,H) : B(j)" 

186 
apply (rule transrec_type) 

187 
apply (insert jini ordi) 

188 
apply (blast intro!: minor 

189 
intro: Ord_trans 

190 
dest: Ord_in_Ord [THEN eclose_sing_Ord, THEN subsetD]) 

191 
done 

192 

193 
(*** Rank ***) 

194 

195 
(*NOT SUITABLE FOR REWRITING  RECURSIVE!*) 

196 
lemma rank: "rank(a) = (UN y:a. succ(rank(y)))" 

197 
by (subst rank_def [THEN def_transrec], simp) 

198 

199 
lemma Ord_rank [simp]: "Ord(rank(a))" 

200 
apply (rule_tac a="a" in eps_induct) 

201 
apply (subst rank) 

202 
apply (rule Ord_succ [THEN Ord_UN]) 

203 
apply (erule bspec, assumption) 

204 
done 

205 

206 
lemma rank_of_Ord: "Ord(i) ==> rank(i) = i" 

207 
apply (erule trans_induct) 

208 
apply (subst rank) 

209 
apply (simp add: Ord_equality) 

210 
done 

211 

212 
lemma rank_lt: "a:b ==> rank(a) < rank(b)" 

213 
apply (rule_tac a1 = "b" in rank [THEN ssubst]) 

214 
apply (erule UN_I [THEN ltI]) 

215 
apply (rule_tac [2] Ord_UN, auto) 

216 
done 

217 

218 
lemma eclose_rank_lt: "a: eclose(b) ==> rank(a) < rank(b)" 

219 
apply (erule eclose_induct_down) 

220 
apply (erule rank_lt) 

221 
apply (erule rank_lt [THEN lt_trans], assumption) 

222 
done 

6070  223 

13164  224 
lemma rank_mono: "a<=b ==> rank(a) le rank(b)" 
225 
apply (rule subset_imp_le) 

226 
apply (subst rank) 

227 
apply (subst rank, auto) 

228 
done 

229 

230 
lemma rank_Pow: "rank(Pow(a)) = succ(rank(a))" 

231 
apply (rule rank [THEN trans]) 

232 
apply (rule le_anti_sym) 

233 
apply (rule_tac [2] UN_upper_le) 

234 
apply (rule UN_least_le) 

235 
apply (auto intro: rank_mono simp add: Ord_UN) 

236 
done 

237 

238 
lemma rank_0 [simp]: "rank(0) = 0" 

239 
by (rule rank [THEN trans], blast) 

240 

241 
lemma rank_succ [simp]: "rank(succ(x)) = succ(rank(x))" 

242 
apply (rule rank [THEN trans]) 

243 
apply (rule equalityI [OF UN_least succI1 [THEN UN_upper]]) 

244 
apply (erule succE, blast) 

245 
apply (erule rank_lt [THEN leI, THEN succ_leI, THEN le_imp_subset]) 

246 
done 

247 

248 
lemma rank_Union: "rank(Union(A)) = (UN x:A. rank(x))" 

249 
apply (rule equalityI) 

250 
apply (rule_tac [2] rank_mono [THEN le_imp_subset, THEN UN_least]) 

251 
apply (erule_tac [2] Union_upper) 

252 
apply (subst rank) 

253 
apply (rule UN_least) 

254 
apply (erule UnionE) 

255 
apply (rule subset_trans) 

256 
apply (erule_tac [2] RepFunI [THEN Union_upper]) 

257 
apply (erule rank_lt [THEN succ_leI, THEN le_imp_subset]) 

258 
done 

259 

260 
lemma rank_eclose: "rank(eclose(a)) = rank(a)" 

261 
apply (rule le_anti_sym) 

262 
apply (rule_tac [2] arg_subset_eclose [THEN rank_mono]) 

263 
apply (rule_tac a1 = "eclose (a) " in rank [THEN ssubst]) 

264 
apply (rule Ord_rank [THEN UN_least_le]) 

265 
apply (erule eclose_rank_lt [THEN succ_leI]) 

266 
done 

267 

268 
lemma rank_pair1: "rank(a) < rank(<a,b>)" 

269 
apply (unfold Pair_def) 

270 
apply (rule consI1 [THEN rank_lt, THEN lt_trans]) 

271 
apply (rule consI1 [THEN consI2, THEN rank_lt]) 

272 
done 

273 

274 
lemma rank_pair2: "rank(b) < rank(<a,b>)" 

275 
apply (unfold Pair_def) 

276 
apply (rule consI1 [THEN consI2, THEN rank_lt, THEN lt_trans]) 

277 
apply (rule consI1 [THEN consI2, THEN rank_lt]) 

278 
done 

279 

280 
(*Not clear how to remove the P(a) condition, since the "then" part 

281 
must refer to "a"*) 

282 
lemma the_equality_if: 

283 
"P(a) ==> (THE x. P(x)) = (if (EX!x. P(x)) then a else 0)" 

284 
by (simp add: the_0 the_equality2) 

285 

13175
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13164
diff
changeset

286 
(*The first premise not only fixs i but ensures f~=0. 
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13164
diff
changeset

287 
The second premise is now essential. Consider otherwise the relation 
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13164
diff
changeset

288 
r = {<0,0>,<0,1>,<0,2>,...}. Then f`0 = Union(f``{0}) = Union(nat) = nat, 
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13164
diff
changeset

289 
whose rank equals that of r.*) 
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13164
diff
changeset

290 
lemma rank_apply: "[i : domain(f); function(f)] ==> rank(f`i) < rank(f)" 
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13164
diff
changeset

291 
apply (clarify ); 
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13164
diff
changeset

292 
apply (simp add: function_apply_equality); 
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13164
diff
changeset

293 
apply (blast intro: lt_trans rank_lt rank_pair2) 
13164  294 
done 
295 

296 

297 
(*** Corollaries of leastness ***) 

298 

299 
lemma mem_eclose_subset: "A:B ==> eclose(A)<=eclose(B)" 

300 
apply (rule Transset_eclose [THEN eclose_least]) 

301 
apply (erule arg_into_eclose [THEN eclose_subset]) 

302 
done 

303 

304 
lemma eclose_mono: "A<=B ==> eclose(A) <= eclose(B)" 

305 
apply (rule Transset_eclose [THEN eclose_least]) 

306 
apply (erule subset_trans) 

307 
apply (rule arg_subset_eclose) 

308 
done 

309 

310 
(** Idempotence of eclose **) 

311 

312 
lemma eclose_idem: "eclose(eclose(A)) = eclose(A)" 

313 
apply (rule equalityI) 

314 
apply (rule eclose_least [OF Transset_eclose subset_refl]) 

315 
apply (rule arg_subset_eclose) 

316 
done 

317 

318 
(** Transfinite recursion for definitions based on the 

319 
three cases of ordinals **) 

320 

321 
lemma transrec2_0 [simp]: "transrec2(0,a,b) = a" 

322 
by (rule transrec2_def [THEN def_transrec, THEN trans], simp) 

323 

324 
lemma transrec2_succ [simp]: "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))" 

325 
apply (rule transrec2_def [THEN def_transrec, THEN trans]) 

326 
apply (simp add: the_equality if_P) 

327 
done 

328 

329 
lemma transrec2_Limit: 

330 
"Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))" 

13175
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13164
diff
changeset

331 
apply (rule transrec2_def [THEN def_transrec, THEN trans]) 
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13164
diff
changeset

332 
apply (auto simp add: OUnion_def); 
13164  333 
done 
334 

13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset

335 
lemma def_transrec2: 
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset

336 
"(!!x. f(x)==transrec2(x,a,b)) 
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset

337 
==> f(0) = a & 
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset

338 
f(succ(i)) = b(i, f(i)) & 
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset

339 
(Limit(K) > f(K) = (UN j<K. f(j)))" 
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset

340 
by (simp add: transrec2_Limit) 
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset

341 

13164  342 

343 
(** recursor  better than nat_rec; the succ case has no type requirement! **) 

344 

345 
(*NOT suitable for rewriting*) 

346 
lemmas recursor_lemma = recursor_def [THEN def_transrec, THEN trans] 

347 

348 
lemma recursor_0: "recursor(a,b,0) = a" 

349 
by (rule nat_case_0 [THEN recursor_lemma]) 

350 

351 
lemma recursor_succ: "recursor(a,b,succ(m)) = b(m, recursor(a,b,m))" 

352 
by (rule recursor_lemma, simp) 

353 

354 

355 
(** rec: old version for compatibility **) 

356 

357 
lemma rec_0 [simp]: "rec(0,a,b) = a" 

358 
apply (unfold rec_def) 

359 
apply (rule recursor_0) 

360 
done 

361 

362 
lemma rec_succ [simp]: "rec(succ(m),a,b) = b(m, rec(m,a,b))" 

363 
apply (unfold rec_def) 

364 
apply (rule recursor_succ) 

365 
done 

366 

367 
lemma rec_type: 

368 
"[ n: nat; 

369 
a: C(0); 

370 
!!m z. [ m: nat; z: C(m) ] ==> b(m,z): C(succ(m)) ] 

371 
==> rec(n,a,b) : C(n)" 

13185  372 
by (erule nat_induct, auto) 
13164  373 

374 
ML 

375 
{* 

376 
val arg_subset_eclose = thm "arg_subset_eclose"; 

377 
val arg_into_eclose = thm "arg_into_eclose"; 

378 
val Transset_eclose = thm "Transset_eclose"; 

379 
val eclose_subset = thm "eclose_subset"; 

380 
val ecloseD = thm "ecloseD"; 

381 
val arg_in_eclose_sing = thm "arg_in_eclose_sing"; 

382 
val arg_into_eclose_sing = thm "arg_into_eclose_sing"; 

383 
val eclose_induct = thm "eclose_induct"; 

384 
val eps_induct = thm "eps_induct"; 

385 
val eclose_least = thm "eclose_least"; 

386 
val eclose_induct_down = thm "eclose_induct_down"; 

387 
val Transset_eclose_eq_arg = thm "Transset_eclose_eq_arg"; 

388 
val mem_eclose_trans = thm "mem_eclose_trans"; 

389 
val mem_eclose_sing_trans = thm "mem_eclose_sing_trans"; 

390 
val under_Memrel = thm "under_Memrel"; 

391 
val under_Memrel_eclose = thm "under_Memrel_eclose"; 

392 
val wfrec_ssubst = thm "wfrec_ssubst"; 

393 
val wfrec_eclose_eq = thm "wfrec_eclose_eq"; 

394 
val wfrec_eclose_eq2 = thm "wfrec_eclose_eq2"; 

395 
val transrec = thm "transrec"; 

396 
val def_transrec = thm "def_transrec"; 

397 
val transrec_type = thm "transrec_type"; 

398 
val eclose_sing_Ord = thm "eclose_sing_Ord"; 

399 
val Ord_transrec_type = thm "Ord_transrec_type"; 

400 
val rank = thm "rank"; 

401 
val Ord_rank = thm "Ord_rank"; 

402 
val rank_of_Ord = thm "rank_of_Ord"; 

403 
val rank_lt = thm "rank_lt"; 

404 
val eclose_rank_lt = thm "eclose_rank_lt"; 

405 
val rank_mono = thm "rank_mono"; 

406 
val rank_Pow = thm "rank_Pow"; 

407 
val rank_0 = thm "rank_0"; 

408 
val rank_succ = thm "rank_succ"; 

409 
val rank_Union = thm "rank_Union"; 

410 
val rank_eclose = thm "rank_eclose"; 

411 
val rank_pair1 = thm "rank_pair1"; 

412 
val rank_pair2 = thm "rank_pair2"; 

413 
val the_equality_if = thm "the_equality_if"; 

414 
val rank_apply = thm "rank_apply"; 

415 
val mem_eclose_subset = thm "mem_eclose_subset"; 

416 
val eclose_mono = thm "eclose_mono"; 

417 
val eclose_idem = thm "eclose_idem"; 

418 
val transrec2_0 = thm "transrec2_0"; 

419 
val transrec2_succ = thm "transrec2_succ"; 

420 
val transrec2_Limit = thm "transrec2_Limit"; 

421 
val recursor_0 = thm "recursor_0"; 

422 
val recursor_succ = thm "recursor_succ"; 

423 
val rec_0 = thm "rec_0"; 

424 
val rec_succ = thm "rec_succ"; 

425 
val rec_type = thm "rec_type"; 

426 
*} 

6070  427 

0  428 
end 