author  wenzelm 
Thu, 26 Apr 2007 14:24:08 +0200  
changeset 22808  a7daa74e2980 
parent 17782  b3846df9d643 
child 24893  b8ef7afe3a6b 
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 

16417  14 
theory QPair imports Sum func begin 
13285  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 

14854  34 
qsplit :: "[[i, i] => 'a, i] => 'a::{}" (*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" 

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13544
diff
changeset

41 
"QSigma(A,B) == \<Union>x\<in>A. \<Union>y\<in>B(x). {<x;y>}" 
0  42 

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

43 
syntax 
22808  44 
"_QSUM" :: "[idt, i, i] => i" ("(3QSUM _:_./ _)" 10) 
0  45 
translations 
46 
"QSUM x:A. B" => "QSigma(A, %x. B)" 

22808  47 

48 
abbreviation 

49 
qprod (infixr "<*>" 80) where 

50 
"A <*> B == QSigma(A, %_. B)" 

0  51 

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

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

3923  55 

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

58 

59 
QInr :: "i=>i" 

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

61 

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

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

64 

65 

13356  66 
subsection{*Quine ordered pairing*} 
13285  67 

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

69 

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

71 
by (simp add: QPair_def) 

72 

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

74 
apply (simp add: QPair_def) 

75 
apply (rule sum_equal_iff) 

76 
done 

77 

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

79 

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

81 
by blast 

82 

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

84 
by blast 

85 

86 

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

13285  89 

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

91 
by (simp add: QSigma_def) 

92 

93 

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

95 

96 
lemma QSigmaE [elim!]: 

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

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

99 
] ==> P" 

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

102 
lemma QSigmaE2 [elim!]: 

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

104 
by (simp add: QSigma_def) 

105 

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

107 
by blast 

108 

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

110 
by blast 

111 

112 
lemma QSigma_cong: 

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

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

115 
by (simp add: QSigma_def) 

116 

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

118 
by blast 

119 

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

121 
by blast 

122 

123 

13356  124 
subsubsection{*Projections: qfst, qsnd*} 
13285  125 

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

13544  127 
by (simp add: qfst_def) 
13285  128 

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

13544  130 
by (simp add: qsnd_def) 
13285  131 

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

133 
by auto 

134 

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

136 
by auto 

137 

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

139 
by auto 

140 

141 

13356  142 
subsubsection{*Eliminator: qsplit*} 
13285  143 

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

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

146 
by (simp add: qsplit_def) 

147 

148 

149 
lemma qsplit_type [elim!]: 

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

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

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

153 
by auto 

154 

155 
lemma expand_qsplit: 

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

157 
apply (simp add: qsplit_def, auto) 

158 
done 

159 

160 

13356  161 
subsubsection{*qsplit for predicates: result type o*} 
13285  162 

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

164 
by (simp add: qsplit_def) 

165 

166 

167 
lemma qsplitE: 

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

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

170 
] ==> P" 

13356  171 
by (simp add: qsplit_def, auto) 
13285  172 

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

174 
by (simp add: qsplit_def) 

175 

176 

13356  177 
subsubsection{*qconverse*} 
13285  178 

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

180 
by (simp add: qconverse_def, blast) 

181 

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

183 
by (simp add: qconverse_def, blast) 

184 

185 
lemma qconverseE [elim!]: 

186 
"[ yx : qconverse(r); 

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

188 
] ==> P" 

13356  189 
by (simp add: qconverse_def, blast) 
13285  190 

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

192 
by blast 

193 

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

195 
by blast 

196 

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

198 
by blast 

199 

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

201 
by blast 

202 

203 

13356  204 
subsection{*The Quineinspired notion of disjoint sum*} 
13285  205 

206 
lemmas qsum_defs = qsum_def QInl_def QInr_def qcase_def 

207 

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

209 

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

211 
by (simp add: qsum_defs, blast) 

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

212 

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

215 

216 
(** Elimination rules **) 

217 

218 
lemma qsumE [elim!]: 

219 
"[ u: A <+> B; 

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

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

222 
] ==> P" 

13356  223 
by (simp add: qsum_defs, blast) 
13285  224 

225 

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

227 

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

229 
by (simp add: qsum_defs ) 

230 

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

232 
by (simp add: qsum_defs ) 

233 

13823  234 
lemma QInl_QInr_iff [simp]: "QInl(a)=QInr(b) <> False" 
13285  235 
by (simp add: qsum_defs ) 
236 

13823  237 
lemma QInr_QInl_iff [simp]: "QInr(b)=QInl(a) <> False" 
13285  238 
by (simp add: qsum_defs ) 
239 

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

241 
by (simp add: qsum_defs ) 

242 

243 
(*Injection and freeness rules*) 

244 

245 
lemmas QInl_inject = QInl_iff [THEN iffD1, standard] 

246 
lemmas QInr_inject = QInr_iff [THEN iffD1, standard] 

13823  247 
lemmas QInl_neq_QInr = QInl_QInr_iff [THEN iffD1, THEN FalseE, elim!] 
248 
lemmas QInr_neq_QInl = QInr_QInl_iff [THEN iffD1, THEN FalseE, elim!] 

13285  249 

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

251 
by blast 

252 

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

254 
by blast 

255 

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

257 

258 
lemma qsum_iff: 

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

13356  260 
by blast 
13285  261 

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

263 
by blast 

264 

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

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

267 
apply blast 

268 
done 

269 

13356  270 
subsubsection{*Eliminator  qcase*} 
13285  271 

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

273 
by (simp add: qsum_defs ) 

274 

275 

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

277 
by (simp add: qsum_defs ) 

278 

279 
lemma qcase_type: 

280 
"[ u: A <+> B; 

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

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

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

13784  284 
by (simp add: qsum_defs, auto) 
13285  285 

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

287 

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

289 
by blast 

290 

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

292 
by blast 

293 

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

295 
by blast 

0  296 

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

299 

300 

13356  301 
subsubsection{*Monotonicity*} 
13285  302 

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

304 
by (simp add: QPair_def sum_mono) 

305 

306 
lemma QSigma_mono [rule_format]: 

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

308 
by blast 

309 

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

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

312 

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

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

315 

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

317 
by blast 

318 

319 
ML 

320 
{* 

321 
val qsum_defs = thms "qsum_defs"; 

322 

323 
val QPair_empty = thm "QPair_empty"; 

324 
val QPair_iff = thm "QPair_iff"; 

325 
val QPair_inject = thm "QPair_inject"; 

326 
val QPair_inject1 = thm "QPair_inject1"; 

327 
val QPair_inject2 = thm "QPair_inject2"; 

328 
val QSigmaI = thm "QSigmaI"; 

329 
val QSigmaE = thm "QSigmaE"; 

330 
val QSigmaE = thm "QSigmaE"; 

331 
val QSigmaE2 = thm "QSigmaE2"; 

332 
val QSigmaD1 = thm "QSigmaD1"; 

333 
val QSigmaD2 = thm "QSigmaD2"; 

334 
val QSigma_cong = thm "QSigma_cong"; 

335 
val QSigma_empty1 = thm "QSigma_empty1"; 

336 
val QSigma_empty2 = thm "QSigma_empty2"; 

337 
val qfst_conv = thm "qfst_conv"; 

338 
val qsnd_conv = thm "qsnd_conv"; 

339 
val qfst_type = thm "qfst_type"; 

340 
val qsnd_type = thm "qsnd_type"; 

341 
val QPair_qfst_qsnd_eq = thm "QPair_qfst_qsnd_eq"; 

342 
val qsplit = thm "qsplit"; 

343 
val qsplit_type = thm "qsplit_type"; 

344 
val expand_qsplit = thm "expand_qsplit"; 

345 
val qsplitI = thm "qsplitI"; 

346 
val qsplitE = thm "qsplitE"; 

347 
val qsplitD = thm "qsplitD"; 

348 
val qconverseI = thm "qconverseI"; 

349 
val qconverseD = thm "qconverseD"; 

350 
val qconverseE = thm "qconverseE"; 

351 
val qconverse_qconverse = thm "qconverse_qconverse"; 

352 
val qconverse_type = thm "qconverse_type"; 

353 
val qconverse_prod = thm "qconverse_prod"; 

354 
val qconverse_empty = thm "qconverse_empty"; 

355 
val QInlI = thm "QInlI"; 

356 
val QInrI = thm "QInrI"; 

357 
val qsumE = thm "qsumE"; 

358 
val QInl_iff = thm "QInl_iff"; 

359 
val QInr_iff = thm "QInr_iff"; 

360 
val QInl_QInr_iff = thm "QInl_QInr_iff"; 

361 
val QInr_QInl_iff = thm "QInr_QInl_iff"; 

362 
val qsum_empty = thm "qsum_empty"; 

363 
val QInl_inject = thm "QInl_inject"; 

364 
val QInr_inject = thm "QInr_inject"; 

365 
val QInl_neq_QInr = thm "QInl_neq_QInr"; 

366 
val QInr_neq_QInl = thm "QInr_neq_QInl"; 

367 
val QInlD = thm "QInlD"; 

368 
val QInrD = thm "QInrD"; 

369 
val qsum_iff = thm "qsum_iff"; 

370 
val qsum_subset_iff = thm "qsum_subset_iff"; 

371 
val qsum_equal_iff = thm "qsum_equal_iff"; 

372 
val qcase_QInl = thm "qcase_QInl"; 

373 
val qcase_QInr = thm "qcase_QInr"; 

374 
val qcase_type = thm "qcase_type"; 

375 
val Part_QInl = thm "Part_QInl"; 

376 
val Part_QInr = thm "Part_QInr"; 

377 
val Part_QInr2 = thm "Part_QInr2"; 

378 
val Part_qsum_equality = thm "Part_qsum_equality"; 

379 
val QPair_mono = thm "QPair_mono"; 

380 
val QSigma_mono = thm "QSigma_mono"; 

381 
val QInl_mono = thm "QInl_mono"; 

382 
val QInr_mono = thm "QInr_mono"; 

383 
val qsum_mono = thm "qsum_mono"; 

384 
*} 

385 

0  386 
end 