Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) 
          id <18977-0@swan.cl.cam.ac.uk>; Fri, 24 Jul 1992 19:35:21 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA12124;
          Fri, 24 Jul 92 11:26:22 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from leopard.cs.uidaho.edu by ted.cs.uidaho.edu (16.6/1.34) 
          id AA12119; Fri, 24 Jul 92 11:26:17 -0700
Received: by leopard.cs.uidaho.edu (16.7/1.34) id AA08842;
          Fri, 24 Jul 92 11:29:39 -0700
From: weiss@edu.uidaho.cs.leopard (Phil Weiss)
Message-Id: <9207241829.AA08842@leopard.cs.uidaho.edu>
Subject: More on GSPEC(\x.(<expr>,F))
To: info-hol@edu.uidaho.cs.ted (HOL Mailing List)
Date: Fri, 24 Jul 92 11:29:39 PDT
Mailer: Elm [revision: 66.33]

Thanks to all who replied about my question.

I had been using SET_SPEC_CONV to rewrite such specifications, but
it seemed to be over-kill and also affects other items in my
specs.

I believe John hit the nail on the head for my problem, in that
what we have is GSPEC(\x. (E[x],P[x])) rather than (E x) and (P x).

I am wondering how difficult it would be to make the parser and
pretty-printer convert sets of the form, {E[x] | P[x]} directly
to the latter form.  While it may be difficult based on how the
parser/pretty-printer works, I would think the semantics would
be straightforward.  For example,

  {SUC x | x < 10}

would become

  GSPEC(\x. ((\x'. SUC x') x, (\x'. x' < 10) x))

rather than

  GSPEC(\x. (SUC x, x < 10))

It seems to me that this would make the definitions of sets much more
general and easy to work with.  Then again, this came just off the
top of my head, so I haven't thought it through, and it may be
rather unworkable, or even logically wrong.

Any comments?

Phil.

--
Philip Weiss	Laboratory for Applied Logic	weiss@leopard.cs.uidaho.edu
(Disclaimer: My views are not their views)	weiss872@snake.cs.uidaho.edu