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