13543
|
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 |
|
13546
|
435 |
lemma (in Nat_Times_Nat) well_ord_L_succ_r:
|
13543
|
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)
|
13546
|
499 |
apply (simp_all add: L_succ_r_type well_ord_L_succ_r rlimit_def, blast)
|
13543
|
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)
|
13546
|
505 |
apply (simp_all add: well_ord0 L_r_type well_ord_L_succ_r well_ord_rlimit ltD)
|
13543
|
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
|