author  paulson 
Sun, 14 Jul 2002 15:14:43 +0200  
changeset 13356  c9cfe1638bf2 
parent 13285  28d1823ce0f2 
child 13357  6f54e992777e 
permissions  rwrr 
1478  1 
(* Title: ZF/qpair.thy 
0  2 
ID: $Id$ 
1478  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1993 University of Cambridge 
5 

13285  6 
Many proofs are borrowed from pair.thy and sum.thy 
7 

8 
Do we EVER have rank(a) < rank(<a;b>) ? Perhaps if the latter rank 

9 
is not a limit ordinal? 

0  10 
*) 
11 

13356  12 
header{*QuineInspired Ordered Pairs and Disjoint Sums*} 
13 

13285  14 
theory QPair = Sum + mono: 
15 

13356  16 
text{*For nonwellfounded data 
17 
structures in ZF. Does not precisely follow Quine's construction. Thanks 

18 
to Thomas Forster for suggesting this approach! 

19 

20 
W. V. Quine, On Ordered Pairs and Relations, in Selected Logic Papers, 

21 
1966. 

22 
*} 

23 

13285  24 
constdefs 
25 
QPair :: "[i, i] => i" ("<(_;/ _)>") 

26 
"<a;b> == a+b" 

3923  27 

13285  28 
qfst :: "i => i" 
29 
"qfst(p) == THE a. EX b. p=<a;b>" 

30 

31 
qsnd :: "i => i" 

32 
"qsnd(p) == THE b. EX a. p=<a;b>" 

33 

13220  34 
qsplit :: "[[i, i] => 'a, i] => 'a::logic" (*for patternmatching*) 
13285  35 
"qsplit(c,p) == c(qfst(p), qsnd(p))" 
0  36 

13285  37 
qconverse :: "i => i" 
38 
"qconverse(r) == {z. w:r, EX x y. w=<x;y> & z=<y;x>}" 

39 

40 
QSigma :: "[i, i => i] => i" 

41 
"QSigma(A,B) == UN x:A. UN y:B(x). {<x;y>}" 

0  42 

929
137035296ad6
Moved declarations of @QSUM and <*> to a syntax section.
lcp
parents:
753
diff
changeset

43 
syntax 
13220  44 
"@QSUM" :: "[idt, i, i] => i" ("(3QSUM _:_./ _)" 10) 
45 
"<*>" :: "[i, i] => i" (infixr 80) 

929
137035296ad6
Moved declarations of @QSUM and <*> to a syntax section.
lcp
parents:
753
diff
changeset

46 

0  47 
translations 
48 
"QSUM x:A. B" => "QSigma(A, %x. B)" 

44  49 
"A <*> B" => "QSigma(A, _K(B))" 
0  50 

13285  51 
constdefs 
52 
qsum :: "[i,i]=>i" (infixr "<+>" 65) 

53 
"A <+> B == ({0} <*> A) Un ({1} <*> B)" 

3923  54 

13285  55 
QInl :: "i=>i" 
56 
"QInl(a) == <0;a>" 

57 

58 
QInr :: "i=>i" 

59 
"QInr(b) == <1;b>" 

60 

61 
qcase :: "[i=>i, i=>i, i]=>i" 

62 
"qcase(c,d) == qsplit(%y z. cond(y, d(z), c(z)))" 

63 

64 

65 
print_translation {* [("QSigma", dependent_tr' ("@QSUM", "op <*>"))] *} 

66 

67 

13356  68 
subsection{*Quine ordered pairing*} 
13285  69 

70 
(** Lemmas for showing that <a;b> uniquely determines a and b **) 

71 

72 
lemma QPair_empty [simp]: "<0;0> = 0" 

73 
by (simp add: QPair_def) 

74 

75 
lemma QPair_iff [simp]: "<a;b> = <c;d> <> a=c & b=d" 

76 
apply (simp add: QPair_def) 

77 
apply (rule sum_equal_iff) 

78 
done 

79 

80 
lemmas QPair_inject = QPair_iff [THEN iffD1, THEN conjE, standard, elim!] 

81 

82 
lemma QPair_inject1: "<a;b> = <c;d> ==> a=c" 

83 
by blast 

84 

85 
lemma QPair_inject2: "<a;b> = <c;d> ==> b=d" 

86 
by blast 

87 

88 

13356  89 
subsubsection{*QSigma: Disjoint union of a family of sets 
90 
Generalizes Cartesian product*} 

13285  91 

92 
lemma QSigmaI [intro!]: "[ a:A; b:B(a) ] ==> <a;b> : QSigma(A,B)" 

93 
by (simp add: QSigma_def) 

94 

95 

96 
(*The general elimination rule*) 

97 
lemma QSigmaE: 

98 
"[ c: QSigma(A,B); 

99 
!!x y.[ x:A; y:B(x); c=<x;y> ] ==> P 

100 
] ==> P" 

13356  101 
by (simp add: QSigma_def, blast) 
13285  102 

103 
(** Elimination rules for <a;b>:A*B  introducing no eigenvariables **) 

104 

105 
lemma QSigmaE [elim!]: 

106 
"[ c: QSigma(A,B); 

107 
!!x y.[ x:A; y:B(x); c=<x;y> ] ==> P 

108 
] ==> P" 

13356  109 
by (simp add: QSigma_def, blast) 
13285  110 

111 
lemma QSigmaE2 [elim!]: 

112 
"[ <a;b>: QSigma(A,B); [ a:A; b:B(a) ] ==> P ] ==> P" 

113 
by (simp add: QSigma_def) 

114 

115 
lemma QSigmaD1: "<a;b> : QSigma(A,B) ==> a : A" 

116 
by blast 

117 

118 
lemma QSigmaD2: "<a;b> : QSigma(A,B) ==> b : B(a)" 

119 
by blast 

120 

121 
lemma QSigma_cong: 

122 
"[ A=A'; !!x. x:A' ==> B(x)=B'(x) ] ==> 

123 
QSigma(A,B) = QSigma(A',B')" 

124 
by (simp add: QSigma_def) 

125 

126 
lemma QSigma_empty1 [simp]: "QSigma(0,B) = 0" 

127 
by blast 

128 

129 
lemma QSigma_empty2 [simp]: "A <*> 0 = 0" 

130 
by blast 

131 

132 

13356  133 
subsubsection{*Projections: qfst, qsnd*} 
13285  134 

135 
lemma qfst_conv [simp]: "qfst(<a;b>) = a" 

136 
by (simp add: qfst_def, blast) 

137 

138 
lemma qsnd_conv [simp]: "qsnd(<a;b>) = b" 

139 
by (simp add: qsnd_def, blast) 

140 

141 
lemma qfst_type [TC]: "p:QSigma(A,B) ==> qfst(p) : A" 

142 
by auto 

143 

144 
lemma qsnd_type [TC]: "p:QSigma(A,B) ==> qsnd(p) : B(qfst(p))" 

145 
by auto 

146 

147 
lemma QPair_qfst_qsnd_eq: "a: QSigma(A,B) ==> <qfst(a); qsnd(a)> = a" 

148 
by auto 

149 

150 

13356  151 
subsubsection{*Eliminator: qsplit*} 
13285  152 

153 
(*A METAequality, so that it applies to higher types as well...*) 

154 
lemma qsplit [simp]: "qsplit(%x y. c(x,y), <a;b>) == c(a,b)" 

155 
by (simp add: qsplit_def) 

156 

157 

158 
lemma qsplit_type [elim!]: 

159 
"[ p:QSigma(A,B); 

160 
!!x y.[ x:A; y:B(x) ] ==> c(x,y):C(<x;y>) 

161 
] ==> qsplit(%x y. c(x,y), p) : C(p)" 

162 
by auto 

163 

164 
lemma expand_qsplit: 

165 
"u: A<*>B ==> R(qsplit(c,u)) <> (ALL x:A. ALL y:B. u = <x;y> > R(c(x,y)))" 

166 
apply (simp add: qsplit_def, auto) 

167 
done 

168 

169 

13356  170 
subsubsection{*qsplit for predicates: result type o*} 
13285  171 

172 
lemma qsplitI: "R(a,b) ==> qsplit(R, <a;b>)" 

173 
by (simp add: qsplit_def) 

174 

175 

176 
lemma qsplitE: 

177 
"[ qsplit(R,z); z:QSigma(A,B); 

178 
!!x y. [ z = <x;y>; R(x,y) ] ==> P 

179 
] ==> P" 

13356  180 
by (simp add: qsplit_def, auto) 
13285  181 

182 
lemma qsplitD: "qsplit(R,<a;b>) ==> R(a,b)" 

183 
by (simp add: qsplit_def) 

184 

185 

13356  186 
subsubsection{*qconverse*} 
13285  187 

188 
lemma qconverseI [intro!]: "<a;b>:r ==> <b;a>:qconverse(r)" 

189 
by (simp add: qconverse_def, blast) 

190 

191 
lemma qconverseD [elim!]: "<a;b> : qconverse(r) ==> <b;a> : r" 

192 
by (simp add: qconverse_def, blast) 

193 

194 
lemma qconverseE [elim!]: 

195 
"[ yx : qconverse(r); 

196 
!!x y. [ yx=<y;x>; <x;y>:r ] ==> P 

197 
] ==> P" 

13356  198 
by (simp add: qconverse_def, blast) 
13285  199 

200 
lemma qconverse_qconverse: "r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r" 

201 
by blast 

202 

203 
lemma qconverse_type: "r <= A <*> B ==> qconverse(r) <= B <*> A" 

204 
by blast 

205 

206 
lemma qconverse_prod: "qconverse(A <*> B) = B <*> A" 

207 
by blast 

208 

209 
lemma qconverse_empty: "qconverse(0) = 0" 

210 
by blast 

211 

212 

13356  213 
subsection{*The Quineinspired notion of disjoint sum*} 
13285  214 

215 
lemmas qsum_defs = qsum_def QInl_def QInr_def qcase_def 

216 

217 
(** Introduction rules for the injections **) 

218 

219 
lemma QInlI [intro!]: "a : A ==> QInl(a) : A <+> B" 

220 
by (simp add: qsum_defs, blast) 

1097
01379c46ad2d
Changed definitions so that qsplit is now defined in terms of
lcp
parents:
929
diff
changeset

221 

13285  222 
lemma QInrI [intro!]: "b : B ==> QInr(b) : A <+> B" 
223 
by (simp add: qsum_defs, blast) 

224 

225 
(** Elimination rules **) 

226 

227 
lemma qsumE [elim!]: 

228 
"[ u: A <+> B; 

229 
!!x. [ x:A; u=QInl(x) ] ==> P; 

230 
!!y. [ y:B; u=QInr(y) ] ==> P 

231 
] ==> P" 

13356  232 
by (simp add: qsum_defs, blast) 
13285  233 

234 

235 
(** Injection and freeness equivalences, for rewriting **) 

236 

237 
lemma QInl_iff [iff]: "QInl(a)=QInl(b) <> a=b" 

238 
by (simp add: qsum_defs ) 

239 

240 
lemma QInr_iff [iff]: "QInr(a)=QInr(b) <> a=b" 

241 
by (simp add: qsum_defs ) 

242 

243 
lemma QInl_QInr_iff [iff]: "QInl(a)=QInr(b) <> False" 

244 
by (simp add: qsum_defs ) 

245 

246 
lemma QInr_QInl_iff [iff]: "QInr(b)=QInl(a) <> False" 

247 
by (simp add: qsum_defs ) 

248 

249 
lemma qsum_empty [simp]: "0<+>0 = 0" 

250 
by (simp add: qsum_defs ) 

251 

252 
(*Injection and freeness rules*) 

253 

254 
lemmas QInl_inject = QInl_iff [THEN iffD1, standard] 

255 
lemmas QInr_inject = QInr_iff [THEN iffD1, standard] 

256 
lemmas QInl_neq_QInr = QInl_QInr_iff [THEN iffD1, THEN FalseE] 

257 
lemmas QInr_neq_QInl = QInr_QInl_iff [THEN iffD1, THEN FalseE] 

258 

259 
lemma QInlD: "QInl(a): A<+>B ==> a: A" 

260 
by blast 

261 

262 
lemma QInrD: "QInr(b): A<+>B ==> b: B" 

263 
by blast 

264 

265 
(** <+> is itself injective... who cares?? **) 

266 

267 
lemma qsum_iff: 

268 
"u: A <+> B <> (EX x. x:A & u=QInl(x))  (EX y. y:B & u=QInr(y))" 

13356  269 
by blast 
13285  270 

271 
lemma qsum_subset_iff: "A <+> B <= C <+> D <> A<=C & B<=D" 

272 
by blast 

273 

274 
lemma qsum_equal_iff: "A <+> B = C <+> D <> A=C & B=D" 

275 
apply (simp (no_asm) add: extension qsum_subset_iff) 

276 
apply blast 

277 
done 

278 

13356  279 
subsubsection{*Eliminator  qcase*} 
13285  280 

281 
lemma qcase_QInl [simp]: "qcase(c, d, QInl(a)) = c(a)" 

282 
by (simp add: qsum_defs ) 

283 

284 

285 
lemma qcase_QInr [simp]: "qcase(c, d, QInr(b)) = d(b)" 

286 
by (simp add: qsum_defs ) 

287 

288 
lemma qcase_type: 

289 
"[ u: A <+> B; 

290 
!!x. x: A ==> c(x): C(QInl(x)); 

291 
!!y. y: B ==> d(y): C(QInr(y)) 

292 
] ==> qcase(c,d,u) : C(u)" 

13356  293 
by (simp add: qsum_defs , auto) 
13285  294 

295 
(** Rules for the Part primitive **) 

296 

297 
lemma Part_QInl: "Part(A <+> B,QInl) = {QInl(x). x: A}" 

298 
by blast 

299 

300 
lemma Part_QInr: "Part(A <+> B,QInr) = {QInr(y). y: B}" 

301 
by blast 

302 

303 
lemma Part_QInr2: "Part(A <+> B, %x. QInr(h(x))) = {QInr(y). y: Part(B,h)}" 

304 
by blast 

0  305 

13285  306 
lemma Part_qsum_equality: "C <= A <+> B ==> Part(C,QInl) Un Part(C,QInr) = C" 
307 
by blast 

308 

309 

13356  310 
subsubsection{*Monotonicity*} 
13285  311 

312 
lemma QPair_mono: "[ a<=c; b<=d ] ==> <a;b> <= <c;d>" 

313 
by (simp add: QPair_def sum_mono) 

314 

315 
lemma QSigma_mono [rule_format]: 

316 
"[ A<=C; ALL x:A. B(x) <= D(x) ] ==> QSigma(A,B) <= QSigma(C,D)" 

317 
by blast 

318 

319 
lemma QInl_mono: "a<=b ==> QInl(a) <= QInl(b)" 

320 
by (simp add: QInl_def subset_refl [THEN QPair_mono]) 

321 

322 
lemma QInr_mono: "a<=b ==> QInr(a) <= QInr(b)" 

323 
by (simp add: QInr_def subset_refl [THEN QPair_mono]) 

324 

325 
lemma qsum_mono: "[ A<=C; B<=D ] ==> A <+> B <= C <+> D" 

326 
by blast 

327 

328 
ML 

329 
{* 

330 
val qsum_defs = thms "qsum_defs"; 

331 

332 
val QPair_empty = thm "QPair_empty"; 

333 
val QPair_iff = thm "QPair_iff"; 

334 
val QPair_inject = thm "QPair_inject"; 

335 
val QPair_inject1 = thm "QPair_inject1"; 

336 
val QPair_inject2 = thm "QPair_inject2"; 

337 
val QSigmaI = thm "QSigmaI"; 

338 
val QSigmaE = thm "QSigmaE"; 

339 
val QSigmaE = thm "QSigmaE"; 

340 
val QSigmaE2 = thm "QSigmaE2"; 

341 
val QSigmaD1 = thm "QSigmaD1"; 

342 
val QSigmaD2 = thm "QSigmaD2"; 

343 
val QSigma_cong = thm "QSigma_cong"; 

344 
val QSigma_empty1 = thm "QSigma_empty1"; 

345 
val QSigma_empty2 = thm "QSigma_empty2"; 

346 
val qfst_conv = thm "qfst_conv"; 

347 
val qsnd_conv = thm "qsnd_conv"; 

348 
val qfst_type = thm "qfst_type"; 

349 
val qsnd_type = thm "qsnd_type"; 

350 
val QPair_qfst_qsnd_eq = thm "QPair_qfst_qsnd_eq"; 

351 
val qsplit = thm "qsplit"; 

352 
val qsplit_type = thm "qsplit_type"; 

353 
val expand_qsplit = thm "expand_qsplit"; 

354 
val qsplitI = thm "qsplitI"; 

355 
val qsplitE = thm "qsplitE"; 

356 
val qsplitD = thm "qsplitD"; 

357 
val qconverseI = thm "qconverseI"; 

358 
val qconverseD = thm "qconverseD"; 

359 
val qconverseE = thm "qconverseE"; 

360 
val qconverse_qconverse = thm "qconverse_qconverse"; 

361 
val qconverse_type = thm "qconverse_type"; 

362 
val qconverse_prod = thm "qconverse_prod"; 

363 
val qconverse_empty = thm "qconverse_empty"; 

364 
val QInlI = thm "QInlI"; 

365 
val QInrI = thm "QInrI"; 

366 
val qsumE = thm "qsumE"; 

367 
val QInl_iff = thm "QInl_iff"; 

368 
val QInr_iff = thm "QInr_iff"; 

369 
val QInl_QInr_iff = thm "QInl_QInr_iff"; 

370 
val QInr_QInl_iff = thm "QInr_QInl_iff"; 

371 
val qsum_empty = thm "qsum_empty"; 

372 
val QInl_inject = thm "QInl_inject"; 

373 
val QInr_inject = thm "QInr_inject"; 

374 
val QInl_neq_QInr = thm "QInl_neq_QInr"; 

375 
val QInr_neq_QInl = thm "QInr_neq_QInl"; 

376 
val QInlD = thm "QInlD"; 

377 
val QInrD = thm "QInrD"; 

378 
val qsum_iff = thm "qsum_iff"; 

379 
val qsum_subset_iff = thm "qsum_subset_iff"; 

380 
val qsum_equal_iff = thm "qsum_equal_iff"; 

381 
val qcase_QInl = thm "qcase_QInl"; 

382 
val qcase_QInr = thm "qcase_QInr"; 

383 
val qcase_type = thm "qcase_type"; 

384 
val Part_QInl = thm "Part_QInl"; 

385 
val Part_QInr = thm "Part_QInr"; 

386 
val Part_QInr2 = thm "Part_QInr2"; 

387 
val Part_qsum_equality = thm "Part_qsum_equality"; 

388 
val QPair_mono = thm "QPair_mono"; 

389 
val QSigma_mono = thm "QSigma_mono"; 

390 
val QInl_mono = thm "QInl_mono"; 

391 
val QInr_mono = thm "QInr_mono"; 

392 
val qsum_mono = thm "qsum_mono"; 

393 
*} 

394 

0  395 
end 
396 