Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
From: Konrad Slind <slind@de.tu-muenchen.informatik>
To: info-hol@edu.uidaho.cs.ted
Subject: finding things in hol
Message-Id: <93Mar29.173949met_dst.8067@sunbroy14.informatik.tu-muenchen.de>
Date: Mon, 29 Mar 1993 17:39:38 +0200


Val asks

> Often however, I'm trying to write a program of my own and I want to
> find the pre-defined ML identifiers that are related to my problem. Is
> there a list of the Pre-defined ML identifers that are grouped together
> in a logical way?

This is a problem with HOL, I must admit. Last I counted (in hol90),
there were about 800 SML identifiers that had specifically to do with
HOL, plus about another 600 acessible in the pervasive environment. This
can only become worse when other libraries are added. It's not *so* bad
in SML, since things have been bundled into structures, but how does one
find the name of the right structure?

The latest release of SML/NJ has external documentation for this which
ought to help. There is also a somewhat slow (last I checked) tool
called "info" (found in the "tools" directory of the SML compiler
distribution) for finding out the contents of the current top-level
environment.

In any case, in hol90, a short answer to your question is that the
following are some of the important (pre-opened) structures in the
pervasive environment

 Ref List Vector Array RealArray  ByteArray Io Bool String Integer 
 Bits Real General System

to see what they provide, one merely does an "open" on the structure:

    - open List;

    open List
    exception Hd = Hd
    exception Tl = Tl
    exception Nth = Nth
    exception NthTail = NthTail
    val hd = fn : 'a list -> 'a
    val tl = fn : 'a list -> 'a list
    val null = fn : 'a list -> bool
    val length = fn : 'a list -> int
    val @ = fn : 'a list * 'a list -> 'a list
    val rev = fn : 'a list -> 'a list
    val map = fn : ('a -> 'b) -> 'a list -> 'b list
    val fold = fn : ('a * 'b -> 'b) -> 'a list -> 'b -> 'b
    val revfold = fn : ('a * 'b -> 'b) -> 'a list -> 'b -> 'b
    val app = fn : ('a -> 'b) -> 'a list -> unit
    val revapp = fn : ('a -> 'b) -> 'a list -> unit
    val nth = fn : 'a list * int -> 'a
    val nthtail = fn : 'a list * int -> 'a list
    val exists = fn : ('a -> bool) -> 'a list -> bool

> 4. Are that there functions that would list all currently available:
> 
>      1) theorems

You could try

    map (fn thy => (definitions thy @ theorems thy)) (ancestry"-");

although this is not for the resource-challenged.

>      2) tactics, conversion, derived rules of inference

In hol90 the system tactics are in the structure Tactic; tacticals are
in Tactical; conversion are in Conv; and many of the basic derived rules
and simple theorems about the type "bool" are in Drule. Most of the
system is available through the structure Hol1:

    - open Hol1;
    open Hol1
    structure Induct_then : Induct_then_sig
    structure Thm_cont : Thm_cont_sig
    structure Type_def_support : Type_def_support_sig
    structure Tactic : Tactic_sig
    structure Resolve : Resolve_sig
    structure Base_logic : Base_logic_sig
    structure Lib : Lib_sig
    structure Exception : Exception_sig
    structure Term_io : Term_io_sig
    structure Globals : Globals_sig
    structure Rewrite : Rewrite_sig
    structure Conv : Conv_sig
    structure Drule : Drule_sig
    structure Taut_thms : Taut_thms_sig
    structure Tactical : Tactical_sig
    structure Goal_stack : Goal_stack_sig
    structure Prim_rec : Prim_rec_sig


Konrad.