author | paulson |
Fri, 11 Aug 2000 13:26:40 +0200 | |
changeset 9577 | 9e66e8ed8237 |
parent 6093 | 87bf8c03b169 |
child 13220 | 62c899c77151 |
permissions | -rw-r--r-- |
1478 | 1 |
(* Title: ZF/qpair.thy |
0 | 2 |
ID: $Id$ |
1478 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 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 |
||
2469 | 14 |
QPair = Sum + |
3923 | 15 |
|
0 | 16 |
consts |
1478 | 17 |
QPair :: [i, i] => i ("<(_;/ _)>") |
1401 | 18 |
qfst,qsnd :: i => i |
19 |
qsplit :: [[i, i] => 'a, i] => 'a::logic (*for pattern-matching*) |
|
20 |
qconverse :: i => i |
|
21 |
QSigma :: [i, i => i] => i |
|
0 | 22 |
|
1478 | 23 |
"<+>" :: [i,i]=>i (infixr 65) |
1401 | 24 |
QInl,QInr :: i=>i |
25 |
qcase :: [i=>i, i=>i, i]=>i |
|
0 | 26 |
|
929
137035296ad6
Moved declarations of @QSUM and <*> to a syntax section.
lcp
parents:
753
diff
changeset
|
27 |
syntax |
1401 | 28 |
"@QSUM" :: [idt, i, i] => i ("(3QSUM _:_./ _)" 10) |
1478 | 29 |
"<*>" :: [i, i] => i (infixr 80) |
929
137035296ad6
Moved declarations of @QSUM and <*> to a syntax section.
lcp
parents:
753
diff
changeset
|
30 |
|
0 | 31 |
translations |
32 |
"QSUM x:A. B" => "QSigma(A, %x. B)" |
|
44 | 33 |
"A <*> B" => "QSigma(A, _K(B))" |
0 | 34 |
|
3923 | 35 |
|
753 | 36 |
defs |
0 | 37 |
QPair_def "<a;b> == a+b" |
1097
01379c46ad2d
Changed definitions so that qsplit is now defined in terms of
lcp
parents:
929
diff
changeset
|
38 |
qfst_def "qfst(p) == THE a. EX b. p=<a;b>" |
01379c46ad2d
Changed definitions so that qsplit is now defined in terms of
lcp
parents:
929
diff
changeset
|
39 |
qsnd_def "qsnd(p) == THE b. EX a. p=<a;b>" |
01379c46ad2d
Changed definitions so that qsplit is now defined in terms of
lcp
parents:
929
diff
changeset
|
40 |
qsplit_def "qsplit(c,p) == c(qfst(p), qsnd(p))" |
01379c46ad2d
Changed definitions so that qsplit is now defined in terms of
lcp
parents:
929
diff
changeset
|
41 |
|
0 | 42 |
qconverse_def "qconverse(r) == {z. w:r, EX x y. w=<x;y> & z=<y;x>}" |
43 |
QSigma_def "QSigma(A,B) == UN x:A. UN y:B(x). {<x;y>}" |
|
44 |
||
120 | 45 |
qsum_def "A <+> B == ({0} <*> A) Un ({1} <*> B)" |
0 | 46 |
QInl_def "QInl(a) == <0;a>" |
47 |
QInr_def "QInr(b) == <1;b>" |
|
48 |
qcase_def "qcase(c,d) == qsplit(%y z. cond(y, d(z), c(z)))" |
|
49 |
end |
|
50 |
||
51 |
ML |
|
52 |
||
53 |
val print_translation = |
|
929
137035296ad6
Moved declarations of @QSUM and <*> to a syntax section.
lcp
parents:
753
diff
changeset
|
54 |
[("QSigma", dependent_tr' ("@QSUM", "op <*>"))]; |