src/ZF/QUniv.ML
author lcp
Fri Sep 17 16:16:38 1993 +0200 (1993-09-17)
changeset 6 8ce8c4d13d4d
parent 0 a5a9c433f639
child 15 6c6d2f6e3185
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.
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))";
lcp@6
   208
by (simp_tac (ZF_ss addsimps [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