src/ZF/Univ.ML
author lcp
Fri Sep 17 16:16:38 1993 +0200 (1993-09-17)
changeset 6 8ce8c4d13d4d
parent 0 a5a9c433f639
child 15 6c6d2f6e3185
permissions -rw-r--r--
Installation of new simplifier for ZF. Deleted all congruence rules not
involving local assumptions. NB the congruence rules for Sigma and Pi
(dependent type constructions) cause difficulties and are not used by
default.
     1 (*  Title: 	ZF/univ
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     5 
     6 The cumulative hierarchy and a small universe for recursive types
     7 *)
     8 
     9 open Univ;
    10 
    11 (*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
    12 goal Univ.thy "Vfrom(A,i) = A Un (UN j:i. Pow(Vfrom(A,j)))";
    13 by (rtac (Vfrom_def RS def_transrec RS ssubst) 1);
    14 by (simp_tac ZF_ss 1);
    15 val Vfrom = result();
    16 
    17 (** Monotonicity **)
    18 
    19 goal Univ.thy "!!A B. A<=B ==> ALL j. i<=j --> Vfrom(A,i) <= Vfrom(B,j)";
    20 by (eps_ind_tac "i" 1);
    21 by (rtac (impI RS allI) 1);
    22 by (rtac (Vfrom RS ssubst) 1);
    23 by (rtac (Vfrom RS ssubst) 1);
    24 by (etac Un_mono 1);
    25 by (rtac UN_mono 1);
    26 by (assume_tac 1);
    27 by (rtac Pow_mono 1);
    28 by (etac (bspec RS spec RS mp) 1);
    29 by (assume_tac 1);
    30 by (rtac subset_refl 1);
    31 val Vfrom_mono_lemma = result();
    32 
    33 (*  [| A<=B; i<=x |] ==> Vfrom(A,i) <= Vfrom(B,x)  *)
    34 val Vfrom_mono = standard (Vfrom_mono_lemma RS spec RS mp);
    35 
    36 
    37 (** A fundamental equality: Vfrom does not require ordinals! **)
    38 
    39 goal Univ.thy "Vfrom(A,x) <= Vfrom(A,rank(x))";
    40 by (eps_ind_tac "x" 1);
    41 by (rtac (Vfrom RS ssubst) 1);
    42 by (rtac (Vfrom RS ssubst) 1);
    43 by (fast_tac (ZF_cs addSIs [rank_lt]) 1);
    44 val Vfrom_rank_subset1 = result();
    45 
    46 goal Univ.thy "Vfrom(A,rank(x)) <= Vfrom(A,x)";
    47 by (eps_ind_tac "x" 1);
    48 by (rtac (Vfrom RS ssubst) 1);
    49 by (rtac (Vfrom RS ssubst) 1);
    50 br (subset_refl RS Un_mono) 1;
    51 br UN_least 1;
    52 by (etac (rank_implies_mem RS bexE) 1);
    53 br subset_trans 1;
    54 be UN_upper 2;
    55 by (etac (subset_refl RS Vfrom_mono RS subset_trans RS Pow_mono) 1);
    56 by (etac bspec 1);
    57 by (assume_tac 1);
    58 val Vfrom_rank_subset2 = result();
    59 
    60 goal Univ.thy "Vfrom(A,rank(x)) = Vfrom(A,x)";
    61 by (rtac equalityI 1);
    62 by (rtac Vfrom_rank_subset2 1);
    63 by (rtac Vfrom_rank_subset1 1);
    64 val Vfrom_rank_eq = result();
    65 
    66 
    67 (*** Basic closure properties ***)
    68 
    69 goal Univ.thy "!!x y. y:x ==> 0 : Vfrom(A,x)";
    70 by (rtac (Vfrom RS ssubst) 1);
    71 by (fast_tac ZF_cs 1);
    72 val zero_in_Vfrom = result();
    73 
    74 goal Univ.thy "i <= Vfrom(A,i)";
    75 by (eps_ind_tac "i" 1);
    76 by (rtac (Vfrom RS ssubst) 1);
    77 by (fast_tac ZF_cs 1);
    78 val i_subset_Vfrom = result();
    79 
    80 goal Univ.thy "A <= Vfrom(A,i)";
    81 by (rtac (Vfrom RS ssubst) 1);
    82 by (rtac Un_upper1 1);
    83 val A_subset_Vfrom = result();
    84 
    85 goal Univ.thy "!!A a i. a <= Vfrom(A,i) ==> a: Vfrom(A,succ(i))";
    86 by (rtac (Vfrom RS ssubst) 1);
    87 by (fast_tac ZF_cs 1);
    88 val subset_mem_Vfrom = result();
    89 
    90 (** Finite sets and ordered pairs **)
    91 
    92 goal Univ.thy "!!a. a: Vfrom(A,i) ==> {a} : Vfrom(A,succ(i))";
    93 by (rtac subset_mem_Vfrom 1);
    94 by (safe_tac ZF_cs);
    95 val singleton_in_Vfrom = result();
    96 
    97 goal Univ.thy
    98     "!!A. [| a: Vfrom(A,i);  b: Vfrom(A,i) |] ==> {a,b} : Vfrom(A,succ(i))";
    99 by (rtac subset_mem_Vfrom 1);
   100 by (safe_tac ZF_cs);
   101 val doubleton_in_Vfrom = result();
   102 
   103 goalw Univ.thy [Pair_def]
   104     "!!A. [| a: Vfrom(A,i);  b: Vfrom(A,i) |] ==> \
   105 \         <a,b> : Vfrom(A,succ(succ(i)))";
   106 by (REPEAT (ares_tac [doubleton_in_Vfrom] 1));
   107 val Pair_in_Vfrom = result();
   108 
   109 val [prem] = goal Univ.thy
   110     "a<=Vfrom(A,i) ==> succ(a) : Vfrom(A,succ(succ(i)))";
   111 by (REPEAT (resolve_tac [subset_mem_Vfrom, succ_subsetI] 1));
   112 by (rtac (Vfrom_mono RSN (2,subset_trans)) 2);
   113 by (REPEAT (resolve_tac [prem, subset_refl, subset_succI] 1));
   114 val succ_in_Vfrom = result();
   115 
   116 (*** 0, successor and limit equations fof Vfrom ***)
   117 
   118 goal Univ.thy "Vfrom(A,0) = A";
   119 by (rtac (Vfrom RS ssubst) 1);
   120 by (fast_tac eq_cs 1);
   121 val Vfrom_0 = result();
   122 
   123 goal Univ.thy "!!i. Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
   124 by (rtac (Vfrom RS trans) 1);
   125 by (rtac (succI1 RS RepFunI RS Union_upper RSN
   126 	      (2, equalityI RS subst_context)) 1);
   127 by (rtac UN_least 1);
   128 by (rtac (subset_refl RS Vfrom_mono RS Pow_mono) 1);
   129 by (etac member_succD 1);
   130 by (assume_tac 1);
   131 val Vfrom_succ_lemma = result();
   132 
   133 goal Univ.thy "Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
   134 by (res_inst_tac [("x1", "succ(i)")] (Vfrom_rank_eq RS subst) 1);
   135 by (res_inst_tac [("x1", "i")] (Vfrom_rank_eq RS subst) 1);
   136 by (rtac (rank_succ RS ssubst) 1);
   137 by (rtac (Ord_rank RS Vfrom_succ_lemma) 1);
   138 val Vfrom_succ = result();
   139 
   140 (*The premise distinguishes this from Vfrom(A,0);  allowing X=0 forces
   141   the conclusion to be Vfrom(A,Union(X)) = A Un (UN y:X. Vfrom(A,y)) *)
   142 val [prem] = goal Univ.thy "y:X ==> Vfrom(A,Union(X)) = (UN y:X. Vfrom(A,y))";
   143 by (rtac (Vfrom RS ssubst) 1);
   144 by (rtac equalityI 1);
   145 (*first inclusion*)
   146 by (rtac Un_least 1);
   147 br (A_subset_Vfrom RS subset_trans) 1;
   148 br (prem RS UN_upper) 1;
   149 br UN_least 1;
   150 be UnionE 1;
   151 br subset_trans 1;
   152 be UN_upper 2;
   153 by (rtac (Vfrom RS ssubst) 1);
   154 be ([UN_upper, Un_upper2] MRS subset_trans) 1;
   155 (*opposite inclusion*)
   156 br UN_least 1;
   157 by (rtac (Vfrom RS ssubst) 1);
   158 by (fast_tac ZF_cs 1);
   159 val Vfrom_Union = result();
   160 
   161 (*** Limit ordinals -- general properties ***)
   162 
   163 goalw Univ.thy [Limit_def] "!!i. Limit(i) ==> Union(i) = i";
   164 by (fast_tac (eq_cs addEs [Ord_trans]) 1);
   165 val Limit_Union_eq = result();
   166 
   167 goalw Univ.thy [Limit_def] "!!i. Limit(i) ==> Ord(i)";
   168 by (etac conjunct1 1);
   169 val Limit_is_Ord = result();
   170 
   171 goalw Univ.thy [Limit_def] "!!i. Limit(i) ==> 0 : i";
   172 by (fast_tac ZF_cs 1);
   173 val Limit_has_0 = result();
   174 
   175 goalw Univ.thy [Limit_def] "!!i. [| Limit(i);  j:i |] ==> succ(j) : i";
   176 by (fast_tac ZF_cs 1);
   177 val Limit_has_succ = result();
   178 
   179 goalw Univ.thy [Limit_def] "Limit(nat)";
   180 by (REPEAT (ares_tac [conjI, ballI, nat_0I, nat_succI, Ord_nat] 1));
   181 val Limit_nat = result();
   182 
   183 goalw Univ.thy [Limit_def]
   184     "!!i. [| Ord(i);  0:i;  ALL y. ~ succ(y)=i |] ==> Limit(i)";
   185 by (safe_tac subset_cs);
   186 br Ord_member 1;
   187 by (REPEAT_FIRST (eresolve_tac [asm_rl, Ord_in_Ord RS Ord_succ]
   188           ORELSE' dresolve_tac [Ord_succ_subsetI]));
   189 by (fast_tac (subset_cs addSIs [equalityI]) 1);
   190 val non_succ_LimitI = result();
   191 
   192 goal Univ.thy "!!i. Ord(i) ==> i=0 | (EX j. i=succ(j)) | Limit(i)";
   193 by (fast_tac (ZF_cs addSIs [non_succ_LimitI, Ord_0_member_iff RS iffD2]) 1);
   194 val Ord_cases_lemma = result();
   195 
   196 val major::prems = goal Univ.thy
   197     "[| Ord(i);			\
   198 \       i=0            ==> P;	\
   199 \       !!j. i=succ(j) ==> P;	\
   200 \       Limit(i)       ==> P	\
   201 \    |] ==> P";
   202 by (cut_facts_tac [major RS Ord_cases_lemma] 1);
   203 by (REPEAT (eresolve_tac (prems@[disjE, exE]) 1));
   204 val Ord_cases = result();
   205 
   206 
   207 (*** Vfrom applied to Limit ordinals ***)
   208 
   209 (*NB. limit ordinals are non-empty;
   210                         Vfrom(A,0) = A = A Un (UN y:0. Vfrom(A,y)) *)
   211 val [limiti] = goal Univ.thy
   212     "Limit(i) ==> Vfrom(A,i) = (UN y:i. Vfrom(A,y))";
   213 by (rtac (limiti RS Limit_has_0 RS Vfrom_Union RS subst) 1);
   214 by (rtac (limiti RS Limit_Union_eq RS ssubst) 1);
   215 by (rtac refl 1);
   216 val Limit_Vfrom_eq = result();
   217 
   218 val Limit_VfromE = standard (Limit_Vfrom_eq RS equalityD1 RS subsetD RS UN_E);
   219 
   220 val [major,limiti] = goal Univ.thy
   221     "[| a: Vfrom(A,i);  Limit(i) |] ==> {a} : Vfrom(A,i)";
   222 by (rtac (limiti RS Limit_VfromE) 1);
   223 by (rtac major 1);
   224 by (rtac (limiti RS Limit_Vfrom_eq RS ssubst) 1);
   225 by (rtac UN_I 1);
   226 by (etac singleton_in_Vfrom 2);
   227 by (etac (limiti RS Limit_has_succ) 1);
   228 val singleton_in_Vfrom_limit = result();
   229 
   230 val Vfrom_UnI1 = Un_upper1 RS (subset_refl RS Vfrom_mono RS subsetD)
   231 and Vfrom_UnI2 = Un_upper2 RS (subset_refl RS Vfrom_mono RS subsetD);
   232 
   233 (*Hard work is finding a single j:i such that {a,b}<=Vfrom(A,j)*)
   234 val [aprem,bprem,limiti] = goal Univ.thy
   235     "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i) |] ==> \
   236 \    {a,b} : Vfrom(A,i)";
   237 by (rtac (aprem RS (limiti RS Limit_VfromE)) 1);
   238 by (rtac (bprem RS (limiti RS Limit_VfromE)) 1);
   239 by (rtac (limiti RS Limit_Vfrom_eq RS ssubst) 1);
   240 by (rtac UN_I 1);
   241 by (rtac doubleton_in_Vfrom 2);
   242 by (etac Vfrom_UnI1 2);
   243 by (etac Vfrom_UnI2 2);
   244 by (REPEAT (ares_tac[limiti, Limit_has_succ, Ord_member_UnI, Limit_is_Ord] 1));
   245 val doubleton_in_Vfrom_limit = result();
   246 
   247 val [aprem,bprem,limiti] = goal Univ.thy
   248     "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i) |] ==> \
   249 \    <a,b> : Vfrom(A,i)";
   250 (*Infer that a, b occur at ordinals x,xa < i.*)
   251 by (rtac (aprem RS (limiti RS Limit_VfromE)) 1);
   252 by (rtac (bprem RS (limiti RS Limit_VfromE)) 1);
   253 by (rtac (limiti RS Limit_Vfrom_eq RS ssubst) 1);
   254 by (rtac UN_I 1);
   255 by (rtac Pair_in_Vfrom 2);
   256 (*Infer that succ(succ(x Un xa)) < i *)
   257 by (etac Vfrom_UnI1 2);
   258 by (etac Vfrom_UnI2 2);
   259 by (REPEAT (ares_tac[limiti, Limit_has_succ, Ord_member_UnI, Limit_is_Ord] 1));
   260 val Pair_in_Vfrom_limit = result();
   261 
   262 
   263 (*** Properties assuming Transset(A) ***)
   264 
   265 goal Univ.thy "!!i A. Transset(A) ==> Transset(Vfrom(A,i))";
   266 by (eps_ind_tac "i" 1);
   267 by (rtac (Vfrom RS ssubst) 1);
   268 by (fast_tac (ZF_cs addSIs [Transset_Union_family, Transset_Un,
   269 			    Transset_Pow]) 1);
   270 val Transset_Vfrom = result();
   271 
   272 goal Univ.thy "!!A i. Transset(A) ==> Vfrom(A, succ(i)) = Pow(Vfrom(A,i))";
   273 by (rtac (Vfrom_succ RS trans) 1);
   274 br (Un_upper2 RSN (2,equalityI)) 1;;
   275 br (subset_refl RSN (2,Un_least)) 1;;
   276 br (A_subset_Vfrom RS subset_trans) 1;
   277 be (Transset_Vfrom RS (Transset_iff_Pow RS iffD1)) 1;
   278 val Transset_Vfrom_succ = result();
   279 
   280 goalw Ord.thy [Pair_def,Transset_def]
   281     "!!C. [| <a,b> <= C; Transset(C) |] ==> a: C & b: C";
   282 by (fast_tac ZF_cs 1);
   283 val Transset_Pair_subset = result();
   284 
   285 goal Univ.thy
   286     "!!a b.[| <a,b> <= Vfrom(A,i);  Transset(A);  Limit(i) |] ==> \
   287 \          <a,b> : Vfrom(A,i)";
   288 be (Transset_Pair_subset RS conjE) 1;
   289 be Transset_Vfrom 1;
   290 by (REPEAT (ares_tac [Pair_in_Vfrom_limit] 1));
   291 val Transset_Pair_subset_Vfrom_limit = result();
   292 
   293 
   294 (*** Closure under product/sum applied to elements -- thus Vfrom(A,i) 
   295      is a model of simple type theory provided A is a transitive set
   296      and i is a limit ordinal
   297 ***)
   298 
   299 (*There are three nearly identical proofs below -- needs a general theorem
   300   for proving  ...a...b : Vfrom(A,i) where i is a limit ordinal*)
   301 
   302 (** products **)
   303 
   304 goal Univ.thy
   305     "!!A. [| a: Vfrom(A,i);  b: Vfrom(A,i);  Transset(A) |] ==> \
   306 \         a*b : Vfrom(A, succ(succ(succ(i))))";
   307 by (dtac Transset_Vfrom 1);
   308 by (rtac subset_mem_Vfrom 1);
   309 by (rewtac Transset_def);
   310 by (fast_tac (ZF_cs addIs [Pair_in_Vfrom]) 1);
   311 val prod_in_Vfrom = result();
   312 
   313 val [aprem,bprem,limiti,transset] = goal Univ.thy
   314   "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
   315 \  a*b : Vfrom(A,i)";
   316 (*Infer that a, b occur at ordinals x,xa < i.*)
   317 by (rtac (aprem RS (limiti RS Limit_VfromE)) 1);
   318 by (rtac (bprem RS (limiti RS Limit_VfromE)) 1);
   319 by (rtac (limiti RS Limit_Vfrom_eq RS ssubst) 1);
   320 by (rtac UN_I 1);
   321 by (rtac prod_in_Vfrom 2);
   322 (*Infer that succ(succ(succ(x Un xa))) < i *)
   323 by (etac (Vfrom_UnI1 RS Vfrom_UnI2) 2);
   324 by (etac (Vfrom_UnI2 RS Vfrom_UnI2) 2);
   325 by (REPEAT (ares_tac [limiti RS Limit_has_succ,
   326 		      Ord_member_UnI, limiti RS Limit_is_Ord, transset] 1));
   327 val prod_in_Vfrom_limit = result();
   328 
   329 (** Disjoint sums, aka Quine ordered pairs **)
   330 
   331 goalw Univ.thy [sum_def]
   332     "!!A. [| a: Vfrom(A,i);  b: Vfrom(A,i);  Transset(A);  1:i |] ==> \
   333 \         a+b : Vfrom(A, succ(succ(succ(i))))";
   334 by (dtac Transset_Vfrom 1);
   335 by (rtac subset_mem_Vfrom 1);
   336 by (rewtac Transset_def);
   337 by (fast_tac (ZF_cs addIs [zero_in_Vfrom, Pair_in_Vfrom, 
   338 			   i_subset_Vfrom RS subsetD]) 1);
   339 val sum_in_Vfrom = result();
   340 
   341 val [aprem,bprem,limiti,transset] = goal Univ.thy
   342   "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
   343 \  a+b : Vfrom(A,i)";
   344 (*Infer that a, b occur at ordinals x,xa < i.*)
   345 by (rtac (aprem RS (limiti RS Limit_VfromE)) 1);
   346 by (rtac (bprem RS (limiti RS Limit_VfromE)) 1);
   347 by (rtac (limiti RS Limit_Vfrom_eq RS ssubst) 1);
   348 by (rtac UN_I 1);
   349 by (rtac (rewrite_rule [one_def] sum_in_Vfrom) 2);
   350 by (rtac (succI1 RS UnI1) 5);
   351 (*Infer that succ(succ(succ(x Un xa))) < i *)
   352 by (etac (Vfrom_UnI1 RS Vfrom_UnI2) 2);
   353 by (etac (Vfrom_UnI2 RS Vfrom_UnI2) 2);
   354 by (REPEAT (ares_tac [limiti RS Limit_has_0, 
   355 		      limiti RS Limit_has_succ,
   356 		      Ord_member_UnI, limiti RS Limit_is_Ord, transset] 1));
   357 val sum_in_Vfrom_limit = result();
   358 
   359 (** function space! **)
   360 
   361 goalw Univ.thy [Pi_def]
   362     "!!A. [| a: Vfrom(A,i);  b: Vfrom(A,i);  Transset(A) |] ==> \
   363 \         a->b : Vfrom(A, succ(succ(succ(succ(i)))))";
   364 by (dtac Transset_Vfrom 1);
   365 by (rtac subset_mem_Vfrom 1);
   366 by (rtac (Collect_subset RS subset_trans) 1);
   367 by (rtac (Vfrom RS ssubst) 1);
   368 by (rtac (subset_trans RS subset_trans) 1);
   369 by (rtac Un_upper2 3);
   370 by (rtac (succI1 RS UN_upper) 2);
   371 by (rtac Pow_mono 1);
   372 by (rewtac Transset_def);
   373 by (fast_tac (ZF_cs addIs [Pair_in_Vfrom]) 1);
   374 val fun_in_Vfrom = result();
   375 
   376 val [aprem,bprem,limiti,transset] = goal Univ.thy
   377   "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
   378 \  a->b : Vfrom(A,i)";
   379 (*Infer that a, b occur at ordinals x,xa < i.*)
   380 by (rtac (aprem RS (limiti RS Limit_VfromE)) 1);
   381 by (rtac (bprem RS (limiti RS Limit_VfromE)) 1);
   382 by (rtac (limiti RS Limit_Vfrom_eq RS ssubst) 1);
   383 by (rtac UN_I 1);
   384 by (rtac fun_in_Vfrom 2);
   385 (*Infer that succ(succ(succ(x Un xa))) < i *)
   386 by (etac (Vfrom_UnI1 RS Vfrom_UnI2) 2);
   387 by (etac (Vfrom_UnI2 RS Vfrom_UnI2) 2);
   388 by (REPEAT (ares_tac [limiti RS Limit_has_succ,
   389 		      Ord_member_UnI, limiti RS Limit_is_Ord, transset] 1));
   390 val fun_in_Vfrom_limit = result();
   391 
   392 
   393 (*** The set Vset(i) ***)
   394 
   395 goal Univ.thy "Vset(i) = (UN j:i. Pow(Vset(j)))";
   396 by (rtac (Vfrom RS ssubst) 1);
   397 by (fast_tac eq_cs 1);
   398 val Vset = result();
   399 
   400 val Vset_succ = Transset_0 RS Transset_Vfrom_succ;
   401 
   402 val Transset_Vset = Transset_0 RS Transset_Vfrom;
   403 
   404 (** Characterisation of the elements of Vset(i) **)
   405 
   406 val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. b : Vset(i) --> rank(b) : i";
   407 by (rtac (ordi RS trans_induct) 1);
   408 by (rtac (Vset RS ssubst) 1);
   409 by (safe_tac ZF_cs);
   410 by (rtac (rank RS ssubst) 1);
   411 by (rtac sup_least2 1);
   412 by (assume_tac 1);
   413 by (assume_tac 1);
   414 by (fast_tac ZF_cs 1);
   415 val Vset_rank_imp1 = result();
   416 
   417 (*  [| Ord(i); x : Vset(i) |] ==> rank(x) : i  *)
   418 val Vset_D = standard (Vset_rank_imp1 RS spec RS mp);
   419 
   420 val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. rank(b) : i --> b : Vset(i)";
   421 by (rtac (ordi RS trans_induct) 1);
   422 by (rtac allI 1);
   423 by (rtac (Vset RS ssubst) 1);
   424 by (fast_tac (ZF_cs addSIs [rank_lt]) 1);
   425 val Vset_rank_imp2 = result();
   426 
   427 (*  [| Ord(i); rank(x) : i |] ==> x : Vset(i)  *)
   428 val VsetI = standard (Vset_rank_imp2 RS spec RS mp);
   429 
   430 val [ordi] = goal Univ.thy "Ord(i) ==> b : Vset(i) <-> rank(b) : i";
   431 by (rtac iffI 1);
   432 by (etac (ordi RS Vset_D) 1);
   433 by (etac (ordi RS VsetI) 1);
   434 val Vset_Ord_rank_iff = result();
   435 
   436 goal Univ.thy "b : Vset(a) <-> rank(b) : rank(a)";
   437 by (rtac (Vfrom_rank_eq RS subst) 1);
   438 by (rtac (Ord_rank RS Vset_Ord_rank_iff) 1);
   439 val Vset_rank_iff = result();
   440 
   441 goal Univ.thy "!!i. Ord(i) ==> rank(Vset(i)) = i";
   442 by (rtac (rank RS ssubst) 1);
   443 by (rtac equalityI 1);
   444 by (safe_tac ZF_cs);
   445 by (EVERY' [wtac UN_I, 
   446 	    etac (i_subset_Vfrom RS subsetD),
   447 	    etac (Ord_in_Ord RS rank_of_Ord RS ssubst),
   448 	    assume_tac,
   449 	    rtac succI1] 3);
   450 by (REPEAT (eresolve_tac [asm_rl,Vset_D,Ord_trans] 1));
   451 val rank_Vset = result();
   452 
   453 (** Lemmas for reasoning about sets in terms of their elements' ranks **)
   454 
   455 (*  rank(x) : rank(a) ==> x : Vset(rank(a))  *)
   456 val Vset_rankI = Ord_rank RS VsetI;
   457 
   458 goal Univ.thy "a <= Vset(rank(a))";
   459 br subsetI 1;
   460 be (rank_lt RS Vset_rankI) 1;
   461 val arg_subset_Vset_rank = result();
   462 
   463 val [iprem] = goal Univ.thy
   464     "[| !!i. Ord(i) ==> a Int Vset(i) <= b |] ==> a <= b";
   465 br ([subset_refl, arg_subset_Vset_rank] MRS Int_greatest RS subset_trans) 1;
   466 br (Ord_rank RS iprem) 1;
   467 val Int_Vset_subset = result();
   468 
   469 (** Set up an environment for simplification **)
   470 
   471 val rank_rls = [rank_Inl, rank_Inr, rank_pair1, rank_pair2];
   472 val rank_trans_rls = rank_rls @ (rank_rls RLN (2, [rank_trans]));
   473 
   474 val rank_ss = ZF_ss 
   475     addsimps [case_Inl, case_Inr, Vset_rankI]
   476     addsimps rank_trans_rls;
   477 
   478 (** Recursion over Vset levels! **)
   479 
   480 (*NOT SUITABLE FOR REWRITING: recursive!*)
   481 goalw Univ.thy [Vrec_def] "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))";
   482 by (rtac (transrec RS ssubst) 1);
   483 by (simp_tac (ZF_ss addsimps [Ord_rank, Ord_succ, Vset_D RS beta, 
   484 			      VsetI RS beta]) 1);
   485 val Vrec = result();
   486 
   487 (*This form avoids giant explosions in proofs.  NOTE USE OF == *)
   488 val rew::prems = goal Univ.thy
   489     "[| !!x. h(x)==Vrec(x,H) |] ==> \
   490 \    h(a) = H(a, lam x: Vset(rank(a)). h(x))";
   491 by (rewtac rew);
   492 by (rtac Vrec 1);
   493 val def_Vrec = result();
   494 
   495 
   496 (*** univ(A) ***)
   497 
   498 goalw Univ.thy [univ_def] "!!A B. A<=B ==> univ(A) <= univ(B)";
   499 by (etac Vfrom_mono 1);
   500 by (rtac subset_refl 1);
   501 val univ_mono = result();
   502 
   503 goalw Univ.thy [univ_def] "!!A. Transset(A) ==> Transset(univ(A))";
   504 by (etac Transset_Vfrom 1);
   505 val Transset_univ = result();
   506 
   507 (** univ(A) as a limit **)
   508 
   509 goalw Univ.thy [univ_def] "univ(A) = (UN i:nat. Vfrom(A,i))";
   510 br (Limit_nat RS Limit_Vfrom_eq) 1;
   511 val univ_eq_UN = result();
   512 
   513 goal Univ.thy "!!c. c <= univ(A) ==> c = (UN i:nat. c Int Vfrom(A,i))";
   514 br (subset_UN_iff_eq RS iffD1) 1;
   515 be (univ_eq_UN RS subst) 1;
   516 val subset_univ_eq_Int = result();
   517 
   518 val [aprem, iprem] = goal Univ.thy
   519     "[| a <= univ(X);			 	\
   520 \       !!i. i:nat ==> a Int Vfrom(X,i) <= b 	\
   521 \    |] ==> a <= b";
   522 br (aprem RS subset_univ_eq_Int RS ssubst) 1;
   523 br UN_least 1;
   524 be iprem 1;
   525 val univ_Int_Vfrom_subset = result();
   526 
   527 val prems = goal Univ.thy
   528     "[| a <= univ(X);   b <= univ(X);   \
   529 \       !!i. i:nat ==> a Int Vfrom(X,i) = b Int Vfrom(X,i) \
   530 \    |] ==> a = b";
   531 br equalityI 1;
   532 by (ALLGOALS
   533     (resolve_tac (prems RL [univ_Int_Vfrom_subset]) THEN'
   534      eresolve_tac (prems RL [equalityD1,equalityD2] RL [subset_trans]) THEN'
   535      rtac Int_lower1));
   536 val univ_Int_Vfrom_eq = result();
   537 
   538 (** Closure properties **)
   539 
   540 goalw Univ.thy [univ_def] "0 : univ(A)";
   541 by (rtac (nat_0I RS zero_in_Vfrom) 1);
   542 val zero_in_univ = result();
   543 
   544 goalw Univ.thy [univ_def] "A <= univ(A)";
   545 by (rtac A_subset_Vfrom 1);
   546 val A_subset_univ = result();
   547 
   548 val A_into_univ = A_subset_univ RS subsetD;
   549 
   550 (** Closure under unordered and ordered pairs **)
   551 
   552 goalw Univ.thy [univ_def] "!!A a. a: univ(A) ==> {a} : univ(A)";
   553 by (rtac singleton_in_Vfrom_limit 1);
   554 by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1));
   555 val singleton_in_univ = result();
   556 
   557 goalw Univ.thy [univ_def] 
   558     "!!A a. [| a: univ(A);  b: univ(A) |] ==> {a,b} : univ(A)";
   559 by (rtac doubleton_in_Vfrom_limit 1);
   560 by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1));
   561 val doubleton_in_univ = result();
   562 
   563 goalw Univ.thy [univ_def]
   564     "!!A a. [| a: univ(A);  b: univ(A) |] ==> <a,b> : univ(A)";
   565 by (rtac Pair_in_Vfrom_limit 1);
   566 by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1));
   567 val Pair_in_univ = result();
   568 
   569 goal Univ.thy "univ(A)*univ(A) <= univ(A)";
   570 by (REPEAT (ares_tac [subsetI,Pair_in_univ] 1
   571      ORELSE eresolve_tac [SigmaE, ssubst] 1));
   572 val product_univ = result();
   573 
   574 val Sigma_subset_univ = standard
   575     (Sigma_mono RS (product_univ RSN (2,subset_trans)));
   576 
   577 goalw Univ.thy [univ_def]
   578     "!!a b.[| <a,b> <= univ(A);  Transset(A) |] ==> <a,b> : univ(A)";
   579 be Transset_Pair_subset_Vfrom_limit 1;
   580 by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1));
   581 val Transset_Pair_subset_univ = result();
   582 
   583 
   584 (** The natural numbers **)
   585 
   586 goalw Univ.thy [univ_def] "nat <= univ(A)";
   587 by (rtac i_subset_Vfrom 1);
   588 val nat_subset_univ = result();
   589 
   590 (* n:nat ==> n:univ(A) *)
   591 val nat_into_univ = standard (nat_subset_univ RS subsetD);
   592 
   593 (** instances for 1 and 2 **)
   594 
   595 goalw Univ.thy [one_def] "1 : univ(A)";
   596 by (REPEAT (ares_tac [nat_into_univ, nat_0I, nat_succI] 1));
   597 val one_in_univ = result();
   598 
   599 (*unused!*)
   600 goal Univ.thy "succ(succ(0)) : univ(A)";
   601 by (REPEAT (ares_tac [nat_into_univ, nat_0I, nat_succI] 1));
   602 val two_in_univ = result();
   603 
   604 goalw Univ.thy [bool_def] "bool <= univ(A)";
   605 by (fast_tac (ZF_cs addSIs [zero_in_univ,one_in_univ]) 1);
   606 val bool_subset_univ = result();
   607 
   608 val bool_into_univ = standard (bool_subset_univ RS subsetD);
   609 
   610 
   611 (** Closure under disjoint union **)
   612 
   613 goalw Univ.thy [Inl_def] "!!A a. a: univ(A) ==> Inl(a) : univ(A)";
   614 by (REPEAT (ares_tac [zero_in_univ,Pair_in_univ] 1));
   615 val Inl_in_univ = result();
   616 
   617 goalw Univ.thy [Inr_def] "!!A b. b: univ(A) ==> Inr(b) : univ(A)";
   618 by (REPEAT (ares_tac [one_in_univ, Pair_in_univ] 1));
   619 val Inr_in_univ = result();
   620 
   621 goal Univ.thy "univ(C)+univ(C) <= univ(C)";
   622 by (REPEAT (ares_tac [subsetI,Inl_in_univ,Inr_in_univ] 1
   623      ORELSE eresolve_tac [sumE, ssubst] 1));
   624 val sum_univ = result();
   625 
   626 val sum_subset_univ = standard
   627     (sum_mono RS (sum_univ RSN (2,subset_trans)));
   628 
   629 
   630 (** Closure under binary union -- use Un_least **)
   631 (** Closure under Collect -- use  (Collect_subset RS subset_trans)  **)
   632 (** Closure under RepFun -- use   RepFun_subset  **)
   633 
   634