src/ZF/QPair.thy
 author wenzelm Thu Dec 14 11:24:26 2017 +0100 (20 months ago) changeset 67198 694f29a5433b parent 60770 240563fbf41d child 69587 53982d5ec0bb permissions -rw-r--r--
merged
```     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
```