src/ZF/QUniv.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/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 Quine-inspired 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 Quine-inspired 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 "take-lemma" ****)
   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 (**** "Take-lemma" 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 (**** "Take-lemma" rules for proving a=b by co-induction ****)
   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