author | wenzelm |
Sun, 07 Oct 2007 21:19:31 +0200 | |
changeset 24893 | b8ef7afe3a6b |
parent 22808 | a7daa74e2980 |
child 35762 | af3ff2ba4c54 |
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 |
||
24893 | 24 |
definition |
25 |
QPair :: "[i, i] => i" ("<(_;/ _)>") where |
|
13285 | 26 |
"<a;b> == a+b" |
3923 | 27 |
|
24893 | 28 |
definition |
29 |
qfst :: "i => i" where |
|
13285 | 30 |
"qfst(p) == THE a. EX b. p=<a;b>" |
31 |
||
24893 | 32 |
definition |
33 |
qsnd :: "i => i" where |
|
13285 | 34 |
"qsnd(p) == THE b. EX a. p=<a;b>" |
35 |
||
24893 | 36 |
definition |
37 |
qsplit :: "[[i, i] => 'a, i] => 'a::{}" (*for pattern-matching*) where |
|
13285 | 38 |
"qsplit(c,p) == c(qfst(p), qsnd(p))" |
0 | 39 |
|
24893 | 40 |
definition |
41 |
qconverse :: "i => i" where |
|
13285 | 42 |
"qconverse(r) == {z. w:r, EX x y. w=<x;y> & z=<y;x>}" |
43 |
||
24893 | 44 |
definition |
45 |
QSigma :: "[i, i => i] => i" where |
|
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13544
diff
changeset
|
46 |
"QSigma(A,B) == \<Union>x\<in>A. \<Union>y\<in>B(x). {<x;y>}" |
0 | 47 |
|
929
137035296ad6
Moved declarations of @QSUM and <*> to a syntax section.
lcp
parents:
753
diff
changeset
|
48 |
syntax |
22808 | 49 |
"_QSUM" :: "[idt, i, i] => i" ("(3QSUM _:_./ _)" 10) |
0 | 50 |
translations |
24893 | 51 |
"QSUM x:A. B" => "CONST QSigma(A, %x. B)" |
22808 | 52 |
|
53 |
abbreviation |
|
54 |
qprod (infixr "<*>" 80) where |
|
55 |
"A <*> B == QSigma(A, %_. B)" |
|
0 | 56 |
|
24893 | 57 |
definition |
58 |
qsum :: "[i,i]=>i" (infixr "<+>" 65) where |
|
13285 | 59 |
"A <+> B == ({0} <*> A) Un ({1} <*> B)" |
3923 | 60 |
|
24893 | 61 |
definition |
62 |
QInl :: "i=>i" where |
|
13285 | 63 |
"QInl(a) == <0;a>" |
64 |
||
24893 | 65 |
definition |
66 |
QInr :: "i=>i" where |
|
13285 | 67 |
"QInr(b) == <1;b>" |
68 |
||
24893 | 69 |
definition |
70 |
qcase :: "[i=>i, i=>i, i]=>i" where |
|
13285 | 71 |
"qcase(c,d) == qsplit(%y z. cond(y, d(z), c(z)))" |
72 |
||
73 |
||
13356 | 74 |
subsection{*Quine ordered pairing*} |
13285 | 75 |
|
76 |
(** Lemmas for showing that <a;b> uniquely determines a and b **) |
|
77 |
||
78 |
lemma QPair_empty [simp]: "<0;0> = 0" |
|
79 |
by (simp add: QPair_def) |
|
80 |
||
81 |
lemma QPair_iff [simp]: "<a;b> = <c;d> <-> a=c & b=d" |
|
82 |
apply (simp add: QPair_def) |
|
83 |
apply (rule sum_equal_iff) |
|
84 |
done |
|
85 |
||
86 |
lemmas QPair_inject = QPair_iff [THEN iffD1, THEN conjE, standard, elim!] |
|
87 |
||
88 |
lemma QPair_inject1: "<a;b> = <c;d> ==> a=c" |
|
89 |
by blast |
|
90 |
||
91 |
lemma QPair_inject2: "<a;b> = <c;d> ==> b=d" |
|
92 |
by blast |
|
93 |
||
94 |
||
13356 | 95 |
subsubsection{*QSigma: Disjoint union of a family of sets |
96 |
Generalizes Cartesian product*} |
|
13285 | 97 |
|
98 |
lemma QSigmaI [intro!]: "[| a:A; b:B(a) |] ==> <a;b> : QSigma(A,B)" |
|
99 |
by (simp add: QSigma_def) |
|
100 |
||
101 |
||
102 |
(** Elimination rules for <a;b>:A*B -- introducing no eigenvariables **) |
|
103 |
||
104 |
lemma QSigmaE [elim!]: |
|
105 |
"[| c: QSigma(A,B); |
|
106 |
!!x y.[| x:A; y:B(x); c=<x;y> |] ==> P |
|
107 |
|] ==> P" |
|
13356 | 108 |
by (simp add: QSigma_def, blast) |
13285 | 109 |
|
110 |
lemma QSigmaE2 [elim!]: |
|
111 |
"[| <a;b>: QSigma(A,B); [| a:A; b:B(a) |] ==> P |] ==> P" |
|
112 |
by (simp add: QSigma_def) |
|
113 |
||
114 |
lemma QSigmaD1: "<a;b> : QSigma(A,B) ==> a : A" |
|
115 |
by blast |
|
116 |
||
117 |
lemma QSigmaD2: "<a;b> : QSigma(A,B) ==> b : B(a)" |
|
118 |
by blast |
|
119 |
||
120 |
lemma QSigma_cong: |
|
121 |
"[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> |
|
122 |
QSigma(A,B) = QSigma(A',B')" |
|
123 |
by (simp add: QSigma_def) |
|
124 |
||
125 |
lemma QSigma_empty1 [simp]: "QSigma(0,B) = 0" |
|
126 |
by blast |
|
127 |
||
128 |
lemma QSigma_empty2 [simp]: "A <*> 0 = 0" |
|
129 |
by blast |
|
130 |
||
131 |
||
13356 | 132 |
subsubsection{*Projections: qfst, qsnd*} |
13285 | 133 |
|
134 |
lemma qfst_conv [simp]: "qfst(<a;b>) = a" |
|
13544 | 135 |
by (simp add: qfst_def) |
13285 | 136 |
|
137 |
lemma qsnd_conv [simp]: "qsnd(<a;b>) = b" |
|
13544 | 138 |
by (simp add: qsnd_def) |
13285 | 139 |
|
140 |
lemma qfst_type [TC]: "p:QSigma(A,B) ==> qfst(p) : A" |
|
141 |
by auto |
|
142 |
||
143 |
lemma qsnd_type [TC]: "p:QSigma(A,B) ==> qsnd(p) : B(qfst(p))" |
|
144 |
by auto |
|
145 |
||
146 |
lemma QPair_qfst_qsnd_eq: "a: QSigma(A,B) ==> <qfst(a); qsnd(a)> = a" |
|
147 |
by auto |
|
148 |
||
149 |
||
13356 | 150 |
subsubsection{*Eliminator: qsplit*} |
13285 | 151 |
|
152 |
(*A META-equality, so that it applies to higher types as well...*) |
|
153 |
lemma qsplit [simp]: "qsplit(%x y. c(x,y), <a;b>) == c(a,b)" |
|
154 |
by (simp add: qsplit_def) |
|
155 |
||
156 |
||
157 |
lemma qsplit_type [elim!]: |
|
158 |
"[| p:QSigma(A,B); |
|
159 |
!!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x;y>) |
|
160 |
|] ==> qsplit(%x y. c(x,y), p) : C(p)" |
|
161 |
by auto |
|
162 |
||
163 |
lemma expand_qsplit: |
|
164 |
"u: A<*>B ==> R(qsplit(c,u)) <-> (ALL x:A. ALL y:B. u = <x;y> --> R(c(x,y)))" |
|
165 |
apply (simp add: qsplit_def, auto) |
|
166 |
done |
|
167 |
||
168 |
||
13356 | 169 |
subsubsection{*qsplit for predicates: result type o*} |
13285 | 170 |
|
171 |
lemma qsplitI: "R(a,b) ==> qsplit(R, <a;b>)" |
|
172 |
by (simp add: qsplit_def) |
|
173 |
||
174 |
||
175 |
lemma qsplitE: |
|
176 |
"[| qsplit(R,z); z:QSigma(A,B); |
|
177 |
!!x y. [| z = <x;y>; R(x,y) |] ==> P |
|
178 |
|] ==> P" |
|
13356 | 179 |
by (simp add: qsplit_def, auto) |
13285 | 180 |
|
181 |
lemma qsplitD: "qsplit(R,<a;b>) ==> R(a,b)" |
|
182 |
by (simp add: qsplit_def) |
|
183 |
||
184 |
||
13356 | 185 |
subsubsection{*qconverse*} |
13285 | 186 |
|
187 |
lemma qconverseI [intro!]: "<a;b>:r ==> <b;a>:qconverse(r)" |
|
188 |
by (simp add: qconverse_def, blast) |
|
189 |
||
190 |
lemma qconverseD [elim!]: "<a;b> : qconverse(r) ==> <b;a> : r" |
|
191 |
by (simp add: qconverse_def, blast) |
|
192 |
||
193 |
lemma qconverseE [elim!]: |
|
194 |
"[| yx : qconverse(r); |
|
195 |
!!x y. [| yx=<y;x>; <x;y>:r |] ==> P |
|
196 |
|] ==> P" |
|
13356 | 197 |
by (simp add: qconverse_def, blast) |
13285 | 198 |
|
199 |
lemma qconverse_qconverse: "r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r" |
|
200 |
by blast |
|
201 |
||
202 |
lemma qconverse_type: "r <= A <*> B ==> qconverse(r) <= B <*> A" |
|
203 |
by blast |
|
204 |
||
205 |
lemma qconverse_prod: "qconverse(A <*> B) = B <*> A" |
|
206 |
by blast |
|
207 |
||
208 |
lemma qconverse_empty: "qconverse(0) = 0" |
|
209 |
by blast |
|
210 |
||
211 |
||
13356 | 212 |
subsection{*The Quine-inspired notion of disjoint sum*} |
13285 | 213 |
|
214 |
lemmas qsum_defs = qsum_def QInl_def QInr_def qcase_def |
|
215 |
||
216 |
(** Introduction rules for the injections **) |
|
217 |
||
218 |
lemma QInlI [intro!]: "a : A ==> QInl(a) : A <+> B" |
|
219 |
by (simp add: qsum_defs, blast) |
|
1097
01379c46ad2d
Changed definitions so that qsplit is now defined in terms of
lcp
parents:
929
diff
changeset
|
220 |
|
13285 | 221 |
lemma QInrI [intro!]: "b : B ==> QInr(b) : A <+> B" |
222 |
by (simp add: qsum_defs, blast) |
|
223 |
||
224 |
(** Elimination rules **) |
|
225 |
||
226 |
lemma qsumE [elim!]: |
|
227 |
"[| u: A <+> B; |
|
228 |
!!x. [| x:A; u=QInl(x) |] ==> P; |
|
229 |
!!y. [| y:B; u=QInr(y) |] ==> P |
|
230 |
|] ==> P" |
|
13356 | 231 |
by (simp add: qsum_defs, blast) |
13285 | 232 |
|
233 |
||
234 |
(** Injection and freeness equivalences, for rewriting **) |
|
235 |
||
236 |
lemma QInl_iff [iff]: "QInl(a)=QInl(b) <-> a=b" |
|
237 |
by (simp add: qsum_defs ) |
|
238 |
||
239 |
lemma QInr_iff [iff]: "QInr(a)=QInr(b) <-> a=b" |
|
240 |
by (simp add: qsum_defs ) |
|
241 |
||
13823 | 242 |
lemma QInl_QInr_iff [simp]: "QInl(a)=QInr(b) <-> False" |
13285 | 243 |
by (simp add: qsum_defs ) |
244 |
||
13823 | 245 |
lemma QInr_QInl_iff [simp]: "QInr(b)=QInl(a) <-> False" |
13285 | 246 |
by (simp add: qsum_defs ) |
247 |
||
248 |
lemma qsum_empty [simp]: "0<+>0 = 0" |
|
249 |
by (simp add: qsum_defs ) |
|
250 |
||
251 |
(*Injection and freeness rules*) |
|
252 |
||
253 |
lemmas QInl_inject = QInl_iff [THEN iffD1, standard] |
|
254 |
lemmas QInr_inject = QInr_iff [THEN iffD1, standard] |
|
13823 | 255 |
lemmas QInl_neq_QInr = QInl_QInr_iff [THEN iffD1, THEN FalseE, elim!] |
256 |
lemmas QInr_neq_QInl = QInr_QInl_iff [THEN iffD1, THEN FalseE, elim!] |
|
13285 | 257 |
|
258 |
lemma QInlD: "QInl(a): A<+>B ==> a: A" |
|
259 |
by blast |
|
260 |
||
261 |
lemma QInrD: "QInr(b): A<+>B ==> b: B" |
|
262 |
by blast |
|
263 |
||
264 |
(** <+> is itself injective... who cares?? **) |
|
265 |
||
266 |
lemma qsum_iff: |
|
267 |
"u: A <+> B <-> (EX x. x:A & u=QInl(x)) | (EX y. y:B & u=QInr(y))" |
|
13356 | 268 |
by blast |
13285 | 269 |
|
270 |
lemma qsum_subset_iff: "A <+> B <= C <+> D <-> A<=C & B<=D" |
|
271 |
by blast |
|
272 |
||
273 |
lemma qsum_equal_iff: "A <+> B = C <+> D <-> A=C & B=D" |
|
274 |
apply (simp (no_asm) add: extension qsum_subset_iff) |
|
275 |
apply blast |
|
276 |
done |
|
277 |
||
13356 | 278 |
subsubsection{*Eliminator -- qcase*} |
13285 | 279 |
|
280 |
lemma qcase_QInl [simp]: "qcase(c, d, QInl(a)) = c(a)" |
|
281 |
by (simp add: qsum_defs ) |
|
282 |
||
283 |
||
284 |
lemma qcase_QInr [simp]: "qcase(c, d, QInr(b)) = d(b)" |
|
285 |
by (simp add: qsum_defs ) |
|
286 |
||
287 |
lemma qcase_type: |
|
288 |
"[| u: A <+> B; |
|
289 |
!!x. x: A ==> c(x): C(QInl(x)); |
|
290 |
!!y. y: B ==> d(y): C(QInr(y)) |
|
291 |
|] ==> qcase(c,d,u) : C(u)" |
|
13784 | 292 |
by (simp add: qsum_defs, auto) |
13285 | 293 |
|
294 |
(** Rules for the Part primitive **) |
|
295 |
||
296 |
lemma Part_QInl: "Part(A <+> B,QInl) = {QInl(x). x: A}" |
|
297 |
by blast |
|
298 |
||
299 |
lemma Part_QInr: "Part(A <+> B,QInr) = {QInr(y). y: B}" |
|
300 |
by blast |
|
301 |
||
302 |
lemma Part_QInr2: "Part(A <+> B, %x. QInr(h(x))) = {QInr(y). y: Part(B,h)}" |
|
303 |
by blast |
|
0 | 304 |
|
13285 | 305 |
lemma Part_qsum_equality: "C <= A <+> B ==> Part(C,QInl) Un Part(C,QInr) = C" |
306 |
by blast |
|
307 |
||
308 |
||
13356 | 309 |
subsubsection{*Monotonicity*} |
13285 | 310 |
|
311 |
lemma QPair_mono: "[| a<=c; b<=d |] ==> <a;b> <= <c;d>" |
|
312 |
by (simp add: QPair_def sum_mono) |
|
313 |
||
314 |
lemma QSigma_mono [rule_format]: |
|
315 |
"[| A<=C; ALL x:A. B(x) <= D(x) |] ==> QSigma(A,B) <= QSigma(C,D)" |
|
316 |
by blast |
|
317 |
||
318 |
lemma QInl_mono: "a<=b ==> QInl(a) <= QInl(b)" |
|
319 |
by (simp add: QInl_def subset_refl [THEN QPair_mono]) |
|
320 |
||
321 |
lemma QInr_mono: "a<=b ==> QInr(a) <= QInr(b)" |
|
322 |
by (simp add: QInr_def subset_refl [THEN QPair_mono]) |
|
323 |
||
324 |
lemma qsum_mono: "[| A<=C; B<=D |] ==> A <+> B <= C <+> D" |
|
325 |
by blast |
|
326 |
||
0 | 327 |
end |