Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Message-Id: <9212111817.AA12049@easynet.crl.dec.com>
Date: Fri, 11 Dec 92 13:17:26 EST
From: "Tim Leonard, DTN 225-5809, HLO2-3/C11 11-Dec-1992 1246" 
      <leonard@com.dec.enet.ricks> 
To: windley@edu.uidaho.cs.panther
Cc: info-hol@edu.uidaho.cs.ted
Apparently-To: info-hol@ted.cs.uidaho.edu, windley@panther.cs.uidaho.edu
Subject: Re: Cartesian sums for alternative representations

Thanks, Phil, I think I see how I was confused.  I'd been thinking that for
"efficient" (hah!) symbolic simulation I would have to express 64-bit values as
primitive terms of some type, like num or (bool list), in order to operate on
them quickly.  I now see that's silly for two reasons.  First, only base terms
are really primitive (like 0 and []: bool list), so almost everything, even
things like 538, are really compound terms.  Second, it's no more expensive to
do the proofs using compound terms.  I can directly compute the results of an
addition with terms like (WORD64 538), by using the theorems showing the
relationship between ADD64 and + (using VAL64 and WORD64), thus bypassing the
changes into and out of a representing type.  I guess that should be obvious to
anyone who's seen abstract types, but I'm being slow.

Thanks for the help,
Tim