author | obua |
Thu, 16 Feb 2006 04:17:19 +0100 | |
changeset 19067 | c0321d7d6b3d |
parent 17782 | b3846df9d643 |
child 22808 | a7daa74e2980 |
permissions | -rw-r--r-- |
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{*Quine-Inspired Ordered Pairs and Disjoint Sums*} |
13 |
||
16417 | 14 |
theory QPair imports Sum func begin |
13285 | 15 |
|
13356 | 16 |
text{*For non-well-founded 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 pattern-matching*) |
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 |
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)" |
|
17782 | 49 |
"A <*> B" => "QSigma(A, %_. 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 |
(** Elimination rules for <a;b>:A*B -- introducing no eigenvariables **) |
|
97 |
||
98 |
lemma QSigmaE [elim!]: |
|
99 |
"[| c: QSigma(A,B); |
|
100 |
!!x y.[| x:A; y:B(x); c=<x;y> |] ==> P |
|
101 |
|] ==> P" |
|
13356 | 102 |
by (simp add: QSigma_def, blast) |
13285 | 103 |
|
104 |
lemma QSigmaE2 [elim!]: |
|
105 |
"[| <a;b>: QSigma(A,B); [| a:A; b:B(a) |] ==> P |] ==> P" |
|
106 |
by (simp add: QSigma_def) |
|
107 |
||
108 |
lemma QSigmaD1: "<a;b> : QSigma(A,B) ==> a : A" |
|
109 |
by blast |
|
110 |
||
111 |
lemma QSigmaD2: "<a;b> : QSigma(A,B) ==> b : B(a)" |
|
112 |
by blast |
|
113 |
||
114 |
lemma QSigma_cong: |
|
115 |
"[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> |
|
116 |
QSigma(A,B) = QSigma(A',B')" |
|
117 |
by (simp add: QSigma_def) |
|
118 |
||
119 |
lemma QSigma_empty1 [simp]: "QSigma(0,B) = 0" |
|
120 |
by blast |
|
121 |
||
122 |
lemma QSigma_empty2 [simp]: "A <*> 0 = 0" |
|
123 |
by blast |
|
124 |
||
125 |
||
13356 | 126 |
subsubsection{*Projections: qfst, qsnd*} |
13285 | 127 |
|
128 |
lemma qfst_conv [simp]: "qfst(<a;b>) = a" |
|
13544 | 129 |
by (simp add: qfst_def) |
13285 | 130 |
|
131 |
lemma qsnd_conv [simp]: "qsnd(<a;b>) = b" |
|
13544 | 132 |
by (simp add: qsnd_def) |
13285 | 133 |
|
134 |
lemma qfst_type [TC]: "p:QSigma(A,B) ==> qfst(p) : A" |
|
135 |
by auto |
|
136 |
||
137 |
lemma qsnd_type [TC]: "p:QSigma(A,B) ==> qsnd(p) : B(qfst(p))" |
|
138 |
by auto |
|
139 |
||
140 |
lemma QPair_qfst_qsnd_eq: "a: QSigma(A,B) ==> <qfst(a); qsnd(a)> = a" |
|
141 |
by auto |
|
142 |
||
143 |
||
13356 | 144 |
subsubsection{*Eliminator: qsplit*} |
13285 | 145 |
|
146 |
(*A META-equality, so that it applies to higher types as well...*) |
|
147 |
lemma qsplit [simp]: "qsplit(%x y. c(x,y), <a;b>) == c(a,b)" |
|
148 |
by (simp add: qsplit_def) |
|
149 |
||
150 |
||
151 |
lemma qsplit_type [elim!]: |
|
152 |
"[| p:QSigma(A,B); |
|
153 |
!!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x;y>) |
|
154 |
|] ==> qsplit(%x y. c(x,y), p) : C(p)" |
|
155 |
by auto |
|
156 |
||
157 |
lemma expand_qsplit: |
|
158 |
"u: A<*>B ==> R(qsplit(c,u)) <-> (ALL x:A. ALL y:B. u = <x;y> --> R(c(x,y)))" |
|
159 |
apply (simp add: qsplit_def, auto) |
|
160 |
done |
|
161 |
||
162 |
||
13356 | 163 |
subsubsection{*qsplit for predicates: result type o*} |
13285 | 164 |
|
165 |
lemma qsplitI: "R(a,b) ==> qsplit(R, <a;b>)" |
|
166 |
by (simp add: qsplit_def) |
|
167 |
||
168 |
||
169 |
lemma qsplitE: |
|
170 |
"[| qsplit(R,z); z:QSigma(A,B); |
|
171 |
!!x y. [| z = <x;y>; R(x,y) |] ==> P |
|
172 |
|] ==> P" |
|
13356 | 173 |
by (simp add: qsplit_def, auto) |
13285 | 174 |
|
175 |
lemma qsplitD: "qsplit(R,<a;b>) ==> R(a,b)" |
|
176 |
by (simp add: qsplit_def) |
|
177 |
||
178 |
||
13356 | 179 |
subsubsection{*qconverse*} |
13285 | 180 |
|
181 |
lemma qconverseI [intro!]: "<a;b>:r ==> <b;a>:qconverse(r)" |
|
182 |
by (simp add: qconverse_def, blast) |
|
183 |
||
184 |
lemma qconverseD [elim!]: "<a;b> : qconverse(r) ==> <b;a> : r" |
|
185 |
by (simp add: qconverse_def, blast) |
|
186 |
||
187 |
lemma qconverseE [elim!]: |
|
188 |
"[| yx : qconverse(r); |
|
189 |
!!x y. [| yx=<y;x>; <x;y>:r |] ==> P |
|
190 |
|] ==> P" |
|
13356 | 191 |
by (simp add: qconverse_def, blast) |
13285 | 192 |
|
193 |
lemma qconverse_qconverse: "r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r" |
|
194 |
by blast |
|
195 |
||
196 |
lemma qconverse_type: "r <= A <*> B ==> qconverse(r) <= B <*> A" |
|
197 |
by blast |
|
198 |
||
199 |
lemma qconverse_prod: "qconverse(A <*> B) = B <*> A" |
|
200 |
by blast |
|
201 |
||
202 |
lemma qconverse_empty: "qconverse(0) = 0" |
|
203 |
by blast |
|
204 |
||
205 |
||
13356 | 206 |
subsection{*The Quine-inspired notion of disjoint sum*} |
13285 | 207 |
|
208 |
lemmas qsum_defs = qsum_def QInl_def QInr_def qcase_def |
|
209 |
||
210 |
(** Introduction rules for the injections **) |
|
211 |
||
212 |
lemma QInlI [intro!]: "a : A ==> QInl(a) : A <+> B" |
|
213 |
by (simp add: qsum_defs, blast) |
|
1097
01379c46ad2d
Changed definitions so that qsplit is now defined in terms of
lcp
parents:
929
diff
changeset
|
214 |
|
13285 | 215 |
lemma QInrI [intro!]: "b : B ==> QInr(b) : A <+> B" |
216 |
by (simp add: qsum_defs, blast) |
|
217 |
||
218 |
(** Elimination rules **) |
|
219 |
||
220 |
lemma qsumE [elim!]: |
|
221 |
"[| u: A <+> B; |
|
222 |
!!x. [| x:A; u=QInl(x) |] ==> P; |
|
223 |
!!y. [| y:B; u=QInr(y) |] ==> P |
|
224 |
|] ==> P" |
|
13356 | 225 |
by (simp add: qsum_defs, blast) |
13285 | 226 |
|
227 |
||
228 |
(** Injection and freeness equivalences, for rewriting **) |
|
229 |
||
230 |
lemma QInl_iff [iff]: "QInl(a)=QInl(b) <-> a=b" |
|
231 |
by (simp add: qsum_defs ) |
|
232 |
||
233 |
lemma QInr_iff [iff]: "QInr(a)=QInr(b) <-> a=b" |
|
234 |
by (simp add: qsum_defs ) |
|
235 |
||
13823 | 236 |
lemma QInl_QInr_iff [simp]: "QInl(a)=QInr(b) <-> False" |
13285 | 237 |
by (simp add: qsum_defs ) |
238 |
||
13823 | 239 |
lemma QInr_QInl_iff [simp]: "QInr(b)=QInl(a) <-> False" |
13285 | 240 |
by (simp add: qsum_defs ) |
241 |
||
242 |
lemma qsum_empty [simp]: "0<+>0 = 0" |
|
243 |
by (simp add: qsum_defs ) |
|
244 |
||
245 |
(*Injection and freeness rules*) |
|
246 |
||
247 |
lemmas QInl_inject = QInl_iff [THEN iffD1, standard] |
|
248 |
lemmas QInr_inject = QInr_iff [THEN iffD1, standard] |
|
13823 | 249 |
lemmas QInl_neq_QInr = QInl_QInr_iff [THEN iffD1, THEN FalseE, elim!] |
250 |
lemmas QInr_neq_QInl = QInr_QInl_iff [THEN iffD1, THEN FalseE, elim!] |
|
13285 | 251 |
|
252 |
lemma QInlD: "QInl(a): A<+>B ==> a: A" |
|
253 |
by blast |
|
254 |
||
255 |
lemma QInrD: "QInr(b): A<+>B ==> b: B" |
|
256 |
by blast |
|
257 |
||
258 |
(** <+> is itself injective... who cares?? **) |
|
259 |
||
260 |
lemma qsum_iff: |
|
261 |
"u: A <+> B <-> (EX x. x:A & u=QInl(x)) | (EX y. y:B & u=QInr(y))" |
|
13356 | 262 |
by blast |
13285 | 263 |
|
264 |
lemma qsum_subset_iff: "A <+> B <= C <+> D <-> A<=C & B<=D" |
|
265 |
by blast |
|
266 |
||
267 |
lemma qsum_equal_iff: "A <+> B = C <+> D <-> A=C & B=D" |
|
268 |
apply (simp (no_asm) add: extension qsum_subset_iff) |
|
269 |
apply blast |
|
270 |
done |
|
271 |
||
13356 | 272 |
subsubsection{*Eliminator -- qcase*} |
13285 | 273 |
|
274 |
lemma qcase_QInl [simp]: "qcase(c, d, QInl(a)) = c(a)" |
|
275 |
by (simp add: qsum_defs ) |
|
276 |
||
277 |
||
278 |
lemma qcase_QInr [simp]: "qcase(c, d, QInr(b)) = d(b)" |
|
279 |
by (simp add: qsum_defs ) |
|
280 |
||
281 |
lemma qcase_type: |
|
282 |
"[| u: A <+> B; |
|
283 |
!!x. x: A ==> c(x): C(QInl(x)); |
|
284 |
!!y. y: B ==> d(y): C(QInr(y)) |
|
285 |
|] ==> qcase(c,d,u) : C(u)" |
|
13784 | 286 |
by (simp add: qsum_defs, auto) |
13285 | 287 |
|
288 |
(** Rules for the Part primitive **) |
|
289 |
||
290 |
lemma Part_QInl: "Part(A <+> B,QInl) = {QInl(x). x: A}" |
|
291 |
by blast |
|
292 |
||
293 |
lemma Part_QInr: "Part(A <+> B,QInr) = {QInr(y). y: B}" |
|
294 |
by blast |
|
295 |
||
296 |
lemma Part_QInr2: "Part(A <+> B, %x. QInr(h(x))) = {QInr(y). y: Part(B,h)}" |
|
297 |
by blast |
|
0 | 298 |
|
13285 | 299 |
lemma Part_qsum_equality: "C <= A <+> B ==> Part(C,QInl) Un Part(C,QInr) = C" |
300 |
by blast |
|
301 |
||
302 |
||
13356 | 303 |
subsubsection{*Monotonicity*} |
13285 | 304 |
|
305 |
lemma QPair_mono: "[| a<=c; b<=d |] ==> <a;b> <= <c;d>" |
|
306 |
by (simp add: QPair_def sum_mono) |
|
307 |
||
308 |
lemma QSigma_mono [rule_format]: |
|
309 |
"[| A<=C; ALL x:A. B(x) <= D(x) |] ==> QSigma(A,B) <= QSigma(C,D)" |
|
310 |
by blast |
|
311 |
||
312 |
lemma QInl_mono: "a<=b ==> QInl(a) <= QInl(b)" |
|
313 |
by (simp add: QInl_def subset_refl [THEN QPair_mono]) |
|
314 |
||
315 |
lemma QInr_mono: "a<=b ==> QInr(a) <= QInr(b)" |
|
316 |
by (simp add: QInr_def subset_refl [THEN QPair_mono]) |
|
317 |
||
318 |
lemma qsum_mono: "[| A<=C; B<=D |] ==> A <+> B <= C <+> D" |
|
319 |
by blast |
|
320 |
||
321 |
ML |
|
322 |
{* |
|
323 |
val qsum_defs = thms "qsum_defs"; |
|
324 |
||
325 |
val QPair_empty = thm "QPair_empty"; |
|
326 |
val QPair_iff = thm "QPair_iff"; |
|
327 |
val QPair_inject = thm "QPair_inject"; |
|
328 |
val QPair_inject1 = thm "QPair_inject1"; |
|
329 |
val QPair_inject2 = thm "QPair_inject2"; |
|
330 |
val QSigmaI = thm "QSigmaI"; |
|
331 |
val QSigmaE = thm "QSigmaE"; |
|
332 |
val QSigmaE = thm "QSigmaE"; |
|
333 |
val QSigmaE2 = thm "QSigmaE2"; |
|
334 |
val QSigmaD1 = thm "QSigmaD1"; |
|
335 |
val QSigmaD2 = thm "QSigmaD2"; |
|
336 |
val QSigma_cong = thm "QSigma_cong"; |
|
337 |
val QSigma_empty1 = thm "QSigma_empty1"; |
|
338 |
val QSigma_empty2 = thm "QSigma_empty2"; |
|
339 |
val qfst_conv = thm "qfst_conv"; |
|
340 |
val qsnd_conv = thm "qsnd_conv"; |
|
341 |
val qfst_type = thm "qfst_type"; |
|
342 |
val qsnd_type = thm "qsnd_type"; |
|
343 |
val QPair_qfst_qsnd_eq = thm "QPair_qfst_qsnd_eq"; |
|
344 |
val qsplit = thm "qsplit"; |
|
345 |
val qsplit_type = thm "qsplit_type"; |
|
346 |
val expand_qsplit = thm "expand_qsplit"; |
|
347 |
val qsplitI = thm "qsplitI"; |
|
348 |
val qsplitE = thm "qsplitE"; |
|
349 |
val qsplitD = thm "qsplitD"; |
|
350 |
val qconverseI = thm "qconverseI"; |
|
351 |
val qconverseD = thm "qconverseD"; |
|
352 |
val qconverseE = thm "qconverseE"; |
|
353 |
val qconverse_qconverse = thm "qconverse_qconverse"; |
|
354 |
val qconverse_type = thm "qconverse_type"; |
|
355 |
val qconverse_prod = thm "qconverse_prod"; |
|
356 |
val qconverse_empty = thm "qconverse_empty"; |
|
357 |
val QInlI = thm "QInlI"; |
|
358 |
val QInrI = thm "QInrI"; |
|
359 |
val qsumE = thm "qsumE"; |
|
360 |
val QInl_iff = thm "QInl_iff"; |
|
361 |
val QInr_iff = thm "QInr_iff"; |
|
362 |
val QInl_QInr_iff = thm "QInl_QInr_iff"; |
|
363 |
val QInr_QInl_iff = thm "QInr_QInl_iff"; |
|
364 |
val qsum_empty = thm "qsum_empty"; |
|
365 |
val QInl_inject = thm "QInl_inject"; |
|
366 |
val QInr_inject = thm "QInr_inject"; |
|
367 |
val QInl_neq_QInr = thm "QInl_neq_QInr"; |
|
368 |
val QInr_neq_QInl = thm "QInr_neq_QInl"; |
|
369 |
val QInlD = thm "QInlD"; |
|
370 |
val QInrD = thm "QInrD"; |
|
371 |
val qsum_iff = thm "qsum_iff"; |
|
372 |
val qsum_subset_iff = thm "qsum_subset_iff"; |
|
373 |
val qsum_equal_iff = thm "qsum_equal_iff"; |
|
374 |
val qcase_QInl = thm "qcase_QInl"; |
|
375 |
val qcase_QInr = thm "qcase_QInr"; |
|
376 |
val qcase_type = thm "qcase_type"; |
|
377 |
val Part_QInl = thm "Part_QInl"; |
|
378 |
val Part_QInr = thm "Part_QInr"; |
|
379 |
val Part_QInr2 = thm "Part_QInr2"; |
|
380 |
val Part_qsum_equality = thm "Part_qsum_equality"; |
|
381 |
val QPair_mono = thm "QPair_mono"; |
|
382 |
val QSigma_mono = thm "QSigma_mono"; |
|
383 |
val QInl_mono = thm "QInl_mono"; |
|
384 |
val QInr_mono = thm "QInr_mono"; |
|
385 |
val qsum_mono = thm "qsum_mono"; |
|
386 |
*} |
|
387 |
||
0 | 388 |
end |
389 |