author | paulson |
Fri, 11 Aug 2000 13:26:40 +0200 | |
changeset 9577 | 9e66e8ed8237 |
parent 9211 | 6236c5285bd8 |
child 9907 | 473a6604da94 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/QPair.ML |
0 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 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 |
||
9211 | 23 |
Goalw [QPair_def] "<0;0> = 0"; |
24 |
by (Simp_tac 1); |
|
25 |
qed "QPair_empty"; |
|
2469 | 26 |
|
9211 | 27 |
Goalw [QPair_def] "<a;b> = <c;d> <-> a=c & b=d"; |
28 |
by (rtac sum_equal_iff 1); |
|
29 |
qed "QPair_iff"; |
|
0 | 30 |
|
9211 | 31 |
bind_thm ("QPair_inject", QPair_iff RS iffD1 RS conjE); |
0 | 32 |
|
2469 | 33 |
Addsimps [QPair_empty, QPair_iff]; |
34 |
AddSEs [QPair_inject]; |
|
35 |
||
9211 | 36 |
Goal "<a;b> = <c;d> ==> a=c"; |
37 |
by (Blast_tac 1) ; |
|
9180 | 38 |
qed "QPair_inject1"; |
0 | 39 |
|
9211 | 40 |
Goal "<a;b> = <c;d> ==> b=d"; |
41 |
by (Blast_tac 1) ; |
|
9180 | 42 |
qed "QPair_inject2"; |
0 | 43 |
|
44 |
||
45 |
(*** QSigma: Disjoint union of a family of sets |
|
46 |
Generalizes Cartesian product ***) |
|
47 |
||
9211 | 48 |
Goalw [QSigma_def] "[| a:A; b:B(a) |] ==> <a;b> : QSigma(A,B)"; |
49 |
by (Blast_tac 1) ; |
|
50 |
qed "QSigmaI"; |
|
2469 | 51 |
|
52 |
AddSIs [QSigmaI]; |
|
0 | 53 |
|
54 |
(*The general elimination rule*) |
|
9211 | 55 |
val major::prems= Goalw [QSigma_def] |
0 | 56 |
"[| c: QSigma(A,B); \ |
57 |
\ !!x y.[| x:A; y:B(x); c=<x;y> |] ==> P \ |
|
9211 | 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"; |
|
0 | 62 |
|
63 |
(** Elimination rules for <a;b>:A*B -- introducing no eigenvariables **) |
|
64 |
||
65 |
val QSigmaE2 = |
|
66 |
rule_by_tactic (REPEAT_FIRST (etac QPair_inject ORELSE' bound_hyp_subst_tac) |
|
1461 | 67 |
THEN prune_params_tac) |
8551 | 68 |
(inst "c" "<a;b>" QSigmaE); |
0 | 69 |
|
9211 | 70 |
AddSEs [QSigmaE2, QSigmaE]; |
71 |
||
72 |
Goal "<a;b> : QSigma(A,B) ==> a : A"; |
|
73 |
by (Blast_tac 1) ; |
|
9180 | 74 |
qed "QSigmaD1"; |
0 | 75 |
|
9211 | 76 |
Goal "<a;b> : QSigma(A,B) ==> b : B(a)"; |
77 |
by (Blast_tac 1) ; |
|
9180 | 78 |
qed "QSigmaD2"; |
0 | 79 |
|
744 | 80 |
|
9211 | 81 |
val prems= Goalw [QSigma_def] |
0 | 82 |
"[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> \ |
9211 | 83 |
\ QSigma(A,B) = QSigma(A',B')"; |
84 |
by (simp_tac (simpset() addsimps prems) 1) ; |
|
85 |
qed "QSigma_cong"; |
|
0 | 86 |
|
9180 | 87 |
Goal "QSigma(0,B) = 0"; |
88 |
by (Blast_tac 1) ; |
|
89 |
qed "QSigma_empty1"; |
|
1096 | 90 |
|
9180 | 91 |
Goal "A <*> 0 = 0"; |
92 |
by (Blast_tac 1) ; |
|
93 |
qed "QSigma_empty2"; |
|
2469 | 94 |
|
95 |
Addsimps [QSigma_empty1, QSigma_empty2]; |
|
0 | 96 |
|
1096 | 97 |
|
98 |
(*** Projections: qfst, qsnd ***) |
|
99 |
||
9211 | 100 |
Goalw [qfst_def] "qfst(<a;b>) = a"; |
101 |
by (Blast_tac 1) ; |
|
102 |
qed "qfst_conv"; |
|
1096 | 103 |
|
9211 | 104 |
Goalw [qsnd_def] "qsnd(<a;b>) = b"; |
105 |
by (Blast_tac 1) ; |
|
106 |
qed "qsnd_conv"; |
|
1096 | 107 |
|
2469 | 108 |
Addsimps [qfst_conv, qsnd_conv]; |
1096 | 109 |
|
9180 | 110 |
Goal "p:QSigma(A,B) ==> qfst(p) : A"; |
111 |
by (Auto_tac) ; |
|
112 |
qed "qfst_type"; |
|
1096 | 113 |
|
9180 | 114 |
Goal "p:QSigma(A,B) ==> qsnd(p) : B(qfst(p))"; |
115 |
by (Auto_tac) ; |
|
116 |
qed "qsnd_type"; |
|
1096 | 117 |
|
5137 | 118 |
Goal "a: QSigma(A,B) ==> <qfst(a); qsnd(a)> = a"; |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4091
diff
changeset
|
119 |
by Auto_tac; |
1096 | 120 |
qed "QPair_qfst_qsnd_eq"; |
0 | 121 |
|
122 |
||
123 |
(*** Eliminator - qsplit ***) |
|
124 |
||
1096 | 125 |
(*A META-equality, so that it applies to higher types as well...*) |
6112 | 126 |
Goalw [qsplit_def] "qsplit(%x y. c(x,y), <a;b>) == c(a,b)"; |
127 |
by (Simp_tac 1); |
|
128 |
qed "qsplit"; |
|
2469 | 129 |
Addsimps [qsplit]; |
130 |
||
9211 | 131 |
val major::prems= Goal |
0 | 132 |
"[| p:QSigma(A,B); \ |
133 |
\ !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x;y>) \ |
|
9180 | 134 |
\ |] ==> qsplit(%x y. c(x,y), p) : C(p)"; |
135 |
by (rtac (major RS QSigmaE) 1); |
|
136 |
by (asm_simp_tac (simpset() addsimps prems) 1) ; |
|
137 |
qed "qsplit_type"; |
|
1096 | 138 |
|
5067 | 139 |
Goalw [qsplit_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
140 |
"u: A<*>B ==> R(qsplit(c,u)) <-> (ALL x:A. ALL y:B. u = <x;y> --> R(c(x,y)))"; |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4091
diff
changeset
|
141 |
by Auto_tac; |
1096 | 142 |
qed "expand_qsplit"; |
143 |
||
144 |
||
145 |
(*** qsplit for predicates: result type o ***) |
|
146 |
||
5137 | 147 |
Goalw [qsplit_def] "R(a,b) ==> qsplit(R, <a;b>)"; |
2469 | 148 |
by (Asm_simp_tac 1); |
1096 | 149 |
qed "qsplitI"; |
150 |
||
9211 | 151 |
val major::sigma::prems = Goalw [qsplit_def] |
1461 | 152 |
"[| qsplit(R,z); z:QSigma(A,B); \ |
153 |
\ !!x y. [| z = <x;y>; R(x,y) |] ==> P \ |
|
1096 | 154 |
\ |] ==> P"; |
155 |
by (rtac (sigma RS QSigmaE) 1); |
|
156 |
by (cut_facts_tac [major] 1); |
|
2469 | 157 |
by (REPEAT (ares_tac prems 1)); |
158 |
by (Asm_full_simp_tac 1); |
|
1096 | 159 |
qed "qsplitE"; |
160 |
||
5137 | 161 |
Goalw [qsplit_def] "qsplit(R,<a;b>) ==> R(a,b)"; |
2469 | 162 |
by (Asm_full_simp_tac 1); |
1096 | 163 |
qed "qsplitD"; |
0 | 164 |
|
165 |
||
166 |
(*** qconverse ***) |
|
167 |
||
9211 | 168 |
Goalw [qconverse_def] "<a;b>:r ==> <b;a>:qconverse(r)"; |
169 |
by (Blast_tac 1) ; |
|
170 |
qed "qconverseI"; |
|
0 | 171 |
|
9211 | 172 |
Goalw [qconverse_def] "<a;b> : qconverse(r) ==> <b;a> : r"; |
173 |
by (Blast_tac 1) ; |
|
174 |
qed "qconverseD"; |
|
0 | 175 |
|
9211 | 176 |
val [major,minor]= Goalw [qconverse_def] |
0 | 177 |
"[| yx : qconverse(r); \ |
178 |
\ !!x y. [| yx=<y;x>; <x;y>:r |] ==> P \ |
|
9211 | 179 |
\ |] ==> P"; |
180 |
by (rtac (major RS ReplaceE) 1); |
|
181 |
by (REPEAT (eresolve_tac [exE, conjE, minor] 1)); |
|
182 |
by (hyp_subst_tac 1); |
|
183 |
by (assume_tac 1) ; |
|
184 |
qed "qconverseE"; |
|
0 | 185 |
|
2469 | 186 |
AddSIs [qconverseI]; |
187 |
AddSEs [qconverseD, qconverseE]; |
|
0 | 188 |
|
9180 | 189 |
Goal "r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r"; |
190 |
by (Blast_tac 1) ; |
|
191 |
qed "qconverse_qconverse"; |
|
192 |
||
193 |
Goal "r <= A <*> B ==> qconverse(r) <= B <*> A"; |
|
194 |
by (Blast_tac 1) ; |
|
195 |
qed "qconverse_type"; |
|
0 | 196 |
|
9180 | 197 |
Goal "qconverse(A <*> B) = B <*> A"; |
198 |
by (Blast_tac 1) ; |
|
199 |
qed "qconverse_prod"; |
|
0 | 200 |
|
9180 | 201 |
Goal "qconverse(0) = 0"; |
202 |
by (Blast_tac 1) ; |
|
203 |
qed "qconverse_empty"; |
|
0 | 204 |
|
205 |
||
206 |
(**** The Quine-inspired notion of disjoint sum ****) |
|
207 |
||
208 |
val qsum_defs = [qsum_def,QInl_def,QInr_def,qcase_def]; |
|
209 |
||
210 |
(** Introduction rules for the injections **) |
|
211 |
||
5137 | 212 |
Goalw qsum_defs "a : A ==> QInl(a) : A <+> B"; |
3016 | 213 |
by (Blast_tac 1); |
760 | 214 |
qed "QInlI"; |
0 | 215 |
|
5137 | 216 |
Goalw qsum_defs "b : B ==> QInr(b) : A <+> B"; |
3016 | 217 |
by (Blast_tac 1); |
760 | 218 |
qed "QInrI"; |
0 | 219 |
|
220 |
(** Elimination rules **) |
|
221 |
||
9211 | 222 |
val major::prems = Goalw qsum_defs |
0 | 223 |
"[| u: A <+> B; \ |
224 |
\ !!x. [| x:A; u=QInl(x) |] ==> P; \ |
|
225 |
\ !!y. [| y:B; u=QInr(y) |] ==> P \ |
|
226 |
\ |] ==> P"; |
|
227 |
by (rtac (major RS UnE) 1); |
|
228 |
by (REPEAT (rtac refl 1 |
|
229 |
ORELSE eresolve_tac (prems@[QSigmaE,singletonE,ssubst]) 1)); |
|
760 | 230 |
qed "qsumE"; |
0 | 231 |
|
2469 | 232 |
AddSIs [QInlI, QInrI]; |
233 |
||
0 | 234 |
(** Injection and freeness equivalences, for rewriting **) |
235 |
||
5067 | 236 |
Goalw qsum_defs "QInl(a)=QInl(b) <-> a=b"; |
2469 | 237 |
by (Simp_tac 1); |
760 | 238 |
qed "QInl_iff"; |
0 | 239 |
|
5067 | 240 |
Goalw qsum_defs "QInr(a)=QInr(b) <-> a=b"; |
2469 | 241 |
by (Simp_tac 1); |
760 | 242 |
qed "QInr_iff"; |
0 | 243 |
|
5067 | 244 |
Goalw qsum_defs "QInl(a)=QInr(b) <-> False"; |
2469 | 245 |
by (Simp_tac 1); |
760 | 246 |
qed "QInl_QInr_iff"; |
0 | 247 |
|
5067 | 248 |
Goalw qsum_defs "QInr(b)=QInl(a) <-> False"; |
2469 | 249 |
by (Simp_tac 1); |
760 | 250 |
qed "QInr_QInl_iff"; |
0 | 251 |
|
5067 | 252 |
Goalw qsum_defs "0<+>0 = 0"; |
2469 | 253 |
by (Simp_tac 1); |
254 |
qed "qsum_empty"; |
|
255 |
||
55 | 256 |
(*Injection and freeness rules*) |
257 |
||
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
258 |
bind_thm ("QInl_inject", (QInl_iff RS iffD1)); |
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
259 |
bind_thm ("QInr_inject", (QInr_iff RS iffD1)); |
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
260 |
bind_thm ("QInl_neq_QInr", (QInl_QInr_iff RS iffD1 RS FalseE)); |
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
261 |
bind_thm ("QInr_neq_QInl", (QInr_QInl_iff RS iffD1 RS FalseE)); |
55 | 262 |
|
2469 | 263 |
AddSEs [qsumE, QInl_neq_QInr, QInr_neq_QInl]; |
264 |
AddSDs [QInl_inject, QInr_inject]; |
|
265 |
Addsimps [QInl_iff, QInr_iff, QInl_QInr_iff, QInr_QInl_iff, qsum_empty]; |
|
0 | 266 |
|
5137 | 267 |
Goal "QInl(a): A<+>B ==> a: A"; |
3016 | 268 |
by (Blast_tac 1); |
760 | 269 |
qed "QInlD"; |
55 | 270 |
|
5137 | 271 |
Goal "QInr(b): A<+>B ==> b: B"; |
3016 | 272 |
by (Blast_tac 1); |
760 | 273 |
qed "QInrD"; |
55 | 274 |
|
0 | 275 |
(** <+> is itself injective... who cares?? **) |
276 |
||
5268 | 277 |
Goal "u: A <+> B <-> (EX x. x:A & u=QInl(x)) | (EX y. y:B & u=QInr(y))"; |
3016 | 278 |
by (Blast_tac 1); |
760 | 279 |
qed "qsum_iff"; |
0 | 280 |
|
5067 | 281 |
Goal "A <+> B <= C <+> D <-> A<=C & B<=D"; |
3016 | 282 |
by (Blast_tac 1); |
760 | 283 |
qed "qsum_subset_iff"; |
0 | 284 |
|
5067 | 285 |
Goal "A <+> B = C <+> D <-> A=C & B=D"; |
4091 | 286 |
by (simp_tac (simpset() addsimps [extension,qsum_subset_iff]) 1); |
3016 | 287 |
by (Blast_tac 1); |
760 | 288 |
qed "qsum_equal_iff"; |
0 | 289 |
|
290 |
(*** Eliminator -- qcase ***) |
|
291 |
||
5067 | 292 |
Goalw qsum_defs "qcase(c, d, QInl(a)) = c(a)"; |
2469 | 293 |
by (Simp_tac 1); |
760 | 294 |
qed "qcase_QInl"; |
0 | 295 |
|
5067 | 296 |
Goalw qsum_defs "qcase(c, d, QInr(b)) = d(b)"; |
2469 | 297 |
by (Simp_tac 1); |
760 | 298 |
qed "qcase_QInr"; |
0 | 299 |
|
2469 | 300 |
Addsimps [qcase_QInl, qcase_QInr]; |
301 |
||
9211 | 302 |
val major::prems = Goal |
0 | 303 |
"[| u: A <+> B; \ |
304 |
\ !!x. x: A ==> c(x): C(QInl(x)); \ |
|
305 |
\ !!y. y: B ==> d(y): C(QInr(y)) \ |
|
306 |
\ |] ==> qcase(c,d,u) : C(u)"; |
|
307 |
by (rtac (major RS qsumE) 1); |
|
308 |
by (ALLGOALS (etac ssubst)); |
|
4091 | 309 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps prems))); |
760 | 310 |
qed "qcase_type"; |
0 | 311 |
|
312 |
(** Rules for the Part primitive **) |
|
313 |
||
5067 | 314 |
Goal "Part(A <+> B,QInl) = {QInl(x). x: A}"; |
3016 | 315 |
by (Blast_tac 1); |
760 | 316 |
qed "Part_QInl"; |
0 | 317 |
|
5067 | 318 |
Goal "Part(A <+> B,QInr) = {QInr(y). y: B}"; |
3016 | 319 |
by (Blast_tac 1); |
760 | 320 |
qed "Part_QInr"; |
0 | 321 |
|
5067 | 322 |
Goal "Part(A <+> B, %x. QInr(h(x))) = {QInr(y). y: Part(B,h)}"; |
3016 | 323 |
by (Blast_tac 1); |
760 | 324 |
qed "Part_QInr2"; |
0 | 325 |
|
5137 | 326 |
Goal "C <= A <+> B ==> Part(C,QInl) Un Part(C,QInr) = C"; |
3016 | 327 |
by (Blast_tac 1); |
760 | 328 |
qed "Part_qsum_equality"; |