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; Fri, 23 Jul 1993 23:38:52 +0100
Received: by ted.cs.uidaho.edu (16.6/2.0) id AA28877;
          Fri, 23 Jul 93 15:29:57 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from leopard.cs.uidaho.edu by cs.uidaho.edu (16.6/2.0) id AA28872;
          Fri, 23 Jul 93 15:29:52 -0700
Received: by leopard.cs.uidaho.edu (16.7/1.34) id AA16846;
          Fri, 23 Jul 93 15:33:36 -0700
From: coe@leopard.cs.uidaho.edu (Mike Coe)
Message-Id: <9307232233.AA16846@leopard.cs.uidaho.edu>
Subject: set library
To: info-hol@ted.cs.uidaho.edu
Date: Fri, 23 Jul 93 15:33:36 PDT
Mailer: Elm [revision: 66.33]



Hi,

I am using the sets library in the specification
of a pipelined microprocessor.  For instance to
check wether or not the current opcode is a
branch instruction, we write


op IN ^BRANCH_OPS   where



 BRANCH_OPS = 
    "{^BC_OP, ^BEQ_OP, ^BGTEZ_OP, ^BGTZ_OP, 
      ^BLTEZ_OP, ^BLTZ_OP, ^BNEQ_OP, ^BOV_OP}";;




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) 




Is something like this possible using the sets library?



thanks,


mike

--
Michael L Coe                 |  "A mind is a terrible thing."
Laboratory of Applied Logic   | 
University of Idaho           | 
coe@leopard.cs.uidaho.edu     | 
coe861@snake.cs.uidaho.edu