author  wenzelm 
Fri, 17 Nov 2006 02:20:03 +0100  
changeset 21404  eb85850d3eb7 
parent 21233  5a5c8ea5f66a 
child 32960  69916a850301 
permissions  rwrr 
13543  1 
(* Title: ZF/Constructible/AC_in_L.thy 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
*) 

5 

6 
header {* The Axiom of Choice Holds in L! *} 

7 

16417  8 
theory AC_in_L imports Formula begin 
13543  9 

10 
subsection{*Extending a Wellordering over a List  Lexicographic Power*} 

11 

12 
text{*This could be moved into a library.*} 

13 

14 
consts 

15 
rlist :: "[i,i]=>i" 

16 

17 
inductive 

18 
domains "rlist(A,r)" \<subseteq> "list(A) * list(A)" 

19 
intros 

20 
shorterI: 

13692  21 
"[ length(l') < length(l); l' \<in> list(A); l \<in> list(A) ] 
13543  22 
==> <l', l> \<in> rlist(A,r)" 
23 

24 
sameI: 

13692  25 
"[ <l',l> \<in> rlist(A,r); a \<in> A ] 
13543  26 
==> <Cons(a,l'), Cons(a,l)> \<in> rlist(A,r)" 
27 

28 
diffI: 

13692  29 
"[ length(l') = length(l); <a',a> \<in> r; 
30 
l' \<in> list(A); l \<in> list(A); a' \<in> A; a \<in> A ] 

13543  31 
==> <Cons(a',l'), Cons(a,l)> \<in> rlist(A,r)" 
32 
type_intros list.intros 

33 

34 

35 
subsubsection{*Type checking*} 

36 

37 
lemmas rlist_type = rlist.dom_subset 

38 

39 
lemmas field_rlist = rlist_type [THEN field_rel_subset] 

40 

41 
subsubsection{*Linearity*} 

42 

43 
lemma rlist_Nil_Cons [intro]: 

44 
"[a \<in> A; l \<in> list(A)] ==> <[], Cons(a,l)> \<in> rlist(A, r)" 

13692  45 
by (simp add: shorterI) 
13543  46 

47 
lemma linear_rlist: 

48 
"linear(A,r) ==> linear(list(A),rlist(A,r))" 

49 
apply (simp (no_asm_simp) add: linear_def) 

13692  50 
apply (rule ballI) 
51 
apply (induct_tac x) 

52 
apply (rule ballI) 

53 
apply (induct_tac y) 

54 
apply (simp_all add: shorterI) 

55 
apply (rule ballI) 

56 
apply (erule_tac a=y in list.cases) 

57 
apply (rename_tac [2] a2 l2) 

13543  58 
apply (rule_tac [2] i = "length(l)" and j = "length(l2)" in Ord_linear_lt) 
13692  59 
apply (simp_all add: shorterI) 
60 
apply (erule_tac x=a and y=a2 in linearE) 

61 
apply (simp_all add: diffI) 

62 
apply (blast intro: sameI) 

13543  63 
done 
64 

65 

66 
subsubsection{*Wellfoundedness*} 

67 

68 
text{*Nothing preceeds Nil in this ordering.*} 

69 
inductive_cases rlist_NilE: " <l,[]> \<in> rlist(A,r)" 

70 

71 
inductive_cases rlist_ConsE: " <l', Cons(x,l)> \<in> rlist(A,r)" 

72 

73 
lemma not_rlist_Nil [simp]: " <l,[]> \<notin> rlist(A,r)" 

74 
by (blast intro: elim: rlist_NilE) 

75 

76 
lemma rlist_imp_length_le: "<l',l> \<in> rlist(A,r) ==> length(l') \<le> length(l)" 

77 
apply (erule rlist.induct) 

13692  78 
apply (simp_all add: leI) 
13543  79 
done 
80 

81 
lemma wf_on_rlist_n: 

82 
"[ n \<in> nat; wf[A](r) ] ==> wf[{l \<in> list(A). length(l) = n}](rlist(A,r))" 

13692  83 
apply (induct_tac n) 
84 
apply (rule wf_onI2, simp) 

85 
apply (rule wf_onI2, clarify) 

86 
apply (erule_tac a=y in list.cases, clarify) 

13543  87 
apply (simp (no_asm_use)) 
13692  88 
apply clarify 
13543  89 
apply (simp (no_asm_use)) 
90 
apply (subgoal_tac "\<forall>l2 \<in> list(A). length(l2) = x > Cons(a,l2) \<in> B", blast) 

91 
apply (erule_tac a=a in wf_on_induct, assumption) 

92 
apply (rule ballI) 

13692  93 
apply (rule impI) 
13543  94 
apply (erule_tac a=l2 in wf_on_induct, blast, clarify) 
13692  95 
apply (rename_tac a' l2 l') 
96 
apply (drule_tac x="Cons(a',l')" in bspec, typecheck) 

97 
apply simp 

98 
apply (erule mp, clarify) 

13543  99 
apply (erule rlist_ConsE, auto) 
100 
done 

101 

102 
lemma list_eq_UN_length: "list(A) = (\<Union>n\<in>nat. {l \<in> list(A). length(l) = n})" 

103 
by (blast intro: length_type) 

104 

105 

106 
lemma wf_on_rlist: "wf[A](r) ==> wf[list(A)](rlist(A,r))" 

13692  107 
apply (subst list_eq_UN_length) 
108 
apply (rule wf_on_Union) 

13543  109 
apply (rule wf_imp_wf_on [OF wf_Memrel [of nat]]) 
110 
apply (simp add: wf_on_rlist_n) 

13692  111 
apply (frule rlist_type [THEN subsetD]) 
112 
apply (simp add: length_type) 

13543  113 
apply (drule rlist_imp_length_le) 
13692  114 
apply (erule leE) 
115 
apply (simp_all add: lt_def) 

13543  116 
done 
117 

118 

119 
lemma wf_rlist: "wf(r) ==> wf(rlist(field(r),r))" 

120 
apply (simp add: wf_iff_wf_on_field) 

121 
apply (rule wf_on_subset_A [OF _ field_rlist]) 

13692  122 
apply (blast intro: wf_on_rlist) 
13543  123 
done 
124 

125 
lemma well_ord_rlist: 

126 
"well_ord(A,r) ==> well_ord(list(A), rlist(A,r))" 

127 
apply (rule well_ordI) 

128 
apply (simp add: well_ord_def wf_on_rlist) 

129 
apply (simp add: well_ord_def tot_ord_def linear_rlist) 

130 
done 

131 

132 

133 
subsection{*An Injection from Formulas into the Natural Numbers*} 

134 

135 
text{*There is a wellknown bijection between @{term "nat*nat"} and @{term 

136 
nat} given by the expression f(m,n) = triangle(m+n) + m, where triangle(k) 

137 
enumerates the triangular numbers and can be defined by triangle(0)=0, 

138 
triangle(succ(k)) = succ(k + triangle(k)). Some small amount of effort is 

13692  139 
needed to show that f is a bijection. We already know that such a bijection exists by the theorem @{text well_ord_InfCard_square_eq}: 
140 
@{thm[display] well_ord_InfCard_square_eq[no_vars]} 

13543  141 

13692  142 
However, this result merely states that there is a bijection between the two 
143 
sets. It provides no means of naming a specific bijection. Therefore, we 

144 
conduct the proofs under the assumption that a bijection exists. The simplest 

145 
way to organize this is to use a locale.*} 

146 

147 
text{*Locale for any arbitrary injection between @{term "nat*nat"} 

13543  148 
and @{term nat}*} 
149 
locale Nat_Times_Nat = 

150 
fixes fn 

151 
assumes fn_inj: "fn \<in> inj(nat*nat, nat)" 

152 

153 

154 
consts enum :: "[i,i]=>i" 

155 
primrec 

156 
"enum(f, Member(x,y)) = f ` <0, f ` <x,y>>" 

157 
"enum(f, Equal(x,y)) = f ` <1, f ` <x,y>>" 

158 
"enum(f, Nand(p,q)) = f ` <2, f ` <enum(f,p), enum(f,q)>>" 

159 
"enum(f, Forall(p)) = f ` <succ(2), enum(f,p)>" 

160 

161 
lemma (in Nat_Times_Nat) fn_type [TC,simp]: 

162 
"[x \<in> nat; y \<in> nat] ==> fn`<x,y> \<in> nat" 

13692  163 
by (blast intro: inj_is_fun [OF fn_inj] apply_funtype) 
13543  164 

165 
lemma (in Nat_Times_Nat) fn_iff: 

13692  166 
"[x \<in> nat; y \<in> nat; u \<in> nat; v \<in> nat] 
13543  167 
==> (fn`<x,y> = fn`<u,v>) <> (x=u & y=v)" 
13692  168 
by (blast dest: inj_apply_equality [OF fn_inj]) 
13543  169 

170 
lemma (in Nat_Times_Nat) enum_type [TC,simp]: 

171 
"p \<in> formula ==> enum(fn,p) \<in> nat" 

13692  172 
by (induct_tac p, simp_all) 
13543  173 

174 
lemma (in Nat_Times_Nat) enum_inject [rule_format]: 

175 
"p \<in> formula ==> \<forall>q\<in>formula. enum(fn,p) = enum(fn,q) > p=q" 

13692  176 
apply (induct_tac p, simp_all) 
177 
apply (rule ballI) 

178 
apply (erule formula.cases) 

179 
apply (simp_all add: fn_iff) 

180 
apply (rule ballI) 

181 
apply (erule formula.cases) 

182 
apply (simp_all add: fn_iff) 

183 
apply (rule ballI) 

184 
apply (erule_tac a=qa in formula.cases) 

185 
apply (simp_all add: fn_iff) 

186 
apply blast 

187 
apply (rule ballI) 

188 
apply (erule_tac a=q in formula.cases) 

189 
apply (simp_all add: fn_iff, blast) 

13543  190 
done 
191 

192 
lemma (in Nat_Times_Nat) inj_formula_nat: 

193 
"(\<lambda>p \<in> formula. enum(fn,p)) \<in> inj(formula, nat)" 

13692  194 
apply (simp add: inj_def lam_type) 
195 
apply (blast intro: enum_inject) 

13543  196 
done 
197 

198 
lemma (in Nat_Times_Nat) well_ord_formula: 

199 
"well_ord(formula, measure(formula, enum(fn)))" 

200 
apply (rule well_ord_measure, simp) 

13692  201 
apply (blast intro: enum_inject) 
13543  202 
done 
203 

204 
lemmas nat_times_nat_lepoll_nat = 

205 
InfCard_nat [THEN InfCard_square_eqpoll, THEN eqpoll_imp_lepoll] 

206 

207 

208 
text{*Not neededbut interesting?*} 

209 
theorem formula_lepoll_nat: "formula \<lesssim> nat" 

210 
apply (insert nat_times_nat_lepoll_nat) 

211 
apply (unfold lepoll_def) 

13692  212 
apply (blast intro: Nat_Times_Nat.inj_formula_nat Nat_Times_Nat.intro) 
213 
done 

214 

215 

216 
subsection{*Defining the Wellordering on @{term "DPow(A)"}*} 

217 

218 
text{*The objective is to build a wellordering on @{term "DPow(A)"} from a 

219 
given one on @{term A}. We first introduce wellorderings for environments, 

220 
which are lists built over @{term "A"}. We combine it with the enumeration of 

221 
formulas. The order type of the resulting wellordering gives us a map from 

222 
(environment, formula) pairs into the ordinals. For each member of @{term 

13702  223 
"DPow(A)"}, we take the minimum such ordinal.*} 
13692  224 

21233  225 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

226 
env_form_r :: "[i,i,i]=>i" where 
13692  227 
{*wellordering on (environment, formula) pairs*} 
228 
"env_form_r(f,r,A) == 

229 
rmult(list(A), rlist(A, r), 

230 
formula, measure(formula, enum(f)))" 

231 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

232 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

233 
env_form_map :: "[i,i,i,i]=>i" where 
13692  234 
{*map from (environment, formula) pairs to ordinals*} 
235 
"env_form_map(f,r,A,z) 

236 
== ordermap(list(A) * formula, env_form_r(f,r,A)) ` z" 

237 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

238 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

239 
DPow_ord :: "[i,i,i,i,i]=>o" where 
13692  240 
{*predicate that holds if @{term k} is a valid index for @{term X}*} 
13702  241 
"DPow_ord(f,r,A,X,k) == 
13692  242 
\<exists>env \<in> list(A). \<exists>p \<in> formula. 
243 
arity(p) \<le> succ(length(env)) & 

244 
X = {x\<in>A. sats(A, p, Cons(x,env))} & 

245 
env_form_map(f,r,A,<env,p>) = k" 

246 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

247 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

248 
DPow_least :: "[i,i,i,i]=>i" where 
13692  249 
{*function yielding the smallest index for @{term X}*} 
14171
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13702
diff
changeset

250 
"DPow_least(f,r,A,X) == \<mu> k. DPow_ord(f,r,A,X,k)" 
13692  251 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

252 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

253 
DPow_r :: "[i,i,i]=>i" where 
13692  254 
{*a wellordering on @{term "DPow(A)"}*} 
13702  255 
"DPow_r(f,r,A) == measure(DPow(A), DPow_least(f,r,A))" 
13692  256 

257 

258 
lemma (in Nat_Times_Nat) well_ord_env_form_r: 

259 
"well_ord(A,r) 

260 
==> well_ord(list(A) * formula, env_form_r(fn,r,A))" 

261 
by (simp add: env_form_r_def well_ord_rmult well_ord_rlist well_ord_formula) 

262 

263 
lemma (in Nat_Times_Nat) Ord_env_form_map: 

264 
"[well_ord(A,r); z \<in> list(A) * formula] 

265 
==> Ord(env_form_map(fn,r,A,z))" 

266 
by (simp add: env_form_map_def Ord_ordermap well_ord_env_form_r) 

267 

13702  268 
lemma DPow_imp_ex_DPow_ord: 
269 
"X \<in> DPow(A) ==> \<exists>k. DPow_ord(fn,r,A,X,k)" 

270 
apply (simp add: DPow_ord_def) 

13692  271 
apply (blast dest!: DPowD) 
272 
done 

273 

13702  274 
lemma (in Nat_Times_Nat) DPow_ord_imp_Ord: 
275 
"[DPow_ord(fn,r,A,X,k); well_ord(A,r)] ==> Ord(k)" 

276 
apply (simp add: DPow_ord_def, clarify) 

13692  277 
apply (simp add: Ord_env_form_map) 
13543  278 
done 
279 

13702  280 
lemma (in Nat_Times_Nat) DPow_imp_DPow_least: 
13692  281 
"[X \<in> DPow(A); well_ord(A,r)] 
13702  282 
==> DPow_ord(fn, r, A, X, DPow_least(fn,r,A,X))" 
283 
apply (simp add: DPow_least_def) 

284 
apply (blast dest: DPow_imp_ex_DPow_ord intro: DPow_ord_imp_Ord LeastI) 

13692  285 
done 
286 

287 
lemma (in Nat_Times_Nat) env_form_map_inject: 

288 
"[env_form_map(fn,r,A,u) = env_form_map(fn,r,A,v); well_ord(A,r); 

289 
u \<in> list(A) * formula; v \<in> list(A) * formula] 

290 
==> u=v" 

291 
apply (simp add: env_form_map_def) 

292 
apply (rule inj_apply_equality [OF bij_is_inj, OF ordermap_bij, 

293 
OF well_ord_env_form_r], assumption+) 

294 
done 

295 

13702  296 
lemma (in Nat_Times_Nat) DPow_ord_unique: 
297 
"[DPow_ord(fn,r,A,X,k); DPow_ord(fn,r,A,Y,k); well_ord(A,r)] 

13692  298 
==> X=Y" 
13702  299 
apply (simp add: DPow_ord_def, clarify) 
13692  300 
apply (drule env_form_map_inject, auto) 
301 
done 

302 

13702  303 
lemma (in Nat_Times_Nat) well_ord_DPow_r: 
304 
"well_ord(A,r) ==> well_ord(DPow(A), DPow_r(fn,r,A))" 

305 
apply (simp add: DPow_r_def) 

13692  306 
apply (rule well_ord_measure) 
13702  307 
apply (simp add: DPow_least_def Ord_Least) 
308 
apply (drule DPow_imp_DPow_least, assumption)+ 

13692  309 
apply simp 
13702  310 
apply (blast intro: DPow_ord_unique) 
13692  311 
done 
312 

313 
lemma (in Nat_Times_Nat) DPow_r_type: 

13702  314 
"DPow_r(fn,r,A) \<subseteq> DPow(A) * DPow(A)" 
315 
by (simp add: DPow_r_def measure_def, blast) 

13692  316 

13543  317 

318 
subsection{*Limit Construction for WellOrderings*} 

319 

320 
text{*Now we work towards the transfinite definition of wellorderings for 

321 
@{term "Lset(i)"}. We assume as an inductive hypothesis that there is a family 

322 
of wellorderings for smaller ordinals.*} 

323 

21233  324 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

325 
rlimit :: "[i,i=>i]=>i" where 
13702  326 
{*Expresses the wellordering at limit ordinals. The conditional 
327 
lets us remove the premise @{term "Limit(i)"} from some theorems.*} 

13692  328 
"rlimit(i,r) == 
13702  329 
if Limit(i) then 
330 
{z: Lset(i) * Lset(i). 

331 
\<exists>x' x. z = <x',x> & 

332 
(lrank(x') < lrank(x)  

333 
(lrank(x') = lrank(x) & <x',x> \<in> r(succ(lrank(x)))))} 

334 
else 0" 

13692  335 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

336 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

337 
Lset_new :: "i=>i" where 
13692  338 
{*This constant denotes the set of elements introduced at level 
339 
@{term "succ(i)"}*} 

13543  340 
"Lset_new(i) == {x \<in> Lset(succ(i)). lrank(x) = i}" 
341 

342 
lemma Limit_Lset_eq2: 

343 
"Limit(i) ==> Lset(i) = (\<Union>j\<in>i. Lset_new(j))" 

13692  344 
apply (simp add: Limit_Lset_eq) 
13543  345 
apply (rule equalityI) 
346 
apply safe 

347 
apply (subgoal_tac "Ord(y)") 

348 
prefer 2 apply (blast intro: Ord_in_Ord Limit_is_Ord) 

13692  349 
apply (simp_all add: Limit_is_Ord Lset_iff_lrank_lt Lset_new_def 
350 
Ord_mem_iff_lt) 

351 
apply (blast intro: lt_trans) 

13543  352 
apply (rule_tac x = "succ(lrank(x))" in bexI) 
13692  353 
apply (simp add: Lset_succ_lrank_iff) 
354 
apply (blast intro: Limit_has_succ ltD) 

13543  355 
done 
356 

357 
lemma wf_on_Lset: 

358 
"wf[Lset(succ(j))](r(succ(j))) ==> wf[Lset_new(j)](rlimit(i,r))" 

13692  359 
apply (simp add: wf_on_def Lset_new_def) 
360 
apply (erule wf_subset) 

13702  361 
apply (simp add: rlimit_def, force) 
13543  362 
done 
363 

364 
lemma wf_on_rlimit: 

13702  365 
"(\<forall>j<i. wf[Lset(j)](r(j))) ==> wf[Lset(i)](rlimit(i,r))" 
366 
apply (case_tac "Limit(i)") 

367 
prefer 2 

368 
apply (simp add: rlimit_def wf_on_any_0) 

13543  369 
apply (simp add: Limit_Lset_eq2) 
370 
apply (rule wf_on_Union) 

13692  371 
apply (rule wf_imp_wf_on [OF wf_Memrel [of i]]) 
372 
apply (blast intro: wf_on_Lset Limit_has_succ Limit_is_Ord ltI) 

13543  373 
apply (force simp add: rlimit_def Limit_is_Ord Lset_iff_lrank_lt Lset_new_def 
374 
Ord_mem_iff_lt) 

375 
done 

376 

377 
lemma linear_rlimit: 

378 
"[Limit(i); \<forall>j<i. linear(Lset(j), r(j)) ] 

379 
==> linear(Lset(i), rlimit(i,r))" 

13692  380 
apply (frule Limit_is_Ord) 
381 
apply (simp add: Limit_Lset_eq2 Lset_new_def) 

382 
apply (simp add: linear_def rlimit_def Ball_def lt_Ord Lset_iff_lrank_lt) 

383 
apply (simp add: ltI, clarify) 

384 
apply (rename_tac u v) 

385 
apply (rule_tac i="lrank(u)" and j="lrank(v)" in Ord_linear_lt, simp_all) 

386 
apply (drule_tac x="succ(lrank(u) Un lrank(v))" in ospec) 

387 
apply (simp add: ltI) 

388 
apply (drule_tac x=u in spec, simp) 

389 
apply (drule_tac x=v in spec, simp) 

13543  390 
done 
391 

392 
lemma well_ord_rlimit: 

393 
"[Limit(i); \<forall>j<i. well_ord(Lset(j), r(j)) ] 

394 
==> well_ord(Lset(i), rlimit(i,r))" 

13692  395 
by (blast intro: well_ordI wf_on_rlimit well_ord_is_wf 
396 
linear_rlimit well_ord_is_linear) 

13543  397 

13702  398 
lemma rlimit_cong: 
399 
"(!!j. j<i ==> r'(j) = r(j)) ==> rlimit(i,r) = rlimit(i,r')" 

400 
apply (simp add: rlimit_def, clarify) 

401 
apply (rule refl iff_refl Collect_cong ex_cong conj_cong)+ 

402 
apply (simp add: Limit_is_Ord Lset_lrank_lt) 

403 
done 

404 

13543  405 

406 
subsection{*Transfinite Definition of the Wellordering on @{term "L"}*} 

407 

21233  408 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

409 
L_r :: "[i, i] => i" where 
13702  410 
"L_r(f) == %i. 
411 
transrec3(i, 0, \<lambda>x r. DPow_r(f, r, Lset(x)), 

412 
\<lambda>x r. rlimit(x, \<lambda>y. r`y))" 

13543  413 

414 
subsubsection{*The Corresponding Recursion Equations*} 

415 
lemma [simp]: "L_r(f,0) = 0" 

13702  416 
by (simp add: L_r_def) 
13543  417 

13702  418 
lemma [simp]: "L_r(f, succ(i)) = DPow_r(f, L_r(f,i), Lset(i))" 
419 
by (simp add: L_r_def) 

13543  420 

13702  421 
text{*The limit case is nontrivial because of the distinction between 
422 
objectlevel and metalevel abstraction.*} 

13543  423 
lemma [simp]: "Limit(i) ==> L_r(f,i) = rlimit(i, L_r(f))" 
13702  424 
by (simp cong: rlimit_cong add: transrec3_Limit L_r_def ltD) 
13543  425 

426 
lemma (in Nat_Times_Nat) L_r_type: 

427 
"Ord(i) ==> L_r(fn,i) \<subseteq> Lset(i) * Lset(i)" 

428 
apply (induct i rule: trans_induct3_rule) 

13692  429 
apply (simp_all add: Lset_succ DPow_r_type well_ord_DPow_r rlimit_def 
430 
Transset_subset_DPow [OF Transset_Lset], blast) 

13543  431 
done 
432 

433 
lemma (in Nat_Times_Nat) well_ord_L_r: 

434 
"Ord(i) ==> well_ord(Lset(i), L_r(fn,i))" 

435 
apply (induct i rule: trans_induct3_rule) 

13692  436 
apply (simp_all add: well_ord0 Lset_succ L_r_type well_ord_DPow_r 
437 
well_ord_rlimit ltD) 

13543  438 
done 
439 

440 
lemma well_ord_L_r: 

441 
"Ord(i) ==> \<exists>r. well_ord(Lset(i), r)" 

442 
apply (insert nat_times_nat_lepoll_nat) 

443 
apply (unfold lepoll_def) 

13692  444 
apply (blast intro: Nat_Times_Nat.well_ord_L_r Nat_Times_Nat.intro) 
13543  445 
done 
446 

447 

448 
text{*Locale for proving results under the assumption @{text "V=L"}*} 

449 
locale V_equals_L = 

450 
assumes VL: "L(x)" 

451 

452 
text{*The Axiom of Choice holds in @{term L}! Or, to be precise, the 

453 
Wellordering Theorem.*} 

454 
theorem (in V_equals_L) AC: "\<exists>r. well_ord(x,r)" 

13692  455 
apply (insert Transset_Lset VL [of x]) 
13543  456 
apply (simp add: Transset_def L_def) 
13692  457 
apply (blast dest!: well_ord_L_r intro: well_ord_subset) 
13543  458 
done 
459 

460 
end 