|
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", " <*>"))]; |