author | webertj |
Tue, 15 Jun 2004 00:06:40 +0200 | |
changeset 14942 | 78ddcbebace1 |
parent 14171 | 0cab06e3bbd0 |
child 16417 | 9bc16273c2d4 |
permissions | -rw-r--r-- |
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 |
||
8 |
theory AC_in_L = Formula: |
|
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{*Well-foundedness*} |
|
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 well-known 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 needed--but 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 |
|
225 |
constdefs |
|
226 |
env_form_r :: "[i,i,i]=>i" |
|
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 |
||
232 |
env_form_map :: "[i,i,i,i]=>i" |
|
233 |
--{*map from (environment, formula) pairs to ordinals*} |
|
234 |
"env_form_map(f,r,A,z) |
|
235 |
== ordermap(list(A) * formula, env_form_r(f,r,A)) ` z" |
|
236 |
||
13702 | 237 |
DPow_ord :: "[i,i,i,i,i]=>o" |
13692 | 238 |
--{*predicate that holds if @{term k} is a valid index for @{term X}*} |
13702 | 239 |
"DPow_ord(f,r,A,X,k) == |
13692 | 240 |
\<exists>env \<in> list(A). \<exists>p \<in> formula. |
241 |
arity(p) \<le> succ(length(env)) & |
|
242 |
X = {x\<in>A. sats(A, p, Cons(x,env))} & |
|
243 |
env_form_map(f,r,A,<env,p>) = k" |
|
244 |
||
13702 | 245 |
DPow_least :: "[i,i,i,i]=>i" |
13692 | 246 |
--{*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
|
247 |
"DPow_least(f,r,A,X) == \<mu> k. DPow_ord(f,r,A,X,k)" |
13692 | 248 |
|
249 |
DPow_r :: "[i,i,i]=>i" |
|
250 |
--{*a wellordering on @{term "DPow(A)"}*} |
|
13702 | 251 |
"DPow_r(f,r,A) == measure(DPow(A), DPow_least(f,r,A))" |
13692 | 252 |
|
253 |
||
254 |
lemma (in Nat_Times_Nat) well_ord_env_form_r: |
|
255 |
"well_ord(A,r) |
|
256 |
==> well_ord(list(A) * formula, env_form_r(fn,r,A))" |
|
257 |
by (simp add: env_form_r_def well_ord_rmult well_ord_rlist well_ord_formula) |
|
258 |
||
259 |
lemma (in Nat_Times_Nat) Ord_env_form_map: |
|
260 |
"[|well_ord(A,r); z \<in> list(A) * formula|] |
|
261 |
==> Ord(env_form_map(fn,r,A,z))" |
|
262 |
by (simp add: env_form_map_def Ord_ordermap well_ord_env_form_r) |
|
263 |
||
13702 | 264 |
lemma DPow_imp_ex_DPow_ord: |
265 |
"X \<in> DPow(A) ==> \<exists>k. DPow_ord(fn,r,A,X,k)" |
|
266 |
apply (simp add: DPow_ord_def) |
|
13692 | 267 |
apply (blast dest!: DPowD) |
268 |
done |
|
269 |
||
13702 | 270 |
lemma (in Nat_Times_Nat) DPow_ord_imp_Ord: |
271 |
"[|DPow_ord(fn,r,A,X,k); well_ord(A,r)|] ==> Ord(k)" |
|
272 |
apply (simp add: DPow_ord_def, clarify) |
|
13692 | 273 |
apply (simp add: Ord_env_form_map) |
13543 | 274 |
done |
275 |
||
13702 | 276 |
lemma (in Nat_Times_Nat) DPow_imp_DPow_least: |
13692 | 277 |
"[|X \<in> DPow(A); well_ord(A,r)|] |
13702 | 278 |
==> DPow_ord(fn, r, A, X, DPow_least(fn,r,A,X))" |
279 |
apply (simp add: DPow_least_def) |
|
280 |
apply (blast dest: DPow_imp_ex_DPow_ord intro: DPow_ord_imp_Ord LeastI) |
|
13692 | 281 |
done |
282 |
||
283 |
lemma (in Nat_Times_Nat) env_form_map_inject: |
|
284 |
"[|env_form_map(fn,r,A,u) = env_form_map(fn,r,A,v); well_ord(A,r); |
|
285 |
u \<in> list(A) * formula; v \<in> list(A) * formula|] |
|
286 |
==> u=v" |
|
287 |
apply (simp add: env_form_map_def) |
|
288 |
apply (rule inj_apply_equality [OF bij_is_inj, OF ordermap_bij, |
|
289 |
OF well_ord_env_form_r], assumption+) |
|
290 |
done |
|
291 |
||
13702 | 292 |
lemma (in Nat_Times_Nat) DPow_ord_unique: |
293 |
"[|DPow_ord(fn,r,A,X,k); DPow_ord(fn,r,A,Y,k); well_ord(A,r)|] |
|
13692 | 294 |
==> X=Y" |
13702 | 295 |
apply (simp add: DPow_ord_def, clarify) |
13692 | 296 |
apply (drule env_form_map_inject, auto) |
297 |
done |
|
298 |
||
13702 | 299 |
lemma (in Nat_Times_Nat) well_ord_DPow_r: |
300 |
"well_ord(A,r) ==> well_ord(DPow(A), DPow_r(fn,r,A))" |
|
301 |
apply (simp add: DPow_r_def) |
|
13692 | 302 |
apply (rule well_ord_measure) |
13702 | 303 |
apply (simp add: DPow_least_def Ord_Least) |
304 |
apply (drule DPow_imp_DPow_least, assumption)+ |
|
13692 | 305 |
apply simp |
13702 | 306 |
apply (blast intro: DPow_ord_unique) |
13692 | 307 |
done |
308 |
||
309 |
lemma (in Nat_Times_Nat) DPow_r_type: |
|
13702 | 310 |
"DPow_r(fn,r,A) \<subseteq> DPow(A) * DPow(A)" |
311 |
by (simp add: DPow_r_def measure_def, blast) |
|
13692 | 312 |
|
13543 | 313 |
|
314 |
subsection{*Limit Construction for Well-Orderings*} |
|
315 |
||
316 |
text{*Now we work towards the transfinite definition of wellorderings for |
|
317 |
@{term "Lset(i)"}. We assume as an inductive hypothesis that there is a family |
|
318 |
of wellorderings for smaller ordinals.*} |
|
319 |
||
320 |
constdefs |
|
13692 | 321 |
rlimit :: "[i,i=>i]=>i" |
13702 | 322 |
--{*Expresses the wellordering at limit ordinals. The conditional |
323 |
lets us remove the premise @{term "Limit(i)"} from some theorems.*} |
|
13692 | 324 |
"rlimit(i,r) == |
13702 | 325 |
if Limit(i) then |
326 |
{z: Lset(i) * Lset(i). |
|
327 |
\<exists>x' x. z = <x',x> & |
|
328 |
(lrank(x') < lrank(x) | |
|
329 |
(lrank(x') = lrank(x) & <x',x> \<in> r(succ(lrank(x)))))} |
|
330 |
else 0" |
|
13692 | 331 |
|
13543 | 332 |
Lset_new :: "i=>i" |
13692 | 333 |
--{*This constant denotes the set of elements introduced at level |
334 |
@{term "succ(i)"}*} |
|
13543 | 335 |
"Lset_new(i) == {x \<in> Lset(succ(i)). lrank(x) = i}" |
336 |
||
337 |
lemma Limit_Lset_eq2: |
|
338 |
"Limit(i) ==> Lset(i) = (\<Union>j\<in>i. Lset_new(j))" |
|
13692 | 339 |
apply (simp add: Limit_Lset_eq) |
13543 | 340 |
apply (rule equalityI) |
341 |
apply safe |
|
342 |
apply (subgoal_tac "Ord(y)") |
|
343 |
prefer 2 apply (blast intro: Ord_in_Ord Limit_is_Ord) |
|
13692 | 344 |
apply (simp_all add: Limit_is_Ord Lset_iff_lrank_lt Lset_new_def |
345 |
Ord_mem_iff_lt) |
|
346 |
apply (blast intro: lt_trans) |
|
13543 | 347 |
apply (rule_tac x = "succ(lrank(x))" in bexI) |
13692 | 348 |
apply (simp add: Lset_succ_lrank_iff) |
349 |
apply (blast intro: Limit_has_succ ltD) |
|
13543 | 350 |
done |
351 |
||
352 |
lemma wf_on_Lset: |
|
353 |
"wf[Lset(succ(j))](r(succ(j))) ==> wf[Lset_new(j)](rlimit(i,r))" |
|
13692 | 354 |
apply (simp add: wf_on_def Lset_new_def) |
355 |
apply (erule wf_subset) |
|
13702 | 356 |
apply (simp add: rlimit_def, force) |
13543 | 357 |
done |
358 |
||
359 |
lemma wf_on_rlimit: |
|
13702 | 360 |
"(\<forall>j<i. wf[Lset(j)](r(j))) ==> wf[Lset(i)](rlimit(i,r))" |
361 |
apply (case_tac "Limit(i)") |
|
362 |
prefer 2 |
|
363 |
apply (simp add: rlimit_def wf_on_any_0) |
|
13543 | 364 |
apply (simp add: Limit_Lset_eq2) |
365 |
apply (rule wf_on_Union) |
|
13692 | 366 |
apply (rule wf_imp_wf_on [OF wf_Memrel [of i]]) |
367 |
apply (blast intro: wf_on_Lset Limit_has_succ Limit_is_Ord ltI) |
|
13543 | 368 |
apply (force simp add: rlimit_def Limit_is_Ord Lset_iff_lrank_lt Lset_new_def |
369 |
Ord_mem_iff_lt) |
|
370 |
done |
|
371 |
||
372 |
lemma linear_rlimit: |
|
373 |
"[|Limit(i); \<forall>j<i. linear(Lset(j), r(j)) |] |
|
374 |
==> linear(Lset(i), rlimit(i,r))" |
|
13692 | 375 |
apply (frule Limit_is_Ord) |
376 |
apply (simp add: Limit_Lset_eq2 Lset_new_def) |
|
377 |
apply (simp add: linear_def rlimit_def Ball_def lt_Ord Lset_iff_lrank_lt) |
|
378 |
apply (simp add: ltI, clarify) |
|
379 |
apply (rename_tac u v) |
|
380 |
apply (rule_tac i="lrank(u)" and j="lrank(v)" in Ord_linear_lt, simp_all) |
|
381 |
apply (drule_tac x="succ(lrank(u) Un lrank(v))" in ospec) |
|
382 |
apply (simp add: ltI) |
|
383 |
apply (drule_tac x=u in spec, simp) |
|
384 |
apply (drule_tac x=v in spec, simp) |
|
13543 | 385 |
done |
386 |
||
387 |
lemma well_ord_rlimit: |
|
388 |
"[|Limit(i); \<forall>j<i. well_ord(Lset(j), r(j)) |] |
|
389 |
==> well_ord(Lset(i), rlimit(i,r))" |
|
13692 | 390 |
by (blast intro: well_ordI wf_on_rlimit well_ord_is_wf |
391 |
linear_rlimit well_ord_is_linear) |
|
13543 | 392 |
|
13702 | 393 |
lemma rlimit_cong: |
394 |
"(!!j. j<i ==> r'(j) = r(j)) ==> rlimit(i,r) = rlimit(i,r')" |
|
395 |
apply (simp add: rlimit_def, clarify) |
|
396 |
apply (rule refl iff_refl Collect_cong ex_cong conj_cong)+ |
|
397 |
apply (simp add: Limit_is_Ord Lset_lrank_lt) |
|
398 |
done |
|
399 |
||
13543 | 400 |
|
401 |
subsection{*Transfinite Definition of the Wellordering on @{term "L"}*} |
|
402 |
||
403 |
constdefs |
|
404 |
L_r :: "[i, i] => i" |
|
13702 | 405 |
"L_r(f) == %i. |
406 |
transrec3(i, 0, \<lambda>x r. DPow_r(f, r, Lset(x)), |
|
407 |
\<lambda>x r. rlimit(x, \<lambda>y. r`y))" |
|
13543 | 408 |
|
409 |
subsubsection{*The Corresponding Recursion Equations*} |
|
410 |
lemma [simp]: "L_r(f,0) = 0" |
|
13702 | 411 |
by (simp add: L_r_def) |
13543 | 412 |
|
13702 | 413 |
lemma [simp]: "L_r(f, succ(i)) = DPow_r(f, L_r(f,i), Lset(i))" |
414 |
by (simp add: L_r_def) |
|
13543 | 415 |
|
13702 | 416 |
text{*The limit case is non-trivial because of the distinction between |
417 |
object-level and meta-level abstraction.*} |
|
13543 | 418 |
lemma [simp]: "Limit(i) ==> L_r(f,i) = rlimit(i, L_r(f))" |
13702 | 419 |
by (simp cong: rlimit_cong add: transrec3_Limit L_r_def ltD) |
13543 | 420 |
|
421 |
lemma (in Nat_Times_Nat) L_r_type: |
|
422 |
"Ord(i) ==> L_r(fn,i) \<subseteq> Lset(i) * Lset(i)" |
|
423 |
apply (induct i rule: trans_induct3_rule) |
|
13692 | 424 |
apply (simp_all add: Lset_succ DPow_r_type well_ord_DPow_r rlimit_def |
425 |
Transset_subset_DPow [OF Transset_Lset], blast) |
|
13543 | 426 |
done |
427 |
||
428 |
lemma (in Nat_Times_Nat) well_ord_L_r: |
|
429 |
"Ord(i) ==> well_ord(Lset(i), L_r(fn,i))" |
|
430 |
apply (induct i rule: trans_induct3_rule) |
|
13692 | 431 |
apply (simp_all add: well_ord0 Lset_succ L_r_type well_ord_DPow_r |
432 |
well_ord_rlimit ltD) |
|
13543 | 433 |
done |
434 |
||
435 |
lemma well_ord_L_r: |
|
436 |
"Ord(i) ==> \<exists>r. well_ord(Lset(i), r)" |
|
437 |
apply (insert nat_times_nat_lepoll_nat) |
|
438 |
apply (unfold lepoll_def) |
|
13692 | 439 |
apply (blast intro: Nat_Times_Nat.well_ord_L_r Nat_Times_Nat.intro) |
13543 | 440 |
done |
441 |
||
442 |
||
443 |
text{*Locale for proving results under the assumption @{text "V=L"}*} |
|
444 |
locale V_equals_L = |
|
445 |
assumes VL: "L(x)" |
|
446 |
||
447 |
text{*The Axiom of Choice holds in @{term L}! Or, to be precise, the |
|
448 |
Wellordering Theorem.*} |
|
449 |
theorem (in V_equals_L) AC: "\<exists>r. well_ord(x,r)" |
|
13692 | 450 |
apply (insert Transset_Lset VL [of x]) |
13543 | 451 |
apply (simp add: Transset_def L_def) |
13692 | 452 |
apply (blast dest!: well_ord_L_r intro: well_ord_subset) |
13543 | 453 |
done |
454 |
||
455 |
end |