author | lcp |
Thu, 30 Sep 1993 10:10:21 +0100 | |
changeset 14 | 1c0926788772 |
parent 6 | 8ce8c4d13d4d |
child 120 | 09287f26bfb8 |
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 |
||
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)"; |
|
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
155 |
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
|
156 |
by (assume_tac 1); |
0 | 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)>"; |
|
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
188 |
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
|
189 |
by (rtac Un_mono 1); |
0 | 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))"; |
|
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
197 |
by (etac ([qunivD, Transset_eclose] MRS Transset_Pair_subset_univ) 1); |
0 | 198 |
val Pair_in_quniv_D = result(); |
199 |
||
200 |
goal QUniv.thy "a*b Int quniv(A) = a*b Int univ(eclose(A))"; |
|
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
201 |
by (rtac equalityI 1); |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
202 |
by (rtac ([subset_refl, univ_eclose_subset_quniv] MRS Int_mono) 2); |
0 | 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))"; |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
208 |
by (simp_tac (ZF_ss addsimps [Int_Un_distrib, product_Int_quniv_eq]) 1); |
0 | 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))"; |
|
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
214 |
by (rtac (Transset_eclose RS Transset_univ RS Transset_Pow) 1); |
0 | 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)"; |
|
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
221 |
by (rtac (univ_Int_Vfrom_subset RS qunivI) 1); |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
222 |
by (rtac (aprem RS qunivD) 1); |
0 | 223 |
by (rtac (Transset_quniv RS Transset_eclose_eq_arg RS ssubst) 1); |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
224 |
by (etac (iprem RS qunivD) 1); |
0 | 225 |
val quniv_Int_Vfrom = result(); |
226 |
||
227 |
(** Rules for level 0 **) |
|
228 |
||
229 |
goal QUniv.thy "<a;b> Int quniv(A) : quniv(A)"; |
|
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
230 |
by (rtac (QPair_Int_quniv_eq RS ssubst) 1); |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
231 |
by (rtac (Int_lower2 RS qunivI) 1); |
0 | 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)"; |
|
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
236 |
by (rtac QPair_Int_quniv_in_quniv 1); |
0 | 237 |
val QInl_Int_quniv_in_quniv = result(); |
238 |
||
239 |
goal QUniv.thy "!!a A X. a : quniv(A) ==> a Int X : quniv(A)"; |
|
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
240 |
by (etac ([Int_lower1, qunivD] MRS subset_trans RS qunivI) 1); |
0 | 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)"; |
|
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
255 |
by (rtac (QPair_Int_Vfrom_succ_subset RS subset_trans RS qunivI) 1); |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
256 |
by (rtac (QPair_in_quniv RS qunivD) 2); |
0 | 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)"; |
|
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
270 |
by (rtac QPair_Int_Vfrom_succ_in_quniv 1); |
0 | 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)>"; |
|
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
279 |
by (etac (Transset_Vfrom RS Transset_sum_Int_subset) 1); |
0 | 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)"; |
|
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
287 |
by (rtac (QPair_Int_Vfrom_subset RS subset_trans RS qunivI) 1); |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
288 |
by (rtac (QPair_in_quniv RS qunivD) 2); |
0 | 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>"; |
|
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
312 |
by (rtac ([Transset_0 RS QPair_Int_Vfrom_succ_subset, QPair_mono] |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
313 |
MRS subset_trans) 1); |
0 | 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)"; |
|
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
320 |
by (etac (Int_lower1 RS QPair_Int_Vset_succ_subset_trans) 1); |
0 | 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>"; |
|
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
328 |
by (rtac ([Transset_0 RS QPair_Int_Vfrom_subset, QPair_mono] |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
329 |
MRS subset_trans) 1); |
0 | 330 |
by (REPEAT (assume_tac 1)); |
331 |
val QPair_Int_Vset_subset_trans = result(); |
|
332 |
||
333 |
||
334 |