src/ZF/quniv.ML
author lcp
Fri Sep 17 16:16:38 1993 +0200 (1993-09-17)
changeset 6 8ce8c4d13d4d
parent 0 a5a9c433f639
child 14 1c0926788772
permissions -rw-r--r--
Installation of new simplifier for ZF. Deleted all congruence rules not
involving local assumptions. NB the congruence rules for Sigma and Pi
(dependent type constructions) cause difficulties and are not used by
default.
     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 addsimps [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