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