src/ZF/QPair.thy
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 44 00597b21a6a9
permissions -rw-r--r--
Initial revision
     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 Quine-inspired ordered pairs and disjoint sums, for non-well-founded data
     7 structures in ZF.  Does not precisely follow Quine's construction.  Thanks
     8 to Thomas Forster for suggesting this approach!
     9 
    10 W. V. Quine, On Ordered Pairs and Relations, in Selected Logic Papers,
    11 1966.
    12 *)
    13 
    14 QPair = Sum +
    15 consts
    16   QPair     :: "[i, i] => i"               	("<(_;/ _)>")
    17   qsplit    :: "[[i,i] => i, i] => i"
    18   qfsplit   :: "[[i,i] => o, i] => o"
    19   qconverse :: "i => i"
    20   "@QSUM"   :: "[idt, i, i] => i"               ("(3QSUM _:_./ _)" 10)
    21   " <*>"    :: "[i, i] => i"         		("(_ <*>/ _)" [81, 80] 80)
    22   QSigma    :: "[i, i => i] => i"
    23 
    24   "<+>"     :: "[i,i]=>i"      			(infixr 65)
    25   QInl,QInr :: "i=>i"
    26   qcase     :: "[i=>i, i=>i, i]=>i"
    27 
    28 translations
    29   "QSUM x:A. B"  => "QSigma(A, %x. B)"
    30 
    31 rules
    32   QPair_def       "<a;b> == a+b"
    33   qsplit_def      "qsplit(c,p)  ==  THE y. EX a b. p=<a;b> & y=c(a,b)"
    34   qfsplit_def     "qfsplit(R,z) == EX x y. z=<x;y> & R(x,y)"
    35   qconverse_def   "qconverse(r) == {z. w:r, EX x y. w=<x;y> & z=<y;x>}"
    36   QSigma_def      "QSigma(A,B)  ==  UN x:A. UN y:B(x). {<x;y>}"
    37 
    38   qsum_def        "A <+> B      == QSigma({0}, %x.A) Un QSigma({1}, %x.B)"
    39   QInl_def        "QInl(a)      == <0;a>"
    40   QInr_def        "QInr(b)      == <1;b>"
    41   qcase_def       "qcase(c,d)   == qsplit(%y z. cond(y, d(z), c(z)))"
    42 end
    43 
    44 ML
    45 
    46 (* 'Dependent' type operators *)
    47 
    48 val parse_translation =
    49   [(" <*>", ndependent_tr "QSigma")];
    50 
    51 val print_translation =
    52   [("QSigma", dependent_tr' ("@QSUM", " <*>"))];