--- a/src/ZF/QPair.thy Thu Mar 15 15:54:22 2012 +0000
+++ b/src/ZF/QPair.thy Thu Mar 15 16:35:02 2012 +0000
@@ -5,7 +5,7 @@
Many proofs are borrowed from pair.thy and sum.thy
Do we EVER have rank(a) < rank(<a;b>) ? Perhaps if the latter rank
-is not a limit ordinal?
+is not a limit ordinal?
*)
header{*Quine-Inspired Ordered Pairs and Disjoint Sums*}
@@ -38,16 +38,16 @@
definition
qconverse :: "i => i" where
- "qconverse(r) == {z. w:r, \<exists>x y. w=<x;y> & z=<y;x>}"
+ "qconverse(r) == {z. w \<in> r, \<exists>x y. w=<x;y> & z=<y;x>}"
definition
QSigma :: "[i, i => i] => i" where
"QSigma(A,B) == \<Union>x\<in>A. \<Union>y\<in>B(x). {<x;y>}"
syntax
- "_QSUM" :: "[idt, i, i] => i" ("(3QSUM _:_./ _)" 10)
+ "_QSUM" :: "[idt, i, i] => i" ("(3QSUM _ \<in> _./ _)" 10)
translations
- "QSUM x:A. B" => "CONST QSigma(A, %x. B)"
+ "QSUM x \<in> A. B" => "CONST QSigma(A, %x. B)"
abbreviation
qprod (infixr "<*>" 80) where
@@ -94,21 +94,21 @@
subsubsection{*QSigma: Disjoint union of a family of sets
Generalizes Cartesian product*}
-lemma QSigmaI [intro!]: "[| a:A; b:B(a) |] ==> <a;b> \<in> QSigma(A,B)"
+lemma QSigmaI [intro!]: "[| a \<in> A; b \<in> B(a) |] ==> <a;b> \<in> QSigma(A,B)"
by (simp add: QSigma_def)
(** Elimination rules for <a;b>:A*B -- introducing no eigenvariables **)
lemma QSigmaE [elim!]:
- "[| c: QSigma(A,B);
- !!x y.[| x:A; y:B(x); c=<x;y> |] ==> P
+ "[| c \<in> QSigma(A,B);
+ !!x y.[| x \<in> A; y \<in> B(x); c=<x;y> |] ==> P
|] ==> P"
-by (simp add: QSigma_def, blast)
+by (simp add: QSigma_def, blast)
lemma QSigmaE2 [elim!]:
- "[| <a;b>: QSigma(A,B); [| a:A; b:B(a) |] ==> P |] ==> P"
-by (simp add: QSigma_def)
+ "[| <a;b>: QSigma(A,B); [| a \<in> A; b \<in> B(a) |] ==> P |] ==> P"
+by (simp add: QSigma_def)
lemma QSigmaD1: "<a;b> \<in> QSigma(A,B) ==> a \<in> A"
by blast
@@ -117,9 +117,9 @@
by blast
lemma QSigma_cong:
- "[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==>
+ "[| A=A'; !!x. x \<in> A' ==> B(x)=B'(x) |] ==>
QSigma(A,B) = QSigma(A',B')"
-by (simp add: QSigma_def)
+by (simp add: QSigma_def)
lemma QSigma_empty1 [simp]: "QSigma(0,B) = 0"
by blast
@@ -136,13 +136,13 @@
lemma qsnd_conv [simp]: "qsnd(<a;b>) = b"
by (simp add: qsnd_def)
-lemma qfst_type [TC]: "p:QSigma(A,B) ==> qfst(p) \<in> A"
+lemma qfst_type [TC]: "p \<in> QSigma(A,B) ==> qfst(p) \<in> A"
by auto
-lemma qsnd_type [TC]: "p:QSigma(A,B) ==> qsnd(p) \<in> B(qfst(p))"
+lemma qsnd_type [TC]: "p \<in> QSigma(A,B) ==> qsnd(p) \<in> B(qfst(p))"
by auto
-lemma QPair_qfst_qsnd_eq: "a: QSigma(A,B) ==> <qfst(a); qsnd(a)> = a"
+lemma QPair_qfst_qsnd_eq: "a \<in> QSigma(A,B) ==> <qfst(a); qsnd(a)> = a"
by auto
@@ -154,13 +154,13 @@
lemma qsplit_type [elim!]:
- "[| p:QSigma(A,B);
- !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x;y>)
+ "[| p \<in> QSigma(A,B);
+ !!x y.[| x \<in> A; y \<in> B(x) |] ==> c(x,y):C(<x;y>)
|] ==> qsplit(%x y. c(x,y), p) \<in> C(p)"
-by auto
+by auto
-lemma expand_qsplit:
- "u: A<*>B ==> R(qsplit(c,u)) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. u = <x;y> \<longrightarrow> R(c(x,y)))"
+lemma expand_qsplit:
+ "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)))"
apply (simp add: qsplit_def, auto)
done
@@ -172,10 +172,10 @@
lemma qsplitE:
- "[| qsplit(R,z); z:QSigma(A,B);
- !!x y. [| z = <x;y>; R(x,y) |] ==> P
+ "[| qsplit(R,z); z \<in> QSigma(A,B);
+ !!x y. [| z = <x;y>; R(x,y) |] ==> P
|] ==> P"
-by (simp add: qsplit_def, auto)
+by (simp add: qsplit_def, auto)
lemma qsplitD: "qsplit(R,<a;b>) ==> R(a,b)"
by (simp add: qsplit_def)
@@ -190,10 +190,10 @@
by (simp add: qconverse_def, blast)
lemma qconverseE [elim!]:
- "[| yx \<in> qconverse(r);
- !!x y. [| yx=<y;x>; <x;y>:r |] ==> P
+ "[| yx \<in> qconverse(r);
+ !!x y. [| yx=<y;x>; <x;y>:r |] ==> P
|] ==> P"
-by (simp add: qconverse_def, blast)
+by (simp add: qconverse_def, blast)
lemma qconverse_qconverse: "r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r"
by blast
@@ -223,11 +223,11 @@
(** Elimination rules **)
lemma qsumE [elim!]:
- "[| u: A <+> B;
- !!x. [| x:A; u=QInl(x) |] ==> P;
- !!y. [| y:B; u=QInr(y) |] ==> P
+ "[| u \<in> A <+> B;
+ !!x. [| x \<in> A; u=QInl(x) |] ==> P;
+ !!y. [| y \<in> B; u=QInr(y) |] ==> P
|] ==> P"
-by (simp add: qsum_defs, blast)
+by (simp add: qsum_defs, blast)
(** Injection and freeness equivalences, for rewriting **)
@@ -254,16 +254,16 @@
lemmas QInl_neq_QInr = QInl_QInr_iff [THEN iffD1, THEN FalseE, elim!]
lemmas QInr_neq_QInl = QInr_QInl_iff [THEN iffD1, THEN FalseE, elim!]
-lemma QInlD: "QInl(a): A<+>B ==> a: A"
+lemma QInlD: "QInl(a): A<+>B ==> a \<in> A"
by blast
-lemma QInrD: "QInr(b): A<+>B ==> b: B"
+lemma QInrD: "QInr(b): A<+>B ==> b \<in> B"
by blast
(** <+> is itself injective... who cares?? **)
lemma qsum_iff:
- "u: A <+> B \<longleftrightarrow> (\<exists>x. x:A & u=QInl(x)) | (\<exists>y. y:B & u=QInr(y))"
+ "u \<in> A <+> B \<longleftrightarrow> (\<exists>x. x \<in> A & u=QInl(x)) | (\<exists>y. y \<in> B & u=QInr(y))"
by blast
lemma qsum_subset_iff: "A <+> B \<subseteq> C <+> D \<longleftrightarrow> A<=C & B<=D"
@@ -284,21 +284,21 @@
by (simp add: qsum_defs )
lemma qcase_type:
- "[| u: A <+> B;
- !!x. x: A ==> c(x): C(QInl(x));
- !!y. y: B ==> d(y): C(QInr(y))
+ "[| u \<in> A <+> B;
+ !!x. x \<in> A ==> c(x): C(QInl(x));
+ !!y. y \<in> B ==> d(y): C(QInr(y))
|] ==> qcase(c,d,u) \<in> C(u)"
-by (simp add: qsum_defs, auto)
+by (simp add: qsum_defs, auto)
(** Rules for the Part primitive **)
-lemma Part_QInl: "Part(A <+> B,QInl) = {QInl(x). x: A}"
+lemma Part_QInl: "Part(A <+> B,QInl) = {QInl(x). x \<in> A}"
by blast
-lemma Part_QInr: "Part(A <+> B,QInr) = {QInr(y). y: B}"
+lemma Part_QInr: "Part(A <+> B,QInr) = {QInr(y). y \<in> B}"
by blast
-lemma Part_QInr2: "Part(A <+> B, %x. QInr(h(x))) = {QInr(y). y: Part(B,h)}"
+lemma Part_QInr2: "Part(A <+> B, %x. QInr(h(x))) = {QInr(y). y \<in> Part(B,h)}"
by blast
lemma Part_qsum_equality: "C \<subseteq> A <+> B ==> Part(C,QInl) \<union> Part(C,QInr) = C"