Implemented "ordered rewriting": rules which merely permute variables, such
as commutativity, are only applied if the term becaomes lexicographically
smaller (according to some fixed ordering on the term structure).
(* Title: ZF/qpair.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Quine-inspired ordered pairs and disjoint sums, for non-well-founded data
structures in ZF. Does not precisely follow Quine's construction. Thanks
to Thomas Forster for suggesting this approach!
W. V. Quine, On Ordered Pairs and Relations, in Selected Logic Papers,
1966.
*)
QPair = Sum + "simpdata" +
consts
QPair :: "[i, i] => i" ("<(_;/ _)>")
qsplit :: "[[i,i] => i, i] => i"
qfsplit :: "[[i,i] => o, i] => o"
qconverse :: "i => i"
"@QSUM" :: "[idt, i, i] => i" ("(3QSUM _:_./ _)" 10)
" <*>" :: "[i, i] => i" ("(_ <*>/ _)" [81, 80] 80)
QSigma :: "[i, i => i] => i"
"<+>" :: "[i,i]=>i" (infixr 65)
QInl,QInr :: "i=>i"
qcase :: "[i=>i, i=>i, i]=>i"
translations
"QSUM x:A. B" => "QSigma(A, %x. B)"
"A <*> B" => "QSigma(A, _K(B))"
rules
QPair_def "<a;b> == a+b"
qsplit_def "qsplit(c,p) == THE y. EX a b. p=<a;b> & y=c(a,b)"
qfsplit_def "qfsplit(R,z) == EX x y. z=<x;y> & R(x,y)"
qconverse_def "qconverse(r) == {z. w:r, EX x y. w=<x;y> & z=<y;x>}"
QSigma_def "QSigma(A,B) == UN x:A. UN y:B(x). {<x;y>}"
qsum_def "A <+> B == ({0} <*> A) Un ({1} <*> B)"
QInl_def "QInl(a) == <0;a>"
QInr_def "QInr(b) == <1;b>"
qcase_def "qcase(c,d) == qsplit(%y z. cond(y, d(z), c(z)))"
end
ML
val print_translation =
[("QSigma", dependent_tr' ("@QSUM", " <*>"))];