# Theory QPair

```(*  Title:      ZF/QPair.thy
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

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‹Quine-Inspired Ordered Pairs and Disjoint Sums›

theory QPair imports Sum func begin

text‹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.
›

definition
QPair     :: "[i, i] ⇒ i"                      (‹<(_;/ _)>›)  where
"<a;b> ≡ a+b"

definition
qfst :: "i ⇒ i"  where
"qfst(p) ≡ THE a. ∃b. p=<a;b>"

definition
qsnd :: "i ⇒ i"  where
"qsnd(p) ≡ THE b. ∃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 ∈ r, ∃x y. w=<x;y> ∧ z=<y;x>}"

definition
QSigma    :: "[i, i ⇒ i] ⇒ i"  where
"QSigma(A,B)  ≡  ⋃x∈A. ⋃y∈B(x). {<x;y>}"

syntax
"_QSUM"   :: "[idt, i, i] ⇒ i"               (‹(3QSUM _ ∈ _./ _)› 10)
translations
"QSUM x ∈ 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) ∪ ({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‹Quine ordered pairing›

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

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

lemma QPair_iff [simp]: "<a;b> = <c;d> ⟷ a=c ∧ b=d"
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‹QSigma: Disjoint union of a family of sets
Generalizes Cartesian product›

lemma QSigmaI [intro!]: "⟦a ∈ A;  b ∈ B(a)⟧ ⟹ <a;b> ∈ QSigma(A,B)"

(** 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
⟧ ⟹ P"

lemma QSigmaE2 [elim!]:
"⟦<a;b>: QSigma(A,B); ⟦a ∈ A;  b ∈ B(a)⟧ ⟹ P⟧ ⟹ P"

lemma QSigmaD1: "<a;b> ∈ QSigma(A,B) ⟹ a ∈ A"
by blast

lemma QSigmaD2: "<a;b> ∈ QSigma(A,B) ⟹ b ∈ B(a)"
by blast

lemma QSigma_cong:
"⟦A=A';  ⋀x. x ∈ A' ⟹ B(x)=B'(x)⟧ ⟹
QSigma(A,B) = QSigma(A',B')"

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

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

subsubsection‹Projections: qfst, qsnd›

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

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

lemma qfst_type [TC]: "p ∈ QSigma(A,B) ⟹ qfst(p) ∈ A"
by auto

lemma qsnd_type [TC]: "p ∈ QSigma(A,B) ⟹ qsnd(p) ∈ B(qfst(p))"
by auto

lemma QPair_qfst_qsnd_eq: "a ∈ QSigma(A,B) ⟹ <qfst(a); qsnd(a)> = a"
by auto

subsubsection‹Eliminator: qsplit›

(*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)"

lemma qsplit_type [elim!]:
"⟦p ∈ QSigma(A,B);
⋀x y.⟦x ∈ A; y ∈ B(x)⟧ ⟹ c(x,y):C(<x;y>)
⟧ ⟹ qsplit(λx y. c(x,y), p) ∈ C(p)"
by auto

lemma expand_qsplit:
"u ∈ A<*>B ⟹ R(qsplit(c,u)) ⟷ (∀x∈A. ∀y∈B. u = <x;y> ⟶ R(c(x,y)))"
done

subsubsection‹qsplit for predicates: result type o›

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

lemma qsplitE:
"⟦qsplit(R,z);  z ∈ QSigma(A,B);
⋀x y. ⟦z = <x;y>;  R(x,y)⟧ ⟹ P
⟧ ⟹ P"

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

subsubsection‹qconverse›

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

lemma qconverseD [elim!]: "<a;b> ∈ qconverse(r) ⟹ <b;a> ∈ r"

lemma qconverseE [elim!]:
"⟦yx ∈ qconverse(r);
⋀x y. ⟦yx=<y;x>;  <x;y>:r⟧ ⟹ P
⟧ ⟹ P"

lemma qconverse_qconverse: "r<=QSigma(A,B) ⟹ qconverse(qconverse(r)) = r"
by blast

lemma qconverse_type: "r ⊆ A <*> B ⟹ qconverse(r) ⊆ B <*> A"
by blast

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

lemma qconverse_empty: "qconverse(0) = 0"
by blast

subsection‹The Quine-inspired notion of disjoint sum›

lemmas qsum_defs = qsum_def QInl_def QInr_def qcase_def

(** Introduction rules for the injections **)

lemma QInlI [intro!]: "a ∈ A ⟹ QInl(a) ∈ A <+> B"

lemma QInrI [intro!]: "b ∈ B ⟹ QInr(b) ∈ A <+> B"

(** Elimination rules **)

lemma qsumE [elim!]:
"⟦u ∈ A <+> B;
⋀x. ⟦x ∈ A;  u=QInl(x)⟧ ⟹ P;
⋀y. ⟦y ∈ B;  u=QInr(y)⟧ ⟹ P
⟧ ⟹ P"

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

lemma QInl_iff [iff]: "QInl(a)=QInl(b) ⟷ a=b"

lemma QInr_iff [iff]: "QInr(a)=QInr(b) ⟷ a=b"

lemma QInl_QInr_iff [simp]: "QInl(a)=QInr(b) ⟷ False"

lemma QInr_QInl_iff [simp]: "QInr(b)=QInl(a) ⟷ False"

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

(*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 ∈ A"
by blast

lemma QInrD: "QInr(b): A<+>B ⟹ b ∈ B"
by blast

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

lemma qsum_iff:
"u ∈ A <+> B ⟷ (∃x. x ∈ A ∧ u=QInl(x)) | (∃y. y ∈ B ∧ u=QInr(y))"
by blast

lemma qsum_subset_iff: "A <+> B ⊆ C <+> D ⟷ A<=C ∧ B<=D"
by blast

lemma qsum_equal_iff: "A <+> B = C <+> D ⟷ A=C ∧ B=D"
apply (simp (no_asm) add: extension qsum_subset_iff)
apply blast
done

subsubsection‹Eliminator -- qcase›

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

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

lemma qcase_type:
"⟦u ∈ A <+> B;
⋀x. x ∈ A ⟹ c(x): C(QInl(x));
⋀y. y ∈ B ⟹ d(y): C(QInr(y))
⟧ ⟹ qcase(c,d,u) ∈ C(u)"

(** Rules for the Part primitive **)

lemma Part_QInl: "Part(A <+> B,QInl) = {QInl(x). x ∈ A}"
by blast

lemma Part_QInr: "Part(A <+> B,QInr) = {QInr(y). y ∈ B}"
by blast

lemma Part_QInr2: "Part(A <+> B, λx. QInr(h(x))) = {QInr(y). y ∈ Part(B,h)}"
by blast

lemma Part_qsum_equality: "C ⊆ A <+> B ⟹ Part(C,QInl) ∪ Part(C,QInr) = C"
by blast

subsubsection‹Monotonicity›

lemma QPair_mono: "⟦a<=c;  b<=d⟧ ⟹ <a;b> ⊆ <c;d>"

lemma QSigma_mono [rule_format]:
"⟦A<=C;  ∀x∈A. B(x) ⊆ D(x)⟧ ⟹ QSigma(A,B) ⊆ QSigma(C,D)"
by blast

lemma QInl_mono: "a<=b ⟹ QInl(a) ⊆ QInl(b)"
by (simp add: QInl_def subset_refl [THEN QPair_mono])

lemma QInr_mono: "a<=b ⟹ QInr(a) ⊆ QInr(b)"
by (simp add: QInr_def subset_refl [THEN QPair_mono])

lemma qsum_mono: "⟦A<=C;  B<=D⟧ ⟹ A <+> B ⊆ C <+> D"
by blast

end
```