|
1 (* Title: ZF/Constructible/AC_in_L.thy |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 2002 University of Cambridge |
|
5 *) |
|
6 |
|
7 header {* The Axiom of Choice Holds in L! *} |
|
8 |
|
9 theory AC_in_L = Formula: |
|
10 |
|
11 subsection{*Extending a Wellordering over a List -- Lexicographic Power*} |
|
12 |
|
13 text{*This could be moved into a library.*} |
|
14 |
|
15 consts |
|
16 rlist :: "[i,i]=>i" |
|
17 |
|
18 inductive |
|
19 domains "rlist(A,r)" \<subseteq> "list(A) * list(A)" |
|
20 intros |
|
21 shorterI: |
|
22 "[| length(l') < length(l); l' \<in> list(A); l \<in> list(A) |] |
|
23 ==> <l', l> \<in> rlist(A,r)" |
|
24 |
|
25 sameI: |
|
26 "[| <l',l> \<in> rlist(A,r); a \<in> A |] |
|
27 ==> <Cons(a,l'), Cons(a,l)> \<in> rlist(A,r)" |
|
28 |
|
29 diffI: |
|
30 "[| length(l') = length(l); <a',a> \<in> r; |
|
31 l' \<in> list(A); l \<in> list(A); a' \<in> A; a \<in> A |] |
|
32 ==> <Cons(a',l'), Cons(a,l)> \<in> rlist(A,r)" |
|
33 type_intros list.intros |
|
34 |
|
35 |
|
36 subsubsection{*Type checking*} |
|
37 |
|
38 lemmas rlist_type = rlist.dom_subset |
|
39 |
|
40 lemmas field_rlist = rlist_type [THEN field_rel_subset] |
|
41 |
|
42 subsubsection{*Linearity*} |
|
43 |
|
44 lemma rlist_Nil_Cons [intro]: |
|
45 "[|a \<in> A; l \<in> list(A)|] ==> <[], Cons(a,l)> \<in> rlist(A, r)" |
|
46 by (simp add: shorterI) |
|
47 |
|
48 lemma linear_rlist: |
|
49 "linear(A,r) ==> linear(list(A),rlist(A,r))" |
|
50 apply (simp (no_asm_simp) add: linear_def) |
|
51 apply (rule ballI) |
|
52 apply (induct_tac x) |
|
53 apply (rule ballI) |
|
54 apply (induct_tac y) |
|
55 apply (simp_all add: shorterI) |
|
56 apply (rule ballI) |
|
57 apply (erule_tac a=y in list.cases) |
|
58 apply (rename_tac [2] a2 l2) |
|
59 apply (rule_tac [2] i = "length(l)" and j = "length(l2)" in Ord_linear_lt) |
|
60 apply (simp_all add: shorterI) |
|
61 apply (erule_tac x=a and y=a2 in linearE) |
|
62 apply (simp_all add: diffI) |
|
63 apply (blast intro: sameI) |
|
64 done |
|
65 |
|
66 |
|
67 subsubsection{*Well-foundedness*} |
|
68 |
|
69 text{*Nothing preceeds Nil in this ordering.*} |
|
70 inductive_cases rlist_NilE: " <l,[]> \<in> rlist(A,r)" |
|
71 |
|
72 inductive_cases rlist_ConsE: " <l', Cons(x,l)> \<in> rlist(A,r)" |
|
73 |
|
74 lemma not_rlist_Nil [simp]: " <l,[]> \<notin> rlist(A,r)" |
|
75 by (blast intro: elim: rlist_NilE) |
|
76 |
|
77 lemma rlist_imp_length_le: "<l',l> \<in> rlist(A,r) ==> length(l') \<le> length(l)" |
|
78 apply (erule rlist.induct) |
|
79 apply (simp_all add: leI) |
|
80 done |
|
81 |
|
82 lemma wf_on_rlist_n: |
|
83 "[| n \<in> nat; wf[A](r) |] ==> wf[{l \<in> list(A). length(l) = n}](rlist(A,r))" |
|
84 apply (induct_tac n) |
|
85 apply (rule wf_onI2, simp) |
|
86 apply (rule wf_onI2, clarify) |
|
87 apply (erule_tac a=y in list.cases, clarify) |
|
88 apply (simp (no_asm_use)) |
|
89 apply clarify |
|
90 apply (simp (no_asm_use)) |
|
91 apply (subgoal_tac "\<forall>l2 \<in> list(A). length(l2) = x --> Cons(a,l2) \<in> B", blast) |
|
92 apply (erule_tac a=a in wf_on_induct, assumption) |
|
93 apply (rule ballI) |
|
94 apply (rule impI) |
|
95 apply (erule_tac a=l2 in wf_on_induct, blast, clarify) |
|
96 apply (rename_tac a' l2 l') |
|
97 apply (drule_tac x="Cons(a',l')" in bspec, typecheck) |
|
98 apply simp |
|
99 apply (erule mp, clarify) |
|
100 apply (erule rlist_ConsE, auto) |
|
101 done |
|
102 |
|
103 lemma list_eq_UN_length: "list(A) = (\<Union>n\<in>nat. {l \<in> list(A). length(l) = n})" |
|
104 by (blast intro: length_type) |
|
105 |
|
106 |
|
107 lemma wf_on_rlist: "wf[A](r) ==> wf[list(A)](rlist(A,r))" |
|
108 apply (subst list_eq_UN_length) |
|
109 apply (rule wf_on_Union) |
|
110 apply (rule wf_imp_wf_on [OF wf_Memrel [of nat]]) |
|
111 apply (simp add: wf_on_rlist_n) |
|
112 apply (frule rlist_type [THEN subsetD]) |
|
113 apply (simp add: length_type) |
|
114 apply (drule rlist_imp_length_le) |
|
115 apply (erule leE) |
|
116 apply (simp_all add: lt_def) |
|
117 done |
|
118 |
|
119 |
|
120 lemma wf_rlist: "wf(r) ==> wf(rlist(field(r),r))" |
|
121 apply (simp add: wf_iff_wf_on_field) |
|
122 apply (rule wf_on_subset_A [OF _ field_rlist]) |
|
123 apply (blast intro: wf_on_rlist) |
|
124 done |
|
125 |
|
126 lemma well_ord_rlist: |
|
127 "well_ord(A,r) ==> well_ord(list(A), rlist(A,r))" |
|
128 apply (rule well_ordI) |
|
129 apply (simp add: well_ord_def wf_on_rlist) |
|
130 apply (simp add: well_ord_def tot_ord_def linear_rlist) |
|
131 done |
|
132 |
|
133 |
|
134 subsection{*An Injection from Formulas into the Natural Numbers*} |
|
135 |
|
136 text{*There is a well-known bijection between @{term "nat*nat"} and @{term |
|
137 nat} given by the expression f(m,n) = triangle(m+n) + m, where triangle(k) |
|
138 enumerates the triangular numbers and can be defined by triangle(0)=0, |
|
139 triangle(succ(k)) = succ(k + triangle(k)). Some small amount of effort is |
|
140 needed to show that f is a bijection. We already know (by the theorem @{text |
|
141 InfCard_square_eqpoll}) that such a bijection exists, but as we have no direct |
|
142 way to refer to it, we must use a locale.*} |
|
143 |
|
144 text{*Locale for any arbitrary injection between @{term "nat*nat"} |
|
145 and @{term nat}*} |
|
146 locale Nat_Times_Nat = |
|
147 fixes fn |
|
148 assumes fn_inj: "fn \<in> inj(nat*nat, nat)" |
|
149 |
|
150 |
|
151 consts enum :: "[i,i]=>i" |
|
152 primrec |
|
153 "enum(f, Member(x,y)) = f ` <0, f ` <x,y>>" |
|
154 "enum(f, Equal(x,y)) = f ` <1, f ` <x,y>>" |
|
155 "enum(f, Nand(p,q)) = f ` <2, f ` <enum(f,p), enum(f,q)>>" |
|
156 "enum(f, Forall(p)) = f ` <succ(2), enum(f,p)>" |
|
157 |
|
158 lemma (in Nat_Times_Nat) fn_type [TC,simp]: |
|
159 "[|x \<in> nat; y \<in> nat|] ==> fn`<x,y> \<in> nat" |
|
160 by (blast intro: inj_is_fun [OF fn_inj] apply_funtype) |
|
161 |
|
162 lemma (in Nat_Times_Nat) fn_iff: |
|
163 "[|x \<in> nat; y \<in> nat; u \<in> nat; v \<in> nat|] |
|
164 ==> (fn`<x,y> = fn`<u,v>) <-> (x=u & y=v)" |
|
165 by (blast dest: inj_apply_equality [OF fn_inj]) |
|
166 |
|
167 lemma (in Nat_Times_Nat) enum_type [TC,simp]: |
|
168 "p \<in> formula ==> enum(fn,p) \<in> nat" |
|
169 by (induct_tac p, simp_all) |
|
170 |
|
171 lemma (in Nat_Times_Nat) enum_inject [rule_format]: |
|
172 "p \<in> formula ==> \<forall>q\<in>formula. enum(fn,p) = enum(fn,q) --> p=q" |
|
173 apply (induct_tac p, simp_all) |
|
174 apply (rule ballI) |
|
175 apply (erule formula.cases) |
|
176 apply (simp_all add: fn_iff) |
|
177 apply (rule ballI) |
|
178 apply (erule formula.cases) |
|
179 apply (simp_all add: fn_iff) |
|
180 apply (rule ballI) |
|
181 apply (erule_tac a=qa in formula.cases) |
|
182 apply (simp_all add: fn_iff) |
|
183 apply blast |
|
184 apply (rule ballI) |
|
185 apply (erule_tac a=q in formula.cases) |
|
186 apply (simp_all add: fn_iff, blast) |
|
187 done |
|
188 |
|
189 lemma (in Nat_Times_Nat) inj_formula_nat: |
|
190 "(\<lambda>p \<in> formula. enum(fn,p)) \<in> inj(formula, nat)" |
|
191 apply (simp add: inj_def lam_type) |
|
192 apply (blast intro: enum_inject) |
|
193 done |
|
194 |
|
195 lemma (in Nat_Times_Nat) well_ord_formula: |
|
196 "well_ord(formula, measure(formula, enum(fn)))" |
|
197 apply (rule well_ord_measure, simp) |
|
198 apply (blast intro: enum_inject) |
|
199 done |
|
200 |
|
201 lemmas nat_times_nat_lepoll_nat = |
|
202 InfCard_nat [THEN InfCard_square_eqpoll, THEN eqpoll_imp_lepoll] |
|
203 |
|
204 |
|
205 text{*Not needed--but interesting?*} |
|
206 theorem formula_lepoll_nat: "formula \<lesssim> nat" |
|
207 apply (insert nat_times_nat_lepoll_nat) |
|
208 apply (unfold lepoll_def) |
|
209 apply (blast intro: exI Nat_Times_Nat.inj_formula_nat Nat_Times_Nat.intro) |
|
210 done |
|
211 |
|
212 |
|
213 subsection{*Limit Construction for Well-Orderings*} |
|
214 |
|
215 text{*Now we work towards the transfinite definition of wellorderings for |
|
216 @{term "Lset(i)"}. We assume as an inductive hypothesis that there is a family |
|
217 of wellorderings for smaller ordinals.*} |
|
218 |
|
219 text{*This constant denotes the set of elements introduced at level |
|
220 @{term "succ(i)"}*} |
|
221 constdefs |
|
222 Lset_new :: "i=>i" |
|
223 "Lset_new(i) == {x \<in> Lset(succ(i)). lrank(x) = i}" |
|
224 |
|
225 lemma Lset_new_iff_lrank_eq: |
|
226 "Ord(i) ==> x \<in> Lset_new(i) <-> L(x) & lrank(x) = i" |
|
227 by (auto simp add: Lset_new_def Lset_iff_lrank_lt) |
|
228 |
|
229 lemma Lset_new_eq: |
|
230 "Ord(i) ==> Lset_new(i) = Lset(succ(i)) - Lset(i)" |
|
231 apply (rule equality_iffI) |
|
232 apply (simp add: Lset_new_iff_lrank_eq Lset_iff_lrank_lt, auto) |
|
233 apply (blast elim: leE) |
|
234 done |
|
235 |
|
236 lemma Limit_Lset_eq2: |
|
237 "Limit(i) ==> Lset(i) = (\<Union>j\<in>i. Lset_new(j))" |
|
238 apply (simp add: Limit_Lset_eq) |
|
239 apply (rule equalityI) |
|
240 apply safe |
|
241 apply (subgoal_tac "Ord(y)") |
|
242 prefer 2 apply (blast intro: Ord_in_Ord Limit_is_Ord) |
|
243 apply (rotate_tac -1) |
|
244 apply (simp_all add: Limit_is_Ord Lset_iff_lrank_lt Lset_new_def |
|
245 Ord_mem_iff_lt) |
|
246 apply (blast intro: lt_trans) |
|
247 apply (rule_tac x = "succ(lrank(x))" in bexI) |
|
248 apply (simp add: Lset_succ_lrank_iff) |
|
249 apply (blast intro: Limit_has_succ ltD) |
|
250 done |
|
251 |
|
252 text{*This constant expresses the wellordering at limit ordinals.*} |
|
253 constdefs |
|
254 rlimit :: "[i,i=>i]=>i" |
|
255 "rlimit(i,r) == |
|
256 {z: Lset(i) * Lset(i). |
|
257 \<exists>x' x. z = <x',x> & |
|
258 (lrank(x') < lrank(x) | |
|
259 (lrank(x') = lrank(x) & <x',x> \<in> r(succ(lrank(x)))))}" |
|
260 |
|
261 lemma rlimit_eqI: |
|
262 "[|Limit(i); \<forall>j<i. r'(j) = r(j)|] ==> rlimit(i,r) = rlimit(i,r')" |
|
263 apply (simp add: rlimit_def) |
|
264 apply (rule refl iff_refl Collect_cong ex_cong conj_cong)+ |
|
265 apply (simp add: Limit_is_Ord Lset_lrank_lt) |
|
266 done |
|
267 |
|
268 lemma wf_on_Lset: |
|
269 "wf[Lset(succ(j))](r(succ(j))) ==> wf[Lset_new(j)](rlimit(i,r))" |
|
270 apply (simp add: wf_on_def Lset_new_def) |
|
271 apply (erule wf_subset) |
|
272 apply (force simp add: rlimit_def) |
|
273 done |
|
274 |
|
275 lemma wf_on_rlimit: |
|
276 "[|Limit(i); \<forall>j<i. wf[Lset(j)](r(j)) |] ==> wf[Lset(i)](rlimit(i,r))" |
|
277 apply (simp add: Limit_Lset_eq2) |
|
278 apply (rule wf_on_Union) |
|
279 apply (rule wf_imp_wf_on [OF wf_Memrel [of i]]) |
|
280 apply (blast intro: wf_on_Lset Limit_has_succ Limit_is_Ord ltI) |
|
281 apply (force simp add: rlimit_def Limit_is_Ord Lset_iff_lrank_lt Lset_new_def |
|
282 Ord_mem_iff_lt) |
|
283 |
|
284 done |
|
285 |
|
286 lemma linear_rlimit: |
|
287 "[|Limit(i); \<forall>j<i. linear(Lset(j), r(j)) |] |
|
288 ==> linear(Lset(i), rlimit(i,r))" |
|
289 apply (frule Limit_is_Ord) |
|
290 apply (simp add: Limit_Lset_eq2) |
|
291 apply (simp add: linear_def Lset_new_def rlimit_def Ball_def) |
|
292 apply (simp add: lt_Ord Lset_iff_lrank_lt) |
|
293 apply (simp add: ltI, clarify) |
|
294 apply (rename_tac u v) |
|
295 apply (rule_tac i="lrank(u)" and j="lrank(v)" in Ord_linear_lt) |
|
296 apply simp_all |
|
297 apply (drule_tac x="succ(lrank(u) Un lrank(v))" in ospec) |
|
298 apply (simp add: ltI) |
|
299 apply (drule_tac x=u in spec, simp) |
|
300 apply (drule_tac x=v in spec, simp) |
|
301 done |
|
302 |
|
303 |
|
304 lemma well_ord_rlimit: |
|
305 "[|Limit(i); \<forall>j<i. well_ord(Lset(j), r(j)) |] |
|
306 ==> well_ord(Lset(i), rlimit(i,r))" |
|
307 by (blast intro: well_ordI wf_on_rlimit well_ord_is_wf |
|
308 linear_rlimit well_ord_is_linear) |
|
309 |
|
310 |
|
311 subsection{*Defining the Wellordering on @{term "Lset(succ(i))"}*} |
|
312 |
|
313 text{*We introduce wellorderings for environments, which are lists built over |
|
314 @{term "Lset(succ(i))"}. We combine it with the enumeration of formulas. The |
|
315 order type of the resulting wellordering gives us a map from (environment, |
|
316 formula) pairs into the ordinals. For each member of @{term "DPow(Lset(i))"}, |
|
317 we take the minimum such ordinal. This yields a wellordering of |
|
318 @{term "DPow(Lset(i))"}, which we then extend to @{term "Lset(succ(i))"}*} |
|
319 |
|
320 constdefs |
|
321 env_form_r :: "[i,i,i]=>i" |
|
322 --{*wellordering on (environment, formula) pairs*} |
|
323 "env_form_r(f,r,i) == |
|
324 rmult(list(Lset(i)), rlist(Lset(i), r), |
|
325 formula, measure(formula, enum(f)))" |
|
326 |
|
327 env_form_map :: "[i,i,i,i]=>i" |
|
328 --{*map from (environment, formula) pairs to ordinals*} |
|
329 "env_form_map(f,r,i,z) |
|
330 == ordermap(list(Lset(i)) * formula, env_form_r(f,r,i)) ` z" |
|
331 |
|
332 L_new_ord :: "[i,i,i,i,i]=>o" |
|
333 --{*predicate that holds if @{term k} is a valid index for @{term X}*} |
|
334 "L_new_ord(f,r,i,X,k) == |
|
335 \<exists>env \<in> list(Lset(i)). \<exists>p \<in> formula. |
|
336 arity(p) \<le> succ(length(env)) & |
|
337 X = {x\<in>Lset(i). sats(Lset(i), p, Cons(x,env))} & |
|
338 env_form_map(f,r,i,<env,p>) = k" |
|
339 |
|
340 L_new_least :: "[i,i,i,i]=>i" |
|
341 --{*function yielding the smallest index for @{term X}*} |
|
342 "L_new_least(f,r,i,X) == \<mu>k. L_new_ord(f,r,i,X,k)" |
|
343 |
|
344 L_new_r :: "[i,i,i]=>i" |
|
345 --{*a wellordering on @{term "DPow(Lset(i))"}*} |
|
346 "L_new_r(f,r,i) == measure(Lset_new(i), L_new_least(f,r,i))" |
|
347 |
|
348 L_succ_r :: "[i,i,i]=>i" |
|
349 --{*a wellordering on @{term "Lset(succ(i))"}*} |
|
350 "L_succ_r(f,r,i) == (L_new_r(f,r,i) Un (Lset(i) * Lset_new(i))) Un r" |
|
351 |
|
352 |
|
353 lemma (in Nat_Times_Nat) well_ord_env_form_r: |
|
354 "well_ord(Lset(i), r) |
|
355 ==> well_ord(list(Lset(i)) * formula, env_form_r(fn,r,i))" |
|
356 by (simp add: env_form_r_def well_ord_rmult well_ord_rlist well_ord_formula) |
|
357 |
|
358 lemma (in Nat_Times_Nat) Ord_env_form_map: |
|
359 "[|well_ord(Lset(i), r); z \<in> list(Lset(i)) * formula|] |
|
360 ==> Ord(env_form_map(fn,r,i,z))" |
|
361 by (simp add: env_form_map_def Ord_ordermap well_ord_env_form_r) |
|
362 |
|
363 |
|
364 lemma DPow_imp_ex_L_new_ord: |
|
365 "X \<in> DPow(Lset(i)) ==> \<exists>k. L_new_ord(fn,r,i,X,k)" |
|
366 apply (simp add: L_new_ord_def) |
|
367 apply (blast dest!: DPowD) |
|
368 done |
|
369 |
|
370 lemma (in Nat_Times_Nat) L_new_ord_imp_Ord: |
|
371 "[|L_new_ord(fn,r,i,X,k); well_ord(Lset(i), r)|] ==> Ord(k)" |
|
372 apply (simp add: L_new_ord_def, clarify) |
|
373 apply (simp add: Ord_env_form_map) |
|
374 done |
|
375 |
|
376 lemma (in Nat_Times_Nat) DPow_imp_L_new_least: |
|
377 "[|X \<in> DPow(Lset(i)); well_ord(Lset(i), r)|] |
|
378 ==> L_new_ord(fn, r, i, X, L_new_least(fn,r,i,X))" |
|
379 apply (simp add: L_new_least_def) |
|
380 apply (blast dest!: DPow_imp_ex_L_new_ord intro: L_new_ord_imp_Ord LeastI) |
|
381 done |
|
382 |
|
383 lemma (in Nat_Times_Nat) env_form_map_inject: |
|
384 "[|env_form_map(fn,r,i,u) = env_form_map(fn,r,i,v); well_ord(Lset(i), r); |
|
385 u \<in> list(Lset(i)) * formula; v \<in> list(Lset(i)) * formula|] |
|
386 ==> u=v" |
|
387 apply (simp add: env_form_map_def) |
|
388 apply (rule inj_apply_equality [OF bij_is_inj, OF ordermap_bij, |
|
389 OF well_ord_env_form_r], assumption+) |
|
390 done |
|
391 |
|
392 |
|
393 lemma (in Nat_Times_Nat) L_new_ord_unique: |
|
394 "[|L_new_ord(fn,r,i,X,k); L_new_ord(fn,r,i,Y,k); well_ord(Lset(i), r)|] |
|
395 ==> X=Y" |
|
396 apply (simp add: L_new_ord_def, clarify) |
|
397 apply (drule env_form_map_inject, auto) |
|
398 done |
|
399 |
|
400 lemma (in Nat_Times_Nat) well_ord_L_new_r: |
|
401 "[|Ord(i); well_ord(Lset(i), r)|] |
|
402 ==> well_ord(Lset_new(i), L_new_r(fn,r,i))" |
|
403 apply (simp add: L_new_r_def) |
|
404 apply (rule well_ord_measure) |
|
405 apply (simp add: L_new_least_def Ord_Least) |
|
406 apply (simp add: Lset_new_eq Lset_succ, clarify) |
|
407 apply (drule DPow_imp_L_new_least, assumption)+ |
|
408 apply simp |
|
409 apply (blast intro: L_new_ord_unique) |
|
410 done |
|
411 |
|
412 lemma L_new_r_subset: "L_new_r(f,r,i) <= Lset_new(i) * Lset_new(i)" |
|
413 by (simp add: L_new_r_def measure_type) |
|
414 |
|
415 lemma Lset_Lset_new_disjoint: "Ord(i) ==> Lset(i) \<inter> Lset_new(i) = 0" |
|
416 by (simp add: Lset_new_eq, blast) |
|
417 |
|
418 lemma (in Nat_Times_Nat) linear_L_succ_r: |
|
419 "[|Ord(i); well_ord(Lset(i), r)|] |
|
420 ==> linear(Lset(succ(i)), L_succ_r(fn, r, i))" |
|
421 apply (frule well_ord_L_new_r, assumption) |
|
422 apply (drule well_ord_is_linear)+ |
|
423 apply (simp add: linear_def L_succ_r_def Lset_new_eq, auto) |
|
424 done |
|
425 |
|
426 |
|
427 lemma (in Nat_Times_Nat) wf_L_new_r: |
|
428 "[|Ord(i); well_ord(Lset(i), r)|] ==> wf(L_new_r(fn,r,i))" |
|
429 apply (rule well_ord_L_new_r [THEN well_ord_is_wf, THEN wf_on_imp_wf], |
|
430 assumption+) |
|
431 apply (rule L_new_r_subset) |
|
432 done |
|
433 |
|
434 |
|
435 lemma (in Nat_Times_Nat) well_ord_L_new_r: |
|
436 "[|Ord(i); well_ord(Lset(i), r); r \<subseteq> Lset(i) * Lset(i)|] |
|
437 ==> well_ord(Lset(succ(i)), L_succ_r(fn,r,i))" |
|
438 apply (rule well_ordI [OF wf_imp_wf_on]) |
|
439 prefer 2 apply (blast intro: linear_L_succ_r) |
|
440 apply (simp add: L_succ_r_def) |
|
441 apply (rule wf_Un) |
|
442 apply (cut_tac L_new_r_subset [of fn r i], simp add: Lset_new_eq, blast) |
|
443 apply (rule wf_Un) |
|
444 apply (cut_tac L_new_r_subset [of fn r i], simp add: Lset_new_eq, blast) |
|
445 apply (blast intro: wf_L_new_r) |
|
446 apply (simp add: wf_times Lset_Lset_new_disjoint) |
|
447 apply (blast intro: well_ord_is_wf wf_on_imp_wf) |
|
448 done |
|
449 |
|
450 |
|
451 lemma (in Nat_Times_Nat) L_succ_r_type: |
|
452 "[|Ord(i); r \<subseteq> Lset(i) * Lset(i)|] |
|
453 ==> L_succ_r(fn,r,i) \<subseteq> Lset(succ(i)) * Lset(succ(i))" |
|
454 apply (simp add: L_succ_r_def L_new_r_def measure_def Lset_new_eq) |
|
455 apply (blast intro: Lset_mono_mem [OF succI1, THEN subsetD] ) |
|
456 done |
|
457 |
|
458 |
|
459 subsection{*Transfinite Definition of the Wellordering on @{term "L"}*} |
|
460 |
|
461 constdefs |
|
462 L_r :: "[i, i] => i" |
|
463 "L_r(f,i) == |
|
464 transrec(i, \<lambda>x r. |
|
465 if x=0 then 0 |
|
466 else if Limit(x) then rlimit(x, \<lambda>y. r`y) |
|
467 else L_succ_r(f, r ` Arith.pred(x), Arith.pred(x)))" |
|
468 |
|
469 subsubsection{*The Corresponding Recursion Equations*} |
|
470 lemma [simp]: "L_r(f,0) = 0" |
|
471 by (simp add: def_transrec [OF L_r_def]) |
|
472 |
|
473 lemma [simp]: "Ord(i) ==> L_r(f, succ(i)) = L_succ_r(f, L_r(f,i), i)" |
|
474 by (simp add: def_transrec [OF L_r_def]) |
|
475 |
|
476 text{*Needed to handle the limit case*} |
|
477 lemma L_r_eq: |
|
478 "Ord(i) ==> |
|
479 L_r(f, i) = |
|
480 (if i = 0 then 0 |
|
481 else if Limit(i) then rlimit(i, op `(Lambda(i, L_r(f)))) |
|
482 else L_succ_r (f, Lambda(i, L_r(f)) ` Arith.pred(i), Arith.pred(i)))" |
|
483 apply (induct i rule: trans_induct3_rule) |
|
484 apply (simp_all add: def_transrec [OF L_r_def]) |
|
485 done |
|
486 |
|
487 text{*I don't know why the limit case is so complicated.*} |
|
488 lemma [simp]: "Limit(i) ==> L_r(f,i) = rlimit(i, L_r(f))" |
|
489 apply (simp add: Limit_nonzero def_transrec [OF L_r_def]) |
|
490 apply (rule rlimit_eqI, assumption) |
|
491 apply (rule oallI) |
|
492 apply (frule lt_Ord) |
|
493 apply (simp only: beta ltD L_r_eq [symmetric]) |
|
494 done |
|
495 |
|
496 lemma (in Nat_Times_Nat) L_r_type: |
|
497 "Ord(i) ==> L_r(fn,i) \<subseteq> Lset(i) * Lset(i)" |
|
498 apply (induct i rule: trans_induct3_rule) |
|
499 apply (simp_all add: L_succ_r_type well_ord_L_new_r rlimit_def, blast) |
|
500 done |
|
501 |
|
502 lemma (in Nat_Times_Nat) well_ord_L_r: |
|
503 "Ord(i) ==> well_ord(Lset(i), L_r(fn,i))" |
|
504 apply (induct i rule: trans_induct3_rule) |
|
505 apply (simp_all add: well_ord0 L_r_type well_ord_L_new_r well_ord_rlimit ltD) |
|
506 done |
|
507 |
|
508 lemma well_ord_L_r: |
|
509 "Ord(i) ==> \<exists>r. well_ord(Lset(i), r)" |
|
510 apply (insert nat_times_nat_lepoll_nat) |
|
511 apply (unfold lepoll_def) |
|
512 apply (blast intro: exI Nat_Times_Nat.well_ord_L_r Nat_Times_Nat.intro) |
|
513 done |
|
514 |
|
515 |
|
516 text{*Locale for proving results under the assumption @{text "V=L"}*} |
|
517 locale V_equals_L = |
|
518 assumes VL: "L(x)" |
|
519 |
|
520 text{*The Axiom of Choice holds in @{term L}! Or, to be precise, the |
|
521 Wellordering Theorem.*} |
|
522 theorem (in V_equals_L) AC: "\<exists>r. well_ord(x,r)" |
|
523 apply (insert Transset_Lset VL [of x]) |
|
524 apply (simp add: Transset_def L_def) |
|
525 apply (blast dest!: well_ord_L_r intro: well_ord_subset) |
|
526 done |
|
527 |
|
528 end |