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}*}
|
13702
|
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
|