Taupo-1 documentation

Apart from the online documentation, the tar file for Taupo-1 does not include any further documentation. This makes the tar file smaller. We felt this was particularly wise as different users are unable to read different formats and distributing all possible formats would have been particularly wasteful. There are three components to the official documentation:

Reference. Available as DVI (880 kB), Postscript (1.28 MB), and PDF (942 kB).
Description. Available as DVI (699 kB), Postscript (1.2 MB), and PDF (839 kB).
Tutorial. Available as DVI (256 kB), Postscript (551 kB), and PDF (400 kB).

If you use the hol98 Emacs mode, you might be interested in the one-page reference for the keybindings it uses.

Note

Of the three official documents above, only the Tutorial is in finished condition. The other two still have many vestiges of HOL88 in them. We have tried to document recent changes to the system fairly thoroughly, but documentation for old parts of the system in these two volumes is mainly untouched. This is not to say that it's wrong; in fact, in many cases it is still very useful because very few functions have changed their semantics. However, the examples for most of the old entries in the Reference use HOL88 Classic ML syntax, which might be rather confusing.

Incompatibilities with previous versions

Here is a list of some of the changes from the Athabasca series of releases that may cause users problems:

The Infix fixity no longer takes just a number specifying precedence, instead Infix is of type (int * associativity) -> fixity. This means that where fixities are required, you can no longer write something like Infix 300, and must now write Infix(300, RIGHT) instead. Possible associativities are LEFT, RIGHT and NONASSOC. Alternatively, it is possible to use Infixl and Infixr as abbreviations for the left and right associative versions of Infix. (I.e., you can write Infixl 300.)
The function new_infix_definition no longer exists. Instead, there are two new functions new_infixl_definition and new_infixr_definition with the same signatures. These define left associative and right associative constants respectively.
The function new_recursive_definition no longer takes fixity information at all. Most definitions with this function specified the ("do nothing") Prefix fixity, and because new_recursive_definition can now define multiple (mutually recursive) functions all at once, an interface where one fixity was specified was deemed inappropriate.
You will need to use set_fixity, add_rule or add_infix to manipulate the grammar in a separate interaction. The last two functions above are documented in the Reference manual.
The syntax for type annotations has changed. Type annotations now bind very tightly as suffixes. In practice this seems to make only one difference; where once one would have written (n,b :num # bool), one now should write (n:num,b:bool) or (n,b):num#bool. This change makes HOL syntax more like the ML syntax.
The tupled constructor and destructor functions (dest_comb, mk_abs etc) are now open when an interactive HOL session begins. The "record" versions of these functions are still available through the Rsyntax structure.
The associativities of many arithmetic operators have changed to be left associative. Affected are addition, subtraction, multiplication and division in all of the numeric libraries. If you have code that depends on these associativities, and you do not wish to change it, you can alter the grammar in effect at the top of the relevant script fairly simply. There is a discussion on page 146 of the Description on how to do this.
The old nested recursive types definition package (Def_MN_Type, or the underlying nested_recLib) expects datatype axioms for types such as lists under which recursive occurrences are nested. These axioms need to be of the "old" form (with a unique existence constant ?!), not the new. For example, the old list axiom is listTheory.list_Axiom_old. In any case, it's recommended that such definitions be reworked to use the Hol_datatype function.
Similarly, the axioms produced by define_type can now no longer be used as input to the new_recursive_definition function. You can convert old style axioms to new style ones, by using Prim_rec_Compat.old_style_to_new.
The theory restr_binderTheory has been merged into res_quanTheory.
Because some operating systems can't handle case senstive file-names very well, ListTheory has been renamed to rich_listTheory.

The bossLib function primDefine no longer exists. This is an oversight that will be corrected in Taupo-3. Here's a workaround; the effect of

         primDefine (Term`fact(x) = (x=0 => 1 | x*fact(x-1))`) Prefix "fact";

       > val it =
          |- (fact x = ((x = 0) => 1 | (x * fact (x - 1)))) /\
             (!P. (!x. (~(x = 0) ==> P (x - 1)) ==> P x) ==> (!v. P v))

can be obtained by

         val tm = Term`fact(x) = (x=0 => 1 | x*fact(x-1))`;

         xDefine "fact" `^tm`;

         Equations stored under "fact_def".
         Induction stored under "fact_ind".
         > val it = |- fact x = (if x=0 then 1 else x * fact (x-1)) : Thm.thm

         - theorem "fact_ind";
         > val it = |- !P. (!x. (~(x = 0) ==> P (x - 1)) ==> P x) ==> !v. P v

Michael Norrish <Michael.Norrish@cl.cam.ac.uk>

Last modified: Mon Jun 26 12:36:27 BST 2000