equal
deleted
inserted
replaced
6 |
6 |
7 Do we EVER have rank(a) < rank(<a;b>) ? Perhaps if the latter rank |
7 Do we EVER have rank(a) < rank(<a;b>) ? Perhaps if the latter rank |
8 is not a limit ordinal? |
8 is not a limit ordinal? |
9 *) |
9 *) |
10 |
10 |
11 section{*Quine-Inspired Ordered Pairs and Disjoint Sums*} |
11 section\<open>Quine-Inspired Ordered Pairs and Disjoint Sums\<close> |
12 |
12 |
13 theory QPair imports Sum func begin |
13 theory QPair imports Sum func begin |
14 |
14 |
15 text{*For non-well-founded data |
15 text\<open>For non-well-founded data |
16 structures in ZF. Does not precisely follow Quine's construction. Thanks |
16 structures in ZF. Does not precisely follow Quine's construction. Thanks |
17 to Thomas Forster for suggesting this approach! |
17 to Thomas Forster for suggesting this approach! |
18 |
18 |
19 W. V. Quine, On Ordered Pairs and Relations, in Selected Logic Papers, |
19 W. V. Quine, On Ordered Pairs and Relations, in Selected Logic Papers, |
20 1966. |
20 1966. |
21 *} |
21 \<close> |
22 |
22 |
23 definition |
23 definition |
24 QPair :: "[i, i] => i" ("<(_;/ _)>") where |
24 QPair :: "[i, i] => i" ("<(_;/ _)>") where |
25 "<a;b> == a+b" |
25 "<a;b> == a+b" |
26 |
26 |
68 definition |
68 definition |
69 qcase :: "[i=>i, i=>i, i]=>i" where |
69 qcase :: "[i=>i, i=>i, i]=>i" where |
70 "qcase(c,d) == qsplit(%y z. cond(y, d(z), c(z)))" |
70 "qcase(c,d) == qsplit(%y z. cond(y, d(z), c(z)))" |
71 |
71 |
72 |
72 |
73 subsection{*Quine ordered pairing*} |
73 subsection\<open>Quine ordered pairing\<close> |
74 |
74 |
75 (** Lemmas for showing that <a;b> uniquely determines a and b **) |
75 (** Lemmas for showing that <a;b> uniquely determines a and b **) |
76 |
76 |
77 lemma QPair_empty [simp]: "<0;0> = 0" |
77 lemma QPair_empty [simp]: "<0;0> = 0" |
78 by (simp add: QPair_def) |
78 by (simp add: QPair_def) |
89 |
89 |
90 lemma QPair_inject2: "<a;b> = <c;d> ==> b=d" |
90 lemma QPair_inject2: "<a;b> = <c;d> ==> b=d" |
91 by blast |
91 by blast |
92 |
92 |
93 |
93 |
94 subsubsection{*QSigma: Disjoint union of a family of sets |
94 subsubsection\<open>QSigma: Disjoint union of a family of sets |
95 Generalizes Cartesian product*} |
95 Generalizes Cartesian product\<close> |
96 |
96 |
97 lemma QSigmaI [intro!]: "[| a \<in> A; b \<in> B(a) |] ==> <a;b> \<in> QSigma(A,B)" |
97 lemma QSigmaI [intro!]: "[| a \<in> A; b \<in> B(a) |] ==> <a;b> \<in> QSigma(A,B)" |
98 by (simp add: QSigma_def) |
98 by (simp add: QSigma_def) |
99 |
99 |
100 |
100 |
126 |
126 |
127 lemma QSigma_empty2 [simp]: "A <*> 0 = 0" |
127 lemma QSigma_empty2 [simp]: "A <*> 0 = 0" |
128 by blast |
128 by blast |
129 |
129 |
130 |
130 |
131 subsubsection{*Projections: qfst, qsnd*} |
131 subsubsection\<open>Projections: qfst, qsnd\<close> |
132 |
132 |
133 lemma qfst_conv [simp]: "qfst(<a;b>) = a" |
133 lemma qfst_conv [simp]: "qfst(<a;b>) = a" |
134 by (simp add: qfst_def) |
134 by (simp add: qfst_def) |
135 |
135 |
136 lemma qsnd_conv [simp]: "qsnd(<a;b>) = b" |
136 lemma qsnd_conv [simp]: "qsnd(<a;b>) = b" |
144 |
144 |
145 lemma QPair_qfst_qsnd_eq: "a \<in> QSigma(A,B) ==> <qfst(a); qsnd(a)> = a" |
145 lemma QPair_qfst_qsnd_eq: "a \<in> QSigma(A,B) ==> <qfst(a); qsnd(a)> = a" |
146 by auto |
146 by auto |
147 |
147 |
148 |
148 |
149 subsubsection{*Eliminator: qsplit*} |
149 subsubsection\<open>Eliminator: qsplit\<close> |
150 |
150 |
151 (*A META-equality, so that it applies to higher types as well...*) |
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)" |
152 lemma qsplit [simp]: "qsplit(%x y. c(x,y), <a;b>) == c(a,b)" |
153 by (simp add: qsplit_def) |
153 by (simp add: qsplit_def) |
154 |
154 |
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)))" |
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) |
164 apply (simp add: qsplit_def, auto) |
165 done |
165 done |
166 |
166 |
167 |
167 |
168 subsubsection{*qsplit for predicates: result type o*} |
168 subsubsection\<open>qsplit for predicates: result type o\<close> |
169 |
169 |
170 lemma qsplitI: "R(a,b) ==> qsplit(R, <a;b>)" |
170 lemma qsplitI: "R(a,b) ==> qsplit(R, <a;b>)" |
171 by (simp add: qsplit_def) |
171 by (simp add: qsplit_def) |
172 |
172 |
173 |
173 |
179 |
179 |
180 lemma qsplitD: "qsplit(R,<a;b>) ==> R(a,b)" |
180 lemma qsplitD: "qsplit(R,<a;b>) ==> R(a,b)" |
181 by (simp add: qsplit_def) |
181 by (simp add: qsplit_def) |
182 |
182 |
183 |
183 |
184 subsubsection{*qconverse*} |
184 subsubsection\<open>qconverse\<close> |
185 |
185 |
186 lemma qconverseI [intro!]: "<a;b>:r ==> <b;a>:qconverse(r)" |
186 lemma qconverseI [intro!]: "<a;b>:r ==> <b;a>:qconverse(r)" |
187 by (simp add: qconverse_def, blast) |
187 by (simp add: qconverse_def, blast) |
188 |
188 |
189 lemma qconverseD [elim!]: "<a;b> \<in> qconverse(r) ==> <b;a> \<in> r" |
189 lemma qconverseD [elim!]: "<a;b> \<in> qconverse(r) ==> <b;a> \<in> r" |
206 |
206 |
207 lemma qconverse_empty: "qconverse(0) = 0" |
207 lemma qconverse_empty: "qconverse(0) = 0" |
208 by blast |
208 by blast |
209 |
209 |
210 |
210 |
211 subsection{*The Quine-inspired notion of disjoint sum*} |
211 subsection\<open>The Quine-inspired notion of disjoint sum\<close> |
212 |
212 |
213 lemmas qsum_defs = qsum_def QInl_def QInr_def qcase_def |
213 lemmas qsum_defs = qsum_def QInl_def QInr_def qcase_def |
214 |
214 |
215 (** Introduction rules for the injections **) |
215 (** Introduction rules for the injections **) |
216 |
216 |
272 lemma qsum_equal_iff: "A <+> B = C <+> D \<longleftrightarrow> A=C & B=D" |
272 lemma qsum_equal_iff: "A <+> B = C <+> D \<longleftrightarrow> A=C & B=D" |
273 apply (simp (no_asm) add: extension qsum_subset_iff) |
273 apply (simp (no_asm) add: extension qsum_subset_iff) |
274 apply blast |
274 apply blast |
275 done |
275 done |
276 |
276 |
277 subsubsection{*Eliminator -- qcase*} |
277 subsubsection\<open>Eliminator -- qcase\<close> |
278 |
278 |
279 lemma qcase_QInl [simp]: "qcase(c, d, QInl(a)) = c(a)" |
279 lemma qcase_QInl [simp]: "qcase(c, d, QInl(a)) = c(a)" |
280 by (simp add: qsum_defs ) |
280 by (simp add: qsum_defs ) |
281 |
281 |
282 |
282 |
303 |
303 |
304 lemma Part_qsum_equality: "C \<subseteq> A <+> B ==> Part(C,QInl) \<union> Part(C,QInr) = C" |
304 lemma Part_qsum_equality: "C \<subseteq> A <+> B ==> Part(C,QInl) \<union> Part(C,QInr) = C" |
305 by blast |
305 by blast |
306 |
306 |
307 |
307 |
308 subsubsection{*Monotonicity*} |
308 subsubsection\<open>Monotonicity\<close> |
309 |
309 |
310 lemma QPair_mono: "[| a<=c; b<=d |] ==> <a;b> \<subseteq> <c;d>" |
310 lemma QPair_mono: "[| a<=c; b<=d |] ==> <a;b> \<subseteq> <c;d>" |
311 by (simp add: QPair_def sum_mono) |
311 by (simp add: QPair_def sum_mono) |
312 |
312 |
313 lemma QSigma_mono [rule_format]: |
313 lemma QSigma_mono [rule_format]: |