author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 46953  2b6e55924af3 
child 58871  c399ae4b836f 
permissions  rwrr 
35762  1 
(* Title: ZF/QPair.thy 
1478  2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  3 
Copyright 1993 University of Cambridge 
4 

13285  5 
Many proofs are borrowed from pair.thy and sum.thy 
6 

7 
Do we EVER have rank(a) < rank(<a;b>) ? Perhaps if the latter rank 

46953  8 
is not a limit ordinal? 
0  9 
*) 
10 

13356  11 
header{*QuineInspired Ordered Pairs and Disjoint Sums*} 
12 

16417  13 
theory QPair imports Sum func begin 
13285  14 

13356  15 
text{*For nonwellfounded data 
16 
structures in ZF. Does not precisely follow Quine's construction. Thanks 

17 
to Thomas Forster for suggesting this approach! 

18 

19 
W. V. Quine, On Ordered Pairs and Relations, in Selected Logic Papers, 

20 
1966. 

21 
*} 

22 

24893  23 
definition 
24 
QPair :: "[i, i] => i" ("<(_;/ _)>") where 

13285  25 
"<a;b> == a+b" 
3923  26 

24893  27 
definition 
28 
qfst :: "i => i" where 

46820  29 
"qfst(p) == THE a. \<exists>b. p=<a;b>" 
13285  30 

24893  31 
definition 
32 
qsnd :: "i => i" where 

46820  33 
"qsnd(p) == THE b. \<exists>a. p=<a;b>" 
13285  34 

24893  35 
definition 
36 
qsplit :: "[[i, i] => 'a, i] => 'a::{}" (*for patternmatching*) where 

13285  37 
"qsplit(c,p) == c(qfst(p), qsnd(p))" 
0  38 

24893  39 
definition 
40 
qconverse :: "i => i" where 

46953  41 
"qconverse(r) == {z. w \<in> r, \<exists>x y. w=<x;y> & z=<y;x>}" 
13285  42 

24893  43 
definition 
44 
QSigma :: "[i, i => i] => i" where 

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13544
diff
changeset

45 
"QSigma(A,B) == \<Union>x\<in>A. \<Union>y\<in>B(x). {<x;y>}" 
0  46 

929
137035296ad6
Moved declarations of @QSUM and <*> to a syntax section.
lcp
parents:
753
diff
changeset

47 
syntax 
46953  48 
"_QSUM" :: "[idt, i, i] => i" ("(3QSUM _ \<in> _./ _)" 10) 
0  49 
translations 
46953  50 
"QSUM x \<in> A. B" => "CONST QSigma(A, %x. B)" 
22808  51 

52 
abbreviation 

53 
qprod (infixr "<*>" 80) where 

54 
"A <*> B == QSigma(A, %_. B)" 

0  55 

24893  56 
definition 
57 
qsum :: "[i,i]=>i" (infixr "<+>" 65) where 

46820  58 
"A <+> B == ({0} <*> A) \<union> ({1} <*> B)" 
3923  59 

24893  60 
definition 
61 
QInl :: "i=>i" where 

13285  62 
"QInl(a) == <0;a>" 
63 

24893  64 
definition 
65 
QInr :: "i=>i" where 

13285  66 
"QInr(b) == <1;b>" 
67 

24893  68 
definition 
69 
qcase :: "[i=>i, i=>i, i]=>i" where 

13285  70 
"qcase(c,d) == qsplit(%y z. cond(y, d(z), c(z)))" 
71 

72 

13356  73 
subsection{*Quine ordered pairing*} 
13285  74 

75 
(** Lemmas for showing that <a;b> uniquely determines a and b **) 

76 

77 
lemma QPair_empty [simp]: "<0;0> = 0" 

78 
by (simp add: QPair_def) 

79 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

80 
lemma QPair_iff [simp]: "<a;b> = <c;d> \<longleftrightarrow> a=c & b=d" 
13285  81 
apply (simp add: QPair_def) 
82 
apply (rule sum_equal_iff) 

83 
done 

84 

45602  85 
lemmas QPair_inject = QPair_iff [THEN iffD1, THEN conjE, elim!] 
13285  86 

87 
lemma QPair_inject1: "<a;b> = <c;d> ==> a=c" 

88 
by blast 

89 

90 
lemma QPair_inject2: "<a;b> = <c;d> ==> b=d" 

91 
by blast 

92 

93 

13356  94 
subsubsection{*QSigma: Disjoint union of a family of sets 
95 
Generalizes Cartesian product*} 

13285  96 

46953  97 
lemma QSigmaI [intro!]: "[ a \<in> A; b \<in> B(a) ] ==> <a;b> \<in> QSigma(A,B)" 
13285  98 
by (simp add: QSigma_def) 
99 

100 

101 
(** Elimination rules for <a;b>:A*B  introducing no eigenvariables **) 

102 

103 
lemma QSigmaE [elim!]: 

46953  104 
"[ c \<in> QSigma(A,B); 
105 
!!x y.[ x \<in> A; y \<in> B(x); c=<x;y> ] ==> P 

13285  106 
] ==> P" 
46953  107 
by (simp add: QSigma_def, blast) 
13285  108 

109 
lemma QSigmaE2 [elim!]: 

46953  110 
"[ <a;b>: QSigma(A,B); [ a \<in> A; b \<in> B(a) ] ==> P ] ==> P" 
111 
by (simp add: QSigma_def) 

13285  112 

46820  113 
lemma QSigmaD1: "<a;b> \<in> QSigma(A,B) ==> a \<in> A" 
13285  114 
by blast 
115 

46820  116 
lemma QSigmaD2: "<a;b> \<in> QSigma(A,B) ==> b \<in> B(a)" 
13285  117 
by blast 
118 

119 
lemma QSigma_cong: 

46953  120 
"[ A=A'; !!x. x \<in> A' ==> B(x)=B'(x) ] ==> 
13285  121 
QSigma(A,B) = QSigma(A',B')" 
46953  122 
by (simp add: QSigma_def) 
13285  123 

124 
lemma QSigma_empty1 [simp]: "QSigma(0,B) = 0" 

125 
by blast 

126 

127 
lemma QSigma_empty2 [simp]: "A <*> 0 = 0" 

128 
by blast 

129 

130 

13356  131 
subsubsection{*Projections: qfst, qsnd*} 
13285  132 

133 
lemma qfst_conv [simp]: "qfst(<a;b>) = a" 

13544  134 
by (simp add: qfst_def) 
13285  135 

136 
lemma qsnd_conv [simp]: "qsnd(<a;b>) = b" 

13544  137 
by (simp add: qsnd_def) 
13285  138 

46953  139 
lemma qfst_type [TC]: "p \<in> QSigma(A,B) ==> qfst(p) \<in> A" 
13285  140 
by auto 
141 

46953  142 
lemma qsnd_type [TC]: "p \<in> QSigma(A,B) ==> qsnd(p) \<in> B(qfst(p))" 
13285  143 
by auto 
144 

46953  145 
lemma QPair_qfst_qsnd_eq: "a \<in> QSigma(A,B) ==> <qfst(a); qsnd(a)> = a" 
13285  146 
by auto 
147 

148 

13356  149 
subsubsection{*Eliminator: qsplit*} 
13285  150 

151 
(*A METAequality, so that it applies to higher types as well...*) 

152 
lemma qsplit [simp]: "qsplit(%x y. c(x,y), <a;b>) == c(a,b)" 

153 
by (simp add: qsplit_def) 

154 

155 

156 
lemma qsplit_type [elim!]: 

46953  157 
"[ p \<in> QSigma(A,B); 
158 
!!x y.[ x \<in> A; y \<in> B(x) ] ==> c(x,y):C(<x;y>) 

46820  159 
] ==> qsplit(%x y. c(x,y), p) \<in> C(p)" 
46953  160 
by auto 
13285  161 

46953  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)))" 

13285  164 
apply (simp add: qsplit_def, auto) 
165 
done 

166 

167 

13356  168 
subsubsection{*qsplit for predicates: result type o*} 
13285  169 

170 
lemma qsplitI: "R(a,b) ==> qsplit(R, <a;b>)" 

171 
by (simp add: qsplit_def) 

172 

173 

174 
lemma qsplitE: 

46953  175 
"[ qsplit(R,z); z \<in> QSigma(A,B); 
176 
!!x y. [ z = <x;y>; R(x,y) ] ==> P 

13285  177 
] ==> P" 
46953  178 
by (simp add: qsplit_def, auto) 
13285  179 

180 
lemma qsplitD: "qsplit(R,<a;b>) ==> R(a,b)" 

181 
by (simp add: qsplit_def) 

182 

183 

13356  184 
subsubsection{*qconverse*} 
13285  185 

186 
lemma qconverseI [intro!]: "<a;b>:r ==> <b;a>:qconverse(r)" 

187 
by (simp add: qconverse_def, blast) 

188 

46820  189 
lemma qconverseD [elim!]: "<a;b> \<in> qconverse(r) ==> <b;a> \<in> r" 
13285  190 
by (simp add: qconverse_def, blast) 
191 

192 
lemma qconverseE [elim!]: 

46953  193 
"[ yx \<in> qconverse(r); 
194 
!!x y. [ yx=<y;x>; <x;y>:r ] ==> P 

13285  195 
] ==> P" 
46953  196 
by (simp add: qconverse_def, blast) 
13285  197 

198 
lemma qconverse_qconverse: "r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r" 

199 
by blast 

200 

46820  201 
lemma qconverse_type: "r \<subseteq> A <*> B ==> qconverse(r) \<subseteq> B <*> A" 
13285  202 
by blast 
203 

204 
lemma qconverse_prod: "qconverse(A <*> B) = B <*> A" 

205 
by blast 

206 

207 
lemma qconverse_empty: "qconverse(0) = 0" 

208 
by blast 

209 

210 

13356  211 
subsection{*The Quineinspired notion of disjoint sum*} 
13285  212 

213 
lemmas qsum_defs = qsum_def QInl_def QInr_def qcase_def 

214 

215 
(** Introduction rules for the injections **) 

216 

46820  217 
lemma QInlI [intro!]: "a \<in> A ==> QInl(a) \<in> A <+> B" 
13285  218 
by (simp add: qsum_defs, blast) 
1097
01379c46ad2d
Changed definitions so that qsplit is now defined in terms of
lcp
parents:
929
diff
changeset

219 

46820  220 
lemma QInrI [intro!]: "b \<in> B ==> QInr(b) \<in> A <+> B" 
13285  221 
by (simp add: qsum_defs, blast) 
222 

223 
(** Elimination rules **) 

224 

225 
lemma qsumE [elim!]: 

46953  226 
"[ u \<in> A <+> B; 
227 
!!x. [ x \<in> A; u=QInl(x) ] ==> P; 

228 
!!y. [ y \<in> B; u=QInr(y) ] ==> P 

13285  229 
] ==> P" 
46953  230 
by (simp add: qsum_defs, blast) 
13285  231 

232 

233 
(** Injection and freeness equivalences, for rewriting **) 

234 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

235 
lemma QInl_iff [iff]: "QInl(a)=QInl(b) \<longleftrightarrow> a=b" 
13285  236 
by (simp add: qsum_defs ) 
237 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

238 
lemma QInr_iff [iff]: "QInr(a)=QInr(b) \<longleftrightarrow> a=b" 
13285  239 
by (simp add: qsum_defs ) 
240 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

241 
lemma QInl_QInr_iff [simp]: "QInl(a)=QInr(b) \<longleftrightarrow> False" 
13285  242 
by (simp add: qsum_defs ) 
243 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

244 
lemma QInr_QInl_iff [simp]: "QInr(b)=QInl(a) \<longleftrightarrow> False" 
13285  245 
by (simp add: qsum_defs ) 
246 

247 
lemma qsum_empty [simp]: "0<+>0 = 0" 

248 
by (simp add: qsum_defs ) 

249 

250 
(*Injection and freeness rules*) 

251 

45602  252 
lemmas QInl_inject = QInl_iff [THEN iffD1] 
253 
lemmas QInr_inject = QInr_iff [THEN iffD1] 

13823  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!] 

13285  256 

46953  257 
lemma QInlD: "QInl(a): A<+>B ==> a \<in> A" 
13285  258 
by blast 
259 

46953  260 
lemma QInrD: "QInr(b): A<+>B ==> b \<in> B" 
13285  261 
by blast 
262 

263 
(** <+> is itself injective... who cares?? **) 

264 

265 
lemma qsum_iff: 

46953  266 
"u \<in> A <+> B \<longleftrightarrow> (\<exists>x. x \<in> A & u=QInl(x))  (\<exists>y. y \<in> B & u=QInr(y))" 
13356  267 
by blast 
13285  268 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

269 
lemma qsum_subset_iff: "A <+> B \<subseteq> C <+> D \<longleftrightarrow> A<=C & B<=D" 
13285  270 
by blast 
271 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

272 
lemma qsum_equal_iff: "A <+> B = C <+> D \<longleftrightarrow> A=C & B=D" 
13285  273 
apply (simp (no_asm) add: extension qsum_subset_iff) 
274 
apply blast 

275 
done 

276 

13356  277 
subsubsection{*Eliminator  qcase*} 
13285  278 

279 
lemma qcase_QInl [simp]: "qcase(c, d, QInl(a)) = c(a)" 

280 
by (simp add: qsum_defs ) 

281 

282 

283 
lemma qcase_QInr [simp]: "qcase(c, d, QInr(b)) = d(b)" 

284 
by (simp add: qsum_defs ) 

285 

286 
lemma qcase_type: 

46953  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)) 

46820  290 
] ==> qcase(c,d,u) \<in> C(u)" 
46953  291 
by (simp add: qsum_defs, auto) 
13285  292 

293 
(** Rules for the Part primitive **) 

294 

46953  295 
lemma Part_QInl: "Part(A <+> B,QInl) = {QInl(x). x \<in> A}" 
13285  296 
by blast 
297 

46953  298 
lemma Part_QInr: "Part(A <+> B,QInr) = {QInr(y). y \<in> B}" 
13285  299 
by blast 
300 

46953  301 
lemma Part_QInr2: "Part(A <+> B, %x. QInr(h(x))) = {QInr(y). y \<in> Part(B,h)}" 
13285  302 
by blast 
0  303 

46820  304 
lemma Part_qsum_equality: "C \<subseteq> A <+> B ==> Part(C,QInl) \<union> Part(C,QInr) = C" 
13285  305 
by blast 
306 

307 

13356  308 
subsubsection{*Monotonicity*} 
13285  309 

46820  310 
lemma QPair_mono: "[ a<=c; b<=d ] ==> <a;b> \<subseteq> <c;d>" 
13285  311 
by (simp add: QPair_def sum_mono) 
312 

313 
lemma QSigma_mono [rule_format]: 

46820  314 
"[ A<=C; \<forall>x\<in>A. B(x) \<subseteq> D(x) ] ==> QSigma(A,B) \<subseteq> QSigma(C,D)" 
13285  315 
by blast 
316 

46820  317 
lemma QInl_mono: "a<=b ==> QInl(a) \<subseteq> QInl(b)" 
13285  318 
by (simp add: QInl_def subset_refl [THEN QPair_mono]) 
319 

46820  320 
lemma QInr_mono: "a<=b ==> QInr(a) \<subseteq> QInr(b)" 
13285  321 
by (simp add: QInr_def subset_refl [THEN QPair_mono]) 
322 

46820  323 
lemma qsum_mono: "[ A<=C; B<=D ] ==> A <+> B \<subseteq> C <+> D" 
13285  324 
by blast 
325 

0  326 
end 