author | obua |
Thu, 16 Feb 2006 04:17:19 +0100 | |
changeset 19067 | c0321d7d6b3d |
parent 16417 | 9bc16273c2d4 |
child 24893 | b8ef7afe3a6b |
permissions | -rw-r--r-- |
1478 | 1 |
(* Title: ZF/epsilon.thy |
0 | 2 |
ID: $Id$ |
1478 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1993 University of Cambridge |
5 |
||
6 |
*) |
|
7 |
||
13328 | 8 |
header{*Epsilon Induction and Recursion*} |
9 |
||
16417 | 10 |
theory Epsilon imports Nat begin |
13164 | 11 |
|
2469 | 12 |
constdefs |
13164 | 13 |
eclose :: "i=>i" |
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13524
diff
changeset
|
14 |
"eclose(A) == \<Union>n\<in>nat. nat_rec(n, A, %m r. Union(r))" |
0 | 15 |
|
13164 | 16 |
transrec :: "[i, [i,i]=>i] =>i" |
2469 | 17 |
"transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)" |
18 |
||
13164 | 19 |
rank :: "i=>i" |
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13524
diff
changeset
|
20 |
"rank(a) == transrec(a, %x f. \<Union>y\<in>x. succ(f`y))" |
2469 | 21 |
|
13164 | 22 |
transrec2 :: "[i, i, [i,i]=>i] =>i" |
2469 | 23 |
"transrec2(k, a, b) == |
24 |
transrec(k, |
|
25 |
%i r. if(i=0, a, |
|
26 |
if(EX j. i=succ(j), |
|
27 |
b(THE j. i=succ(j), r`(THE j. i=succ(j))), |
|
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13524
diff
changeset
|
28 |
\<Union>j<i. r`j)))" |
2469 | 29 |
|
13164 | 30 |
recursor :: "[i, [i,i]=>i, i]=>i" |
31 |
"recursor(a,b,k) == transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))" |
|
32 |
||
33 |
rec :: "[i, i, [i,i]=>i]=>i" |
|
34 |
"rec(k,a,b) == recursor(a,b,k)" |
|
35 |
||
36 |
||
13356 | 37 |
subsection{*Basic Closure Properties*} |
13164 | 38 |
|
39 |
lemma arg_subset_eclose: "A <= eclose(A)" |
|
40 |
apply (unfold eclose_def) |
|
41 |
apply (rule nat_rec_0 [THEN equalityD2, THEN subset_trans]) |
|
42 |
apply (rule nat_0I [THEN UN_upper]) |
|
43 |
done |
|
44 |
||
45 |
lemmas arg_into_eclose = arg_subset_eclose [THEN subsetD, standard] |
|
46 |
||
47 |
lemma Transset_eclose: "Transset(eclose(A))" |
|
48 |
apply (unfold eclose_def Transset_def) |
|
49 |
apply (rule subsetI [THEN ballI]) |
|
50 |
apply (erule UN_E) |
|
51 |
apply (rule nat_succI [THEN UN_I], assumption) |
|
52 |
apply (erule nat_rec_succ [THEN ssubst]) |
|
53 |
apply (erule UnionI, assumption) |
|
54 |
done |
|
55 |
||
56 |
(* x : eclose(A) ==> x <= eclose(A) *) |
|
57 |
lemmas eclose_subset = |
|
58 |
Transset_eclose [unfolded Transset_def, THEN bspec, standard] |
|
59 |
||
60 |
(* [| A : eclose(B); c : A |] ==> c : eclose(B) *) |
|
61 |
lemmas ecloseD = eclose_subset [THEN subsetD, standard] |
|
62 |
||
63 |
lemmas arg_in_eclose_sing = arg_subset_eclose [THEN singleton_subsetD] |
|
64 |
lemmas arg_into_eclose_sing = arg_in_eclose_sing [THEN ecloseD, standard] |
|
65 |
||
66 |
(* This is epsilon-induction for eclose(A); see also eclose_induct_down... |
|
67 |
[| a: eclose(A); !!x. [| x: eclose(A); ALL y:x. P(y) |] ==> P(x) |
|
68 |
|] ==> P(a) |
|
69 |
*) |
|
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
70 |
lemmas eclose_induct = |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
71 |
Transset_induct [OF _ Transset_eclose, induct set: eclose] |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
72 |
|
13164 | 73 |
|
74 |
(*Epsilon induction*) |
|
75 |
lemma eps_induct: |
|
76 |
"[| !!x. ALL y:x. P(y) ==> P(x) |] ==> P(a)" |
|
77 |
by (rule arg_in_eclose_sing [THEN eclose_induct], blast) |
|
78 |
||
79 |
||
13356 | 80 |
subsection{*Leastness of @{term eclose}*} |
13164 | 81 |
|
82 |
(** eclose(A) is the least transitive set including A as a subset. **) |
|
83 |
||
84 |
lemma eclose_least_lemma: |
|
85 |
"[| Transset(X); A<=X; n: nat |] ==> nat_rec(n, A, %m r. Union(r)) <= X" |
|
86 |
apply (unfold Transset_def) |
|
87 |
apply (erule nat_induct) |
|
88 |
apply (simp add: nat_rec_0) |
|
89 |
apply (simp add: nat_rec_succ, blast) |
|
90 |
done |
|
91 |
||
92 |
lemma eclose_least: |
|
93 |
"[| Transset(X); A<=X |] ==> eclose(A) <= X" |
|
94 |
apply (unfold eclose_def) |
|
95 |
apply (rule eclose_least_lemma [THEN UN_least], assumption+) |
|
96 |
done |
|
97 |
||
98 |
(*COMPLETELY DIFFERENT induction principle from eclose_induct!!*) |
|
13524 | 99 |
lemma eclose_induct_down [consumes 1]: |
13164 | 100 |
"[| a: eclose(b); |
101 |
!!y. [| y: b |] ==> P(y); |
|
102 |
!!y z. [| y: eclose(b); P(y); z: y |] ==> P(z) |
|
103 |
|] ==> P(a)" |
|
104 |
apply (rule eclose_least [THEN subsetD, THEN CollectD2, of "eclose(b)"]) |
|
105 |
prefer 3 apply assumption |
|
106 |
apply (unfold Transset_def) |
|
107 |
apply (blast intro: ecloseD) |
|
108 |
apply (blast intro: arg_subset_eclose [THEN subsetD]) |
|
109 |
done |
|
110 |
||
111 |
lemma Transset_eclose_eq_arg: "Transset(X) ==> eclose(X) = X" |
|
112 |
apply (erule equalityI [OF eclose_least arg_subset_eclose]) |
|
113 |
apply (rule subset_refl) |
|
114 |
done |
|
115 |
||
13387 | 116 |
text{*A transitive set either is empty or contains the empty set.*} |
117 |
lemma Transset_0_lemma [rule_format]: "Transset(A) ==> x\<in>A --> 0\<in>A"; |
|
118 |
apply (simp add: Transset_def) |
|
119 |
apply (rule_tac a=x in eps_induct, clarify) |
|
120 |
apply (drule bspec, assumption) |
|
14153 | 121 |
apply (case_tac "x=0", auto) |
13387 | 122 |
done |
123 |
||
124 |
lemma Transset_0_disj: "Transset(A) ==> A=0 | 0\<in>A"; |
|
125 |
by (blast dest: Transset_0_lemma) |
|
126 |
||
13164 | 127 |
|
13356 | 128 |
subsection{*Epsilon Recursion*} |
13164 | 129 |
|
130 |
(*Unused...*) |
|
131 |
lemma mem_eclose_trans: "[| A: eclose(B); B: eclose(C) |] ==> A: eclose(C)" |
|
132 |
by (rule eclose_least [OF Transset_eclose eclose_subset, THEN subsetD], |
|
133 |
assumption+) |
|
134 |
||
135 |
(*Variant of the previous lemma in a useable form for the sequel*) |
|
136 |
lemma mem_eclose_sing_trans: |
|
137 |
"[| A: eclose({B}); B: eclose({C}) |] ==> A: eclose({C})" |
|
138 |
by (rule eclose_least [OF Transset_eclose singleton_subsetI, THEN subsetD], |
|
139 |
assumption+) |
|
140 |
||
141 |
lemma under_Memrel: "[| Transset(i); j:i |] ==> Memrel(i)-``{j} = j" |
|
142 |
by (unfold Transset_def, blast) |
|
143 |
||
13217 | 144 |
lemma lt_Memrel: "j < i ==> Memrel(i) -`` {j} = j" |
145 |
by (simp add: lt_def Ord_def under_Memrel) |
|
146 |
||
13164 | 147 |
(* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *) |
148 |
lemmas under_Memrel_eclose = Transset_eclose [THEN under_Memrel, standard] |
|
149 |
||
150 |
lemmas wfrec_ssubst = wf_Memrel [THEN wfrec, THEN ssubst] |
|
151 |
||
152 |
lemma wfrec_eclose_eq: |
|
153 |
"[| k:eclose({j}); j:eclose({i}) |] ==> |
|
154 |
wfrec(Memrel(eclose({i})), k, H) = wfrec(Memrel(eclose({j})), k, H)" |
|
155 |
apply (erule eclose_induct) |
|
156 |
apply (rule wfrec_ssubst) |
|
157 |
apply (rule wfrec_ssubst) |
|
158 |
apply (simp add: under_Memrel_eclose mem_eclose_sing_trans [of _ j i]) |
|
159 |
done |
|
160 |
||
161 |
lemma wfrec_eclose_eq2: |
|
162 |
"k: i ==> wfrec(Memrel(eclose({i})),k,H) = wfrec(Memrel(eclose({k})),k,H)" |
|
163 |
apply (rule arg_in_eclose_sing [THEN wfrec_eclose_eq]) |
|
164 |
apply (erule arg_into_eclose_sing) |
|
165 |
done |
|
166 |
||
167 |
lemma transrec: "transrec(a,H) = H(a, lam x:a. transrec(x,H))" |
|
168 |
apply (unfold transrec_def) |
|
169 |
apply (rule wfrec_ssubst) |
|
170 |
apply (simp add: wfrec_eclose_eq2 arg_in_eclose_sing under_Memrel_eclose) |
|
171 |
done |
|
172 |
||
173 |
(*Avoids explosions in proofs; resolve it with a meta-level definition.*) |
|
174 |
lemma def_transrec: |
|
175 |
"[| !!x. f(x)==transrec(x,H) |] ==> f(a) = H(a, lam x:a. f(x))" |
|
176 |
apply simp |
|
177 |
apply (rule transrec) |
|
178 |
done |
|
179 |
||
180 |
lemma transrec_type: |
|
181 |
"[| !!x u. [| x:eclose({a}); u: Pi(x,B) |] ==> H(x,u) : B(x) |] |
|
182 |
==> transrec(a,H) : B(a)" |
|
13784 | 183 |
apply (rule_tac i = a in arg_in_eclose_sing [THEN eclose_induct]) |
13164 | 184 |
apply (subst transrec) |
185 |
apply (simp add: lam_type) |
|
186 |
done |
|
187 |
||
188 |
lemma eclose_sing_Ord: "Ord(i) ==> eclose({i}) <= succ(i)" |
|
189 |
apply (erule Ord_is_Transset [THEN Transset_succ, THEN eclose_least]) |
|
190 |
apply (rule succI1 [THEN singleton_subsetI]) |
|
191 |
done |
|
192 |
||
13269 | 193 |
lemma succ_subset_eclose_sing: "succ(i) <= eclose({i})" |
194 |
apply (insert arg_subset_eclose [of "{i}"], simp) |
|
195 |
apply (frule eclose_subset, blast) |
|
196 |
done |
|
197 |
||
198 |
lemma eclose_sing_Ord_eq: "Ord(i) ==> eclose({i}) = succ(i)" |
|
199 |
apply (rule equalityI) |
|
200 |
apply (erule eclose_sing_Ord) |
|
201 |
apply (rule succ_subset_eclose_sing) |
|
202 |
done |
|
203 |
||
13164 | 204 |
lemma Ord_transrec_type: |
205 |
assumes jini: "j: i" |
|
206 |
and ordi: "Ord(i)" |
|
207 |
and minor: " !!x u. [| x: i; u: Pi(x,B) |] ==> H(x,u) : B(x)" |
|
208 |
shows "transrec(j,H) : B(j)" |
|
209 |
apply (rule transrec_type) |
|
210 |
apply (insert jini ordi) |
|
211 |
apply (blast intro!: minor |
|
212 |
intro: Ord_trans |
|
213 |
dest: Ord_in_Ord [THEN eclose_sing_Ord, THEN subsetD]) |
|
214 |
done |
|
215 |
||
13356 | 216 |
subsection{*Rank*} |
13164 | 217 |
|
218 |
(*NOT SUITABLE FOR REWRITING -- RECURSIVE!*) |
|
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13524
diff
changeset
|
219 |
lemma rank: "rank(a) = (\<Union>y\<in>a. succ(rank(y)))" |
13164 | 220 |
by (subst rank_def [THEN def_transrec], simp) |
221 |
||
222 |
lemma Ord_rank [simp]: "Ord(rank(a))" |
|
13784 | 223 |
apply (rule_tac a=a in eps_induct) |
13164 | 224 |
apply (subst rank) |
225 |
apply (rule Ord_succ [THEN Ord_UN]) |
|
226 |
apply (erule bspec, assumption) |
|
227 |
done |
|
228 |
||
229 |
lemma rank_of_Ord: "Ord(i) ==> rank(i) = i" |
|
230 |
apply (erule trans_induct) |
|
231 |
apply (subst rank) |
|
232 |
apply (simp add: Ord_equality) |
|
233 |
done |
|
234 |
||
235 |
lemma rank_lt: "a:b ==> rank(a) < rank(b)" |
|
13784 | 236 |
apply (rule_tac a1 = b in rank [THEN ssubst]) |
13164 | 237 |
apply (erule UN_I [THEN ltI]) |
238 |
apply (rule_tac [2] Ord_UN, auto) |
|
239 |
done |
|
240 |
||
241 |
lemma eclose_rank_lt: "a: eclose(b) ==> rank(a) < rank(b)" |
|
242 |
apply (erule eclose_induct_down) |
|
243 |
apply (erule rank_lt) |
|
244 |
apply (erule rank_lt [THEN lt_trans], assumption) |
|
245 |
done |
|
6070 | 246 |
|
13164 | 247 |
lemma rank_mono: "a<=b ==> rank(a) le rank(b)" |
248 |
apply (rule subset_imp_le) |
|
15481 | 249 |
apply (auto simp add: rank [of a] rank [of b]) |
13164 | 250 |
done |
251 |
||
252 |
lemma rank_Pow: "rank(Pow(a)) = succ(rank(a))" |
|
253 |
apply (rule rank [THEN trans]) |
|
254 |
apply (rule le_anti_sym) |
|
255 |
apply (rule_tac [2] UN_upper_le) |
|
256 |
apply (rule UN_least_le) |
|
257 |
apply (auto intro: rank_mono simp add: Ord_UN) |
|
258 |
done |
|
259 |
||
260 |
lemma rank_0 [simp]: "rank(0) = 0" |
|
261 |
by (rule rank [THEN trans], blast) |
|
262 |
||
263 |
lemma rank_succ [simp]: "rank(succ(x)) = succ(rank(x))" |
|
264 |
apply (rule rank [THEN trans]) |
|
265 |
apply (rule equalityI [OF UN_least succI1 [THEN UN_upper]]) |
|
266 |
apply (erule succE, blast) |
|
267 |
apply (erule rank_lt [THEN leI, THEN succ_leI, THEN le_imp_subset]) |
|
268 |
done |
|
269 |
||
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13524
diff
changeset
|
270 |
lemma rank_Union: "rank(Union(A)) = (\<Union>x\<in>A. rank(x))" |
13164 | 271 |
apply (rule equalityI) |
272 |
apply (rule_tac [2] rank_mono [THEN le_imp_subset, THEN UN_least]) |
|
273 |
apply (erule_tac [2] Union_upper) |
|
274 |
apply (subst rank) |
|
275 |
apply (rule UN_least) |
|
276 |
apply (erule UnionE) |
|
277 |
apply (rule subset_trans) |
|
278 |
apply (erule_tac [2] RepFunI [THEN Union_upper]) |
|
279 |
apply (erule rank_lt [THEN succ_leI, THEN le_imp_subset]) |
|
280 |
done |
|
281 |
||
282 |
lemma rank_eclose: "rank(eclose(a)) = rank(a)" |
|
283 |
apply (rule le_anti_sym) |
|
284 |
apply (rule_tac [2] arg_subset_eclose [THEN rank_mono]) |
|
285 |
apply (rule_tac a1 = "eclose (a) " in rank [THEN ssubst]) |
|
286 |
apply (rule Ord_rank [THEN UN_least_le]) |
|
287 |
apply (erule eclose_rank_lt [THEN succ_leI]) |
|
288 |
done |
|
289 |
||
290 |
lemma rank_pair1: "rank(a) < rank(<a,b>)" |
|
291 |
apply (unfold Pair_def) |
|
292 |
apply (rule consI1 [THEN rank_lt, THEN lt_trans]) |
|
293 |
apply (rule consI1 [THEN consI2, THEN rank_lt]) |
|
294 |
done |
|
295 |
||
296 |
lemma rank_pair2: "rank(b) < rank(<a,b>)" |
|
297 |
apply (unfold Pair_def) |
|
298 |
apply (rule consI1 [THEN consI2, THEN rank_lt, THEN lt_trans]) |
|
299 |
apply (rule consI1 [THEN consI2, THEN rank_lt]) |
|
300 |
done |
|
301 |
||
302 |
(*Not clear how to remove the P(a) condition, since the "then" part |
|
303 |
must refer to "a"*) |
|
304 |
lemma the_equality_if: |
|
305 |
"P(a) ==> (THE x. P(x)) = (if (EX!x. P(x)) then a else 0)" |
|
306 |
by (simp add: the_0 the_equality2) |
|
307 |
||
13175
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13164
diff
changeset
|
308 |
(*The first premise not only fixs i but ensures f~=0. |
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13164
diff
changeset
|
309 |
The second premise is now essential. Consider otherwise the relation |
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13164
diff
changeset
|
310 |
r = {<0,0>,<0,1>,<0,2>,...}. Then f`0 = Union(f``{0}) = Union(nat) = nat, |
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13164
diff
changeset
|
311 |
whose rank equals that of r.*) |
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13164
diff
changeset
|
312 |
lemma rank_apply: "[|i : domain(f); function(f)|] ==> rank(f`i) < rank(f)" |
13269 | 313 |
apply clarify |
314 |
apply (simp add: function_apply_equality) |
|
13175
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13164
diff
changeset
|
315 |
apply (blast intro: lt_trans rank_lt rank_pair2) |
13164 | 316 |
done |
317 |
||
318 |
||
13356 | 319 |
subsection{*Corollaries of Leastness*} |
13164 | 320 |
|
321 |
lemma mem_eclose_subset: "A:B ==> eclose(A)<=eclose(B)" |
|
322 |
apply (rule Transset_eclose [THEN eclose_least]) |
|
323 |
apply (erule arg_into_eclose [THEN eclose_subset]) |
|
324 |
done |
|
325 |
||
326 |
lemma eclose_mono: "A<=B ==> eclose(A) <= eclose(B)" |
|
327 |
apply (rule Transset_eclose [THEN eclose_least]) |
|
328 |
apply (erule subset_trans) |
|
329 |
apply (rule arg_subset_eclose) |
|
330 |
done |
|
331 |
||
332 |
(** Idempotence of eclose **) |
|
333 |
||
334 |
lemma eclose_idem: "eclose(eclose(A)) = eclose(A)" |
|
335 |
apply (rule equalityI) |
|
336 |
apply (rule eclose_least [OF Transset_eclose subset_refl]) |
|
337 |
apply (rule arg_subset_eclose) |
|
338 |
done |
|
339 |
||
340 |
(** Transfinite recursion for definitions based on the |
|
341 |
three cases of ordinals **) |
|
342 |
||
343 |
lemma transrec2_0 [simp]: "transrec2(0,a,b) = a" |
|
344 |
by (rule transrec2_def [THEN def_transrec, THEN trans], simp) |
|
345 |
||
346 |
lemma transrec2_succ [simp]: "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))" |
|
347 |
apply (rule transrec2_def [THEN def_transrec, THEN trans]) |
|
348 |
apply (simp add: the_equality if_P) |
|
349 |
done |
|
350 |
||
351 |
lemma transrec2_Limit: |
|
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13524
diff
changeset
|
352 |
"Limit(i) ==> transrec2(i,a,b) = (\<Union>j<i. transrec2(j,a,b))" |
13175
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13164
diff
changeset
|
353 |
apply (rule transrec2_def [THEN def_transrec, THEN trans]) |
13269 | 354 |
apply (auto simp add: OUnion_def) |
13164 | 355 |
done |
356 |
||
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
357 |
lemma def_transrec2: |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
358 |
"(!!x. f(x)==transrec2(x,a,b)) |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
359 |
==> f(0) = a & |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
360 |
f(succ(i)) = b(i, f(i)) & |
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13524
diff
changeset
|
361 |
(Limit(K) --> f(K) = (\<Union>j<K. f(j)))" |
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
362 |
by (simp add: transrec2_Limit) |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
363 |
|
13164 | 364 |
|
365 |
(** recursor -- better than nat_rec; the succ case has no type requirement! **) |
|
366 |
||
367 |
(*NOT suitable for rewriting*) |
|
368 |
lemmas recursor_lemma = recursor_def [THEN def_transrec, THEN trans] |
|
369 |
||
370 |
lemma recursor_0: "recursor(a,b,0) = a" |
|
371 |
by (rule nat_case_0 [THEN recursor_lemma]) |
|
372 |
||
373 |
lemma recursor_succ: "recursor(a,b,succ(m)) = b(m, recursor(a,b,m))" |
|
374 |
by (rule recursor_lemma, simp) |
|
375 |
||
376 |
||
377 |
(** rec: old version for compatibility **) |
|
378 |
||
379 |
lemma rec_0 [simp]: "rec(0,a,b) = a" |
|
380 |
apply (unfold rec_def) |
|
381 |
apply (rule recursor_0) |
|
382 |
done |
|
383 |
||
384 |
lemma rec_succ [simp]: "rec(succ(m),a,b) = b(m, rec(m,a,b))" |
|
385 |
apply (unfold rec_def) |
|
386 |
apply (rule recursor_succ) |
|
387 |
done |
|
388 |
||
389 |
lemma rec_type: |
|
390 |
"[| n: nat; |
|
391 |
a: C(0); |
|
392 |
!!m z. [| m: nat; z: C(m) |] ==> b(m,z): C(succ(m)) |] |
|
393 |
==> rec(n,a,b) : C(n)" |
|
13185 | 394 |
by (erule nat_induct, auto) |
13164 | 395 |
|
396 |
ML |
|
397 |
{* |
|
398 |
val arg_subset_eclose = thm "arg_subset_eclose"; |
|
399 |
val arg_into_eclose = thm "arg_into_eclose"; |
|
400 |
val Transset_eclose = thm "Transset_eclose"; |
|
401 |
val eclose_subset = thm "eclose_subset"; |
|
402 |
val ecloseD = thm "ecloseD"; |
|
403 |
val arg_in_eclose_sing = thm "arg_in_eclose_sing"; |
|
404 |
val arg_into_eclose_sing = thm "arg_into_eclose_sing"; |
|
405 |
val eclose_induct = thm "eclose_induct"; |
|
406 |
val eps_induct = thm "eps_induct"; |
|
407 |
val eclose_least = thm "eclose_least"; |
|
408 |
val eclose_induct_down = thm "eclose_induct_down"; |
|
409 |
val Transset_eclose_eq_arg = thm "Transset_eclose_eq_arg"; |
|
410 |
val mem_eclose_trans = thm "mem_eclose_trans"; |
|
411 |
val mem_eclose_sing_trans = thm "mem_eclose_sing_trans"; |
|
412 |
val under_Memrel = thm "under_Memrel"; |
|
413 |
val under_Memrel_eclose = thm "under_Memrel_eclose"; |
|
414 |
val wfrec_ssubst = thm "wfrec_ssubst"; |
|
415 |
val wfrec_eclose_eq = thm "wfrec_eclose_eq"; |
|
416 |
val wfrec_eclose_eq2 = thm "wfrec_eclose_eq2"; |
|
417 |
val transrec = thm "transrec"; |
|
418 |
val def_transrec = thm "def_transrec"; |
|
419 |
val transrec_type = thm "transrec_type"; |
|
420 |
val eclose_sing_Ord = thm "eclose_sing_Ord"; |
|
421 |
val Ord_transrec_type = thm "Ord_transrec_type"; |
|
422 |
val rank = thm "rank"; |
|
423 |
val Ord_rank = thm "Ord_rank"; |
|
424 |
val rank_of_Ord = thm "rank_of_Ord"; |
|
425 |
val rank_lt = thm "rank_lt"; |
|
426 |
val eclose_rank_lt = thm "eclose_rank_lt"; |
|
427 |
val rank_mono = thm "rank_mono"; |
|
428 |
val rank_Pow = thm "rank_Pow"; |
|
429 |
val rank_0 = thm "rank_0"; |
|
430 |
val rank_succ = thm "rank_succ"; |
|
431 |
val rank_Union = thm "rank_Union"; |
|
432 |
val rank_eclose = thm "rank_eclose"; |
|
433 |
val rank_pair1 = thm "rank_pair1"; |
|
434 |
val rank_pair2 = thm "rank_pair2"; |
|
435 |
val the_equality_if = thm "the_equality_if"; |
|
436 |
val rank_apply = thm "rank_apply"; |
|
437 |
val mem_eclose_subset = thm "mem_eclose_subset"; |
|
438 |
val eclose_mono = thm "eclose_mono"; |
|
439 |
val eclose_idem = thm "eclose_idem"; |
|
440 |
val transrec2_0 = thm "transrec2_0"; |
|
441 |
val transrec2_succ = thm "transrec2_succ"; |
|
442 |
val transrec2_Limit = thm "transrec2_Limit"; |
|
443 |
val recursor_0 = thm "recursor_0"; |
|
444 |
val recursor_succ = thm "recursor_succ"; |
|
445 |
val rec_0 = thm "rec_0"; |
|
446 |
val rec_succ = thm "rec_succ"; |
|
447 |
val rec_type = thm "rec_type"; |
|
448 |
*} |
|
6070 | 449 |
|
0 | 450 |
end |