HOL98 Frequently Asked Questions

HOL is failing to complete the build process. It stops when trying to create the HolBdd theory. Why is this, and what should I do? (5)

The problem is almost certainly that your copy of MoscowML hasn't been built with dynamic linking correctly enabled. This in turn means that the Muddy BDD package that HolBdd uses can't load. You can test that this is the problem by running hol, and then trying

     - load "HolBdd";

This should fail with an error message about not being able to load muddy.so.

If you decide you do want HolBdd (there is nothing else in HOL that depends on dynamic linking) you will probably need to build Moscow ML yourself. Binaries from the central site in Denmark don't seem to work. However the install.txt file in the distribution does talk about things you need to do to binaries in order to get dynamic linking to work for them, and it would be interesting to hear that someone had got this to work. In any case, to build from sources, you must make sure that you alter the src/Makefile.inc in the MoscowML distribution in line with the instructions in the comments there.

This advice seems to solve this problem for 90% of the people reporting it. If it doesn't in your case, please get back to us.

How do I antiquote types? (3)

Antiquoting types works as you would expect when parsing types, so that it is fine to write:

         - val ty = Type`:bool`;

and then

         - Type`:num -> ^ty`;

However, you may wish to also introduce type antiquotations into term parses (as a type constraint on a variable for example). The problem is that you can't just write ^ty in this context, because the parsing function's type insists that all antiquotes be of type term. You must use the ty_antiq function, which magically makes a type appear as a term:

         - val antity = ty_antiq ty;
         > val antity = `(ty_antiq(`:bool`))` : term

Then:

         - val x = Term `x:^antity`;

It's quite easy to figure out when and why ty_antiq is required if one understands the type of the parsing functions. For example, Term and (fn q => -- q --) have type

         term frag list -> term

While Type and (fn q => == q ==) have type

       hol_type frag list -> hol_type

The frag list refers to the fact that there is a quotation being consumed. A quotation is something that appears between back-quotes. A quotation consists of strings and antiquotations. A term frag list must have antiquotations that are of type term. A hol_type frag list must have antiquotations that are of type hol_type.

So, if you use Term to parse a term, you can't directly antiquote in types, because this would violate the typing rules (you can only antiquote in terms if you call Term, because it requires a term frag list).

So, in order to accomplish this there is a bit of magic called ty_antiq, which if you look at its type (hol_type -> term) turns a type into a term. The term formed is completely bogus in a logical sense (it's actually a var with a special name and the given type), but can be pushed into the parsing function Term so as to give the effect of antiquoting a type.

The function Hol_datatype takes a hol_type frag list, so if you want to antiquote a type into the quotations it takes, you will not need to ty_antiq it.

Are error messages during the build like the following a source for concern? (2)

 
   > File "Term.sml", line 1328, characters 10-42:
   > !   let val {const=Const(r1,_),theory,place} = const_decl name
   > !           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   > ! Warning: pattern matching is not exhaustive

No. Nor is the following sort of output, when configuring the system before building:

     > /local/scratch/kxs/144/bin/mosmlyac: 4 shift/reduce conflicts.

Why can't I write ``MAP ~ x``? (1)

When you attempt this, you will get the error message

       No rule for [~]

meaning that the parser wants to do a reduction involving just the special symbol ~, and it can't find a rule that allows this. The rule in the grammar is TM ::= ~ TM.

~ is treated specially, and not just as a function that you'd apply to arguments normally, for two reasons:

• it can have precedence weaker than just function application. This means that when you write ~f x, this is parsed as ~(f x).

• it can group without needing extra parentheses, so you can write ~~b; you don't need to write ~(~b).

To make ~ lose its special status, you should prefix it with a $. ``MAP $~ x`` will work in the example, assuming that x has type :bool list.

How do I prove strings equal or inequal? (1)

Use stringLib.string_EQ_CONV, which reduces equalities over string literals to either T or F. For example, to demonstrate that ``(if "foo" = "bar" then 3 else 1) = 1``, you could write:

     - val t = ``(if "foo" = "bar" then 3 else 1)``;
     > val t = ``(if "foo" = "bar" then 3 else 1)`` : Term.term
     - (DEPTH_CONV stringLib.string_EQ_CONV THENC REWRITE_CONV []) t;
     > val it = |- (if "foo" = "bar" then 3 else 1) = 1 : Thm.thm

I'd like to use MEM as an infix, not a Prefix. Can I do this? (1)

Yes! Use grammar manipulation functions such as set_fixity to alter its parsing information. These changes can be made to persist when the current theory is exported. For example:

       - load "listTheory";
       - set_fixity "MEM" (Infixr 450);
       > val it = () : unit
       - listTheory.MEM;
       > val it =
           |- (!x. x MEM [] = F) /\ !x h t. x MEM (h::t) = (x = h) \/ x MEM t
           : thm

How do I get a datatype's axiom after using Hol_datatype? (1)

Use TypeBase.axiom_of (valOf (TypeBase.read "mytypename")). Hopefully you won't need to do this very much because many of the contexts in which you previously needed the axiom will be dealt with more smoothly. For example, cases, induction, one-one and distinctness theorems are now proved automatically, and are available from the TypeBase. For example,

     TypeBase.one_one_of (valOf (TypeBase.read "mytypename"))

How to rewrite with a theorem the other way round? (0)

Use GSYM

What's with all this "cut looping" stuff? (0)

It's the simplifier, and it's turned off in Taupo releases onwards unless you set the trace level to one or higher.

How can I find out more information about a HOL_ERR exception? (0)

If expression e is causing the grief, then write (e) handle E => Raise E (Often the parentheses around e will not be required.)

How do I put hol98 in a state so that theorem assumptions are printed? (1)

show_assums := true; 

This flag, along with several others that control HOL behaviour can be found in the Globals structure.