guidebook.smd

% [HOL Guidebook][Guidebook]
<!--
>>__ val () = elision_string1 := " (* output elided *)";
-->

Introduction
-------------

HOL stands for higher-order logic. HOL is also the name of a theorem prover,
the [HOL theorem prover][HOL website]. This is a guidebook for the theorem
prover.

I assume you are familiar with [functional programming][w:fp] and [higher-order
logic][7]. (If you are not, don't worry, these topics will be treated gently
and are easy to pick up.) The main point of this tutorial is to show you how to
build theories in the HOL theorem prover, assuming you have an idea of what you
want to formalise and how to prove your theorems mathematically.

If you have trouble with anything, there is plenty of community support
available including mailing lists and online chat. See the [HOL website][]
for details.

For support on or contributions to this guidebook itself, see its repository on
[GitHub][Guidebook].

[HOL website]: https://hol-theorem-prover.org
[Guidebook]: https://github.com/HOL-Theorem-Prover/hol-guidebook
[7]: http://www.cas.mcmaster.ca/sqrl/papers/SQRLreport18_rev2.pdf
[w:fp]: https://en.wikipedia.org/wiki/Functional_programming

Installation
-------------
Go to the [HOL website][].
Follow the instructions there to install HOL.

Alternatively, you can follow the first part of the
[CakeML build instructions](https://code.cakeml.org/tree/master/build-instructions.sh).

It is a good idea to set the environment variable `$HOLDIR` to point to the
location of your HOL installation. I will refer to this directory by `$HOLDIR`
from now on.

Running hol
------------
Now you can run `hol` at the command line. You will be greeted with a welcome
message, and prompted with a read-eval-print loop (REPL). This is in fact the
REPL for the underlying ML system.

HOL is just a library for theorem proving in <a href="http://sml-family.org/">Standard ML</a> (abbreviated as ML).
Interacting with HOL, therefore, can be seen as programming in ML. If you don't
use any of the HOL-specific parts, you just have Standard ML:

     >> 3 + 4;

The HOL additions include new datatypes like `thm`, which represents a proven
theorem. Some values of this type are already in scope:

     >> SKOLEM_THM;

Script files
-------------
Usual practice is not to program directly at the REPL. Instead, you write a
_script file_ which can be processed by a tool called `Holmake` to build a
theory. A typical script file looks like this:

    open HolKernel boolLib bossLib Parse;

    val _ = new_theory"test";

    (* SML declarations  *)
    (* for example: *)
    val th = save_thm("SKOLEM_AGAIN",SKOLEM_THM);

    val _ = export_theory();

The script file above should be saved as `testScript.sml`, because the name passed to `new_theory` is `"test"`.
To produce a theory from this script file, run `Holmake` as follows:

    $ Holmake testTheory.uo

`Holmake` knows to look for `testScript.sml` when given the target `testTheory.uo`.
It will run the script and produce the following files as output:
`testTheory.sig`, `testTheory.sml`, `testTheory.ui`, and `testTheory.uo`.

The `testTheory.sig` file contains a summary of the contents of the generated
theory.  In this case, you will see that `testTheory` contains a single
theorem, which is just a copy of `SKOLEM_THM` saved under the name
`SKOLEM_AGAIN`.

The other generated files are the mechanism by which persistent theories are
implemented on disk, and can be ignored for now.

Interaction
------------
One would like to develop a script file with the same ease as programming at
the REPL. For this, there are plugins for two text editors, Vim and Emacs,
which enable script-file writing alongside an interactive HOL session. Both are
included in your HOL installation. The Vim plugin is documented at
`$HOLDIR/tools/vim/README` ([also here](https://github.com/HOL-Theorem-Prover/HOL/tree/master/tools/vim/README)).
The Emacs plugin is documented [online](https://hol-theorem-prover.org/hol-mode.html).

The idea behind these interaction plugins is to write a script file that will
eventually be suitable for processing by `Holmake`, but to see, step-by-step in
the REPL, what is happening at each point of the script file as you are writing
it.

As an example, let's try the Vim plugin on the `testScript.sml` file from
above. First, install the Vim plugin by following the instructions in its
`README`. Next, open `testScript.sml` in Vim, and also start `hol`. I usually
put these two windows (`hol` and `vim`) side by side, so I can see what is
happening in both at once.

We begin processing from the top of the file. Select the first line (the one
containing `open`). (To select a line in `vim`, position the cursor on the line
and press `V`.) Tell `hol` to load those theories and libraries by typing `hl`.
You should see some output like:

    HOLLoadSendQuiet HolKernel boolLib bossLib Parse completed

Next, move down to the line containing `save_thm` and send it to `hol` by
typing `hs`. You should see some output like:

    >>- val th = save_thm("SKOLEM_AGAIN",SKOLEM_THM);

You can, at this point, also write directly into the REPL if you want.
For example, to see that this theorem has no hypotheses, try:

    >> hyp th;

But of course, if you want to add anything to the theory you produce, you
should write it in the script file.

Types
------
The syntax of higher-order logic includes types and terms. These are two of the
main datatypes implemented by HOL, over and above what is provided by ML. Here
is a type:

    >> bool;

In fact, `bool` is one of a handful of types that are bound to ML variables by
default. In general, you can make a type by providing the name of a type
operator and a list of arguments:

    >> mk_type("bool",[]);

    >> mk_type("list",[bool]); (* the type of a list of Booleans *)

    >> dest_type it;

Type variables can also be made by providing a name.

    >> mk_vartype("'test");

    >> mk_vartype("'f");

    >> dest_vartype it;

Type variable names, by convention, start with a single quote, unless they are a Greek letter.
The first several letters of the (Roman) alphabet are synonymous with certain Greek letters (as demonstrated above).

Every type in HOL is either a type variable or a type operator (like `list`) applied to type arguments.
Even `bool` is a type operator; it has no arguments.

Logically, there are only two primitive type operators: `bool`, and `fun`, the type of functions.
Others, like `list`, are defined types, but they are already defined by default.
Function types can be manipulated as follows.

    >> val ty = bool --> alpha;

    >> dom_rng ty;

    >> dest_type ty;

If you try to destruct a type operator as if it were a variable, HOL will raise an exception.

    >> is_vartype bool;

    >>+ dest_vartype bool;

Parsing
--------
It is often more convenient to call the _type parser_ rather than `mk_type` directly.
Compare these alternatives for building a certain type.

    >> mk_type("fun",[mk_type("list",[mk_type("num",[])]),mk_type("num",[])]);

    >> let val num = mk_type("num",[]) in mk_type("list",[num]) --> num end;

    >> ``:num list -> num``;

The backticks (\`) above are special syntax provided by HOL for calling the
type parser. The underlying parser function is called `Type`. We can call the
parser more directly:

    >> Type `:num list -> num`;

The single backticks represent another special syntax, this time for a
_quotation_. Removing the special syntax entirely, we can write:

    >> Type [QUOTE":num list -> num"];

The string passed to the type parser should start with a colon as above.

Types can include variables. `alpha` is bound to a type variable, which can also be written as `:'a`.

    >> alpha; ``:'a``;

(In the example above, two results are printed because two declarations were provided.)

Quotations can include values that do not need to be parsed. For example:

    >> ``:^alpha list``;

    >> ``:^(mk_type("list",[alpha])) list``; (* list of lists of alphas *)

The last input expression is syntactic sugar for:

    >> Type [QUOTE":", ANTIQUOTE (mk_type("list",[alpha])), QUOTE " list"];

Terms
------
The terms of higher-order logic include: variables, constants, abstractions, and
combinations (sometimes called applications).
I will show examples of all these kinds of terms, made both using term-making
functions directly and using the term parser.

#### Variables
A variable is identified by a name and a type.

    >> val x = mk_var("x",beta);

    >> val x = ``x:β``; (* or ``x:'b`` *)

If you don't provide a type, HOL will invent one.

    >> val y = ``y``;

Variables are equal if and only if both their name and type match.

    >> Term.compare (y,``y:'b``);

    >> Term.compare (y, mk_var("y",alpha));

#### Constants
A constant also has a name and a type.

    >> val z = mk_const("0",``:num``);

    >> val z = ``0``;

Unlike variables, the type of a constant is fixed.

    >>+ mk_const("0",bool);

So why provide a type at all? Because constants can be _polymorphic_.
More details about polymorphism [below][polymorphism].

Furthermore, unlike variable names, constant names are scoped into theories.
More details about theories [later][theories].
The full name of a constant can be recovered with `dest_thy_const`.

    >> dest_thy_const z;

#### Abstractions
An abstraction represents a function.
It consists of a variable and a term (body).

    >> val f = mk_abs(x,z);

    >> val f = ``λx:β. 0``; (* or ``\x:'b. 0`` *)

    >> dest_abs f;

Terms can be tested for _alpha-equivalence_, which means equality up to a renaming of bound variables, using `aconv`.

    >> aconv f (mk_abs(y,z));

    >> val y' = mk_var("y",beta);

    >> aconv f (mk_abs(y',z));

To see why the first version is false, recall the type of `y` declared above.

    >> dest_var y;

A more interesting example follows.
The syntax `λx y. b` is shorthand for `λx. (λy. b)`.

    >> val f1 = ``λx y. ¬x``;

    >> val f2 = ``λy x. ¬x``;

    >> val f3 = ``λy x. ¬y``;

    >> aconv f1 f2;
    >> aconv f1 f3;

In `f1`, the type of `y` is invented, but the type of `x` is fixed (as `:bool`) by _type inference_.
The Boolean negation operator (`¬`) takes a Boolean argument, so HOL infers that its argument must have type `:bool`.

#### Combinations
A combination represents application of a function to an argument.

    >> mk_comb(f,y');

The syntax is simply juxtaposition of function with argument.

    >> ``f y``;

The type of the argument must match the domain of the function's type.

    >>+ mk_comb(f,y);

To understand why this fails, recall that `f` requires an argument of type `β`, but `y` has type `α`.

    >> val (v,b) = dest_abs f;
    >> dest_var v;

When \``f y`\` was given to the term parser, it invented new types to ensure the application was type-correct.
In fact, the HOL variables in that quotation are unrelated to the ML variables `f` and `y`.

Every function in HOL takes one argument, but multiple arguments can be implemented using higher-order functions by [_currying_](https://en.wikipedia.org/wiki/Currying).

    >> val fxyz = ``f x y z``;

    >> dest_comb fxyz;

All the arguments can be stripped off at once.

    >> strip_comb fxyz;

The counterpart for creating multiple applications at once is `list_mk_comb`.

    >> val tm = list_mk_comb (f3,[``x:bool``,y]);

There is shorthand for extracting either of the results of `dest_comb`:

    >> rator tm;

    >> rand tm;

These functions stand for "operator" and "operand" respectively.

The lambda view
---------------

Trying to destruct a variable as an abstraction, or other such mismatches, will raise exceptions.

    >>+ dest_abs ``f``;

However, an arbitrary term can be destructed using `dest_term`.

    >> dest_term ``f``;

    >> dest_term ``λx. x``;

The other `lambda` constructors are `CONST` and `COMB`.

Boolean connectives
--------------------
There are two canonical values of type `:bool`, namely true and false.
In HOL they are written as `T` and `F`, and are also bound by default to ML variables.

    >> T;

    >> Term.compare (``F``, F);

    >> type_of F;

The ML function `type_of`, used above, returns the HOL type of a term.

    >> type_of;

The connectives of Boolean logic can be written using either ASCII or Unicode syntax.
Here are examples using both styles.

    >> ``~p``;

    >> ``p /\ q``;

    >> ``p ∨ q``;

    >> ``x ==> y``;

    >> ``x ⇔ y``;

In HOL, unlike in propositional logic, these connectives have no special syntactic status: they are simply higher-order functions.

    >> val imp = ``x ⇒ y``;

    >> rator imp;

    >> type_of it;

    >> type_of``$~``;

As you can see, when writing partial applications of the connectives, their ASCII names must be used.
Furthermore leading dollar signs must be used, since the default grammar used by the term parser has rules for these connectives expecting them to be fully applied.
Another way to escape the special parsing of infix (and other special) tokens is to use parentheses:

    >> rand ``P (~)``;

Some library functions
-----------------------
HOL comes with a small selection of pre-defined ML functions that are generally useful (and not specific to theorem proving).

The `#1` and `#2` functions are record selectors for elements of tuples in ML.
In HOL they are also defined as `fst` and `snd`.

    >> fst (0,1);

    >> #2 (0,1,2)

The `el` function extracts elements from a list.
It is the same as `List.nth` in ML, but indexes from `1` rather than `0`.

    >> el 2 [1,2,3];

The `|>` combinator does function application.
Thus, `tm2 |> dest_comb` is the same as `dest_comb tm2`.
Its utility is in adding readabilty (and avoiding parentheses) when applying many functions in a row.

    >> ("hi",1,"bye") |> #3 |> String.explode |> el 2;

Traces
-------
In HOL, there is a global table of configuration options called _traces_, which affect the interactive system in various ways.
The list of traces can be found by calling the `traces` function:

    >>_ traces();

Each trace has a name (a string) and a value (an integer). Usually `0` means
off, and `1` means on. For traces with more values, higher numbers
usually mean more of the behaviour.

Traces can be set with `set_trace`.

Unicode
--------

If you are using Vim, the Vim plugin (see [Interaction]) documentation explains how to type Unicode characters using digraphs.
HOL prints output back using Unicode, but you can turn this off if desired.

    >> set_trace "Unicode" 0;

    >> val tm1 = ``x <=> y``;

    >> val tm2 = ``x ⇔ y``;

    >> set_trace "Unicode" 1;

    >> tm1;

Observe that `tm2` actually contains a variable called `⇔`, which is printed with a leading `$` when Unicode is turned on to avoid conflicting with the bi-implication constant (`<=>`).

    >> tm2;

    >> dest_comb tm2;

    >> tm2 |> dest_comb |> #1 |> dest_comb;

    >> is_var (#2 it);

Equality
---------
One important constant in HOL is the equality function, which makes equations.
Recall `f1` and `f3` from the section on [Abstractions].
We can make an equation between them:

    >> val eqn = mk_eq(f1,f3);

    >> lhs eqn;

    >> rhs eqn;

    >> dest_eq eqn;

In fact, we have already seen an instance of equality in the section on [Boolean connectives].
On Booleans, equality is the same as bi-implication.

    >> val iff = mk_eq(``p:bool``,``q:bool``);

However, equality can be applied at any type.
In the first equation above, we find that equality is comparing higher-order functions.

    >> rator eqn;

    >> rator it;

    >> eqn |> rator |> rator |> type_of;

Whereas in the second equation:

    >> iff |> rator |> rator |> type_of;

In general, we have the following _polymorphic_ type for equality.

    >> type_of``$=``;

Polymorphism
-------------
Many constants are polymorphic.
A polymorphic constant has a most general type that includes type variables.
Those variables can be _instantiated_ to form a type instance of the constant.

One example is the `MAP` constant on lists.

    >> type_of``MAP``;

    >> val tm = ``MAP f [T;T;F]``;

    >> strip_comb tm |> #1;

    >> type_of it;

The instance of `MAP` obtained from `tm` is more specialised because it was
applied to a list of Booleans.

To find the most general type of a constant, one can parse the constant and HOL
will invent type variables where it can. A more principled method is to use
`prim_mk_const`, which makes a constant without taking a type as an argument
(and instead returns the instance of the constant with most general type), but
this requires the full name of the constant (as described later under
[Theories]).

Any term can be instantiated with a type substitution, which maps type
variables to types. In the following examples, let us pretty-print terms with
types on.

    >> set_trace "types" 1;

    >> val tm = ``MAP f``;

    >> inst [alpha |-> bool] tm;

    >> inst [alpha |-> bool, beta |-> alpha] tm;

The `inst` function performs a simultaneous substitution of types for type
variables. The `|->` operator constructs a binding, and a substitution is just
a list of these bindings.

    >> set_trace "types" 0;

Substitution
-------------
The `subst` function performs simultaneous substitution of terms for term variables.
Term substitutions are created using the same `|->` operator as used for type substitutions.
For an example, recall the term we made earlier, `imp`, which contains two free variables.

    >> imp;

    >> val s = [``x:bool`` |-> F, ``y:bool`` |-> ``x = y``];

    >> subst s imp;

Substitution only works on free variables. Recall `tm3`, which has none.

    >> f3;

The same substitution does nothing.

    >> subst s f3;

However, if we add a free occurrence of `y`, it will be substituted.

    >> val f3y = mk_comb(f3,``y:bool``);

    >> subst s f3y;

What happens if we do the same in the body of the abstraction?

    >> val (_,f3b) = dest_abs f3;

    >> subst s f3b;

Now the bound `x` got renamed to `x'`, since a different `x` appears in the body after the substitution.
(In fact, these variables don't even have the same type.)

First-order logic
------------------
To the [Boolean connectives] of propositional logic, first-order logic adds quantifiers.
In particular, there is a universal and an existential quantifier.
Here are some examples.

    >> val q = ``q:bool``;
    >> mk_forall(q,``^q ==> ^q``);

    >> ``!y. ~y ==> x``;

    >> ``?y. x ==> ~y``;

Using the term-building functions directly, one must be careful to ensure all variables have the desired types.

    >> mk_exists(``q``,``q ==> q``);

Here, the quanified variable, `q'`, is not the same as the variable `q` in the body of the existential.
It has a different type, namely `:'a`, whereas `q` must have type `bool`.
This happened because the bound `q'` was parsed in a separate context from that constraining the type of `q` to be `:bool`.

There is shorthand syntax for nesting the same quantifier multiple times, which HOL will print back by default.

    >> ``!x. !y. !z. x = y``;

The corresponding term-manipulation functions are illustrated below.

    >> strip_forall it;

    >> list_mk_exists([x,q],q);

In HOL, the quantifiers are in fact simply higher-order functions.

    >> val tm = ``∀x. ∃y. x = y``;

    >> val (x,ex) = dest_forall tm;

    >> dest_comb it;

`dest_forall` splits the quantifier into the bound variable and the body, but `dest_comb`, used on the second quantifier, reveals that `ex` is an application of `$?` to a lambda term.

    >> type_of ``$!``;

A predicate is a function with codomain `:bool`.
Quantifiers are predicates on predicates.

Theorems
---------
The third (and final) datatype HOL provides on top of ML, after types and terms, is `thm`, the type of proven theorems.
A very simple theorem is bound by default to the ML variable `TRUTH`.

    >> TRUTH;

Every theorem contains a set of hypotheses and a conclusion. All these are terms of type `:bool`.

    >> dest_thm TRUTH;

    >> hypset TRUTH;

    >> concl TRUTH;

`hyp`, like `dest_thm`, returns the hypotheses as a list, which is often less efficient when writing automation, but easier to deal with interactively.

    >> hyp TRUTH;

Hypotheses are not printed by default, but there is a trace to show them.

    >> set_trace "assumptions" 1;

    >> TRUTH;

A key feature of HOL (and all [LCF-style] theorem provers) is that values of type `thm` can only be produced by a small number of trusted functions in a trusted module.
In HOL, the relevant structure is `Thm`, and the functions it exports are available by default.
(See [Finding documentation] for how to inspect the contents of such structures.)
Any other theorem-producing functions must ultimately build their theorems via calls to the trusted functions, thereby ensuring that a proof (in the form of a sequence of calls to kernel functions) exists for every theorem.
There are many theorem-producing functions (sometimes called "derived rules") that build on the ones in `Thm`.

[LCF-style]: https://en.wikipedia.org/wiki/Logic_for_Computable_Functions

A simple kernel function is `ASSUME`, which creates a theorem with an assumption.

    >> val th = ASSUME ``x ≠ y``;

The `DISCH` rule can move an assumption into the conclusion.

    >> DISCH ``x ≠ y`` th;

It does not have to be in the assumptions in the first place.

    >> DISCH ``y ≠ x`` th;

To pull the antecedent of an implication into the assumptions, use `UNDISCH`.

    >> UNDISCH it;

To discharge all assumptions, use `DISCH_ALL`.

    >> DISCH_ALL it;

This is useful to avoid having to write which assumption you want in theorems with only one anyway.

Theories
---------
In the HOL theorem prover, type operators, constants, and stored theorems are organised into _theories_.
Every type operator (such as `list`) is defined in some theory; in the case of `list`, it is `listTheory`.
The fully-qualified name of the type operator is `list$list`.

By convention, a theory `foo` is stored in an ML structure called `fooTheory` which is produced by building `fooScript.sml`.

To find the fully-qualified name of a type operator or constant, the following functions can be used.

    >> dest_thy_type ``:'a list``;

(Since `dest_thy_type` takes a type, a type operator must be applied to arguments first.
These are also returned, as with `dest_type`.)

    >> dest_thy_const T;

    >> dest_thy_type ``:num``;

Every interactive session has a "current theory", which is where any new logical content (constants, theorems/axioms) will be stored.
By default, this will be "scratch".

    >> current_theory();

To start working in a new theory, use `new_theory`.

    >> new_theory "test";

    >> current_theory();

Only one theory can be current at a time, so the call to `new_theory` first exported the theory "scratch".
Generally, `new_theory` should not be used interactively except when editing a [script file][script files]: then, it should appear near the start of the file to avoid adding any content to a `scratchTheory`.
To save the current theory to disk, use `export_theory`; this should generally only happen at the bottom of a script file.

Every theory has a series of _ancestors_, which can be found (in a meaningless order) as follows.

    >> ancestry "-";

The argument to `ancestry` is the name of a theory, with "-" being interpreted as the current theory.
One of the earliest theories is `boolTheory`.

    >> ancestry "bool";

The _theory hierarchy_ is the tree of theories organised by ancestry.
One theory depends on another (and therefore includes the other amongst its ancestors) if it makes use of that theory's types, constants, or theorems.
The root of the hierarchy is `minTheory`, which contains some primitive types and constants.

The contents of a theory can be seen as follows.

    >> types "min";

    >> constants "min";

    >> theorems "min";

    >> axioms "min";

Names in the theory hierarchy must be unique.

    >>+ new_theory "bool";

Finding theorems
-----------------------
The contents of the current theory hierarchy are stored in a database and can be searched.
Stored theorems are stored with a name, and can be searched for by name as follows.

    >> DB.find"skolem";

    >> DB.find"Tru";

The search is case-insensitive.
The output format includes the theory, theorem name, and the theorem itself.
Let us turn off the printing of hypotheses for now.

    >> set_trace "assumptions" 0;

One can also search again within the results.

    >> DB.find_in "add" (DB.find "zero");

The data are printed more nicely by `print_find`, which prints the data list as follows.

~~~~
>>_ val s = Hol_pp.data_list_to_string it;

>>__ val s = Substring.string(Substring.triml 2 (Substring.full s))
>> say s;
~~~~

Theorems can also be searched for by matching on their conclusion.

    >> DB.apropos_in ``_ ++ _ = _`` (DB.apropos ``[x]``);

Underscores are treated specially by the parser; in particular, each underscore is parsed as a variable with a distinct name from the other underscores.
Matching allows substitution of any variable by any term (of the correct type), so the treatment of underscores enables their convenient use as wildcards in terms to be matched.

Evaluation
-----------

Tags
-----
Theorems also contain a set of tags indicating how they were produced. These tags propagate through
uses in inference applications (e.g. if a theorem has a tag, then a theorem derived from the former
will inherit this tag). These tags are especially useful with axioms in case there is a suspicion
the axiom may be unsound (e.g. the axiom is taken for correct while not proven, or the axiom comes from
an "oracle", or the axiom comes from an external prover but without a proof that can be replayed by HOL).

Simple proofs
--------------

Useful tactics
---------------

Finding documentation
----------------------

HOL contains in-built documentation available from the REPL via the `help` function.
The same documentation is also available in HTML format both from `$HOLDIR/help/HOLindex.html` and [online](https://hol-theorem-prover.org/kananaskis-10-helpdocs/help/HOLindex.html).

In some cases, some libraries have not yet provided help documentation, but there is still information available in comments in their signature files.
TODO: Also, how to set up Poly/ML to show the signatures of structures.

Finally, the [HOL website](https://hol-theorem-prover.org/#doc) has information regarding HOL's manuals, which can also be found under `$HOLDIR/Manual` in your local installation.

System conventions
-------------------
TODO: When HOL is built, links to all the theories and libraries are created under `$HOLDIR/sigobj`. This can be a useful resource for finding out where the sources corresponding to a particular structure are kept.

Standard theories
------------------

Defining constants
------------------

Overloading
------------

To parse a fully-qualified name, use a `$` symbol.

    >> ``bool$T``;

This is useful when the bare constant name (i.e., `T` in this case) is overloaded and might refer to more than one constant.
The constant `0` often falls into this category, since it is overloaded at different numeric types.

    >> dest_thy_const ``0``;


Defining datatypes
------------------

Induction
----------

Conversions
------------

The simplifier
---------------

Defining relations
-------------------

The type database
------------------

Defining quotients
-------------------

Changing the parser
--------------------

Writing more tactics
--------------------

More proofs
------------

Modern syntax
-------------

We summarise the additions of new surface syntax that entered in recent versions of HOL4, which reduces code-smells and is closer to syntax of other theorem provers.

#### Theorem

We have implemented new syntaxes for `store_thm` and `save_thm`, which better satisfy the recommendation that `name1` and `name2` below should be the same:

```
val name1 = store_thm("name2", tm, tac);
```

Now we can remove the "code smell" by writing

```
Theorem name: term-syntax
Proof tac
QED
```

which might look like

```
Theorem name:
  ∀x. P x ⇒ Q x
Proof
  rpt strip_tac >> ...
QED
```

This latter form must have the `Proof` and `QED` keywords in column 0 in order for the lexing machinery to detect the end of the term and tactic respectively.
Both forms map to applications of `Q.store_thm` underneath, with an ML binding also made to the appropriate name.
Both forms allow for theorem attributes to be associated with the name, so that one can write

```
Theorem ADD0[simp]: ∀x. x + 0 = x
Proof tactic
QED
```

Finally, to replace

```
val nm = save_thm(“nm”, thm_expr);
```

one can now write

```
Theorem nm = thm_expr
```

These names can also be given attributes in the same way.

There is also a new `local` attribute available for use with `store_thm`, `save_thm` and the `Theorem` syntax above.
This attribute causes a theorem to not be exported when `export_theory` is called, making it local-only.
Use of `Theorem`-`local` is thus an alternative to using `prove` or `Q.prove`.
In addition, the `Theorem`-`local` combination can be abbreviated with `Triviality`; one can write `Triviality foo[...]` instead of `Theorem foo[local,...]`.

#### Definition

Relatedly, there is a similar syntax for making definitions.
The idiom is to write

```
Definition name[attrs]:
  def
End
```

Or

```
Definition name[attrs]:
  def
Termination
  tactic
End
```

The latter form maps to a call to `tDefine`; the former to `xDefine`.
In both cases, the `name` is taken to be the name of the theorem stored to disk (it does *not* have a suffix such as `_def` appended to it), and is also the name of the local SML binding.
The attributes given by `attrs` can be any standard attribute (such as `simp`), and/or drawn from `Definition`-specific options:

- the attribute `schematic` alllows the definition to be schematic;
- the attribute `nocompute` stops the definition from being added to the global compset used by `EVAL`
- the attribute `induction=iname` makes the induction theorem that is automatically derived for definitions with interesting termination be called `iname`.
  If this is omitted, the name chosen will be derived from the `name` of the definition: if `name` ends with `_def` or `_DEF`, the induction name will replace this suffix with `_ind` or `_IND` respectively; otherwise the induction name will simply be `name` with `_ind` appended.

Whether or not the `induction=` attribute is used, the induction theorem is also made available as an SML binding under the appropriate name.
This means that one does not need to follow one's definition with a call to something like `DB.fetch` or `theorem` just to make the induction theorem available at the SML level.

#### Inductive and CoInductive

Similarly, there are analogous `Inductive` and `CoInductive` syntaxes for defining inductive and coinductive relations (using `Hol_reln` and `Hol_coreln` underneath).
The syntax is

```
Inductive stem:
  quoted term material
End
```

or

```
CoInductive stem:
  quoted term material
End
```

where, as above, the `Inductive`, `CoInductive` and `End` keywords must be in the leftmost column of the script file.
The `stem` part of the syntax drives the selection of the various theorem names (*e.g.*, `stem_rules`, `stem_ind`, `stem_cases` and `stem_strongind` for inductive definitions) for both the SML environment and the exported theory.
The actual names of new constants in the quoted term material do not affect these bindings.

Each (co)inductive rule can be exported under a theorem name provided in square-bracket syntax `[~name:]`, where `~` is a place-holder for the relation.
For example

```
Inductive RTC:
[~refl:]
  (!x. RTC R x x) /\
[~induct:]
  !x y z. R x y /\ RTC R y z ==> RTC R x z
End
```

additionally exports the theorems `RTC_refl` and `RTC_induct`.


#### Datatype

There are new syntaxes for `Datatype` and type-abbreviation.
Users can replace `` val _ = Datatype`...`  `` with

```
Datatype: ...
End
```

and `val _ = type_abbrev("name", ty)` with

```
Type name = ty
```

if the abbreviation should introduce pretty-printing (which would be done with `type_abbrev_pp`), the syntax is

```
Type name[pp] = ty
```

Note that in both `Type` forms the `ty` is a correct ML value, and may thus require quoting.
For example, the `set` abbreviation is established with

```
Type set = “:α -> bool”
```

The special `Type` syntax for making type abbreviations can now map to
`temp_type_abbrev` (or `temp_type_abbrev_pp`) by adding the `local`
attribute to the name of the abbreviation.

For example

```
Type foo[local] = “:num -> bool # num”
```

or

```
Type foo[local,pp] = “:num -> bool # num”
```

#### Overload

We have added a special syntactic form `Overload` to replace various flavours of `overload_on` calls. The core syntax is exemplified by

```
Overload foo = “myterm”
```

Attributes can be added after the name.
Possible attributes are `local` (for overloads that won't be exported) and `inferior` to cause a call `inferior_overload_on` (which makes the overload the pretty-printer's last choice).