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