author | blanchet |
Wed, 27 Aug 2014 08:41:12 +0200 | |
changeset 58043 | a90847f03ec8 |
parent 47085 | 4a8a8b9bf414 |
child 58871 | c399ae4b836f |
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 |
||
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{*Well-foundedness*} |
|
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 well-known 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 needed--but 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 tab-width;
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 Well-Orderings*} |
|
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 tab-width;
wenzelm
parents:
21404
diff
changeset
|
339 |
{z: Lset(i) * Lset(i). |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
21404
diff
changeset
|
340 |
\<exists>x' x. z = <x',x> & |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
21404
diff
changeset
|
341 |
(lrank(x') < lrank(x) | |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
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 non-trivial because of the distinction between |
431 |
object-level and meta-level 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 well-ordered! 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 |