Notes for HOL90 Beginners

Having started to learn HOL90 without the aid of a HOL90 specific manual, I've put together this page in hopes of helping other beginners over the early hurdles that I encountered in trying to learn to use the system. This is in no way intended to be a full tutorial for HOL90; it is basically a reference page for the things I`ve needed to know so far in order to start seriously playing with HOL90. Send any corrections or suggestions about these notes (including other personal notes that might be helpful to beginners) to me (Kathi Fisler) at kfisler@cs.indiana.edu and I'll add them to the page. (I may also try to keep them updated as I learn more, but I don't make any promises on that front.)

The HOL Documentation System

Presumably, if you found this page you have also found the on-line documentation system for HOL. The information here is quite thorough, with it's only drawback being that it is written for HOL88 as opposed to HOL90. I've put together a series of notes for adapting the existing on-line tutorial to HOL90. I found that most of the existing documentation is easily usable in HOL90 once you've figured out a few syntactic differences. Most of the rest of this page will make no sense unless you've done the tutorial or had some prior experience with the system.

SML/NJ

HOL90 is implemented on top of SML/NJ, so knowing some of that system helps.

Help for Error Messages

If you get a HOL_ERROR from typing "exp;", typing "exp handle e => Raise e;" usually returns a more detailed error message.

Interactive versus Non-interactive Proof

The distribution files are a good source for sample proofs and definitions (I've also provided a very easy theory definition with some proofs below), but there are some minor tricks that might help you use the system interactively.

It helps tremendously to run HOL90 inside of Emacs. You can either refer to the information on this in the HOL documentation, or you can simply run HOL90 within a shell running inside of Emacs. I've found it very helpful to use a large Emacs screen, split it in two (C-x 2), and run HOL90 in one half while editing an Emacs file with the theory I'm trying to write in the other half. This allows me to construct a non-interactive proof in the file as I find the steps work in the interactive proof. I've yet to find a built-in way to save the steps taken in an interactive proof.

I've found two ways to use steps saved in a file on an interactive proof. One is to cut and paste steps from the file into an e( ) at the HOL90 prompt (this is one reason why running in emacs is a great help). The other is to just cut and paste the steps into the session without the e( ). If you do the latter, the variable "it" now contains a tactic that performs the series of pasted steps. This tactic can be applied by typing

 e it;

at the prompt. I find this is sometimes helpful in debugging the syntax of the commands without affecting the goalstack history.

Learning the HOL style of proof

Once you understand the syntactic differences between HOL90 and classic HOL, the on-line documentation can be used easily for learning how proofs work in the system. Read the HOL description manual for information on tactics, conversions, rewriting, and anything else you need to know to get started.

Miscellaneous Notes

This is a random collection of things that I have picked up or needed to know while learning the system.

The backup(); command demonstrated in the tutorial can be abbreviated as b();
Sometimes you need to add typing information when trying to discharge assumptions, even if that information is not displayed in the assumption. For example, in the following proof fragment, I want to discharge (--`x t`--), where x is a function from num to bool.
```
  ____________________________
      (--`x t`--)
      (--`y t`--)
  
   : goalstack
- e(UNDISCH_TAC (--`x t`--));
Unconstrained type variable in the variable
   (x :?2 -> ?3)

Exception raised at Preterm.typecheck_cleanup:


uncaught exception HOL_ERR
-
```
If the command is given as
```
e(UNDISCH_TAC (--`(x:num->bool) t`--)); 
```
it will discharge without error.
If you are working interactively and have made enough errors that the goal stack is no longer visible on the screen, typing
```
e(ALL_TAC); 
```
will bring up the current goal stack without changing it. I've been told that the stack history (what you can undo with backup) is limited to 15 steps, so after the ALL_TAC you might want to backup once, to avoid leaving the ALL_TAC in the goal history.
When rewriting, HOL90 rewrites the left side of a theorem with the right. If you need to rewrite the right side with the left, you have to manually switch the right and left hand sides using the GSYM command before trying to rewrite.
```
- ADD_SUC;
val it = |- !m n. SUC (m + n) = m + SUC n : thm
- GSYM(ADD_SUC);
val it = |- !m n. m + SUC n = SUC (m + n) : thm
```
You can apply a conversion as a tactic by applying CONV_TAC to the conversion.
Certain single-letter variable names are reserved as combinators in the language, and are not available for use in your own definitions. I ran into this problem trying to use the letter o to define a function from num->bool. I don't know the full list of such letters, but be aware of the problem.
Rewriting can sometimes go into an infinite loop if you have a formula that rewrites to something that can itself be rewritten. Using ONCE_REWRITE_TAC (or ONCE_ASM_REWRITE_TAC if you are rewriting with the assumptions) will avoid this problem.

If all else fails ...

and you are UNIX literate, grepping the source files can be very helpful. Look in src/[0,1,2,3]/* in the distribution.

The people on info-hol are also very helpful if you have questions. Send mail to info-hol-request@lal.cs.byu.edu to join the mailing list.