HOL Source File Syntax

Files written by HOL users are of the same form as those written by HOL developers. In this way, HOL aims to be easy to extend, and this chapter’s description of HOL source files should be useful for users and developers both.

HOL organises its files into two categories:

• “script” files that specify a theory segment: where definitions are made, types defined and theorems proved; and

• “library” files that provide SML implementations of important theorem-proving infrastructure, typically providing SML functions to support those actions done in script files (definitions, types, proofs).

Library files are written in SML, using the HOL API that is described both in this manual, but also in REFERENCE. Script files have their own rather special syntax that is a superset of SML. Script files will be the bulk of what most users write. Both flavours of file should observe the conventions documented in this chapter.

Library Files

A library is typically implemented in two SML files, Libname.sig and Libname.sml, where Libname.sig defines the SML signature for the library, and the corresponding .sml file provides the implementation. Conventionally, the stem of the file-name is also the name of both the signature and the structure. If our library is called “foo”, then foo.sig would have content:

   signature foo =
   sig
    …
   end

and foo.sml would contain

   structure foo :> foo =
   struct
    …
   end

Because of the link between the file-name and the SML structure’s name, the stem of the file-name will always be a valid SML identifier (ruling out hyphens, for example). It is permitted to omit the signature and to have no ascription in the .sml file. To support Moscow ML, when there is a signature, it is recommended to always use opaque ascription with the :> token.

By convention, a library written to support work with respect to a particular concept or type will often be called conceptLib. Thus, wordsLib supports work with the type of fixed-width words. Another common flavour of library is the so-called “syntax” library, designed to support working with terms and types related to these common syntaxes. Thus, HOL provides the library optionSyntax, where the SML function mk_some of type term -> term, builds a HOL term with the HOL constant SOME applied to the provided argument. Occasionally, a conceptLib library will import and re-export the contents of a linked conceptSyntax library.

Generally, library implementations should only provide entry-points to effect changes to the global state of the system; they should not directly make changes themselves. Logical content (definitions of constants, proofs of theorems, etc.) should always be prompted by user‐written function calls in script files. Changes to other aspects of the global state (e.g., the state of the grammar) should also only happen in the body of functions provided by the library, not as a side effect of the library being loaded.

Script Files

When writing a theory called name, the user must write a file with name nameScript.sml. This will ultimately generate an SML structure that users will be able to refer to as nameTheory. That generated structure will contain bindings for the user’s definitions and theorems. For example, HOL comes with a dividesScript.sml that when built allows:

> dividesTheory.prime_def;
val it = ⊢ ∀a. prime a ⇔ a ≠ 1 ∧ ∀b. divides b a ⇒ b = a ∨ b = 1: thm

The recommended syntax for a script file begins

   Theory <thyname>
   Ancestors <thy1> <thy2> ..
   Libs <lib1> <lib2> ..

   <Script Declarations>

The three keywords (Theory, Ancestors and Libs) must all appear in column 0 of the input file. The Ancestors and Libs components may be omitted.

The name following the Theory keyword must match the name that precedes the Script.sml of the file-name, and must be a valid SML structure identifier. In some cases, such as when a theory is huge and the theorems not particularly interesting, it is possible to disable the generation of documentation in <thyname>Theory.sig by following the theory name with the no_sig_docs annotation. The other annotation possible in this position is bare, which is used to indicate that the theory is built with the minimal hol --bare mode (and won't be using the facilities in bossLib, for example). We expect this modifier should only be necessary for developers.

If present, the names following Ancestors identify theories that this theory builds upon. These names should be “bare”: they cannot include the Theory suffix. By default, all of the SML identifiers within the exported theories mentioned in this section are available without qualification. Thus, if list is one of the names following Ancestors, one need not write listTheory.MAP in the rest of the file to refer to its theorem MAP, but can instead write simply MAP. If two ancestor theories use the same names for their exported theories, the names belonging to the theory whose name occurs later in the Ancestors list will shadow earlier occurrences.

It is reasonable and permitted to list a theory as an ancestor solely to be able to write its names without qualification. For example, one need not explicitly write pred_set as an ancestor because pred_setTheory is always included in HOL’s standard logical context. Nonetheless, one might mention it in order to be able to write IN_INSERT instead of pred_setTheory.IN_INSERT. Conversely, one might want a theory as an ancestor, but not to have its SML names available at the top-level. This effect is achieved by following the theory name with the [qualified] annotation.

In some situations, one wants to have a theory as an ancestor, but not to use its notations and other grammar changes. To achieve this, the ignore_grammar attribute can be used.

The names following the Libs keyword are the names of HOL libraries that the script-file depends on. These can also be imported in qualified fashion.

Finally, both ancestors and libraries can be given aliases for easy (qualified) access with the alias modifier. For example, if one writes Libs fooLib[alias=F], then fooLib's bindings are available in the SML structure F, allowing one to write F.entrypoint. Aliases can be used with or without the qualified option.

For convenience, the qualified and ignore_grammar options can be given “all at once” to a number of theory or library dependencies by attaching these attributes (again in square brackets) to the relevant Ancestors or Libs keyword directly. The alias=ident modifier does not make sense immediately after the Ancestors and Libs keywords; it should only be used after individual theory or library names to establish aliases for just those names.

Table: Script File Syntax. Square brackets in the table are input characters; they are not meta-characters (unlike the parentheses, pipe symbols and superscripts). All keywords beginning with capital letters (Theory, Ancestors, Libs, ...) must occur in column 0 of the input file.

Table: Syntax for expressing theorem proofs, definitions and other theory changes. Again, upper-case keywords (End in particular, despite the table layout), must occur in column 0.

Attributes

Many commands take a variety of attributes to modify or tweak the behaviour of the command. Attribute specifications are added to commands, usually after user-provided identifiers, within square brackets using a common syntax:

If multiple identifiers appear to the right of an equals-sign in the above syntax, they are separated by whitespace. Libraries can enable more attributes than this core set for theorems and definitions; this allows theorem values to be stored in custom data-sets for later retrieval by customisable tools.

In addition, the Resume command is required to include an attribute list that has as its first element the name/label for the particular sub-case that is to be proved in this resumption block.

The following describes the attributes listed above:

by_nametype

Used with Overload. This requires the SML-expression that appears after the =-sign in the syntax to be of type {Thy : string, Name : string} (normally this argument is a term), and maps to the underlying overload_on_by_nametype or temp_overload_on_by_nametype SML calls.

compute

Used with Theorem forms. This causes the theorem value to be added to the global “computation set” that is used by EVAL.

cong

Used with Theorem forms. This adds the corresponding theorem to the set of congruence rules used by the termination analysis behind function definition.

exclude_frags=...

Used with Proof or Resume. The list of fragment names following is removed from the global simpset for the duration of the given proof, affecting all simplifier tactics that refer to the global simpset. The exclusion is sticky: while it is in effect, attempts to add back a fragment with one of the named names via the ++ operator (including those performed implicitly by derived simpsets such as the one used by simp[]) are silent no-ops. To opt back in for a specific simplification call, use the SF marker in its theorem-list argument (e.g. simp[SF ARITH_ss] inside a Proof[exclude_frags = ARITH] body re-enables ARITH_ss for that one call).

exclude_simps=...

Used with Proof or Resume. The list of theorem names following is removed from the global simpset for the duration of the given proof. Names are not SML identifiers, but rather references to the names used internally by the simpset (visible by examining it with a call to srw_ss()), and can be given without theory-qualification. For example, with or without sumTheory’s identifiers visible to SML, one can use exclude_simps=ISR to stop the ISR rewrite from being used.

ind=⟨ident⟩

Used with Definition. Specifies the name for a recursive function's induction theorem.

inferior

Used with Overload. Makes the chosen overload “least liked” by the parsing and printing machinery. It will be chosen last when resolving ambiguous parses, and will only be used when printing if no other overload matches.

local

Used with Overload, Theorem, and Type. Makes the “effect” of the corresponding keyword local to the script file, meaning it will not persist into descendent theories. In the case of Theorem, this means the theorem will not be exported, and so it will not be possible to refer to it as fooTheory.ident in descendents. For the parsing directives, the changes to the grammar are not exported.

mono

Used with Theorem. Adds the theorem to the list of monotonicity results used by the inductive/coinductive definitions package.

nocompute

Used with Definition. This stops the definition theorem from being added to EVAL’s global “computation set”, which otherwise happens by default.

pp

Used with Type. Causes the new type abbreviation to be used when types are printed; by default, abbreviations are used only for parsing strings into types.

rule_induction

Used with Theorem. Makes the provided theorem available for use as a rule induction principle when using the Induct_on tactic.

schematic

Used with Definition. Allows schematic definitions.

simp

Used with Theorem and Definition. Adds the corresponding theorem to the global simpset. This effect will not persist beyond the current script file where it occurs if used with a local attribute.

smlname=⟨ident⟩

Used with Resume. Gives the subresult corresponding to this theorem resumption the name ⟨ident⟩ in the SML namespace.