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
```