src/ZF/QPair.thy
author wenzelm
Mon Dec 04 22:54:31 2017 +0100 (20 months ago)
changeset 67131 85d10959c2e4
parent 60770 240563fbf41d
child 69587 53982d5ec0bb
permissions -rw-r--r--
tuned signature;
     1 (*  Title:      ZF/QPair.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1993  University of Cambridge
     4 
     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
     8 is not a limit ordinal?
     9 *)
    10 
    11 section\<open>Quine-Inspired Ordered Pairs and Disjoint Sums\<close>
    12 
    13 theory QPair imports Sum func begin
    14 
    15 text\<open>For non-well-founded 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 \<close>
    22 
    23 definition
    24   QPair     :: "[i, i] => i"                      ("<(_;/ _)>")  where
    25     "<a;b> == a+b"
    26 
    27 definition
    28   qfst :: "i => i"  where
    29     "qfst(p) == THE a. \<exists>b. p=<a;b>"
    30 
    31 definition
    32   qsnd :: "i => i"  where
    33     "qsnd(p) == THE b. \<exists>a. p=<a;b>"
    34 
    35 definition
    36   qsplit    :: "[[i, i] => 'a, i] => 'a::{}"  (*for pattern-matching*)  where
    37     "qsplit(c,p) == c(qfst(p), qsnd(p))"
    38 
    39 definition
    40   qconverse :: "i => i"  where
    41     "qconverse(r) == {z. w \<in> r, \<exists>x y. w=<x;y> & z=<y;x>}"
    42 
    43 definition
    44   QSigma    :: "[i, i => i] => i"  where
    45     "QSigma(A,B)  ==  \<Union>x\<in>A. \<Union>y\<in>B(x). {<x;y>}"
    46 
    47 syntax
    48   "_QSUM"   :: "[idt, i, i] => i"               ("(3QSUM _ \<in> _./ _)" 10)
    49 translations
    50   "QSUM x \<in> A. B"  => "CONST QSigma(A, %x. B)"
    51 
    52 abbreviation
    53   qprod  (infixr "<*>" 80) where
    54   "A <*> B == QSigma(A, %_. B)"
    55 
    56 definition
    57   qsum    :: "[i,i]=>i"                         (infixr "<+>" 65)  where
    58     "A <+> B      == ({0} <*> A) \<union> ({1} <*> B)"
    59 
    60 definition
    61   QInl :: "i=>i"  where
    62     "QInl(a)      == <0;a>"
    63 
    64 definition
    65   QInr :: "i=>i"  where
    66     "QInr(b)      == <1;b>"
    67 
    68 definition
    69   qcase     :: "[i=>i, i=>i, i]=>i"  where
    70     "qcase(c,d)   == qsplit(%y z. cond(y, d(z), c(z)))"
    71 
    72 
    73 subsection\<open>Quine ordered pairing\<close>
    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 
    80 lemma QPair_iff [simp]: "<a;b> = <c;d> \<longleftrightarrow> a=c & b=d"
    81 apply (simp add: QPair_def)
    82 apply (rule sum_equal_iff)
    83 done
    84 
    85 lemmas QPair_inject = QPair_iff [THEN iffD1, THEN conjE, elim!]
    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 
    94 subsubsection\<open>QSigma: Disjoint union of a family of sets
    95      Generalizes Cartesian product\<close>
    96 
    97 lemma QSigmaI [intro!]: "[| a \<in> A;  b \<in> B(a) |] ==> <a;b> \<in> QSigma(A,B)"
    98 by (simp add: QSigma_def)
    99 
   100 
   101 (** Elimination rules for <a;b>:A*B -- introducing no eigenvariables **)
   102 
   103 lemma QSigmaE [elim!]:
   104     "[| c \<in> QSigma(A,B);
   105         !!x y.[| x \<in> A;  y \<in> B(x);  c=<x;y> |] ==> P
   106      |] ==> P"
   107 by (simp add: QSigma_def, blast)
   108 
   109 lemma QSigmaE2 [elim!]:
   110     "[| <a;b>: QSigma(A,B); [| a \<in> A;  b \<in> B(a) |] ==> P |] ==> P"
   111 by (simp add: QSigma_def)
   112 
   113 lemma QSigmaD1: "<a;b> \<in> QSigma(A,B) ==> a \<in> A"
   114 by blast
   115 
   116 lemma QSigmaD2: "<a;b> \<in> QSigma(A,B) ==> b \<in> B(a)"
   117 by blast
   118 
   119 lemma QSigma_cong:
   120     "[| A=A';  !!x. x \<in> A' ==> B(x)=B'(x) |] ==>
   121      QSigma(A,B) = QSigma(A',B')"
   122 by (simp add: QSigma_def)
   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 
   131 subsubsection\<open>Projections: qfst, qsnd\<close>
   132 
   133 lemma qfst_conv [simp]: "qfst(<a;b>) = a"
   134 by (simp add: qfst_def)
   135 
   136 lemma qsnd_conv [simp]: "qsnd(<a;b>) = b"
   137 by (simp add: qsnd_def)
   138 
   139 lemma qfst_type [TC]: "p \<in> QSigma(A,B) ==> qfst(p) \<in> A"
   140 by auto
   141 
   142 lemma qsnd_type [TC]: "p \<in> QSigma(A,B) ==> qsnd(p) \<in> B(qfst(p))"
   143 by auto
   144 
   145 lemma QPair_qfst_qsnd_eq: "a \<in> QSigma(A,B) ==> <qfst(a); qsnd(a)> = a"
   146 by auto
   147 
   148 
   149 subsubsection\<open>Eliminator: qsplit\<close>
   150 
   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)"
   153 by (simp add: qsplit_def)
   154 
   155 
   156 lemma qsplit_type [elim!]:
   157     "[|  p \<in> QSigma(A,B);
   158          !!x y.[| x \<in> A; y \<in> B(x) |] ==> c(x,y):C(<x;y>)
   159      |] ==> qsplit(%x y. c(x,y), p) \<in> C(p)"
   160 by auto
   161 
   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)))"
   164 apply (simp add: qsplit_def, auto)
   165 done
   166 
   167 
   168 subsubsection\<open>qsplit for predicates: result type o\<close>
   169 
   170 lemma qsplitI: "R(a,b) ==> qsplit(R, <a;b>)"
   171 by (simp add: qsplit_def)
   172 
   173 
   174 lemma qsplitE:
   175     "[| qsplit(R,z);  z \<in> QSigma(A,B);
   176         !!x y. [| z = <x;y>;  R(x,y) |] ==> P
   177     |] ==> P"
   178 by (simp add: qsplit_def, auto)
   179 
   180 lemma qsplitD: "qsplit(R,<a;b>) ==> R(a,b)"
   181 by (simp add: qsplit_def)
   182 
   183 
   184 subsubsection\<open>qconverse\<close>
   185 
   186 lemma qconverseI [intro!]: "<a;b>:r ==> <b;a>:qconverse(r)"
   187 by (simp add: qconverse_def, blast)
   188 
   189 lemma qconverseD [elim!]: "<a;b> \<in> qconverse(r) ==> <b;a> \<in> r"
   190 by (simp add: qconverse_def, blast)
   191 
   192 lemma qconverseE [elim!]:
   193     "[| yx \<in> qconverse(r);
   194         !!x y. [| yx=<y;x>;  <x;y>:r |] ==> P
   195      |] ==> P"
   196 by (simp add: qconverse_def, blast)
   197 
   198 lemma qconverse_qconverse: "r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r"
   199 by blast
   200 
   201 lemma qconverse_type: "r \<subseteq> A <*> B ==> qconverse(r) \<subseteq> B <*> A"
   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 
   211 subsection\<open>The Quine-inspired notion of disjoint sum\<close>
   212 
   213 lemmas qsum_defs = qsum_def QInl_def QInr_def qcase_def
   214 
   215 (** Introduction rules for the injections **)
   216 
   217 lemma QInlI [intro!]: "a \<in> A ==> QInl(a) \<in> A <+> B"
   218 by (simp add: qsum_defs, blast)
   219 
   220 lemma QInrI [intro!]: "b \<in> B ==> QInr(b) \<in> A <+> B"
   221 by (simp add: qsum_defs, blast)
   222 
   223 (** Elimination rules **)
   224 
   225 lemma qsumE [elim!]:
   226     "[| u \<in> A <+> B;
   227         !!x. [| x \<in> A;  u=QInl(x) |] ==> P;
   228         !!y. [| y \<in> B;  u=QInr(y) |] ==> P
   229      |] ==> P"
   230 by (simp add: qsum_defs, blast)
   231 
   232 
   233 (** Injection and freeness equivalences, for rewriting **)
   234 
   235 lemma QInl_iff [iff]: "QInl(a)=QInl(b) \<longleftrightarrow> a=b"
   236 by (simp add: qsum_defs )
   237 
   238 lemma QInr_iff [iff]: "QInr(a)=QInr(b) \<longleftrightarrow> a=b"
   239 by (simp add: qsum_defs )
   240 
   241 lemma QInl_QInr_iff [simp]: "QInl(a)=QInr(b) \<longleftrightarrow> False"
   242 by (simp add: qsum_defs )
   243 
   244 lemma QInr_QInl_iff [simp]: "QInr(b)=QInl(a) \<longleftrightarrow> False"
   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 
   252 lemmas QInl_inject = QInl_iff [THEN iffD1]
   253 lemmas QInr_inject = QInr_iff [THEN iffD1]
   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!]
   256 
   257 lemma QInlD: "QInl(a): A<+>B ==> a \<in> A"
   258 by blast
   259 
   260 lemma QInrD: "QInr(b): A<+>B ==> b \<in> B"
   261 by blast
   262 
   263 (** <+> is itself injective... who cares?? **)
   264 
   265 lemma qsum_iff:
   266      "u \<in> A <+> B \<longleftrightarrow> (\<exists>x. x \<in> A & u=QInl(x)) | (\<exists>y. y \<in> B & u=QInr(y))"
   267 by blast
   268 
   269 lemma qsum_subset_iff: "A <+> B \<subseteq> C <+> D \<longleftrightarrow> A<=C & B<=D"
   270 by blast
   271 
   272 lemma qsum_equal_iff: "A <+> B = C <+> D \<longleftrightarrow> A=C & B=D"
   273 apply (simp (no_asm) add: extension qsum_subset_iff)
   274 apply blast
   275 done
   276 
   277 subsubsection\<open>Eliminator -- qcase\<close>
   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:
   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))
   290      |] ==> qcase(c,d,u) \<in> C(u)"
   291 by (simp add: qsum_defs, auto)
   292 
   293 (** Rules for the Part primitive **)
   294 
   295 lemma Part_QInl: "Part(A <+> B,QInl) = {QInl(x). x \<in> A}"
   296 by blast
   297 
   298 lemma Part_QInr: "Part(A <+> B,QInr) = {QInr(y). y \<in> B}"
   299 by blast
   300 
   301 lemma Part_QInr2: "Part(A <+> B, %x. QInr(h(x))) = {QInr(y). y \<in> Part(B,h)}"
   302 by blast
   303 
   304 lemma Part_qsum_equality: "C \<subseteq> A <+> B ==> Part(C,QInl) \<union> Part(C,QInr) = C"
   305 by blast
   306 
   307 
   308 subsubsection\<open>Monotonicity\<close>
   309 
   310 lemma QPair_mono: "[| a<=c;  b<=d |] ==> <a;b> \<subseteq> <c;d>"
   311 by (simp add: QPair_def sum_mono)
   312 
   313 lemma QSigma_mono [rule_format]:
   314      "[| A<=C;  \<forall>x\<in>A. B(x) \<subseteq> D(x) |] ==> QSigma(A,B) \<subseteq> QSigma(C,D)"
   315 by blast
   316 
   317 lemma QInl_mono: "a<=b ==> QInl(a) \<subseteq> QInl(b)"
   318 by (simp add: QInl_def subset_refl [THEN QPair_mono])
   319 
   320 lemma QInr_mono: "a<=b ==> QInr(a) \<subseteq> QInr(b)"
   321 by (simp add: QInr_def subset_refl [THEN QPair_mono])
   322 
   323 lemma qsum_mono: "[| A<=C;  B<=D |] ==> A <+> B \<subseteq> C <+> D"
   324 by blast
   325 
   326 end