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
clasohm@0
     1
(*  Title: 	ZF/quniv
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
clasohm@0
     6
For quniv.thy.  A small universe for lazy recursive types
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
open QUniv;
clasohm@0
    10
clasohm@0
    11
(** Introduction and elimination rules avoid tiresome folding/unfolding **)
clasohm@0
    12
clasohm@0
    13
goalw QUniv.thy [quniv_def]
clasohm@0
    14
    "!!X A. X <= univ(eclose(A)) ==> X : quniv(A)";
clasohm@0
    15
be PowI 1;
clasohm@0
    16
val qunivI = result();
clasohm@0
    17
clasohm@0
    18
goalw QUniv.thy [quniv_def]
clasohm@0
    19
    "!!X A. X : quniv(A) ==> X <= univ(eclose(A))";
clasohm@0
    20
be PowD 1;
clasohm@0
    21
val qunivD = result();
clasohm@0
    22
clasohm@0
    23
goalw QUniv.thy [quniv_def] "!!A B. A<=B ==> quniv(A) <= quniv(B)";
clasohm@0
    24
by (etac (eclose_mono RS univ_mono RS Pow_mono) 1);
clasohm@0
    25
val quniv_mono = result();
clasohm@0
    26
clasohm@0
    27
(*** Closure properties ***)
clasohm@0
    28
clasohm@0
    29
goalw QUniv.thy [quniv_def] "univ(eclose(A)) <= quniv(A)";
clasohm@0
    30
by (rtac (Transset_iff_Pow RS iffD1) 1);
clasohm@0
    31
by (rtac (Transset_eclose RS Transset_univ) 1);
clasohm@0
    32
val univ_eclose_subset_quniv = result();
clasohm@0
    33
clasohm@0
    34
goal QUniv.thy "univ(A) <= quniv(A)";
clasohm@0
    35
by (rtac (arg_subset_eclose RS univ_mono RS subset_trans) 1);
clasohm@0
    36
by (rtac univ_eclose_subset_quniv 1);
clasohm@0
    37
val univ_subset_quniv = result();
clasohm@0
    38
clasohm@0
    39
val univ_into_quniv = standard (univ_subset_quniv RS subsetD);
clasohm@0
    40
clasohm@0
    41
goalw QUniv.thy [quniv_def] "Pow(univ(A)) <= quniv(A)";
clasohm@0
    42
by (rtac (arg_subset_eclose RS univ_mono RS Pow_mono) 1);
clasohm@0
    43
val Pow_univ_subset_quniv = result();
clasohm@0
    44
clasohm@0
    45
val univ_subset_into_quniv = standard
clasohm@0
    46
	(PowI RS (Pow_univ_subset_quniv RS subsetD));
clasohm@0
    47
clasohm@0
    48
val zero_in_quniv = standard (zero_in_univ RS univ_into_quniv);
clasohm@0
    49
val one_in_quniv = standard (one_in_univ RS univ_into_quniv);
clasohm@0
    50
val two_in_quniv = standard (two_in_univ RS univ_into_quniv);
clasohm@0
    51
clasohm@0
    52
val A_subset_quniv = standard
clasohm@0
    53
	([A_subset_univ, univ_subset_quniv] MRS subset_trans);
clasohm@0
    54
clasohm@0
    55
val A_into_quniv = A_subset_quniv RS subsetD;
clasohm@0
    56
clasohm@0
    57
(*** univ(A) closure for Quine-inspired pairs and injections ***)
clasohm@0
    58
clasohm@0
    59
(*Quine ordered pairs*)
clasohm@0
    60
goalw QUniv.thy [QPair_def]
clasohm@0
    61
    "!!A a. [| a <= univ(A);  b <= univ(A) |] ==> <a;b> <= univ(A)";
clasohm@0
    62
by (REPEAT (ares_tac [sum_subset_univ] 1));
clasohm@0
    63
val QPair_subset_univ = result();
clasohm@0
    64
clasohm@0
    65
(** Quine disjoint sum **)
clasohm@0
    66
clasohm@0
    67
goalw QUniv.thy [QInl_def] "!!A a. a <= univ(A) ==> QInl(a) <= univ(A)";
clasohm@0
    68
by (etac (empty_subsetI RS QPair_subset_univ) 1);
clasohm@0
    69
val QInl_subset_univ = result();
clasohm@0
    70
clasohm@0
    71
val naturals_subset_nat =
clasohm@0
    72
    rewrite_rule [Transset_def] (Ord_nat RS Ord_is_Transset)
clasohm@0
    73
    RS bspec;
clasohm@0
    74
clasohm@0
    75
val naturals_subset_univ = 
clasohm@0
    76
    [naturals_subset_nat, nat_subset_univ] MRS subset_trans;
clasohm@0
    77
clasohm@0
    78
goalw QUniv.thy [QInr_def] "!!A a. a <= univ(A) ==> QInr(a) <= univ(A)";
clasohm@0
    79
by (etac (nat_1I RS naturals_subset_univ RS QPair_subset_univ) 1);
clasohm@0
    80
val QInr_subset_univ = result();
clasohm@0
    81
clasohm@0
    82
(*** Closure for Quine-inspired products and sums ***)
clasohm@0
    83
clasohm@0
    84
(*Quine ordered pairs*)
clasohm@0
    85
goalw QUniv.thy [quniv_def,QPair_def]
clasohm@0
    86
    "!!A a. [| a: quniv(A);  b: quniv(A) |] ==> <a;b> : quniv(A)";
clasohm@0
    87
by (REPEAT (dtac PowD 1));
clasohm@0
    88
by (REPEAT (ares_tac [PowI, sum_subset_univ] 1));
clasohm@0
    89
val QPair_in_quniv = result();
clasohm@0
    90
clasohm@0
    91
goal QUniv.thy "quniv(A) <*> quniv(A) <= quniv(A)";
clasohm@0
    92
by (REPEAT (ares_tac [subsetI, QPair_in_quniv] 1
clasohm@0
    93
     ORELSE eresolve_tac [QSigmaE, ssubst] 1));
clasohm@0
    94
val QSigma_quniv = result();
clasohm@0
    95
clasohm@0
    96
val QSigma_subset_quniv = standard
clasohm@0
    97
    (QSigma_mono RS (QSigma_quniv RSN (2,subset_trans)));
clasohm@0
    98
clasohm@0
    99
(*The opposite inclusion*)
clasohm@0
   100
goalw QUniv.thy [quniv_def,QPair_def]
clasohm@0
   101
    "!!A a b. <a;b> : quniv(A) ==> a: quniv(A) & b: quniv(A)";
clasohm@0
   102
be ([Transset_eclose RS Transset_univ, PowD] MRS 
clasohm@0
   103
    Transset_includes_summands RS conjE) 1;
clasohm@0
   104
by (REPEAT (ares_tac [conjI,PowI] 1));
clasohm@0
   105
val quniv_QPair_D = result();
clasohm@0
   106
clasohm@0
   107
val quniv_QPair_E = standard (quniv_QPair_D RS conjE);
clasohm@0
   108
clasohm@0
   109
goal QUniv.thy "<a;b> : quniv(A) <-> a: quniv(A) & b: quniv(A)";
clasohm@0
   110
by (REPEAT (ares_tac [iffI, QPair_in_quniv, quniv_QPair_D] 1
clasohm@0
   111
     ORELSE etac conjE 1));
clasohm@0
   112
val quniv_QPair_iff = result();
clasohm@0
   113
clasohm@0
   114
clasohm@0
   115
(** Quine disjoint sum **)
clasohm@0
   116
clasohm@0
   117
goalw QUniv.thy [QInl_def] "!!A a. a: quniv(A) ==> QInl(a) : quniv(A)";
clasohm@0
   118
by (REPEAT (ares_tac [zero_in_quniv,QPair_in_quniv] 1));
clasohm@0
   119
val QInl_in_quniv = result();
clasohm@0
   120
clasohm@0
   121
goalw QUniv.thy [QInr_def] "!!A b. b: quniv(A) ==> QInr(b) : quniv(A)";
clasohm@0
   122
by (REPEAT (ares_tac [one_in_quniv, QPair_in_quniv] 1));
clasohm@0
   123
val QInr_in_quniv = result();
clasohm@0
   124
clasohm@0
   125
goal QUniv.thy "quniv(C) <+> quniv(C) <= quniv(C)";
clasohm@0
   126
by (REPEAT (ares_tac [subsetI, QInl_in_quniv, QInr_in_quniv] 1
clasohm@0
   127
     ORELSE eresolve_tac [qsumE, ssubst] 1));
clasohm@0
   128
val qsum_quniv = result();
clasohm@0
   129
clasohm@0
   130
val qsum_subset_quniv = standard
clasohm@0
   131
    (qsum_mono RS (qsum_quniv RSN (2,subset_trans)));
clasohm@0
   132
clasohm@0
   133
(*** The natural numbers ***)
clasohm@0
   134
clasohm@0
   135
val nat_subset_quniv = standard
clasohm@0
   136
	([nat_subset_univ, univ_subset_quniv] MRS subset_trans);
clasohm@0
   137
clasohm@0
   138
(* n:nat ==> n:quniv(A) *)
clasohm@0
   139
val nat_into_quniv = standard (nat_subset_quniv RS subsetD);
clasohm@0
   140
clasohm@0
   141
val bool_subset_quniv = standard
clasohm@0
   142
	([bool_subset_univ, univ_subset_quniv] MRS subset_trans);
clasohm@0
   143
clasohm@0
   144
val bool_into_quniv = standard (bool_subset_quniv RS subsetD);
clasohm@0
   145
clasohm@0
   146
clasohm@0
   147
(**** Properties of Vfrom analogous to the "take-lemma" ****)
clasohm@0
   148
clasohm@0
   149
(*** Intersecting a*b with Vfrom... ***)
clasohm@0
   150
clasohm@0
   151
(*This version says a, b exist one level down, in the smaller set Vfrom(X,i)*)
clasohm@0
   152
goal Univ.thy
clasohm@0
   153
    "!!X. [| {a,b} : Vfrom(X,succ(i));  Transset(X) |] ==> \
clasohm@0
   154
\         a: Vfrom(X,i)  &  b: Vfrom(X,i)";
clasohm@0
   155
bd (Transset_Vfrom_succ RS equalityD1 RS subsetD RS PowD) 1;
clasohm@0
   156
ba 1;
clasohm@0
   157
by (fast_tac ZF_cs 1);
clasohm@0
   158
val doubleton_in_Vfrom_D = result();
clasohm@0
   159
clasohm@0
   160
(*This weaker version says a, b exist at the same level*)
clasohm@0
   161
val Vfrom_doubleton_D = standard (Transset_Vfrom RS Transset_doubleton_D);
clasohm@0
   162
clasohm@0
   163
(** Using only the weaker theorem would prove <a,b> : Vfrom(X,i)
clasohm@0
   164
      implies a, b : Vfrom(X,i), which is useless for induction.
clasohm@0
   165
    Using only the stronger theorem would prove <a,b> : Vfrom(X,succ(succ(i)))
clasohm@0
   166
      implies a, b : Vfrom(X,i), leaving the succ(i) case untreated.
clasohm@0
   167
    The combination gives a reduction by precisely one level, which is
clasohm@0
   168
      most convenient for proofs.
clasohm@0
   169
**)
clasohm@0
   170
clasohm@0
   171
goalw Univ.thy [Pair_def]
clasohm@0
   172
    "!!X. [| <a,b> : Vfrom(X,succ(i));  Transset(X) |] ==> \
clasohm@0
   173
\         a: Vfrom(X,i)  &  b: Vfrom(X,i)";
clasohm@0
   174
by (fast_tac (ZF_cs addSDs [doubleton_in_Vfrom_D, Vfrom_doubleton_D]) 1);
clasohm@0
   175
val Pair_in_Vfrom_D = result();
clasohm@0
   176
clasohm@0
   177
goal Univ.thy
clasohm@0
   178
 "!!X. Transset(X) ==> 		\
clasohm@0
   179
\      (a*b) Int Vfrom(X, succ(i)) <= (a Int Vfrom(X,i)) * (b Int Vfrom(X,i))";
clasohm@0
   180
by (fast_tac (ZF_cs addSDs [Pair_in_Vfrom_D]) 1);
clasohm@0
   181
val product_Int_Vfrom_subset = result();
clasohm@0
   182
clasohm@0
   183
(*** Intersecting <a;b> with Vfrom... ***)
clasohm@0
   184
clasohm@0
   185
goalw QUniv.thy [QPair_def,sum_def]
clasohm@0
   186
 "!!X. Transset(X) ==> 		\
clasohm@0
   187
\      <a;b> Int Vfrom(X, succ(i))  <=  <a Int Vfrom(X,i);  b Int Vfrom(X,i)>";
clasohm@0
   188
br (Int_Un_distrib RS ssubst) 1;
clasohm@0
   189
br Un_mono 1;
clasohm@0
   190
by (REPEAT (ares_tac [product_Int_Vfrom_subset RS subset_trans,
clasohm@0
   191
		      [Int_lower1, subset_refl] MRS Sigma_mono] 1));
clasohm@0
   192
val QPair_Int_Vfrom_succ_subset = result();
clasohm@0
   193
clasohm@0
   194
(** Pairs in quniv -- for handling the base case **)
clasohm@0
   195
clasohm@0
   196
goal QUniv.thy "!!X. <a,b> : quniv(X) ==> <a,b> : univ(eclose(X))";
clasohm@0
   197
be ([qunivD, Transset_eclose] MRS Transset_Pair_subset_univ) 1;
clasohm@0
   198
val Pair_in_quniv_D = result();
clasohm@0
   199
clasohm@0
   200
goal QUniv.thy "a*b Int quniv(A) = a*b Int univ(eclose(A))";
clasohm@0
   201
br equalityI 1;
clasohm@0
   202
br ([subset_refl, univ_eclose_subset_quniv] MRS Int_mono) 2;
clasohm@0
   203
by (fast_tac (ZF_cs addSEs [Pair_in_quniv_D]) 1);
clasohm@0
   204
val product_Int_quniv_eq = result();
clasohm@0
   205
clasohm@0
   206
goalw QUniv.thy [QPair_def,sum_def]
clasohm@0
   207
    "<a;b> Int quniv(A) = <a;b> Int univ(eclose(A))";
clasohm@0
   208
by (SIMP_TAC (ZF_ss addrews [Int_Un_distrib, product_Int_quniv_eq]) 1);
clasohm@0
   209
val QPair_Int_quniv_eq = result();
clasohm@0
   210
clasohm@0
   211
(**** "Take-lemma" rules for proving c: quniv(A) ****)
clasohm@0
   212
clasohm@0
   213
goalw QUniv.thy [quniv_def] "Transset(quniv(A))";
clasohm@0
   214
br (Transset_eclose RS Transset_univ RS Transset_Pow) 1;
clasohm@0
   215
val Transset_quniv = result();
clasohm@0
   216
clasohm@0
   217
val [aprem, iprem] = goal QUniv.thy
clasohm@0
   218
    "[| a: quniv(quniv(X));  	\
clasohm@0
   219
\       !!i. i:nat ==> a Int Vfrom(quniv(X),i) : quniv(A) \
clasohm@0
   220
\    |] ==> a : quniv(A)";
clasohm@0
   221
br (univ_Int_Vfrom_subset RS qunivI) 1;
clasohm@0
   222
br (aprem RS qunivD) 1;
clasohm@0
   223
by (rtac (Transset_quniv RS Transset_eclose_eq_arg RS ssubst) 1);
clasohm@0
   224
be (iprem RS qunivD) 1;
clasohm@0
   225
val quniv_Int_Vfrom = result();
clasohm@0
   226
clasohm@0
   227
(** Rules for level 0 **)
clasohm@0
   228
clasohm@0
   229
goal QUniv.thy "<a;b> Int quniv(A) : quniv(A)";
clasohm@0
   230
br (QPair_Int_quniv_eq RS ssubst) 1;
clasohm@0
   231
br (Int_lower2 RS qunivI) 1;
clasohm@0
   232
val QPair_Int_quniv_in_quniv = result();
clasohm@0
   233
clasohm@0
   234
(*Unused; kept as an example.  QInr rule is similar*)
clasohm@0
   235
goalw QUniv.thy [QInl_def] "QInl(a) Int quniv(A) : quniv(A)";
clasohm@0
   236
br QPair_Int_quniv_in_quniv 1;
clasohm@0
   237
val QInl_Int_quniv_in_quniv = result();
clasohm@0
   238
clasohm@0
   239
goal QUniv.thy "!!a A X. a : quniv(A) ==> a Int X : quniv(A)";
clasohm@0
   240
be ([Int_lower1, qunivD] MRS subset_trans RS qunivI) 1;
clasohm@0
   241
val Int_quniv_in_quniv = result();
clasohm@0
   242
clasohm@0
   243
goal QUniv.thy 
clasohm@0
   244
 "!!X. a Int X : quniv(A) ==> a Int Vfrom(X, 0) : quniv(A)";
clasohm@0
   245
by (etac (Vfrom_0 RS ssubst) 1);
clasohm@0
   246
val Int_Vfrom_0_in_quniv = result();
clasohm@0
   247
clasohm@0
   248
(** Rules for level succ(i), decreasing it to i **)
clasohm@0
   249
clasohm@0
   250
goal QUniv.thy 
clasohm@0
   251
 "!!X. [| a Int Vfrom(X,i) : quniv(A);	\
clasohm@0
   252
\         b Int Vfrom(X,i) : quniv(A);	\
clasohm@0
   253
\         Transset(X) 			\
clasohm@0
   254
\      |] ==> <a;b> Int Vfrom(X, succ(i)) : quniv(A)";
clasohm@0
   255
br (QPair_Int_Vfrom_succ_subset RS subset_trans RS qunivI) 1;
clasohm@0
   256
br (QPair_in_quniv RS qunivD) 2;
clasohm@0
   257
by (REPEAT (assume_tac 1));
clasohm@0
   258
val QPair_Int_Vfrom_succ_in_quniv = result();
clasohm@0
   259
clasohm@0
   260
val zero_Int_in_quniv = standard
clasohm@0
   261
    ([Int_lower1,empty_subsetI] MRS subset_trans RS qunivI);
clasohm@0
   262
clasohm@0
   263
val one_Int_in_quniv = standard
clasohm@0
   264
    ([Int_lower1, one_in_quniv RS qunivD] MRS subset_trans RS qunivI);
clasohm@0
   265
clasohm@0
   266
(*Unused; kept as an example.  QInr rule is similar*)
clasohm@0
   267
goalw QUniv.thy [QInl_def]
clasohm@0
   268
 "!!X. [| a Int Vfrom(X,i) : quniv(A);	Transset(X) 		\
clasohm@0
   269
\      |] ==> QInl(a) Int Vfrom(X, succ(i)) : quniv(A)";
clasohm@0
   270
br QPair_Int_Vfrom_succ_in_quniv 1;
clasohm@0
   271
by (REPEAT (ares_tac [zero_Int_in_quniv] 1));
clasohm@0
   272
val QInl_Int_Vfrom_succ_in_quniv = result();
clasohm@0
   273
clasohm@0
   274
(** Rules for level i -- preserving the level, not decreasing it **)
clasohm@0
   275
clasohm@0
   276
goalw QUniv.thy [QPair_def]
clasohm@0
   277
 "!!X. Transset(X) ==> 		\
clasohm@0
   278
\      <a;b> Int Vfrom(X,i)  <=  <a Int Vfrom(X,i);  b Int Vfrom(X,i)>";
clasohm@0
   279
be (Transset_Vfrom RS Transset_sum_Int_subset) 1;
clasohm@0
   280
val QPair_Int_Vfrom_subset = result();
clasohm@0
   281
clasohm@0
   282
goal QUniv.thy 
clasohm@0
   283
 "!!X. [| a Int Vfrom(X,i) : quniv(A);	\
clasohm@0
   284
\         b Int Vfrom(X,i) : quniv(A);	\
clasohm@0
   285
\         Transset(X) 			\
clasohm@0
   286
\      |] ==> <a;b> Int Vfrom(X,i) : quniv(A)";
clasohm@0
   287
br (QPair_Int_Vfrom_subset RS subset_trans RS qunivI) 1;
clasohm@0
   288
br (QPair_in_quniv RS qunivD) 2;
clasohm@0
   289
by (REPEAT (assume_tac 1));
clasohm@0
   290
val QPair_Int_Vfrom_in_quniv = result();
clasohm@0
   291
clasohm@0
   292
clasohm@0
   293
(**** "Take-lemma" rules for proving a=b by co-induction ****)
clasohm@0
   294
clasohm@0
   295
(** Unfortunately, the technique used above does not apply here, since
clasohm@0
   296
    the base case appears impossible to prove: it involves an intersection
clasohm@0
   297
    with eclose(X) for arbitrary X.  So a=b is proved by transfinite induction
clasohm@0
   298
    over ALL ordinals, using Vset(i) instead of Vfrom(X,i).
clasohm@0
   299
**)
clasohm@0
   300
clasohm@0
   301
(*Rule for level 0*)
clasohm@0
   302
goal QUniv.thy "a Int Vset(0) <= b";
clasohm@0
   303
by (rtac (Vfrom_0 RS ssubst) 1);
clasohm@0
   304
by (fast_tac ZF_cs 1);
clasohm@0
   305
val Int_Vset_0_subset = result();
clasohm@0
   306
clasohm@0
   307
(*Rule for level succ(i), decreasing it to i*)
clasohm@0
   308
goal QUniv.thy 
clasohm@0
   309
 "!!i. [| a Int Vset(i) <= c;	\
clasohm@0
   310
\         b Int Vset(i) <= d	\
clasohm@0
   311
\      |] ==> <a;b> Int Vset(succ(i))  <=  <c;d>";
clasohm@0
   312
br ([Transset_0 RS QPair_Int_Vfrom_succ_subset, QPair_mono] 
clasohm@0
   313
    MRS subset_trans) 1;
clasohm@0
   314
by (REPEAT (assume_tac 1));
clasohm@0
   315
val QPair_Int_Vset_succ_subset_trans = result();
clasohm@0
   316
clasohm@0
   317
(*Unused; kept as an example.  QInr rule is similar*)
clasohm@0
   318
goalw QUniv.thy [QInl_def] 
clasohm@0
   319
 "!!i. a Int Vset(i) <= b ==> QInl(a) Int Vset(succ(i)) <= QInl(b)";
clasohm@0
   320
be (Int_lower1 RS QPair_Int_Vset_succ_subset_trans) 1;
clasohm@0
   321
val QInl_Int_Vset_succ_subset_trans = result();
clasohm@0
   322
clasohm@0
   323
(*Rule for level i -- preserving the level, not decreasing it*)
clasohm@0
   324
goal QUniv.thy 
clasohm@0
   325
 "!!i. [| a Int Vset(i) <= c;	\
clasohm@0
   326
\         b Int Vset(i) <= d	\
clasohm@0
   327
\      |] ==> <a;b> Int Vset(i)  <=  <c;d>";
clasohm@0
   328
br ([Transset_0 RS QPair_Int_Vfrom_subset, QPair_mono] 
clasohm@0
   329
    MRS subset_trans) 1;
clasohm@0
   330
by (REPEAT (assume_tac 1));
clasohm@0
   331
val QPair_Int_Vset_subset_trans = result();
clasohm@0
   332
clasohm@0
   333
clasohm@0
   334