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 email@example.com 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.
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.
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.
- 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
- 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.
val it = |- !m n. SUC (m + n) = m + SUC n : thm
val it = |- !m n. m + SUC n = SUC (m + n) : thm
- You can apply a conversion as a tactic by applying CONV_TAC to
- 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 firstname.lastname@example.org to join the mailing list.