0

1 
(* Title: ZF/quniv


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1993 University of Cambridge


5 


6 
For quniv.thy. A small universe for lazy recursive types


7 
*)


8 


9 
open QUniv;


10 


11 
(** Introduction and elimination rules avoid tiresome folding/unfolding **)


12 


13 
goalw QUniv.thy [quniv_def]


14 
"!!X A. X <= univ(eclose(A)) ==> X : quniv(A)";


15 
be PowI 1;


16 
val qunivI = result();


17 


18 
goalw QUniv.thy [quniv_def]


19 
"!!X A. X : quniv(A) ==> X <= univ(eclose(A))";


20 
be PowD 1;


21 
val qunivD = result();


22 


23 
goalw QUniv.thy [quniv_def] "!!A B. A<=B ==> quniv(A) <= quniv(B)";


24 
by (etac (eclose_mono RS univ_mono RS Pow_mono) 1);


25 
val quniv_mono = result();


26 


27 
(*** Closure properties ***)


28 


29 
goalw QUniv.thy [quniv_def] "univ(eclose(A)) <= quniv(A)";


30 
by (rtac (Transset_iff_Pow RS iffD1) 1);


31 
by (rtac (Transset_eclose RS Transset_univ) 1);


32 
val univ_eclose_subset_quniv = result();


33 


34 
goal QUniv.thy "univ(A) <= quniv(A)";


35 
by (rtac (arg_subset_eclose RS univ_mono RS subset_trans) 1);


36 
by (rtac univ_eclose_subset_quniv 1);


37 
val univ_subset_quniv = result();


38 


39 
val univ_into_quniv = standard (univ_subset_quniv RS subsetD);


40 


41 
goalw QUniv.thy [quniv_def] "Pow(univ(A)) <= quniv(A)";


42 
by (rtac (arg_subset_eclose RS univ_mono RS Pow_mono) 1);


43 
val Pow_univ_subset_quniv = result();


44 


45 
val univ_subset_into_quniv = standard


46 
(PowI RS (Pow_univ_subset_quniv RS subsetD));


47 


48 
val zero_in_quniv = standard (zero_in_univ RS univ_into_quniv);


49 
val one_in_quniv = standard (one_in_univ RS univ_into_quniv);


50 
val two_in_quniv = standard (two_in_univ RS univ_into_quniv);


51 


52 
val A_subset_quniv = standard


53 
([A_subset_univ, univ_subset_quniv] MRS subset_trans);


54 


55 
val A_into_quniv = A_subset_quniv RS subsetD;


56 


57 
(*** univ(A) closure for Quineinspired pairs and injections ***)


58 


59 
(*Quine ordered pairs*)


60 
goalw QUniv.thy [QPair_def]


61 
"!!A a. [ a <= univ(A); b <= univ(A) ] ==> <a;b> <= univ(A)";


62 
by (REPEAT (ares_tac [sum_subset_univ] 1));


63 
val QPair_subset_univ = result();


64 


65 
(** Quine disjoint sum **)


66 


67 
goalw QUniv.thy [QInl_def] "!!A a. a <= univ(A) ==> QInl(a) <= univ(A)";


68 
by (etac (empty_subsetI RS QPair_subset_univ) 1);


69 
val QInl_subset_univ = result();


70 


71 
val naturals_subset_nat =


72 
rewrite_rule [Transset_def] (Ord_nat RS Ord_is_Transset)


73 
RS bspec;


74 


75 
val naturals_subset_univ =


76 
[naturals_subset_nat, nat_subset_univ] MRS subset_trans;


77 


78 
goalw QUniv.thy [QInr_def] "!!A a. a <= univ(A) ==> QInr(a) <= univ(A)";


79 
by (etac (nat_1I RS naturals_subset_univ RS QPair_subset_univ) 1);


80 
val QInr_subset_univ = result();


81 


82 
(*** Closure for Quineinspired products and sums ***)


83 


84 
(*Quine ordered pairs*)


85 
goalw QUniv.thy [quniv_def,QPair_def]


86 
"!!A a. [ a: quniv(A); b: quniv(A) ] ==> <a;b> : quniv(A)";


87 
by (REPEAT (dtac PowD 1));


88 
by (REPEAT (ares_tac [PowI, sum_subset_univ] 1));


89 
val QPair_in_quniv = result();


90 


91 
goal QUniv.thy "quniv(A) <*> quniv(A) <= quniv(A)";


92 
by (REPEAT (ares_tac [subsetI, QPair_in_quniv] 1


93 
ORELSE eresolve_tac [QSigmaE, ssubst] 1));


94 
val QSigma_quniv = result();


95 


96 
val QSigma_subset_quniv = standard


97 
(QSigma_mono RS (QSigma_quniv RSN (2,subset_trans)));


98 


99 
(*The opposite inclusion*)


100 
goalw QUniv.thy [quniv_def,QPair_def]


101 
"!!A a b. <a;b> : quniv(A) ==> a: quniv(A) & b: quniv(A)";


102 
be ([Transset_eclose RS Transset_univ, PowD] MRS


103 
Transset_includes_summands RS conjE) 1;


104 
by (REPEAT (ares_tac [conjI,PowI] 1));


105 
val quniv_QPair_D = result();


106 


107 
val quniv_QPair_E = standard (quniv_QPair_D RS conjE);


108 


109 
goal QUniv.thy "<a;b> : quniv(A) <> a: quniv(A) & b: quniv(A)";


110 
by (REPEAT (ares_tac [iffI, QPair_in_quniv, quniv_QPair_D] 1


111 
ORELSE etac conjE 1));


112 
val quniv_QPair_iff = result();


113 


114 


115 
(** Quine disjoint sum **)


116 


117 
goalw QUniv.thy [QInl_def] "!!A a. a: quniv(A) ==> QInl(a) : quniv(A)";


118 
by (REPEAT (ares_tac [zero_in_quniv,QPair_in_quniv] 1));


119 
val QInl_in_quniv = result();


120 


121 
goalw QUniv.thy [QInr_def] "!!A b. b: quniv(A) ==> QInr(b) : quniv(A)";


122 
by (REPEAT (ares_tac [one_in_quniv, QPair_in_quniv] 1));


123 
val QInr_in_quniv = result();


124 


125 
goal QUniv.thy "quniv(C) <+> quniv(C) <= quniv(C)";


126 
by (REPEAT (ares_tac [subsetI, QInl_in_quniv, QInr_in_quniv] 1


127 
ORELSE eresolve_tac [qsumE, ssubst] 1));


128 
val qsum_quniv = result();


129 


130 
val qsum_subset_quniv = standard


131 
(qsum_mono RS (qsum_quniv RSN (2,subset_trans)));


132 


133 
(*** The natural numbers ***)


134 


135 
val nat_subset_quniv = standard


136 
([nat_subset_univ, univ_subset_quniv] MRS subset_trans);


137 


138 
(* n:nat ==> n:quniv(A) *)


139 
val nat_into_quniv = standard (nat_subset_quniv RS subsetD);


140 


141 
val bool_subset_quniv = standard


142 
([bool_subset_univ, univ_subset_quniv] MRS subset_trans);


143 


144 
val bool_into_quniv = standard (bool_subset_quniv RS subsetD);


145 


146 


147 
(**** Properties of Vfrom analogous to the "takelemma" ****)


148 


149 
(*** Intersecting a*b with Vfrom... ***)


150 


151 
(*This version says a, b exist one level down, in the smaller set Vfrom(X,i)*)


152 
goal Univ.thy


153 
"!!X. [ {a,b} : Vfrom(X,succ(i)); Transset(X) ] ==> \


154 
\ a: Vfrom(X,i) & b: Vfrom(X,i)";


155 
bd (Transset_Vfrom_succ RS equalityD1 RS subsetD RS PowD) 1;


156 
ba 1;


157 
by (fast_tac ZF_cs 1);


158 
val doubleton_in_Vfrom_D = result();


159 


160 
(*This weaker version says a, b exist at the same level*)


161 
val Vfrom_doubleton_D = standard (Transset_Vfrom RS Transset_doubleton_D);


162 


163 
(** Using only the weaker theorem would prove <a,b> : Vfrom(X,i)


164 
implies a, b : Vfrom(X,i), which is useless for induction.


165 
Using only the stronger theorem would prove <a,b> : Vfrom(X,succ(succ(i)))


166 
implies a, b : Vfrom(X,i), leaving the succ(i) case untreated.


167 
The combination gives a reduction by precisely one level, which is


168 
most convenient for proofs.


169 
**)


170 


171 
goalw Univ.thy [Pair_def]


172 
"!!X. [ <a,b> : Vfrom(X,succ(i)); Transset(X) ] ==> \


173 
\ a: Vfrom(X,i) & b: Vfrom(X,i)";


174 
by (fast_tac (ZF_cs addSDs [doubleton_in_Vfrom_D, Vfrom_doubleton_D]) 1);


175 
val Pair_in_Vfrom_D = result();


176 


177 
goal Univ.thy


178 
"!!X. Transset(X) ==> \


179 
\ (a*b) Int Vfrom(X, succ(i)) <= (a Int Vfrom(X,i)) * (b Int Vfrom(X,i))";


180 
by (fast_tac (ZF_cs addSDs [Pair_in_Vfrom_D]) 1);


181 
val product_Int_Vfrom_subset = result();


182 


183 
(*** Intersecting <a;b> with Vfrom... ***)


184 


185 
goalw QUniv.thy [QPair_def,sum_def]


186 
"!!X. Transset(X) ==> \


187 
\ <a;b> Int Vfrom(X, succ(i)) <= <a Int Vfrom(X,i); b Int Vfrom(X,i)>";


188 
br (Int_Un_distrib RS ssubst) 1;


189 
br Un_mono 1;


190 
by (REPEAT (ares_tac [product_Int_Vfrom_subset RS subset_trans,


191 
[Int_lower1, subset_refl] MRS Sigma_mono] 1));


192 
val QPair_Int_Vfrom_succ_subset = result();


193 


194 
(** Pairs in quniv  for handling the base case **)


195 


196 
goal QUniv.thy "!!X. <a,b> : quniv(X) ==> <a,b> : univ(eclose(X))";


197 
be ([qunivD, Transset_eclose] MRS Transset_Pair_subset_univ) 1;


198 
val Pair_in_quniv_D = result();


199 


200 
goal QUniv.thy "a*b Int quniv(A) = a*b Int univ(eclose(A))";


201 
br equalityI 1;


202 
br ([subset_refl, univ_eclose_subset_quniv] MRS Int_mono) 2;


203 
by (fast_tac (ZF_cs addSEs [Pair_in_quniv_D]) 1);


204 
val product_Int_quniv_eq = result();


205 


206 
goalw QUniv.thy [QPair_def,sum_def]


207 
"<a;b> Int quniv(A) = <a;b> Int univ(eclose(A))";


208 
by (SIMP_TAC (ZF_ss addrews [Int_Un_distrib, product_Int_quniv_eq]) 1);


209 
val QPair_Int_quniv_eq = result();


210 


211 
(**** "Takelemma" rules for proving c: quniv(A) ****)


212 


213 
goalw QUniv.thy [quniv_def] "Transset(quniv(A))";


214 
br (Transset_eclose RS Transset_univ RS Transset_Pow) 1;


215 
val Transset_quniv = result();


216 


217 
val [aprem, iprem] = goal QUniv.thy


218 
"[ a: quniv(quniv(X)); \


219 
\ !!i. i:nat ==> a Int Vfrom(quniv(X),i) : quniv(A) \


220 
\ ] ==> a : quniv(A)";


221 
br (univ_Int_Vfrom_subset RS qunivI) 1;


222 
br (aprem RS qunivD) 1;


223 
by (rtac (Transset_quniv RS Transset_eclose_eq_arg RS ssubst) 1);


224 
be (iprem RS qunivD) 1;


225 
val quniv_Int_Vfrom = result();


226 


227 
(** Rules for level 0 **)


228 


229 
goal QUniv.thy "<a;b> Int quniv(A) : quniv(A)";


230 
br (QPair_Int_quniv_eq RS ssubst) 1;


231 
br (Int_lower2 RS qunivI) 1;


232 
val QPair_Int_quniv_in_quniv = result();


233 


234 
(*Unused; kept as an example. QInr rule is similar*)


235 
goalw QUniv.thy [QInl_def] "QInl(a) Int quniv(A) : quniv(A)";


236 
br QPair_Int_quniv_in_quniv 1;


237 
val QInl_Int_quniv_in_quniv = result();


238 


239 
goal QUniv.thy "!!a A X. a : quniv(A) ==> a Int X : quniv(A)";


240 
be ([Int_lower1, qunivD] MRS subset_trans RS qunivI) 1;


241 
val Int_quniv_in_quniv = result();


242 


243 
goal QUniv.thy


244 
"!!X. a Int X : quniv(A) ==> a Int Vfrom(X, 0) : quniv(A)";


245 
by (etac (Vfrom_0 RS ssubst) 1);


246 
val Int_Vfrom_0_in_quniv = result();


247 


248 
(** Rules for level succ(i), decreasing it to i **)


249 


250 
goal QUniv.thy


251 
"!!X. [ a Int Vfrom(X,i) : quniv(A); \


252 
\ b Int Vfrom(X,i) : quniv(A); \


253 
\ Transset(X) \


254 
\ ] ==> <a;b> Int Vfrom(X, succ(i)) : quniv(A)";


255 
br (QPair_Int_Vfrom_succ_subset RS subset_trans RS qunivI) 1;


256 
br (QPair_in_quniv RS qunivD) 2;


257 
by (REPEAT (assume_tac 1));


258 
val QPair_Int_Vfrom_succ_in_quniv = result();


259 


260 
val zero_Int_in_quniv = standard


261 
([Int_lower1,empty_subsetI] MRS subset_trans RS qunivI);


262 


263 
val one_Int_in_quniv = standard


264 
([Int_lower1, one_in_quniv RS qunivD] MRS subset_trans RS qunivI);


265 


266 
(*Unused; kept as an example. QInr rule is similar*)


267 
goalw QUniv.thy [QInl_def]


268 
"!!X. [ a Int Vfrom(X,i) : quniv(A); Transset(X) \


269 
\ ] ==> QInl(a) Int Vfrom(X, succ(i)) : quniv(A)";


270 
br QPair_Int_Vfrom_succ_in_quniv 1;


271 
by (REPEAT (ares_tac [zero_Int_in_quniv] 1));


272 
val QInl_Int_Vfrom_succ_in_quniv = result();


273 


274 
(** Rules for level i  preserving the level, not decreasing it **)


275 


276 
goalw QUniv.thy [QPair_def]


277 
"!!X. Transset(X) ==> \


278 
\ <a;b> Int Vfrom(X,i) <= <a Int Vfrom(X,i); b Int Vfrom(X,i)>";


279 
be (Transset_Vfrom RS Transset_sum_Int_subset) 1;


280 
val QPair_Int_Vfrom_subset = result();


281 


282 
goal QUniv.thy


283 
"!!X. [ a Int Vfrom(X,i) : quniv(A); \


284 
\ b Int Vfrom(X,i) : quniv(A); \


285 
\ Transset(X) \


286 
\ ] ==> <a;b> Int Vfrom(X,i) : quniv(A)";


287 
br (QPair_Int_Vfrom_subset RS subset_trans RS qunivI) 1;


288 
br (QPair_in_quniv RS qunivD) 2;


289 
by (REPEAT (assume_tac 1));


290 
val QPair_Int_Vfrom_in_quniv = result();


291 


292 


293 
(**** "Takelemma" rules for proving a=b by coinduction ****)


294 


295 
(** Unfortunately, the technique used above does not apply here, since


296 
the base case appears impossible to prove: it involves an intersection


297 
with eclose(X) for arbitrary X. So a=b is proved by transfinite induction


298 
over ALL ordinals, using Vset(i) instead of Vfrom(X,i).


299 
**)


300 


301 
(*Rule for level 0*)


302 
goal QUniv.thy "a Int Vset(0) <= b";


303 
by (rtac (Vfrom_0 RS ssubst) 1);


304 
by (fast_tac ZF_cs 1);


305 
val Int_Vset_0_subset = result();


306 


307 
(*Rule for level succ(i), decreasing it to i*)


308 
goal QUniv.thy


309 
"!!i. [ a Int Vset(i) <= c; \


310 
\ b Int Vset(i) <= d \


311 
\ ] ==> <a;b> Int Vset(succ(i)) <= <c;d>";


312 
br ([Transset_0 RS QPair_Int_Vfrom_succ_subset, QPair_mono]


313 
MRS subset_trans) 1;


314 
by (REPEAT (assume_tac 1));


315 
val QPair_Int_Vset_succ_subset_trans = result();


316 


317 
(*Unused; kept as an example. QInr rule is similar*)


318 
goalw QUniv.thy [QInl_def]


319 
"!!i. a Int Vset(i) <= b ==> QInl(a) Int Vset(succ(i)) <= QInl(b)";


320 
be (Int_lower1 RS QPair_Int_Vset_succ_subset_trans) 1;


321 
val QInl_Int_Vset_succ_subset_trans = result();


322 


323 
(*Rule for level i  preserving the level, not decreasing it*)


324 
goal QUniv.thy


325 
"!!i. [ a Int Vset(i) <= c; \


326 
\ b Int Vset(i) <= d \


327 
\ ] ==> <a;b> Int Vset(i) <= <c;d>";


328 
br ([Transset_0 RS QPair_Int_Vfrom_subset, QPair_mono]


329 
MRS subset_trans) 1;


330 
by (REPEAT (assume_tac 1));


331 
val QPair_Int_Vset_subset_trans = result();


332 


333 


334 
