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 <10934-0@swan.cl.cam.ac.uk>; Fri, 24 Jul 1992 12:44:09 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA11666;
          Fri, 24 Jul 92 04:35:13 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA11661;
          Fri, 24 Jul 92 04:35:07 -0700
Received: from scaup.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl 
          id <10723-0@swan.cl.cam.ac.uk>; Fri, 24 Jul 1992 12:35:41 +0100
To: weiss@edu.uidaho.cs.leopard (Phil Weiss)
Cc: info-hol@edu.uidaho.cs.ted (HOL Mailing List), Tom.Melham@uk.ac.cam.cl
Subject: Re: Equivalence of GSPEC(\x. ( ,F)) and EMPTY
In-Reply-To: Your message of Thu, 23 Jul 92 11:10:21 -0700. <9207231810.AA27324@leopard.cs.uidaho.edu>
Date: Fri, 24 Jul 92 12:35:17 +0100
From: Tom Melham <Tom.Melham@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.736:24.06.92.11.35.58"@cl.cam.ac.uk>


weiss> Could anyone tell me if they have managed to prove
weiss> 
weiss> GSPEC (\x. (<any expression>, F)) = EMPTY
weiss> 
weiss> for all expressions?  Or if they have written a conversion?

des> try making it into a conversion ...

Note also that the `standard' way of dealing with GSPEC terms is to use
the supplied conversion SET_SPEC_CONV, the manual entry for which is
attached.  That is, I have tried to arrange that users will never have
to appeal to the actual definition of GSPEC, but can always use this
conversion instead.

Using SET_SPEC_CONV, here are the first few steps of the required
conversion (broken into individual steps to show what's going on):

  #let tm = "GSPEC (\x:*. E x:**,F) = {}";;
  tm = "GSPEC(\x. (E x,F)) = {}" : term
  
  % Standard way of dealing with equations between sets %
  #let th1 = REWR_CONV EXTENSION tm;;
  th1 = 
  |- (GSPEC(\x. (E x,F)) = {}) = (!x. x IN (GSPEC(\x. (E x,F))) = x IN {})

  % Standard way of dealing with membership in GSPEC sets. %
  #let th2 = ONCE_DEPTH_CONV SET_SPEC_CONV (rand(concl th1));;
  th2 = 
   |- (!x. x IN (GSPEC(\x. (E x,F))) = x IN {}) =
      (!x. (?x'. (x = E x') /\ F) = x IN {})
 
From this point, one would proceed much as David has shown.

Tom

============================================================================
SET_SPEC_CONV : conv

SYNOPSIS

Axiom-scheme of specification for set abstractions.

DESCRIPTION

The conversion SET_SPEC_CONV expects its term argument to be an assertion of
the form "t IN {E | P}". Given such a term, the conversion returns a
theorem that defines the condition under which this membership assertion holds.
When E is just a variable v, the conversion returns:

   |- t IN {v | P} = P[t/v]

and when E is not a variable but some other expression, the theorem
returned is:

   |- t IN {E | P} = ?x1...xn. (t = E) /\ P

where x1, ..., xn are the variables that occur free both in
the expression E and in the proposition P.

EXAMPLES


#SET_SPEC_CONV "12 IN {n | n > N}";;
|- 12 IN {n | n > N} = 12 > N

#SET_SPEC_CONV "p IN {(n,m) | n < m}";;
|- p IN {(n,m) | n < m} = (?n m. (p = n,m) /\ n < m)


FAILURE CONDITIONS

Fails if applied to a term that is not of the form  "t IN {E | P}".