author | wenzelm |
Sat, 17 Oct 2009 14:43:18 +0200 | |
changeset 32960 | 69916a850301 |
parent 21404 | eb85850d3eb7 |
child 46823 | 57bf0cecb366 |
permissions | -rw-r--r-- |
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 |
||
16417 | 7 |
theory AC_in_L imports Formula 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: |
|
47 |
"linear(A,r) ==> linear(list(A),rlist(A,r))" |
|
48 |
apply (simp (no_asm_simp) add: linear_def) |
|
13692 | 49 |
apply (rule ballI) |
50 |
apply (induct_tac x) |
|
51 |
apply (rule ballI) |
|
52 |
apply (induct_tac y) |
|
53 |
apply (simp_all add: shorterI) |
|
54 |
apply (rule ballI) |
|
55 |
apply (erule_tac a=y in list.cases) |
|
56 |
apply (rename_tac [2] a2 l2) |
|
13543 | 57 |
apply (rule_tac [2] i = "length(l)" and j = "length(l2)" in Ord_linear_lt) |
13692 | 58 |
apply (simp_all add: shorterI) |
59 |
apply (erule_tac x=a and y=a2 in linearE) |
|
60 |
apply (simp_all add: diffI) |
|
61 |
apply (blast intro: sameI) |
|
13543 | 62 |
done |
63 |
||
64 |
||
65 |
subsubsection{*Well-foundedness*} |
|
66 |
||
67 |
text{*Nothing preceeds Nil in this ordering.*} |
|
68 |
inductive_cases rlist_NilE: " <l,[]> \<in> rlist(A,r)" |
|
69 |
||
70 |
inductive_cases rlist_ConsE: " <l', Cons(x,l)> \<in> rlist(A,r)" |
|
71 |
||
72 |
lemma not_rlist_Nil [simp]: " <l,[]> \<notin> rlist(A,r)" |
|
73 |
by (blast intro: elim: rlist_NilE) |
|
74 |
||
75 |
lemma rlist_imp_length_le: "<l',l> \<in> rlist(A,r) ==> length(l') \<le> length(l)" |
|
76 |
apply (erule rlist.induct) |
|
13692 | 77 |
apply (simp_all add: leI) |
13543 | 78 |
done |
79 |
||
80 |
lemma wf_on_rlist_n: |
|
81 |
"[| n \<in> nat; wf[A](r) |] ==> wf[{l \<in> list(A). length(l) = n}](rlist(A,r))" |
|
13692 | 82 |
apply (induct_tac n) |
83 |
apply (rule wf_onI2, simp) |
|
84 |
apply (rule wf_onI2, clarify) |
|
85 |
apply (erule_tac a=y in list.cases, clarify) |
|
13543 | 86 |
apply (simp (no_asm_use)) |
13692 | 87 |
apply clarify |
13543 | 88 |
apply (simp (no_asm_use)) |
89 |
apply (subgoal_tac "\<forall>l2 \<in> list(A). length(l2) = x --> Cons(a,l2) \<in> B", blast) |
|
90 |
apply (erule_tac a=a in wf_on_induct, assumption) |
|
91 |
apply (rule ballI) |
|
13692 | 92 |
apply (rule impI) |
13543 | 93 |
apply (erule_tac a=l2 in wf_on_induct, blast, clarify) |
13692 | 94 |
apply (rename_tac a' l2 l') |
95 |
apply (drule_tac x="Cons(a',l')" in bspec, typecheck) |
|
96 |
apply simp |
|
97 |
apply (erule mp, clarify) |
|
13543 | 98 |
apply (erule rlist_ConsE, auto) |
99 |
done |
|
100 |
||
101 |
lemma list_eq_UN_length: "list(A) = (\<Union>n\<in>nat. {l \<in> list(A). length(l) = n})" |
|
102 |
by (blast intro: length_type) |
|
103 |
||
104 |
||
105 |
lemma wf_on_rlist: "wf[A](r) ==> wf[list(A)](rlist(A,r))" |
|
13692 | 106 |
apply (subst list_eq_UN_length) |
107 |
apply (rule wf_on_Union) |
|
13543 | 108 |
apply (rule wf_imp_wf_on [OF wf_Memrel [of nat]]) |
109 |
apply (simp add: wf_on_rlist_n) |
|
13692 | 110 |
apply (frule rlist_type [THEN subsetD]) |
111 |
apply (simp add: length_type) |
|
13543 | 112 |
apply (drule rlist_imp_length_le) |
13692 | 113 |
apply (erule leE) |
114 |
apply (simp_all add: lt_def) |
|
13543 | 115 |
done |
116 |
||
117 |
||
118 |
lemma wf_rlist: "wf(r) ==> wf(rlist(field(r),r))" |
|
119 |
apply (simp add: wf_iff_wf_on_field) |
|
120 |
apply (rule wf_on_subset_A [OF _ field_rlist]) |
|
13692 | 121 |
apply (blast intro: wf_on_rlist) |
13543 | 122 |
done |
123 |
||
124 |
lemma well_ord_rlist: |
|
125 |
"well_ord(A,r) ==> well_ord(list(A), rlist(A,r))" |
|
126 |
apply (rule well_ordI) |
|
127 |
apply (simp add: well_ord_def wf_on_rlist) |
|
128 |
apply (simp add: well_ord_def tot_ord_def linear_rlist) |
|
129 |
done |
|
130 |
||
131 |
||
132 |
subsection{*An Injection from Formulas into the Natural Numbers*} |
|
133 |
||
134 |
text{*There is a well-known bijection between @{term "nat*nat"} and @{term |
|
135 |
nat} given by the expression f(m,n) = triangle(m+n) + m, where triangle(k) |
|
136 |
enumerates the triangular numbers and can be defined by triangle(0)=0, |
|
137 |
triangle(succ(k)) = succ(k + triangle(k)). Some small amount of effort is |
|
13692 | 138 |
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}: |
139 |
@{thm[display] well_ord_InfCard_square_eq[no_vars]} |
|
13543 | 140 |
|
13692 | 141 |
However, this result merely states that there is a bijection between the two |
142 |
sets. It provides no means of naming a specific bijection. Therefore, we |
|
143 |
conduct the proofs under the assumption that a bijection exists. The simplest |
|
144 |
way to organize this is to use a locale.*} |
|
145 |
||
146 |
text{*Locale for any arbitrary injection between @{term "nat*nat"} |
|
13543 | 147 |
and @{term nat}*} |
148 |
locale Nat_Times_Nat = |
|
149 |
fixes fn |
|
150 |
assumes fn_inj: "fn \<in> inj(nat*nat, nat)" |
|
151 |
||
152 |
||
153 |
consts enum :: "[i,i]=>i" |
|
154 |
primrec |
|
155 |
"enum(f, Member(x,y)) = f ` <0, f ` <x,y>>" |
|
156 |
"enum(f, Equal(x,y)) = f ` <1, f ` <x,y>>" |
|
157 |
"enum(f, Nand(p,q)) = f ` <2, f ` <enum(f,p), enum(f,q)>>" |
|
158 |
"enum(f, Forall(p)) = f ` <succ(2), enum(f,p)>" |
|
159 |
||
160 |
lemma (in Nat_Times_Nat) fn_type [TC,simp]: |
|
161 |
"[|x \<in> nat; y \<in> nat|] ==> fn`<x,y> \<in> nat" |
|
13692 | 162 |
by (blast intro: inj_is_fun [OF fn_inj] apply_funtype) |
13543 | 163 |
|
164 |
lemma (in Nat_Times_Nat) fn_iff: |
|
13692 | 165 |
"[|x \<in> nat; y \<in> nat; u \<in> nat; v \<in> nat|] |
13543 | 166 |
==> (fn`<x,y> = fn`<u,v>) <-> (x=u & y=v)" |
13692 | 167 |
by (blast dest: inj_apply_equality [OF fn_inj]) |
13543 | 168 |
|
169 |
lemma (in Nat_Times_Nat) enum_type [TC,simp]: |
|
170 |
"p \<in> formula ==> enum(fn,p) \<in> nat" |
|
13692 | 171 |
by (induct_tac p, simp_all) |
13543 | 172 |
|
173 |
lemma (in Nat_Times_Nat) enum_inject [rule_format]: |
|
174 |
"p \<in> formula ==> \<forall>q\<in>formula. enum(fn,p) = enum(fn,q) --> p=q" |
|
13692 | 175 |
apply (induct_tac p, simp_all) |
176 |
apply (rule ballI) |
|
177 |
apply (erule formula.cases) |
|
178 |
apply (simp_all add: fn_iff) |
|
179 |
apply (rule ballI) |
|
180 |
apply (erule formula.cases) |
|
181 |
apply (simp_all add: fn_iff) |
|
182 |
apply (rule ballI) |
|
183 |
apply (erule_tac a=qa in formula.cases) |
|
184 |
apply (simp_all add: fn_iff) |
|
185 |
apply blast |
|
186 |
apply (rule ballI) |
|
187 |
apply (erule_tac a=q in formula.cases) |
|
188 |
apply (simp_all add: fn_iff, blast) |
|
13543 | 189 |
done |
190 |
||
191 |
lemma (in Nat_Times_Nat) inj_formula_nat: |
|
192 |
"(\<lambda>p \<in> formula. enum(fn,p)) \<in> inj(formula, nat)" |
|
13692 | 193 |
apply (simp add: inj_def lam_type) |
194 |
apply (blast intro: enum_inject) |
|
13543 | 195 |
done |
196 |
||
197 |
lemma (in Nat_Times_Nat) well_ord_formula: |
|
198 |
"well_ord(formula, measure(formula, enum(fn)))" |
|
199 |
apply (rule well_ord_measure, simp) |
|
13692 | 200 |
apply (blast intro: enum_inject) |
13543 | 201 |
done |
202 |
||
203 |
lemmas nat_times_nat_lepoll_nat = |
|
204 |
InfCard_nat [THEN InfCard_square_eqpoll, THEN eqpoll_imp_lepoll] |
|
205 |
||
206 |
||
207 |
text{*Not needed--but interesting?*} |
|
208 |
theorem formula_lepoll_nat: "formula \<lesssim> nat" |
|
209 |
apply (insert nat_times_nat_lepoll_nat) |
|
210 |
apply (unfold lepoll_def) |
|
13692 | 211 |
apply (blast intro: Nat_Times_Nat.inj_formula_nat Nat_Times_Nat.intro) |
212 |
done |
|
213 |
||
214 |
||
215 |
subsection{*Defining the Wellordering on @{term "DPow(A)"}*} |
|
216 |
||
217 |
text{*The objective is to build a wellordering on @{term "DPow(A)"} from a |
|
218 |
given one on @{term A}. We first introduce wellorderings for environments, |
|
219 |
which are lists built over @{term "A"}. We combine it with the enumeration of |
|
220 |
formulas. The order type of the resulting wellordering gives us a map from |
|
221 |
(environment, formula) pairs into the ordinals. For each member of @{term |
|
13702 | 222 |
"DPow(A)"}, we take the minimum such ordinal.*} |
13692 | 223 |
|
21233 | 224 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
225 |
env_form_r :: "[i,i,i]=>i" where |
13692 | 226 |
--{*wellordering on (environment, formula) pairs*} |
227 |
"env_form_r(f,r,A) == |
|
228 |
rmult(list(A), rlist(A, r), |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
21404
diff
changeset
|
229 |
formula, measure(formula, enum(f)))" |
13692 | 230 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
231 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
232 |
env_form_map :: "[i,i,i,i]=>i" where |
13692 | 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 |
||
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
237 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
238 |
DPow_ord :: "[i,i,i,i,i]=>o" where |
13692 | 239 |
--{*predicate that holds if @{term k} is a valid index for @{term X}*} |
13702 | 240 |
"DPow_ord(f,r,A,X,k) == |
13692 | 241 |
\<exists>env \<in> list(A). \<exists>p \<in> formula. |
242 |
arity(p) \<le> succ(length(env)) & |
|
243 |
X = {x\<in>A. sats(A, p, Cons(x,env))} & |
|
244 |
env_form_map(f,r,A,<env,p>) = k" |
|
245 |
||
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
246 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
247 |
DPow_least :: "[i,i,i,i]=>i" where |
13692 | 248 |
--{*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
|
249 |
"DPow_least(f,r,A,X) == \<mu> k. DPow_ord(f,r,A,X,k)" |
13692 | 250 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
251 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
252 |
DPow_r :: "[i,i,i]=>i" where |
13692 | 253 |
--{*a wellordering on @{term "DPow(A)"}*} |
13702 | 254 |
"DPow_r(f,r,A) == measure(DPow(A), DPow_least(f,r,A))" |
13692 | 255 |
|
256 |
||
257 |
lemma (in Nat_Times_Nat) well_ord_env_form_r: |
|
258 |
"well_ord(A,r) |
|
259 |
==> well_ord(list(A) * formula, env_form_r(fn,r,A))" |
|
260 |
by (simp add: env_form_r_def well_ord_rmult well_ord_rlist well_ord_formula) |
|
261 |
||
262 |
lemma (in Nat_Times_Nat) Ord_env_form_map: |
|
263 |
"[|well_ord(A,r); z \<in> list(A) * formula|] |
|
264 |
==> Ord(env_form_map(fn,r,A,z))" |
|
265 |
by (simp add: env_form_map_def Ord_ordermap well_ord_env_form_r) |
|
266 |
||
13702 | 267 |
lemma DPow_imp_ex_DPow_ord: |
268 |
"X \<in> DPow(A) ==> \<exists>k. DPow_ord(fn,r,A,X,k)" |
|
269 |
apply (simp add: DPow_ord_def) |
|
13692 | 270 |
apply (blast dest!: DPowD) |
271 |
done |
|
272 |
||
13702 | 273 |
lemma (in Nat_Times_Nat) DPow_ord_imp_Ord: |
274 |
"[|DPow_ord(fn,r,A,X,k); well_ord(A,r)|] ==> Ord(k)" |
|
275 |
apply (simp add: DPow_ord_def, clarify) |
|
13692 | 276 |
apply (simp add: Ord_env_form_map) |
13543 | 277 |
done |
278 |
||
13702 | 279 |
lemma (in Nat_Times_Nat) DPow_imp_DPow_least: |
13692 | 280 |
"[|X \<in> DPow(A); well_ord(A,r)|] |
13702 | 281 |
==> DPow_ord(fn, r, A, X, DPow_least(fn,r,A,X))" |
282 |
apply (simp add: DPow_least_def) |
|
283 |
apply (blast dest: DPow_imp_ex_DPow_ord intro: DPow_ord_imp_Ord LeastI) |
|
13692 | 284 |
done |
285 |
||
286 |
lemma (in Nat_Times_Nat) env_form_map_inject: |
|
287 |
"[|env_form_map(fn,r,A,u) = env_form_map(fn,r,A,v); well_ord(A,r); |
|
288 |
u \<in> list(A) * formula; v \<in> list(A) * formula|] |
|
289 |
==> u=v" |
|
290 |
apply (simp add: env_form_map_def) |
|
291 |
apply (rule inj_apply_equality [OF bij_is_inj, OF ordermap_bij, |
|
292 |
OF well_ord_env_form_r], assumption+) |
|
293 |
done |
|
294 |
||
13702 | 295 |
lemma (in Nat_Times_Nat) DPow_ord_unique: |
296 |
"[|DPow_ord(fn,r,A,X,k); DPow_ord(fn,r,A,Y,k); well_ord(A,r)|] |
|
13692 | 297 |
==> X=Y" |
13702 | 298 |
apply (simp add: DPow_ord_def, clarify) |
13692 | 299 |
apply (drule env_form_map_inject, auto) |
300 |
done |
|
301 |
||
13702 | 302 |
lemma (in Nat_Times_Nat) well_ord_DPow_r: |
303 |
"well_ord(A,r) ==> well_ord(DPow(A), DPow_r(fn,r,A))" |
|
304 |
apply (simp add: DPow_r_def) |
|
13692 | 305 |
apply (rule well_ord_measure) |
13702 | 306 |
apply (simp add: DPow_least_def Ord_Least) |
307 |
apply (drule DPow_imp_DPow_least, assumption)+ |
|
13692 | 308 |
apply simp |
13702 | 309 |
apply (blast intro: DPow_ord_unique) |
13692 | 310 |
done |
311 |
||
312 |
lemma (in Nat_Times_Nat) DPow_r_type: |
|
13702 | 313 |
"DPow_r(fn,r,A) \<subseteq> DPow(A) * DPow(A)" |
314 |
by (simp add: DPow_r_def measure_def, blast) |
|
13692 | 315 |
|
13543 | 316 |
|
317 |
subsection{*Limit Construction for Well-Orderings*} |
|
318 |
||
319 |
text{*Now we work towards the transfinite definition of wellorderings for |
|
320 |
@{term "Lset(i)"}. We assume as an inductive hypothesis that there is a family |
|
321 |
of wellorderings for smaller ordinals.*} |
|
322 |
||
21233 | 323 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
324 |
rlimit :: "[i,i=>i]=>i" where |
13702 | 325 |
--{*Expresses the wellordering at limit ordinals. The conditional |
326 |
lets us remove the premise @{term "Limit(i)"} from some theorems.*} |
|
13692 | 327 |
"rlimit(i,r) == |
13702 | 328 |
if Limit(i) then |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
21404
diff
changeset
|
329 |
{z: Lset(i) * Lset(i). |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
21404
diff
changeset
|
330 |
\<exists>x' x. z = <x',x> & |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
21404
diff
changeset
|
331 |
(lrank(x') < lrank(x) | |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
21404
diff
changeset
|
332 |
(lrank(x') = lrank(x) & <x',x> \<in> r(succ(lrank(x)))))} |
13702 | 333 |
else 0" |
13692 | 334 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
335 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
336 |
Lset_new :: "i=>i" where |
13692 | 337 |
--{*This constant denotes the set of elements introduced at level |
338 |
@{term "succ(i)"}*} |
|
13543 | 339 |
"Lset_new(i) == {x \<in> Lset(succ(i)). lrank(x) = i}" |
340 |
||
341 |
lemma Limit_Lset_eq2: |
|
342 |
"Limit(i) ==> Lset(i) = (\<Union>j\<in>i. Lset_new(j))" |
|
13692 | 343 |
apply (simp add: Limit_Lset_eq) |
13543 | 344 |
apply (rule equalityI) |
345 |
apply safe |
|
346 |
apply (subgoal_tac "Ord(y)") |
|
347 |
prefer 2 apply (blast intro: Ord_in_Ord Limit_is_Ord) |
|
13692 | 348 |
apply (simp_all add: Limit_is_Ord Lset_iff_lrank_lt Lset_new_def |
349 |
Ord_mem_iff_lt) |
|
350 |
apply (blast intro: lt_trans) |
|
13543 | 351 |
apply (rule_tac x = "succ(lrank(x))" in bexI) |
13692 | 352 |
apply (simp add: Lset_succ_lrank_iff) |
353 |
apply (blast intro: Limit_has_succ ltD) |
|
13543 | 354 |
done |
355 |
||
356 |
lemma wf_on_Lset: |
|
357 |
"wf[Lset(succ(j))](r(succ(j))) ==> wf[Lset_new(j)](rlimit(i,r))" |
|
13692 | 358 |
apply (simp add: wf_on_def Lset_new_def) |
359 |
apply (erule wf_subset) |
|
13702 | 360 |
apply (simp add: rlimit_def, force) |
13543 | 361 |
done |
362 |
||
363 |
lemma wf_on_rlimit: |
|
13702 | 364 |
"(\<forall>j<i. wf[Lset(j)](r(j))) ==> wf[Lset(i)](rlimit(i,r))" |
365 |
apply (case_tac "Limit(i)") |
|
366 |
prefer 2 |
|
367 |
apply (simp add: rlimit_def wf_on_any_0) |
|
13543 | 368 |
apply (simp add: Limit_Lset_eq2) |
369 |
apply (rule wf_on_Union) |
|
13692 | 370 |
apply (rule wf_imp_wf_on [OF wf_Memrel [of i]]) |
371 |
apply (blast intro: wf_on_Lset Limit_has_succ Limit_is_Ord ltI) |
|
13543 | 372 |
apply (force simp add: rlimit_def Limit_is_Ord Lset_iff_lrank_lt Lset_new_def |
373 |
Ord_mem_iff_lt) |
|
374 |
done |
|
375 |
||
376 |
lemma linear_rlimit: |
|
377 |
"[|Limit(i); \<forall>j<i. linear(Lset(j), r(j)) |] |
|
378 |
==> linear(Lset(i), rlimit(i,r))" |
|
13692 | 379 |
apply (frule Limit_is_Ord) |
380 |
apply (simp add: Limit_Lset_eq2 Lset_new_def) |
|
381 |
apply (simp add: linear_def rlimit_def Ball_def lt_Ord Lset_iff_lrank_lt) |
|
382 |
apply (simp add: ltI, clarify) |
|
383 |
apply (rename_tac u v) |
|
384 |
apply (rule_tac i="lrank(u)" and j="lrank(v)" in Ord_linear_lt, simp_all) |
|
385 |
apply (drule_tac x="succ(lrank(u) Un lrank(v))" in ospec) |
|
386 |
apply (simp add: ltI) |
|
387 |
apply (drule_tac x=u in spec, simp) |
|
388 |
apply (drule_tac x=v in spec, simp) |
|
13543 | 389 |
done |
390 |
||
391 |
lemma well_ord_rlimit: |
|
392 |
"[|Limit(i); \<forall>j<i. well_ord(Lset(j), r(j)) |] |
|
393 |
==> well_ord(Lset(i), rlimit(i,r))" |
|
13692 | 394 |
by (blast intro: well_ordI wf_on_rlimit well_ord_is_wf |
395 |
linear_rlimit well_ord_is_linear) |
|
13543 | 396 |
|
13702 | 397 |
lemma rlimit_cong: |
398 |
"(!!j. j<i ==> r'(j) = r(j)) ==> rlimit(i,r) = rlimit(i,r')" |
|
399 |
apply (simp add: rlimit_def, clarify) |
|
400 |
apply (rule refl iff_refl Collect_cong ex_cong conj_cong)+ |
|
401 |
apply (simp add: Limit_is_Ord Lset_lrank_lt) |
|
402 |
done |
|
403 |
||
13543 | 404 |
|
405 |
subsection{*Transfinite Definition of the Wellordering on @{term "L"}*} |
|
406 |
||
21233 | 407 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
408 |
L_r :: "[i, i] => i" where |
13702 | 409 |
"L_r(f) == %i. |
410 |
transrec3(i, 0, \<lambda>x r. DPow_r(f, r, Lset(x)), |
|
411 |
\<lambda>x r. rlimit(x, \<lambda>y. r`y))" |
|
13543 | 412 |
|
413 |
subsubsection{*The Corresponding Recursion Equations*} |
|
414 |
lemma [simp]: "L_r(f,0) = 0" |
|
13702 | 415 |
by (simp add: L_r_def) |
13543 | 416 |
|
13702 | 417 |
lemma [simp]: "L_r(f, succ(i)) = DPow_r(f, L_r(f,i), Lset(i))" |
418 |
by (simp add: L_r_def) |
|
13543 | 419 |
|
13702 | 420 |
text{*The limit case is non-trivial because of the distinction between |
421 |
object-level and meta-level abstraction.*} |
|
13543 | 422 |
lemma [simp]: "Limit(i) ==> L_r(f,i) = rlimit(i, L_r(f))" |
13702 | 423 |
by (simp cong: rlimit_cong add: transrec3_Limit L_r_def ltD) |
13543 | 424 |
|
425 |
lemma (in Nat_Times_Nat) L_r_type: |
|
426 |
"Ord(i) ==> L_r(fn,i) \<subseteq> Lset(i) * Lset(i)" |
|
427 |
apply (induct i rule: trans_induct3_rule) |
|
13692 | 428 |
apply (simp_all add: Lset_succ DPow_r_type well_ord_DPow_r rlimit_def |
429 |
Transset_subset_DPow [OF Transset_Lset], blast) |
|
13543 | 430 |
done |
431 |
||
432 |
lemma (in Nat_Times_Nat) well_ord_L_r: |
|
433 |
"Ord(i) ==> well_ord(Lset(i), L_r(fn,i))" |
|
434 |
apply (induct i rule: trans_induct3_rule) |
|
13692 | 435 |
apply (simp_all add: well_ord0 Lset_succ L_r_type well_ord_DPow_r |
436 |
well_ord_rlimit ltD) |
|
13543 | 437 |
done |
438 |
||
439 |
lemma well_ord_L_r: |
|
440 |
"Ord(i) ==> \<exists>r. well_ord(Lset(i), r)" |
|
441 |
apply (insert nat_times_nat_lepoll_nat) |
|
442 |
apply (unfold lepoll_def) |
|
13692 | 443 |
apply (blast intro: Nat_Times_Nat.well_ord_L_r Nat_Times_Nat.intro) |
13543 | 444 |
done |
445 |
||
446 |
||
447 |
text{*Locale for proving results under the assumption @{text "V=L"}*} |
|
448 |
locale V_equals_L = |
|
449 |
assumes VL: "L(x)" |
|
450 |
||
451 |
text{*The Axiom of Choice holds in @{term L}! Or, to be precise, the |
|
452 |
Wellordering Theorem.*} |
|
453 |
theorem (in V_equals_L) AC: "\<exists>r. well_ord(x,r)" |
|
13692 | 454 |
apply (insert Transset_Lset VL [of x]) |
13543 | 455 |
apply (simp add: Transset_def L_def) |
13692 | 456 |
apply (blast dest!: well_ord_L_r intro: well_ord_subset) |
13543 | 457 |
done |
458 |
||
459 |
end |