author | paulson |
Fri, 11 Aug 2000 13:26:40 +0200 | |
changeset 9577 | 9e66e8ed8237 |
parent 170 | 590c9d1e0d73 |
permissions | -rw-r--r-- |
0 | 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)"; |
|
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
15 |
by (etac PowI 1); |
0 | 16 |
val qunivI = result(); |
17 |
||
18 |
goalw QUniv.thy [quniv_def] |
|
19 |
"!!X A. X : quniv(A) ==> X <= univ(eclose(A))"; |
|
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
20 |
by (etac PowD 1); |
0 | 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 |
||
170
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
34 |
(*Key property for proving A_subset_quniv; requires eclose in def of quniv*) |
0 | 35 |
goal QUniv.thy "univ(A) <= quniv(A)"; |
36 |
by (rtac (arg_subset_eclose RS univ_mono RS subset_trans) 1); |
|
37 |
by (rtac univ_eclose_subset_quniv 1); |
|
38 |
val univ_subset_quniv = result(); |
|
39 |
||
40 |
val univ_into_quniv = standard (univ_subset_quniv RS subsetD); |
|
41 |
||
42 |
goalw QUniv.thy [quniv_def] "Pow(univ(A)) <= quniv(A)"; |
|
43 |
by (rtac (arg_subset_eclose RS univ_mono RS Pow_mono) 1); |
|
44 |
val Pow_univ_subset_quniv = result(); |
|
45 |
||
46 |
val univ_subset_into_quniv = standard |
|
47 |
(PowI RS (Pow_univ_subset_quniv RS subsetD)); |
|
48 |
||
49 |
val zero_in_quniv = standard (zero_in_univ RS univ_into_quniv); |
|
50 |
val one_in_quniv = standard (one_in_univ RS univ_into_quniv); |
|
51 |
val two_in_quniv = standard (two_in_univ RS univ_into_quniv); |
|
52 |
||
53 |
val A_subset_quniv = standard |
|
54 |
([A_subset_univ, univ_subset_quniv] MRS subset_trans); |
|
55 |
||
56 |
val A_into_quniv = A_subset_quniv RS subsetD; |
|
57 |
||
58 |
(*** univ(A) closure for Quine-inspired pairs and injections ***) |
|
59 |
||
60 |
(*Quine ordered pairs*) |
|
61 |
goalw QUniv.thy [QPair_def] |
|
62 |
"!!A a. [| a <= univ(A); b <= univ(A) |] ==> <a;b> <= univ(A)"; |
|
63 |
by (REPEAT (ares_tac [sum_subset_univ] 1)); |
|
64 |
val QPair_subset_univ = result(); |
|
65 |
||
66 |
(** Quine disjoint sum **) |
|
67 |
||
68 |
goalw QUniv.thy [QInl_def] "!!A a. a <= univ(A) ==> QInl(a) <= univ(A)"; |
|
69 |
by (etac (empty_subsetI RS QPair_subset_univ) 1); |
|
70 |
val QInl_subset_univ = result(); |
|
71 |
||
72 |
val naturals_subset_nat = |
|
73 |
rewrite_rule [Transset_def] (Ord_nat RS Ord_is_Transset) |
|
74 |
RS bspec; |
|
75 |
||
76 |
val naturals_subset_univ = |
|
77 |
[naturals_subset_nat, nat_subset_univ] MRS subset_trans; |
|
78 |
||
79 |
goalw QUniv.thy [QInr_def] "!!A a. a <= univ(A) ==> QInr(a) <= univ(A)"; |
|
80 |
by (etac (nat_1I RS naturals_subset_univ RS QPair_subset_univ) 1); |
|
81 |
val QInr_subset_univ = result(); |
|
82 |
||
83 |
(*** Closure for Quine-inspired products and sums ***) |
|
84 |
||
85 |
(*Quine ordered pairs*) |
|
86 |
goalw QUniv.thy [quniv_def,QPair_def] |
|
87 |
"!!A a. [| a: quniv(A); b: quniv(A) |] ==> <a;b> : quniv(A)"; |
|
88 |
by (REPEAT (dtac PowD 1)); |
|
89 |
by (REPEAT (ares_tac [PowI, sum_subset_univ] 1)); |
|
90 |
val QPair_in_quniv = result(); |
|
91 |
||
92 |
goal QUniv.thy "quniv(A) <*> quniv(A) <= quniv(A)"; |
|
93 |
by (REPEAT (ares_tac [subsetI, QPair_in_quniv] 1 |
|
94 |
ORELSE eresolve_tac [QSigmaE, ssubst] 1)); |
|
95 |
val QSigma_quniv = result(); |
|
96 |
||
97 |
val QSigma_subset_quniv = standard |
|
98 |
(QSigma_mono RS (QSigma_quniv RSN (2,subset_trans))); |
|
99 |
||
100 |
(*The opposite inclusion*) |
|
101 |
goalw QUniv.thy [quniv_def,QPair_def] |
|
102 |
"!!A a b. <a;b> : quniv(A) ==> a: quniv(A) & b: quniv(A)"; |
|
129 | 103 |
by (etac ([Transset_eclose RS Transset_univ, PowD] MRS |
104 |
Transset_includes_summands RS conjE) 1); |
|
0 | 105 |
by (REPEAT (ares_tac [conjI,PowI] 1)); |
106 |
val quniv_QPair_D = result(); |
|
107 |
||
108 |
val quniv_QPair_E = standard (quniv_QPair_D RS conjE); |
|
109 |
||
110 |
goal QUniv.thy "<a;b> : quniv(A) <-> a: quniv(A) & b: quniv(A)"; |
|
111 |
by (REPEAT (ares_tac [iffI, QPair_in_quniv, quniv_QPair_D] 1 |
|
112 |
ORELSE etac conjE 1)); |
|
113 |
val quniv_QPair_iff = result(); |
|
114 |
||
115 |
||
116 |
(** Quine disjoint sum **) |
|
117 |
||
118 |
goalw QUniv.thy [QInl_def] "!!A a. a: quniv(A) ==> QInl(a) : quniv(A)"; |
|
119 |
by (REPEAT (ares_tac [zero_in_quniv,QPair_in_quniv] 1)); |
|
120 |
val QInl_in_quniv = result(); |
|
121 |
||
122 |
goalw QUniv.thy [QInr_def] "!!A b. b: quniv(A) ==> QInr(b) : quniv(A)"; |
|
123 |
by (REPEAT (ares_tac [one_in_quniv, QPair_in_quniv] 1)); |
|
124 |
val QInr_in_quniv = result(); |
|
125 |
||
126 |
goal QUniv.thy "quniv(C) <+> quniv(C) <= quniv(C)"; |
|
127 |
by (REPEAT (ares_tac [subsetI, QInl_in_quniv, QInr_in_quniv] 1 |
|
128 |
ORELSE eresolve_tac [qsumE, ssubst] 1)); |
|
129 |
val qsum_quniv = result(); |
|
130 |
||
131 |
val qsum_subset_quniv = standard |
|
132 |
(qsum_mono RS (qsum_quniv RSN (2,subset_trans))); |
|
133 |
||
134 |
(*** The natural numbers ***) |
|
135 |
||
136 |
val nat_subset_quniv = standard |
|
137 |
([nat_subset_univ, univ_subset_quniv] MRS subset_trans); |
|
138 |
||
139 |
(* n:nat ==> n:quniv(A) *) |
|
140 |
val nat_into_quniv = standard (nat_subset_quniv RS subsetD); |
|
141 |
||
142 |
val bool_subset_quniv = standard |
|
143 |
([bool_subset_univ, univ_subset_quniv] MRS subset_trans); |
|
144 |
||
145 |
val bool_into_quniv = standard (bool_subset_quniv RS subsetD); |
|
146 |
||
147 |
||
148 |
(**** Properties of Vfrom analogous to the "take-lemma" ****) |
|
149 |
||
150 |
(*** Intersecting a*b with Vfrom... ***) |
|
151 |
||
152 |
(*This version says a, b exist one level down, in the smaller set Vfrom(X,i)*) |
|
153 |
goal Univ.thy |
|
154 |
"!!X. [| {a,b} : Vfrom(X,succ(i)); Transset(X) |] ==> \ |
|
155 |
\ a: Vfrom(X,i) & b: Vfrom(X,i)"; |
|
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
156 |
by (dtac (Transset_Vfrom_succ RS equalityD1 RS subsetD RS PowD) 1); |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
157 |
by (assume_tac 1); |
0 | 158 |
by (fast_tac ZF_cs 1); |
159 |
val doubleton_in_Vfrom_D = result(); |
|
160 |
||
161 |
(*This weaker version says a, b exist at the same level*) |
|
162 |
val Vfrom_doubleton_D = standard (Transset_Vfrom RS Transset_doubleton_D); |
|
163 |
||
164 |
(** Using only the weaker theorem would prove <a,b> : Vfrom(X,i) |
|
165 |
implies a, b : Vfrom(X,i), which is useless for induction. |
|
166 |
Using only the stronger theorem would prove <a,b> : Vfrom(X,succ(succ(i))) |
|
167 |
implies a, b : Vfrom(X,i), leaving the succ(i) case untreated. |
|
168 |
The combination gives a reduction by precisely one level, which is |
|
169 |
most convenient for proofs. |
|
170 |
**) |
|
171 |
||
172 |
goalw Univ.thy [Pair_def] |
|
173 |
"!!X. [| <a,b> : Vfrom(X,succ(i)); Transset(X) |] ==> \ |
|
174 |
\ a: Vfrom(X,i) & b: Vfrom(X,i)"; |
|
175 |
by (fast_tac (ZF_cs addSDs [doubleton_in_Vfrom_D, Vfrom_doubleton_D]) 1); |
|
176 |
val Pair_in_Vfrom_D = result(); |
|
177 |
||
178 |
goal Univ.thy |
|
179 |
"!!X. Transset(X) ==> \ |
|
180 |
\ (a*b) Int Vfrom(X, succ(i)) <= (a Int Vfrom(X,i)) * (b Int Vfrom(X,i))"; |
|
181 |
by (fast_tac (ZF_cs addSDs [Pair_in_Vfrom_D]) 1); |
|
182 |
val product_Int_Vfrom_subset = result(); |
|
183 |
||
184 |
(*** Intersecting <a;b> with Vfrom... ***) |
|
185 |
||
186 |
goalw QUniv.thy [QPair_def,sum_def] |
|
187 |
"!!X. Transset(X) ==> \ |
|
188 |
\ <a;b> Int Vfrom(X, succ(i)) <= <a Int Vfrom(X,i); b Int Vfrom(X,i)>"; |
|
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
189 |
by (rtac (Int_Un_distrib RS ssubst) 1); |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
190 |
by (rtac Un_mono 1); |
0 | 191 |
by (REPEAT (ares_tac [product_Int_Vfrom_subset RS subset_trans, |
192 |
[Int_lower1, subset_refl] MRS Sigma_mono] 1)); |
|
193 |
val QPair_Int_Vfrom_succ_subset = result(); |
|
194 |
||
170
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
195 |
(**** "Take-lemma" rules for proving a=b by coinduction and c: quniv(A) ****) |
0 | 196 |
|
170
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
197 |
(*Rule for level i -- preserving the level, not decreasing it*) |
0 | 198 |
|
199 |
goalw QUniv.thy [QPair_def] |
|
200 |
"!!X. Transset(X) ==> \ |
|
201 |
\ <a;b> Int Vfrom(X,i) <= <a Int Vfrom(X,i); b Int Vfrom(X,i)>"; |
|
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
202 |
by (etac (Transset_Vfrom RS Transset_sum_Int_subset) 1); |
0 | 203 |
val QPair_Int_Vfrom_subset = result(); |
204 |
||
170
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
205 |
(*[| a Int Vset(i) <= c; b Int Vset(i) <= d |] ==> <a;b> Int Vset(i) <= <c;d>*) |
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
206 |
val QPair_Int_Vset_subset_trans = standard |
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
207 |
([Transset_0 RS QPair_Int_Vfrom_subset, QPair_mono] MRS subset_trans); |
0 | 208 |
|
170
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
209 |
goal QUniv.thy |
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
210 |
"!!i. [| Ord(i) \ |
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
211 |
\ |] ==> <a;b> Int Vset(i) <= (UN j:i. <a Int Vset(j); b Int Vset(j)>)"; |
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
212 |
by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac); |
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
213 |
(*0 case*) |
0 | 214 |
by (rtac (Vfrom_0 RS ssubst) 1); |
215 |
by (fast_tac ZF_cs 1); |
|
170
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
216 |
(*succ(j) case*) |
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
217 |
by (rtac (Transset_0 RS QPair_Int_Vfrom_succ_subset RS subset_trans) 1); |
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
218 |
by (rtac (succI1 RS UN_upper) 1); |
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
219 |
(*Limit(i) case*) |
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
220 |
by (asm_simp_tac (ZF_ss addsimps [Limit_Vfrom_eq, Int_UN_distrib, subset_refl, |
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
221 |
UN_mono, QPair_Int_Vset_subset_trans]) 1); |
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
222 |
val QPair_Int_Vset_subset_UN = result(); |