1 (* Title: ZF/QPair.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 Quine-inspired ordered pairs and disjoint sums, for non-well-founded data |
|
7 structures in ZF. Does not precisely follow Quine's construction. Thanks |
|
8 to Thomas Forster for suggesting this approach! |
|
9 |
|
10 W. V. Quine, On Ordered Pairs and Relations, in Selected Logic Papers, |
|
11 1966. |
|
12 |
|
13 Many proofs are borrowed from pair.ML and sum.ML |
|
14 |
|
15 Do we EVER have rank(a) < rank(<a;b>) ? Perhaps if the latter rank |
|
16 is not a limit ordinal? |
|
17 *) |
|
18 |
|
19 (**** Quine ordered pairing ****) |
|
20 |
|
21 (** Lemmas for showing that <a;b> uniquely determines a and b **) |
|
22 |
|
23 Goalw [QPair_def] "<0;0> = 0"; |
|
24 by (Simp_tac 1); |
|
25 qed "QPair_empty"; |
|
26 |
|
27 Goalw [QPair_def] "<a;b> = <c;d> <-> a=c & b=d"; |
|
28 by (rtac sum_equal_iff 1); |
|
29 qed "QPair_iff"; |
|
30 |
|
31 bind_thm ("QPair_inject", QPair_iff RS iffD1 RS conjE); |
|
32 |
|
33 Addsimps [QPair_empty, QPair_iff]; |
|
34 AddSEs [QPair_inject]; |
|
35 |
|
36 Goal "<a;b> = <c;d> ==> a=c"; |
|
37 by (Blast_tac 1) ; |
|
38 qed "QPair_inject1"; |
|
39 |
|
40 Goal "<a;b> = <c;d> ==> b=d"; |
|
41 by (Blast_tac 1) ; |
|
42 qed "QPair_inject2"; |
|
43 |
|
44 |
|
45 (*** QSigma: Disjoint union of a family of sets |
|
46 Generalizes Cartesian product ***) |
|
47 |
|
48 Goalw [QSigma_def] "[| a:A; b:B(a) |] ==> <a;b> : QSigma(A,B)"; |
|
49 by (Blast_tac 1) ; |
|
50 qed "QSigmaI"; |
|
51 |
|
52 AddSIs [QSigmaI]; |
|
53 |
|
54 (*The general elimination rule*) |
|
55 val major::prems= Goalw [QSigma_def] |
|
56 "[| c: QSigma(A,B); \ |
|
57 \ !!x y.[| x:A; y:B(x); c=<x;y> |] ==> P \ |
|
58 \ |] ==> P"; |
|
59 by (cut_facts_tac [major] 1); |
|
60 by (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ; |
|
61 qed "QSigmaE"; |
|
62 |
|
63 (** Elimination rules for <a;b>:A*B -- introducing no eigenvariables **) |
|
64 |
|
65 bind_thm ("QSigmaE2", |
|
66 rule_by_tactic (REPEAT_FIRST (etac QPair_inject ORELSE' bound_hyp_subst_tac) |
|
67 THEN prune_params_tac) |
|
68 (inst "c" "<a;b>" QSigmaE)); |
|
69 |
|
70 AddSEs [QSigmaE2, QSigmaE]; |
|
71 |
|
72 Goal "<a;b> : QSigma(A,B) ==> a : A"; |
|
73 by (Blast_tac 1) ; |
|
74 qed "QSigmaD1"; |
|
75 |
|
76 Goal "<a;b> : QSigma(A,B) ==> b : B(a)"; |
|
77 by (Blast_tac 1) ; |
|
78 qed "QSigmaD2"; |
|
79 |
|
80 |
|
81 val prems= Goalw [QSigma_def] |
|
82 "[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> \ |
|
83 \ QSigma(A,B) = QSigma(A',B')"; |
|
84 by (simp_tac (simpset() addsimps prems) 1) ; |
|
85 qed "QSigma_cong"; |
|
86 |
|
87 Goal "QSigma(0,B) = 0"; |
|
88 by (Blast_tac 1) ; |
|
89 qed "QSigma_empty1"; |
|
90 |
|
91 Goal "A <*> 0 = 0"; |
|
92 by (Blast_tac 1) ; |
|
93 qed "QSigma_empty2"; |
|
94 |
|
95 Addsimps [QSigma_empty1, QSigma_empty2]; |
|
96 |
|
97 |
|
98 (*** Projections: qfst, qsnd ***) |
|
99 |
|
100 Goalw [qfst_def] "qfst(<a;b>) = a"; |
|
101 by (Blast_tac 1) ; |
|
102 qed "qfst_conv"; |
|
103 |
|
104 Goalw [qsnd_def] "qsnd(<a;b>) = b"; |
|
105 by (Blast_tac 1) ; |
|
106 qed "qsnd_conv"; |
|
107 |
|
108 Addsimps [qfst_conv, qsnd_conv]; |
|
109 |
|
110 Goal "p:QSigma(A,B) ==> qfst(p) : A"; |
|
111 by (Auto_tac) ; |
|
112 qed "qfst_type"; |
|
113 AddTCs [qfst_type]; |
|
114 |
|
115 Goal "p:QSigma(A,B) ==> qsnd(p) : B(qfst(p))"; |
|
116 by (Auto_tac) ; |
|
117 qed "qsnd_type"; |
|
118 AddTCs [qsnd_type]; |
|
119 |
|
120 Goal "a: QSigma(A,B) ==> <qfst(a); qsnd(a)> = a"; |
|
121 by Auto_tac; |
|
122 qed "QPair_qfst_qsnd_eq"; |
|
123 |
|
124 |
|
125 (*** Eliminator - qsplit ***) |
|
126 |
|
127 (*A META-equality, so that it applies to higher types as well...*) |
|
128 Goalw [qsplit_def] "qsplit(%x y. c(x,y), <a;b>) == c(a,b)"; |
|
129 by (Simp_tac 1); |
|
130 qed "qsplit"; |
|
131 Addsimps [qsplit]; |
|
132 |
|
133 val major::prems= Goal |
|
134 "[| p:QSigma(A,B); \ |
|
135 \ !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x;y>) \ |
|
136 \ |] ==> qsplit(%x y. c(x,y), p) : C(p)"; |
|
137 by (rtac (major RS QSigmaE) 1); |
|
138 by (asm_simp_tac (simpset() addsimps prems) 1) ; |
|
139 qed "qsplit_type"; |
|
140 |
|
141 Goalw [qsplit_def] |
|
142 "u: A<*>B ==> R(qsplit(c,u)) <-> (ALL x:A. ALL y:B. u = <x;y> --> R(c(x,y)))"; |
|
143 by Auto_tac; |
|
144 qed "expand_qsplit"; |
|
145 |
|
146 |
|
147 (*** qsplit for predicates: result type o ***) |
|
148 |
|
149 Goalw [qsplit_def] "R(a,b) ==> qsplit(R, <a;b>)"; |
|
150 by (Asm_simp_tac 1); |
|
151 qed "qsplitI"; |
|
152 |
|
153 val major::sigma::prems = Goalw [qsplit_def] |
|
154 "[| qsplit(R,z); z:QSigma(A,B); \ |
|
155 \ !!x y. [| z = <x;y>; R(x,y) |] ==> P \ |
|
156 \ |] ==> P"; |
|
157 by (rtac (sigma RS QSigmaE) 1); |
|
158 by (cut_facts_tac [major] 1); |
|
159 by (REPEAT (ares_tac prems 1)); |
|
160 by (Asm_full_simp_tac 1); |
|
161 qed "qsplitE"; |
|
162 |
|
163 Goalw [qsplit_def] "qsplit(R,<a;b>) ==> R(a,b)"; |
|
164 by (Asm_full_simp_tac 1); |
|
165 qed "qsplitD"; |
|
166 |
|
167 |
|
168 (*** qconverse ***) |
|
169 |
|
170 Goalw [qconverse_def] "<a;b>:r ==> <b;a>:qconverse(r)"; |
|
171 by (Blast_tac 1) ; |
|
172 qed "qconverseI"; |
|
173 |
|
174 Goalw [qconverse_def] "<a;b> : qconverse(r) ==> <b;a> : r"; |
|
175 by (Blast_tac 1) ; |
|
176 qed "qconverseD"; |
|
177 |
|
178 val [major,minor]= Goalw [qconverse_def] |
|
179 "[| yx : qconverse(r); \ |
|
180 \ !!x y. [| yx=<y;x>; <x;y>:r |] ==> P \ |
|
181 \ |] ==> P"; |
|
182 by (rtac (major RS ReplaceE) 1); |
|
183 by (REPEAT (eresolve_tac [exE, conjE, minor] 1)); |
|
184 by (hyp_subst_tac 1); |
|
185 by (assume_tac 1) ; |
|
186 qed "qconverseE"; |
|
187 |
|
188 AddSIs [qconverseI]; |
|
189 AddSEs [qconverseD, qconverseE]; |
|
190 |
|
191 Goal "r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r"; |
|
192 by (Blast_tac 1) ; |
|
193 qed "qconverse_qconverse"; |
|
194 |
|
195 Goal "r <= A <*> B ==> qconverse(r) <= B <*> A"; |
|
196 by (Blast_tac 1) ; |
|
197 qed "qconverse_type"; |
|
198 |
|
199 Goal "qconverse(A <*> B) = B <*> A"; |
|
200 by (Blast_tac 1) ; |
|
201 qed "qconverse_prod"; |
|
202 |
|
203 Goal "qconverse(0) = 0"; |
|
204 by (Blast_tac 1) ; |
|
205 qed "qconverse_empty"; |
|
206 |
|
207 |
|
208 (**** The Quine-inspired notion of disjoint sum ****) |
|
209 |
|
210 bind_thms ("qsum_defs", [qsum_def,QInl_def,QInr_def,qcase_def]); |
|
211 |
|
212 (** Introduction rules for the injections **) |
|
213 |
|
214 Goalw qsum_defs "a : A ==> QInl(a) : A <+> B"; |
|
215 by (Blast_tac 1); |
|
216 qed "QInlI"; |
|
217 |
|
218 Goalw qsum_defs "b : B ==> QInr(b) : A <+> B"; |
|
219 by (Blast_tac 1); |
|
220 qed "QInrI"; |
|
221 |
|
222 (** Elimination rules **) |
|
223 |
|
224 val major::prems = Goalw qsum_defs |
|
225 "[| u: A <+> B; \ |
|
226 \ !!x. [| x:A; u=QInl(x) |] ==> P; \ |
|
227 \ !!y. [| y:B; u=QInr(y) |] ==> P \ |
|
228 \ |] ==> P"; |
|
229 by (rtac (major RS UnE) 1); |
|
230 by (REPEAT (rtac refl 1 |
|
231 ORELSE eresolve_tac (prems@[QSigmaE,singletonE,ssubst]) 1)); |
|
232 qed "qsumE"; |
|
233 |
|
234 AddSIs [QInlI, QInrI]; |
|
235 |
|
236 (** Injection and freeness equivalences, for rewriting **) |
|
237 |
|
238 Goalw qsum_defs "QInl(a)=QInl(b) <-> a=b"; |
|
239 by (Simp_tac 1); |
|
240 qed "QInl_iff"; |
|
241 |
|
242 Goalw qsum_defs "QInr(a)=QInr(b) <-> a=b"; |
|
243 by (Simp_tac 1); |
|
244 qed "QInr_iff"; |
|
245 |
|
246 Goalw qsum_defs "QInl(a)=QInr(b) <-> False"; |
|
247 by (Simp_tac 1); |
|
248 qed "QInl_QInr_iff"; |
|
249 |
|
250 Goalw qsum_defs "QInr(b)=QInl(a) <-> False"; |
|
251 by (Simp_tac 1); |
|
252 qed "QInr_QInl_iff"; |
|
253 |
|
254 Goalw qsum_defs "0<+>0 = 0"; |
|
255 by (Simp_tac 1); |
|
256 qed "qsum_empty"; |
|
257 |
|
258 (*Injection and freeness rules*) |
|
259 |
|
260 bind_thm ("QInl_inject", (QInl_iff RS iffD1)); |
|
261 bind_thm ("QInr_inject", (QInr_iff RS iffD1)); |
|
262 bind_thm ("QInl_neq_QInr", (QInl_QInr_iff RS iffD1 RS FalseE)); |
|
263 bind_thm ("QInr_neq_QInl", (QInr_QInl_iff RS iffD1 RS FalseE)); |
|
264 |
|
265 AddSEs [qsumE, QInl_neq_QInr, QInr_neq_QInl]; |
|
266 AddSDs [QInl_inject, QInr_inject]; |
|
267 Addsimps [QInl_iff, QInr_iff, QInl_QInr_iff, QInr_QInl_iff, qsum_empty]; |
|
268 |
|
269 Goal "QInl(a): A<+>B ==> a: A"; |
|
270 by (Blast_tac 1); |
|
271 qed "QInlD"; |
|
272 |
|
273 Goal "QInr(b): A<+>B ==> b: B"; |
|
274 by (Blast_tac 1); |
|
275 qed "QInrD"; |
|
276 |
|
277 (** <+> is itself injective... who cares?? **) |
|
278 |
|
279 Goal "u: A <+> B <-> (EX x. x:A & u=QInl(x)) | (EX y. y:B & u=QInr(y))"; |
|
280 by (Blast_tac 1); |
|
281 qed "qsum_iff"; |
|
282 |
|
283 Goal "A <+> B <= C <+> D <-> A<=C & B<=D"; |
|
284 by (Blast_tac 1); |
|
285 qed "qsum_subset_iff"; |
|
286 |
|
287 Goal "A <+> B = C <+> D <-> A=C & B=D"; |
|
288 by (simp_tac (simpset() addsimps [extension,qsum_subset_iff]) 1); |
|
289 by (Blast_tac 1); |
|
290 qed "qsum_equal_iff"; |
|
291 |
|
292 (*** Eliminator -- qcase ***) |
|
293 |
|
294 Goalw qsum_defs "qcase(c, d, QInl(a)) = c(a)"; |
|
295 by (Simp_tac 1); |
|
296 qed "qcase_QInl"; |
|
297 |
|
298 Goalw qsum_defs "qcase(c, d, QInr(b)) = d(b)"; |
|
299 by (Simp_tac 1); |
|
300 qed "qcase_QInr"; |
|
301 |
|
302 Addsimps [qcase_QInl, qcase_QInr]; |
|
303 |
|
304 val major::prems = Goal |
|
305 "[| u: A <+> B; \ |
|
306 \ !!x. x: A ==> c(x): C(QInl(x)); \ |
|
307 \ !!y. y: B ==> d(y): C(QInr(y)) \ |
|
308 \ |] ==> qcase(c,d,u) : C(u)"; |
|
309 by (rtac (major RS qsumE) 1); |
|
310 by (ALLGOALS (etac ssubst)); |
|
311 by (ALLGOALS (asm_simp_tac (simpset() addsimps prems))); |
|
312 qed "qcase_type"; |
|
313 |
|
314 (** Rules for the Part primitive **) |
|
315 |
|
316 Goal "Part(A <+> B,QInl) = {QInl(x). x: A}"; |
|
317 by (Blast_tac 1); |
|
318 qed "Part_QInl"; |
|
319 |
|
320 Goal "Part(A <+> B,QInr) = {QInr(y). y: B}"; |
|
321 by (Blast_tac 1); |
|
322 qed "Part_QInr"; |
|
323 |
|
324 Goal "Part(A <+> B, %x. QInr(h(x))) = {QInr(y). y: Part(B,h)}"; |
|
325 by (Blast_tac 1); |
|
326 qed "Part_QInr2"; |
|
327 |
|
328 Goal "C <= A <+> B ==> Part(C,QInl) Un Part(C,QInr) = C"; |
|
329 by (Blast_tac 1); |
|
330 qed "Part_qsum_equality"; |
|
331 |
|
332 |
|
333 (*** Monotonicity ***) |
|
334 |
|
335 Goalw [QPair_def] "[| a<=c; b<=d |] ==> <a;b> <= <c;d>"; |
|
336 by (REPEAT (ares_tac [sum_mono] 1)); |
|
337 qed "QPair_mono"; |
|
338 |
|
339 Goal "[| A<=C; ALL x:A. B(x) <= D(x) |] ==> \ |
|
340 \ QSigma(A,B) <= QSigma(C,D)"; |
|
341 by (Blast_tac 1); |
|
342 qed "QSigma_mono_lemma"; |
|
343 bind_thm ("QSigma_mono", ballI RSN (2,QSigma_mono_lemma)); |
|
344 |
|
345 Goalw [QInl_def] "a<=b ==> QInl(a) <= QInl(b)"; |
|
346 by (REPEAT (ares_tac [subset_refl RS QPair_mono] 1)); |
|
347 qed "QInl_mono"; |
|
348 |
|
349 Goalw [QInr_def] "a<=b ==> QInr(a) <= QInr(b)"; |
|
350 by (REPEAT (ares_tac [subset_refl RS QPair_mono] 1)); |
|
351 qed "QInr_mono"; |
|
352 |
|
353 Goal "[| A<=C; B<=D |] ==> A <+> B <= C <+> D"; |
|
354 by (Blast_tac 1); |
|
355 qed "qsum_mono"; |
|
356 |
|
357 |
|