src/ZF/Univ.ML
changeset 0 a5a9c433f639
child 6 8ce8c4d13d4d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/Univ.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,642 @@
     1.4 +(*  Title: 	ZF/univ
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1992  University of Cambridge
     1.8 +
     1.9 +The cumulative hierarchy and a small universe for recursive types
    1.10 +*)
    1.11 +
    1.12 +open Univ;
    1.13 +
    1.14 +(*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
    1.15 +goal Univ.thy "Vfrom(A,i) = A Un (UN j:i. Pow(Vfrom(A,j)))";
    1.16 +by (rtac (Vfrom_def RS def_transrec RS ssubst) 1);
    1.17 +by (SIMP_TAC ZF_ss 1);
    1.18 +val Vfrom = result();
    1.19 +
    1.20 +(** Monotonicity **)
    1.21 +
    1.22 +goal Univ.thy "!!A B. A<=B ==> ALL j. i<=j --> Vfrom(A,i) <= Vfrom(B,j)";
    1.23 +by (eps_ind_tac "i" 1);
    1.24 +by (rtac (impI RS allI) 1);
    1.25 +by (rtac (Vfrom RS ssubst) 1);
    1.26 +by (rtac (Vfrom RS ssubst) 1);
    1.27 +by (etac Un_mono 1);
    1.28 +by (rtac UN_mono 1);
    1.29 +by (assume_tac 1);
    1.30 +by (rtac Pow_mono 1);
    1.31 +by (etac (bspec RS spec RS mp) 1);
    1.32 +by (assume_tac 1);
    1.33 +by (rtac subset_refl 1);
    1.34 +val Vfrom_mono_lemma = result();
    1.35 +
    1.36 +(*  [| A<=B; i<=x |] ==> Vfrom(A,i) <= Vfrom(B,x)  *)
    1.37 +val Vfrom_mono = standard (Vfrom_mono_lemma RS spec RS mp);
    1.38 +
    1.39 +
    1.40 +(** A fundamental equality: Vfrom does not require ordinals! **)
    1.41 +
    1.42 +goal Univ.thy "Vfrom(A,x) <= Vfrom(A,rank(x))";
    1.43 +by (eps_ind_tac "x" 1);
    1.44 +by (rtac (Vfrom RS ssubst) 1);
    1.45 +by (rtac (Vfrom RS ssubst) 1);
    1.46 +by (fast_tac (ZF_cs addSIs [rank_lt]) 1);
    1.47 +val Vfrom_rank_subset1 = result();
    1.48 +
    1.49 +goal Univ.thy "Vfrom(A,rank(x)) <= Vfrom(A,x)";
    1.50 +by (eps_ind_tac "x" 1);
    1.51 +by (rtac (Vfrom RS ssubst) 1);
    1.52 +by (rtac (Vfrom RS ssubst) 1);
    1.53 +br (subset_refl RS Un_mono) 1;
    1.54 +br UN_least 1;
    1.55 +by (etac (rank_implies_mem RS bexE) 1);
    1.56 +br subset_trans 1;
    1.57 +be UN_upper 2;
    1.58 +by (etac (subset_refl RS Vfrom_mono RS subset_trans RS Pow_mono) 1);
    1.59 +by (etac bspec 1);
    1.60 +by (assume_tac 1);
    1.61 +val Vfrom_rank_subset2 = result();
    1.62 +
    1.63 +goal Univ.thy "Vfrom(A,rank(x)) = Vfrom(A,x)";
    1.64 +by (rtac equalityI 1);
    1.65 +by (rtac Vfrom_rank_subset2 1);
    1.66 +by (rtac Vfrom_rank_subset1 1);
    1.67 +val Vfrom_rank_eq = result();
    1.68 +
    1.69 +
    1.70 +(*** Basic closure properties ***)
    1.71 +
    1.72 +goal Univ.thy "!!x y. y:x ==> 0 : Vfrom(A,x)";
    1.73 +by (rtac (Vfrom RS ssubst) 1);
    1.74 +by (fast_tac ZF_cs 1);
    1.75 +val zero_in_Vfrom = result();
    1.76 +
    1.77 +goal Univ.thy "i <= Vfrom(A,i)";
    1.78 +by (eps_ind_tac "i" 1);
    1.79 +by (rtac (Vfrom RS ssubst) 1);
    1.80 +by (fast_tac ZF_cs 1);
    1.81 +val i_subset_Vfrom = result();
    1.82 +
    1.83 +goal Univ.thy "A <= Vfrom(A,i)";
    1.84 +by (rtac (Vfrom RS ssubst) 1);
    1.85 +by (rtac Un_upper1 1);
    1.86 +val A_subset_Vfrom = result();
    1.87 +
    1.88 +goal Univ.thy "!!A a i. a <= Vfrom(A,i) ==> a: Vfrom(A,succ(i))";
    1.89 +by (rtac (Vfrom RS ssubst) 1);
    1.90 +by (fast_tac ZF_cs 1);
    1.91 +val subset_mem_Vfrom = result();
    1.92 +
    1.93 +(** Finite sets and ordered pairs **)
    1.94 +
    1.95 +goal Univ.thy "!!a. a: Vfrom(A,i) ==> {a} : Vfrom(A,succ(i))";
    1.96 +by (rtac subset_mem_Vfrom 1);
    1.97 +by (safe_tac ZF_cs);
    1.98 +val singleton_in_Vfrom = result();
    1.99 +
   1.100 +goal Univ.thy
   1.101 +    "!!A. [| a: Vfrom(A,i);  b: Vfrom(A,i) |] ==> {a,b} : Vfrom(A,succ(i))";
   1.102 +by (rtac subset_mem_Vfrom 1);
   1.103 +by (safe_tac ZF_cs);
   1.104 +val doubleton_in_Vfrom = result();
   1.105 +
   1.106 +goalw Univ.thy [Pair_def]
   1.107 +    "!!A. [| a: Vfrom(A,i);  b: Vfrom(A,i) |] ==> \
   1.108 +\         <a,b> : Vfrom(A,succ(succ(i)))";
   1.109 +by (REPEAT (ares_tac [doubleton_in_Vfrom] 1));
   1.110 +val Pair_in_Vfrom = result();
   1.111 +
   1.112 +val [prem] = goal Univ.thy
   1.113 +    "a<=Vfrom(A,i) ==> succ(a) : Vfrom(A,succ(succ(i)))";
   1.114 +by (REPEAT (resolve_tac [subset_mem_Vfrom, succ_subsetI] 1));
   1.115 +by (rtac (Vfrom_mono RSN (2,subset_trans)) 2);
   1.116 +by (REPEAT (resolve_tac [prem, subset_refl, subset_succI] 1));
   1.117 +val succ_in_Vfrom = result();
   1.118 +
   1.119 +(*** 0, successor and limit equations fof Vfrom ***)
   1.120 +
   1.121 +goal Univ.thy "Vfrom(A,0) = A";
   1.122 +by (rtac (Vfrom RS ssubst) 1);
   1.123 +by (fast_tac eq_cs 1);
   1.124 +val Vfrom_0 = result();
   1.125 +
   1.126 +goal Univ.thy "!!i. Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
   1.127 +by (rtac (Vfrom RS trans) 1);
   1.128 +brs ([refl] RL ZF_congs) 1;
   1.129 +by (rtac equalityI 1);
   1.130 +by (rtac (succI1 RS RepFunI RS Union_upper) 2);
   1.131 +by (rtac UN_least 1);
   1.132 +by (rtac (subset_refl RS Vfrom_mono RS Pow_mono) 1);
   1.133 +by (etac member_succD 1);
   1.134 +by (assume_tac 1);
   1.135 +val Vfrom_succ_lemma = result();
   1.136 +
   1.137 +goal Univ.thy "Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
   1.138 +by (res_inst_tac [("x1", "succ(i)")] (Vfrom_rank_eq RS subst) 1);
   1.139 +by (res_inst_tac [("x1", "i")] (Vfrom_rank_eq RS subst) 1);
   1.140 +by (rtac (rank_succ RS ssubst) 1);
   1.141 +by (rtac (Ord_rank RS Vfrom_succ_lemma) 1);
   1.142 +val Vfrom_succ = result();
   1.143 +
   1.144 +(*The premise distinguishes this from Vfrom(A,0);  allowing X=0 forces
   1.145 +  the conclusion to be Vfrom(A,Union(X)) = A Un (UN y:X. Vfrom(A,y)) *)
   1.146 +val [prem] = goal Univ.thy "y:X ==> Vfrom(A,Union(X)) = (UN y:X. Vfrom(A,y))";
   1.147 +by (rtac (Vfrom RS ssubst) 1);
   1.148 +by (rtac equalityI 1);
   1.149 +(*first inclusion*)
   1.150 +by (rtac Un_least 1);
   1.151 +br (A_subset_Vfrom RS subset_trans) 1;
   1.152 +br (prem RS UN_upper) 1;
   1.153 +br UN_least 1;
   1.154 +be UnionE 1;
   1.155 +br subset_trans 1;
   1.156 +be UN_upper 2;
   1.157 +by (rtac (Vfrom RS ssubst) 1);
   1.158 +be ([UN_upper, Un_upper2] MRS subset_trans) 1;
   1.159 +(*opposite inclusion*)
   1.160 +br UN_least 1;
   1.161 +by (rtac (Vfrom RS ssubst) 1);
   1.162 +by (fast_tac ZF_cs 1);
   1.163 +val Vfrom_Union = result();
   1.164 +
   1.165 +(*** Limit ordinals -- general properties ***)
   1.166 +
   1.167 +goalw Univ.thy [Limit_def] "!!i. Limit(i) ==> Union(i) = i";
   1.168 +by (fast_tac (eq_cs addEs [Ord_trans]) 1);
   1.169 +val Limit_Union_eq = result();
   1.170 +
   1.171 +goalw Univ.thy [Limit_def] "!!i. Limit(i) ==> Ord(i)";
   1.172 +by (etac conjunct1 1);
   1.173 +val Limit_is_Ord = result();
   1.174 +
   1.175 +goalw Univ.thy [Limit_def] "!!i. Limit(i) ==> 0 : i";
   1.176 +by (fast_tac ZF_cs 1);
   1.177 +val Limit_has_0 = result();
   1.178 +
   1.179 +goalw Univ.thy [Limit_def] "!!i. [| Limit(i);  j:i |] ==> succ(j) : i";
   1.180 +by (fast_tac ZF_cs 1);
   1.181 +val Limit_has_succ = result();
   1.182 +
   1.183 +goalw Univ.thy [Limit_def] "Limit(nat)";
   1.184 +by (REPEAT (ares_tac [conjI, ballI, nat_0I, nat_succI, Ord_nat] 1));
   1.185 +val Limit_nat = result();
   1.186 +
   1.187 +goalw Univ.thy [Limit_def]
   1.188 +    "!!i. [| Ord(i);  0:i;  ALL y. ~ succ(y)=i |] ==> Limit(i)";
   1.189 +by (safe_tac subset_cs);
   1.190 +br Ord_member 1;
   1.191 +by (REPEAT_FIRST (eresolve_tac [asm_rl, Ord_in_Ord RS Ord_succ]
   1.192 +          ORELSE' dresolve_tac [Ord_succ_subsetI]));
   1.193 +by (fast_tac (subset_cs addSIs [equalityI]) 1);
   1.194 +val non_succ_LimitI = result();
   1.195 +
   1.196 +goal Univ.thy "!!i. Ord(i) ==> i=0 | (EX j. i=succ(j)) | Limit(i)";
   1.197 +by (fast_tac (ZF_cs addSIs [non_succ_LimitI, Ord_0_member_iff RS iffD2]) 1);
   1.198 +val Ord_cases_lemma = result();
   1.199 +
   1.200 +val major::prems = goal Univ.thy
   1.201 +    "[| Ord(i);			\
   1.202 +\       i=0            ==> P;	\
   1.203 +\       !!j. i=succ(j) ==> P;	\
   1.204 +\       Limit(i)       ==> P	\
   1.205 +\    |] ==> P";
   1.206 +by (cut_facts_tac [major RS Ord_cases_lemma] 1);
   1.207 +by (REPEAT (eresolve_tac (prems@[disjE, exE]) 1));
   1.208 +val Ord_cases = result();
   1.209 +
   1.210 +
   1.211 +(*** Vfrom applied to Limit ordinals ***)
   1.212 +
   1.213 +(*NB. limit ordinals are non-empty;
   1.214 +                        Vfrom(A,0) = A = A Un (UN y:0. Vfrom(A,y)) *)
   1.215 +val [limiti] = goal Univ.thy
   1.216 +    "Limit(i) ==> Vfrom(A,i) = (UN y:i. Vfrom(A,y))";
   1.217 +by (rtac (limiti RS Limit_has_0 RS Vfrom_Union RS subst) 1);
   1.218 +by (rtac (limiti RS Limit_Union_eq RS ssubst) 1);
   1.219 +by (rtac refl 1);
   1.220 +val Limit_Vfrom_eq = result();
   1.221 +
   1.222 +val Limit_VfromE = standard (Limit_Vfrom_eq RS equalityD1 RS subsetD RS UN_E);
   1.223 +
   1.224 +val [major,limiti] = goal Univ.thy
   1.225 +    "[| a: Vfrom(A,i);  Limit(i) |] ==> {a} : Vfrom(A,i)";
   1.226 +by (rtac (limiti RS Limit_VfromE) 1);
   1.227 +by (rtac major 1);
   1.228 +by (rtac (limiti RS Limit_Vfrom_eq RS ssubst) 1);
   1.229 +by (rtac UN_I 1);
   1.230 +by (etac singleton_in_Vfrom 2);
   1.231 +by (etac (limiti RS Limit_has_succ) 1);
   1.232 +val singleton_in_Vfrom_limit = result();
   1.233 +
   1.234 +val Vfrom_UnI1 = Un_upper1 RS (subset_refl RS Vfrom_mono RS subsetD)
   1.235 +and Vfrom_UnI2 = Un_upper2 RS (subset_refl RS Vfrom_mono RS subsetD);
   1.236 +
   1.237 +(*Hard work is finding a single j:i such that {a,b}<=Vfrom(A,j)*)
   1.238 +val [aprem,bprem,limiti] = goal Univ.thy
   1.239 +    "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i) |] ==> \
   1.240 +\    {a,b} : Vfrom(A,i)";
   1.241 +by (rtac (aprem RS (limiti RS Limit_VfromE)) 1);
   1.242 +by (rtac (bprem RS (limiti RS Limit_VfromE)) 1);
   1.243 +by (rtac (limiti RS Limit_Vfrom_eq RS ssubst) 1);
   1.244 +by (rtac UN_I 1);
   1.245 +by (rtac doubleton_in_Vfrom 2);
   1.246 +by (etac Vfrom_UnI1 2);
   1.247 +by (etac Vfrom_UnI2 2);
   1.248 +by (REPEAT (ares_tac[limiti, Limit_has_succ, Ord_member_UnI, Limit_is_Ord] 1));
   1.249 +val doubleton_in_Vfrom_limit = result();
   1.250 +
   1.251 +val [aprem,bprem,limiti] = goal Univ.thy
   1.252 +    "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i) |] ==> \
   1.253 +\    <a,b> : Vfrom(A,i)";
   1.254 +(*Infer that a, b occur at ordinals x,xa < i.*)
   1.255 +by (rtac (aprem RS (limiti RS Limit_VfromE)) 1);
   1.256 +by (rtac (bprem RS (limiti RS Limit_VfromE)) 1);
   1.257 +by (rtac (limiti RS Limit_Vfrom_eq RS ssubst) 1);
   1.258 +by (rtac UN_I 1);
   1.259 +by (rtac Pair_in_Vfrom 2);
   1.260 +(*Infer that succ(succ(x Un xa)) < i *)
   1.261 +by (etac Vfrom_UnI1 2);
   1.262 +by (etac Vfrom_UnI2 2);
   1.263 +by (REPEAT (ares_tac[limiti, Limit_has_succ, Ord_member_UnI, Limit_is_Ord] 1));
   1.264 +val Pair_in_Vfrom_limit = result();
   1.265 +
   1.266 +
   1.267 +(*** Properties assuming Transset(A) ***)
   1.268 +
   1.269 +goal Univ.thy "!!i A. Transset(A) ==> Transset(Vfrom(A,i))";
   1.270 +by (eps_ind_tac "i" 1);
   1.271 +by (rtac (Vfrom RS ssubst) 1);
   1.272 +by (fast_tac (ZF_cs addSIs [Transset_Union_family, Transset_Un,
   1.273 +			    Transset_Pow]) 1);
   1.274 +val Transset_Vfrom = result();
   1.275 +
   1.276 +goal Univ.thy "!!A i. Transset(A) ==> Vfrom(A, succ(i)) = Pow(Vfrom(A,i))";
   1.277 +by (rtac (Vfrom_succ RS trans) 1);
   1.278 +br (Un_upper2 RSN (2,equalityI)) 1;;
   1.279 +br (subset_refl RSN (2,Un_least)) 1;;
   1.280 +br (A_subset_Vfrom RS subset_trans) 1;
   1.281 +be (Transset_Vfrom RS (Transset_iff_Pow RS iffD1)) 1;
   1.282 +val Transset_Vfrom_succ = result();
   1.283 +
   1.284 +goalw Ord.thy [Pair_def,Transset_def]
   1.285 +    "!!C. [| <a,b> <= C; Transset(C) |] ==> a: C & b: C";
   1.286 +by (fast_tac ZF_cs 1);
   1.287 +val Transset_Pair_subset = result();
   1.288 +
   1.289 +goal Univ.thy
   1.290 +    "!!a b.[| <a,b> <= Vfrom(A,i);  Transset(A);  Limit(i) |] ==> \
   1.291 +\          <a,b> : Vfrom(A,i)";
   1.292 +be (Transset_Pair_subset RS conjE) 1;
   1.293 +be Transset_Vfrom 1;
   1.294 +by (REPEAT (ares_tac [Pair_in_Vfrom_limit] 1));
   1.295 +val Transset_Pair_subset_Vfrom_limit = result();
   1.296 +
   1.297 +
   1.298 +(*** Closure under product/sum applied to elements -- thus Vfrom(A,i) 
   1.299 +     is a model of simple type theory provided A is a transitive set
   1.300 +     and i is a limit ordinal
   1.301 +***)
   1.302 +
   1.303 +(*There are three nearly identical proofs below -- needs a general theorem
   1.304 +  for proving  ...a...b : Vfrom(A,i) where i is a limit ordinal*)
   1.305 +
   1.306 +(** products **)
   1.307 +
   1.308 +goal Univ.thy
   1.309 +    "!!A. [| a: Vfrom(A,i);  b: Vfrom(A,i);  Transset(A) |] ==> \
   1.310 +\         a*b : Vfrom(A, succ(succ(succ(i))))";
   1.311 +by (dtac Transset_Vfrom 1);
   1.312 +by (rtac subset_mem_Vfrom 1);
   1.313 +by (rewtac Transset_def);
   1.314 +by (fast_tac (ZF_cs addIs [Pair_in_Vfrom]) 1);
   1.315 +val prod_in_Vfrom = result();
   1.316 +
   1.317 +val [aprem,bprem,limiti,transset] = goal Univ.thy
   1.318 +  "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
   1.319 +\  a*b : Vfrom(A,i)";
   1.320 +(*Infer that a, b occur at ordinals x,xa < i.*)
   1.321 +by (rtac (aprem RS (limiti RS Limit_VfromE)) 1);
   1.322 +by (rtac (bprem RS (limiti RS Limit_VfromE)) 1);
   1.323 +by (rtac (limiti RS Limit_Vfrom_eq RS ssubst) 1);
   1.324 +by (rtac UN_I 1);
   1.325 +by (rtac prod_in_Vfrom 2);
   1.326 +(*Infer that succ(succ(succ(x Un xa))) < i *)
   1.327 +by (etac (Vfrom_UnI1 RS Vfrom_UnI2) 2);
   1.328 +by (etac (Vfrom_UnI2 RS Vfrom_UnI2) 2);
   1.329 +by (REPEAT (ares_tac [limiti RS Limit_has_succ,
   1.330 +		      Ord_member_UnI, limiti RS Limit_is_Ord, transset] 1));
   1.331 +val prod_in_Vfrom_limit = result();
   1.332 +
   1.333 +(** Disjoint sums, aka Quine ordered pairs **)
   1.334 +
   1.335 +goalw Univ.thy [sum_def]
   1.336 +    "!!A. [| a: Vfrom(A,i);  b: Vfrom(A,i);  Transset(A);  1:i |] ==> \
   1.337 +\         a+b : Vfrom(A, succ(succ(succ(i))))";
   1.338 +by (dtac Transset_Vfrom 1);
   1.339 +by (rtac subset_mem_Vfrom 1);
   1.340 +by (rewtac Transset_def);
   1.341 +by (fast_tac (ZF_cs addIs [zero_in_Vfrom, Pair_in_Vfrom, 
   1.342 +			   i_subset_Vfrom RS subsetD]) 1);
   1.343 +val sum_in_Vfrom = result();
   1.344 +
   1.345 +val [aprem,bprem,limiti,transset] = goal Univ.thy
   1.346 +  "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
   1.347 +\  a+b : Vfrom(A,i)";
   1.348 +(*Infer that a, b occur at ordinals x,xa < i.*)
   1.349 +by (rtac (aprem RS (limiti RS Limit_VfromE)) 1);
   1.350 +by (rtac (bprem RS (limiti RS Limit_VfromE)) 1);
   1.351 +by (rtac (limiti RS Limit_Vfrom_eq RS ssubst) 1);
   1.352 +by (rtac UN_I 1);
   1.353 +by (rtac (rewrite_rule [one_def] sum_in_Vfrom) 2);
   1.354 +by (rtac (succI1 RS UnI1) 5);
   1.355 +(*Infer that succ(succ(succ(x Un xa))) < i *)
   1.356 +by (etac (Vfrom_UnI1 RS Vfrom_UnI2) 2);
   1.357 +by (etac (Vfrom_UnI2 RS Vfrom_UnI2) 2);
   1.358 +by (REPEAT (ares_tac [limiti RS Limit_has_0, 
   1.359 +		      limiti RS Limit_has_succ,
   1.360 +		      Ord_member_UnI, limiti RS Limit_is_Ord, transset] 1));
   1.361 +val sum_in_Vfrom_limit = result();
   1.362 +
   1.363 +(** function space! **)
   1.364 +
   1.365 +goalw Univ.thy [Pi_def]
   1.366 +    "!!A. [| a: Vfrom(A,i);  b: Vfrom(A,i);  Transset(A) |] ==> \
   1.367 +\         a->b : Vfrom(A, succ(succ(succ(succ(i)))))";
   1.368 +by (dtac Transset_Vfrom 1);
   1.369 +by (rtac subset_mem_Vfrom 1);
   1.370 +by (rtac (Collect_subset RS subset_trans) 1);
   1.371 +by (rtac (Vfrom RS ssubst) 1);
   1.372 +by (rtac (subset_trans RS subset_trans) 1);
   1.373 +by (rtac Un_upper2 3);
   1.374 +by (rtac (succI1 RS UN_upper) 2);
   1.375 +by (rtac Pow_mono 1);
   1.376 +by (rewtac Transset_def);
   1.377 +by (fast_tac (ZF_cs addIs [Pair_in_Vfrom]) 1);
   1.378 +val fun_in_Vfrom = result();
   1.379 +
   1.380 +val [aprem,bprem,limiti,transset] = goal Univ.thy
   1.381 +  "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
   1.382 +\  a->b : Vfrom(A,i)";
   1.383 +(*Infer that a, b occur at ordinals x,xa < i.*)
   1.384 +by (rtac (aprem RS (limiti RS Limit_VfromE)) 1);
   1.385 +by (rtac (bprem RS (limiti RS Limit_VfromE)) 1);
   1.386 +by (rtac (limiti RS Limit_Vfrom_eq RS ssubst) 1);
   1.387 +by (rtac UN_I 1);
   1.388 +by (rtac fun_in_Vfrom 2);
   1.389 +(*Infer that succ(succ(succ(x Un xa))) < i *)
   1.390 +by (etac (Vfrom_UnI1 RS Vfrom_UnI2) 2);
   1.391 +by (etac (Vfrom_UnI2 RS Vfrom_UnI2) 2);
   1.392 +by (REPEAT (ares_tac [limiti RS Limit_has_succ,
   1.393 +		      Ord_member_UnI, limiti RS Limit_is_Ord, transset] 1));
   1.394 +val fun_in_Vfrom_limit = result();
   1.395 +
   1.396 +
   1.397 +(*** The set Vset(i) ***)
   1.398 +
   1.399 +goal Univ.thy "Vset(i) = (UN j:i. Pow(Vset(j)))";
   1.400 +by (rtac (Vfrom RS ssubst) 1);
   1.401 +by (fast_tac eq_cs 1);
   1.402 +val Vset = result();
   1.403 +
   1.404 +val Vset_succ = Transset_0 RS Transset_Vfrom_succ;
   1.405 +
   1.406 +val Transset_Vset = Transset_0 RS Transset_Vfrom;
   1.407 +
   1.408 +(** Characterisation of the elements of Vset(i) **)
   1.409 +
   1.410 +val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. b : Vset(i) --> rank(b) : i";
   1.411 +by (rtac (ordi RS trans_induct) 1);
   1.412 +by (rtac (Vset RS ssubst) 1);
   1.413 +by (safe_tac ZF_cs);
   1.414 +by (rtac (rank RS ssubst) 1);
   1.415 +by (rtac sup_least2 1);
   1.416 +by (assume_tac 1);
   1.417 +by (assume_tac 1);
   1.418 +by (fast_tac ZF_cs 1);
   1.419 +val Vset_rank_imp1 = result();
   1.420 +
   1.421 +(*  [| Ord(i); x : Vset(i) |] ==> rank(x) : i  *)
   1.422 +val Vset_D = standard (Vset_rank_imp1 RS spec RS mp);
   1.423 +
   1.424 +val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. rank(b) : i --> b : Vset(i)";
   1.425 +by (rtac (ordi RS trans_induct) 1);
   1.426 +by (rtac allI 1);
   1.427 +by (rtac (Vset RS ssubst) 1);
   1.428 +by (fast_tac (ZF_cs addSIs [rank_lt]) 1);
   1.429 +val Vset_rank_imp2 = result();
   1.430 +
   1.431 +(*  [| Ord(i); rank(x) : i |] ==> x : Vset(i)  *)
   1.432 +val VsetI = standard (Vset_rank_imp2 RS spec RS mp);
   1.433 +
   1.434 +val [ordi] = goal Univ.thy "Ord(i) ==> b : Vset(i) <-> rank(b) : i";
   1.435 +by (rtac iffI 1);
   1.436 +by (etac (ordi RS Vset_D) 1);
   1.437 +by (etac (ordi RS VsetI) 1);
   1.438 +val Vset_Ord_rank_iff = result();
   1.439 +
   1.440 +goal Univ.thy "b : Vset(a) <-> rank(b) : rank(a)";
   1.441 +by (rtac (Vfrom_rank_eq RS subst) 1);
   1.442 +by (rtac (Ord_rank RS Vset_Ord_rank_iff) 1);
   1.443 +val Vset_rank_iff = result();
   1.444 +
   1.445 +goal Univ.thy "!!i. Ord(i) ==> rank(Vset(i)) = i";
   1.446 +by (rtac (rank RS ssubst) 1);
   1.447 +by (rtac equalityI 1);
   1.448 +by (safe_tac ZF_cs);
   1.449 +by (EVERY' [wtac UN_I, 
   1.450 +	    etac (i_subset_Vfrom RS subsetD),
   1.451 +	    etac (Ord_in_Ord RS rank_of_Ord RS ssubst),
   1.452 +	    assume_tac,
   1.453 +	    rtac succI1] 3);
   1.454 +by (REPEAT (eresolve_tac [asm_rl,Vset_D,Ord_trans] 1));
   1.455 +val rank_Vset = result();
   1.456 +
   1.457 +(** Lemmas for reasoning about sets in terms of their elements' ranks **)
   1.458 +
   1.459 +(*  rank(x) : rank(a) ==> x : Vset(rank(a))  *)
   1.460 +val Vset_rankI = Ord_rank RS VsetI;
   1.461 +
   1.462 +goal Univ.thy "a <= Vset(rank(a))";
   1.463 +br subsetI 1;
   1.464 +be (rank_lt RS Vset_rankI) 1;
   1.465 +val arg_subset_Vset_rank = result();
   1.466 +
   1.467 +val [iprem] = goal Univ.thy
   1.468 +    "[| !!i. Ord(i) ==> a Int Vset(i) <= b |] ==> a <= b";
   1.469 +br ([subset_refl, arg_subset_Vset_rank] MRS Int_greatest RS subset_trans) 1;
   1.470 +br (Ord_rank RS iprem) 1;
   1.471 +val Int_Vset_subset = result();
   1.472 +
   1.473 +(** Set up an environment for simplification **)
   1.474 +
   1.475 +val rank_rls = [rank_Inl, rank_Inr, rank_pair1, rank_pair2];
   1.476 +val rank_trans_rls = rank_rls @ (rank_rls RLN (2, [rank_trans]));
   1.477 +
   1.478 +val rank_ss = ZF_ss 
   1.479 +    addrews [split, case_Inl, case_Inr, Vset_rankI]
   1.480 +    addrews rank_trans_rls;
   1.481 +
   1.482 +(** Recursion over Vset levels! **)
   1.483 +
   1.484 +(*NOT SUITABLE FOR REWRITING: recursive!*)
   1.485 +goalw Univ.thy [Vrec_def] "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))";
   1.486 +by (rtac (transrec RS ssubst) 1);
   1.487 +by (SIMP_TAC (wf_ss addrews [Ord_rank, Ord_succ, Vset_D RS beta, 
   1.488 +			     VsetI RS beta]) 1);
   1.489 +val Vrec = result();
   1.490 +
   1.491 +(*This form avoids giant explosions in proofs.  NOTE USE OF == *)
   1.492 +val rew::prems = goal Univ.thy
   1.493 +    "[| !!x. h(x)==Vrec(x,H) |] ==> \
   1.494 +\    h(a) = H(a, lam x: Vset(rank(a)). h(x))";
   1.495 +by (rewtac rew);
   1.496 +by (rtac Vrec 1);
   1.497 +val def_Vrec = result();
   1.498 +
   1.499 +val prems = goalw Univ.thy [Vrec_def]
   1.500 +    "[| a=a';  !!x u. H(x,u)=H'(x,u) |]  ==> Vrec(a,H)=Vrec(a',H')";
   1.501 +val Vrec_ss = ZF_ss addcongs ([transrec_cong] @ mk_congs Univ.thy ["rank"])
   1.502 +		      addrews (prems RL [sym]);
   1.503 +by (SIMP_TAC Vrec_ss 1);
   1.504 +val Vrec_cong = result();
   1.505 +
   1.506 +
   1.507 +(*** univ(A) ***)
   1.508 +
   1.509 +goalw Univ.thy [univ_def] "!!A B. A<=B ==> univ(A) <= univ(B)";
   1.510 +by (etac Vfrom_mono 1);
   1.511 +by (rtac subset_refl 1);
   1.512 +val univ_mono = result();
   1.513 +
   1.514 +goalw Univ.thy [univ_def] "!!A. Transset(A) ==> Transset(univ(A))";
   1.515 +by (etac Transset_Vfrom 1);
   1.516 +val Transset_univ = result();
   1.517 +
   1.518 +(** univ(A) as a limit **)
   1.519 +
   1.520 +goalw Univ.thy [univ_def] "univ(A) = (UN i:nat. Vfrom(A,i))";
   1.521 +br (Limit_nat RS Limit_Vfrom_eq) 1;
   1.522 +val univ_eq_UN = result();
   1.523 +
   1.524 +goal Univ.thy "!!c. c <= univ(A) ==> c = (UN i:nat. c Int Vfrom(A,i))";
   1.525 +br (subset_UN_iff_eq RS iffD1) 1;
   1.526 +be (univ_eq_UN RS subst) 1;
   1.527 +val subset_univ_eq_Int = result();
   1.528 +
   1.529 +val [aprem, iprem] = goal Univ.thy
   1.530 +    "[| a <= univ(X);			 	\
   1.531 +\       !!i. i:nat ==> a Int Vfrom(X,i) <= b 	\
   1.532 +\    |] ==> a <= b";
   1.533 +br (aprem RS subset_univ_eq_Int RS ssubst) 1;
   1.534 +br UN_least 1;
   1.535 +be iprem 1;
   1.536 +val univ_Int_Vfrom_subset = result();
   1.537 +
   1.538 +val prems = goal Univ.thy
   1.539 +    "[| a <= univ(X);   b <= univ(X);   \
   1.540 +\       !!i. i:nat ==> a Int Vfrom(X,i) = b Int Vfrom(X,i) \
   1.541 +\    |] ==> a = b";
   1.542 +br equalityI 1;
   1.543 +by (ALLGOALS
   1.544 +    (resolve_tac (prems RL [univ_Int_Vfrom_subset]) THEN'
   1.545 +     eresolve_tac (prems RL [equalityD1,equalityD2] RL [subset_trans]) THEN'
   1.546 +     rtac Int_lower1));
   1.547 +val univ_Int_Vfrom_eq = result();
   1.548 +
   1.549 +(** Closure properties **)
   1.550 +
   1.551 +goalw Univ.thy [univ_def] "0 : univ(A)";
   1.552 +by (rtac (nat_0I RS zero_in_Vfrom) 1);
   1.553 +val zero_in_univ = result();
   1.554 +
   1.555 +goalw Univ.thy [univ_def] "A <= univ(A)";
   1.556 +by (rtac A_subset_Vfrom 1);
   1.557 +val A_subset_univ = result();
   1.558 +
   1.559 +val A_into_univ = A_subset_univ RS subsetD;
   1.560 +
   1.561 +(** Closure under unordered and ordered pairs **)
   1.562 +
   1.563 +goalw Univ.thy [univ_def] "!!A a. a: univ(A) ==> {a} : univ(A)";
   1.564 +by (rtac singleton_in_Vfrom_limit 1);
   1.565 +by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1));
   1.566 +val singleton_in_univ = result();
   1.567 +
   1.568 +goalw Univ.thy [univ_def] 
   1.569 +    "!!A a. [| a: univ(A);  b: univ(A) |] ==> {a,b} : univ(A)";
   1.570 +by (rtac doubleton_in_Vfrom_limit 1);
   1.571 +by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1));
   1.572 +val doubleton_in_univ = result();
   1.573 +
   1.574 +goalw Univ.thy [univ_def]
   1.575 +    "!!A a. [| a: univ(A);  b: univ(A) |] ==> <a,b> : univ(A)";
   1.576 +by (rtac Pair_in_Vfrom_limit 1);
   1.577 +by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1));
   1.578 +val Pair_in_univ = result();
   1.579 +
   1.580 +goal Univ.thy "univ(A)*univ(A) <= univ(A)";
   1.581 +by (REPEAT (ares_tac [subsetI,Pair_in_univ] 1
   1.582 +     ORELSE eresolve_tac [SigmaE, ssubst] 1));
   1.583 +val product_univ = result();
   1.584 +
   1.585 +val Sigma_subset_univ = standard
   1.586 +    (Sigma_mono RS (product_univ RSN (2,subset_trans)));
   1.587 +
   1.588 +goalw Univ.thy [univ_def]
   1.589 +    "!!a b.[| <a,b> <= univ(A);  Transset(A) |] ==> <a,b> : univ(A)";
   1.590 +be Transset_Pair_subset_Vfrom_limit 1;
   1.591 +by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1));
   1.592 +val Transset_Pair_subset_univ = result();
   1.593 +
   1.594 +
   1.595 +(** The natural numbers **)
   1.596 +
   1.597 +goalw Univ.thy [univ_def] "nat <= univ(A)";
   1.598 +by (rtac i_subset_Vfrom 1);
   1.599 +val nat_subset_univ = result();
   1.600 +
   1.601 +(* n:nat ==> n:univ(A) *)
   1.602 +val nat_into_univ = standard (nat_subset_univ RS subsetD);
   1.603 +
   1.604 +(** instances for 1 and 2 **)
   1.605 +
   1.606 +goalw Univ.thy [one_def] "1 : univ(A)";
   1.607 +by (REPEAT (ares_tac [nat_into_univ, nat_0I, nat_succI] 1));
   1.608 +val one_in_univ = result();
   1.609 +
   1.610 +(*unused!*)
   1.611 +goal Univ.thy "succ(succ(0)) : univ(A)";
   1.612 +by (REPEAT (ares_tac [nat_into_univ, nat_0I, nat_succI] 1));
   1.613 +val two_in_univ = result();
   1.614 +
   1.615 +goalw Univ.thy [bool_def] "bool <= univ(A)";
   1.616 +by (fast_tac (ZF_cs addSIs [zero_in_univ,one_in_univ]) 1);
   1.617 +val bool_subset_univ = result();
   1.618 +
   1.619 +val bool_into_univ = standard (bool_subset_univ RS subsetD);
   1.620 +
   1.621 +
   1.622 +(** Closure under disjoint union **)
   1.623 +
   1.624 +goalw Univ.thy [Inl_def] "!!A a. a: univ(A) ==> Inl(a) : univ(A)";
   1.625 +by (REPEAT (ares_tac [zero_in_univ,Pair_in_univ] 1));
   1.626 +val Inl_in_univ = result();
   1.627 +
   1.628 +goalw Univ.thy [Inr_def] "!!A b. b: univ(A) ==> Inr(b) : univ(A)";
   1.629 +by (REPEAT (ares_tac [one_in_univ, Pair_in_univ] 1));
   1.630 +val Inr_in_univ = result();
   1.631 +
   1.632 +goal Univ.thy "univ(C)+univ(C) <= univ(C)";
   1.633 +by (REPEAT (ares_tac [subsetI,Inl_in_univ,Inr_in_univ] 1
   1.634 +     ORELSE eresolve_tac [sumE, ssubst] 1));
   1.635 +val sum_univ = result();
   1.636 +
   1.637 +val sum_subset_univ = standard
   1.638 +    (sum_mono RS (sum_univ RSN (2,subset_trans)));
   1.639 +
   1.640 +
   1.641 +(** Closure under binary union -- use Un_least **)
   1.642 +(** Closure under Collect -- use  (Collect_subset RS subset_trans)  **)
   1.643 +(** Closure under RepFun -- use   RepFun_subset  **)
   1.644 +
   1.645 +