(* Title: ZF/QPair.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
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?
*)
section\<open>Quine-Inspired Ordered Pairs and Disjoint Sums\<close>
theory QPair imports Sum func begin
text\<open>For non-well-founded data
structures in ZF. Does not precisely follow Quine's construction. Thanks
to Thomas Forster for suggesting this approach!
W. V. Quine, On Ordered Pairs and Relations, in Selected Logic Papers,
1966.
\<close>
definition
QPair :: "[i, i] => i" ("<(_;/ _)>") where
"<a;b> == a+b"
definition
qfst :: "i => i" where
"qfst(p) == THE a. \<exists>b. p=<a;b>"
definition
qsnd :: "i => i" where
"qsnd(p) == THE b. \<exists>a. p=<a;b>"
definition
qsplit :: "[[i, i] => 'a, i] => 'a::{}" (*for pattern-matching*) where
"qsplit(c,p) == c(qfst(p), qsnd(p))"
definition
qconverse :: "i => i" where
"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 _ \<in> _./ _)" 10)
translations
"QSUM x \<in> A. B" => "CONST QSigma(A, %x. B)"
abbreviation
qprod (infixr "<*>" 80) where
"A <*> B == QSigma(A, %_. B)"
definition
qsum :: "[i,i]=>i" (infixr "<+>" 65) where
"A <+> B == ({0} <*> A) \<union> ({1} <*> B)"
definition
QInl :: "i=>i" where
"QInl(a) == <0;a>"
definition
QInr :: "i=>i" where
"QInr(b) == <1;b>"
definition
qcase :: "[i=>i, i=>i, i]=>i" where
"qcase(c,d) == qsplit(%y z. cond(y, d(z), c(z)))"
subsection\<open>Quine ordered pairing\<close>
(** Lemmas for showing that <a;b> uniquely determines a and b **)
lemma QPair_empty [simp]: "<0;0> = 0"
by (simp add: QPair_def)
lemma QPair_iff [simp]: "<a;b> = <c;d> \<longleftrightarrow> a=c & b=d"
apply (simp add: QPair_def)
apply (rule sum_equal_iff)
done
lemmas QPair_inject = QPair_iff [THEN iffD1, THEN conjE, elim!]
lemma QPair_inject1: "<a;b> = <c;d> ==> a=c"
by blast
lemma QPair_inject2: "<a;b> = <c;d> ==> b=d"
by blast
subsubsection\<open>QSigma: Disjoint union of a family of sets
Generalizes Cartesian product\<close>
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 \<in> QSigma(A,B);
!!x y.[| x \<in> A; y \<in> B(x); c=<x;y> |] ==> P
|] ==> P"
by (simp add: QSigma_def, blast)
lemma QSigmaE2 [elim!]:
"[| <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
lemma QSigmaD2: "<a;b> \<in> QSigma(A,B) ==> b \<in> B(a)"
by blast
lemma QSigma_cong:
"[| A=A'; !!x. x \<in> A' ==> B(x)=B'(x) |] ==>
QSigma(A,B) = QSigma(A',B')"
by (simp add: QSigma_def)
lemma QSigma_empty1 [simp]: "QSigma(0,B) = 0"
by blast
lemma QSigma_empty2 [simp]: "A <*> 0 = 0"
by blast
subsubsection\<open>Projections: qfst, qsnd\<close>
lemma qfst_conv [simp]: "qfst(<a;b>) = a"
by (simp add: qfst_def)
lemma qsnd_conv [simp]: "qsnd(<a;b>) = b"
by (simp add: qsnd_def)
lemma qfst_type [TC]: "p \<in> QSigma(A,B) ==> qfst(p) \<in> A"
by auto
lemma qsnd_type [TC]: "p \<in> QSigma(A,B) ==> qsnd(p) \<in> B(qfst(p))"
by auto
lemma QPair_qfst_qsnd_eq: "a \<in> QSigma(A,B) ==> <qfst(a); qsnd(a)> = a"
by auto
subsubsection\<open>Eliminator: qsplit\<close>
(*A META-equality, so that it applies to higher types as well...*)
lemma qsplit [simp]: "qsplit(%x y. c(x,y), <a;b>) == c(a,b)"
by (simp add: qsplit_def)
lemma qsplit_type [elim!]:
"[| 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
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
subsubsection\<open>qsplit for predicates: result type o\<close>
lemma qsplitI: "R(a,b) ==> qsplit(R, <a;b>)"
by (simp add: qsplit_def)
lemma qsplitE:
"[| qsplit(R,z); z \<in> QSigma(A,B);
!!x y. [| z = <x;y>; R(x,y) |] ==> P
|] ==> P"
by (simp add: qsplit_def, auto)
lemma qsplitD: "qsplit(R,<a;b>) ==> R(a,b)"
by (simp add: qsplit_def)
subsubsection\<open>qconverse\<close>
lemma qconverseI [intro!]: "<a;b>:r ==> <b;a>:qconverse(r)"
by (simp add: qconverse_def, blast)
lemma qconverseD [elim!]: "<a;b> \<in> qconverse(r) ==> <b;a> \<in> r"
by (simp add: qconverse_def, blast)
lemma qconverseE [elim!]:
"[| yx \<in> qconverse(r);
!!x y. [| yx=<y;x>; <x;y>:r |] ==> P
|] ==> P"
by (simp add: qconverse_def, blast)
lemma qconverse_qconverse: "r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r"
by blast
lemma qconverse_type: "r \<subseteq> A <*> B ==> qconverse(r) \<subseteq> B <*> A"
by blast
lemma qconverse_prod: "qconverse(A <*> B) = B <*> A"
by blast
lemma qconverse_empty: "qconverse(0) = 0"
by blast
subsection\<open>The Quine-inspired notion of disjoint sum\<close>
lemmas qsum_defs = qsum_def QInl_def QInr_def qcase_def
(** Introduction rules for the injections **)
lemma QInlI [intro!]: "a \<in> A ==> QInl(a) \<in> A <+> B"
by (simp add: qsum_defs, blast)
lemma QInrI [intro!]: "b \<in> B ==> QInr(b) \<in> A <+> B"
by (simp add: qsum_defs, blast)
(** Elimination rules **)
lemma qsumE [elim!]:
"[| 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)
(** Injection and freeness equivalences, for rewriting **)
lemma QInl_iff [iff]: "QInl(a)=QInl(b) \<longleftrightarrow> a=b"
by (simp add: qsum_defs )
lemma QInr_iff [iff]: "QInr(a)=QInr(b) \<longleftrightarrow> a=b"
by (simp add: qsum_defs )
lemma QInl_QInr_iff [simp]: "QInl(a)=QInr(b) \<longleftrightarrow> False"
by (simp add: qsum_defs )
lemma QInr_QInl_iff [simp]: "QInr(b)=QInl(a) \<longleftrightarrow> False"
by (simp add: qsum_defs )
lemma qsum_empty [simp]: "0<+>0 = 0"
by (simp add: qsum_defs )
(*Injection and freeness rules*)
lemmas QInl_inject = QInl_iff [THEN iffD1]
lemmas QInr_inject = QInr_iff [THEN iffD1]
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 \<in> A"
by blast
lemma QInrD: "QInr(b): A<+>B ==> b \<in> B"
by blast
(** <+> is itself injective... who cares?? **)
lemma qsum_iff:
"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"
by blast
lemma qsum_equal_iff: "A <+> B = C <+> D \<longleftrightarrow> A=C & B=D"
apply (simp (no_asm) add: extension qsum_subset_iff)
apply blast
done
subsubsection\<open>Eliminator -- qcase\<close>
lemma qcase_QInl [simp]: "qcase(c, d, QInl(a)) = c(a)"
by (simp add: qsum_defs )
lemma qcase_QInr [simp]: "qcase(c, d, QInr(b)) = d(b)"
by (simp add: qsum_defs )
lemma qcase_type:
"[| 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)
(** Rules for the Part primitive **)
lemma Part_QInl: "Part(A <+> B,QInl) = {QInl(x). x \<in> A}"
by blast
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 \<in> Part(B,h)}"
by blast
lemma Part_qsum_equality: "C \<subseteq> A <+> B ==> Part(C,QInl) \<union> Part(C,QInr) = C"
by blast
subsubsection\<open>Monotonicity\<close>
lemma QPair_mono: "[| a<=c; b<=d |] ==> <a;b> \<subseteq> <c;d>"
by (simp add: QPair_def sum_mono)
lemma QSigma_mono [rule_format]:
"[| A<=C; \<forall>x\<in>A. B(x) \<subseteq> D(x) |] ==> QSigma(A,B) \<subseteq> QSigma(C,D)"
by blast
lemma QInl_mono: "a<=b ==> QInl(a) \<subseteq> QInl(b)"
by (simp add: QInl_def subset_refl [THEN QPair_mono])
lemma QInr_mono: "a<=b ==> QInr(a) \<subseteq> QInr(b)"
by (simp add: QInr_def subset_refl [THEN QPair_mono])
lemma qsum_mono: "[| A<=C; B<=D |] ==> A <+> B \<subseteq> C <+> D"
by blast
end