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--
added Tools/lin_arith.ML;
     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