author  paulson 
Thu, 15 Mar 2012 16:35:02 +0000  
changeset 46953  2b6e55924af3 
parent 46820  c656222c4dc1 
child 58860  fee7cfa69c50 
permissions  rwrr 
35762  1 
(* Title: ZF/Epsilon.thy 
1478  2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  3 
Copyright 1993 University of Cambridge 
4 
*) 

5 

13328  6 
header{*Epsilon Induction and Recursion*} 
7 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
24893
diff
changeset

8 
theory Epsilon imports Nat_ZF begin 
13164  9 

24893  10 
definition 
11 
eclose :: "i=>i" where 

46820  12 
"eclose(A) == \<Union>n\<in>nat. nat_rec(n, A, %m r. \<Union>(r))" 
0  13 

24893  14 
definition 
15 
transrec :: "[i, [i,i]=>i] =>i" where 

2469  16 
"transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)" 
46820  17 

24893  18 
definition 
19 
rank :: "i=>i" where 

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13524
diff
changeset

20 
"rank(a) == transrec(a, %x f. \<Union>y\<in>x. succ(f`y))" 
2469  21 

24893  22 
definition 
23 
transrec2 :: "[i, i, [i,i]=>i] =>i" where 

46820  24 
"transrec2(k, a, b) == 
25 
transrec(k, 

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

27 
if(\<exists>j. i=succ(j), 

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

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13524
diff
changeset

29 
\<Union>j<i. r`j)))" 
2469  30 

24893  31 
definition 
32 
recursor :: "[i, [i,i]=>i, i]=>i" where 

13164  33 
"recursor(a,b,k) == transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))" 
34 

24893  35 
definition 
36 
rec :: "[i, i, [i,i]=>i]=>i" where 

13164  37 
"rec(k,a,b) == recursor(a,b,k)" 
38 

39 

13356  40 
subsection{*Basic Closure Properties*} 
13164  41 

46820  42 
lemma arg_subset_eclose: "A \<subseteq> eclose(A)" 
13164  43 
apply (unfold eclose_def) 
44 
apply (rule nat_rec_0 [THEN equalityD2, THEN subset_trans]) 

45 
apply (rule nat_0I [THEN UN_upper]) 

46 
done 

47 

45602  48 
lemmas arg_into_eclose = arg_subset_eclose [THEN subsetD] 
13164  49 

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

51 
apply (unfold eclose_def Transset_def) 

52 
apply (rule subsetI [THEN ballI]) 

53 
apply (erule UN_E) 

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

55 
apply (erule nat_rec_succ [THEN ssubst]) 

56 
apply (erule UnionI, assumption) 

57 
done 

58 

46820  59 
(* @{term"x \<in> eclose(A) ==> x \<subseteq> eclose(A)"} *) 
60 
lemmas eclose_subset = 

45602  61 
Transset_eclose [unfolded Transset_def, THEN bspec] 
13164  62 

46820  63 
(* @{term"[ A \<in> eclose(B); c \<in> A ] ==> c \<in> eclose(B)"} *) 
45602  64 
lemmas ecloseD = eclose_subset [THEN subsetD] 
13164  65 

66 
lemmas arg_in_eclose_sing = arg_subset_eclose [THEN singleton_subsetD] 

45602  67 
lemmas arg_into_eclose_sing = arg_in_eclose_sing [THEN ecloseD] 
13164  68 

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

46953  70 
[ a \<in> eclose(A); !!x. [ x \<in> eclose(A); \<forall>y\<in>x. P(y) ] ==> P(x) 
46820  71 
] ==> P(a) 
13164  72 
*) 
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset

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

74 
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

75 

13164  76 

77 
(*Epsilon induction*) 

78 
lemma eps_induct: 

46820  79 
"[ !!x. \<forall>y\<in>x. P(y) ==> P(x) ] ==> P(a)" 
80 
by (rule arg_in_eclose_sing [THEN eclose_induct], blast) 

13164  81 

82 

13356  83 
subsection{*Leastness of @{term eclose}*} 
13164  84 

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

86 

46820  87 
lemma eclose_least_lemma: 
46953  88 
"[ Transset(X); A<=X; n \<in> nat ] ==> nat_rec(n, A, %m r. \<Union>(r)) \<subseteq> X" 
13164  89 
apply (unfold Transset_def) 
46820  90 
apply (erule nat_induct) 
13164  91 
apply (simp add: nat_rec_0) 
92 
apply (simp add: nat_rec_succ, blast) 

93 
done 

94 

46820  95 
lemma eclose_least: 
96 
"[ Transset(X); A<=X ] ==> eclose(A) \<subseteq> X" 

13164  97 
apply (unfold eclose_def) 
98 
apply (rule eclose_least_lemma [THEN UN_least], assumption+) 

99 
done 

100 

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

13524  102 
lemma eclose_induct_down [consumes 1]: 
46953  103 
"[ a \<in> eclose(b); 
104 
!!y. [ y \<in> b ] ==> P(y); 

105 
!!y z. [ y \<in> eclose(b); P(y); z \<in> y ] ==> P(z) 

13164  106 
] ==> P(a)" 
107 
apply (rule eclose_least [THEN subsetD, THEN CollectD2, of "eclose(b)"]) 

108 
prefer 3 apply assumption 

46820  109 
apply (unfold Transset_def) 
13164  110 
apply (blast intro: ecloseD) 
111 
apply (blast intro: arg_subset_eclose [THEN subsetD]) 

112 
done 

113 

114 
lemma Transset_eclose_eq_arg: "Transset(X) ==> eclose(X) = X" 

115 
apply (erule equalityI [OF eclose_least arg_subset_eclose]) 

116 
apply (rule subset_refl) 

117 
done 

118 

13387  119 
text{*A transitive set either is empty or contains the empty set.*} 
46820  120 
lemma Transset_0_lemma [rule_format]: "Transset(A) ==> x\<in>A \<longrightarrow> 0\<in>A"; 
121 
apply (simp add: Transset_def) 

122 
apply (rule_tac a=x in eps_induct, clarify) 

123 
apply (drule bspec, assumption) 

14153  124 
apply (case_tac "x=0", auto) 
13387  125 
done 
126 

127 
lemma Transset_0_disj: "Transset(A) ==> A=0  0\<in>A"; 

128 
by (blast dest: Transset_0_lemma) 

129 

13164  130 

13356  131 
subsection{*Epsilon Recursion*} 
13164  132 

133 
(*Unused...*) 

46953  134 
lemma mem_eclose_trans: "[ A \<in> eclose(B); B \<in> eclose(C) ] ==> A \<in> eclose(C)" 
46820  135 
by (rule eclose_least [OF Transset_eclose eclose_subset, THEN subsetD], 
13164  136 
assumption+) 
137 

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

139 
lemma mem_eclose_sing_trans: 

46953  140 
"[ A \<in> eclose({B}); B \<in> eclose({C}) ] ==> A \<in> eclose({C})" 
46820  141 
by (rule eclose_least [OF Transset_eclose singleton_subsetI, THEN subsetD], 
13164  142 
assumption+) 
143 

46953  144 
lemma under_Memrel: "[ Transset(i); j \<in> i ] ==> Memrel(i)``{j} = j" 
13164  145 
by (unfold Transset_def, blast) 
146 

13217  147 
lemma lt_Memrel: "j < i ==> Memrel(i) `` {j} = j" 
46820  148 
by (simp add: lt_def Ord_def under_Memrel) 
13217  149 

46820  150 
(* @{term"j \<in> eclose(A) ==> Memrel(eclose(A)) `` j = j"} *) 
45602  151 
lemmas under_Memrel_eclose = Transset_eclose [THEN under_Memrel] 
13164  152 

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

154 

155 
lemma wfrec_eclose_eq: 

46953  156 
"[ k \<in> eclose({j}); j \<in> eclose({i}) ] ==> 
13164  157 
wfrec(Memrel(eclose({i})), k, H) = wfrec(Memrel(eclose({j})), k, H)" 
158 
apply (erule eclose_induct) 

159 
apply (rule wfrec_ssubst) 

160 
apply (rule wfrec_ssubst) 

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

162 
done 

163 

46820  164 
lemma wfrec_eclose_eq2: 
46953  165 
"k \<in> i ==> wfrec(Memrel(eclose({i})),k,H) = wfrec(Memrel(eclose({k})),k,H)" 
13164  166 
apply (rule arg_in_eclose_sing [THEN wfrec_eclose_eq]) 
167 
apply (erule arg_into_eclose_sing) 

168 
done 

169 

46820  170 
lemma transrec: "transrec(a,H) = H(a, \<lambda>x\<in>a. transrec(x,H))" 
13164  171 
apply (unfold transrec_def) 
172 
apply (rule wfrec_ssubst) 

173 
apply (simp add: wfrec_eclose_eq2 arg_in_eclose_sing under_Memrel_eclose) 

174 
done 

175 

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

177 
lemma def_transrec: 

46820  178 
"[ !!x. f(x)==transrec(x,H) ] ==> f(a) = H(a, \<lambda>x\<in>a. f(x))" 
13164  179 
apply simp 
180 
apply (rule transrec) 

181 
done 

182 

183 
lemma transrec_type: 

46953  184 
"[ !!x u. [ x \<in> eclose({a}); u \<in> Pi(x,B) ] ==> H(x,u) \<in> B(x) ] 
46820  185 
==> transrec(a,H) \<in> B(a)" 
13784  186 
apply (rule_tac i = a in arg_in_eclose_sing [THEN eclose_induct]) 
13164  187 
apply (subst transrec) 
46820  188 
apply (simp add: lam_type) 
13164  189 
done 
190 

46820  191 
lemma eclose_sing_Ord: "Ord(i) ==> eclose({i}) \<subseteq> succ(i)" 
13164  192 
apply (erule Ord_is_Transset [THEN Transset_succ, THEN eclose_least]) 
193 
apply (rule succI1 [THEN singleton_subsetI]) 

194 
done 

195 

46820  196 
lemma succ_subset_eclose_sing: "succ(i) \<subseteq> eclose({i})" 
197 
apply (insert arg_subset_eclose [of "{i}"], simp) 

198 
apply (frule eclose_subset, blast) 

13269  199 
done 
200 

201 
lemma eclose_sing_Ord_eq: "Ord(i) ==> eclose({i}) = succ(i)" 

202 
apply (rule equalityI) 

46820  203 
apply (erule eclose_sing_Ord) 
204 
apply (rule succ_subset_eclose_sing) 

13269  205 
done 
206 

13164  207 
lemma Ord_transrec_type: 
46953  208 
assumes jini: "j \<in> i" 
13164  209 
and ordi: "Ord(i)" 
46953  210 
and minor: " !!x u. [ x \<in> i; u \<in> Pi(x,B) ] ==> H(x,u) \<in> B(x)" 
46820  211 
shows "transrec(j,H) \<in> B(j)" 
13164  212 
apply (rule transrec_type) 
213 
apply (insert jini ordi) 

214 
apply (blast intro!: minor 

46820  215 
intro: Ord_trans 
13164  216 
dest: Ord_in_Ord [THEN eclose_sing_Ord, THEN subsetD]) 
217 
done 

218 

13356  219 
subsection{*Rank*} 
13164  220 

221 
(*NOT SUITABLE FOR REWRITING  RECURSIVE!*) 

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13524
diff
changeset

222 
lemma rank: "rank(a) = (\<Union>y\<in>a. succ(rank(y)))" 
13164  223 
by (subst rank_def [THEN def_transrec], simp) 
224 

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

46820  226 
apply (rule_tac a=a in eps_induct) 
13164  227 
apply (subst rank) 
228 
apply (rule Ord_succ [THEN Ord_UN]) 

229 
apply (erule bspec, assumption) 

230 
done 

231 

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

233 
apply (erule trans_induct) 

234 
apply (subst rank) 

235 
apply (simp add: Ord_equality) 

236 
done 

237 

46953  238 
lemma rank_lt: "a \<in> b ==> rank(a) < rank(b)" 
13784  239 
apply (rule_tac a1 = b in rank [THEN ssubst]) 
13164  240 
apply (erule UN_I [THEN ltI]) 
241 
apply (rule_tac [2] Ord_UN, auto) 

242 
done 

243 

46953  244 
lemma eclose_rank_lt: "a \<in> eclose(b) ==> rank(a) < rank(b)" 
13164  245 
apply (erule eclose_induct_down) 
246 
apply (erule rank_lt) 

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

248 
done 

6070  249 

46820  250 
lemma rank_mono: "a<=b ==> rank(a) \<le> rank(b)" 
13164  251 
apply (rule subset_imp_le) 
46820  252 
apply (auto simp add: rank [of a] rank [of b]) 
13164  253 
done 
254 

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

256 
apply (rule rank [THEN trans]) 

257 
apply (rule le_anti_sym) 

258 
apply (rule_tac [2] UN_upper_le) 

259 
apply (rule UN_least_le) 

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

261 
done 

262 

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

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

265 

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

267 
apply (rule rank [THEN trans]) 

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

269 
apply (erule succE, blast) 

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

271 
done 

272 

46820  273 
lemma rank_Union: "rank(\<Union>(A)) = (\<Union>x\<in>A. rank(x))" 
13164  274 
apply (rule equalityI) 
275 
apply (rule_tac [2] rank_mono [THEN le_imp_subset, THEN UN_least]) 

276 
apply (erule_tac [2] Union_upper) 

277 
apply (subst rank) 

278 
apply (rule UN_least) 

279 
apply (erule UnionE) 

280 
apply (rule subset_trans) 

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

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

283 
done 

284 

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

286 
apply (rule le_anti_sym) 

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

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

289 
apply (rule Ord_rank [THEN UN_least_le]) 

290 
apply (erule eclose_rank_lt [THEN succ_leI]) 

291 
done 

292 

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

294 
apply (unfold Pair_def) 

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

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

297 
done 

298 

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

300 
apply (unfold Pair_def) 

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

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

303 
done 

304 

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

306 
must refer to "a"*) 

307 
lemma the_equality_if: 

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

309 
by (simp add: the_0 the_equality2) 

310 

46820  311 
(*The first premise not only fixs i but ensures @{term"f\<noteq>0"}. 
312 
The second premise is now essential. Consider otherwise the relation 

313 
r = {<0,0>,<0,1>,<0,2>,...}. Then f`0 = \<Union>(f``{0}) = \<Union>(nat) = nat, 

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

314 
whose rank equals that of r.*) 
46820  315 
lemma rank_apply: "[i \<in> domain(f); function(f)] ==> rank(f`i) < rank(f)" 
316 
apply clarify 

317 
apply (simp add: function_apply_equality) 

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

318 
apply (blast intro: lt_trans rank_lt rank_pair2) 
13164  319 
done 
320 

321 

13356  322 
subsection{*Corollaries of Leastness*} 
13164  323 

46953  324 
lemma mem_eclose_subset: "A \<in> B ==> eclose(A)<=eclose(B)" 
13164  325 
apply (rule Transset_eclose [THEN eclose_least]) 
326 
apply (erule arg_into_eclose [THEN eclose_subset]) 

327 
done 

328 

46820  329 
lemma eclose_mono: "A<=B ==> eclose(A) \<subseteq> eclose(B)" 
13164  330 
apply (rule Transset_eclose [THEN eclose_least]) 
331 
apply (erule subset_trans) 

332 
apply (rule arg_subset_eclose) 

333 
done 

334 

335 
(** Idempotence of eclose **) 

336 

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

338 
apply (rule equalityI) 

339 
apply (rule eclose_least [OF Transset_eclose subset_refl]) 

340 
apply (rule arg_subset_eclose) 

341 
done 

342 

46820  343 
(** Transfinite recursion for definitions based on the 
13164  344 
three cases of ordinals **) 
345 

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

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

348 

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

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

351 
apply (simp add: the_equality if_P) 

352 
done 

353 

354 
lemma transrec2_Limit: 

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13524
diff
changeset

355 
"Limit(i) ==> transrec2(i,a,b) = (\<Union>j<i. transrec2(j,a,b))" 
13175
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13164
diff
changeset

356 
apply (rule transrec2_def [THEN def_transrec, THEN trans]) 
46820  357 
apply (auto simp add: OUnion_def) 
13164  358 
done 
359 

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

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

361 
"(!!x. f(x)==transrec2(x,a,b)) 
46820  362 
==> f(0) = a & 
363 
f(succ(i)) = b(i, f(i)) & 

364 
(Limit(K) \<longrightarrow> f(K) = (\<Union>j<K. f(j)))" 

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

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

366 

13164  367 

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

369 

370 
(*NOT suitable for rewriting*) 

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

372 

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

374 
by (rule nat_case_0 [THEN recursor_lemma]) 

375 

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

377 
by (rule recursor_lemma, simp) 

378 

379 

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

381 

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

383 
apply (unfold rec_def) 

384 
apply (rule recursor_0) 

385 
done 

386 

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

388 
apply (unfold rec_def) 

389 
apply (rule recursor_succ) 

390 
done 

391 

392 
lemma rec_type: 

46953  393 
"[ n \<in> nat; 
394 
a \<in> C(0); 

395 
!!m z. [ m \<in> nat; z \<in> C(m) ] ==> b(m,z): C(succ(m)) ] 

46820  396 
==> rec(n,a,b) \<in> C(n)" 
13185  397 
by (erule nat_induct, auto) 
13164  398 

0  399 
end 