Received: from scaup.cl.cam.ac.uk by Steve.CL.Cam.AC.UK
          with SMTP/TCP/IP over Ethernet id a005783; 30 May 89 20:18 BST
Via:  uk.ac.nsf; 30 May 89 20:13 BST  (UK.AC.Cam.Cl.scaup)
Received: from clover.ucdavis.edu by NSFnet-Relay.AC.UK   via NSFnet with SMTP
           id aa02106; 30 May 89 19:41 BST
Received: from tina.Stanford.EDU by clover.ucdavis.edu (5.59/UCD.EECS.1.9)
        id AA04055; Tue, 30 May 89 10:30:57 PDT
Received: by tina (4.0/inc-1.0)
        id AA02539; Tue, 30 May 89 10:30:05 PDT
Date: Tue, 30 May 89 10:30:05 PDT
From: "Paul N. Loewenstein" <paul@edu.stanford.tina>
Message-Id: <8905301730.AA02539@tina>
To: info-hol@edu.ucdavis.clover
Subject: Dealing with large natural constants.
Sender: paul <paul%edu.ucdavis.tina@edu.ucdavis.clover>
Status: R


I agree with Tom's point that one should avoid reasoning about large
natural-number constants. However, once one has proven a parameterised
design correct, one has at some point to set that parameter to some
value to make un-parameterised hardware. If one is going to get out
of the theorem prover in some clean manner, then the unwinding to
some defined translatable sub-set of HOL has to be done inside HOL.

By using what is currently available in HOL, this unwinding often takes
far longer than the proof of correctness! It is this process that
often requires more efficient arithmetic to execute in a reasonable
time.

       Paul.