0

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 nonempty;


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' [wtac 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 
