0

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 
Quineinspired ordered pairs and disjoint sums, for nonwellfounded 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", " <*>"))];
