author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 47085  4a8a8b9bf414 
child 58871  c399ae4b836f 
permissions  rwrr 
13543  1 
(* Title: ZF/Constructible/AC_in_L.thy 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

3 
*) 

4 

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

6 

47084  7 
theory AC_in_L imports Formula Separation begin 
13543  8 

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

10 

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

12 

13 
consts 

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

15 

16 
inductive 

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

18 
intros 

19 
shorterI: 

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

23 
sameI: 

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

27 
diffI: 

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

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

32 

33 

34 
subsubsection{*Type checking*} 

35 

36 
lemmas rlist_type = rlist.dom_subset 

37 

38 
lemmas field_rlist = rlist_type [THEN field_rel_subset] 

39 

40 
subsubsection{*Linearity*} 

41 

42 
lemma rlist_Nil_Cons [intro]: 

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

13692  44 
by (simp add: shorterI) 
13543  45 

46 
lemma linear_rlist: 

47085  47 
assumes r: "linear(A,r)" shows "linear(list(A),rlist(A,r))" 
48 
proof  

49 
{ fix xs ys 

50 
have "xs \<in> list(A) \<Longrightarrow> ys \<in> list(A) \<Longrightarrow> \<langle>xs,ys\<rangle> \<in> rlist(A,r) \<or> xs = ys \<or> \<langle>ys,xs\<rangle> \<in> rlist(A, r) " 

51 
proof (induct xs arbitrary: ys rule: list.induct) 

52 
case Nil 

53 
thus ?case by (induct ys rule: list.induct) (auto simp add: shorterI) 

54 
next 

55 
case (Cons x xs) 

56 
{ fix y ys 

57 
assume "y \<in> A" and "ys \<in> list(A)" 

58 
with Cons 

59 
have "\<langle>Cons(x,xs),Cons(y,ys)\<rangle> \<in> rlist(A,r) \<or> x=y & xs = ys \<or> \<langle>Cons(y,ys), Cons(x,xs)\<rangle> \<in> rlist(A,r)" 

60 
apply (rule_tac i = "length(xs)" and j = "length(ys)" in Ord_linear_lt) 

61 
apply (simp_all add: shorterI) 

62 
apply (rule linearE [OF r, of x y]) 

63 
apply (auto simp add: diffI intro: sameI) 

64 
done 

65 
} 

66 
note yConsCase = this 

67 
show ?case using `ys \<in> list(A)` 

68 
by (cases rule: list.cases) (simp_all add: Cons rlist_Nil_Cons yConsCase) 

69 
qed 

70 
} 

71 
thus ?thesis by (simp add: linear_def) 

72 
qed 

13543  73 

74 

75 
subsubsection{*Wellfoundedness*} 

76 

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

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

79 

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

81 

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

83 
by (blast intro: elim: rlist_NilE) 

84 

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

86 
apply (erule rlist.induct) 

13692  87 
apply (simp_all add: leI) 
13543  88 
done 
89 

90 
lemma wf_on_rlist_n: 

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

13692  92 
apply (induct_tac n) 
93 
apply (rule wf_onI2, simp) 

94 
apply (rule wf_onI2, clarify) 

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

13543  96 
apply (simp (no_asm_use)) 
13692  97 
apply clarify 
13543  98 
apply (simp (no_asm_use)) 
46823  99 
apply (subgoal_tac "\<forall>l2 \<in> list(A). length(l2) = x \<longrightarrow> Cons(a,l2) \<in> B", blast) 
13543  100 
apply (erule_tac a=a in wf_on_induct, assumption) 
101 
apply (rule ballI) 

13692  102 
apply (rule impI) 
13543  103 
apply (erule_tac a=l2 in wf_on_induct, blast, clarify) 
13692  104 
apply (rename_tac a' l2 l') 
105 
apply (drule_tac x="Cons(a',l')" in bspec, typecheck) 

106 
apply simp 

107 
apply (erule mp, clarify) 

13543  108 
apply (erule rlist_ConsE, auto) 
109 
done 

110 

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

112 
by (blast intro: length_type) 

113 

114 

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

13692  116 
apply (subst list_eq_UN_length) 
117 
apply (rule wf_on_Union) 

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

13692  120 
apply (frule rlist_type [THEN subsetD]) 
121 
apply (simp add: length_type) 

13543  122 
apply (drule rlist_imp_length_le) 
13692  123 
apply (erule leE) 
124 
apply (simp_all add: lt_def) 

13543  125 
done 
126 

127 

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

129 
apply (simp add: wf_iff_wf_on_field) 

130 
apply (rule wf_on_subset_A [OF _ field_rlist]) 

13692  131 
apply (blast intro: wf_on_rlist) 
13543  132 
done 
133 

134 
lemma well_ord_rlist: 

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

136 
apply (rule well_ordI) 

137 
apply (simp add: well_ord_def wf_on_rlist) 

138 
apply (simp add: well_ord_def tot_ord_def linear_rlist) 

139 
done 

140 

141 

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

143 

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

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

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

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

13692  148 
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}: 
149 
@{thm[display] well_ord_InfCard_square_eq[no_vars]} 

13543  150 

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

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

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

155 

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

13543  157 
and @{term nat}*} 
158 
locale Nat_Times_Nat = 

159 
fixes fn 

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

161 

162 

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

164 
primrec 

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

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

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

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

169 

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

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

13692  172 
by (blast intro: inj_is_fun [OF fn_inj] apply_funtype) 
13543  173 

174 
lemma (in Nat_Times_Nat) fn_iff: 

13692  175 
"[x \<in> nat; y \<in> nat; u \<in> nat; v \<in> nat] 
46823  176 
==> (fn`<x,y> = fn`<u,v>) \<longleftrightarrow> (x=u & y=v)" 
13692  177 
by (blast dest: inj_apply_equality [OF fn_inj]) 
13543  178 

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

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

13692  181 
by (induct_tac p, simp_all) 
13543  182 

183 
lemma (in Nat_Times_Nat) enum_inject [rule_format]: 

46823  184 
"p \<in> formula ==> \<forall>q\<in>formula. enum(fn,p) = enum(fn,q) \<longrightarrow> p=q" 
13692  185 
apply (induct_tac p, simp_all) 
186 
apply (rule ballI) 

187 
apply (erule formula.cases) 

188 
apply (simp_all add: fn_iff) 

189 
apply (rule ballI) 

190 
apply (erule formula.cases) 

191 
apply (simp_all add: fn_iff) 

192 
apply (rule ballI) 

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

194 
apply (simp_all add: fn_iff) 

195 
apply blast 

196 
apply (rule ballI) 

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

198 
apply (simp_all add: fn_iff, blast) 

13543  199 
done 
200 

201 
lemma (in Nat_Times_Nat) inj_formula_nat: 

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

13692  203 
apply (simp add: inj_def lam_type) 
204 
apply (blast intro: enum_inject) 

13543  205 
done 
206 

207 
lemma (in Nat_Times_Nat) well_ord_formula: 

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

209 
apply (rule well_ord_measure, simp) 

13692  210 
apply (blast intro: enum_inject) 
13543  211 
done 
212 

213 
lemmas nat_times_nat_lepoll_nat = 

214 
InfCard_nat [THEN InfCard_square_eqpoll, THEN eqpoll_imp_lepoll] 

215 

216 

217 
text{*Not neededbut interesting?*} 

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

219 
apply (insert nat_times_nat_lepoll_nat) 

220 
apply (unfold lepoll_def) 

13692  221 
apply (blast intro: Nat_Times_Nat.inj_formula_nat Nat_Times_Nat.intro) 
222 
done 

223 

224 

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

226 

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

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

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

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

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

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

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

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

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

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

239 
formula, measure(formula, enum(f)))" 
13692  240 

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

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

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

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

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_ord :: "[i,i,i,i,i]=>o" where 
13692  249 
{*predicate that holds if @{term k} is a valid index for @{term X}*} 
13702  250 
"DPow_ord(f,r,A,X,k) == 
13692  251 
\<exists>env \<in> list(A). \<exists>p \<in> formula. 
252 
arity(p) \<le> succ(length(env)) & 

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

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

255 

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

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

257 
DPow_least :: "[i,i,i,i]=>i" where 
13692  258 
{*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

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

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

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

262 
DPow_r :: "[i,i,i]=>i" where 
13692  263 
{*a wellordering on @{term "DPow(A)"}*} 
13702  264 
"DPow_r(f,r,A) == measure(DPow(A), DPow_least(f,r,A))" 
13692  265 

266 

267 
lemma (in Nat_Times_Nat) well_ord_env_form_r: 

268 
"well_ord(A,r) 

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

270 
by (simp add: env_form_r_def well_ord_rmult well_ord_rlist well_ord_formula) 

271 

272 
lemma (in Nat_Times_Nat) Ord_env_form_map: 

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

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

275 
by (simp add: env_form_map_def Ord_ordermap well_ord_env_form_r) 

276 

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

279 
apply (simp add: DPow_ord_def) 

13692  280 
apply (blast dest!: DPowD) 
281 
done 

282 

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

285 
apply (simp add: DPow_ord_def, clarify) 

13692  286 
apply (simp add: Ord_env_form_map) 
13543  287 
done 
288 

13702  289 
lemma (in Nat_Times_Nat) DPow_imp_DPow_least: 
13692  290 
"[X \<in> DPow(A); well_ord(A,r)] 
13702  291 
==> DPow_ord(fn, r, A, X, DPow_least(fn,r,A,X))" 
292 
apply (simp add: DPow_least_def) 

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

13692  294 
done 
295 

296 
lemma (in Nat_Times_Nat) env_form_map_inject: 

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

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

299 
==> u=v" 

300 
apply (simp add: env_form_map_def) 

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

302 
OF well_ord_env_form_r], assumption+) 

303 
done 

304 

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

13692  307 
==> X=Y" 
13702  308 
apply (simp add: DPow_ord_def, clarify) 
13692  309 
apply (drule env_form_map_inject, auto) 
310 
done 

311 

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

314 
apply (simp add: DPow_r_def) 

13692  315 
apply (rule well_ord_measure) 
13702  316 
apply (simp add: DPow_least_def Ord_Least) 
317 
apply (drule DPow_imp_DPow_least, assumption)+ 

13692  318 
apply simp 
13702  319 
apply (blast intro: DPow_ord_unique) 
13692  320 
done 
321 

322 
lemma (in Nat_Times_Nat) DPow_r_type: 

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

13692  325 

13543  326 

327 
subsection{*Limit Construction for WellOrderings*} 

328 

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

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

331 
of wellorderings for smaller ordinals.*} 

332 

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

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

13692  337 
"rlimit(i,r) == 
13702  338 
if Limit(i) then 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

339 
{z: Lset(i) * Lset(i). 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

340 
\<exists>x' x. z = <x',x> & 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

341 
(lrank(x') < lrank(x)  
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
21404
diff
changeset

342 
(lrank(x') = lrank(x) & <x',x> \<in> r(succ(lrank(x)))))} 
13702  343 
else 0" 
13692  344 

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

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

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

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

351 
lemma Limit_Lset_eq2: 

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

13692  353 
apply (simp add: Limit_Lset_eq) 
13543  354 
apply (rule equalityI) 
355 
apply safe 

356 
apply (subgoal_tac "Ord(y)") 

357 
prefer 2 apply (blast intro: Ord_in_Ord Limit_is_Ord) 

13692  358 
apply (simp_all add: Limit_is_Ord Lset_iff_lrank_lt Lset_new_def 
359 
Ord_mem_iff_lt) 

360 
apply (blast intro: lt_trans) 

13543  361 
apply (rule_tac x = "succ(lrank(x))" in bexI) 
13692  362 
apply (simp add: Lset_succ_lrank_iff) 
363 
apply (blast intro: Limit_has_succ ltD) 

13543  364 
done 
365 

366 
lemma wf_on_Lset: 

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

13692  368 
apply (simp add: wf_on_def Lset_new_def) 
369 
apply (erule wf_subset) 

13702  370 
apply (simp add: rlimit_def, force) 
13543  371 
done 
372 

373 
lemma wf_on_rlimit: 

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

376 
prefer 2 

377 
apply (simp add: rlimit_def wf_on_any_0) 

13543  378 
apply (simp add: Limit_Lset_eq2) 
379 
apply (rule wf_on_Union) 

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

13543  382 
apply (force simp add: rlimit_def Limit_is_Ord Lset_iff_lrank_lt Lset_new_def 
383 
Ord_mem_iff_lt) 

384 
done 

385 

386 
lemma linear_rlimit: 

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

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

13692  389 
apply (frule Limit_is_Ord) 
390 
apply (simp add: Limit_Lset_eq2 Lset_new_def) 

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

392 
apply (simp add: ltI, clarify) 

393 
apply (rename_tac u v) 

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

46823  395 
apply (drule_tac x="succ(lrank(u) \<union> lrank(v))" in ospec) 
13692  396 
apply (simp add: ltI) 
397 
apply (drule_tac x=u in spec, simp) 

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

13543  399 
done 
400 

401 
lemma well_ord_rlimit: 

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

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

13692  404 
by (blast intro: well_ordI wf_on_rlimit well_ord_is_wf 
405 
linear_rlimit well_ord_is_linear) 

13543  406 

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

409 
apply (simp add: rlimit_def, clarify) 

410 
apply (rule refl iff_refl Collect_cong ex_cong conj_cong)+ 

411 
apply (simp add: Limit_is_Ord Lset_lrank_lt) 

412 
done 

413 

13543  414 

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

416 

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

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

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

13543  422 

423 
subsubsection{*The Corresponding Recursion Equations*} 

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

13702  425 
by (simp add: L_r_def) 
13543  426 

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

13543  429 

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

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

435 
lemma (in Nat_Times_Nat) L_r_type: 

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

46927  437 
apply (induct i rule: trans_induct3) 
13692  438 
apply (simp_all add: Lset_succ DPow_r_type well_ord_DPow_r rlimit_def 
439 
Transset_subset_DPow [OF Transset_Lset], blast) 

13543  440 
done 
441 

442 
lemma (in Nat_Times_Nat) well_ord_L_r: 

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

46927  444 
apply (induct i rule: trans_induct3) 
13692  445 
apply (simp_all add: well_ord0 Lset_succ L_r_type well_ord_DPow_r 
446 
well_ord_rlimit ltD) 

13543  447 
done 
448 

449 
lemma well_ord_L_r: 

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

451 
apply (insert nat_times_nat_lepoll_nat) 

452 
apply (unfold lepoll_def) 

13692  453 
apply (blast intro: Nat_Times_Nat.well_ord_L_r Nat_Times_Nat.intro) 
13543  454 
done 
455 

456 

47072  457 
text{*Every constructible set is wellordered! Therefore the Wellordering Theorem and 
458 
the Axiom of Choice hold in @{term L}!!*} 

459 
theorem L_implies_AC: assumes x: "L(x)" shows "\<exists>r. well_ord(x,r)" 

460 
using Transset_Lset x 

13543  461 
apply (simp add: Transset_def L_def) 
13692  462 
apply (blast dest!: well_ord_L_r intro: well_ord_subset) 
13543  463 
done 
464 

47084  465 
interpretation L?: M_basic L by (rule M_basic_L) 
466 

467 
theorem "\<forall>x[L]. \<exists>r. wellordered(L,x,r)" 

468 
proof 

469 
fix x 

470 
assume "L(x)" 

471 
then obtain r where "well_ord(x,r)" 

472 
by (blast dest: L_implies_AC) 

473 
thus "\<exists>r. wellordered(L,x,r)" 

474 
by (blast intro: well_ord_imp_relativized) 

475 
qed 

476 

47085  477 
text{*In order to prove @{term" \<exists>r[L]. wellordered(L,x,r)"}, it's necessary to know 
478 
that @{term r} is actually constructible. It follows from the assumption ``@{term V} equals @{term L''}, 

47072  479 
but this reasoning doesn't appear to work in Isabelle.*} 
480 

13543  481 
end 