29 l' \<in> list(A); l \<in> list(A); a' \<in> A; a \<in> A |] |
29 l' \<in> list(A); l \<in> list(A); a' \<in> A; a \<in> A |] |
30 ==> <Cons(a',l'), Cons(a,l)> \<in> rlist(A,r)" |
30 ==> <Cons(a',l'), Cons(a,l)> \<in> rlist(A,r)" |
31 type_intros list.intros |
31 type_intros list.intros |
32 |
32 |
33 |
33 |
34 subsubsection{*Type checking*} |
34 subsubsection\<open>Type checking\<close> |
35 |
35 |
36 lemmas rlist_type = rlist.dom_subset |
36 lemmas rlist_type = rlist.dom_subset |
37 |
37 |
38 lemmas field_rlist = rlist_type [THEN field_rel_subset] |
38 lemmas field_rlist = rlist_type [THEN field_rel_subset] |
39 |
39 |
40 subsubsection{*Linearity*} |
40 subsubsection\<open>Linearity\<close> |
41 |
41 |
42 lemma rlist_Nil_Cons [intro]: |
42 lemma rlist_Nil_Cons [intro]: |
43 "[|a \<in> A; l \<in> list(A)|] ==> <[], Cons(a,l)> \<in> rlist(A, r)" |
43 "[|a \<in> A; l \<in> list(A)|] ==> <[], Cons(a,l)> \<in> rlist(A, r)" |
44 by (simp add: shorterI) |
44 by (simp add: shorterI) |
45 |
45 |
62 apply (rule linearE [OF r, of x y]) |
62 apply (rule linearE [OF r, of x y]) |
63 apply (auto simp add: diffI intro: sameI) |
63 apply (auto simp add: diffI intro: sameI) |
64 done |
64 done |
65 } |
65 } |
66 note yConsCase = this |
66 note yConsCase = this |
67 show ?case using `ys \<in> list(A)` |
67 show ?case using \<open>ys \<in> list(A)\<close> |
68 by (cases rule: list.cases) (simp_all add: Cons rlist_Nil_Cons yConsCase) |
68 by (cases rule: list.cases) (simp_all add: Cons rlist_Nil_Cons yConsCase) |
69 qed |
69 qed |
70 } |
70 } |
71 thus ?thesis by (simp add: linear_def) |
71 thus ?thesis by (simp add: linear_def) |
72 qed |
72 qed |
73 |
73 |
74 |
74 |
75 subsubsection{*Well-foundedness*} |
75 subsubsection\<open>Well-foundedness\<close> |
76 |
76 |
77 text{*Nothing preceeds Nil in this ordering.*} |
77 text\<open>Nothing preceeds Nil in this ordering.\<close> |
78 inductive_cases rlist_NilE: " <l,[]> \<in> rlist(A,r)" |
78 inductive_cases rlist_NilE: " <l,[]> \<in> rlist(A,r)" |
79 |
79 |
80 inductive_cases rlist_ConsE: " <l', Cons(x,l)> \<in> rlist(A,r)" |
80 inductive_cases rlist_ConsE: " <l', Cons(x,l)> \<in> rlist(A,r)" |
81 |
81 |
82 lemma not_rlist_Nil [simp]: " <l,[]> \<notin> rlist(A,r)" |
82 lemma not_rlist_Nil [simp]: " <l,[]> \<notin> rlist(A,r)" |
137 apply (simp add: well_ord_def wf_on_rlist) |
137 apply (simp add: well_ord_def wf_on_rlist) |
138 apply (simp add: well_ord_def tot_ord_def linear_rlist) |
138 apply (simp add: well_ord_def tot_ord_def linear_rlist) |
139 done |
139 done |
140 |
140 |
141 |
141 |
142 subsection{*An Injection from Formulas into the Natural Numbers*} |
142 subsection\<open>An Injection from Formulas into the Natural Numbers\<close> |
143 |
143 |
144 text{*There is a well-known bijection between @{term "nat*nat"} and @{term |
144 text\<open>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) |
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, |
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 |
147 triangle(succ(k)) = succ(k + triangle(k)). Some small amount of effort is |
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}: |
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]} |
149 @{thm[display] well_ord_InfCard_square_eq[no_vars]} |
150 |
150 |
151 However, this result merely states that there is a bijection between the two |
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 |
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 |
153 conduct the proofs under the assumption that a bijection exists. The simplest |
154 way to organize this is to use a locale.*} |
154 way to organize this is to use a locale.\<close> |
155 |
155 |
156 text{*Locale for any arbitrary injection between @{term "nat*nat"} |
156 text\<open>Locale for any arbitrary injection between @{term "nat*nat"} |
157 and @{term nat}*} |
157 and @{term nat}\<close> |
158 locale Nat_Times_Nat = |
158 locale Nat_Times_Nat = |
159 fixes fn |
159 fixes fn |
160 assumes fn_inj: "fn \<in> inj(nat*nat, nat)" |
160 assumes fn_inj: "fn \<in> inj(nat*nat, nat)" |
161 |
161 |
162 |
162 |
212 |
212 |
213 lemmas nat_times_nat_lepoll_nat = |
213 lemmas nat_times_nat_lepoll_nat = |
214 InfCard_nat [THEN InfCard_square_eqpoll, THEN eqpoll_imp_lepoll] |
214 InfCard_nat [THEN InfCard_square_eqpoll, THEN eqpoll_imp_lepoll] |
215 |
215 |
216 |
216 |
217 text{*Not needed--but interesting?*} |
217 text\<open>Not needed--but interesting?\<close> |
218 theorem formula_lepoll_nat: "formula \<lesssim> nat" |
218 theorem formula_lepoll_nat: "formula \<lesssim> nat" |
219 apply (insert nat_times_nat_lepoll_nat) |
219 apply (insert nat_times_nat_lepoll_nat) |
220 apply (unfold lepoll_def) |
220 apply (unfold lepoll_def) |
221 apply (blast intro: Nat_Times_Nat.inj_formula_nat Nat_Times_Nat.intro) |
221 apply (blast intro: Nat_Times_Nat.inj_formula_nat Nat_Times_Nat.intro) |
222 done |
222 done |
223 |
223 |
224 |
224 |
225 subsection{*Defining the Wellordering on @{term "DPow(A)"}*} |
225 subsection\<open>Defining the Wellordering on @{term "DPow(A)"}\<close> |
226 |
226 |
227 text{*The objective is to build a wellordering on @{term "DPow(A)"} from a |
227 text\<open>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, |
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 |
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 |
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 |
231 (environment, formula) pairs into the ordinals. For each member of @{term |
232 "DPow(A)"}, we take the minimum such ordinal.*} |
232 "DPow(A)"}, we take the minimum such ordinal.\<close> |
233 |
233 |
234 definition |
234 definition |
235 env_form_r :: "[i,i,i]=>i" where |
235 env_form_r :: "[i,i,i]=>i" where |
236 --{*wellordering on (environment, formula) pairs*} |
236 --\<open>wellordering on (environment, formula) pairs\<close> |
237 "env_form_r(f,r,A) == |
237 "env_form_r(f,r,A) == |
238 rmult(list(A), rlist(A, r), |
238 rmult(list(A), rlist(A, r), |
239 formula, measure(formula, enum(f)))" |
239 formula, measure(formula, enum(f)))" |
240 |
240 |
241 definition |
241 definition |
242 env_form_map :: "[i,i,i,i]=>i" where |
242 env_form_map :: "[i,i,i,i]=>i" where |
243 --{*map from (environment, formula) pairs to ordinals*} |
243 --\<open>map from (environment, formula) pairs to ordinals\<close> |
244 "env_form_map(f,r,A,z) |
244 "env_form_map(f,r,A,z) |
245 == ordermap(list(A) * formula, env_form_r(f,r,A)) ` z" |
245 == ordermap(list(A) * formula, env_form_r(f,r,A)) ` z" |
246 |
246 |
247 definition |
247 definition |
248 DPow_ord :: "[i,i,i,i,i]=>o" where |
248 DPow_ord :: "[i,i,i,i,i]=>o" where |
249 --{*predicate that holds if @{term k} is a valid index for @{term X}*} |
249 --\<open>predicate that holds if @{term k} is a valid index for @{term X}\<close> |
250 "DPow_ord(f,r,A,X,k) == |
250 "DPow_ord(f,r,A,X,k) == |
251 \<exists>env \<in> list(A). \<exists>p \<in> formula. |
251 \<exists>env \<in> list(A). \<exists>p \<in> formula. |
252 arity(p) \<le> succ(length(env)) & |
252 arity(p) \<le> succ(length(env)) & |
253 X = {x\<in>A. sats(A, p, Cons(x,env))} & |
253 X = {x\<in>A. sats(A, p, Cons(x,env))} & |
254 env_form_map(f,r,A,<env,p>) = k" |
254 env_form_map(f,r,A,<env,p>) = k" |
255 |
255 |
256 definition |
256 definition |
257 DPow_least :: "[i,i,i,i]=>i" where |
257 DPow_least :: "[i,i,i,i]=>i" where |
258 --{*function yielding the smallest index for @{term X}*} |
258 --\<open>function yielding the smallest index for @{term X}\<close> |
259 "DPow_least(f,r,A,X) == \<mu> k. DPow_ord(f,r,A,X,k)" |
259 "DPow_least(f,r,A,X) == \<mu> k. DPow_ord(f,r,A,X,k)" |
260 |
260 |
261 definition |
261 definition |
262 DPow_r :: "[i,i,i]=>i" where |
262 DPow_r :: "[i,i,i]=>i" where |
263 --{*a wellordering on @{term "DPow(A)"}*} |
263 --\<open>a wellordering on @{term "DPow(A)"}\<close> |
264 "DPow_r(f,r,A) == measure(DPow(A), DPow_least(f,r,A))" |
264 "DPow_r(f,r,A) == measure(DPow(A), DPow_least(f,r,A))" |
265 |
265 |
266 |
266 |
267 lemma (in Nat_Times_Nat) well_ord_env_form_r: |
267 lemma (in Nat_Times_Nat) well_ord_env_form_r: |
268 "well_ord(A,r) |
268 "well_ord(A,r) |
322 lemma (in Nat_Times_Nat) DPow_r_type: |
322 lemma (in Nat_Times_Nat) DPow_r_type: |
323 "DPow_r(fn,r,A) \<subseteq> DPow(A) * DPow(A)" |
323 "DPow_r(fn,r,A) \<subseteq> DPow(A) * DPow(A)" |
324 by (simp add: DPow_r_def measure_def, blast) |
324 by (simp add: DPow_r_def measure_def, blast) |
325 |
325 |
326 |
326 |
327 subsection{*Limit Construction for Well-Orderings*} |
327 subsection\<open>Limit Construction for Well-Orderings\<close> |
328 |
328 |
329 text{*Now we work towards the transfinite definition of wellorderings for |
329 text\<open>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 |
330 @{term "Lset(i)"}. We assume as an inductive hypothesis that there is a family |
331 of wellorderings for smaller ordinals.*} |
331 of wellorderings for smaller ordinals.\<close> |
332 |
332 |
333 definition |
333 definition |
334 rlimit :: "[i,i=>i]=>i" where |
334 rlimit :: "[i,i=>i]=>i" where |
335 --{*Expresses the wellordering at limit ordinals. The conditional |
335 --\<open>Expresses the wellordering at limit ordinals. The conditional |
336 lets us remove the premise @{term "Limit(i)"} from some theorems.*} |
336 lets us remove the premise @{term "Limit(i)"} from some theorems.\<close> |
337 "rlimit(i,r) == |
337 "rlimit(i,r) == |
338 if Limit(i) then |
338 if Limit(i) then |
339 {z: Lset(i) * Lset(i). |
339 {z: Lset(i) * Lset(i). |
340 \<exists>x' x. z = <x',x> & |
340 \<exists>x' x. z = <x',x> & |
341 (lrank(x') < lrank(x) | |
341 (lrank(x') < lrank(x) | |
342 (lrank(x') = lrank(x) & <x',x> \<in> r(succ(lrank(x)))))} |
342 (lrank(x') = lrank(x) & <x',x> \<in> r(succ(lrank(x)))))} |
343 else 0" |
343 else 0" |
344 |
344 |
345 definition |
345 definition |
346 Lset_new :: "i=>i" where |
346 Lset_new :: "i=>i" where |
347 --{*This constant denotes the set of elements introduced at level |
347 --\<open>This constant denotes the set of elements introduced at level |
348 @{term "succ(i)"}*} |
348 @{term "succ(i)"}\<close> |
349 "Lset_new(i) == {x \<in> Lset(succ(i)). lrank(x) = i}" |
349 "Lset_new(i) == {x \<in> Lset(succ(i)). lrank(x) = i}" |
350 |
350 |
351 lemma Limit_Lset_eq2: |
351 lemma Limit_Lset_eq2: |
352 "Limit(i) ==> Lset(i) = (\<Union>j\<in>i. Lset_new(j))" |
352 "Limit(i) ==> Lset(i) = (\<Union>j\<in>i. Lset_new(j))" |
353 apply (simp add: Limit_Lset_eq) |
353 apply (simp add: Limit_Lset_eq) |
410 apply (rule refl iff_refl Collect_cong ex_cong conj_cong)+ |
410 apply (rule refl iff_refl Collect_cong ex_cong conj_cong)+ |
411 apply (simp add: Limit_is_Ord Lset_lrank_lt) |
411 apply (simp add: Limit_is_Ord Lset_lrank_lt) |
412 done |
412 done |
413 |
413 |
414 |
414 |
415 subsection{*Transfinite Definition of the Wellordering on @{term "L"}*} |
415 subsection\<open>Transfinite Definition of the Wellordering on @{term "L"}\<close> |
416 |
416 |
417 definition |
417 definition |
418 L_r :: "[i, i] => i" where |
418 L_r :: "[i, i] => i" where |
419 "L_r(f) == %i. |
419 "L_r(f) == %i. |
420 transrec3(i, 0, \<lambda>x r. DPow_r(f, r, Lset(x)), |
420 transrec3(i, 0, \<lambda>x r. DPow_r(f, r, Lset(x)), |
421 \<lambda>x r. rlimit(x, \<lambda>y. r`y))" |
421 \<lambda>x r. rlimit(x, \<lambda>y. r`y))" |
422 |
422 |
423 subsubsection{*The Corresponding Recursion Equations*} |
423 subsubsection\<open>The Corresponding Recursion Equations\<close> |
424 lemma [simp]: "L_r(f,0) = 0" |
424 lemma [simp]: "L_r(f,0) = 0" |
425 by (simp add: L_r_def) |
425 by (simp add: L_r_def) |
426 |
426 |
427 lemma [simp]: "L_r(f, succ(i)) = DPow_r(f, L_r(f,i), Lset(i))" |
427 lemma [simp]: "L_r(f, succ(i)) = DPow_r(f, L_r(f,i), Lset(i))" |
428 by (simp add: L_r_def) |
428 by (simp add: L_r_def) |
429 |
429 |
430 text{*The limit case is non-trivial because of the distinction between |
430 text\<open>The limit case is non-trivial because of the distinction between |
431 object-level and meta-level abstraction.*} |
431 object-level and meta-level abstraction.\<close> |
432 lemma [simp]: "Limit(i) ==> L_r(f,i) = rlimit(i, L_r(f))" |
432 lemma [simp]: "Limit(i) ==> L_r(f,i) = rlimit(i, L_r(f))" |
433 by (simp cong: rlimit_cong add: transrec3_Limit L_r_def ltD) |
433 by (simp cong: rlimit_cong add: transrec3_Limit L_r_def ltD) |
434 |
434 |
435 lemma (in Nat_Times_Nat) L_r_type: |
435 lemma (in Nat_Times_Nat) L_r_type: |
436 "Ord(i) ==> L_r(fn,i) \<subseteq> Lset(i) * Lset(i)" |
436 "Ord(i) ==> L_r(fn,i) \<subseteq> Lset(i) * Lset(i)" |