Delivery-Date: 
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
From: David Shepherd <des@inmos.co.uk>
Message-Id: <19068.9308261027@frogland.inmos.co.uk>
Subject: Re: numerals by pretty printer instead by num_CONV?
To: info-hol@dworshak.cs.uidaho.edu (info-hol mailing list)
Date: Thu, 26 Aug 1993 11:27:26 +0100 (BST)
Content-Type: text
Content-Length: 2309

Richard Boulton has said:
> Tim Leonard wrote
> > 	DECIMAL [1;2;3;4;5]		% = 12345	%
> > 	BINARY [1;0;0;0;0]		% = 16		%
> > 	HEX [15;15]			% = 255		%
> 
> I'm curious: Did you find having the most significant digit as the first element
> of the list to be advantageous?

I've been doing something similar recently with my word theory (based on an
abstract theory of arrays of length n) in which I'm using hexadecimal
notation for most of the interfaces to it. My feelings so far are

i) For readability you need least significant item on the right
ii) For proof efficiency you need least significant item at head of list.

Hence I define my "interface" functions as

hex_word(h1,h2,h3,h4,h5,h6,h7,h8) 
= @ (w:word). val_word w = hex_list_val[h8;h7;h6;h5;h4;h3;h2;h1]


> >      o  that hol define a small number (like 16) of numeric constants *for use
> > 	  only by the numeral library, parser, and pretty-printer*
> 
> One good thing about this is that the constants can be defined rather than being
> built in as an axiom scheme:
> 
>    1 = SUC 0
>    2 = SUC (SUC 0)
>    3 = SUC (SUC (SUC 0))
>    etc. (upto a *finite* (and fairly small!) number)
> 
> By defining the digits as fully expanded SUC forms (as above) there is no need
> for num_CONV. One can simply expand using these definitions. My first reaction
> was to define the hex digits 0,...,9,A,...,F, but realised that having A,...,F
> defined like this was probably a bad idea because they are likely to get used
> for other things. My next reaction was to only want to define the decimal digits
> 0,...,9 and have 10,...,15 represented in some other way, but I couldn't come
> up with anything clean, so perhaps it's best to define 10,...,15 as well.

My approach was to define an "enumerated type" :hex with elements x0, x1, ... x9,
xa, xb, xc, xd, xe, xf (I sort of have misgivings about using "obvious" variable
names like x1) and then defining a valuation function to the obvious :num's

--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		"They didn't like the rates, they don't like the poll tax,
		 and they won't like the council tax."   - Nicholas Ridley