src/ZF/QPair.thy
 author wenzelm Mon Dec 04 22:54:31 2017 +0100 (20 months ago) changeset 67131 85d10959c2e4 parent 60770 240563fbf41d child 69587 53982d5ec0bb permissions -rw-r--r--
tuned signature;
1 (*  Title:      ZF/QPair.thy
2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3     Copyright   1993  University of Cambridge
5 Many proofs are borrowed from pair.thy and sum.thy
7 Do we EVER have rank(a) < rank(<a;b>) ?  Perhaps if the latter rank
8 is not a limit ordinal?
9 *)
11 section\<open>Quine-Inspired Ordered Pairs and Disjoint Sums\<close>
13 theory QPair imports Sum func begin
15 text\<open>For non-well-founded data
16 structures in ZF.  Does not precisely follow Quine's construction.  Thanks
17 to Thomas Forster for suggesting this approach!
19 W. V. Quine, On Ordered Pairs and Relations, in Selected Logic Papers,
20 1966.
21 \<close>
23 definition
24   QPair     :: "[i, i] => i"                      ("<(_;/ _)>")  where
25     "<a;b> == a+b"
27 definition
28   qfst :: "i => i"  where
29     "qfst(p) == THE a. \<exists>b. p=<a;b>"
31 definition
32   qsnd :: "i => i"  where
33     "qsnd(p) == THE b. \<exists>a. p=<a;b>"
35 definition
36   qsplit    :: "[[i, i] => 'a, i] => 'a::{}"  (*for pattern-matching*)  where
37     "qsplit(c,p) == c(qfst(p), qsnd(p))"
39 definition
40   qconverse :: "i => i"  where
41     "qconverse(r) == {z. w \<in> r, \<exists>x y. w=<x;y> & z=<y;x>}"
43 definition
44   QSigma    :: "[i, i => i] => i"  where
45     "QSigma(A,B)  ==  \<Union>x\<in>A. \<Union>y\<in>B(x). {<x;y>}"
47 syntax
48   "_QSUM"   :: "[idt, i, i] => i"               ("(3QSUM _ \<in> _./ _)" 10)
49 translations
50   "QSUM x \<in> A. B"  => "CONST QSigma(A, %x. B)"
52 abbreviation
53   qprod  (infixr "<*>" 80) where
54   "A <*> B == QSigma(A, %_. B)"
56 definition
57   qsum    :: "[i,i]=>i"                         (infixr "<+>" 65)  where
58     "A <+> B      == ({0} <*> A) \<union> ({1} <*> B)"
60 definition
61   QInl :: "i=>i"  where
62     "QInl(a)      == <0;a>"
64 definition
65   QInr :: "i=>i"  where
66     "QInr(b)      == <1;b>"
68 definition
69   qcase     :: "[i=>i, i=>i, i]=>i"  where
70     "qcase(c,d)   == qsplit(%y z. cond(y, d(z), c(z)))"
73 subsection\<open>Quine ordered pairing\<close>
75 (** Lemmas for showing that <a;b> uniquely determines a and b **)
77 lemma QPair_empty [simp]: "<0;0> = 0"
80 lemma QPair_iff [simp]: "<a;b> = <c;d> \<longleftrightarrow> a=c & b=d"
82 apply (rule sum_equal_iff)
83 done
85 lemmas QPair_inject = QPair_iff [THEN iffD1, THEN conjE, elim!]
87 lemma QPair_inject1: "<a;b> = <c;d> ==> a=c"
88 by blast
90 lemma QPair_inject2: "<a;b> = <c;d> ==> b=d"
91 by blast
94 subsubsection\<open>QSigma: Disjoint union of a family of sets
95      Generalizes Cartesian product\<close>
97 lemma QSigmaI [intro!]: "[| a \<in> A;  b \<in> B(a) |] ==> <a;b> \<in> QSigma(A,B)"
101 (** Elimination rules for <a;b>:A*B -- introducing no eigenvariables **)
103 lemma QSigmaE [elim!]:
104     "[| c \<in> QSigma(A,B);
105         !!x y.[| x \<in> A;  y \<in> B(x);  c=<x;y> |] ==> P
106      |] ==> P"
107 by (simp add: QSigma_def, blast)
109 lemma QSigmaE2 [elim!]:
110     "[| <a;b>: QSigma(A,B); [| a \<in> A;  b \<in> B(a) |] ==> P |] ==> P"
113 lemma QSigmaD1: "<a;b> \<in> QSigma(A,B) ==> a \<in> A"
114 by blast
116 lemma QSigmaD2: "<a;b> \<in> QSigma(A,B) ==> b \<in> B(a)"
117 by blast
119 lemma QSigma_cong:
120     "[| A=A';  !!x. x \<in> A' ==> B(x)=B'(x) |] ==>
121      QSigma(A,B) = QSigma(A',B')"
124 lemma QSigma_empty1 [simp]: "QSigma(0,B) = 0"
125 by blast
127 lemma QSigma_empty2 [simp]: "A <*> 0 = 0"
128 by blast
131 subsubsection\<open>Projections: qfst, qsnd\<close>
133 lemma qfst_conv [simp]: "qfst(<a;b>) = a"
136 lemma qsnd_conv [simp]: "qsnd(<a;b>) = b"
139 lemma qfst_type [TC]: "p \<in> QSigma(A,B) ==> qfst(p) \<in> A"
140 by auto
142 lemma qsnd_type [TC]: "p \<in> QSigma(A,B) ==> qsnd(p) \<in> B(qfst(p))"
143 by auto
145 lemma QPair_qfst_qsnd_eq: "a \<in> QSigma(A,B) ==> <qfst(a); qsnd(a)> = a"
146 by auto
149 subsubsection\<open>Eliminator: qsplit\<close>
151 (*A META-equality, so that it applies to higher types as well...*)
152 lemma qsplit [simp]: "qsplit(%x y. c(x,y), <a;b>) == c(a,b)"
156 lemma qsplit_type [elim!]:
157     "[|  p \<in> QSigma(A,B);
158          !!x y.[| x \<in> A; y \<in> B(x) |] ==> c(x,y):C(<x;y>)
159      |] ==> qsplit(%x y. c(x,y), p) \<in> C(p)"
160 by auto
162 lemma expand_qsplit:
163  "u \<in> A<*>B ==> R(qsplit(c,u)) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. u = <x;y> \<longrightarrow> R(c(x,y)))"
164 apply (simp add: qsplit_def, auto)
165 done
168 subsubsection\<open>qsplit for predicates: result type o\<close>
170 lemma qsplitI: "R(a,b) ==> qsplit(R, <a;b>)"
174 lemma qsplitE:
175     "[| qsplit(R,z);  z \<in> QSigma(A,B);
176         !!x y. [| z = <x;y>;  R(x,y) |] ==> P
177     |] ==> P"
178 by (simp add: qsplit_def, auto)
180 lemma qsplitD: "qsplit(R,<a;b>) ==> R(a,b)"
184 subsubsection\<open>qconverse\<close>
186 lemma qconverseI [intro!]: "<a;b>:r ==> <b;a>:qconverse(r)"
187 by (simp add: qconverse_def, blast)
189 lemma qconverseD [elim!]: "<a;b> \<in> qconverse(r) ==> <b;a> \<in> r"
190 by (simp add: qconverse_def, blast)
192 lemma qconverseE [elim!]:
193     "[| yx \<in> qconverse(r);
194         !!x y. [| yx=<y;x>;  <x;y>:r |] ==> P
195      |] ==> P"
196 by (simp add: qconverse_def, blast)
198 lemma qconverse_qconverse: "r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r"
199 by blast
201 lemma qconverse_type: "r \<subseteq> A <*> B ==> qconverse(r) \<subseteq> B <*> A"
202 by blast
204 lemma qconverse_prod: "qconverse(A <*> B) = B <*> A"
205 by blast
207 lemma qconverse_empty: "qconverse(0) = 0"
208 by blast
211 subsection\<open>The Quine-inspired notion of disjoint sum\<close>
213 lemmas qsum_defs = qsum_def QInl_def QInr_def qcase_def
215 (** Introduction rules for the injections **)
217 lemma QInlI [intro!]: "a \<in> A ==> QInl(a) \<in> A <+> B"
218 by (simp add: qsum_defs, blast)
220 lemma QInrI [intro!]: "b \<in> B ==> QInr(b) \<in> A <+> B"
221 by (simp add: qsum_defs, blast)
223 (** Elimination rules **)
225 lemma qsumE [elim!]:
226     "[| u \<in> A <+> B;
227         !!x. [| x \<in> A;  u=QInl(x) |] ==> P;
228         !!y. [| y \<in> B;  u=QInr(y) |] ==> P
229      |] ==> P"
230 by (simp add: qsum_defs, blast)
233 (** Injection and freeness equivalences, for rewriting **)
235 lemma QInl_iff [iff]: "QInl(a)=QInl(b) \<longleftrightarrow> a=b"
236 by (simp add: qsum_defs )
238 lemma QInr_iff [iff]: "QInr(a)=QInr(b) \<longleftrightarrow> a=b"
239 by (simp add: qsum_defs )
241 lemma QInl_QInr_iff [simp]: "QInl(a)=QInr(b) \<longleftrightarrow> False"
242 by (simp add: qsum_defs )
244 lemma QInr_QInl_iff [simp]: "QInr(b)=QInl(a) \<longleftrightarrow> False"
245 by (simp add: qsum_defs )
247 lemma qsum_empty [simp]: "0<+>0 = 0"
248 by (simp add: qsum_defs )
250 (*Injection and freeness rules*)
252 lemmas QInl_inject = QInl_iff [THEN iffD1]
253 lemmas QInr_inject = QInr_iff [THEN iffD1]
254 lemmas QInl_neq_QInr = QInl_QInr_iff [THEN iffD1, THEN FalseE, elim!]
255 lemmas QInr_neq_QInl = QInr_QInl_iff [THEN iffD1, THEN FalseE, elim!]
257 lemma QInlD: "QInl(a): A<+>B ==> a \<in> A"
258 by blast
260 lemma QInrD: "QInr(b): A<+>B ==> b \<in> B"
261 by blast
263 (** <+> is itself injective... who cares?? **)
265 lemma qsum_iff:
266      "u \<in> A <+> B \<longleftrightarrow> (\<exists>x. x \<in> A & u=QInl(x)) | (\<exists>y. y \<in> B & u=QInr(y))"
267 by blast
269 lemma qsum_subset_iff: "A <+> B \<subseteq> C <+> D \<longleftrightarrow> A<=C & B<=D"
270 by blast
272 lemma qsum_equal_iff: "A <+> B = C <+> D \<longleftrightarrow> A=C & B=D"
273 apply (simp (no_asm) add: extension qsum_subset_iff)
274 apply blast
275 done
277 subsubsection\<open>Eliminator -- qcase\<close>
279 lemma qcase_QInl [simp]: "qcase(c, d, QInl(a)) = c(a)"
280 by (simp add: qsum_defs )
283 lemma qcase_QInr [simp]: "qcase(c, d, QInr(b)) = d(b)"
284 by (simp add: qsum_defs )
286 lemma qcase_type:
287     "[| u \<in> A <+> B;
288         !!x. x \<in> A ==> c(x): C(QInl(x));
289         !!y. y \<in> B ==> d(y): C(QInr(y))
290      |] ==> qcase(c,d,u) \<in> C(u)"
291 by (simp add: qsum_defs, auto)
293 (** Rules for the Part primitive **)
295 lemma Part_QInl: "Part(A <+> B,QInl) = {QInl(x). x \<in> A}"
296 by blast
298 lemma Part_QInr: "Part(A <+> B,QInr) = {QInr(y). y \<in> B}"
299 by blast
301 lemma Part_QInr2: "Part(A <+> B, %x. QInr(h(x))) = {QInr(y). y \<in> Part(B,h)}"
302 by blast
304 lemma Part_qsum_equality: "C \<subseteq> A <+> B ==> Part(C,QInl) \<union> Part(C,QInr) = C"
305 by blast
308 subsubsection\<open>Monotonicity\<close>
310 lemma QPair_mono: "[| a<=c;  b<=d |] ==> <a;b> \<subseteq> <c;d>"
311 by (simp add: QPair_def sum_mono)
313 lemma QSigma_mono [rule_format]:
314      "[| A<=C;  \<forall>x\<in>A. B(x) \<subseteq> D(x) |] ==> QSigma(A,B) \<subseteq> QSigma(C,D)"
315 by blast
317 lemma QInl_mono: "a<=b ==> QInl(a) \<subseteq> QInl(b)"
318 by (simp add: QInl_def subset_refl [THEN QPair_mono])
320 lemma QInr_mono: "a<=b ==> QInr(a) \<subseteq> QInr(b)"
321 by (simp add: QInr_def subset_refl [THEN QPair_mono])
323 lemma qsum_mono: "[| A<=C;  B<=D |] ==> A <+> B \<subseteq> C <+> D"
324 by blast
326 end