Received: from scaup.cl.cam.ac.uk by Steve.CL.Cam.AC.UK
          with SMTP/TCP/IP over Ethernet id a003642; 26 May 89 21:59 BST
Via:  uk.ac.nsf; 26 May 89 21:57 BST  (UK.AC.Cam.Cl.scaup)
Received: from clover.ucdavis.edu by NSFnet-Relay.AC.UK   via NSFnet with SMTP
           id aa19727; 26 May 89 21:28 BST
Received: from tina.Stanford.EDU by clover.ucdavis.edu (5.59/UCD.EECS.1.9)
        id AA12648; Fri, 26 May 89 09:35:56 PDT
Received: by tina (4.0/inc-1.0)
        id AA01754; Fri, 26 May 89 09:35:13 PDT
Date: Fri, 26 May 89 09:35:13 PDT
From: "Paul N. Loewenstein" <paul@edu.stanford.tina>
Message-Id: <8905261635.AA01754@tina>
To: info-hol@edu.ucdavis.clover
In-Reply-To: Tom Melham's message of Fri, 26 May 89 14:02:01 BST <8905261406.aa23850@scaup.Cl.Cam.AC.UK>
Subject: Related to binary word definitions in HOL
Sender: paul <paul%edu.ucdavis.tina@edu.ucdavis.clover>
Status: R


          Some comments on speed of Val_CONV.

It seems that the speed of Val_CONV is hammered by having to do
arithmetic using SUC. How about changing the default representation of
natural number constants to be binary words, and change num_CONV to
perform a binary decrement operation? Theorems and conversions can
then be developed to do arithmetic directly on the binary
representation.  The only hack then has to be on how to print and read
the numbers, any radix conversion can be done at that time. If one
really wants to do things properly, one could develop a theory of
radix arithmetic, but that is probably overdoing things.


       Paul.