author  lcp 
Fri, 19 Nov 1993 11:25:36 +0100  
changeset 129  dc50a4b96d7b 
parent 120  09287f26bfb8 
child 170  590c9d1e0d73 
permissions  rwrr 
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 Quineinspired 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 Quineinspired 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)"; 

129  102 
by (etac ([Transset_eclose RS Transset_univ, PowD] MRS 
103 
Transset_includes_summands RS conjE) 1); 

0  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 "takelemma" ****) 

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 
(**** "Takelemma" 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 

120  293 
(**** "Takelemma" rules for proving a=b by coinduction ****) 
0  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 