author | paulson |
Wed, 05 Jun 2002 15:34:55 +0200 | |
changeset 13203 | fac77a839aa2 |
parent 13185 | da61bfa0a391 |
child 13220 | 62c899c77151 |
permissions | -rw-r--r-- |
1478 | 1 |
(* Title: ZF/univ.thy |
0 | 2 |
ID: $Id$ |
1478 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1992 University of Cambridge |
5 |
||
6 |
The cumulative hierarchy and a small universe for recursive types |
|
7 |
||
8 |
Standard notation for Vset(i) is V(i), but users might want V for a variable |
|
516 | 9 |
|
10 |
NOTE: univ(A) could be a translation; would simplify many proofs! |
|
6093 | 11 |
But Ind_Syntax.univ refers to the constant "Univ.univ" |
0 | 12 |
*) |
13 |
||
13163 | 14 |
theory Univ = Epsilon + Sum + Finite + mono: |
3923 | 15 |
|
13163 | 16 |
constdefs |
17 |
Vfrom :: "[i,i]=>i" |
|
18 |
"Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))" |
|
0 | 19 |
|
13163 | 20 |
syntax Vset :: "i=>i" |
0 | 21 |
translations |
1478 | 22 |
"Vset(x)" == "Vfrom(0,x)" |
0 | 23 |
|
3923 | 24 |
|
13163 | 25 |
constdefs |
26 |
Vrec :: "[i, [i,i]=>i] =>i" |
|
27 |
"Vrec(a,H) == transrec(rank(a), %x g. lam z: Vset(succ(x)). |
|
28 |
H(z, lam w:Vset(x). g`rank(w)`w)) ` a" |
|
29 |
||
30 |
Vrecursor :: "[[i,i]=>i, i] =>i" |
|
31 |
"Vrecursor(H,a) == transrec(rank(a), %x g. lam z: Vset(succ(x)). |
|
32 |
H(lam w:Vset(x). g`rank(w)`w, z)) ` a" |
|
33 |
||
34 |
univ :: "i=>i" |
|
35 |
"univ(A) == Vfrom(A,nat)" |
|
36 |
||
37 |
||
38 |
text{*NOT SUITABLE FOR REWRITING -- RECURSIVE!*} |
|
39 |
lemma Vfrom: "Vfrom(A,i) = A Un (UN j:i. Pow(Vfrom(A,j)))" |
|
40 |
apply (subst Vfrom_def [THEN def_transrec]) |
|
41 |
apply simp |
|
42 |
done |
|
43 |
||
44 |
subsubsection{* Monotonicity *} |
|
45 |
||
46 |
lemma Vfrom_mono [rule_format]: |
|
47 |
"A<=B ==> ALL j. i<=j --> Vfrom(A,i) <= Vfrom(B,j)" |
|
48 |
apply (rule_tac a=i in eps_induct) |
|
49 |
apply (rule impI [THEN allI]) |
|
50 |
apply (subst Vfrom) |
|
51 |
apply (subst Vfrom) |
|
52 |
apply (erule Un_mono) |
|
53 |
apply (erule UN_mono, blast) |
|
54 |
done |
|
55 |
||
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
56 |
lemma VfromI: "[| a: Vfrom(A,j); j<i |] ==> a : Vfrom(A,i)" |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
57 |
by (blast dest: Vfrom_mono [OF subset_refl le_imp_subset [OF leI]]) |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
58 |
|
13163 | 59 |
|
60 |
subsubsection{* A fundamental equality: Vfrom does not require ordinals! *} |
|
61 |
||
62 |
lemma Vfrom_rank_subset1: "Vfrom(A,x) <= Vfrom(A,rank(x))" |
|
63 |
apply (rule_tac a=x in eps_induct) |
|
64 |
apply (subst Vfrom) |
|
65 |
apply (subst Vfrom) |
|
66 |
apply (blast intro!: rank_lt [THEN ltD]) |
|
67 |
done |
|
68 |
||
69 |
lemma Vfrom_rank_subset2: "Vfrom(A,rank(x)) <= Vfrom(A,x)" |
|
70 |
apply (rule_tac a=x in eps_induct) |
|
71 |
apply (subst Vfrom) |
|
72 |
apply (subst Vfrom) |
|
73 |
apply (rule subset_refl [THEN Un_mono]) |
|
74 |
apply (rule UN_least) |
|
75 |
txt{*expand rank(x1) = (UN y:x1. succ(rank(y))) in assumptions*} |
|
76 |
apply (erule rank [THEN equalityD1, THEN subsetD, THEN UN_E]) |
|
77 |
apply (rule subset_trans) |
|
78 |
apply (erule_tac [2] UN_upper) |
|
79 |
apply (rule subset_refl [THEN Vfrom_mono, THEN subset_trans, THEN Pow_mono]) |
|
80 |
apply (erule ltI [THEN le_imp_subset]) |
|
81 |
apply (rule Ord_rank [THEN Ord_succ]) |
|
82 |
apply (erule bspec, assumption) |
|
83 |
done |
|
84 |
||
85 |
lemma Vfrom_rank_eq: "Vfrom(A,rank(x)) = Vfrom(A,x)" |
|
86 |
apply (rule equalityI) |
|
87 |
apply (rule Vfrom_rank_subset2) |
|
88 |
apply (rule Vfrom_rank_subset1) |
|
89 |
done |
|
90 |
||
91 |
||
92 |
subsection{* Basic closure properties *} |
|
93 |
||
94 |
lemma zero_in_Vfrom: "y:x ==> 0 : Vfrom(A,x)" |
|
95 |
by (subst Vfrom, blast) |
|
96 |
||
97 |
lemma i_subset_Vfrom: "i <= Vfrom(A,i)" |
|
98 |
apply (rule_tac a=i in eps_induct) |
|
99 |
apply (subst Vfrom, blast) |
|
100 |
done |
|
101 |
||
102 |
lemma A_subset_Vfrom: "A <= Vfrom(A,i)" |
|
103 |
apply (subst Vfrom) |
|
104 |
apply (rule Un_upper1) |
|
105 |
done |
|
106 |
||
107 |
lemmas A_into_Vfrom = A_subset_Vfrom [THEN subsetD] |
|
108 |
||
109 |
lemma subset_mem_Vfrom: "a <= Vfrom(A,i) ==> a: Vfrom(A,succ(i))" |
|
110 |
by (subst Vfrom, blast) |
|
111 |
||
112 |
subsubsection{* Finite sets and ordered pairs *} |
|
113 |
||
114 |
lemma singleton_in_Vfrom: "a: Vfrom(A,i) ==> {a} : Vfrom(A,succ(i))" |
|
115 |
by (rule subset_mem_Vfrom, safe) |
|
116 |
||
117 |
lemma doubleton_in_Vfrom: |
|
118 |
"[| a: Vfrom(A,i); b: Vfrom(A,i) |] ==> {a,b} : Vfrom(A,succ(i))" |
|
119 |
by (rule subset_mem_Vfrom, safe) |
|
120 |
||
121 |
lemma Pair_in_Vfrom: |
|
122 |
"[| a: Vfrom(A,i); b: Vfrom(A,i) |] ==> <a,b> : Vfrom(A,succ(succ(i)))" |
|
123 |
apply (unfold Pair_def) |
|
124 |
apply (blast intro: doubleton_in_Vfrom) |
|
125 |
done |
|
126 |
||
127 |
lemma succ_in_Vfrom: "a <= Vfrom(A,i) ==> succ(a) : Vfrom(A,succ(succ(i)))" |
|
128 |
apply (intro subset_mem_Vfrom succ_subsetI, assumption) |
|
129 |
apply (erule subset_trans) |
|
130 |
apply (rule Vfrom_mono [OF subset_refl subset_succI]) |
|
131 |
done |
|
132 |
||
133 |
subsection{* 0, successor and limit equations fof Vfrom *} |
|
134 |
||
135 |
lemma Vfrom_0: "Vfrom(A,0) = A" |
|
136 |
by (subst Vfrom, blast) |
|
137 |
||
138 |
lemma Vfrom_succ_lemma: "Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))" |
|
139 |
apply (rule Vfrom [THEN trans]) |
|
140 |
apply (rule equalityI [THEN subst_context, |
|
141 |
OF _ succI1 [THEN RepFunI, THEN Union_upper]]) |
|
142 |
apply (rule UN_least) |
|
143 |
apply (rule subset_refl [THEN Vfrom_mono, THEN Pow_mono]) |
|
144 |
apply (erule ltI [THEN le_imp_subset]) |
|
145 |
apply (erule Ord_succ) |
|
146 |
done |
|
147 |
||
148 |
lemma Vfrom_succ: "Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))" |
|
149 |
apply (rule_tac x1 = "succ (i)" in Vfrom_rank_eq [THEN subst]) |
|
150 |
apply (rule_tac x1 = "i" in Vfrom_rank_eq [THEN subst]) |
|
151 |
apply (subst rank_succ) |
|
152 |
apply (rule Ord_rank [THEN Vfrom_succ_lemma]) |
|
153 |
done |
|
154 |
||
155 |
(*The premise distinguishes this from Vfrom(A,0); allowing X=0 forces |
|
156 |
the conclusion to be Vfrom(A,Union(X)) = A Un (UN y:X. Vfrom(A,y)) *) |
|
157 |
lemma Vfrom_Union: "y:X ==> Vfrom(A,Union(X)) = (UN y:X. Vfrom(A,y))" |
|
158 |
apply (subst Vfrom) |
|
159 |
apply (rule equalityI) |
|
160 |
txt{*first inclusion*} |
|
161 |
apply (rule Un_least) |
|
162 |
apply (rule A_subset_Vfrom [THEN subset_trans]) |
|
163 |
apply (rule UN_upper, assumption) |
|
164 |
apply (rule UN_least) |
|
165 |
apply (erule UnionE) |
|
166 |
apply (rule subset_trans) |
|
167 |
apply (erule_tac [2] UN_upper, |
|
168 |
subst Vfrom, erule subset_trans [OF UN_upper Un_upper2]) |
|
169 |
txt{*opposite inclusion*} |
|
170 |
apply (rule UN_least) |
|
171 |
apply (subst Vfrom, blast) |
|
172 |
done |
|
173 |
||
174 |
subsection{* Vfrom applied to Limit ordinals *} |
|
175 |
||
176 |
(*NB. limit ordinals are non-empty: |
|
177 |
Vfrom(A,0) = A = A Un (UN y:0. Vfrom(A,y)) *) |
|
178 |
lemma Limit_Vfrom_eq: |
|
179 |
"Limit(i) ==> Vfrom(A,i) = (UN y:i. Vfrom(A,y))" |
|
180 |
apply (rule Limit_has_0 [THEN ltD, THEN Vfrom_Union, THEN subst], assumption) |
|
181 |
apply (simp add: Limit_Union_eq) |
|
182 |
done |
|
183 |
||
184 |
lemma Limit_VfromE: |
|
185 |
"[| a: Vfrom(A,i); ~R ==> Limit(i); |
|
186 |
!!x. [| x<i; a: Vfrom(A,x) |] ==> R |
|
187 |
|] ==> R" |
|
188 |
apply (rule classical) |
|
189 |
apply (rule Limit_Vfrom_eq [THEN equalityD1, THEN subsetD, THEN UN_E]) |
|
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
190 |
prefer 2 apply assumption |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
191 |
apply blast |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
192 |
apply (blast intro: ltI Limit_is_Ord) |
13163 | 193 |
done |
194 |
||
195 |
lemmas zero_in_VLimit = Limit_has_0 [THEN ltD, THEN zero_in_Vfrom, standard] |
|
196 |
||
197 |
lemma singleton_in_VLimit: |
|
198 |
"[| a: Vfrom(A,i); Limit(i) |] ==> {a} : Vfrom(A,i)" |
|
199 |
apply (erule Limit_VfromE, assumption) |
|
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
200 |
apply (erule singleton_in_Vfrom [THEN VfromI]) |
13163 | 201 |
apply (blast intro: Limit_has_succ) |
202 |
done |
|
203 |
||
204 |
lemmas Vfrom_UnI1 = |
|
205 |
Un_upper1 [THEN subset_refl [THEN Vfrom_mono, THEN subsetD], standard] |
|
206 |
lemmas Vfrom_UnI2 = |
|
207 |
Un_upper2 [THEN subset_refl [THEN Vfrom_mono, THEN subsetD], standard] |
|
208 |
||
209 |
text{*Hard work is finding a single j:i such that {a,b}<=Vfrom(A,j)*} |
|
210 |
lemma doubleton_in_VLimit: |
|
211 |
"[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i) |] ==> {a,b} : Vfrom(A,i)" |
|
212 |
apply (erule Limit_VfromE, assumption) |
|
213 |
apply (erule Limit_VfromE, assumption) |
|
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
214 |
apply (blast intro: VfromI [OF doubleton_in_Vfrom] |
13163 | 215 |
Vfrom_UnI1 Vfrom_UnI2 Limit_has_succ Un_least_lt) |
216 |
done |
|
217 |
||
218 |
lemma Pair_in_VLimit: |
|
219 |
"[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i) |] ==> <a,b> : Vfrom(A,i)" |
|
220 |
txt{*Infer that a, b occur at ordinals x,xa < i.*} |
|
221 |
apply (erule Limit_VfromE, assumption) |
|
222 |
apply (erule Limit_VfromE, assumption) |
|
223 |
txt{*Infer that succ(succ(x Un xa)) < i *} |
|
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
224 |
apply (blast intro: VfromI [OF Pair_in_Vfrom] |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
225 |
Vfrom_UnI1 Vfrom_UnI2 Limit_has_succ Un_least_lt) |
13163 | 226 |
done |
227 |
||
228 |
lemma product_VLimit: "Limit(i) ==> Vfrom(A,i) * Vfrom(A,i) <= Vfrom(A,i)" |
|
229 |
by (blast intro: Pair_in_VLimit) |
|
230 |
||
231 |
lemmas Sigma_subset_VLimit = |
|
232 |
subset_trans [OF Sigma_mono product_VLimit] |
|
233 |
||
234 |
lemmas nat_subset_VLimit = |
|
235 |
subset_trans [OF nat_le_Limit [THEN le_imp_subset] i_subset_Vfrom] |
|
236 |
||
237 |
lemma nat_into_VLimit: "[| n: nat; Limit(i) |] ==> n : Vfrom(A,i)" |
|
238 |
by (blast intro: nat_subset_VLimit [THEN subsetD]) |
|
239 |
||
240 |
subsubsection{* Closure under disjoint union *} |
|
241 |
||
242 |
lemmas zero_in_VLimit = Limit_has_0 [THEN ltD, THEN zero_in_Vfrom, standard] |
|
243 |
||
244 |
lemma one_in_VLimit: "Limit(i) ==> 1 : Vfrom(A,i)" |
|
245 |
by (blast intro: nat_into_VLimit) |
|
246 |
||
247 |
lemma Inl_in_VLimit: |
|
248 |
"[| a: Vfrom(A,i); Limit(i) |] ==> Inl(a) : Vfrom(A,i)" |
|
249 |
apply (unfold Inl_def) |
|
250 |
apply (blast intro: zero_in_VLimit Pair_in_VLimit) |
|
251 |
done |
|
252 |
||
253 |
lemma Inr_in_VLimit: |
|
254 |
"[| b: Vfrom(A,i); Limit(i) |] ==> Inr(b) : Vfrom(A,i)" |
|
255 |
apply (unfold Inr_def) |
|
256 |
apply (blast intro: one_in_VLimit Pair_in_VLimit) |
|
257 |
done |
|
258 |
||
259 |
lemma sum_VLimit: "Limit(i) ==> Vfrom(C,i)+Vfrom(C,i) <= Vfrom(C,i)" |
|
260 |
by (blast intro!: Inl_in_VLimit Inr_in_VLimit) |
|
261 |
||
262 |
lemmas sum_subset_VLimit = subset_trans [OF sum_mono sum_VLimit] |
|
263 |
||
264 |
||
265 |
||
266 |
subsection{* Properties assuming Transset(A) *} |
|
267 |
||
268 |
lemma Transset_Vfrom: "Transset(A) ==> Transset(Vfrom(A,i))" |
|
269 |
apply (rule_tac a=i in eps_induct) |
|
270 |
apply (subst Vfrom) |
|
271 |
apply (blast intro!: Transset_Union_family Transset_Un Transset_Pow) |
|
272 |
done |
|
273 |
||
274 |
lemma Transset_Vfrom_succ: |
|
275 |
"Transset(A) ==> Vfrom(A, succ(i)) = Pow(Vfrom(A,i))" |
|
276 |
apply (rule Vfrom_succ [THEN trans]) |
|
277 |
apply (rule equalityI [OF _ Un_upper2]) |
|
278 |
apply (rule Un_least [OF _ subset_refl]) |
|
279 |
apply (rule A_subset_Vfrom [THEN subset_trans]) |
|
280 |
apply (erule Transset_Vfrom [THEN Transset_iff_Pow [THEN iffD1]]) |
|
281 |
done |
|
282 |
||
283 |
lemma Transset_Pair_subset: "[| <a,b> <= C; Transset(C) |] ==> a: C & b: C" |
|
284 |
by (unfold Pair_def Transset_def, blast) |
|
285 |
||
286 |
lemma Transset_Pair_subset_VLimit: |
|
287 |
"[| <a,b> <= Vfrom(A,i); Transset(A); Limit(i) |] |
|
288 |
==> <a,b> : Vfrom(A,i)" |
|
289 |
apply (erule Transset_Pair_subset [THEN conjE]) |
|
290 |
apply (erule Transset_Vfrom) |
|
291 |
apply (blast intro: Pair_in_VLimit) |
|
292 |
done |
|
293 |
||
294 |
lemma Union_in_Vfrom: |
|
295 |
"[| X: Vfrom(A,j); Transset(A) |] ==> Union(X) : Vfrom(A, succ(j))" |
|
296 |
apply (drule Transset_Vfrom) |
|
297 |
apply (rule subset_mem_Vfrom) |
|
298 |
apply (unfold Transset_def, blast) |
|
299 |
done |
|
300 |
||
301 |
lemma Union_in_VLimit: |
|
302 |
"[| X: Vfrom(A,i); Limit(i); Transset(A) |] ==> Union(X) : Vfrom(A,i)" |
|
303 |
apply (rule Limit_VfromE, assumption+) |
|
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
304 |
apply (blast intro: Limit_has_succ VfromI Union_in_Vfrom) |
13163 | 305 |
done |
306 |
||
307 |
||
308 |
(*** Closure under product/sum applied to elements -- thus Vfrom(A,i) |
|
309 |
is a model of simple type theory provided A is a transitive set |
|
310 |
and i is a limit ordinal |
|
311 |
***) |
|
312 |
||
313 |
text{*General theorem for membership in Vfrom(A,i) when i is a limit ordinal*} |
|
314 |
lemma in_VLimit: |
|
315 |
"[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); |
|
316 |
!!x y j. [| j<i; 1:j; x: Vfrom(A,j); y: Vfrom(A,j) |] |
|
317 |
==> EX k. h(x,y): Vfrom(A,k) & k<i |] |
|
318 |
==> h(a,b) : Vfrom(A,i)" |
|
319 |
txt{*Infer that a, b occur at ordinals x,xa < i.*} |
|
320 |
apply (erule Limit_VfromE, assumption) |
|
321 |
apply (erule Limit_VfromE, assumption, atomize) |
|
322 |
apply (drule_tac x=a in spec) |
|
323 |
apply (drule_tac x=b in spec) |
|
324 |
apply (drule_tac x="x Un xa Un 2" in spec) |
|
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
325 |
apply (simp add: Un_least_lt_iff lt_Ord Vfrom_UnI1 Vfrom_UnI2) |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
326 |
apply (blast intro: Limit_has_0 Limit_has_succ VfromI) |
13163 | 327 |
done |
328 |
||
329 |
subsubsection{* products *} |
|
330 |
||
331 |
lemma prod_in_Vfrom: |
|
332 |
"[| a: Vfrom(A,j); b: Vfrom(A,j); Transset(A) |] |
|
333 |
==> a*b : Vfrom(A, succ(succ(succ(j))))" |
|
334 |
apply (drule Transset_Vfrom) |
|
335 |
apply (rule subset_mem_Vfrom) |
|
336 |
apply (unfold Transset_def) |
|
337 |
apply (blast intro: Pair_in_Vfrom) |
|
338 |
done |
|
339 |
||
340 |
lemma prod_in_VLimit: |
|
341 |
"[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) |] |
|
342 |
==> a*b : Vfrom(A,i)" |
|
343 |
apply (erule in_VLimit, assumption+) |
|
344 |
apply (blast intro: prod_in_Vfrom Limit_has_succ) |
|
345 |
done |
|
346 |
||
347 |
subsubsection{* Disjoint sums, aka Quine ordered pairs *} |
|
348 |
||
349 |
lemma sum_in_Vfrom: |
|
350 |
"[| a: Vfrom(A,j); b: Vfrom(A,j); Transset(A); 1:j |] |
|
351 |
==> a+b : Vfrom(A, succ(succ(succ(j))))" |
|
352 |
apply (unfold sum_def) |
|
353 |
apply (drule Transset_Vfrom) |
|
354 |
apply (rule subset_mem_Vfrom) |
|
355 |
apply (unfold Transset_def) |
|
356 |
apply (blast intro: zero_in_Vfrom Pair_in_Vfrom i_subset_Vfrom [THEN subsetD]) |
|
357 |
done |
|
358 |
||
359 |
lemma sum_in_VLimit: |
|
360 |
"[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) |] |
|
361 |
==> a+b : Vfrom(A,i)" |
|
362 |
apply (erule in_VLimit, assumption+) |
|
363 |
apply (blast intro: sum_in_Vfrom Limit_has_succ) |
|
364 |
done |
|
365 |
||
366 |
subsubsection{* function space! *} |
|
367 |
||
368 |
lemma fun_in_Vfrom: |
|
369 |
"[| a: Vfrom(A,j); b: Vfrom(A,j); Transset(A) |] ==> |
|
370 |
a->b : Vfrom(A, succ(succ(succ(succ(j)))))" |
|
371 |
apply (unfold Pi_def) |
|
372 |
apply (drule Transset_Vfrom) |
|
373 |
apply (rule subset_mem_Vfrom) |
|
374 |
apply (rule Collect_subset [THEN subset_trans]) |
|
375 |
apply (subst Vfrom) |
|
376 |
apply (rule subset_trans [THEN subset_trans]) |
|
377 |
apply (rule_tac [3] Un_upper2) |
|
378 |
apply (rule_tac [2] succI1 [THEN UN_upper]) |
|
379 |
apply (rule Pow_mono) |
|
380 |
apply (unfold Transset_def) |
|
381 |
apply (blast intro: Pair_in_Vfrom) |
|
382 |
done |
|
383 |
||
384 |
lemma fun_in_VLimit: |
|
385 |
"[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) |] |
|
386 |
==> a->b : Vfrom(A,i)" |
|
387 |
apply (erule in_VLimit, assumption+) |
|
388 |
apply (blast intro: fun_in_Vfrom Limit_has_succ) |
|
389 |
done |
|
390 |
||
391 |
lemma Pow_in_Vfrom: |
|
392 |
"[| a: Vfrom(A,j); Transset(A) |] ==> Pow(a) : Vfrom(A, succ(succ(j)))" |
|
393 |
apply (drule Transset_Vfrom) |
|
394 |
apply (rule subset_mem_Vfrom) |
|
395 |
apply (unfold Transset_def) |
|
396 |
apply (subst Vfrom, blast) |
|
397 |
done |
|
398 |
||
399 |
lemma Pow_in_VLimit: |
|
400 |
"[| a: Vfrom(A,i); Limit(i); Transset(A) |] ==> Pow(a) : Vfrom(A,i)" |
|
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
401 |
by (blast elim: Limit_VfromE intro: Limit_has_succ Pow_in_Vfrom VfromI) |
13163 | 402 |
|
403 |
||
404 |
subsection{* The set Vset(i) *} |
|
405 |
||
406 |
lemma Vset: "Vset(i) = (UN j:i. Pow(Vset(j)))" |
|
407 |
by (subst Vfrom, blast) |
|
408 |
||
409 |
lemmas Vset_succ = Transset_0 [THEN Transset_Vfrom_succ, standard] |
|
410 |
lemmas Transset_Vset = Transset_0 [THEN Transset_Vfrom, standard] |
|
411 |
||
412 |
subsubsection{* Characterisation of the elements of Vset(i) *} |
|
413 |
||
414 |
lemma VsetD [rule_format]: "Ord(i) ==> ALL b. b : Vset(i) --> rank(b) < i" |
|
415 |
apply (erule trans_induct) |
|
416 |
apply (subst Vset, safe) |
|
417 |
apply (subst rank) |
|
418 |
apply (blast intro: ltI UN_succ_least_lt) |
|
419 |
done |
|
420 |
||
421 |
lemma VsetI_lemma [rule_format]: |
|
422 |
"Ord(i) ==> ALL b. rank(b) : i --> b : Vset(i)" |
|
423 |
apply (erule trans_induct) |
|
424 |
apply (rule allI) |
|
425 |
apply (subst Vset) |
|
426 |
apply (blast intro!: rank_lt [THEN ltD]) |
|
427 |
done |
|
428 |
||
429 |
lemma VsetI: "rank(x)<i ==> x : Vset(i)" |
|
430 |
by (blast intro: VsetI_lemma elim: ltE) |
|
431 |
||
432 |
text{*Merely a lemma for the next result*} |
|
433 |
lemma Vset_Ord_rank_iff: "Ord(i) ==> b : Vset(i) <-> rank(b) < i" |
|
434 |
by (blast intro: VsetD VsetI) |
|
435 |
||
436 |
lemma Vset_rank_iff [simp]: "b : Vset(a) <-> rank(b) < rank(a)" |
|
437 |
apply (rule Vfrom_rank_eq [THEN subst]) |
|
438 |
apply (rule Ord_rank [THEN Vset_Ord_rank_iff]) |
|
439 |
done |
|
440 |
||
441 |
text{*This is rank(rank(a)) = rank(a) *} |
|
442 |
declare Ord_rank [THEN rank_of_Ord, simp] |
|
443 |
||
444 |
lemma rank_Vset: "Ord(i) ==> rank(Vset(i)) = i" |
|
445 |
apply (subst rank) |
|
446 |
apply (rule equalityI, safe) |
|
447 |
apply (blast intro: VsetD [THEN ltD]) |
|
448 |
apply (blast intro: VsetD [THEN ltD] Ord_trans) |
|
449 |
apply (blast intro: i_subset_Vfrom [THEN subsetD] |
|
450 |
Ord_in_Ord [THEN rank_of_Ord, THEN ssubst]) |
|
451 |
done |
|
452 |
||
453 |
subsubsection{* Lemmas for reasoning about sets in terms of their elements' ranks *} |
|
0 | 454 |
|
13163 | 455 |
lemma arg_subset_Vset_rank: "a <= Vset(rank(a))" |
456 |
apply (rule subsetI) |
|
457 |
apply (erule rank_lt [THEN VsetI]) |
|
458 |
done |
|
459 |
||
460 |
lemma Int_Vset_subset: |
|
461 |
"[| !!i. Ord(i) ==> a Int Vset(i) <= b |] ==> a <= b" |
|
462 |
apply (rule subset_trans) |
|
463 |
apply (rule Int_greatest [OF subset_refl arg_subset_Vset_rank]) |
|
464 |
apply (blast intro: Ord_rank) |
|
465 |
done |
|
466 |
||
467 |
subsubsection{* Set up an environment for simplification *} |
|
468 |
||
469 |
lemma rank_Inl: "rank(a) < rank(Inl(a))" |
|
470 |
apply (unfold Inl_def) |
|
471 |
apply (rule rank_pair2) |
|
472 |
done |
|
473 |
||
474 |
lemma rank_Inr: "rank(a) < rank(Inr(a))" |
|
475 |
apply (unfold Inr_def) |
|
476 |
apply (rule rank_pair2) |
|
477 |
done |
|
478 |
||
479 |
lemmas rank_rls = rank_Inl rank_Inr rank_pair1 rank_pair2 |
|
480 |
||
481 |
subsubsection{* Recursion over Vset levels! *} |
|
482 |
||
483 |
text{*NOT SUITABLE FOR REWRITING: recursive!*} |
|
484 |
lemma Vrec: "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))" |
|
485 |
apply (unfold Vrec_def) |
|
486 |
apply (subst transrec) |
|
487 |
apply simp |
|
13175
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13163
diff
changeset
|
488 |
apply (rule refl [THEN lam_cong, THEN subst_context], simp add: lt_def) |
13163 | 489 |
done |
490 |
||
491 |
text{*This form avoids giant explosions in proofs. NOTE USE OF == *} |
|
492 |
lemma def_Vrec: |
|
493 |
"[| !!x. h(x)==Vrec(x,H) |] ==> |
|
494 |
h(a) = H(a, lam x: Vset(rank(a)). h(x))" |
|
495 |
apply simp |
|
496 |
apply (rule Vrec) |
|
497 |
done |
|
498 |
||
499 |
text{*NOT SUITABLE FOR REWRITING: recursive!*} |
|
500 |
lemma Vrecursor: |
|
501 |
"Vrecursor(H,a) = H(lam x:Vset(rank(a)). Vrecursor(H,x), a)" |
|
502 |
apply (unfold Vrecursor_def) |
|
503 |
apply (subst transrec, simp) |
|
13175
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13163
diff
changeset
|
504 |
apply (rule refl [THEN lam_cong, THEN subst_context], simp add: lt_def) |
13163 | 505 |
done |
506 |
||
507 |
text{*This form avoids giant explosions in proofs. NOTE USE OF == *} |
|
508 |
lemma def_Vrecursor: |
|
509 |
"h == Vrecursor(H) ==> h(a) = H(lam x: Vset(rank(a)). h(x), a)" |
|
510 |
apply simp |
|
511 |
apply (rule Vrecursor) |
|
512 |
done |
|
513 |
||
514 |
||
515 |
subsection{* univ(A) *} |
|
516 |
||
517 |
lemma univ_mono: "A<=B ==> univ(A) <= univ(B)" |
|
518 |
apply (unfold univ_def) |
|
519 |
apply (erule Vfrom_mono) |
|
520 |
apply (rule subset_refl) |
|
521 |
done |
|
522 |
||
523 |
lemma Transset_univ: "Transset(A) ==> Transset(univ(A))" |
|
524 |
apply (unfold univ_def) |
|
525 |
apply (erule Transset_Vfrom) |
|
526 |
done |
|
527 |
||
528 |
subsubsection{* univ(A) as a limit *} |
|
529 |
||
530 |
lemma univ_eq_UN: "univ(A) = (UN i:nat. Vfrom(A,i))" |
|
531 |
apply (unfold univ_def) |
|
532 |
apply (rule Limit_nat [THEN Limit_Vfrom_eq]) |
|
533 |
done |
|
534 |
||
535 |
lemma subset_univ_eq_Int: "c <= univ(A) ==> c = (UN i:nat. c Int Vfrom(A,i))" |
|
536 |
apply (rule subset_UN_iff_eq [THEN iffD1]) |
|
537 |
apply (erule univ_eq_UN [THEN subst]) |
|
538 |
done |
|
539 |
||
540 |
lemma univ_Int_Vfrom_subset: |
|
541 |
"[| a <= univ(X); |
|
542 |
!!i. i:nat ==> a Int Vfrom(X,i) <= b |] |
|
543 |
==> a <= b" |
|
544 |
apply (subst subset_univ_eq_Int, assumption) |
|
545 |
apply (rule UN_least, simp) |
|
546 |
done |
|
547 |
||
548 |
lemma univ_Int_Vfrom_eq: |
|
549 |
"[| a <= univ(X); b <= univ(X); |
|
550 |
!!i. i:nat ==> a Int Vfrom(X,i) = b Int Vfrom(X,i) |
|
551 |
|] ==> a = b" |
|
552 |
apply (rule equalityI) |
|
553 |
apply (rule univ_Int_Vfrom_subset, assumption) |
|
554 |
apply (blast elim: equalityCE) |
|
555 |
apply (rule univ_Int_Vfrom_subset, assumption) |
|
556 |
apply (blast elim: equalityCE) |
|
557 |
done |
|
558 |
||
559 |
subsubsection{* Closure properties *} |
|
560 |
||
561 |
lemma zero_in_univ: "0 : univ(A)" |
|
562 |
apply (unfold univ_def) |
|
563 |
apply (rule nat_0I [THEN zero_in_Vfrom]) |
|
564 |
done |
|
565 |
||
566 |
lemma A_subset_univ: "A <= univ(A)" |
|
567 |
apply (unfold univ_def) |
|
568 |
apply (rule A_subset_Vfrom) |
|
569 |
done |
|
570 |
||
571 |
lemmas A_into_univ = A_subset_univ [THEN subsetD, standard] |
|
572 |
||
573 |
subsubsection{* Closure under unordered and ordered pairs *} |
|
574 |
||
575 |
lemma singleton_in_univ: "a: univ(A) ==> {a} : univ(A)" |
|
576 |
apply (unfold univ_def) |
|
577 |
apply (blast intro: singleton_in_VLimit Limit_nat) |
|
578 |
done |
|
579 |
||
580 |
lemma doubleton_in_univ: |
|
581 |
"[| a: univ(A); b: univ(A) |] ==> {a,b} : univ(A)" |
|
582 |
apply (unfold univ_def) |
|
583 |
apply (blast intro: doubleton_in_VLimit Limit_nat) |
|
584 |
done |
|
585 |
||
586 |
lemma Pair_in_univ: |
|
587 |
"[| a: univ(A); b: univ(A) |] ==> <a,b> : univ(A)" |
|
588 |
apply (unfold univ_def) |
|
589 |
apply (blast intro: Pair_in_VLimit Limit_nat) |
|
590 |
done |
|
591 |
||
592 |
lemma Union_in_univ: |
|
593 |
"[| X: univ(A); Transset(A) |] ==> Union(X) : univ(A)" |
|
594 |
apply (unfold univ_def) |
|
595 |
apply (blast intro: Union_in_VLimit Limit_nat) |
|
596 |
done |
|
597 |
||
598 |
lemma product_univ: "univ(A)*univ(A) <= univ(A)" |
|
599 |
apply (unfold univ_def) |
|
600 |
apply (rule Limit_nat [THEN product_VLimit]) |
|
601 |
done |
|
602 |
||
603 |
||
604 |
subsubsection{* The natural numbers *} |
|
605 |
||
606 |
lemma nat_subset_univ: "nat <= univ(A)" |
|
607 |
apply (unfold univ_def) |
|
608 |
apply (rule i_subset_Vfrom) |
|
609 |
done |
|
610 |
||
611 |
text{* n:nat ==> n:univ(A) *} |
|
612 |
lemmas nat_into_univ = nat_subset_univ [THEN subsetD, standard] |
|
613 |
||
614 |
subsubsection{* instances for 1 and 2 *} |
|
615 |
||
616 |
lemma one_in_univ: "1 : univ(A)" |
|
617 |
apply (unfold univ_def) |
|
618 |
apply (rule Limit_nat [THEN one_in_VLimit]) |
|
619 |
done |
|
620 |
||
621 |
text{*unused!*} |
|
622 |
lemma two_in_univ: "2 : univ(A)" |
|
623 |
by (blast intro: nat_into_univ) |
|
624 |
||
625 |
lemma bool_subset_univ: "bool <= univ(A)" |
|
626 |
apply (unfold bool_def) |
|
627 |
apply (blast intro!: zero_in_univ one_in_univ) |
|
628 |
done |
|
629 |
||
630 |
lemmas bool_into_univ = bool_subset_univ [THEN subsetD, standard] |
|
631 |
||
632 |
||
633 |
subsubsection{* Closure under disjoint union *} |
|
634 |
||
635 |
lemma Inl_in_univ: "a: univ(A) ==> Inl(a) : univ(A)" |
|
636 |
apply (unfold univ_def) |
|
637 |
apply (erule Inl_in_VLimit [OF _ Limit_nat]) |
|
638 |
done |
|
639 |
||
640 |
lemma Inr_in_univ: "b: univ(A) ==> Inr(b) : univ(A)" |
|
641 |
apply (unfold univ_def) |
|
642 |
apply (erule Inr_in_VLimit [OF _ Limit_nat]) |
|
643 |
done |
|
644 |
||
645 |
lemma sum_univ: "univ(C)+univ(C) <= univ(C)" |
|
646 |
apply (unfold univ_def) |
|
647 |
apply (rule Limit_nat [THEN sum_VLimit]) |
|
648 |
done |
|
649 |
||
650 |
lemmas sum_subset_univ = subset_trans [OF sum_mono sum_univ] |
|
651 |
||
652 |
||
653 |
subsubsection{* Closure under binary union -- use Un_least *} |
|
654 |
subsubsection{* Closure under Collect -- use (Collect_subset RS subset_trans) *} |
|
655 |
subsubsection{* Closure under RepFun -- use RepFun_subset *} |
|
656 |
||
657 |
||
658 |
subsection{* Finite Branching Closure Properties *} |
|
659 |
||
660 |
subsubsection{* Closure under finite powerset *} |
|
661 |
||
662 |
lemma Fin_Vfrom_lemma: |
|
663 |
"[| b: Fin(Vfrom(A,i)); Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j<i" |
|
664 |
apply (erule Fin_induct) |
|
665 |
apply (blast dest!: Limit_has_0, safe) |
|
666 |
apply (erule Limit_VfromE, assumption) |
|
667 |
apply (blast intro!: Un_least_lt intro: Vfrom_UnI1 Vfrom_UnI2) |
|
668 |
done |
|
0 | 669 |
|
13163 | 670 |
lemma Fin_VLimit: "Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)" |
671 |
apply (rule subsetI) |
|
672 |
apply (drule Fin_Vfrom_lemma, safe) |
|
673 |
apply (rule Vfrom [THEN ssubst]) |
|
674 |
apply (blast dest!: ltD) |
|
675 |
done |
|
676 |
||
677 |
lemmas Fin_subset_VLimit = subset_trans [OF Fin_mono Fin_VLimit] |
|
678 |
||
679 |
lemma Fin_univ: "Fin(univ(A)) <= univ(A)" |
|
680 |
apply (unfold univ_def) |
|
681 |
apply (rule Limit_nat [THEN Fin_VLimit]) |
|
682 |
done |
|
683 |
||
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
684 |
subsubsection{* Closure under finite powers: functions from a natural number *} |
13163 | 685 |
|
686 |
lemma nat_fun_VLimit: |
|
687 |
"[| n: nat; Limit(i) |] ==> n -> Vfrom(A,i) <= Vfrom(A,i)" |
|
688 |
apply (erule nat_fun_subset_Fin [THEN subset_trans]) |
|
689 |
apply (blast del: subsetI |
|
690 |
intro: subset_refl Fin_subset_VLimit Sigma_subset_VLimit nat_subset_VLimit) |
|
691 |
done |
|
692 |
||
693 |
lemmas nat_fun_subset_VLimit = subset_trans [OF Pi_mono nat_fun_VLimit] |
|
694 |
||
695 |
lemma nat_fun_univ: "n: nat ==> n -> univ(A) <= univ(A)" |
|
696 |
apply (unfold univ_def) |
|
697 |
apply (erule nat_fun_VLimit [OF _ Limit_nat]) |
|
698 |
done |
|
699 |
||
700 |
||
701 |
subsubsection{* Closure under finite function space *} |
|
702 |
||
703 |
text{*General but seldom-used version; normally the domain is fixed*} |
|
704 |
lemma FiniteFun_VLimit1: |
|
705 |
"Limit(i) ==> Vfrom(A,i) -||> Vfrom(A,i) <= Vfrom(A,i)" |
|
706 |
apply (rule FiniteFun.dom_subset [THEN subset_trans]) |
|
707 |
apply (blast del: subsetI |
|
708 |
intro: Fin_subset_VLimit Sigma_subset_VLimit subset_refl) |
|
709 |
done |
|
710 |
||
711 |
lemma FiniteFun_univ1: "univ(A) -||> univ(A) <= univ(A)" |
|
712 |
apply (unfold univ_def) |
|
713 |
apply (rule Limit_nat [THEN FiniteFun_VLimit1]) |
|
714 |
done |
|
715 |
||
716 |
text{*Version for a fixed domain*} |
|
717 |
lemma FiniteFun_VLimit: |
|
718 |
"[| W <= Vfrom(A,i); Limit(i) |] ==> W -||> Vfrom(A,i) <= Vfrom(A,i)" |
|
719 |
apply (rule subset_trans) |
|
720 |
apply (erule FiniteFun_mono [OF _ subset_refl]) |
|
721 |
apply (erule FiniteFun_VLimit1) |
|
722 |
done |
|
723 |
||
724 |
lemma FiniteFun_univ: |
|
725 |
"W <= univ(A) ==> W -||> univ(A) <= univ(A)" |
|
726 |
apply (unfold univ_def) |
|
727 |
apply (erule FiniteFun_VLimit [OF _ Limit_nat]) |
|
728 |
done |
|
729 |
||
730 |
lemma FiniteFun_in_univ: |
|
731 |
"[| f: W -||> univ(A); W <= univ(A) |] ==> f : univ(A)" |
|
732 |
by (erule FiniteFun_univ [THEN subsetD], assumption) |
|
733 |
||
734 |
text{*Remove <= from the rule above*} |
|
735 |
lemmas FiniteFun_in_univ' = FiniteFun_in_univ [OF _ subsetI] |
|
736 |
||
737 |
||
738 |
subsection{** For QUniv. Properties of Vfrom analogous to the "take-lemma" **} |
|
739 |
||
740 |
subsection{* Intersecting a*b with Vfrom... *} |
|
741 |
||
742 |
text{*This version says a, b exist one level down, in the smaller set Vfrom(X,i)*} |
|
743 |
lemma doubleton_in_Vfrom_D: |
|
744 |
"[| {a,b} : Vfrom(X,succ(i)); Transset(X) |] |
|
745 |
==> a: Vfrom(X,i) & b: Vfrom(X,i)" |
|
746 |
by (drule Transset_Vfrom_succ [THEN equalityD1, THEN subsetD, THEN PowD], |
|
747 |
assumption, fast) |
|
748 |
||
749 |
text{*This weaker version says a, b exist at the same level*} |
|
750 |
lemmas Vfrom_doubleton_D = Transset_Vfrom [THEN Transset_doubleton_D, standard] |
|
751 |
||
752 |
(** Using only the weaker theorem would prove <a,b> : Vfrom(X,i) |
|
753 |
implies a, b : Vfrom(X,i), which is useless for induction. |
|
754 |
Using only the stronger theorem would prove <a,b> : Vfrom(X,succ(succ(i))) |
|
755 |
implies a, b : Vfrom(X,i), leaving the succ(i) case untreated. |
|
756 |
The combination gives a reduction by precisely one level, which is |
|
757 |
most convenient for proofs. |
|
758 |
**) |
|
759 |
||
760 |
lemma Pair_in_Vfrom_D: |
|
761 |
"[| <a,b> : Vfrom(X,succ(i)); Transset(X) |] |
|
762 |
==> a: Vfrom(X,i) & b: Vfrom(X,i)" |
|
763 |
apply (unfold Pair_def) |
|
764 |
apply (blast dest!: doubleton_in_Vfrom_D Vfrom_doubleton_D) |
|
765 |
done |
|
766 |
||
767 |
lemma product_Int_Vfrom_subset: |
|
768 |
"Transset(X) ==> |
|
769 |
(a*b) Int Vfrom(X, succ(i)) <= (a Int Vfrom(X,i)) * (b Int Vfrom(X,i))" |
|
770 |
by (blast dest!: Pair_in_Vfrom_D) |
|
771 |
||
772 |
||
773 |
ML |
|
774 |
{* |
|
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3940
diff
changeset
|
775 |
|
13163 | 776 |
val Vfrom = thm "Vfrom"; |
777 |
val Vfrom_mono = thm "Vfrom_mono"; |
|
778 |
val Vfrom_rank_subset1 = thm "Vfrom_rank_subset1"; |
|
779 |
val Vfrom_rank_subset2 = thm "Vfrom_rank_subset2"; |
|
780 |
val Vfrom_rank_eq = thm "Vfrom_rank_eq"; |
|
781 |
val zero_in_Vfrom = thm "zero_in_Vfrom"; |
|
782 |
val i_subset_Vfrom = thm "i_subset_Vfrom"; |
|
783 |
val A_subset_Vfrom = thm "A_subset_Vfrom"; |
|
784 |
val subset_mem_Vfrom = thm "subset_mem_Vfrom"; |
|
785 |
val singleton_in_Vfrom = thm "singleton_in_Vfrom"; |
|
786 |
val doubleton_in_Vfrom = thm "doubleton_in_Vfrom"; |
|
787 |
val Pair_in_Vfrom = thm "Pair_in_Vfrom"; |
|
788 |
val succ_in_Vfrom = thm "succ_in_Vfrom"; |
|
789 |
val Vfrom_0 = thm "Vfrom_0"; |
|
790 |
val Vfrom_succ = thm "Vfrom_succ"; |
|
791 |
val Vfrom_Union = thm "Vfrom_Union"; |
|
792 |
val Limit_Vfrom_eq = thm "Limit_Vfrom_eq"; |
|
793 |
val zero_in_VLimit = thm "zero_in_VLimit"; |
|
794 |
val singleton_in_VLimit = thm "singleton_in_VLimit"; |
|
795 |
val Vfrom_UnI1 = thm "Vfrom_UnI1"; |
|
796 |
val Vfrom_UnI2 = thm "Vfrom_UnI2"; |
|
797 |
val doubleton_in_VLimit = thm "doubleton_in_VLimit"; |
|
798 |
val Pair_in_VLimit = thm "Pair_in_VLimit"; |
|
799 |
val product_VLimit = thm "product_VLimit"; |
|
800 |
val Sigma_subset_VLimit = thm "Sigma_subset_VLimit"; |
|
801 |
val nat_subset_VLimit = thm "nat_subset_VLimit"; |
|
802 |
val nat_into_VLimit = thm "nat_into_VLimit"; |
|
803 |
val zero_in_VLimit = thm "zero_in_VLimit"; |
|
804 |
val one_in_VLimit = thm "one_in_VLimit"; |
|
805 |
val Inl_in_VLimit = thm "Inl_in_VLimit"; |
|
806 |
val Inr_in_VLimit = thm "Inr_in_VLimit"; |
|
807 |
val sum_VLimit = thm "sum_VLimit"; |
|
808 |
val sum_subset_VLimit = thm "sum_subset_VLimit"; |
|
809 |
val Transset_Vfrom = thm "Transset_Vfrom"; |
|
810 |
val Transset_Vfrom_succ = thm "Transset_Vfrom_succ"; |
|
811 |
val Transset_Pair_subset = thm "Transset_Pair_subset"; |
|
812 |
val Union_in_Vfrom = thm "Union_in_Vfrom"; |
|
813 |
val Union_in_VLimit = thm "Union_in_VLimit"; |
|
814 |
val in_VLimit = thm "in_VLimit"; |
|
815 |
val prod_in_Vfrom = thm "prod_in_Vfrom"; |
|
816 |
val prod_in_VLimit = thm "prod_in_VLimit"; |
|
817 |
val sum_in_Vfrom = thm "sum_in_Vfrom"; |
|
818 |
val sum_in_VLimit = thm "sum_in_VLimit"; |
|
819 |
val fun_in_Vfrom = thm "fun_in_Vfrom"; |
|
820 |
val fun_in_VLimit = thm "fun_in_VLimit"; |
|
821 |
val Pow_in_Vfrom = thm "Pow_in_Vfrom"; |
|
822 |
val Pow_in_VLimit = thm "Pow_in_VLimit"; |
|
823 |
val Vset = thm "Vset"; |
|
824 |
val Vset_succ = thm "Vset_succ"; |
|
825 |
val Transset_Vset = thm "Transset_Vset"; |
|
826 |
val VsetD = thm "VsetD"; |
|
827 |
val VsetI = thm "VsetI"; |
|
828 |
val Vset_Ord_rank_iff = thm "Vset_Ord_rank_iff"; |
|
829 |
val Vset_rank_iff = thm "Vset_rank_iff"; |
|
830 |
val rank_Vset = thm "rank_Vset"; |
|
831 |
val arg_subset_Vset_rank = thm "arg_subset_Vset_rank"; |
|
832 |
val Int_Vset_subset = thm "Int_Vset_subset"; |
|
833 |
val rank_Inl = thm "rank_Inl"; |
|
834 |
val rank_Inr = thm "rank_Inr"; |
|
835 |
val Vrec = thm "Vrec"; |
|
836 |
val def_Vrec = thm "def_Vrec"; |
|
837 |
val Vrecursor = thm "Vrecursor"; |
|
838 |
val def_Vrecursor = thm "def_Vrecursor"; |
|
839 |
val univ_mono = thm "univ_mono"; |
|
840 |
val Transset_univ = thm "Transset_univ"; |
|
841 |
val univ_eq_UN = thm "univ_eq_UN"; |
|
842 |
val subset_univ_eq_Int = thm "subset_univ_eq_Int"; |
|
843 |
val univ_Int_Vfrom_subset = thm "univ_Int_Vfrom_subset"; |
|
844 |
val univ_Int_Vfrom_eq = thm "univ_Int_Vfrom_eq"; |
|
845 |
val zero_in_univ = thm "zero_in_univ"; |
|
846 |
val A_subset_univ = thm "A_subset_univ"; |
|
847 |
val A_into_univ = thm "A_into_univ"; |
|
848 |
val singleton_in_univ = thm "singleton_in_univ"; |
|
849 |
val doubleton_in_univ = thm "doubleton_in_univ"; |
|
850 |
val Pair_in_univ = thm "Pair_in_univ"; |
|
851 |
val Union_in_univ = thm "Union_in_univ"; |
|
852 |
val product_univ = thm "product_univ"; |
|
853 |
val nat_subset_univ = thm "nat_subset_univ"; |
|
854 |
val nat_into_univ = thm "nat_into_univ"; |
|
855 |
val one_in_univ = thm "one_in_univ"; |
|
856 |
val two_in_univ = thm "two_in_univ"; |
|
857 |
val bool_subset_univ = thm "bool_subset_univ"; |
|
858 |
val bool_into_univ = thm "bool_into_univ"; |
|
859 |
val Inl_in_univ = thm "Inl_in_univ"; |
|
860 |
val Inr_in_univ = thm "Inr_in_univ"; |
|
861 |
val sum_univ = thm "sum_univ"; |
|
862 |
val sum_subset_univ = thm "sum_subset_univ"; |
|
863 |
val Fin_VLimit = thm "Fin_VLimit"; |
|
864 |
val Fin_subset_VLimit = thm "Fin_subset_VLimit"; |
|
865 |
val Fin_univ = thm "Fin_univ"; |
|
866 |
val nat_fun_VLimit = thm "nat_fun_VLimit"; |
|
867 |
val nat_fun_subset_VLimit = thm "nat_fun_subset_VLimit"; |
|
868 |
val nat_fun_univ = thm "nat_fun_univ"; |
|
869 |
val FiniteFun_VLimit1 = thm "FiniteFun_VLimit1"; |
|
870 |
val FiniteFun_univ1 = thm "FiniteFun_univ1"; |
|
871 |
val FiniteFun_VLimit = thm "FiniteFun_VLimit"; |
|
872 |
val FiniteFun_univ = thm "FiniteFun_univ"; |
|
873 |
val FiniteFun_in_univ = thm "FiniteFun_in_univ"; |
|
874 |
val FiniteFun_in_univ' = thm "FiniteFun_in_univ'"; |
|
875 |
val doubleton_in_Vfrom_D = thm "doubleton_in_Vfrom_D"; |
|
876 |
val Vfrom_doubleton_D = thm "Vfrom_doubleton_D"; |
|
877 |
val Pair_in_Vfrom_D = thm "Pair_in_Vfrom_D"; |
|
878 |
val product_Int_Vfrom_subset = thm "product_Int_Vfrom_subset"; |
|
879 |
||
880 |
val rank_rls = thms "rank_rls"; |
|
881 |
val rank_ss = simpset() addsimps [VsetI] |
|
882 |
addsimps rank_rls @ (rank_rls RLN (2, [lt_trans])); |
|
883 |
||
884 |
*} |
|
0 | 885 |
|
886 |
end |