Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Sat, 24 Jul 1993 14:25:01 +0100
Received: by ted.cs.uidaho.edu (16.6/2.0) id AA29117;
          Sat, 24 Jul 93 06:14:49 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from swan.cl.cam.ac.uk by cs.uidaho.edu (16.6/2.0) id AA29112;
          Sat, 24 Jul 93 06:14:42 -0700
Received: from guillemot.cl.cam.ac.uk (user tfm (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Sat, 24 Jul 1993 14:14:44 +0100
To: coe@leopard.cs.uidaho.edu (Mike Coe)
Cc: info-hol@ted.cs.uidaho.edu, Tom.Melham@cl.cam.ac.uk
Subject: Re: set library
In-Reply-To: Your message of "Fri, 23 Jul 93 15:33:36 PDT." <9307232233.AA16846@leopard.cs.uidaho.edu>
Date: Wed, 21 Jul 93 01:52:23 +0100
From: Tom Melham <Tom.Melham@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:144150:930724131449"@cl.cam.ac.uk>


Regarding Mike Coe's query:

> Now I noticed in the documenation of the sets library
> that there is a universe defined.  What I would like
> to do is define my own universe such as 
> 
> let ALL_OPS = { all legal opcodes}
> 
> And then if I have an assumption in a proof like
> 
> ~(op IN {^BRANCH_OPS}),  I could show  that
> 
> op IN  (ALL_OPS DIFF  BRANCH_OPS) 

The first thing to note is that the universe in the sets library is 
a typed one.  The constant UNIV:(*)set denotes the set of all values
of type :*.  So if your set "{all legal opcodes}" is in fact denoted
by a logical type, :opcode say, then UNIV:(opcode)set is the "ALL_OPS"
set you're looking for.  On the other hand, if the "legal opcodes" do
not form a type, then what you are asking for is not possible to do
in this straightforward way.  I.e:

 ~((op:ty) IN S) ==> op IN (ALL_OPS DIFF S) 

holds (for all S) only if 

  !op:ty. op IN ALL_OPS

In the library:

let COE_THM =
    PROVE
    ("!U. (!s. !op:*. ~(op IN s) ==> op IN (U DIFF s)) = !op. op IN U",
     PURE_ONCE_REWRITE_TAC [IN_DIFF] THEN
     REPEAT (EQ_TAC ORELSE STRIP_TAC) THENL
     [ASSUME_TAC (SPEC "op:*" NOT_IN_EMPTY) THEN RES_TAC;
      FIRST_ASSUM MATCH_ACCEPT_TAC;
      RES_TAC]);;

Tom