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