Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) outside ac.uk; Mon, 29 Mar 1993 15:54:39 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA28735;
          Mon, 29 Mar 93 06:29:54 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA28730;
          Mon, 29 Mar 93 06:29:45 -0800
Received: from guillemot.cl.cam.ac.uk (user tfm (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) to cl; Mon, 29 Mar 1993 15:28:48 +0100
To: val@com.netcom (Dewey Val Schorre)
Cc: info-hol@edu.uidaho.cs.ted, Tom.Melham@uk.ac.cam.cl
Subject: Re: Beginners Questions
In-Reply-To: Your message of Mon, 29 Mar 93 05:45:03 -0800. <9303291345.AA28769@netcom2.netcom.com>
Date: Mon, 29 Mar 93 15:28:36 +0100
From: Tom Melham <Tom.Melham@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.578:29.03.93.14.29.08"@cl.cam.ac.uk>


> that are related to my problem. Is there a list of the Pre-defined ML 
> identifers that are grouped together in a logical way?

I'm afraid there is no really good subject index of ML identifiers in
HOL (despite the half-baked \KEYWORDS field of .doc files). However, a
very useful concise list of the most important things in HOL is Wai
Wong's summary in contrib/hol-sum.

> 2. Is there a tactic that will drive negation down? For example, 

There is a comprehensive set of conversions for doing this. See section
13.3.6 ("Quantifier movement conversions") of DESCRIPTION (latest
edition).  Use CONV_TAC and the depth conversions (see section 13.2) to
create the required tactics.

> 3. Where are 0 and 1 defined. I want to prove ~(0=1).

You should be aware of num_CONV (see DESCRIPTION). This allows you to
prove

   |- 1 = SUC 0

The following built-in fact 

    SUC_NOT arithmetic
    |- !n. ~(0 = SUC n)

then immediately gives |- ~(0=1).  Alternatively, use the function
REDUCE_CONV in the extremely useful reduce library in version 2.01:

    #REDUCE_CONV "0=1";;
    |- (0 = 1) = F

> 4. Are that there functions that would list all currently available:
> 
>      1) theorems
>      2) tactics
>      3) conversions
>      4) derrived rules of inference

I'm afraid not, but again see Wai Wong's useful summary.

Tom