src/ZF/QPair.thy
 author wenzelm Tue Jul 31 19:40:22 2007 +0200 (2007-07-31) changeset 24091 109f19a13872 parent 22808 a7daa74e2980 child 24893 b8ef7afe3a6b permissions -rw-r--r--
```     1 (*  Title:      ZF/qpair.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     4     Copyright   1993  University of Cambridge
```
```     5
```
```     6 Many proofs are borrowed from pair.thy and sum.thy
```
```     7
```
```     8 Do we EVER have rank(a) < rank(<a;b>) ?  Perhaps if the latter rank
```
```     9     is not a limit ordinal?
```
```    10 *)
```
```    11
```
```    12 header{*Quine-Inspired Ordered Pairs and Disjoint Sums*}
```
```    13
```
```    14 theory QPair imports Sum func begin
```
```    15
```
```    16 text{*For non-well-founded data
```
```    17 structures in ZF.  Does not precisely follow Quine's construction.  Thanks
```
```    18 to Thomas Forster for suggesting this approach!
```
```    19
```
```    20 W. V. Quine, On Ordered Pairs and Relations, in Selected Logic Papers,
```
```    21 1966.
```
```    22 *}
```
```    23
```
```    24 constdefs
```
```    25   QPair     :: "[i, i] => i"                      ("<(_;/ _)>")
```
```    26     "<a;b> == a+b"
```
```    27
```
```    28   qfst :: "i => i"
```
```    29     "qfst(p) == THE a. EX b. p=<a;b>"
```
```    30
```
```    31   qsnd :: "i => i"
```
```    32     "qsnd(p) == THE b. EX a. p=<a;b>"
```
```    33
```
```    34   qsplit    :: "[[i, i] => 'a, i] => 'a::{}"  (*for pattern-matching*)
```
```    35     "qsplit(c,p) == c(qfst(p), qsnd(p))"
```
```    36
```
```    37   qconverse :: "i => i"
```
```    38     "qconverse(r) == {z. w:r, EX x y. w=<x;y> & z=<y;x>}"
```
```    39
```
```    40   QSigma    :: "[i, i => i] => i"
```
```    41     "QSigma(A,B)  ==  \<Union>x\<in>A. \<Union>y\<in>B(x). {<x;y>}"
```
```    42
```
```    43 syntax
```
```    44   "_QSUM"   :: "[idt, i, i] => i"               ("(3QSUM _:_./ _)" 10)
```
```    45 translations
```
```    46   "QSUM x:A. B"  => "QSigma(A, %x. B)"
```
```    47
```
```    48 abbreviation
```
```    49   qprod  (infixr "<*>" 80) where
```
```    50   "A <*> B == QSigma(A, %_. B)"
```
```    51
```
```    52 constdefs
```
```    53   qsum    :: "[i,i]=>i"                         (infixr "<+>" 65)
```
```    54     "A <+> B      == ({0} <*> A) Un ({1} <*> B)"
```
```    55
```
```    56   QInl :: "i=>i"
```
```    57     "QInl(a)      == <0;a>"
```
```    58
```
```    59   QInr :: "i=>i"
```
```    60     "QInr(b)      == <1;b>"
```
```    61
```
```    62   qcase     :: "[i=>i, i=>i, i]=>i"
```
```    63     "qcase(c,d)   == qsplit(%y z. cond(y, d(z), c(z)))"
```
```    64
```
```    65
```
```    66 subsection{*Quine ordered pairing*}
```
```    67
```
```    68 (** Lemmas for showing that <a;b> uniquely determines a and b **)
```
```    69
```
```    70 lemma QPair_empty [simp]: "<0;0> = 0"
```
```    71 by (simp add: QPair_def)
```
```    72
```
```    73 lemma QPair_iff [simp]: "<a;b> = <c;d> <-> a=c & b=d"
```
```    74 apply (simp add: QPair_def)
```
```    75 apply (rule sum_equal_iff)
```
```    76 done
```
```    77
```
```    78 lemmas QPair_inject = QPair_iff [THEN iffD1, THEN conjE, standard, elim!]
```
```    79
```
```    80 lemma QPair_inject1: "<a;b> = <c;d> ==> a=c"
```
```    81 by blast
```
```    82
```
```    83 lemma QPair_inject2: "<a;b> = <c;d> ==> b=d"
```
```    84 by blast
```
```    85
```
```    86
```
```    87 subsubsection{*QSigma: Disjoint union of a family of sets
```
```    88      Generalizes Cartesian product*}
```
```    89
```
```    90 lemma QSigmaI [intro!]: "[| a:A;  b:B(a) |] ==> <a;b> : QSigma(A,B)"
```
```    91 by (simp add: QSigma_def)
```
```    92
```
```    93
```
```    94 (** Elimination rules for <a;b>:A*B -- introducing no eigenvariables **)
```
```    95
```
```    96 lemma QSigmaE [elim!]:
```
```    97     "[| c: QSigma(A,B);
```
```    98         !!x y.[| x:A;  y:B(x);  c=<x;y> |] ==> P
```
```    99      |] ==> P"
```
```   100 by (simp add: QSigma_def, blast)
```
```   101
```
```   102 lemma QSigmaE2 [elim!]:
```
```   103     "[| <a;b>: QSigma(A,B); [| a:A;  b:B(a) |] ==> P |] ==> P"
```
```   104 by (simp add: QSigma_def)
```
```   105
```
```   106 lemma QSigmaD1: "<a;b> : QSigma(A,B) ==> a : A"
```
```   107 by blast
```
```   108
```
```   109 lemma QSigmaD2: "<a;b> : QSigma(A,B) ==> b : B(a)"
```
```   110 by blast
```
```   111
```
```   112 lemma QSigma_cong:
```
```   113     "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==>
```
```   114      QSigma(A,B) = QSigma(A',B')"
```
```   115 by (simp add: QSigma_def)
```
```   116
```
```   117 lemma QSigma_empty1 [simp]: "QSigma(0,B) = 0"
```
```   118 by blast
```
```   119
```
```   120 lemma QSigma_empty2 [simp]: "A <*> 0 = 0"
```
```   121 by blast
```
```   122
```
```   123
```
```   124 subsubsection{*Projections: qfst, qsnd*}
```
```   125
```
```   126 lemma qfst_conv [simp]: "qfst(<a;b>) = a"
```
```   127 by (simp add: qfst_def)
```
```   128
```
```   129 lemma qsnd_conv [simp]: "qsnd(<a;b>) = b"
```
```   130 by (simp add: qsnd_def)
```
```   131
```
```   132 lemma qfst_type [TC]: "p:QSigma(A,B) ==> qfst(p) : A"
```
```   133 by auto
```
```   134
```
```   135 lemma qsnd_type [TC]: "p:QSigma(A,B) ==> qsnd(p) : B(qfst(p))"
```
```   136 by auto
```
```   137
```
```   138 lemma QPair_qfst_qsnd_eq: "a: QSigma(A,B) ==> <qfst(a); qsnd(a)> = a"
```
```   139 by auto
```
```   140
```
```   141
```
```   142 subsubsection{*Eliminator: qsplit*}
```
```   143
```
```   144 (*A META-equality, so that it applies to higher types as well...*)
```
```   145 lemma qsplit [simp]: "qsplit(%x y. c(x,y), <a;b>) == c(a,b)"
```
```   146 by (simp add: qsplit_def)
```
```   147
```
```   148
```
```   149 lemma qsplit_type [elim!]:
```
```   150     "[|  p:QSigma(A,B);
```
```   151          !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x;y>)
```
```   152      |] ==> qsplit(%x y. c(x,y), p) : C(p)"
```
```   153 by auto
```
```   154
```
```   155 lemma expand_qsplit:
```
```   156  "u: A<*>B ==> R(qsplit(c,u)) <-> (ALL x:A. ALL y:B. u = <x;y> --> R(c(x,y)))"
```
```   157 apply (simp add: qsplit_def, auto)
```
```   158 done
```
```   159
```
```   160
```
```   161 subsubsection{*qsplit for predicates: result type o*}
```
```   162
```
```   163 lemma qsplitI: "R(a,b) ==> qsplit(R, <a;b>)"
```
```   164 by (simp add: qsplit_def)
```
```   165
```
```   166
```
```   167 lemma qsplitE:
```
```   168     "[| qsplit(R,z);  z:QSigma(A,B);
```
```   169         !!x y. [| z = <x;y>;  R(x,y) |] ==> P
```
```   170     |] ==> P"
```
```   171 by (simp add: qsplit_def, auto)
```
```   172
```
```   173 lemma qsplitD: "qsplit(R,<a;b>) ==> R(a,b)"
```
```   174 by (simp add: qsplit_def)
```
```   175
```
```   176
```
```   177 subsubsection{*qconverse*}
```
```   178
```
```   179 lemma qconverseI [intro!]: "<a;b>:r ==> <b;a>:qconverse(r)"
```
```   180 by (simp add: qconverse_def, blast)
```
```   181
```
```   182 lemma qconverseD [elim!]: "<a;b> : qconverse(r) ==> <b;a> : r"
```
```   183 by (simp add: qconverse_def, blast)
```
```   184
```
```   185 lemma qconverseE [elim!]:
```
```   186     "[| yx : qconverse(r);
```
```   187         !!x y. [| yx=<y;x>;  <x;y>:r |] ==> P
```
```   188      |] ==> P"
```
```   189 by (simp add: qconverse_def, blast)
```
```   190
```
```   191 lemma qconverse_qconverse: "r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r"
```
```   192 by blast
```
```   193
```
```   194 lemma qconverse_type: "r <= A <*> B ==> qconverse(r) <= B <*> A"
```
```   195 by blast
```
```   196
```
```   197 lemma qconverse_prod: "qconverse(A <*> B) = B <*> A"
```
```   198 by blast
```
```   199
```
```   200 lemma qconverse_empty: "qconverse(0) = 0"
```
```   201 by blast
```
```   202
```
```   203
```
```   204 subsection{*The Quine-inspired notion of disjoint sum*}
```
```   205
```
```   206 lemmas qsum_defs = qsum_def QInl_def QInr_def qcase_def
```
```   207
```
```   208 (** Introduction rules for the injections **)
```
```   209
```
```   210 lemma QInlI [intro!]: "a : A ==> QInl(a) : A <+> B"
```
```   211 by (simp add: qsum_defs, blast)
```
```   212
```
```   213 lemma QInrI [intro!]: "b : B ==> QInr(b) : A <+> B"
```
```   214 by (simp add: qsum_defs, blast)
```
```   215
```
```   216 (** Elimination rules **)
```
```   217
```
```   218 lemma qsumE [elim!]:
```
```   219     "[| u: A <+> B;
```
```   220         !!x. [| x:A;  u=QInl(x) |] ==> P;
```
```   221         !!y. [| y:B;  u=QInr(y) |] ==> P
```
```   222      |] ==> P"
```
```   223 by (simp add: qsum_defs, blast)
```
```   224
```
```   225
```
```   226 (** Injection and freeness equivalences, for rewriting **)
```
```   227
```
```   228 lemma QInl_iff [iff]: "QInl(a)=QInl(b) <-> a=b"
```
```   229 by (simp add: qsum_defs )
```
```   230
```
```   231 lemma QInr_iff [iff]: "QInr(a)=QInr(b) <-> a=b"
```
```   232 by (simp add: qsum_defs )
```
```   233
```
```   234 lemma QInl_QInr_iff [simp]: "QInl(a)=QInr(b) <-> False"
```
```   235 by (simp add: qsum_defs )
```
```   236
```
```   237 lemma QInr_QInl_iff [simp]: "QInr(b)=QInl(a) <-> False"
```
```   238 by (simp add: qsum_defs )
```
```   239
```
```   240 lemma qsum_empty [simp]: "0<+>0 = 0"
```
```   241 by (simp add: qsum_defs )
```
```   242
```
```   243 (*Injection and freeness rules*)
```
```   244
```
```   245 lemmas QInl_inject = QInl_iff [THEN iffD1, standard]
```
```   246 lemmas QInr_inject = QInr_iff [THEN iffD1, standard]
```
```   247 lemmas QInl_neq_QInr = QInl_QInr_iff [THEN iffD1, THEN FalseE, elim!]
```
```   248 lemmas QInr_neq_QInl = QInr_QInl_iff [THEN iffD1, THEN FalseE, elim!]
```
```   249
```
```   250 lemma QInlD: "QInl(a): A<+>B ==> a: A"
```
```   251 by blast
```
```   252
```
```   253 lemma QInrD: "QInr(b): A<+>B ==> b: B"
```
```   254 by blast
```
```   255
```
```   256 (** <+> is itself injective... who cares?? **)
```
```   257
```
```   258 lemma qsum_iff:
```
```   259      "u: A <+> B <-> (EX x. x:A & u=QInl(x)) | (EX y. y:B & u=QInr(y))"
```
```   260 by blast
```
```   261
```
```   262 lemma qsum_subset_iff: "A <+> B <= C <+> D <-> A<=C & B<=D"
```
```   263 by blast
```
```   264
```
```   265 lemma qsum_equal_iff: "A <+> B = C <+> D <-> A=C & B=D"
```
```   266 apply (simp (no_asm) add: extension qsum_subset_iff)
```
```   267 apply blast
```
```   268 done
```
```   269
```
```   270 subsubsection{*Eliminator -- qcase*}
```
```   271
```
```   272 lemma qcase_QInl [simp]: "qcase(c, d, QInl(a)) = c(a)"
```
```   273 by (simp add: qsum_defs )
```
```   274
```
```   275
```
```   276 lemma qcase_QInr [simp]: "qcase(c, d, QInr(b)) = d(b)"
```
```   277 by (simp add: qsum_defs )
```
```   278
```
```   279 lemma qcase_type:
```
```   280     "[| u: A <+> B;
```
```   281         !!x. x: A ==> c(x): C(QInl(x));
```
```   282         !!y. y: B ==> d(y): C(QInr(y))
```
```   283      |] ==> qcase(c,d,u) : C(u)"
```
```   284 by (simp add: qsum_defs, auto)
```
```   285
```
```   286 (** Rules for the Part primitive **)
```
```   287
```
```   288 lemma Part_QInl: "Part(A <+> B,QInl) = {QInl(x). x: A}"
```
```   289 by blast
```
```   290
```
```   291 lemma Part_QInr: "Part(A <+> B,QInr) = {QInr(y). y: B}"
```
```   292 by blast
```
```   293
```
```   294 lemma Part_QInr2: "Part(A <+> B, %x. QInr(h(x))) = {QInr(y). y: Part(B,h)}"
```
```   295 by blast
```
```   296
```
```   297 lemma Part_qsum_equality: "C <= A <+> B ==> Part(C,QInl) Un Part(C,QInr) = C"
```
```   298 by blast
```
```   299
```
```   300
```
```   301 subsubsection{*Monotonicity*}
```
```   302
```
```   303 lemma QPair_mono: "[| a<=c;  b<=d |] ==> <a;b> <= <c;d>"
```
```   304 by (simp add: QPair_def sum_mono)
```
```   305
```
```   306 lemma QSigma_mono [rule_format]:
```
```   307      "[| A<=C;  ALL x:A. B(x) <= D(x) |] ==> QSigma(A,B) <= QSigma(C,D)"
```
```   308 by blast
```
```   309
```
```   310 lemma QInl_mono: "a<=b ==> QInl(a) <= QInl(b)"
```
```   311 by (simp add: QInl_def subset_refl [THEN QPair_mono])
```
```   312
```
```   313 lemma QInr_mono: "a<=b ==> QInr(a) <= QInr(b)"
```
```   314 by (simp add: QInr_def subset_refl [THEN QPair_mono])
```
```   315
```
```   316 lemma qsum_mono: "[| A<=C;  B<=D |] ==> A <+> B <= C <+> D"
```
```   317 by blast
```
```   318
```
```   319 ML
```
```   320 {*
```
```   321 val qsum_defs = thms "qsum_defs";
```
```   322
```
```   323 val QPair_empty = thm "QPair_empty";
```
```   324 val QPair_iff = thm "QPair_iff";
```
```   325 val QPair_inject = thm "QPair_inject";
```
```   326 val QPair_inject1 = thm "QPair_inject1";
```
```   327 val QPair_inject2 = thm "QPair_inject2";
```
```   328 val QSigmaI = thm "QSigmaI";
```
```   329 val QSigmaE = thm "QSigmaE";
```
```   330 val QSigmaE = thm "QSigmaE";
```
```   331 val QSigmaE2 = thm "QSigmaE2";
```
```   332 val QSigmaD1 = thm "QSigmaD1";
```
```   333 val QSigmaD2 = thm "QSigmaD2";
```
```   334 val QSigma_cong = thm "QSigma_cong";
```
```   335 val QSigma_empty1 = thm "QSigma_empty1";
```
```   336 val QSigma_empty2 = thm "QSigma_empty2";
```
```   337 val qfst_conv = thm "qfst_conv";
```
```   338 val qsnd_conv = thm "qsnd_conv";
```
```   339 val qfst_type = thm "qfst_type";
```
```   340 val qsnd_type = thm "qsnd_type";
```
```   341 val QPair_qfst_qsnd_eq = thm "QPair_qfst_qsnd_eq";
```
```   342 val qsplit = thm "qsplit";
```
```   343 val qsplit_type = thm "qsplit_type";
```
```   344 val expand_qsplit = thm "expand_qsplit";
```
```   345 val qsplitI = thm "qsplitI";
```
```   346 val qsplitE = thm "qsplitE";
```
```   347 val qsplitD = thm "qsplitD";
```
```   348 val qconverseI = thm "qconverseI";
```
```   349 val qconverseD = thm "qconverseD";
```
```   350 val qconverseE = thm "qconverseE";
```
```   351 val qconverse_qconverse = thm "qconverse_qconverse";
```
```   352 val qconverse_type = thm "qconverse_type";
```
```   353 val qconverse_prod = thm "qconverse_prod";
```
```   354 val qconverse_empty = thm "qconverse_empty";
```
```   355 val QInlI = thm "QInlI";
```
```   356 val QInrI = thm "QInrI";
```
```   357 val qsumE = thm "qsumE";
```
```   358 val QInl_iff = thm "QInl_iff";
```
```   359 val QInr_iff = thm "QInr_iff";
```
```   360 val QInl_QInr_iff = thm "QInl_QInr_iff";
```
```   361 val QInr_QInl_iff = thm "QInr_QInl_iff";
```
```   362 val qsum_empty = thm "qsum_empty";
```
```   363 val QInl_inject = thm "QInl_inject";
```
```   364 val QInr_inject = thm "QInr_inject";
```
```   365 val QInl_neq_QInr = thm "QInl_neq_QInr";
```
```   366 val QInr_neq_QInl = thm "QInr_neq_QInl";
```
```   367 val QInlD = thm "QInlD";
```
```   368 val QInrD = thm "QInrD";
```
```   369 val qsum_iff = thm "qsum_iff";
```
```   370 val qsum_subset_iff = thm "qsum_subset_iff";
```
```   371 val qsum_equal_iff = thm "qsum_equal_iff";
```
```   372 val qcase_QInl = thm "qcase_QInl";
```
```   373 val qcase_QInr = thm "qcase_QInr";
```
```   374 val qcase_type = thm "qcase_type";
```
```   375 val Part_QInl = thm "Part_QInl";
```
```   376 val Part_QInr = thm "Part_QInr";
```
```   377 val Part_QInr2 = thm "Part_QInr2";
```
```   378 val Part_qsum_equality = thm "Part_qsum_equality";
```
```   379 val QPair_mono = thm "QPair_mono";
```
```   380 val QSigma_mono = thm "QSigma_mono";
```
```   381 val QInl_mono = thm "QInl_mono";
```
```   382 val QInr_mono = thm "QInr_mono";
```
```   383 val qsum_mono = thm "qsum_mono";
```
```   384 *}
```
```   385
```
```   386 end
```