Date: Thu, 27 Oct 88 17:55:12 BST
From: tfm%computer-lab.cambridge.ac.uk@NSS.Cs.Ucl.AC.UK (Tom Melham)
To: info-hol%clover.ucdavis.edu@NSS.Cs.Ucl.AC.UK
Subject: RE: type definitions
Message-Id:  <8810271658.aa05233@scaup.Cl.Cam.AC.UK>


I suspect the problem of defining a type of "symbol tables"
(recently posted by Phil Windley) can be solved using my
package for automating recursive type definitions. (This
has been installed in the forthcoming new release of HOL.)

As far as I can tell, Phil wanted a type :(*)symtab with a
recursive constructor:

     addid: (*)symtab -> string -> (*)list -> (*)symtab

and a selector:

    retrieve: (*)symtab -> string -> (*)list

such that:

    retrieve (addid symtab id attrlist) id'
        = (id = id') => attrlist | retrieve symtab id'

Such a type can be defined by a grammar:

    symtab  =  empty | addid symtab string (*)list

This defines :(*)symtab to be the smallest set constructed by
the constructors empty and addid.  In HOL88, a formal type
definition for :(*)symtab can be done as follows:

% ----------- start of HOL88 session ------------------------------ %

#let thm1 =
     define_type `symtab`
                 `symtab  =  empty | addid symtab string (*)list`;;
thm1 =
|- !e f.
    ?! fn.
         (fn empty = e) /\ (!s l s'. fn(addid s' s l) = f(fn s')s l s')

#let retrieve =
     new_recursive_definition false thm1 `retrieve`
        "retrieve (addid symtab id attrlist) id':(*)list
                  = ((id = id') => attrlist | retrieve symtab id')";;
retrieve =
|- !symtab id attrlist id'.
    retrieve(addid symtab id attrlist)id' =
        ((id = id') => attrlist | retrieve symtab id')

% ----------- end of HOL88 session -------------------------------- %

The first interaction above defines the type :(*)symtab and binds the
resulting abstract axiom for this type to the variable thm1.

The second interaction defines the function "retrieve", as desired.
Note that the "selector" retrieve is not an essential feature of
the type's axiomatization; it's just a recursive function defined
by "primitive recursion" on :(*)symtab.

The recursive types package used above will be included in the
forthcoming release of HOL88.  It makes the formal definition of
logical types like :(*)symtab trivial; the user just gives an
abstract grammar for the desired type.  The formal details of
the underlying definition for :(*)symtab are quite messy.  But
the automatic package used above hides all this from the user.

I should add a little note here about type definitions: if you've
"defined" a new type in HOL by using the ml function new_type, then
you haven't DEFINED the type at all!  The goal is to define types
using only new_type_definition.

Tom Melham