src/ZF/QUniv.ML
changeset 0 a5a9c433f639
child 6 8ce8c4d13d4d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/QUniv.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,334 @@
     1.4 +(*  Title: 	ZF/quniv
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1993  University of Cambridge
     1.8 +
     1.9 +For quniv.thy.  A small universe for lazy recursive types
    1.10 +*)
    1.11 +
    1.12 +open QUniv;
    1.13 +
    1.14 +(** Introduction and elimination rules avoid tiresome folding/unfolding **)
    1.15 +
    1.16 +goalw QUniv.thy [quniv_def]
    1.17 +    "!!X A. X <= univ(eclose(A)) ==> X : quniv(A)";
    1.18 +be PowI 1;
    1.19 +val qunivI = result();
    1.20 +
    1.21 +goalw QUniv.thy [quniv_def]
    1.22 +    "!!X A. X : quniv(A) ==> X <= univ(eclose(A))";
    1.23 +be PowD 1;
    1.24 +val qunivD = result();
    1.25 +
    1.26 +goalw QUniv.thy [quniv_def] "!!A B. A<=B ==> quniv(A) <= quniv(B)";
    1.27 +by (etac (eclose_mono RS univ_mono RS Pow_mono) 1);
    1.28 +val quniv_mono = result();
    1.29 +
    1.30 +(*** Closure properties ***)
    1.31 +
    1.32 +goalw QUniv.thy [quniv_def] "univ(eclose(A)) <= quniv(A)";
    1.33 +by (rtac (Transset_iff_Pow RS iffD1) 1);
    1.34 +by (rtac (Transset_eclose RS Transset_univ) 1);
    1.35 +val univ_eclose_subset_quniv = result();
    1.36 +
    1.37 +goal QUniv.thy "univ(A) <= quniv(A)";
    1.38 +by (rtac (arg_subset_eclose RS univ_mono RS subset_trans) 1);
    1.39 +by (rtac univ_eclose_subset_quniv 1);
    1.40 +val univ_subset_quniv = result();
    1.41 +
    1.42 +val univ_into_quniv = standard (univ_subset_quniv RS subsetD);
    1.43 +
    1.44 +goalw QUniv.thy [quniv_def] "Pow(univ(A)) <= quniv(A)";
    1.45 +by (rtac (arg_subset_eclose RS univ_mono RS Pow_mono) 1);
    1.46 +val Pow_univ_subset_quniv = result();
    1.47 +
    1.48 +val univ_subset_into_quniv = standard
    1.49 +	(PowI RS (Pow_univ_subset_quniv RS subsetD));
    1.50 +
    1.51 +val zero_in_quniv = standard (zero_in_univ RS univ_into_quniv);
    1.52 +val one_in_quniv = standard (one_in_univ RS univ_into_quniv);
    1.53 +val two_in_quniv = standard (two_in_univ RS univ_into_quniv);
    1.54 +
    1.55 +val A_subset_quniv = standard
    1.56 +	([A_subset_univ, univ_subset_quniv] MRS subset_trans);
    1.57 +
    1.58 +val A_into_quniv = A_subset_quniv RS subsetD;
    1.59 +
    1.60 +(*** univ(A) closure for Quine-inspired pairs and injections ***)
    1.61 +
    1.62 +(*Quine ordered pairs*)
    1.63 +goalw QUniv.thy [QPair_def]
    1.64 +    "!!A a. [| a <= univ(A);  b <= univ(A) |] ==> <a;b> <= univ(A)";
    1.65 +by (REPEAT (ares_tac [sum_subset_univ] 1));
    1.66 +val QPair_subset_univ = result();
    1.67 +
    1.68 +(** Quine disjoint sum **)
    1.69 +
    1.70 +goalw QUniv.thy [QInl_def] "!!A a. a <= univ(A) ==> QInl(a) <= univ(A)";
    1.71 +by (etac (empty_subsetI RS QPair_subset_univ) 1);
    1.72 +val QInl_subset_univ = result();
    1.73 +
    1.74 +val naturals_subset_nat =
    1.75 +    rewrite_rule [Transset_def] (Ord_nat RS Ord_is_Transset)
    1.76 +    RS bspec;
    1.77 +
    1.78 +val naturals_subset_univ = 
    1.79 +    [naturals_subset_nat, nat_subset_univ] MRS subset_trans;
    1.80 +
    1.81 +goalw QUniv.thy [QInr_def] "!!A a. a <= univ(A) ==> QInr(a) <= univ(A)";
    1.82 +by (etac (nat_1I RS naturals_subset_univ RS QPair_subset_univ) 1);
    1.83 +val QInr_subset_univ = result();
    1.84 +
    1.85 +(*** Closure for Quine-inspired products and sums ***)
    1.86 +
    1.87 +(*Quine ordered pairs*)
    1.88 +goalw QUniv.thy [quniv_def,QPair_def]
    1.89 +    "!!A a. [| a: quniv(A);  b: quniv(A) |] ==> <a;b> : quniv(A)";
    1.90 +by (REPEAT (dtac PowD 1));
    1.91 +by (REPEAT (ares_tac [PowI, sum_subset_univ] 1));
    1.92 +val QPair_in_quniv = result();
    1.93 +
    1.94 +goal QUniv.thy "quniv(A) <*> quniv(A) <= quniv(A)";
    1.95 +by (REPEAT (ares_tac [subsetI, QPair_in_quniv] 1
    1.96 +     ORELSE eresolve_tac [QSigmaE, ssubst] 1));
    1.97 +val QSigma_quniv = result();
    1.98 +
    1.99 +val QSigma_subset_quniv = standard
   1.100 +    (QSigma_mono RS (QSigma_quniv RSN (2,subset_trans)));
   1.101 +
   1.102 +(*The opposite inclusion*)
   1.103 +goalw QUniv.thy [quniv_def,QPair_def]
   1.104 +    "!!A a b. <a;b> : quniv(A) ==> a: quniv(A) & b: quniv(A)";
   1.105 +be ([Transset_eclose RS Transset_univ, PowD] MRS 
   1.106 +    Transset_includes_summands RS conjE) 1;
   1.107 +by (REPEAT (ares_tac [conjI,PowI] 1));
   1.108 +val quniv_QPair_D = result();
   1.109 +
   1.110 +val quniv_QPair_E = standard (quniv_QPair_D RS conjE);
   1.111 +
   1.112 +goal QUniv.thy "<a;b> : quniv(A) <-> a: quniv(A) & b: quniv(A)";
   1.113 +by (REPEAT (ares_tac [iffI, QPair_in_quniv, quniv_QPair_D] 1
   1.114 +     ORELSE etac conjE 1));
   1.115 +val quniv_QPair_iff = result();
   1.116 +
   1.117 +
   1.118 +(** Quine disjoint sum **)
   1.119 +
   1.120 +goalw QUniv.thy [QInl_def] "!!A a. a: quniv(A) ==> QInl(a) : quniv(A)";
   1.121 +by (REPEAT (ares_tac [zero_in_quniv,QPair_in_quniv] 1));
   1.122 +val QInl_in_quniv = result();
   1.123 +
   1.124 +goalw QUniv.thy [QInr_def] "!!A b. b: quniv(A) ==> QInr(b) : quniv(A)";
   1.125 +by (REPEAT (ares_tac [one_in_quniv, QPair_in_quniv] 1));
   1.126 +val QInr_in_quniv = result();
   1.127 +
   1.128 +goal QUniv.thy "quniv(C) <+> quniv(C) <= quniv(C)";
   1.129 +by (REPEAT (ares_tac [subsetI, QInl_in_quniv, QInr_in_quniv] 1
   1.130 +     ORELSE eresolve_tac [qsumE, ssubst] 1));
   1.131 +val qsum_quniv = result();
   1.132 +
   1.133 +val qsum_subset_quniv = standard
   1.134 +    (qsum_mono RS (qsum_quniv RSN (2,subset_trans)));
   1.135 +
   1.136 +(*** The natural numbers ***)
   1.137 +
   1.138 +val nat_subset_quniv = standard
   1.139 +	([nat_subset_univ, univ_subset_quniv] MRS subset_trans);
   1.140 +
   1.141 +(* n:nat ==> n:quniv(A) *)
   1.142 +val nat_into_quniv = standard (nat_subset_quniv RS subsetD);
   1.143 +
   1.144 +val bool_subset_quniv = standard
   1.145 +	([bool_subset_univ, univ_subset_quniv] MRS subset_trans);
   1.146 +
   1.147 +val bool_into_quniv = standard (bool_subset_quniv RS subsetD);
   1.148 +
   1.149 +
   1.150 +(**** Properties of Vfrom analogous to the "take-lemma" ****)
   1.151 +
   1.152 +(*** Intersecting a*b with Vfrom... ***)
   1.153 +
   1.154 +(*This version says a, b exist one level down, in the smaller set Vfrom(X,i)*)
   1.155 +goal Univ.thy
   1.156 +    "!!X. [| {a,b} : Vfrom(X,succ(i));  Transset(X) |] ==> \
   1.157 +\         a: Vfrom(X,i)  &  b: Vfrom(X,i)";
   1.158 +bd (Transset_Vfrom_succ RS equalityD1 RS subsetD RS PowD) 1;
   1.159 +ba 1;
   1.160 +by (fast_tac ZF_cs 1);
   1.161 +val doubleton_in_Vfrom_D = result();
   1.162 +
   1.163 +(*This weaker version says a, b exist at the same level*)
   1.164 +val Vfrom_doubleton_D = standard (Transset_Vfrom RS Transset_doubleton_D);
   1.165 +
   1.166 +(** Using only the weaker theorem would prove <a,b> : Vfrom(X,i)
   1.167 +      implies a, b : Vfrom(X,i), which is useless for induction.
   1.168 +    Using only the stronger theorem would prove <a,b> : Vfrom(X,succ(succ(i)))
   1.169 +      implies a, b : Vfrom(X,i), leaving the succ(i) case untreated.
   1.170 +    The combination gives a reduction by precisely one level, which is
   1.171 +      most convenient for proofs.
   1.172 +**)
   1.173 +
   1.174 +goalw Univ.thy [Pair_def]
   1.175 +    "!!X. [| <a,b> : Vfrom(X,succ(i));  Transset(X) |] ==> \
   1.176 +\         a: Vfrom(X,i)  &  b: Vfrom(X,i)";
   1.177 +by (fast_tac (ZF_cs addSDs [doubleton_in_Vfrom_D, Vfrom_doubleton_D]) 1);
   1.178 +val Pair_in_Vfrom_D = result();
   1.179 +
   1.180 +goal Univ.thy
   1.181 + "!!X. Transset(X) ==> 		\
   1.182 +\      (a*b) Int Vfrom(X, succ(i)) <= (a Int Vfrom(X,i)) * (b Int Vfrom(X,i))";
   1.183 +by (fast_tac (ZF_cs addSDs [Pair_in_Vfrom_D]) 1);
   1.184 +val product_Int_Vfrom_subset = result();
   1.185 +
   1.186 +(*** Intersecting <a;b> with Vfrom... ***)
   1.187 +
   1.188 +goalw QUniv.thy [QPair_def,sum_def]
   1.189 + "!!X. Transset(X) ==> 		\
   1.190 +\      <a;b> Int Vfrom(X, succ(i))  <=  <a Int Vfrom(X,i);  b Int Vfrom(X,i)>";
   1.191 +br (Int_Un_distrib RS ssubst) 1;
   1.192 +br Un_mono 1;
   1.193 +by (REPEAT (ares_tac [product_Int_Vfrom_subset RS subset_trans,
   1.194 +		      [Int_lower1, subset_refl] MRS Sigma_mono] 1));
   1.195 +val QPair_Int_Vfrom_succ_subset = result();
   1.196 +
   1.197 +(** Pairs in quniv -- for handling the base case **)
   1.198 +
   1.199 +goal QUniv.thy "!!X. <a,b> : quniv(X) ==> <a,b> : univ(eclose(X))";
   1.200 +be ([qunivD, Transset_eclose] MRS Transset_Pair_subset_univ) 1;
   1.201 +val Pair_in_quniv_D = result();
   1.202 +
   1.203 +goal QUniv.thy "a*b Int quniv(A) = a*b Int univ(eclose(A))";
   1.204 +br equalityI 1;
   1.205 +br ([subset_refl, univ_eclose_subset_quniv] MRS Int_mono) 2;
   1.206 +by (fast_tac (ZF_cs addSEs [Pair_in_quniv_D]) 1);
   1.207 +val product_Int_quniv_eq = result();
   1.208 +
   1.209 +goalw QUniv.thy [QPair_def,sum_def]
   1.210 +    "<a;b> Int quniv(A) = <a;b> Int univ(eclose(A))";
   1.211 +by (SIMP_TAC (ZF_ss addrews [Int_Un_distrib, product_Int_quniv_eq]) 1);
   1.212 +val QPair_Int_quniv_eq = result();
   1.213 +
   1.214 +(**** "Take-lemma" rules for proving c: quniv(A) ****)
   1.215 +
   1.216 +goalw QUniv.thy [quniv_def] "Transset(quniv(A))";
   1.217 +br (Transset_eclose RS Transset_univ RS Transset_Pow) 1;
   1.218 +val Transset_quniv = result();
   1.219 +
   1.220 +val [aprem, iprem] = goal QUniv.thy
   1.221 +    "[| a: quniv(quniv(X));  	\
   1.222 +\       !!i. i:nat ==> a Int Vfrom(quniv(X),i) : quniv(A) \
   1.223 +\    |] ==> a : quniv(A)";
   1.224 +br (univ_Int_Vfrom_subset RS qunivI) 1;
   1.225 +br (aprem RS qunivD) 1;
   1.226 +by (rtac (Transset_quniv RS Transset_eclose_eq_arg RS ssubst) 1);
   1.227 +be (iprem RS qunivD) 1;
   1.228 +val quniv_Int_Vfrom = result();
   1.229 +
   1.230 +(** Rules for level 0 **)
   1.231 +
   1.232 +goal QUniv.thy "<a;b> Int quniv(A) : quniv(A)";
   1.233 +br (QPair_Int_quniv_eq RS ssubst) 1;
   1.234 +br (Int_lower2 RS qunivI) 1;
   1.235 +val QPair_Int_quniv_in_quniv = result();
   1.236 +
   1.237 +(*Unused; kept as an example.  QInr rule is similar*)
   1.238 +goalw QUniv.thy [QInl_def] "QInl(a) Int quniv(A) : quniv(A)";
   1.239 +br QPair_Int_quniv_in_quniv 1;
   1.240 +val QInl_Int_quniv_in_quniv = result();
   1.241 +
   1.242 +goal QUniv.thy "!!a A X. a : quniv(A) ==> a Int X : quniv(A)";
   1.243 +be ([Int_lower1, qunivD] MRS subset_trans RS qunivI) 1;
   1.244 +val Int_quniv_in_quniv = result();
   1.245 +
   1.246 +goal QUniv.thy 
   1.247 + "!!X. a Int X : quniv(A) ==> a Int Vfrom(X, 0) : quniv(A)";
   1.248 +by (etac (Vfrom_0 RS ssubst) 1);
   1.249 +val Int_Vfrom_0_in_quniv = result();
   1.250 +
   1.251 +(** Rules for level succ(i), decreasing it to i **)
   1.252 +
   1.253 +goal QUniv.thy 
   1.254 + "!!X. [| a Int Vfrom(X,i) : quniv(A);	\
   1.255 +\         b Int Vfrom(X,i) : quniv(A);	\
   1.256 +\         Transset(X) 			\
   1.257 +\      |] ==> <a;b> Int Vfrom(X, succ(i)) : quniv(A)";
   1.258 +br (QPair_Int_Vfrom_succ_subset RS subset_trans RS qunivI) 1;
   1.259 +br (QPair_in_quniv RS qunivD) 2;
   1.260 +by (REPEAT (assume_tac 1));
   1.261 +val QPair_Int_Vfrom_succ_in_quniv = result();
   1.262 +
   1.263 +val zero_Int_in_quniv = standard
   1.264 +    ([Int_lower1,empty_subsetI] MRS subset_trans RS qunivI);
   1.265 +
   1.266 +val one_Int_in_quniv = standard
   1.267 +    ([Int_lower1, one_in_quniv RS qunivD] MRS subset_trans RS qunivI);
   1.268 +
   1.269 +(*Unused; kept as an example.  QInr rule is similar*)
   1.270 +goalw QUniv.thy [QInl_def]
   1.271 + "!!X. [| a Int Vfrom(X,i) : quniv(A);	Transset(X) 		\
   1.272 +\      |] ==> QInl(a) Int Vfrom(X, succ(i)) : quniv(A)";
   1.273 +br QPair_Int_Vfrom_succ_in_quniv 1;
   1.274 +by (REPEAT (ares_tac [zero_Int_in_quniv] 1));
   1.275 +val QInl_Int_Vfrom_succ_in_quniv = result();
   1.276 +
   1.277 +(** Rules for level i -- preserving the level, not decreasing it **)
   1.278 +
   1.279 +goalw QUniv.thy [QPair_def]
   1.280 + "!!X. Transset(X) ==> 		\
   1.281 +\      <a;b> Int Vfrom(X,i)  <=  <a Int Vfrom(X,i);  b Int Vfrom(X,i)>";
   1.282 +be (Transset_Vfrom RS Transset_sum_Int_subset) 1;
   1.283 +val QPair_Int_Vfrom_subset = result();
   1.284 +
   1.285 +goal QUniv.thy 
   1.286 + "!!X. [| a Int Vfrom(X,i) : quniv(A);	\
   1.287 +\         b Int Vfrom(X,i) : quniv(A);	\
   1.288 +\         Transset(X) 			\
   1.289 +\      |] ==> <a;b> Int Vfrom(X,i) : quniv(A)";
   1.290 +br (QPair_Int_Vfrom_subset RS subset_trans RS qunivI) 1;
   1.291 +br (QPair_in_quniv RS qunivD) 2;
   1.292 +by (REPEAT (assume_tac 1));
   1.293 +val QPair_Int_Vfrom_in_quniv = result();
   1.294 +
   1.295 +
   1.296 +(**** "Take-lemma" rules for proving a=b by co-induction ****)
   1.297 +
   1.298 +(** Unfortunately, the technique used above does not apply here, since
   1.299 +    the base case appears impossible to prove: it involves an intersection
   1.300 +    with eclose(X) for arbitrary X.  So a=b is proved by transfinite induction
   1.301 +    over ALL ordinals, using Vset(i) instead of Vfrom(X,i).
   1.302 +**)
   1.303 +
   1.304 +(*Rule for level 0*)
   1.305 +goal QUniv.thy "a Int Vset(0) <= b";
   1.306 +by (rtac (Vfrom_0 RS ssubst) 1);
   1.307 +by (fast_tac ZF_cs 1);
   1.308 +val Int_Vset_0_subset = result();
   1.309 +
   1.310 +(*Rule for level succ(i), decreasing it to i*)
   1.311 +goal QUniv.thy 
   1.312 + "!!i. [| a Int Vset(i) <= c;	\
   1.313 +\         b Int Vset(i) <= d	\
   1.314 +\      |] ==> <a;b> Int Vset(succ(i))  <=  <c;d>";
   1.315 +br ([Transset_0 RS QPair_Int_Vfrom_succ_subset, QPair_mono] 
   1.316 +    MRS subset_trans) 1;
   1.317 +by (REPEAT (assume_tac 1));
   1.318 +val QPair_Int_Vset_succ_subset_trans = result();
   1.319 +
   1.320 +(*Unused; kept as an example.  QInr rule is similar*)
   1.321 +goalw QUniv.thy [QInl_def] 
   1.322 + "!!i. a Int Vset(i) <= b ==> QInl(a) Int Vset(succ(i)) <= QInl(b)";
   1.323 +be (Int_lower1 RS QPair_Int_Vset_succ_subset_trans) 1;
   1.324 +val QInl_Int_Vset_succ_subset_trans = result();
   1.325 +
   1.326 +(*Rule for level i -- preserving the level, not decreasing it*)
   1.327 +goal QUniv.thy 
   1.328 + "!!i. [| a Int Vset(i) <= c;	\
   1.329 +\         b Int Vset(i) <= d	\
   1.330 +\      |] ==> <a;b> Int Vset(i)  <=  <c;d>";
   1.331 +br ([Transset_0 RS QPair_Int_Vfrom_subset, QPair_mono] 
   1.332 +    MRS subset_trans) 1;
   1.333 +by (REPEAT (assume_tac 1));
   1.334 +val QPair_Int_Vset_subset_trans = result();
   1.335 +
   1.336 +
   1.337 +