File: system.tex

package info (click to toggle)
hol88 2.02.19940316dfsg-5
links: PTS
area: main
in suites: bookworm
size: 65,816 kB
sloc: ml: 199,939; ansic: 9,666; sh: 6,913; makefile: 6,032; lisp: 2,747; yacc: 894; sed: 201; cpp: 87; awk: 5
file content (5951 lines) | stat: -rw-r--r-- 256,210 bytes
parent folder | download | duplicates (11)
\chapter{The HOL Logic in ML}\label{HOLsyschapter}

In this chapter, the concrete representation of the \HOL\ logic is described.
This involves describing the \ML\ functions that comprise the interface to the
logic (up to and including Section~\ref{avra_terms}); the quotation, printing
and parsing of logical terms (Section~\ref{quotation}); the representation of
theorems (Section~\ref{avra_theorems}); the representation of theories
(Section~\ref{theoryfns}); the basic \HOL\ theories that are built into the
\HOL\ system (Sections~\ref{HOL-theory} and \ref{rules}); the methods for
extending theories (throughout Section~\ref{HOL-ancestry} and in
Section~\ref{types-package}); and the \ML\ system functions concerning the
logic (Section~\ref{HOLflags}).  It is assumed that the reader is familiar
with \ML.  If  not, the introduction to \ML\ in {\sl Getting  Started with
HOL\/} in \TUTORIAL\ should be read first. 

The \HOL\ system provides \ML\ types \ml{type} and \ml{term} to represent
types and terms of the \HOL\ logic, as defined in Sections~\ref{types} and
\ref{terms}, respectively.\footnote{Care must be taken to avoid confusion
between ML types and types of the HOL logic: the ML type {\tt type} represents
types of the HOL logic in ML.} It also provides primitive \ML\ functions for
creating and manipulating values of these types.  The key idea of the \HOL\
system, due to Robin Milner\index{Milner, R.}, and discussed in this chapter,
is that theorems are represented as an abstract \ML\ type whose only
pre-defined values are axioms, and whose only operations are rules of
inference. This means that the only way to construct theorems in \HOL\ is
to apply rules of inference to axioms or existing theorems; hence the
consistency of the logic is preserved.

The purpose of the meta-language \ML\ is to provide a programming environment
in which to build theorem proving tools to assist in the construction of
proofs.  When the \HOL\ system is built, a range of useful theorems are
pre-proved and a set of tools pre-defined. The basic system thus offers a rich
initial environment; users can further enrich it by implementing their own
application specific tools and building their own application specific
theories.


\section{Lexical matters}
\label{HOL-lex}

\index{identifiers, in HOL logic@identifiers, in \HOL\ logic|(}
The name of a \HOL\  variable\index{variables, in HOL logic@variables, in \HOL\ logic!names of|(} 
can be any  \ML\ string, but the quotation
mechanism will parse  only names that are  
identifiers (see Section~\ref{ident} below).  
The use of non-identifiers as  variable names  is discouraged except
in special  circumstances  (for example, when  writing  
derived   rules  that  generate
variables with names that are guaranteed to be different from existing names).
The names of type 
variables\index{type variables, in HOL logic@type variables, in \HOL\ logic!names of} in the \HOL\ logic are strings
of \ml{*}s optionally followed by a number or an identifier (see
Section~\ref{tyvars} for examples).
The name of a type constant or a term constant of the \HOL\ logic can
be any identifier.  \ML\ identifiers are described in Part~\ref{MLpart}; the 
lexical structure of \HOL\ identifiers is identical, however the
description is repeated here for convenience. 
\index{identifiers, in HOL logic@identifiers, in \HOL\ logic|)}

\subsection{Identifiers}
\label{ident}

The structure of \HOL\ identifiers is partly programmable. The default
is that an identifier can be of two forms:
\begin{myenumerate}
\item A sequence of alphanumerics starting with a letter, 
where the default structure of an alphanumeric is that it is a letter, 
a digit, a prime (\ml{'}) or an underbar (\ty{\_}).
\item A special symbol chosen from the following list

{\small \begin{verbatim}
   **     ++     <--    <->    -->    ---    ><     >>

   >=     <==    <=>    ===    ==>    \/     //     /\

   !?     !!     !\     ?!     ??     ?\     :=     <>

   <-     <<     <=     --     ->     =>     ==
\end{verbatim}}

\end{myenumerate}

\noindent A letter is a member of the list:


\begin{hol}\begin{verbatim}
   a b c d e f g h i j k l m n o p q r s t u v w x y z

   A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
\end{verbatim}\end{hol}

\noindent \HOL\ is case-sensitive: upper and lower case letters are 
considered to be different. 

The function

\begin{boxed}\index{new_letter@\ml{new\_letter}|pin}
\begin{verbatim}
   new_letter : string -> void
\end{verbatim}\end{boxed}

\noindent makes a new character behave like a letter. For example:

\begin{hol}\begin{verbatim}
   new_letter `+`;;
\end{verbatim}\end{hol}

\noindent will make \ml{+int} and \ml{foo+bar} become allowable identifiers.
Failure occurs if the argument string is longer than one character.

The function

\begin{boxed}\index{is_letter@\ml{is\_letter}|pin}
\begin{verbatim}
   is_letter : string -> bool
\end{verbatim}\end{boxed}

\noindent tests if a unit string is a letter; it fails if the string has more
than one character.

Alphanumerics are, by default, letters or digits.  A digit is one of
{\small\verb%0%}, {\small\verb%1%}, {\small\verb%2%}, {\small\verb%3%},
{\small\verb%4%}, {\small\verb%5%}, {\small\verb%6%}, {\small\verb%7%},
{\small\verb%8%}, or {\small\verb%9%}. 
A {\it number\/} is a string of one or more digits.
The function

\begin{boxed}\index{new_alphanum@\ml{new\_alphanum}|pin}
\begin{verbatim}
   new_alphanum : string -> void
\end{verbatim}\end{boxed}
   
\noindent makes a new character behave like an alphanumeric. For example:

\begin{hol}\begin{verbatim}
   new_alphanum `+`;;
\end{verbatim}\end{hol}

\noindent will make \ml{foo+bar} and \ml{foo+} become allowable names (but not
\ml{+bar}). Failure occurs if the argument string is longer than one
character.

The function

\begin{boxed}\index{is_alphanum@\ml{is\_alphanum}|pin}
\begin{verbatim}
   is_alphanum : string -> bool
\end{verbatim}\end{boxed}

\noindent tests if a unit string is an alphanumeric; it fails if the string
has more than one character.

It is a consequence of the way lexical analysis is implemented that any
initial subsequence of a special symbol is also a special symbol (e.g. since
\ml{==>} is a special symbol, so are \ml{==} and \ml{=}). The function

\begin{boxed}\index{new_special_symbol@\ml{new\_special\_symbol}|pin}
\begin{verbatim}
   new_special_symbol : string -> bool
\end{verbatim}\end{boxed}
  
\noindent makes the argument string, and all its substrings, special symbols;
it fails if 
\begin{myenumerate}
\item the argument string is a single character, or 
\item it starts with a letter or an alphanumeric. 
\end{myenumerate}

\noindent For example:

\begin{hol}\begin{verbatim}
   new_special_symbol `===>>>`;;
\end{verbatim}\end{hol}

\noindent makes \ml{===>>>}, \ml{===>>}, \ml{===>} and \ml{===} 
into new special symbols 
(\ml{==} is already a special symbol because \ml{==>} is).

The function

\begin{boxed}\index{special_symbols@\ml{special\_symbols}|pin}
\begin{verbatim}
   special_symbols : void -> string list
\end{verbatim}\end{boxed}

\noindent  gives the list of currently declared special symbols\index{variables, in HOL logic@variables, in \HOL\ logic!names of|)} .


\subsubsection{Separators}

The separators used by the \HOL\ lexical analyser are (with ascii codes in
brackets):

\bigskip

space (32), carriage return (13), line feed (10), tab ({\verb%^%}I, 9), 
form feed ({\verb%^%}L, 12)



\subsection{Type variable names}
\label{tyvars}

The names of type variables in the \HOL\ logic are strings
of \ml{*}s optionally followed by a number or by an identifier; for example:

\begin{hol}\begin{verbatim}
   *   **   ***   *'   **'   **25   ***thing
\end{verbatim}\end{hol}


\section{Types}\index{types, in HOL logic@types, in \HOL\ logic}

The allowed types\index{type constraint!in HOL logic@in \HOL\ logic} depend on which type constants\index{type constants, in HOL logic@type constants, in \HOL\ logic} have been declared in the
current theory. See Section~\ref{theoryfns} for details of how such
declarations are made.


There are two primitive constructor\index{types, in HOL logic@types, in \HOL\ logic!constructors for}
\index{type constructors!in HOL logic@in \HOL\ logic} functions for values of type
\ml{type}:


\begin{boxed}
\index{function types, in HOL logic@function types, in \HOL\ logic!constructors for}\index{mk_vartype@\ml{mk\_vartype}|pin}
\index{mk_type@\ml{mk\_type}|pin}
\begin{verbatim}
   mk_vartype : string -> type
   mk_type    : (string # type list) -> type
\end{verbatim}\end{boxed}

The function \ml{mk\_vartype}
 constructs a type variable\index{type variables, in HOL logic@type variables, in \HOL\ logic!constructor for} with a given name;
it fails if the name is not an allowable type variable name (\ie\ not
a string of \ml{*}s followed by a number or identifier).  

The function \ml{mk\_type} constructs a compound type\index{compound types, in HOL logic@compound types, in \HOL\ logic!constructors for}
 from a string
representing the name of the type operator and a list of types representing the
arguments to   the  operator.     Function   types  $\sigma_1\fun\sigma_2$  
of the logic are
represented in \ML\ as though they were compound types
$(\sigma_1,\sigma_2)$\ml{fun} (in  Section~\ref{types}, however,
function types were not regarded as compound types).

The evaluation of 
\ml{mk\_type(`}$name$\ml{`,\ [}$\sigma_1$\ml{;}$\cdots$\ml{;}$\sigma_n$\ml{])}
fails if
\begin{myenumerate}
\item $name$ is not an identifier;
\item $name$ is not a type operator of the current theory;
\item $name$ is a type operator of the current theory, 
but its arity is not $n$.
\end{myenumerate}

For example, \ml{mk\_type(`bool`,[])}\index{truth values, in HOL logic@truth values, in \HOL\ logic}\index{bool, the type in HOL logic@\ml{bool}, the type in \HOL\ logic} evaluates to
an \ML\ value of type term representing the type \ty{bool} and
{\small\verb%mk_type(`fun`, [mk_type(`ind`,[]); mk_type(`bool`,[])])%}
evaluates to a value representing $\ty{ind}\fun\ty{bool}$.
(These types are introduced in Section~\ref{boolthy}).

There are two primitive destructor\index{types, in HOL logic@types, in
\HOL\ logic!destructors for}\index{type destructors, in HOL logic@type destructors, in \HOL\ logic}
 functions for values of type
\ml{type}:


\begin{boxed}
\index{function types, in HOL logic@function types, in \HOL\ logic!destructors for}
\index{dest_vartype@\ml{dest\_vartype}|pin}
\index{dest_type@\ml{dest\_type}|pin}
\begin{verbatim}
   dest_vartype : type -> string
   dest_type    : type -> (string # type list)
\end{verbatim}\end{boxed}

\noindent The function \ml{dest\_vartype}\index{type variables, in HOL logic@type variables, in \HOL\ logic!destructors for}\index{compound types, in HOL logic@compound types, in \HOL\ logic!destructors for}
 extracts the name of a type variable.
The function \ml{dest\_type}  destructs a  compound type  into the  name of the
type operator  and  a  list  of  the  argument  types;  \ml{dest\_vartype}  and
\ml{dest\_type} are  thus the  inverses of  \ml{mk\_vartype} and \ml{mk\_type},
respectively.  The destructors fail on arguments of the wrong form.


Types are printed\index{ type constraint, in HOL logic@\ml{:} (type constraint, in \HOL\ logic)}
\index{printing, in HOL logic@printing, in \HOL\ logic!of types} in the form \ml{":}$\ \cdots\ $\ml{"}
using the quotation syntax described in Section~\ref{quotation}.
For example, the \ML\ value of type \ml{type} representing
$\ty{ind}\fun(\ty{ind}\fun\ty{bool})$ would be printed
as \ml{":ind -> ind -> bool"}.

\section{Terms}
\label{avra_terms}

The four primitive kinds of  terms of the logic
are  described in  Section~\ref{terms}.  The
\ML\ functions for manipulating these are described in this section.  There are
also various derived terms that are described in Section~\ref{derived-terms}.

The allowed terms depend on which constants have been declared
in the current theory. See Section~\ref{theoryfns} for details
of how such declarations are made. 

There are four primitive constructor\index{variables, in HOL logic@variables, in \HOL\ logic!constructor for}\index{terms, in HOL logic@terms, in \HOL\ logic!constructors for}\index{term constructors, in HOL logic@term constructors, in \HOL\ logic}
functions for values of type
\ml{term}:

\begin{boxed}
\index{mk_var@\ml{mk\_var}|pin}
\begin{verbatim}
   mk_var : (string # type) -> term
\end{verbatim}\end{boxed}

\noindent\ml{mk\_var(}$x$\ml{,}$\sigma$\ml{)} evaluates to a variable with name
$x$ and type $\sigma$; it always succeeds.

\begin{boxed}
\index{mk_const@\ml{mk\_const}|pin}
\begin{verbatim}
   mk_const : (string # type) -> term
\end{verbatim}\end{boxed}


\noindent\ml{mk\_const(}$c$\ml{,}$\sigma$\ml{)} evaluates to a 
term representing
the constant\index{constants, in HOL logic@constants, in \HOL\ logic!constructor for} with name $c$ and type $\sigma$; it fails if:
\begin{myenumerate}
\item $c$ is not an allowable constant name;
\item $c$ is not the name of a constant in the current theory;
\item $\sigma$ is not an instance of the generic type of $c$
(the generic type of a constant is established when the constant is defined;
see Section~\ref{theoryfns}).
\end{myenumerate}

\begin{boxed}\index{mk_comb@\ml{mk\_comb}|pin}
\begin{verbatim}
   mk_comb : (term # term) -> term
\end{verbatim}\end{boxed}

\noindent\ml{mk\_comb(}$t_1$\ml{,}$t_2$\ml{)}\index{function application, in HOL logic@function application, in \HOL\ logic!constructor for} evaluates to a term 
representing the combination\index{combinations, in HOL logic@combinations, in \HOL\ logic!constructor for}
$t_1\ t_2$. It fails if:
\begin{myenumerate}
\item the type of $t_1$ does not have the form \ml{$\sigma'$->$\sigma$};
\item the type of $t_1$ has the form \ml{$\sigma'$->$\sigma$}, but the
type of $t_2$ is not equal to $\sigma'$.
\end{myenumerate}

\begin{boxed}
\index{mk_abs@\ml{mk\_abs}|pin}
\begin{verbatim}
   mk_abs : (term # term) -> term
\end{verbatim}\end{boxed}

\noindent\ml{mk\_abs(}$x$\ml{,}$t$\ml{)} evaluates to a term representing
the abstraction\index{function abstraction, in HOL logic@function abstraction, in \HOL\ logic!constructor for} $\lquant{x}t$; it fails if $x$ is not a variable.


There are four primitive destructor\index{term destructors, in HOL logic@term destructors, in \HOL\ logic}\index{variables, in HOL logic@variables, in \HOL\ logic!destructor for}\index{constants, in HOL logic@constants, in \HOL\ logic!destructor for}\index{combinations, in HOL logic@combinations, in \HOL\ logic!destructor for}\index{function abstraction, in HOL logic@function abstraction, in \HOL\ logic!destructor for}\index{function application, in HOL logic@function application, in \HOL\ logic!destructor for} functions on terms:

\begin{boxed}

\index{dest_var@\ml{dest\_var}|pin
}\index{dest_const@\ml{dest\_const}|pin}
\index{dest_comb@\ml{dest\_comb}|pin}
\index{dest_abs@\ml{dest\_abs}|pin}
\begin{verbatim}
   dest_var   : term -> (string # type)
   dest_const : term -> (string # type)
   dest_comb  : term -> (term # term)
   dest_abs   : term -> (term # term)
\end{verbatim}\end{boxed}

These are the inverses of \ml{mk\_var}, \ml{mk\_const},
\ml{mk\_comb} and \ml{mk\_abs}, respectively. They fail when applied
to terms of the wrong form. Other useful destructor functions are
\ml{rator}\index{rator@\ml{rator}},
\ml{rand}\index{rand@\ml{rand}},
\ml{bndvar}\index{bndvar@\ml{bndvar}},
\ml{body}\index{body@\ml{body}},
\ml{lhs}\index{lhs@\ml{lhs}} and
\ml{rhs}\index{rhs@\ml{rhs}}.
See \REFERENCE\ for details.

The function

\begin{boxed}\index{type_of@\ml{type\_of}|pin}
\begin{verbatim}
   type_of : term -> type
\end{verbatim}\end{boxed}

\noindent returns the type\index{types, in HOL logic@types, in \HOL\ logic!determination of} of a term. It could be defined (recursively)
in terms of the
destructors but is predefined for convenience.

Terms are printed in the form \ml{"}$\ \cdots\ $\ml{"}
using the quotation syntax\index{quotation, in HOL logic@quotation, in \HOL\ logic} described in Section~\ref{quotation}.
For example, the term representing 

\[ \uquant{x\ y}x<y \imp\equant{z}x+z = y \]

\noindent would be printed as:

\[ \ml{"!x y. x < y ==> ?z. x + z = y"} \]

Note that a colon\index{ type constraint, in HOL logic@\ml{:} (type constraint, in \HOL\ logic)}
 is used to distinguish type quotation from term quotation;
the former have the form \ml{":}$\ \cdots\ $\ml{"} and the latter have
 the form \ml{"}$\ \cdots\ $\ml{"}.


\section{Quotation}
\label{quotation}\label{gen-abs}\label{let}
\index{type checking, in HOL logic@type checking, in \HOL\ logic!of quotation syntax|(}

\index{quotation, in HOL logic@quotation, in \HOL\ logic|(}
\index{ type quotes, in ML@\ml{"":$\cdots$""} (type quotes, in \ML)|(}
\index{ term quotes, in ML@\ml{""$\cdots$""} (term quotes, in \ML)|(}
\HOL\ types and terms can be input\index{terms, in HOL logic@terms, in \HOL\ logic!input of} to the system in two ways:  by using
constructor functions, or by using {\it quotation\/}.  The 
former 
allows some terms to be built which cannot be  constructed using quotation.
For example, a term containing two variables with  the same  name but different
types, \eg\ the term  $x_{\ty{bool}}=(x_{\ty{num}}=1)$, 
 can be built only by using
constructors.

It would be tedious, however, to always have to input types and terms using the
constructor functions. The \HOL\ system, following \LCF\index{LCF@\LCF}, has a special 
quotation\index{quotation, in HOL logic@quotation, in \HOL\ logic!parser for}\index{parsing, of HOL logic@parsing, of \HOL\ logic!of quotation syntax} parser and
type checker that enables terms to be input using a fairly standard syntax.  The
\HOL\ printer also outputs types and terms using this syntax\index{printing, in HOL logic@printing, in \HOL\ logic!of quotation syntax}.

For example, the \ML\ expression {\small\verb%":bool->bool"%} denotes
exactly the same value (of \ML\ type {\small\verb%type%}) as

\begin{hol}\index{bool, the type in HOL logic@\ml{bool}, the type in \HOL\ logic}
\begin{verbatim}
   mk_type(`fun`,[mk_type(`bool`,[]);mk_type(`bool`,[])])
\end{verbatim}\end{hol}

\noindent and
{\small\verb%"\x.x+1"%}\index{function abstraction, in HOL logic@function abstraction, in \HOL\ logic} can be used instead of

\newpage %PBHACK

{\small\baselineskip\HOLSpacing\begin{verbatim}

   mk_abs
    (mk_var(`x`,mk_type(`num`,[])),
     mk_comb
     (mk_comb
      (mk_const
       (`+`,
        mk_type(`fun`,[mk_type(`num`,[]);
                       mk_type(`fun`,[mk_type(`num`,[]);
                                      mk_type(`num`,[])])])),
       mk_var(`x`, mk_type(`num`,[]))),
      mk_const(`1`, mk_type(`num`,[]))))
\end{verbatim}}

\index{type constraint!in HOL logic@in \HOL\ logic|(}It should be noted 
that there is no  explicit type  information in {\small\verb%"\x.x+1"%}.
The \HOL\ type checker knows that \ml{1} has type \ml{num} and  \ml{+} has type
\ml{num->(num->num)}.  From this information it can infer that both occurrences
of {\small\verb%x%} in {\small\verb%"\x.x+1"%} could have type
{\small\verb%num%}.  This  is  not  the  only  possible type  assignment;  for
example, the first occurrence of {\small\verb%x%} could have type \ml{bool} and
the second one have type {\small\verb%num%}.  In that  case there  would be two
{\it different\/} variables with name {\small\verb%x%}, namely
{\small\verb%x%}$_{\tt bool}$ and  {\small\verb%x%}$_{\tt num}$,  the second of
which is free.  In fact, as mentioned, 
the only  way to  construct a  term with this
second type assignment is  by using  constructors, since  the type checker uses
the heuristic that all variables in a term
 with the same name  have the  same type.   This is
illustrated in the following session.

\setcounter{sessioncount}{1}
\begin{session}\begin{verbatim}
#"x = (x = 1)";;
Badly typed application of:  "$= x"
   which has type:           ":num -> bool"
to the argument term:        "x = 1"
   which has type:           ":bool"

evaluation failed     mk_comb in quotation

#mk_eq
# (mk_var(`x`,mk_type(`bool`,[])), 
#  mk_eq
#   (mk_var(`x`,mk_type(`num`,[])),
#    mk_const(`1`,mk_type(`num`,[]))));;
"x = (x = 1)" : term
\end{verbatim}\end{session}

The quotation type checker was designed  and implemented  by Robin  Milner\index{Milner, R.}.  It
employs heuristics  like  the  one  above  to  infer  a  sensible  type for all
variables occurring in a term.  If there are not enough clues,  then the system
will complain with an error message.

To give the system a hint, types can be  explicitly indicated  by following any
subterm with a colon and then a type.  For example,
{\small\verb%"f(x:num):bool"%} will   type check   with   {\small\verb%f%}   and
{\small\verb%x%} getting types  {\small\verb%num->bool%} and {\small\verb%num%}
respectively.  If  there  are polymorphic  constants in  a term,  there must be
enough type  information  to uniquely  identify a  type instance  for each such
constant.  There is  also a  feature called  {\it sticky  types\/} that enables
variables to be given default types; this is described in
Section~\ref{stickytypes}.

The type checking\index{type checker, for HOL logic vs ML@type checker, for \HOL\ logic {\it vs} \ML} algorithm used for the \HOL\ logic differs from that used
for \ML. For example, the \ML\ expression {\small\verb%\x.x%}\index{terms, in HOL logic@terms, in \HOL\ logic!function abstraction}\index{function abstraction, in HOL logic@function abstraction, in \HOL\ logic!type checking of}\index{function abstraction, in HOL logic@function abstraction, in \HOL\ logic!syntax of}
 will get \ML\
type {\small\verb%*->*%}, but the \HOL\ term {\small\verb%"\x.x"%} will
fail to type check, as shown in the session below.

\setcounter{sessioncount}{1}
\begin{session}\begin{verbatim}
#"\x. x";;
Indeterminate types:  "x:?"

evaluation failed     types indeterminate in quotation
\end{verbatim}\end{session}

\noindent To get the term {\small\verb%\x.x%} 
to type check, the type of the variable \ml{x} must be  given explicitly, 
for example by writing {\small\verb%"\x:*.x"%}. 

\begin{session}\begin{verbatim}
#"\x:*. x";;
"\x. x" : term
\end{verbatim}\end{session}

\noindent This treatment of types within quotations is inherited from \LCF\index{LCF@\LCF}.
\index{type constraint!in HOL logic@in \HOL\ logic|)}
\index{ term quotes, in ML@\ml{""$\cdots$""} (term quotes, in \ML)|)}

\subsection{Type quotation}

\index{type variables, in HOL logic@type variables, in \HOL\ logic!constructor for}
\index{type constructors!in HOL logic@in \HOL\ logic}
\index{term constructors, in HOL logic@term constructors, in \HOL\ logic|(}
\index{terms, in HOL logic@terms, in \HOL\ logic!constructors for|(}
The table below shows \ML\ expressions for various kinds of type
quotations\index{quotation, in HOL logic@quotation, in \HOL\ logic!of types}.
The expressions in the same row are equivalent.

\bigskip


\begin{center}
\index{compound types, in HOL logic@compound types, in \HOL\ logic!constructors for}
\index{ type variables, in HOL logic@\ml{*,\,**,\,}$\ldots$ (type variables, in \HOL\ logic)}
\index{types, in HOL logic@types, in \HOL\ logic!constructors for}
\index{ function type operator, in HOL logic@\ml{->} (function type operator, in \HOL\ logic)}
\index{mk_vartype@\ml{mk\_vartype}}
\index{mk_type@\ml{mk\_type}}
\begin{tabular}{|l|l|l|} \hline
\multicolumn{3}{|c|}{ } \\
\multicolumn{3}{|c|}{\bf Types} \\
\multicolumn{3}{|c|}{ } \\
{\it Kind of type} & {\it \ML\ quotation} & 
{\it Constructor expression}  \\ \hline
 & & \\
Type variable &
{\small\verb%":*%}$\cdots${\small\verb%"%} & {\small\verb%mk_vartype(`*%}$\cdots${\small\verb%`)%}   \\ \hline
Type constant &
{\small\verb%":%}$op${\small\verb%"%} & {\small\verb%mk_type(`%}$op${\small\verb%`,[])%}   \\ \hline
Function type &
{\small\verb%":%}$\sigma_1${\small\verb%->%}$\sigma_2${\small\verb%"%} &
{\small\verb%mk_type(`fun`, [":%}$\sigma_1${\small\verb%";":%}$\sigma_2${\small\verb%"])%} \\ \hline
Compound type &
{\small\verb%":(%}$\sigma_1${\small\verb%,%} $\ldots$ {\small\verb%,%} $\sigma_n${\small\verb%)%}$op${\small\verb%"%} &
{\small\verb%mk_type(`%}$op${\small\verb%`, [":%}$\sigma_1${\small\verb%";%} $\ldots$ {\small\verb%;":%}$\sigma_n${\small\verb%"])%}
\\ \hline
\end{tabular}
\end{center}

\index{ type quotes, in ML@\ml{"":$\cdots$""} (type quotes, in \ML)|)}

\subsection{Term quotation}

\index{terms, in HOL logic@terms, in \HOL\ logic!syntax of|(}
Equivalent ways of inputting the four primitive kinds of term are shown in
the next table.

\bigskip

\begin{center}
\index{combinations, in HOL logic@combinations, in \HOL\ logic!quotation of}
\index{terms, in HOL logic@terms, in \HOL\ logic!primitive}
\index{terms, in HOL logic@terms, in \HOL\ logic!constructors for}
\index{quotation, in HOL logic@quotation, in \HOL\ logic!of primitive terms}
\index{function abstraction, in HOL logic@function abstraction, in \HOL\ logic!symbol for}
\index{function application, in HOL logic@function application, in \HOL\ logic!constructor for}
\index{function application, in HOL logic@function application, in \HOL\ logic!syntax of}
\index{variables, in HOL logic@variables, in \HOL\ logic!constructor for}
\index{variables, in HOL logic@variables, in \HOL\ logic!syntax of} 
\index{mk_var@\ml{mk\_var}}
\index{mk_const@\ml{mk\_const}}
\index{mk_comb@\ml{mk\_comb}}
\index{mk_abs@\ml{mk\_abs}}
\begin{tabular}{|l|l|l|} \hline
\multicolumn{3}{|c|}{ } \\
\multicolumn{3}{|c|}{\bf Primitive terms} \\
\multicolumn{3}{|c|}{ } \\
{\it Kind of term} & {\it \ML\ quotation} & 
{\it Constructor expression}  \\ \hline
 & & \\
Variable & {\small\verb%"%}$var${\small\verb%:%}$\sigma${\small\verb%"%} &
{\small\verb%mk_var(`%}$var${\small\verb%`,":%}$\sigma${\small\verb%")%} \\ \hline
Constant & {\small\verb%"%}$const${\small\verb%:%}$\sigma${\small\verb%"%} &
{\small\verb%mk_const(`%}$const${\small\verb%`,":%}$\sigma${\small\verb%")%} \\ \hline
Combination & {\small\verb%"%}$t_1\ t_2${\small\verb%"%} &
{\small\verb%mk_comb("%}$t_1${\small\verb%","%}$t_2${\small\verb%")%} \\ \hline
Abstraction & {\small\verb%"\%}$x${\small\verb%.%}$t${\small\verb%"%} &
{\small\verb%mk_abs("%}$x${\small\verb%","%}$t${\small\verb%")%} \\ \hline
\end{tabular}
\end{center}\index{type checking, in HOL logic@type checking, in \HOL\ logic!of quotation syntax|)}

\subsection{Special syntactic forms}
\label{derived-terms}

\index{type checking, in HOL logic@type checking, in \HOL\ logic!special forms in|(}
\index{quotation, in HOL logic@quotation, in \HOL\ logic!of non-primitive terms|(}
The \HOL\ quotation parser\index{quotation, in HOL logic@quotation, in \HOL\ logic!parser for} can translate
various standard logical
notations\index{parsing, of HOL logic@parsing, of \HOL\ logic!of standard notations} into primitive terms. For example, if {\small\verb%+%} has been
declared an infix\index{infixes, in HOL logic@infixes, in \HOL\ logic} (as explained in Section~\ref{theoryfns}), then
{\small\verb%"x+1"%} is translated to {\small\verb%"$+ x 1"%}. The escape
character {\small\verb%$%}\index{ escape, in HOL logic parser@{\small\verb+$+} (escape, in \HOL\ logic parser)}\index{declared constants, in HOL logic@declared constants, in \HOL\ logic}\index{infixes, in HOL logic@infixes, in \HOL\ logic}
 suppresses the infix behaviour of
{\small\verb%+%} and prevents the quotation parser getting confused.  In
general, {\small\verb%$%} can be used to suppress any special syntactic
behaviour a constant name\index{constants, in HOL logic@constants, in \HOL\ logic!supressing parsing behaviour of} might have. This is illustrated in the table
below, in which the terms in the column headed `{\it \ML\ quotation}' are
translated by the quotation parser to the corresponding terms in the column
headed `{\it Primitive term\/}'. Conversely, the terms in the latter
column are always printed in the form shown in the former one.
\label{cond}The \ML\ constructor expressions in the rightmost column
evaluate to the same values (of type {\small\verb%term%}) as the other
quotations in the same row.

\bigskip

\begin{center}
\index{choice operator, in HOL logic@choice operator, in \HOL\ logic!syntax of}
\index{ negation, in HOL logic@{\small\verb+~+} (negation, in \HOL\ logic)}
\index{ disjunction, in HOL logic@{\small\verb+\/+} (disjunction, in \HOL\ logic)}
\index{ conjunction, in HOL logic@{\small\verb+/\+} (conjunction, in \HOL\ logic)}
\index{ implication, in HOL logic@{\small\verb+==>+} (implication, in \HOL\ logic)}
\index{ equality, in HOL logic@\ml{=} (equality, in \HOL\ logic)}
\index{ universal quantifier, in HOL logic@{\small\verb+"!+} (universal quantifier, in \HOL\ logic)}
\index{ existential quantifier, in HOL logic@{\small\verb+?+} (existential quantifier, in \HOL\ logic)}
\index{ choice function, in HOL logic@{\small\verb+"@+} (choice function, in \HOL\ logic)}
\index{terms, in HOL logic@terms, in \HOL\ logic!non-primitive}
\index{terms, in HOL logic@terms, in \HOL\ logic!constructors for}
\index{conditional predicate, in HOL logic@conditional predicate, in \HOL\ logic}
\index{conditionals, in HOL logic@conditionals, in \HOL\ logic}
\index{conjunction, in HOL logic@conjunction, in \HOL\ logic!constructor for}
\index{disjunction, in HOL logic@disjunction, in \HOL\ logic!constructor for}
\index{equality, in HOL logic@equality, in \HOL\ logic!syntax of}
\index{negation, in HOL logic@negation, in \HOL\ logic!syntax of}
\index{negation, in HOL logic@negation, in \HOL\ logic!constructor for}
\index{existential quantifier, in HOL logic@existential quantifier, in \HOL\ logic!syntax of}
\index{universal quantifier, in HOL logic@universal quantifier, in \HOL\ logic!syntax of}
\index{implication, in HOL logic@implication, in \HOL\ logic!syntax of}
\index{mk_neg@\ml{mk\_neg}}
\index{mk_disj@\ml{mk\_disj}}
\index{mk_conj@\ml{mk\_conj}}
\index{mk_imp@\ml{mk\_imp}}
\index{mk_eq@\ml{mk\_eq}}
\index{mk_forall@\ml{mk\_forall}}
\index{mk_exists@\ml{mk\_exists}}
\index{mk_select@\ml{mk\_select}}
\index{mk_cond@\ml{mk\_cond}}
\index{mk_let@\ml{mk\_let}}
\index{conjunction, in HOL logic@conjunction, in \HOL\ logic!syntax of}
\begin{tabular}{|l|l|l|l|} \hline
\multicolumn{4}{|c|}{ } \\
\multicolumn{4}{|c|}{\bf Non-primitive terms} \\
\multicolumn{4}{|c|}{ } \\
{\it Kind of term} & {\it \ML\ quotation} & 
{\it Primitive term} &
{\it Constructor expression} \\ \hline
 & & & \\
Negation & {\small\verb%"~%}$t${\small\verb%"%} & {\small\verb%"$~ %}$t${\small\verb%"%} & {\small\verb%mk_neg("%}$t${\small\verb%")%} \\ \hline
Disjunction & {\small\verb%"%}$t_1${\small\verb%\/%}$t_2${\small\verb%"%} & {\small\verb%"$\/ %}$t_1\ t_2${\small\verb%"%} &
{\small\verb%mk_disj("%}$t_1${\small\verb%","%}$t_2${\small\verb%")%} \\ \hline
Conjunction & {\small\verb%"%}$t_1${\small\verb%/\%}$t_2${\small\verb%"%} & {\small\verb%"$/\ %}$t_1\ t_2${\small\verb%"%} &
{\small\verb%mk_conj("%}$t_1${\small\verb%","%}$t_2${\small\verb%")%} \\ \hline
Implication & {\small\verb%"%}$t_1${\small\verb%==>%}$t_2${\small\verb%"%} & {\small\verb%"$==> %}$t_1\ t_2${\small\verb%"%} &
{\small\verb%mk_imp("%}$t_1${\small\verb%","%}$t_2${\small\verb%")%} \\ \hline
Equality & {\small\verb%"%}$t_1${\small\verb%=%}$t_2${\small\verb%"%} & {\small\verb%"$= %}$t_1\ t_2${\small\verb%"%} &
{\small\verb%mk_eq("%}$t_1${\small\verb%","%}$t_2${\small\verb%")%} \\ \hline
$\forall$-quantification & {\small\verb%"!%}$x${\small\verb%.%}$t${\small\verb%"%} &
{\small\verb%"$!(\%}$x${\small\verb%.%}$t${\small\verb%)"%} & {\small\verb%mk_forall("%}$x${\small\verb%","%}$t${\small\verb%")%} \\ \hline
$\exists$-quantification & {\small\verb%"?%}$x${\small\verb%.%}$t${\small\verb%"%} &
{\small\verb%"$?(\%}$x${\small\verb%.%}$t${\small\verb%)"%} & {\small\verb%mk_exists("%}$x${\small\verb%","%}$t${\small\verb%")%} \\ \hline
$\hilbert$-term & {\small\verb%"@%}$x${\small\verb%.%}$t${\small\verb%"%} &
{\small\verb%"$@(\%}$x${\small\verb%.%}$t${\small\verb%)"%} & {\small\verb%mk_select("%}$x${\small\verb%","%}$t${\small\verb%")%} \\ \hline
Conditional\index{COND@\ml{COND}} & {\small\verb%"(%}$t${\small\verb%=>%}$t_1${\small\verb%|%}$t_2${\small\verb%)"%} &
{\small\verb%"COND %}$t\ t_1\ t_2${\small\verb%"%} & {\small\verb%mk_cond("%}$t${\small\verb%","%}$t_1${\small\verb%","%}$t_2${\small\verb%")%}
 \\ \hline
{\small\verb%let%}-expression & {\small\verb%"let %}$x${\small\verb%=%}$t_1${\small\verb% in %}$t_2${\small\verb%"%} &
{\small\verb%"LET(\%}$x${\small\verb%.%}$t_2${\small\verb%)%}$t_1${\small\verb%"%} &
{\small\verb%mk_let("\%}$x${\small\verb%.%}$t_1${\small\verb%","%}$t_2${\small\verb%")%} \\ \hline
\end{tabular}
\end{center}

\bigskip

There are constructors, destructors and indicators for all the
obvious constructs. (Indicators, \eg\ \ml{is\_neg}, return truth
values indicating whether or not a term belongs to the syntax
class in question.) In addition to the constructors listed in the table there
are constructors for pairs and lists, namely
\ml{mk\_pair}\index{mk_pair@\ml{mk\_pair}},
\ml{mk\_cons}\index{mk_cons@\ml{mk\_cons}} and
\ml{mk\_list}\index{mk_list@\ml{mk\_list}} (see \REFERENCE).
The constants {\small\verb%COND%}\index{COND@\ml{COND}} and {\small\verb%LET%} are explained in
Sections~\ref{conditionals} and \ref{let-exp}, respectively.  
The constants {\small\verb%\/%}\index{disjunction, in HOL logic@disjunction, in \HOL\ logic!syntax of}, {\small\verb%/\%},
{\small\verb%==>%} and {\small\verb%=%} are examples of {\it infixes\/}
and represent $\vee$, $\wedge$, $\imp$ and equality, respectively. If
$c$ is declared to be an infix, then the \HOL\ parser will translate
{\small\verb%"%}$t_1\ c\ t_2${\small\verb%"%} to 
{\small\verb%"$%}$c\ t_1\ t_2${\small\verb%"%}.  

The constants {\small\verb%!%}, {\small\verb%?%} and {\small\verb%@%} are examples
of \label{binder} {\it binders\/}\index{binders, in HOL logic@binders, in \HOL\ logic}
 and represent $\forall$, $\exists$ and $\hilbert$, respectively.  If $c$ 
is declared to be a binder, then the
\HOL\ parser will translate {\small\verb%"%}$c\ x${\small\verb%.%}$t${\small\verb%"%} to the combination
{\small\verb%"$%}$c${\small\verb%(\%}$x${\small\verb%.%}$t${\small\verb%)"%}
(\ie\ the application of the constant $c$ to the representation of
the abstraction $\lquant{x}t$)\index{ function abstraction binder, in HOL logic@{\small\verb+\+} (function abstraction binder, in \HOL\ logic)}.

In addition to the kinds of terms in the tables above, 
the parser also supports the following syntactic abbreviations.


\begin{center}

\index{variables, in HOL logic@variables, in \HOL\ logic!multiple bound}
\index{list_mk_comb@\ml{list\_mk\_comb}|pin} 
\index{list_mk_abs@\ml{list\_mk\_abs}|pin} 
\index{list_mk_forall@\ml{list\_mk\_forall}|pin} 
\index{list_mk_exists@\ml{list\_mk\_exists}|pin}
\index{combinations, in HOL logic@combinations, in \HOL\ logic!abbreviation for multiple} 
\index{existential quantifier, in HOL logic@existential quantifier, in \HOL\ logic!abbreviation for multiple}
\index{universal quantifier, in HOL logic@universal quantifier, in \HOL\ logic!abbreviation for multiple}
\begin{tabular}{|l|l|l|} \hline
\multicolumn{3}{|c|}{ } \\
\multicolumn{3}{|c|}{\bf Syntactic abbreviations} \\
\multicolumn{3}{|c|}{ } \\
{\it Abbreviated term} & {\it Meaning} & 
{\it Constructor expression} \\ \hline
 & &  \\
{\small\verb%"%}$t\ t_1 \cdots t_n${\small\verb%"%} &
{\small\verb%"(%}$\cdots${\small\verb%(%}$t\ t_1${\small\verb%)%}$\cdots t_n${\small\verb%)"%} &
{\small\verb%list_mk_comb("%}$t${\small\verb%",["%}$t_1${\small\verb%"; %}$\ldots${\small\verb% ;"%}$t_n${\small\verb%"])%} \\ \hline
{\small\verb%"\%}$x_1\cdots x_n${\small\verb%.%}$t${\small\verb%"%} &
{\small\verb%"\%}$x_1${\small\verb%. %}$\cdots${\small\verb% \%}$x_n${\small\verb%.%}$t${\small\verb%"%} &
{\small\verb%list_mk_abs(["%}$x_1${\small\verb%"; %}$\ldots${\small\verb% ;"%}$x_n${\small\verb%"],"%}$t${\small\verb%")%}
\\ \hline
{\small\verb%"!%}$x_1\cdots x_n${\small\verb%.%}$t${\small\verb%"%} &
{\small\verb%"!%}$x_1${\small\verb%. %}$\cdots${\small\verb% !%}$x_n${\small\verb%.%}$t${\small\verb%"%} &
{\small\verb%list_mk_forall(["%}$x_1${\small\verb%"; %}$\ldots${\small\verb% ;"%}$x_n${\small\verb%"],"%}$t${\small\verb%")%} 
\\ \hline
{\small\verb%"?%}$x_1\cdots x_n${\small\verb%.%}$t${\small\verb%"%} &
{\small\verb%"?%}$x_1${\small\verb%. %}$\cdots${\small\verb% ?%}$x_n${\small\verb%.%}$t${\small\verb%"%} &
{\small\verb%list_mk_exists(["%}$x_1${\small\verb%"; %}$\ldots${\small\verb% ;"%}$x_n${\small\verb%"],"%}$t${\small\verb%")%} \\ 
\hline
\end{tabular}
\end{center}

\noindent There are also constructors
\ml{list\_mk\_conj}\index{list_mk_conj@\ml{list\_mk\_conj}},
\ml{list\_mk\_disj}\index{list_mk_disj@\ml{list\_mk\_disj}},
\ml{list\_mk\_imp}\index{list_mk_imp@\ml{list\_mk\_imp}} and
\ml{list\_mk\_pair}\index{list_mk_pair@\ml{list\_mk\_pair}}
for conjunctions, disjunctions, implications and tuples respectively.
The corresponding destructor functions are called \ml{strip\_comb}, \etc,
except that there is no \ml{strip\_conj} or \ml{strip\_disj}. Instead there are
functions called \ml{conjuncts} and \ml{disjuncts}, but it should be noted
that these are not proper inverses of \ml{list\_mk\_conj} and
\ml{list\_mk\_disj}.
\index{term constructors, in HOL logic@term constructors, in \HOL\ logic|)}
\index{terms, in HOL logic@terms, in \HOL\ logic!constructors for|)}


\section{Syntax for restricted quantification}\label{res-quant}
\index{types, in HOL logic@types, in \HOL\ logic!dependent}
\index{dependent types in HOL logic@dependent types in \HOL\ logic}
\index{quantifiers!restricted}

Syntactic support for restricted quantification and abstraction is 
provided. This follows a suggestion discussed at the Second \HOL\ Users
Meeting and implements a method of simulating subtypes and dependent
types with predicates. 

Currently no derived rules are provided to support this notation, so
any inferences will need to work on the underlying semantic
representation.

The new syntax automatically translates as follows:

\begin{hol}
{\small\verb%   \%}$v${\small\verb%::%}$P${\small\verb%.%}$B${\small\verb%    <---->   RES_ABSTRACT %}$P${\small\verb% (\%}$v${\small\verb%.%}$B${\small\verb%)%}\\
{\small\verb%   !%}$v${\small\verb%::%}$P${\small\verb%.%}$B${\small\verb%    <---->   RES_FORALL   %}$P${\small\verb% (\%}$v${\small\verb%.%}$B${\small\verb%)%}\\
{\small\verb%   ?%}$v${\small\verb%::%}$P${\small\verb%.%}$B${\small\verb%    <---->   RES_EXISTS   %}$P${\small\verb% (\%}$v${\small\verb%.%}$B${\small\verb%)%}\\
{\small\verb%   @%}$v${\small\verb%::%}$P${\small\verb%.%}$B${\small\verb%    <---->   RES_SELECT   %}$P${\small\verb% (\%}$v${\small\verb%.%}$B${\small\verb%)%}
\end{hol}

Anything can be written between the binder and `\ml{::}' that can be
written between the binder and `\ml{.}`. See the examples below.

The flag \ml{print\_restrict} has default \ml{true}, but if set to \ml{false}
will disable the pretty printing. This is useful for seeing what the semantics
of particular restricted abstractions are.

The constants \ml{RES\_ABSTRACT}, \ml{RES\_FORALL}, \ml{RES\_EXISTS} and 
\ml{RES\_SELECT} are
defined in the theory \ml{bool} by:


\begin{hol}\index{RES_FORALL@\ml{RES\_FORALL}}
\index{RES_EXISTS@\ml{RES\_EXISTS}}
\index{RES_SELECT@\ml{RES\_SELECT}}
\index{RES_ABSTRACT@\ml{RES\_ABSTRACT}}\begin{verbatim}
   RES_ABSTRACT P B  =  \x:*. (P x => B x | ARB:**)

   RES_FORALL   P B  =  !x:*. P x ==> B x

   RES_EXISTS   P B  =  ?x:*. P x /\ B x

   RES_SELECT   P B  =  @x:*. P x /\ B x
\end{verbatim}\end{hol}

\noindent where the constant \ml{ARB}\index{ARB@\ml{ARB}},
which is also defined in the theory \ml{bool}, has the definition:

\begin{hol}\begin{verbatim}
   ARB  =  @x:*. T
\end{verbatim}\end{hol}

User-defined binders can also have restricted forms, which are set up
with the function:

\begin{boxed}\index{associate_restriction@\ml{associate\_restriction}|pin}
\begin{verbatim}
   associate_restriction : (string # string) -> *
\end{verbatim}\end{boxed}


\noindent If \m{c} is the name
of a binder and \ml{RES\_}\m{c} is the name of a suitable constant (which
must be explicitly defined), then executing:

\begin{hol}
{\small\verb%   associate_restriction(`%}$c${\small\verb%`, `RES_%}$c${\small\verb%`)%}
\end{hol}

\noindent will cause the parser and pretty-printer to support:

\begin{hol}
{\small\verb%   %}$c$ $v${\small\verb%::%}$P${\small\verb%. %}$B${\small\verb%    <---->   RES_%}$c$ $P${\small\verb% (\%}$v${\small\verb%. %}$B${\small\verb%)%}
\end{hol}

\noindent Note that associations between user defined binders and their
restrictions are not stored in theory files, so they have to be set up
for each \HOL\ session (e.g. with a {\small\verb%hol-init.ml%}
initialization file -- see Section~\ref{hol-init}).

Here is an example session:

\setcounter{sessioncount}{1}
\begin{session}\begin{verbatim}
#"!x y::P. x<y";;
"!x y :: P. x < y" : term

#set_flag(`print_restrict`, false);;
true : bool

#"!x y::P. x<y";;
"RES_FORALL P(\x. RES_FORALL P(\y. x < y))" : term

#"?(x,y) p::(\(m,n).m<n). p=(x,y)";;
"RES_EXISTS
 (\(m,n). m < n)
 (\(x,y). RES_EXISTS(\(m,n). m < n)(\p. p = x,y))"
: term

#"\x y z::P.[0;x;y;z]";;
"RES_ABSTRACT P(\x. RES_ABSTRACT P(\y. RES_ABSTRACT P(\z. [0;x;y;z])))"
: term
\end{verbatim}\end{session}

A conversion that rewrites away the constants \ml{RES\_ABSTRACT},
\ml{RES\_FORALL}, \ml{RES\_EXISTS} and \ml{RES\_SELECT} is:

\begin{hol}\begin{verbatim}
   let RESTRICT_CONV =
	(PURE_REWRITE_CONV [definition `bool` `RES_ABSTRACT`;
                            definition `bool` `RES_FORALL`;
                            definition `bool` `RES_EXISTS`;
                            definition `bool` `RES_SELECT`])
        THENC (DEPTH_CONV BETA_CONV)
\end{verbatim}\end{hol}

\noindent This is a bit unsatisfactory, as is shown by the artificial
example below:

\setcounter{sessioncount}{1}
\begin{session}\begin{verbatim}
#let t = "!x y::P.?f:num->num::Q. f(@n::R.T) = (x+y)";;
t = "!x y :: P. ?f :: Q. f(@n :: R. T) = x + y" : term

#RESTRICT_CONV t;;
|- (!x y :: P. ?f :: Q. f(@n :: R. T) = x + y) =
   (!x. P x ==> (!x'. P x' ==> (?x. Q x /\ (x(@x. R x /\ T) = x + x'))))
\end{verbatim}\end{session}

The variable $x$ in the definitions of the constants
\ml{RES\_ABSTRACT}, \ml{RES\_FORALL}, \ml{RES\_EXISTS} and
\ml{RES\_SELECT} gets confused with the variable in the supplied term.
This can be avoided by changing \ml{RESTRICT\_CONV} to perform
explicit alpha-conversion. For example, by implementing a conversion:

\begin{hol}
{\small\verb%   RES_FORALL %}$P${\small\verb% (\%}$v$\ml{.}$B$\ml{[}$v$\ml{])  ---->  !}$v$\ml{. }$P$ $v$\ml{ ==> }$B$\ml{[}$v$\ml{]}
\end{hol}

\noindent Dealing with the case when
$v$ is a variable structure is also desirable. For example:

\begin{session}\begin{verbatim}
#let t1 = "!(m,n)::P. m<n";;
t1 = "!(m,n) :: P. m < n" : term

#RESTRICT_CONV t1;;
|- (!(m,n) :: P. m < n) = (!x. P x ==> (\(m,n). m < n)x)

\end{verbatim}\end{session}

\noindent If anyone writes the desired conversions please let us know!

Here is an example of a user-defined restriction:

\begin{session}\begin{verbatim}
#new_binder_definition(`DURING`, "DURING(p:num#num->bool) = $!p");;
|- !p. $DURING p = $! p

#"DURING x::(m,n). p x";;
no restriction constant associated with DURING
skipping: x " ;; parse failed  

#new_definition
# (`RES_DURING`, "RES_DURING(m,n)p = !x. m<=x /\ x<=n ==> p x");;
|- !m n p. RES_DURING(m,n)p = (!x. m <= x /\ x <= n ==> p x)

#associate_restriction(`DURING`,`RES_DURING`);;
() : void

#"DURING x::(m,n). p x";;
"DURING x :: (m,n). p x" : term

#set_flag(`print_restrict`,false);;
true : bool

#"DURING x::(m,n). p x";;
"RES_DURING(m,n)(\x. p x)" : term
\end{verbatim}\end{session}




\subsection{Conditionals}
\label{conditionals}

A conditional\index{terms, in HOL logic@terms, in \HOL\ logic!conditional}\index{conditional predicate, in HOL logic@conditional predicate, in \HOL\ logic}\index{conditionals, in HOL logic@conditionals, in \HOL\ logic}
 term \ml{"$t_1\ $=>$\ t_2\ $|$\ t_3$"} means 
`if $t_1$ then $t_2$ else
$t_3$' and abbreviates the application 
\ml{"COND\ $t_1\ t_2\ t_3$"}, where \ml{COND}\index{COND@\ml{COND}}\index{conditionals, in HOL logic@conditionals, in \HOL\ logic}
is a predefined
constant of the theory \ml{bool} (see Section~\ref{boolthy}). 
An iterated conditional

\[
t_{11}\ \ml{=>}\ t_{12}\ \ml{|}\ 
t_{21}\ \ml{=>}\ t_{22}\ \ml{|}\ 
\ \ldots\ \ml{|}\ 
t_{n1}\ \ml{=>}\ t_{n2}\ \ml{|}\ t_{n3}
\]

\noindent translates\index{parsing, of HOL logic@parsing, of \HOL\ logic!of conditionals} to:

\[
t_{11}\ \ml{=>}\ t_{12}\ \ml{|}\ 
(t_{21}\ \ml{=>}\ t_{22}\ \ml{|}\ 
\ \ldots\ \ml{|}\ 
(t_{n1}\ \ml{=>}\ t_{n2}\ \ml{|}\ t_{n3})\ \ldots\ )
\]

\noindent which, in turn, abbreviates:

\[\ml{COND}\ t_{11}\ t_{12}\ \ml{(COND}\ t_{21}\ t_{22}\ \ldots\ 
\ml{(COND}\ t_{n1}\ t_{n2}\ t_{n3}\ml{)}\ \ldots\ \ml{)}\]

\subsection{Paired abstractions}
\label{HOL-varstruct}
\index{pairs, in HOL logic@pairs, in \HOL\ logic!in abstractions|(}
\index{UNCURRY@\ml{UNCURRY}|(}

\index{terms, in HOL logic@terms, in \HOL\ logic!pair|(}
\index{parsing, of HOL logic@parsing, of \HOL\ logic!of quotation syntax|(}
\index{function abstraction, in HOL logic@function abstraction, in \HOL\ logic!paired|(}
\index{function abstraction, in HOL logic@function abstraction, in \HOL\ logic!uncurrying, in paired|(}
The quotation parser\index{parsing, of HOL logic@parsing, of \HOL\ logic!of function abstractions}\index{function abstraction, in HOL logic@function abstraction, in \HOL\ logic!abbreviation for multiple}\index{terms, in HOL logic@terms, in \HOL\ logic!function abstraction}
 will convert
{\small\verb%"\(%}$x_1${\small\verb%,%}$x_2${\small\verb%).%}$t${\small\verb%"%}
to {\small\verb%"UNCURRY(\%}$x_1\ x_2${\small\verb%.%}$t${\small\verb%)"%},
where the constant {\small\verb%UNCURRY%} 
is defined by:

\begin{hol}\begin{verbatim}
   UNCURRY f (x,y)  =  f x y
\end{verbatim}\end{hol}

\noindent See Section~\ref{prod} for more details and an explanation
of pair terms \ml{($t_1$,$t_2$)}.
The transformation is done recursively so that, for example,


\begin{hol}\begin{alltt}
   "\verb%\%(\m{x\sb{1}},\m{x\sb{2}},\m{x\sb{3}}).\m{t}"
\end{alltt}\end{hol}

\noindent is converted to

\begin{hol}\begin{alltt}
   "UNCURRY \verb%\%\m{x\sb{1}}.UNCURRY(\verb%\%\m{x\sb{2}},\m{x\sb{3}}.\m{t}))"
\end{alltt}\end{hol}

\noindent More generally,
the quotation parser repeatedly applies the transformation:

\begin{hol}\begin{alltt}
   "\verb%\%(\m{v\sb{1}},\m{v\sb{2}}).\m{t}"\m{\quad \leadsto\quad }"UNCURRY(\verb%\%\m{v\sb{1}}.\verb%\%\m{v\sb{2}}.\m{t})"
\end{alltt}\end{hol}

\noindent until no more variable structures remain. For example:

\begin{flushleft}
\begin{tabular}{@{}ll}
{\small\verb%   "\(%}$x${\small\verb%,%}$y${\small\verb%).%}$t${\small\verb%"%}
&$\leadsto\ \ ${\small\verb%"UNCURRY(\%}$x\
y${\small\verb%.%}$t${\small\verb%)"%}\\
{\small\verb%   "\(%}$x_1${\small\verb%,%}$x_2${\small\verb%,%}$\ldots${\small\verb%,%}$x_n${\small\verb%).%}$t${\small\verb%"%}
&$\leadsto\ \ ${\small\verb%"UNCURRY(\%}$x_1${\small\verb%.\(%}$x_2${\small\verb%,%}$\ldots${\small\verb%,%}$x_n${\small\verb%).%}$t${\small\verb%)"%}\\
{\small\verb%   "\((%}$x_1${\small\verb%,%}$\ldots${\small\verb%,%}$x_n${\small\verb%),%}$y_1${\small\verb%,%}$\ldots${\small\verb%,%}$y_m${\small\verb%).%}t{\small\verb%"%}
&$\leadsto\ \ ${\small\verb%"UNCURRY(\(%}$x_1${\small\verb%,%}$\ldots${\small\verb%,%}$x_n${\small\verb%).\(%}$y_1${\small\verb%,%}$\ldots${\small\verb%,%}$y_m${\small\verb%).%}$t${\small\verb%)"%}\\
\end{tabular}
\end{flushleft}

\index{parsing, of HOL logic@parsing, of \HOL\ logic!of quotation syntax|)} 
The \HOL\ top-level printer\index{printing, in HOL logic@printing, in \HOL\ logic!of function abstractions}
 inverts these transformations if the 
flag\footnote{See Section~\ref{flags} for details of \ML\ flags.}
\ml{print\_uncurry} is \ml{true}. For example:

\setcounter{sessioncount}{1}
\begin{session}\begin{verbatim}
#"\((a,b),(x,y)). (a+b) < (x*y)";;
"\((a,b),x,y). (a + b) < (x * y)" : term

#set_flag(`print_uncurry`,false);;
true : bool

#"\((a,b),(x,y)). (a+b) < (x*y)";;
"UNCURRY(UNCURRY(\a b. UNCURRY(\x y. (a + b) < (x * y))))" : term
\end{verbatim}\end{session}

Note that a variable structure like \ml{"(x,y)"} in 
{\small\verb%"\(x,y).x+y"%} 
is not a subterm
of the abstraction\index{function abstraction, in HOL logic@function abstraction, in \HOL\ logic!subterms of} in which it occurs; it disappears on parsing\index{binders, in HOL logic@binders, in \HOL\ logic!parsing of}\index{parsing, of HOL logic@parsing, of \HOL\ logic!of binders}. This can 
lead to unexpected errors (accompanied by obscure error messages).  
For example:

\begin{session}\begin{verbatim}
#"\(x,y).x+y";;
"\(x,y). x + y" : term

#let p = "(x:num,y:num)";;
p = "x,y" : term

#"\^p.x+y";;
evaluation failed     mk_abs in quotation 
\end{verbatim}\end{session}

Furthermore, if the type checker complains, it may print out
diagnostic messages referring to the transformed term:

\begin{session}\begin{verbatim}
#"\(x,y). x+1";;
Indeterminate types:
    "UNCURRY:(num -> (?1 -> num)) -> (num # ?2 -> num)"

evaluation failed     types indeterminate in quotation 
\end{verbatim}\end{session}

If $b$ is a binder, then
\ml{"}$b$\ml{(}$x_1${\small\verb%,%}$x_2${\small\verb%).%}$t${\small\verb%"%}
is parsed as
{\small\verb%"$%}$b${\small\verb%(\(%}$x_1${\small\verb%,%}$x_2${\small\verb%).%}$t${\small\verb%)"%}, and hence transformed as above.
For example, {\small\verb%"!(x,y).x>y"%} parses to
{\small\verb%"$!(UNCURRY(\x.\y.$> x y))"%} (where {\small{\tt >}} is an infixed
constant of the theory {\small\verb%num%} meaning `is greater than')\index{function abstraction, in HOL logic@function abstraction, in \HOL\ logic!paired|)}. 
\index{function abstraction, in HOL logic@function abstraction, in \HOL\ logic!uncurrying, in paired|)}\index{pairs, in HOL logic@pairs, in \HOL\ logic!in abstractions|)}\index{terms, in HOL logic@terms, in \HOL\ logic!pair|)}\index{UNCURRY@\ml{UNCURRY}|)}


%A good exercise for the reader would be to understand why this use 
%of \ml{UNCURRY} supports the intuitive meaning suggested by the surface
%notation.

Applications of paired abstraction to tuples can be $\beta$-reduced using
\ml{PAIRED\_BETA\_CONV} (see Section~\ref{genbeta}).

\subsection{{\tt let}-terms}
\label{let-exp}


The quotation parser\index{parsing, of HOL logic@parsing, of \HOL\ logic!of let-terms@of \ml{let}-terms}
 accepts \ml{let}-terms\index{terms, in HOL logic@terms, in \HOL\ logic!let-@\ml{let}-}\index{let-terms, in HOL logic@\ml{let}-terms, in \HOL\ logic!as abbreviations} superficially similar to those in 
\ML. For example, the following terms are allowed:

\begin{hol}\begin{verbatim}
   "let x = 1 and y = 2 in x+y"

   "let f(x,y) = (x*x)+(y*y) and a = 20*20 and b = 50*49 in f(a,b)"
\end{verbatim}\end{hol}

As with paired abstractions, \ml{let}-terms are actually abbreviations for 
ordinary  terms which are specially supported by the parser and pretty printer.
The constant \ml{LET}\index{LET@\ml{LET}} is defined (in the theory \ml{bool}) by:

\begin{hol}\index{function abstraction, in HOL logic@function abstraction, in \HOL\ logic!relation to let-terms@relation to \ml{let}-terms}
\begin{verbatim}
   LET = (\f x. f x)
\end{verbatim}\end{hol}

\noindent and is used to encode \ml{let}-terms in the logic. The parser
repeatedly applies the transformations:

\bigskip

\noindent
{\small\begin{tabular}{@{}ll}
{\small\verb%   "let %}$f\ v_1\ \ldots\ v_n${\small\verb% = %}$t_1${\small\verb% in
%}$t_2${\small\verb%"%}
&$\leadsto\ \ ${\small\verb%"LET(\%}$f${\small\verb%.%}$t_2$
{\small\verb%)(\%}$v_1\ \ldots\ v_n${\small\verb%.%}$t_1${\small\verb%)"%}\\
{\small\verb%   "let (%}$v_1${\small\verb%,%}$\ldots${\small\verb%,%}$v_n${\small\verb%) =
%}$t_1${\small\verb% in %}$t_2${\small\verb%"%}
&$\leadsto\ \ ${\small\verb%"LET(\(%}$v_1${\small\verb%,%}$\ldots${\small\verb%,%}$v_n${\small\verb%).%}$t_2${\small\verb%)%}$t_1${\small\verb%"%}\\
{\small\verb%   "let %}$v_1${\small\verb%=%}$t_1${\small\verb% and %}$\ldots${\small\verb% and %}$v_n${\small\verb%=%}$t_n${\small\verb% in
%}$t${\small\verb%"%}
&$\leadsto\ \ ${\small\verb%"LET(%}$\ldots${\small\verb%(LET(LET(\%}$v_1\ldots v_n${\small\verb%.%}$t${\small\verb%)%}$t_1${\small\verb%)%}$t_2${\small\verb%)%}$\ldots${\small\verb%)%}$t_n${\small\verb%"%}\\
\end{tabular}}

\bigskip
 

\noindent The printer\index{printing, in HOL logic@printing, in \HOL\ logic!of let-terms@of \ml{let}-terms} inverts these transformations if the flag 
\ml{print\_let} is \ml{true}.  For example:

\setcounter{sessioncount}{1}
\begin{session}\begin{verbatim}
#"let x = 1 and y = 2 in x+y";;
"let x = 1 and y = 2 in x + y" : term

#set_flag(`print_let`,false);;
true : bool

#"let x = 1 and y = 2 in x+y";;
"LET(LET(\x y. x + y)1)2"

#"let (x,y) = (1,2) in x+y";;
"LET(UNCURRY(\x y. x + y))(1,2)" : term
\end{verbatim}\end{session}

Note that, as with uncurried terms, the underlying representation in \HOL\ can
manifest itself in error messages. For example:

\setcounter{sessioncount}{1}
\begin{session}\begin{verbatim}
#"let x = y in z";;
Indeterminate types:  "LET:(?1 -> ?2) -> (?3 -> ?4)"
 
evaluation failed     types indeterminate in quotation 
\end{verbatim}\end{session}

The reader is recommended to convince himself or herself that the
translations of \ml{let}-terms represent the intuitive meaning suggested by 
the surface syntax.\index{quotation, in HOL logic@quotation, in \HOL\ logic|)}\index{quotation, in HOL logic@quotation, in \HOL\ logic!of non-primitive terms|)}\index{terms, in HOL logic@terms, in \HOL\ logic!syntax of|)}\index{type checking, in HOL logic@type checking, in \HOL\ logic!special forms in|)}

\ml{let}-terms can be simplified with \ml{let\_CONV} -- see Section~\ref{let-terms}.

\section{Syntax for sets}\index{set theory notation}

The special purpose set-theoretic notations 
{\small\verb%"{%}$t_1,t_2,\ldots,t_n${\small\verb%}"%} and
{\small\verb%"{%}$t${\small\verb%|%}$p${\small\verb%}"%} are available.
The normal interpretation of the former is the finite set containing 
$t_1,t_2,\ldots, t_n$ and the normal interpretation of the latter
is the set of all $t$s such that $p$. These interpretations are predefined for
the library \ml{sets}, but the user can use the syntax for other purposes if
he or she wishes, using the functions:

\begin{boxed}
\index{define_finite_set_syntax@\ml{define\_finite\_set\_syntax}|pin}
\index{define_set_abstraction_syntax@\ml{define\_set\_abstraction\_syntax}|pin}
\begin{alltt}
   define_finite_set_syntax      : (string # string) -> void
   define_set_abstraction_syntax : string -> void
\end{alltt}\end{boxed}

\noindent Executing:

\begin{hol}\begin{alltt}
   define_finite_set_syntax(`\(c\sb{1}\)`,`\(c\sb{2}\)`)
\end{alltt}\end{hol}

\noindent causes {\small\verb%"{%}$t_1,\ldots,t_n${\small\verb%}"%}
to parse to:

\begin{hol}\begin{alltt}
   "\(c\sb{2}\) \(t\sb{1}\) (\(c\sb{2}\) \(t\sb{2}\) \(\cdots\) (\(c\sb{2}\) \(t\sb{n}\) \(c\sb{1}\)) \(\cdots\) ))"
\end{alltt}\end{hol}

\noindent with failure if either $c_1$ or $c_2$ is not the name of a constant.

In the library \ml{sets}, the empty set is \ml{EMPTY} and
the infixed function \ml{INSERT} adds an element to a set.
Executing:

\begin{hol}\begin{verbatim}
   define_finite_set_syntax(`EMPTY`,`INSERT`)
\end{verbatim}\end{hol}

\noindent will cause

\begin{hol}\begin{verbatim}
   "{1,2,3,4}"
\end{verbatim}\end{hol}

\noindent to parse to

\begin{hol}\begin{verbatim}
   "1 INSERT (2 INSERT (3 INSERT (4 INSERT EMPTY)))"
\end{verbatim}\end{hol}


Executing:

\begin{hol}\begin{alltt}
   define_set_abstraction_syntax `\(c\)`
\end{alltt}\end{hol}

\noindent causes  {\small\verb%"{%}$t${\small\verb%|%}$p${\small\verb%}"%}
to parse to:

\medskip

\noindent{\small
{\verb%   "%}}$c${\small{\verb%(\(%}$x_1${\verb%,%}$\ldots${\verb%,%}$x_n${\verb%).(%}$t${\verb%,%}$p${\verb%))"%}
}

\medskip

\noindent where $x_1$, $\ldots$ , $x_n$ are the free variables occurring in both $t$
and $p$.  If there are no such free variables then an error results.
The order in which the variables are listed in the variable structure
of the paired abstraction is an unspecified function of the structure
of $t$ (it is approximately left to right). Failure if $c$ is not the
name of a constant.

For example, if the library \ml{sets} (i.e. what used to be \ml{all\_sets})
is loaded, then

\begin{hol}\begin{verbatim}
   define_set_abstraction_syntax `GSPEC`
\end{verbatim}\end{hol}

\noindent will cause

\begin{hol}\begin{verbatim}
   "{x+y | (x < y) /\ (y < z)}"
\end{verbatim}\end{hol}

\noindent to parse to:

\begin{hol}\begin{verbatim}
   "GSPEC(\(x,y). ((x+y), (x < y) /\ (y < z)))"
\end{verbatim}\end{hol}

\noindent where \ml{GSPEC} is defined by:

\begin{hol}\begin{verbatim}
   |- !f. GSPEC f = SPEC(\x. ?y. x,T = f y)
\end{verbatim}\end{hol}

\noindent and \ml{SPEC} abstracts a predicate to a set (it is the abstraction
bijection used in the definition of the type operator \ml{set}).
Other examples are:

\begin{hol}\begin{verbatim}
   "{x+y+z | (x < y) /\ (y < z)}"
\end{verbatim}\end{hol}

\noindent will parse to:

\begin{hol}\begin{verbatim}
   "GSPEC(\(x,y,z). (x+(y+z), (x < y /\ y < z)))" 
\end{verbatim}\end{hol}

\noindent and

\begin{hol}\begin{verbatim}
   "{x+y+w | (x < y) /\ (y < z)}"
\end{verbatim}\end{hol}

\noindent will parse to:

\begin{hol}\begin{verbatim}
   "GSPEC(\(x,y). (x+(y+w), (x < y /\ y < z)))"
\end{verbatim}\end{hol}


Note that the precedence of comma is increased in the contexts 
``{\small\verb%{%}$\cdots${\small\verb%}%}'' and 
``{\small\verb%{%}$\cdots${\small\verb%|%}''.
Terms will be printed in set notation if the flag \ml{print\_set} is
\ml{true}.
Note that 

\medskip

\ml{"}$c${\small\verb%(\(%}$x_1$\ml{,}$\ldots$\ml{,}$x_n$\ml{).(}$t$\ml{,}$p$\ml{))"} 

\medskip

\noindent will only print as 
{\small\verb%"{%}$t${\small\verb%|%}$p${\small\verb%}"%} 
if the variables $x_1$, $\ldots$ , 
$x_n$ occur free in both $t$ and $p$ (and \ml{print\_set} is \ml{true}) .


\subsection{Antiquotation}

Within a quotation, expressions of the form
{\small\verb%^(%}$t${\small\verb%)%}\index{ antiquotation, in HOL logic@{\small\verb+^+} (antiquotation, in \HOL\ logic)} (where $t$ is an \ML\ expression of
type\index{type checking, in HOL logic@type checking, in \HOL\ logic!antiquotation in} {\small\verb%term%} or {\small\verb%type%}) are called {\it
antiquotations\/}\index{terms, in HOL logic@terms, in \HOL\ logic!antiquotation}\index{antiquotation, in HOL logic terms@antiquotation, in \HOL\ logic terms}.
An antiquotation {\small\verb%^(%}$t${\small\verb%)%}
evaluates to the \ML\ value of $t$. For example, {\small\verb%"x \/
^(mk_conj("y:bool","z:bool"))"%} evaluates to the same term as
{\small\verb%"x \/ (y /\ z)"%}. The most common use of antiquotation
is when the term $t$ is just an \ML\ variable $x$. In this case
{\small\verb%^(%}$x${\small\verb%)%} can be abbreviated by
{\small\verb%^%}$x$. 

The following session illustrates antiquotation.

\setcounter{sessioncount}{1}
\begin{session}\begin{verbatim}
#let y = "x+1";;
y = "x + 1" : term

#let z = "y = ^y";;
z = "y = x + 1" : term

#"!x:num.?y:num.^z";;
"!x. ?y. y = x + 1" : term
\end{verbatim}\end{session}


\subsection{User-programmable quotation typechecker}
\index{quotation, in HOL logic@quotation, in \HOL\ logic!typechecker for|(}

The typechecker for \HOL\ quotations contains a number of arbitrary
design decisions. Several people have suggested changes, e.g. that
full Hindley/Milner type inference be performed. Rather than try to
create a single new improved typechecker, a facility is now provided
that enables the user to write his or her own one and then to install
it in the system.

\index{preterms|(}
The \ML\ abstract type {\small\verb%preterm%} represents the parse trees of \HOL\ 
terms. A typechecker is a function of type {\small\verb%preterm->term%}. If the flag
\ml{preterm} is set to \ml{true} (the default is \ml{false}), then \HOL\ will use
whatever \ML\ function is currently bound to the name 
\ml{preterm\_handler} as
the quotation typechecker. The way this works is that when
\ml{preterm} is true the parser produces a preterm rather than a term,
and then wraps a call of \ml{preterm\_handler} 
around the quotation.\index{type checking, in HOL logic@type checking, 
in \HOL\ logic!user programmed} Other uses of preterms are possible, for example
as patterns for describing terms. 

The definition of the \ML\ type {\small\verb%preterm%} is:

\begin{hol}\index{preterm@\ml{preterm}!the type}\begin{alltt}
   rectype preterm = 
     preterm_var      of string                        \({\it Variables}\) 
   | preterm_const    of string                        \({\it Constants}\) 
   | preterm_comb     of preterm # preterm             \({\it Combinations}\) 
   | preterm_abs      of preterm # preterm             \({\it Abstractions}\) 
   | preterm_typed    of preterm # type                \({\it Explicit typing}\) 
   | preterm_antiquot of term                          \({\it Antiquotation}\) 
\end{alltt}\end{hol}

The function:

\begin{boxed}\index{preterm_to_term@\ml{preterm\_to\_term}|pin}
\begin{verbatim}
   preterm_to_term : preterm -> term
\end{verbatim}\end{boxed}

\noindent invokes the standard \HOL\ typechecker on a preterm and returns the
resulting typechecked term (or causes the standard error message).\index{preterms|)}



The following is a rather contrived example:

\setcounter{sessioncount}{1}
\begin{session}\index{preterm_handler@\ml{preterm\_handler}|pin}
\begin{verbatim}
#letref p_reg = preterm_var `x`;;
p_reg = preterm_var `x` : preterm

#let preterm_handler p = p_reg:=p; 
                         print_string `Typechecking ... `;
                         print_newline();
                         preterm_to_term p;;
preterm_handler = - : (preterm -> term)
\end{verbatim}\end{session}

\begin{session}
\begin{verbatim}
#set_flag(`preterm`,true);;
false : bool

#"x+y";;
Typechecking ...
"x + y" : term

#p_reg;;
preterm_comb((preterm_comb((preterm_const `+`), preterm_var `x`)),
             preterm_var `y`)
: preterm
\end{verbatim}\end{session}

\noindent Different top-level typechecking can be defined by using a
different definition of the function
\ml{preterm\_handler}. Note that quotations and their typechecking
is purely a `user interface' feature, so changing the typechecker does
not compromise the logical soundness of \HOL.\index{quotation, in HOL logic@quotation, in \HOL\ logic!typechecker for|)}



\section{Theorems}
\label{avra_theorems}
% I have added this section in a hurry 9 Nov 89.  Was missing!

In Chapter~\ref{logic}, the notion of deduction was introduced in terms
of {\it sequents\/}\index{sequents!in natural deduction}, where a sequent
is a pair whose second component is a formula being
asserted (a conclusion)\index{conclusions!of sequents}, 
and whose first component is a set of formulas (hypotheses)\index{hypotheses!of sequents}.
Based on this was the notion of a {\it deductive system\/}\index{natural deduction}\index{deductive systems}: a set of pairs,
whose second component is a sequent, and
whose first component is a sequent list\footnote{Note that these sequents
form a list, not a set; that is, are ordered.}.
The concept of a sequent {\it following from\/}\index{follows from, in natural deduction}
a set of sequents via a
deductive system was then defined: a sequent follows from a set of sequents if
the sequent
is the last element of some chain of sequents, each of whose
elements is either in the set, or itself follows from the set along with
earlier elements of the chain, via the deductive system.

A notation for `follows from' was then introduced.
That a
sequent $(\{t_1,\ldots,t_n\},\ t)$ follows from
a set of sequents $\Delta$, via a deductive system ${\cal D}$, is
denoted\index{turnstile notation|(} by: $t_1,\ldots,t_n\vdash_{{\cal D},\Delta} t$.
(It was noted that
where either ${\cal D}$ or $\Delta$ were clear by context, their mention
could be omitted; and where the set of hypotheses was empty,
its mention could be omitted.)

A sequent that follows from the empty set of sequents via
a deductive system is called a {\it theorem\/} of that deductive system.
That is, a theorem\index{theorems, in natural deduction} is the last element of a {\it proof\/}\index{proof!in natural deduction} (in the sense
of Chapter~\ref{logic}) from the empty
set of sequents. When a pair $(L,(\Gamma,t))$ belongs to a deductive system,
and the list $L$ is empty, 
then the sequent $(\Gamma,t)$ is called an {\it axiom\/}\index{axioms!in
natural deduction}. 
Any pair $(L,(\Gamma,t))$ belonging to 
a deductive system is called a {\it primitive inference\/}\index{inference, in natural deduction}\index{primitive inference, in natural deduction}
of the system, with hypotheses\footnote{Note that
`hypotheses' and `conclusion' are also used for the components
of sequents.} $L$ and 
conclusion $(\Gamma,t)$.

A formula\index{formulas as terms, in HOL logic@formulas as terms, in \HOL\ logic}
 in the abstract is represented concretely in \HOL\ by
a term whose \HOL\ type is {\small\verb%":bool"%}.
Therefore, a term\index{terms, in HOL logic@terms, in \HOL\ logic!as logical formulas} of type {\small\verb%":bool"%} is used to represent
a member of the set of hypotheses of a sequent;
and likewise to represent the
conclusion of a sequent.
Sets in this context
are represented by lists, so the set of hypotheses of a sequent\index{sequents!representation of, in HOL logic@representation of, in \HOL\ logic}
is represented by a list of {\small\verb%":bool"%}-typed terms.

A theorem in the abstract is represented concretely in the \HOL\
system by a value with the \ML\ abstract type
{\small\verb%thm%}\index{thm@\ml{thm}}. 
The type {\small\verb%thm%} has a primitive destructor function

\begin{boxed}
\index{dest_thm@\ml{dest\_thm}|pin}
\begin{verbatim}
   dest_thm : thm -> (term list # term)
\end{verbatim}\end{boxed}

\noindent which returns a pair consisting of the hypothesis\index{hypotheses!of theorems} list and
the conclusion\index{conclusions!of theorems}, respectively, of a theorem.
From this, two destructor\index{theorems, in HOL logic@theorems, in \HOL\ logic!destructors for} functions are derived


\begin{boxed}
\index{hyp@\ml{hyp}|pin}
\index{concl@\ml{concl}|pin}
\begin{verbatim}
   hyp   : thm -> term list
   concl : thm -> term
\end{verbatim}\end{boxed}

\noindent for extracting the hypothesis list and the conclusion, respectively,
of a theorem. The \ML\ type {\small\verb%thm%} does not have
a primitive constructor function.  In this way, the \ML\ type system protects
the \HOL\ logic
from the arbitrary and unrecorded construction 
of theorems, which would compromise
the consistency\index{consistency, of HOL logic@consistency, of \HOL\ logic} of the logic. (Functions which return theorems as values,
\eg\ functions representing primitive inferences,
are discussed first in Section~\ref{rules}, and further in 
Chapter\ref{derived-rules}.)

It was mentioned in Chapter~\ref{logic} that the deductive system of \HOL\
includes five axioms\footnote{This is
a simplification: 
%each inference rule corresponds to an infinite family of elements
%of the deductive system, and
the axioms are an extension 
of the basic logic. See Sections~\ref{boolthy} and \ref{ind}.}.
In that Chapter, the axioms were presented in abstract form.
The concrete representation of the axioms in \HOL\ is given
in Section~\ref{HOL-theory}.
% and of the inference rules, in 
%Section~\ref{rules}. 
To anticipate, the axiom \ml{BOOL\_CASES\_AX}
mentioned in Chapter~\ref{logic} is printed in \HOL\ as follows
(where \ml{"T"} and \ml{"F"} 
are the \HOL\ logic's constants representing truth and
falsity, respectively):

\begin{hol}
\index{F@\ml{F}!axiom for}
\begin{verbatim}
   |- !t. (t = T) \/ (t = F)
\end{verbatim}\end{hol}

\noindent Note the special print format\index{printing, in HOL logic@printing, in \HOL\ logic!of theorems},
 with the approximation
to the abstract $\vdash$ notation\index{theorem notation, in HOL logic@theorem notation, in \HOL\ logic|(}, \ml{|-}, used to indicate \ML\ type
{\small\verb%thm%} status;
the absence of \HOL\ quotation marks\index{ theorem marker, in HOL logic@\ml{"|-} (theorem marker, in \HOL\ logic)} 
 in the \ml{|-} context; and
the absence of type information following the printed term.
The session below illustrates
the use of the destructor functions:

\setcounter{sessioncount}{1}
\begin{session}\begin{verbatim}
#let th = BOOL_CASES_AX;;
th = |- !t. (t = T) \/ (t = F)

#hyp th;;
[] : term list

#concl th;;
"!t. (t = T) \/ (t = F)" : term

#type_of it;;
":bool" : type
\end{verbatim}\end{session}\index{turnstile notation|)}

\noindent In addition to the print conventions mentioned above,
the printing of theorems prints hypotheses\index{printing, in HOL logic@printing, in \HOL\ logic!of hypotheses of theorems}
 as periods (\ie\ full stops or
dots).  The function \ml{print\_all\_thm}\index{print_all_thm@\ml{print\_all\_thm}} prints theorems with
hypotheses shown in full. These points are illustrated with a
theorem inferred, for example purposes, from another axiom mentioned
in Chapter~\ref{logic}: \ml{SELECT\_AX}.

\setcounter{sessioncount}{1}
\begin{session}\begin{verbatim}
th = . |- P($@ P)

#print_all_thm th;;
P x |- P($@ P)() : void
\end{verbatim}\end{session}\index{theorem notation, in HOL logic@theorem notation, in \HOL\ logic|)}


\section{Theories}\index{theories, in HOL logic@theories, in \HOL\ logic!representation of|(}
\label{theoryfns}

It was mentioned in Chapter~\ref{logic} that a theory is a $4$-tuple

\[ {\cal T}\ =\ \langle{\sf Struc}_{\cal T},\ 
                {\sf Sig}_{\cal T},\ 
                {\sf Axioms}_{\cal T},\ 
                {\sf Theorems}_{\cal T}\rangle \]

\noindent where
\begin{myenumerate}
\item ${\sf Struc}_{\cal T}$ is
the type structure of ${\cal T}$;
\item ${\sf Sig}_{\cal T}$ is 
the signature of ${\cal T}$;
\item ${\sf Axioms}_{\cal T}$ is 
the set of axioms of ${\cal T}$;
\item ${\sf Theorems}_{\cal T}$ is the set of
theorems of ${\cal T}$.
\end{myenumerate}

Such a theory is represented  in the  \HOL\ system  as a  collection of files,
called theory files\index{theory files|(}. Each  file has  a name  of the  form $name$\ml{.th}, where
$name$ is a string supplied by the user.  Various additional pieces of
information are stored in the theory files, including the parsing status of the
constants (\ie\ whether they are infixes or binders), as well as several items
involving concepts not yet introduced: type abbreviations (see
Section~\ref{typeabbrev} for this); and which axioms are definitions, type
definitions or specifications (see Section~\ref{avra_definitional} for the last
three).

Theory files are structured hierarchically to represent sequences of
extensions of an initial theory (see Section~\ref{extensions}) called
\ml{HOL}\index{HOL@\ml{HOL}}. Each theory file making up a theory records some types, constants,
axioms and theorems, together with pointers to other theory files called its
{\it parents\/}\index{parents, of HOL theories@parents, of \HOL\ theories}.  The theory represented by such a theory file is obtained by
taking the union of all the types, constants, axioms and theorems in the file,
together with the types, constants, axioms and theorems in all the theory
files reachable by following pointers to parents. This collection of reachable
files is called the {\it ancestry\/}\index{ancestry, of HOL system theories@ancestry, of \HOL\ system theories}\index{theories, in HOL logic@theories, in \HOL\ logic!hierarchies of}
of the theory file. Axioms (including
definitions and specifications) and theorems are named in the \HOL\ system by
two strings: the name of the theory file in which they are stored, together with
a name supplied by the user\index{theory files|)}.

The data stored in a single theory file is called a {\it theory segment\/}\index{theory segments};
this is not really a logical concept, but rather a concept of the
representation of theories in the \HOL\ system. It is necessary to distinguish
theories from their constituent theory segments  because the naming of data
in theories is based on the names given to segments.  Specifically, axioms,
definitions, specifications and theorems are named\index{theories, in HOL logic@theories, in \HOL\ logic!naming of}
 by a pair of strings
$\langle thy,name \rangle$,
where $thy$ is the name of the theory segment current when the
item was declared and $name$ is a specific name supplied by the user (see the
functions \ml{new\_axiom}, \ml{new\_definition}, below). Different items
can have the same specific name if the associated segment is different.

A typical\index{HOL system@\HOL\ system!typical work in} piece of work with the \HOL\ system consists in a number of
sessions\index{sessions with HOL system@sessions, with \HOL\ system}.
In the first of these, a new theory, ${\cal T}$ say, is created by
extending existing theories with a number of definitions. The concrete result
of the session will be a theory file ${\cal T}$\ml{.th} whose contents is the
segment created during the session and whose ancestry represents the desired
logical theory.  In subsequent sessions this theory is extended by proving new
theorems that will be stored in the file ${\cal T}$\ml{.th}. The logical
meaning of these sessions is that a new extension to ${\cal T}$ is created
which replaces the old version.  Subsequent pieces of work can build on (\ie\
extend) the definitions and theorems of ${\cal T}$ by making it a parent of
new theories.

There are two modes of working with \HOL: {\it draft mode\/}\index{draft mode, in HOL system@draft mode, in \HOL\ system} and {\it proof
mode\/}\index{proof mode, in HOL system@proof mode, in \HOL\ system}.
In the former, the sets ${\sf Struc}_{\cal T}$, ${\sf Sig}_{\cal T}$
and ${\sf Axioms}_{\cal T}$ can be extended; in the latter only ${\sf
Theorems}_{\cal T}$ can be changed. In draft mode, inconsistencies can be
introduced by asserting inconsistent axioms, but in proof mode only
consistency-preserving actions (namely valid proof) can be evaluated. Draft mode is
analogous to `super user mode' in Unix, in that it gives access to dangerous
facilities. Everything that can be done in proof mode can be done in draft
mode, but not vice versa.

There is always a {\it current theory\/} which is the theory represented by
the current theory segment together with its ancestry. The name of the current
theory is returned by the \ML\ function:

\begin{boxed}\index{current_theory@\ml{current\_theory}|pin}
\begin{verbatim}
   current_theory : void -> string
\end{verbatim}\end{boxed}

Initially \HOL\ is in proof mode with current
theory called \ml{HOL}, which is described in Section~\ref{HOL-theory}\index{theories, in HOL logic@theories, in \HOL\ logic!representation of|)}.

\subsection{Primitive ML functions for creating theories}
\label{theoryprims}

The \ML\ functions for creating theories\index{theories, in HOL logic@theories, in \HOL\ logic!creation of|(} are listed below.

\begin{boxed}
\index{new_theory@\ml{new\_theory}|pin}
\begin{verbatim}
   new_theory : string -> void
\end{verbatim}\end{boxed}

\noindent \ml{new\_theory `$thy$`} can be done in both
proof\index{proof mode, in HOL system@proof mode, in \HOL\ system} and
draft\index{draft mode, in HOL system@draft mode, in \HOL\ system} modes. It
switches into draft mode for a new theory with name $thy$ and it fails if
there already exists a file $thy$\ml{.th} in the current search path. The
current theory becomes a new parent of $thy$.


\begin{boxed}
\index{new_parent@\ml{new\_parent}|pin}
\begin{verbatim}
   new_parent : string -> void
\end{verbatim}\end{boxed}


\noindent Executing \ml{new\_parent}\ $thy$ makes $thy$ into
a parent
of the current theory. Failure if:
\begin{myenumerate}
\item not in draft mode;
\item $thy$ is not a theory on the current search path;
\item there is a type in $thy$ with the same
name as a type in the current theory;
\item there is a constant in $thy$ with the same
name as a constant in the current theory.
\end{myenumerate}


\begin{boxed}
\index{new_type@\ml{new\_type}|pin}
\begin{verbatim}
   new_type : int -> string -> void
\end{verbatim}\end{boxed}


\noindent Executing \ml{new\_type}$\ n\ \ml{`\ty{op}`}$ makes \ty{op}
a new $n$-ary type operator\index{type operators, in HOL logic@type operators, in \HOL\ logic!declaration} in the current theory.
Failure if:
\begin{myenumerate}
\item not in draft mode;
\item there already exists a type operator named $\ty{op}$ in the current
theory.
\end{myenumerate}


\begin{boxed}
\index{new_constant@\ml{new\_constant}|pin}
\begin{verbatim}
   new_constant : (string # type) -> void
\end{verbatim}\end{boxed}

\noindent Executing {\small\verb%new_constant(`%}$c${\small\verb%`,%}$\sigma${\small\verb%)%} makes
$c_{\sigma'}$ a new constant\index{constants, in HOL logic@constants, in \HOL\ logic!declaration of} of the current theory,
for all $c_{\sigma'}$ where $\sigma'$ is an instance of $\sigma$.
The type $\sigma$ is
called the {\it generic type\/}\index{generic types, in HOL logic@generic types, in \HOL\ logic} of $c$. Failure if:
\begin{myenumerate}
\item not in draft mode;
\item there already exists a constant named $c$ in the current
theory.
\end{myenumerate}

\begin{boxed}
\index{new_infix@\ml{new\_infix}|pin}
\begin{verbatim}
   new_infix : (string # type) -> void
\end{verbatim}\end{boxed}


\noindent Executing \ml{new\_infix(`}$ix$\ml{`,}$\sigma$\ml{)}
declares $ix$ to be a new constant with generic type $\sigma$ and
infix status.
Failure if:
\begin{myenumerate}
\item not in draft mode;
\item there already exists a constant named $ix$ in the current theory;
\item $\sigma$ not of the form \ml{$\sigma_1$->$\sigma_2$->$\sigma_3$}.
\end{myenumerate}


\begin{boxed}
\index{new_binder@\ml{new\_binder}|pin}
\begin{verbatim}
   new_binder : (string # type) -> void
\end{verbatim}\end{boxed}


\noindent Executing \ml{new\_binder(`}$b$\ml{`,}$\sigma$\ml{)}\index{binders, in HOL logic@binders, in \HOL\ logic!declaration of}
declares $b$ to be a new constant with generic type $\sigma$ and 
binder status.
Failure if:
\begin{myenumerate}
\item not in draft mode;
\item there already exists a constant named $b$ in the current theory;
\item $\sigma$ not of the form \ml{($\sigma_1$->$\sigma_2$)->$\sigma_3$}.
\end{myenumerate}

\begin{boxed}
\index{new_axiom@\ml{new\_axiom}|pin}
\begin{verbatim}
   new_axiom : (string # term) -> thm
\end{verbatim}\end{boxed}


\noindent Executing \ml{new\_axiom(`}$name$\ml{`,}$t$\ml{)} declares the 
sequent
\ml{(\{\},$t$)} to be an axiom\index{axioms!declaration of, in HOL logic@declaration of, in \HOL\ logic} of the current theory with name $name$. 
Failure if:
\begin{myenumerate}
\item not in draft mode;
\item there is already an axiom, definition or specification 
named $name$ in the current theory segment.
\end{myenumerate}


Once a theorem has been proved, it can be saved with the function

\begin{boxed}
\index{save_thm@\ml{save\_thm}|pin}
\begin{verbatim}
   save_thm : (string # thm) -> thm
\end{verbatim}\end{boxed}

\noindent
Evaluating \ml{save\_thm(`}$name$\ml{`,}$th$\ml{)} will save the theorem\index{theorems, in HOL logic@theorems, in \HOL\ logic!saving of}\index{saving theorems}
$th$ with name $name$ in the current theory segment.

The following function is used to finish a session in  draft mode\index{draft mode, in HOL system@draft mode, in \HOL\ system}  and save the
current theory segment in a theory file on disk.

\begin{boxed}
\index{close_theory@\ml{close\_theory}|pin}
\begin{verbatim}
   close_theory : void -> void
\end{verbatim}\end{boxed}

\noindent {\bf Warning:} quitting \HOL\ without\index{exiting of HOL system@exiting of \HOL\ system} closing the session with
\ml{close\_theory} may result in the theory segment created during the session
being lost (\ie\ not saved in a theory file)!\index{theories, in HOL logic@theories, in \HOL\ logic!creation of|)}

\subsection{Functions for creating definitional extensions}\index{extension, of HOL logic@extension, of \HOL\ logic!definitional}\index{definitional extension, of HOL logic@definitional extension, of \HOL\ logic}\index{theories, in HOL logic@theories, in \HOL\ logic!extension of|(}
\label{avra_definitional}

There are three kinds of definitional extensions:
constant definitions, constant specifications and type definitions.

\subsubsection{Constant definitions}

In Section~\ref{defs} a constant definition\index{extension, of HOL logic@extension, of \HOL\ logic!by constant definition}\index{constant definition extension, of HOL logic@constant definition extension, of \HOL\ logic!ML function for@\ML\ function for|(}
over a signature $\Sigma_{\Omega}$ is defined to be
an equation, \ie\ a formula of the form $c_{\sigma}=t_{\sigma}$,
such that:
\begin{myenumerate}
\item $c$ is not the name of any constant in $\Sigma_{\Omega}$;
\item $t_{\sigma}$ is a closed term in ${\sf Terms}_{\Sigma_{\Omega}}$;
\item all the type variables occurring in $t_{\sigma}$ occur in $\sigma$.
\end{myenumerate}

In \HOL, definitions can be slightly more general than this, in that
an equation:

\[ c\ v_1\ \cdots\ v_n\ =\ t \]

\noindent is  allowed  to  be a  definition where  $v_1$, $\dots$, $v_n$ are
variable structures (\ie\ tuples of distinct variables).   Such  an equation is
logically equivalent to:

\[ c\ =\ \lambda v_1\ \cdots\ v_n.\  t \]

\noindent which is a definition in the sense of  Section~\ref{defs} if (i),
(ii) and (iii) hold.  

The following  \ML\ function  creates\index{defining mechanisms, for HOL logic@defining mechanisms, for \HOL\ logic} a  new definition in
the current theory.

\begin{boxed}
\index{new_definition@\ml{new\_definition}|pin}
\begin{verbatim}
   new_definition : (string # term) -> thm
\end{verbatim}\end{boxed}


\noindent Evaluating
 \ml{new\_definition(`}$name$\ml{`,\ "}$c\ v_1\ \cdots\ v_n\ =\ t$\ml{")},
where $c$ is not already a constant, declares the sequent
\ml{(\{\},$\lambda v_1\ \cdots\ v_n.\  t$)} to be a constant definition\index{definitions, adding to HOL logic@definitions, adding to \HOL\ logic} 
of the current theory. The name associated with the definition in
this theory is $name$. 
Failure if:
\begin{myenumerate}
\item not in draft mode;
\item there is already an axiom, definition or specification 
named $name$ in the current theory segment;
\item $c$ is already a constant in the current theory;
\item $t$ contains free variables that are not in any of
the variable structures $v_1$, $\dots$, $v_n$ (this is equivalent
to requiring $\lambda v_1\ \cdots\ v_n.\  t$ to be a closed term);
\item there is a type variable in  $v_1$, $\dots$, $v_n$ or $t$
that does not occur in the type of $c$.
\end{myenumerate}

The following two functions declare new constants that have infix\index{infixes, in HOL logic@infixes, in \HOL\ logic!declaration of}\index{infixes, in HOL logic@infixes, in \HOL\ logic} or binder
status. The failure conditions are the same as for \ml{new\_definition}, 
with the
additional conditions that the constants being declared must be types of
the appropriate form (\ml{$\sigma_1$->$\sigma_2$->$\sigma_3$} for infixes and
\ml{($\sigma_1$->$\sigma_2$)->$\sigma_3$} for binders).


\begin{boxed}
\index{new_infix_definition@\ml{new\_infix\_definition}|pin}
\index{new_binder_definition@\ml{new\_binder\_definition}|pin}
\begin{verbatim}
   new_infix_definition  : (string # term) -> thm
   new_binder_definition : (string # term) -> thm
\end{verbatim}\end{boxed}

\noindent Note that until an infix or binder declaration has been processed the
constant being defined will not have its special status.\index{parsing, of HOL logic@parsing, of \HOL\ logic!of constants, before definition} It is therefore
necessary to use
the constant in normal prefix position when making the definition\index{defining mechanisms, for HOL logic@defining mechanisms, for \HOL\ logic}. For example,

\begin{hol}
{\small\verb%   new_infix_definition(`%}$ix${\small\verb%_DEF`, "%}$m$ $ix$ $n${\small\verb% = ... ")%}
\end{hol}

\noindent will not work, as at the time when the quotation is parsed, \ml{ix}
does not have infix status and hence \ml{m ix n} will parse with \ml{m} as the
function. The definition must thus have the form:

\begin{hol}
{\small\verb%   new_infix_definition(`%}$ix${\small\verb%_DEF`, "%}$ix$ $m$ $n${\small\verb% = ... ")%}
\end{hol}

\noindent Only after this has been processed will $ix$ be an infix. It is a
common practice among \HOL\ users to write a {\small\verb%$%}\index{ escape, in HOL logic parser@{\small\verb+$+} (escape, in \HOL\ logic parser)}\index{declared constants, in HOL logic@declared constants, in \HOL\ logic}
before
the constant being defined as an infix or binder
to indicate that after the definition is made, it will have a special
syntactic status; \ie\ to write:

\begin{hol}
{\small\verb%   new_infix_definition(`%}$ix${\small\verb%_DEF`, "$%}$ix$ $m$ $n${\small\verb% = ... ")%}
\end{hol}

\noindent and similarly with \ml{new\_binder\_definition}. This use of
{\small\verb%$%} is not necessary; but after the definition has been
made {\small\verb%$%} must, of course, 
 be used if the syntactic status needs to be suppressed.
\index{constant definition extension, of HOL logic@constant definition extension, of \HOL\ logic!ML function for@\ML\ function for|)}

\subsubsection{Constant specifications}
\label{conspec}

\index{specification of constants, in HOL logic@specification of constants, in \HOL\ logic|(}
\index{extension, of HOL logic@extension, of \HOL\ logic!by constant specification}
In Section~\ref{specs} a constant specification\index{constant specification extension, of HOL logic@constant specification extension, of \HOL\ logic!ML function for@\ML\ function for} for a theory ${\cal T}$
is defined to be a pair:

\[ \langle(c_1,\ldots,c_n),\ \lquant{{x_1}_{\sigma_1}
\cdots {x_n}_{\sigma_n}}t_{\ty{bool}}\rangle \]

\noindent such that:

\begin{myenumerate}
\item $c_1$, $\dots$, $c_n$ are distinct names that
are not the names of any constants in ${\sf Sig}_{\cal T}$.
\item $\lquant{{x_1}_{\sigma_1}
\cdots {x_n}_{\sigma_n}}t_{\ty{bool}}\ \in\ {\sf Terms}_{\cal T}$.
\item $tyvars(\lquant{{x_1}_{\sigma_1}
\cdots {x_n}_{\sigma_n}}t_{\ty{bool}})\ \subseteq\ tyvars(\sigma_i)$ for
$1\leq i\leq n$.
\item $\equant{{x_1}_{\sigma_1}\ \cdots\ {x_n}_{\sigma_n}}t
\ \in\ {\sf Theorems}_{\cal T}$.
\end{myenumerate}

The following \ML\ function is used to make constant specifications in
the \HOL\ system.

\begin{boxed}
\index{new_specification@\ml{new\_specification}|pin}
\begin{verbatim}
   new_specification : string -> ((string#string)list) -> thm -> thm
\end{verbatim}\end{boxed}

Evaluating:

\medskip

\begin{tabular}{l}
   \ml{new\_specification}\\
\ \ml{`}$name$\ml{`}\\ 
\ \ml{[`}$flag_1$\ml{`,`}$c_1$\ml{`;\ }$\ldots$\ml{\ ;\ `}$flag_n$\ml{`,`}$c_n$\ml{`]}\\
\ \ml{|-\ ?}$x_1\ \cdots\ x_n$\ml{.}\  $t$\ml{[}$x_1$\ml{,}$\ \ldots\
$\ml{,}$x_n$\ml{]}\\
\end{tabular}

\medskip

\noindent simultaneously  introduces  new constants  named $c_1$, $\dots$,
$c_n$ satisfying the property:



\[ \ml{|- }t\ml{[}c_1\ml{,}\ \ldots\ \ml{,}c_n\ml{]} \]


\noindent If \ml{`}$flag_i$\ml{`} is \ml{`constant`} 
then $c_i$ is declared an ordinary constant, if it is
\ml{`infix`} then $c_i$ is declared an infix and if it is 
\ml{`binder`}\index{binders, in HOL logic@binders, in \HOL\ logic} then $\ml{c}_i$ is declared
a binder.  Any other value of flag causes an error. This theorem is stored,
with name $name$, as a definition in the current theory segment. A call to
\ml{new\_specification} fails if:

\begin{myenumerate}
\item not in draft mode;
\item there is already an axiom, definition or specification 
named $name$ in the current theory segment;
\item the theorem argument has a non-empty assumption list;
\item there are free variables in the theorem argument;
\item $c_1$, $\dots$, $c_n$ are not distinct variables;
\item some $c_i$ is already a constant in the current theory;
\item some $c_i$ is not an allowed name for a constant;
\item some $flag_i$ is not either \ml{constant}, \ml{infix}
or \ml{binder};
\item the type of $c_i$ is not suitable for a constant with the syntactic
status specified by $flag_i$;
\item the type of some $c_i$ does not contain all the type
variables which occur in the term
{\small\verb%\%}$x_1\ \cdots\ x_n$\ml{.}\  $t$\ml{[}$x_1$\ml{,}$\ \ldots\
$\ml{,}$x_n$\ml{]}.
\end{myenumerate}

% =====================================================================
% Following section deleted [TFM 90.12.01]		

% Specifications with assumptions\index{constant specifications, in HOL
% logic@constant specifications, in \HOL\ logic!with
% assumptions|(}\index{assumptions!in constant specifications} are sometimes
% convenient. Rather than generalize the primitive mechanism to support this,
% \HOL\ achieves the same effect by providing a way of encoding specifications
% with assumptions as specifications without them.  This encoding uses the 
% infix constant
% \ml{IS\_ASSUMPTION\_OF}\index{IS_ASSUMPTION_OF@\ml{IS\_ASSUMPTION\_OF}|(},
% which has type \ml{bool->bool->bool} and is 
% defined (in the theory \ml{bool})
% to be equal to the primitive constant \ml{==>}.  A theorem of the form
% $t_1$\ml{,}$t_2$\ml{,}$\ldots$\ml{,}$t_n$\ml{\ |-\ }$t$ is logically
% equivalent to the following theorem without assumptions:

% \[\ml{|-\ }  \begin{array}[t]{@{}l}
% 	  t_1\ \ml{IS\_ASSUMPTION\_OF}\\
%           t_2\ \ml{IS\_ASSUMPTION\_OF}\\
%           \qquad\qquad \vdots\\
%           t_n\ \ml{IS\_ASSUMPTION\_OF}\ t\\
% \end{array} \]

% If the flag \ml{undisch\_defs} is \ml{true} (the default), then a
% specification that encodes a theorem with assumptions using
% \ml{IS\_ASSUMPTION\_OF} will be returned by the \ML\ definition retrieving
% functions (\ie\ \ml{definition} and \ml{definitions}) as a theorem with
% assumptions. For example, specifying \ml{c} by:

% \begin{hol}\begin{verbatim}
%    |- ?x. (?x.t[x]) IS_ASSUMPTION_OF t[x]
% \end{verbatim}\end{hol}

% \noindent will result in \ml{c} being defined\index{defining mechanisms, for
% HOL logic@defining mechanisms, for \HOL\ logic} by:

% \begin{hol}\begin{verbatim}
%    ?x.t[x] |- t[c]
% \end{verbatim}\end{hol}

% \noindent(although, in fact, \ml{|- (?x.t[x]) IS\_ASSUMPTION\_OF t[c]}, is
% what is actually stored). Note that the constant \ml{==>} could not be used
% instead of \ml{IS\_ASSUMPTION\_OF}, because there would then be no way of
% preventing the specification:


% \begin{hol}\begin{verbatim}
%    |- ?x.t[x] ==> t[c]
% \end{verbatim}\end{hol}

% \noindent being interpreted as the specification:

% \begin{hol}\begin{verbatim}
%    ?x.t[x] |- t[c]
% \end{verbatim}\end{hol}

% \noindent These two specifications are logically equivalent, but there may be
% pragmatic reasons for wanting one form or the other.  \index{constant
% specifications, in HOL logic@constant specifications, in \HOL\ logic!with
% assumptions|)} \index{extension, of HOL logic@extension, of \HOL\ logic!by
% constant specification|)}\index{constant specification extension, of HOL
% logic@constant specification extension, of \HOL\ logic!ML function for@\ML\
% function for|)} \index{IS_ASSUMPTION_OF@\ml{IS\_ASSUMPTION\_OF}|)}

\subsubsection{Type definitions}\index{extension, of HOL logic@extension, of \HOL\ logic!by type definition|(}
\label{type-defs}\index{type definitions, in HOL logic@type definitions, in \HOL\ logic|(}

In Section~\ref{tydefs} it is explained that
defining\index{type definitions, in HOL logic@type definitions, in \HOL\ logic!introduction of}\index{type definition extension, in HOL logic@type definition extension, in \HOL\ logic!ML function for@\ML\ function for|(}
a new type $(\alpha_1,\ldots,\alpha_n)\ty{op}$ in a theory ${\cal T}$ consists
of introducing $\ty{op}$ as a new $n$-ary type operator and 

\[\turn \equant{f_{(\alpha_1,\ldots,\alpha_n)\ty{op}\fun\sigma}}\TyDef\ p\ f\]

\noindent as a new axiom, where $p$ is a predicate
characterizing\index{characteristic predicate, of type definitions} a
non-empty subset of an existing type $\sigma$.  Formally, a type definition
for a theory ${\cal T}$ is a $3$-tuple 

\[ \langle \sigma,\ (\alpha_1,\ldots,\alpha_n)\ty{op},
    \ p_{\sigma\fun\ty{bool}}\rangle \]

\noindent where:

\begin{myenumerate}
\item $\sigma\in{\sf Types}_{\cal T}$  and
$tyvars(\sigma)\in\{\alpha_1, \ldots , \alpha_n\}$.
\item \ty{op} is not the name of a type constant in ${\sf Struc}_{\cal T}$.
\item $p\in{\sf Terms}_{\cal T}$ is a closed term of
type $\sigma\fun\ty{bool}$  and
$tyvars(p)\subseteq\{\alpha_1, \ldots , \alpha_n\}$.
\item $\equant{x_{\sigma}}p\ x \ \subseteq\ {\sf Theorems}_{\cal T}$.
\end{myenumerate}

The following \ML\ function makes a type definition in the \HOL\ system.

\begin{boxed}
\index{new_type_definition@\ml{new\_type\_definition}|pin}
\begin{verbatim}
   new_type_definition : (string # term # thm) -> thm
\end{verbatim}\end{boxed}

\noindent If $t$ is a term of type
$\sigma$\ml{->bool} containing $n$ distinct type variables, then
evaluating:

{\def\op{{\normalsize\sl op}}
\begin{hol}\begin{alltt}
   new_type_definition(`{\op}`, \m{t}, |- ?\m{x}.\m{\:t \;x}) 
\end{alltt}\end{hol}}

\noindent results in \ty{op} being declared as a new $n$-ary type operator
characterized by the definitional\index{definitional axioms}\index{type operators, in HOL logic@type operators, in \HOL\ logic!definitional axioms for} axiom:

\begin{hol}\begin{alltt}
   |- ?rep. TYPE\_DEFINITION \m{t} rep
\end{alltt}\end{hol}

\noindent which is stored as a definition with the automatically 
generated name
\ty{op}\ml{\_TY\_DEF}.\index{TY_DEF@$\ldots$\ml{\_TY\_DEF}}\footnote{In 
previous versions of HOL, type definitions 
were stored as axioms rather than definitions.} The constant 
\ml{TYPE\_DEFINITION}\index{TYPE_DEFINITION@\ml{TYPE\_DEFINITION}} 
is defined in the theory \ml{bool} by:

\begin{hol}\begin{verbatim}
   |- TYPE_DEFINITION (P:*->bool) (rep:**->*) =
       (!x' x''. (rep x' = rep x'') ==> (x' = x'')) /\	
       (!x. P x = (?x'. x = rep x'))
\end{verbatim}\end{hol}

\noindent Executing \ml{new\_type\_definition(`\ty{op}`,\ }$t$\ml{,\ 
|- ?}$x$\ml{.}\ $t\ x$\ml{)} fails if:
\begin{myenumerate}
\item not in draft mode;
\item $\ty{op}$ is already the name of a type or type operator 
in the current theory;
\item there already exists a constant definition, constant specification,
type definition or axiom named  \ty{op}\ml{\_TY\_DEF} in the current theory; 
\item $t$ does not have a type of the form $\sigma$\ml{->bool}.
\end{myenumerate}
\index{extension, of HOL logic@extension, of \HOL\ logic!by type definition|)}
\index{theories, in HOL logic@theories, in \HOL\ logic!extension of|)}\index{type definition extension, in HOL logic@type definition extension, in \HOL\ logic!ML function for@\ML\ function for|)}\index{type definitions, in HOL logic@type definitions, in \HOL\ logic|)}

\subsubsection{Defining bijections}
\index{type definitions, in HOL logic@type definitions, in \HOL\ logic!defining bijections for|(}

The result of a type definition using \ml{new\_type\_definition} is a theorem
which asserts only the {\it existence\/} of a
bijection\index{bijection of types, in HOL logic@bijection of types, in \HOL\ logic} 
from the type it defines to the corresponding subset of an existing type.  To
introduce constants that in fact denote such a bijection and its inverse, the
following \ML\ function is provided:

\begin{boxed}
\index{define_new_type_bijections@\ml{define\_new\_type\_bijections}|pin}
\begin{verbatim}
   define_new_type_bijections : string -> string -> string -> thm -> thm
\end{verbatim}\end{boxed}

\noindent This function takes three string arguments and a theorem argument.
The theorem argument must be a definitional axiom of the form returned by
\ml{new\_type\_definition}.  The first string argument is the name under which
the constant definition (a constant specification, in fact) made by
{\small\verb!define_new_type_bijections!} will be stored in the current theory
segment, and the second and third string arguments are user-specified names for
the two constants that are to be defined. These constants are defined so as to
denote mutually inverse bijections between the defined type, whose definition
is given by the supplied theorem, and the representing type of this defined
type.

Evaluating:

\medskip
{\def\op{{\normalsize\sl op}}
\begin{hol}\begin{alltt}
   define\_new\_type\_bijections `\m{name}` `\m{abs}` `\m{rep}` 
           |- ?rep:newty->ty. TYPE\_DEFINITION \m{P} rep
\end{alltt}\end{hol}}

\medskip

\noindent automatically defines two new constants
\m{abs}{\small\verb!:ty->newty!} and \m{rep}{\small\verb!:ty->newty!} 
such that:

{\def\bk{\char'134}
\begin{hol}\begin{alltt}
   |- (!a. \m{abs}(\m{rep} a) = a) /\bk (!r. \m{P} r = (\m{rep}(\m{abs} r) = r))
\end{alltt}\end{hol}}

\noindent This theorem, which is the defining property for the constants
\m{abs} and \m{rep}, is stored under the name `\m{name}` in the current theory
segment.  It is also the value returned by \ml{define\_new\_type\_bijections}.
The theorem states that \m{abs} is the left inverse of \m{rep} and---for
values satisfying \m{P}---that \m{rep} is the left inverse of \m{abs}.

A call to 
\ml{define\_new\_type\_bijections \m{name} \m{abs} \m{rep} \m{th}}
fails if:

\begin{myenumerate}
\item not in draft mode;
\item either $abs$ or $rep$ is already the name of a constant in
the current theory;
\item there already exists a constant definition, constant specification,
type definition or axiom named  \m{name} in the current theory; 
\item $th$ is not a theorem of the form returned by
\ml{new\_type\_definition}.
\end{myenumerate}%
\index{type definitions, in HOL logic@type definitions, in \HOL\ logic!defining bijections for|)}

\subsubsection{Properties of type bijections}
\index{type definitions, in HOL logic@type definitions, in \HOL\ logic!properties of bijections for|(}

The following \ML\ functions are provided for proving that the bijections
introduced by \ml{define\_new\_type\_isomorphisms} are injective (one-to-one)
and surjective (onto):

\begin{boxed}
\index{prove_rep_fn_one_one@\ml{prove\_rep\_fn\_one\_one}|pin}
\index{prove_rep_fn_onto@\ml{prove\_rep\_fn\_onto}|pin}
\index{prove_abs_fn_one_one@\ml{prove\_abs\_fn\_one\_one}|pin}
\index{prove_abs_fn_onto@\ml{prove\_abs\_fn\_onto}|pin}
\begin{verbatim}
   prove_rep_fn_one_one : thm -> thm
   prove_rep_fn_onto    : thm -> thm
   prove_abs_fn_one_one : thm -> thm
   prove_abs_fn_onto    : thm -> thm
\end{verbatim}\end{boxed}

\noindent The theorem argument to each of these functions must be a theorem 
of the form returned by \ml{define\_new\_type\_bijections}:

{\def\bk{\char'134}
\begin{hol}\begin{alltt}
   |- (!a. \m{abs}(\m{rep} a) = a) /\bk (!r. \m{P} r = (\m{rep}(\m{abs} r) = r))
\end{alltt}\end{hol}}

\noindent If \m{th} is a theorem of this form, then evaluating
\ml{prove\_rep\_fn\_one\_one \m{th}} proves that the function \m{rep} is
one-to-one, and returns the theorem:

\begin{hol}\begin{alltt}
   |- !a a'. (\m{rep} a = \m{rep} a') = (a = a')
\end{alltt}\end{hol}

\noindent Likewise, \ml{prove\_rep\_fn\_onto \m{th}} proves that \m{rep} is
onto the set of values that satisfy \m{P}:

{\def\bk{\char'134}
\begin{hol}\begin{alltt}
   |- !r. \m{P} r = (?a. r = \m{rep} a)
\end{alltt}\end{hol}}

\noindent Evaluating \ml{prove\_abs\_fn\_one\_one \m{th}} proves that \m{abs}
is one-to-one for values that satisfy \m{P}, and returns the theorem:

{\def\bk{\char'134}
\begin{hol}\begin{alltt}
   |- !r r'. \m{P} r ==> \m{P} r' ==> ((\m{abs} r = \m{abs} r') = (r = r'))
\end{alltt}\end{hol}}

\noindent And evaluating \ml{prove\_abs\_fn\_onto \m{th}} proves that \m{abs}
is onto, returning the theorem:

{\def\bk{\char'134}
\begin{hol}\begin{alltt}
   |- !a. ?r. (a = \m{abs} r) /\bk \m{P} r
\end{alltt}\end{hol}}

\noindent All four functions will fail if applied to any theorem that does not
have the form of a theorem returned by \ml{define\_new\_type\_bijections}.
None of these functions saves anything on the current theory file. In fact, it
should usually be unnecessary to save the results proved by these functions,
since they can be generated quickly whenever required from the theorem returned
by \ml{define\_new\_type\_bijections}, which is itself saved.  Of course,
within any given session, one would bind results to \ML\ identifiers.

\index{type definitions, in HOL logic@type definitions, in \HOL\ logic!properties of bijections for|)}

\subsection{Primitive ML function for accessing theories}

\index{theories, in HOL logic@theories, in \HOL\ logic!functions for accessing|(}
\index{axioms!retrieval of, in HOL system@retrieval of, in \HOL\ system|(}
The arguments of \ML\ type {\small\verb%string%} to {\small\verb%new_axiom%},
{\small\verb%new_definition%}
\etc\ are the names of the corresponding axioms and definitions. These
names are used when accessing theories with the functions
{\small\verb%axiom%}, {\small\verb%definition%}, \etc, described below.
%The various functions for setting up theories are illustrated in the
%example session in Section~\ref{example}.



A theory with no descendants\index{theories, in HOL logic@theories, in \HOL\ logic!hierarchies of}
can be extended by adding new parents, types,
constants, axioms and definitions. Theories that are already the parents of
other theories cannot be extended in this way.\footnote{It 
would be difficult
to implement the necessary checks to ensure that added types,
constants \etc\ did not invalidate declarations in the descendant theories.}
When a new theory is being created or an existing one extended it is necessary
to be in draft mode.\index{draft mode, in HOL system@draft mode, in \HOL\ system}
In proof mode\index{proof mode, in HOL system@proof mode, in \HOL\ system} the
functions with prefix `{\small\verb%new_%}'\index{new_@\ml{new\_}$\ldots$}
listed above are not available.  

The functions for entering an already existing theory in either draft mode
or proof mode are, respectively:


\begin{boxed}\index{extend_theory@\ml{extend\_theory}|pin}
\index{load_theory@\ml{load\_theory}|pin}
\begin{verbatim}
   extend_theory : string -> void
   load_theory   : string -> void
\end{verbatim}\end{boxed}

The function \ml{close\_theory}\index{close_theory@\ml{close\_theory}}
 (see Section~\ref{theoryprims}) is used 
to finish a session and write all new declarations to the theory file.

There are various functions for loading the contents of theory files:

\begin{boxed}
\index{parents@\ml{parents}|pin}
\index{types@\ml{types}|pin}
\index{constants@\ml{constants}|pin}
\index{infixes@\ml{infixes}|pin}
\index{binders@\ml{binders}|pin}
\index{axioms@\ml{axioms}|pin}
\index{definitions@\ml{definitions}|pin}
\index{theorems@\ml{theorems}|pin}
\begin{verbatim}
   parents     : string -> string list
   types       : string -> (int # string) list
   constants   : string -> term list
   infixes     : string -> term list
   binders     : string -> term list
   axioms      : string -> (string # thm) list
   definitions : string -> (string # thm) list
   theorems    : string -> (string # thm) list
\end{verbatim}\end{boxed}

\noindent The first argument is the name of a theory (which must be in the
ancestry of the current theory segment); the result is a list of the
components of the theory. The name of the current theory can be abbreviated by
\ml{`-`}.\index{ abbreviation, of HOL theory part names@\ml{-}
(abbreviation, of \HOL\ theory part names)} For example, \ml{parents `-`} returns the parents of the current
theory.

In the case of \ml{types} a list of arity-name pairs is returned; in the
case of  \ml{axioms}, \ml{definitions} or \ml{theorems} a list 
of string-theorem
pairs is returned, where the string is the name of the theorem representing the
axiom, definition or theorem that was supplied by the user. Note that constant
specifications and type definitions are both retrieved using the function
\ml{definitions}.



Individual axioms, definitions and theorems can be read (from the current or
ancestor theories) using the following \ML\ functions:



\begin{boxed}
\index{axiom@\ml{axiom}|pin}
\index{definition@\ml{definition}|pin}
\index{theorem@\ml{theorem}|pin}
\begin{verbatim}
   axiom      : string -> string -> thm
   definition : string -> string -> thm
   theorem    : string -> string -> thm
\end{verbatim}\end{boxed}

\noindent The  first  argument  is  the  theory (\ml{`-`}  can be  used for the
current theory); the second argument is  the user  supplied name  of the axiom,
definition or theorem in the theory.

Theories can be printed using the function
{\small\verb%print_theory%}\index{printing, in HOL logic@printing, in \HOL\ logic!of theories}\index{print_theory@\ml{print\_theory}}, 
which takes a theory name and then
prints out the named theory in a readable format.\index{axioms!retrieval of, in HOL system@retrieval of, in \HOL\ system|)}\index{theories, in HOL logic@theories, in \HOL\ logic!functions for accessing|)}


\subsection{The theory {\tt HOL}}
\label{HOL-theory}

%The types and constants in the built-in theories are listed here.  The axioms,
%definitions and pre-proved theorems are not listed; they can be found in
%Section~\ref{preproved-theories}.  

\index{axioms!primitive, of HOL logic@primitive, of \HOL\ logic|(}
At start-up,  the  initial  theory  for  users  of  the \HOL\  system is called
\ml{HOL}\index{HOL@\ml{HOL}}, which is constructed when the \HOL\ system is made.   The ancestry of
this theory is quite complicated and reflects, to  some extent,  the history of
\HOL\ as  it  evolved  from  \LCF.\index{LCF@\LCF}    This ancestry, which
is described  in detail in
Section~\ref{HOL-ancestry},  contains two important  theories: \ml{bool}\index{bool, the HOL theory@\ml{bool}, the \HOL\ theory} and
\ml{ind}. These define the primitive logical basis of the \HOL\ logic.

\subsubsection{The theory {\tt bool}}
\label{boolthy}

The theory {\small\verb%bool%} introduces the type
 {\small\verb%bool%} and
contains four of the five axioms\index{axioms!in bool theory@in \ml{bool} theory}
for higher order logic (the fifth axiom is
in the theory {\small\verb%ind%}).  These axioms, together with the rules
of inference described later in Section~\ref{rules}, constitute the core of the
\HOL\ logic.  Because of the way the \HOL\ system evolved from
\LCF,\index{LCF@\LCF}\footnote{To simplify the porting of the LCF theorem-proving
tools to the HOL system, the HOL logic was made as like PP$\lambda$ (the logic
built-in to LCF) as possible.} the particular axiomatization\index{axioms!non-primitive, of HOL logic@non-primitive, of \HOL\ logic} of
higher order logic it uses differs from the classical
axiomatization due to Church\index{Church, A.} \cite{Church}.  The biggest difference is that
in Church's formulation type variables\index{type variables, in HOL logic@type variables, in \HOL\ logic!differences from classical} are in the meta-language, whereas
in the \HOL\ logic they are part of the object language.

There are three primitive constants\index{constants, in HOL logic@constants, in \HOL\ logic!primitive logical}\index{primitive constants, of HOL logic@primitive constants, of \HOL\ logic}
 in the theory {\small\verb%bool%}\index{bool, the type in HOL logic@\ml{bool}, the type in \HOL\ logic}:
{\small\verb%=%}\index{ equality, in HOL logic@\ml{=} (equality, in \HOL\ logic)}\index{equality, in HOL logic@equality, in \HOL\ logic}
 (equality, an infix), {\small\verb%==>%}\index{ implication, in HOL logic@{\small\verb+==>+} (implication, in \HOL\ logic)} (implication, an
infix) and {\small\verb%@%}\index{ choice function, in HOL logic@{\small\verb+"@+} (choice function, in \HOL\ logic)}\index{choice operator, in HOL logic@choice operator, in \HOL\ logic} (choice, a binder).  Equality\index{equality, in HOL logic@equality, in \HOL\ logic}\index{implication, in HOL logic@implication, in \HOL\ logic}
 and implication
are standard predicate calculus notions, but choice is more exotic:
if $t$ is a term having type $\sigma${\small\verb%->bool%}, 
then {\small\verb%@x.%}$t${\small\verb% x%} (or, equivalently,
{\small\verb%$@%}$t$) denotes {\it some\/} member of the set whose
characteristic\index{characteristic predicate, of type definitions}
 function is $t$. If the set is empty, then
{\small\verb%@x.%}$t${\small\verb% x%} denotes an arbitrary member of the
set denoted by $\sigma$. The constant {\small\verb%@%} is a higher order
version of Hilbert's\index{Hilbert, D.}\index{epsilon operator}
 $\hilbert$-operator; it is related to the constant
$\iota$ in Church's formulation of higher order logic. For more details,
see Church's\index{Church, A.} original paper \cite{Church}, Leisenring's\index{Leisenring, A.} book 
on Hilbert's $\hilbert$-symbol \cite{Leisenring}, or
Andrews' textbook on type theory \cite{Andrews}.


The logical constants\index{logical constants, in HOL logic@logical constants, in \HOL\ logic} {\small\verb%T%}\index{truth values, in HOL logic@truth values, in \HOL\ logic!constants for}\index{T@\ml{T}!defined in terms of primitives} (truth), {\small\verb%F%}\index{F@\ml{F}!defined in terms of primitives} (falsity),
{\small\verb%~%} (negation)\index{ negation, in HOL logic@{\small\verb+~+} (negation, in \HOL\ logic)}, {\small\verb%/\%} (conjunction)\index{ conjunction, in HOL logic@{\small\verb+/\+} (conjunction, in \HOL\ logic)}\index{conjunction, in HOL logic@conjunction, in \HOL\ logic!defined in terms of primitives},
{\small\verb%\/%} (disjunction)\index{ disjunction, in HOL logic@{\small\verb+\/+} (disjunction, in \HOL\ logic)}\index{disjunction, in HOL logic@disjunction, in \HOL\ logic!defined in terms of primitives}, {\small\verb%!%} (universal
quantification)\index{ universal quantifier, in HOL logic@{\small\verb+"!+} (universal quantifier, in \HOL\ logic)}\index{universal quantifier, in HOL logic@universal quantifier, in \HOL\ logic!defined in terms of primitives}, {\small\verb%?%} (existential quantification)\index{ existential quantifier, in HOL logic@{\small\verb+?+} (existential quantifier, in \HOL\ logic)}\index{existential quantifier, in HOL logic@existential quantifier, in \HOL\ logic!defined in terms of primitives}
and {\small\verb%?!%} (unique existence quantifier)\index{ exists unique, in HOL logic@{\small\verb+?"!+} (exists unique, in \HOL\ logic)}\index{exists unique, in HOL logic@exists unique, in \HOL\ logic!defined in terms of primitives}
 can all
be defined in terms of equality\index{equality, in HOL logic@equality, in \HOL\ logic}, implication and choice.  The definitions
listed below are fairly standard; each one is preceded by its \ML\ name.
(Later definitions sometimes use earlier ones.) 


\begin{hol}
\index{truth values, in HOL logic@truth values, in \HOL\ logic!definition of}
\index{T_DEF@\ml{T\_DEF}}
\index{T@\ml{T}!definitional axiom for}
\index{disjunction, in HOL logic@disjunction, in \HOL\ logic!definitional axiom for}
\index{conjunction, in HOL logic@conjunction, in \HOL\ logic!definitional axiom for}
\index{iff, in HOL logic@iff, in \HOL\ logic!definitional axiom for}
\index{negation, in HOL logic@negation, in \HOL\ logic!definitional axiom for}
\index{exists unique, in HOL logic@exists unique, in \HOL\ logic}
\index{F@\ml{F}!axiom for}
\index{F@\ml{F}!definitional axiom for}
\index{ exists unique, in HOL logic@{\small\verb+?"!+} (exists unique, in \HOL\ logic)}
\index{T_DEF@\ml{T\_DEF}}
\index{FORALL_DEF@\ml{FORALL\_DEF}}
\index{EXISTS_DEF@\ml{EXISTS\_DEF}}
\index{AND_DEF@\ml{AND\_DEF}}
\index{OR_DEF@\ml{OR\_DEF}}
\index{F_DEF@\ml{F\_DEF}}
\index{NOT_DEF@\ml{NOT\_DEF}}
\index{EXISTS_UNIQUE_DEF@\ml{EXISTS\_UNIQUE\_DEF}}
\index{conjunction, in HOL logic@conjunction, in \HOL\ logic!definitional axiom for}
\index{disjunction, in HOL logic@disjunction, in \HOL\ logic!definitional axiom for}
\index{equality, in HOL logic@equality, in \HOL\ logic!primitive axiom for}
\index{existential quantifier, in HOL logic@existential quantifier, in \HOL\ logic!definitional axiom for}
\index{universal quantifier, in HOL logic@universal quantifier, in \HOL\ logic!definitional axiom for}
\index{exists unique, in HOL logic@exists unique, in \HOL\ logic!definitional axiom for}
\begin{verbatim}
   T_DEF              |- T   = ((\x:bool. x)=(\x. x))

   FORALL_DEF         |- $!  = \P:*->bool. P=(\x. T)

   EXISTS_DEF         |- $?  = \P:*->bool. P($@ P)

   AND_DEF            |- $/\ = \t1 t2. !t. (t1 ==> t2 ==> t) ==> t

   OR_DEF             |- $\/ = \t1 t2. !t. (t1 ==> t) ==> (t2 ==> t) ==> t

   F_DEF              |- F   = !t. t

   NOT_DEF            |- $~  = \t. t ==> F

   EXISTS_UNIQUE_DEF  |- $?! = (\P. $? P /\ (!x y. P x /\ P y ==> (x = y)))
\end{verbatim}\end{hol}


There are four\index{universal quantifier, in HOL logic@universal quantifier, in \HOL\ logic!in four primitive axioms} axioms in the theory {\small\verb%bool%}\index{bool, the HOL theory@\ml{bool}, the \HOL\ theory}:

\begin{hol}
\index{BOOL_CASES_AX@\ml{BOOL\_CASES\_AX}}
\index{IMP_ANTISYM_AX@\ml{IMP\_ANTISYM\_AX}}
\index{ETA_AX@\ml{ETA\_AX}}
\index{SELECT_AX@\ml{SELECT\_AX}}
\index{implication, in HOL logic@implication, in \HOL\ logic!primitive axiom for}
\index{ choice function, in HOL logic@{\small\verb+"@+} (choice function, in \HOL\ logic)}
\index{choice axiom}
\index{choice operator, in HOL logic@choice operator, in \HOL\ logic!primitive axiom for}
\begin{verbatim}
   BOOL_CASES_AX   |- !t. (t = T) \/ (t = F)

   IMP_ANTISYM_AX  |- !t1 t2. (t1 ==> t2) ==> (t2 ==> t1) ==> (t1 = t2)

   ETA_AX          |- !t. (\x. t x) = t

   SELECT_AX       |- !P:*->bool x. P x ==> P($@ P)
\end{verbatim}\end{hol}

\noindent
The fifth and last axiom of the \HOL\ logic is the Axiom of
Infinity;\index{axiom of infinity} this
is in the theory {\small\verb%ind%} described in Section~\ref{ind}.  

The theory {\small\verb%bool%} also supplies the definitions of a number of
useful constants. The constant {\small\verb%LET%}\index{let-terms, in HOL logic@\ml{let}-terms, in \HOL\ logic!constant for} is used in representing terms
containing local variable bindings (\ie\
{\small\verb%let%}-terms\index{let-terms, in HOL logic@\ml{let}-terms, in \HOL\ logic!definitional axiom for}, as discussed in Section~\ref{let}), and the
constant {\small\verb%COND%} is used in representing conditionals.  Both
constants are defined in the theory \ml{bool}, and have the following
definitions:

\begin{hol}
\index{LET_DEF@\ml{LET\_DEF}}
\index{COND_DEF@\ml{COND\_DEF}}
\index{COND@\ml{COND}}
\index{LET@\ml{LET}}
\index{conditional predicate, in HOL logic@conditional predicate, in \HOL\ logic!definitional axiom for}
\index{conditionals, in HOL logic@conditionals, in \HOL\ logic}
\begin{verbatim}
   LET_DEF      |- LET       = \f x. f x

   COND_DEF     |- COND      = \t t1 t2.@x.((t=T)==>(x=t1))/\((t=F)==>(x=t2))
\end{verbatim}\end{hol}

\noindent The theory \ml{bool} also contains the definitions of the constants
{\small\verb!RES_FORALL!}, {\small\verb!RES_EXISTS!},
{\small\verb!RES_SELECT!}, {\small\verb!ARB!} and {\small\verb!RES_ABSTRACT!},
which are used to support restricted
quantification\index{quantifiers!restricted} in the \HOL\ logic (see
Section~\ref{res-quant}).  The definitions are:

\begin{hol}
\index{RES_FORALL@\ml{RES\_FORALL}}
\index{RES_EXISTS@\ml{RES\_EXISTS}}
\index{RES_SELECT@\ml{RES\_SELECT}}
\index{RES_ABSTRACT@\ml{RES\_ABSTRACT}}
\index{ARB@\ml{ARB}}
\begin{verbatim}
   RES_FORALL   |- !P B. RES_FORALL P B = (!x. P x ==> B x)

   RES_EXISTS   |- !P B. RES_EXISTS P B = (?x. P x /\ B x)

   RES_SELECT   |- !P B. RES_SELECT P B = (@x. P x /\ B x)

   ARB          |- ARB = (@x. T)

   RES_ABSTRACT |- !P B. RES_ABSTRACT P B = (\x. (P x => B x | ARB))
\end{verbatim}\end{hol}

\noindent The theory \ml{bool} also contains the definitions of
the constants {\small\verb%ONE_ONE%} and
{\small\verb%ONTO%}, which are used in stating the Axiom of Infinity\index{axioms!non-primitive, of HOL logic@non-primitive, of \HOL\ logic}\index{axiom of infinity} (see Section~\ref{ind})\index{specification of constants, in HOL logic@specification of constants, in \HOL\ logic|)}. The definitions are:

\begin{hol}
\index{ONE_ONE_DEF@\ml{ONE\_ONE\_DEF}}
\index{ONTO_DEF@\ml{ONTO\_DEF}}
\index{one-to-one predicate, in HOL logic@one-to-one predicate, in \HOL\ logic!definitional axiom for}
\index{onto predicate, in HOL logic@onto predicate, in \HOL\ logic!definitional axiom for}
\begin{verbatim}
   ONE_ONE_DEF |- ONE_ONE f = (!x1 x2. (f x1 = f x2) ==> (x1 = x2))

   ONTO_DEF    |- ONTO f    = (!y. ?x. y = f x)
\end{verbatim}\end{hol}

\noindent For further discussion of the 
theory \ml{bool} see Section~\ref{boolfull}. 

\subsubsection{The theory {\tt ind}}
\label{ind}

The theory {\small\verb%ind%}\index{ind, the theory@\ml{ind}, the theory} introduces the type {\small\verb%ind%}\index{ind, the type@\ml{ind}, the type} of 
{\it individuals\/}\index{individuals}
 and the {\it Axiom of Infinity\/}\index{axiom of infinity}. This axiom states
that the set denoted by {\small\verb%ind%} is infinite. The four axioms of
the theory {\small\verb%bool%}, the rules of inference in
Section~\ref{rules} and the Axiom of Infinity are, together, sufficient for
developing all of standard mathematics. Thus, in principle, the user of the
\HOL\ system should never need to make a non-definitional\index{axioms!dispensibility of adding}\index{definitional theories} theory. In
practice, it is often very tempting to take the risk of introducing new
axioms because deriving them from definitions can be tedious---proving that
`axioms' follow from definitions amounts to proving their consistency.


The Axiom of Infinity\index{axioms!in ind theory@in \ml{ind} theory} is


{\begin{hol}
\index{INFINITY_AX@\ml{INFINITY\_AX}}
\index{axiom of infinity}
\index{existential quantifier, in HOL logic@existential quantifier, in \HOL\ logic!in infinity axiom}
\begin{verbatim}
  INFINITY_AX  |- ?f:ind->ind. ONE_ONE f /\ ~(ONTO f)
\end{verbatim}\end{hol}}

\noindent
This asserts that there exists a one-to-one map from {\small\verb%ind%} to
itself that is not onto. This implies that the type {\small\verb%ind%}
denotes an infinite set.\index{axioms!primitive, of HOL logic@primitive, of \HOL\ logic|)}

\subsection{Primitive rules of inference of the HOL Logic}
\label{rules}

\index{inference rules, of HOL logic@inference rules, of \HOL\ logic!primitive|(}
The primitive rules of inference of the logic were described abstractly
in Section~\ref{HOLrules}. The descriptions relied on meta-variables
$t$, $t_1$, $t_2$, and so on.
%In Section~\ref{avra_theorems}, a primitive inference was defined as
%a pair $(L,(\Gamma,t))$ belonging to 
%a deductive system. 
In the \HOL\ logic, infinite families of primitive
inferences are grouped together and thought of as single primitive inference
schemes.\index{families of inferences, in HOL logic@families of inferences, in \HOL\ logic}  Each family contains all the concrete instances of one
particular inference `pattern'. These can be produced, in
abstract form, by instantiating the meta-variables in Section~\ref{HOLrules}
to concrete terms.

In \HOL, primitive inference schemes are represented
by \ML\ functions that return theorems as values.
That is, for particular \HOL\ terms, the \ML\ functions return
the instance of the theorem at those terms. The \ML\ functions
are part of the \ML\ abstract type
 \ml{thm}\index{thm@\ml{thm}}:
although \ml{thm} has no primitive constructors, it has (eight)
operations which return theorems as values: \ml{ASSUME}, \ml{REFL}, 
\ml{BETA\_CONV}, \ml{SUBST}, \ml{ABS}, \ml{INST\_TYPE},
\ml{DISCH} and \ml{MP}.\index{inference schemes, in HOL logic@inference schemes, in \HOL\ logic}

The \ML\ functions that implement the primitive inference
schemes in the \HOL\
system are  described  below.
The same notation\index{notation!for specification of rules}\index{inferences, in HOL logic@inferences, in \HOL\ logic!notation for}
 is used here as in Section~\ref{HOLrules}:
hypotheses above a horizontal line and conclusion\index{conclusions!of inference rules} beneath.
The  machine-readable  {\small ASCII}
notation is used for the logical constants.

\subsubsection{Assumption introduction}\index{assumption introduction, in HOL logic@assumption introduction, in \HOL\ logic!ML function for@\ML\ function for} 

\begin{boxed}
\index{ASSUME@\ml{ASSUME}|pin}
\begin{verbatim}
   ASSUME : term -> thm
\end{verbatim}\end{boxed}

\begin{center}
\begin{tabular}{c}
  \\ \hline
$t${\small\verb% |- %}$t$ \\
\end{tabular}
\end{center}

\noindent
{\small\verb%ASSUME %}$t${\small\verb%%} evaluates to $t${\small\verb%|- %}$t$.
Failure if $t$ is not of type \ml{bool}.

\bigskip

\subsubsection{Reflexivity}\index{reflexivity, in HOL logic@reflexivity, in \HOL\ logic!ML function for@\ML\ function for} 

\begin{boxed}\index{REFL@\ml{REFL}|pin}
\begin{verbatim}
   REFL : term -> thm
\end{verbatim}\end{boxed}

\begin{center}
\begin{tabular}{c}
  \\ \hline
{\small\verb% |- %}$t${\small\verb% = %}$t$ \\
\end{tabular}
\end{center}

\noindent {\small\verb%REFL %}$t${\small\verb%%} evaluates to {\small\verb%|-
%}$t${\small\verb% = %}$t$. A call to \ml{REFL} never fails.

\bigskip

\subsubsection{Beta-conversion}\index{beta-conversion, in HOL logic@beta-conversion, in \HOL\ logic!ML function for@\ML\ function for} 

\begin{boxed}\index{BETA_CONV@\ml{BETA\_CONV}|pin}
\begin{verbatim}
   BETA_CONV : term -> thm
\end{verbatim}\end{boxed}

\begin{center}
\begin{tabular}{c}
  \\ \hline
{\small\verb% |- (\%}$x${\small\verb%.%}$t_1${\small\verb%)%}$t_2${\small\verb% = %}$t_1[t_2/x]$
\end{tabular}
\end{center}

\begin{itemize}
\item where $t_1[t_2/x]$ denotes the result of substituting $t_2$ for $x$
in $t_1$, with suitable renaming of variables to prevent free variables
in $t_2$ becoming bound after substitution. The substitution
 $t_1[t_2/x]$ is always defined.
\end{itemize}


\noindent {\small\verb%BETA_CONV (\%}$x${\small\verb%.%}$t_1${\small\verb%)%}$t_2${\small\verb%%} evaluates to the
theorem {\small\verb%|-
(\%}$x${\small\verb%.%}$t_1${\small\verb%)%}$t_2${\small\verb% = %}$t_1[t_2/x]$.
Failure if the argument to \ml{BETA\_CONV} is not a $\beta$-redex (\ie\ is not
of the form {\small\verb%(\%}$x${\small\verb%.%}$t_1${\small\verb%)%}$t_2${\small\verb%%}).

\bigskip

\subsubsection{Substitution}\index{substitution rule, in HOL logic@substitution rule, in \HOL\ logic!ML function for@\ML\ function for|(}\index{SUBST@\ml{SUBST}|(} 

\begin{boxed}
\begin{verbatim}
   SUBST : (thm # term)list -> term -> thm -> thm
\end{verbatim}\end{boxed}

\begin{center}
\begin{tabular}{c}
$\Gamma_1${\small\verb% |- %} $t_1${\small\verb%=%}$t'_1$ {\small\verb%  %} $\cdots$ {\small\verb%  %}
$\Gamma_n${\small\verb% |- %} $t_n${\small\verb%=%}$t'_n$ {\small\verb%  %} 
$\Gamma${\small\verb% |- %} $t[t_1,\ldots,t_n]$ \\ \hline
$\Gamma_1 \cup \cdots 
\cup \Gamma_n \cup \Gamma${\small\verb% |- %} $t[t'_1,\ldots,t'_n]$ \\
\end{tabular}
\end{center}

\bigskip

\begin{itemize}
\item where $t[t_1,\ldots,t_n]$ denotes a term $t$ with some free 
occurrences of the terms $t_1$, $\dots$, $t_n$ singled out and
$t[t'_1,\ldots,t'_n]$ denotes the result of simultaneously replacing each
such occurrences of $t_i$ by $t'_i$ (for $1{\leq}i {\leq} n$), 
with suitable renaming of variables to prevent free variables
in $t_i'$ becoming bound after substitution.
\end{itemize}

\noindent
The first argument to {\small\verb%SUBST%} is a list
{\small\verb%[(|-%}$t_1${\small\verb%=%}$t'_1${\small\verb%, %}$x_1${\small\verb%);%}$\:\ldots\:${\small\verb%;(|-%}$t_n${\small\verb%=%}
$t'_n${\small\verb%, %}$x_n${\small\verb%)]%}.  The second argument is a
template term $t[x_1,\ldots,x_n]$ in which occurrences of the variable
$x_i$ (where $1 \leq i\leq n$) are used to mark the places where
substitutions with {\small\verb%|- %}$t_i${\small\verb%=%}$t'_i$ are to be
done. Thus

\bigskip

{\small\verb%SUBST [(|-%}$t_1${\small\verb%=%}$t'_1${\small\verb%, %}$x_1${\small\verb%);%}$\ldots${\small\verb%;(|-%}$t_n${\small\verb%=%}
$t'_n${\small\verb%, %}$x_n${\small\verb%)]  %}$t[x_1,\ldots,x_n]${\small\verb%  %}
$\Gamma${\small\verb% |- %}$t[t_1,\ldots,t_n]$

\bigskip 

\noindent returns $\Gamma${\small\verb% |- %}$t[t'_1,\ldots,t'_n]$.
Failure if:
\begin{myenumerate}
\item any of the arguments are of the wrong form;
\item the type of $x_i$ is not equal to the type of $t_i$ for some
$1\leq i\leq n$.
\end{myenumerate}\index{SUBST@\ml{SUBST}|)}\index{substitution rule, in HOL logic@substitution rule, in \HOL\ logic!ML function for@\ML\ function for|)}

\subsubsection{Abstraction}\index{abstraction rule, in HOL logic@abstraction rule, in \HOL\ logic!ML function for@\ML\ function for} 
\index{function abstraction, in HOL logic@function abstraction, in \HOL\ logic!inference rules for}

 
\begin{boxed}\index{ABS@\ml{ABS}|pin}
\begin{verbatim}
   ABS : term -> thm -> thm
\end{verbatim}\end{boxed}


\begin{center}
\begin{tabular}{c}
$\Gamma${\small\verb% |- %}$t_1${\small\verb% = %}$t_2$ \\ \hline
$\Gamma${\small\verb% |- (\%}$x${\small\verb%.%}$t_1${\small\verb%) = (\%}$x${\small\verb%.%}$t_2${\small\verb%)%} \\
\end{tabular}
\end{center}

\begin{itemize}
\item where $x$ is not free in $\Gamma$.
\end{itemize}

\noindent 
{\small\verb%ABS %}$x${\small\verb% %}$\Gamma${\small\verb% |- %}$t_1${\small\verb%=%}$t_2$ returns the theorem
$\Gamma${\small\verb% |- (\%}$x${\small\verb%.%}$t_1${\small\verb%) = (\%}$x${\small\verb%.%}$t_2${\small\verb%)%}.
Failure if $x$ is not a variable, or $x$
 occurs free in any assumption in $\Gamma$.


\bigskip

\subsubsection{Type instantiation}\index{type instantiation, in HOL logic@type instantiation, in \HOL\ logic!ML function for@\ML\ function for}\index{types, in HOL logic@types, in \HOL\ logic!instantiation of}

\begin{boxed}\index{INST_TYPE@\ml{INST\_TYPE}|pin}
\begin{verbatim}
   INST_TYPE : (type#type) list -> thm -> thm
\end{verbatim}\end{boxed}

\begin{center}
\begin{tabular}{c}
$\Gamma${\small\verb% |- %}$t$ \\ \hline
$\Gamma${\small\verb% |- %}$t[\sigma_1,\ \ldots\ ,\sigma_n/\alpha_1,\ \ldots\ ,\alpha_n]$
\end{tabular}
\end{center}

\bigskip

\begin{itemize}
\item $t[\sigma_1,\ \ldots\ ,\sigma_n/\alpha_1,\ \ldots\ ,\alpha_n]$ 
denotes the result of substituting (in parallel) the types $\sigma_1$,
$\ldots$\ , $\sigma_n$ for the type variables $\alpha_1$, $\ldots$\ ,
$\alpha_n$ in $t$, with the restriction that none of $\alpha_1$, $\ldots$\
, $\alpha_n$ occur in $\Gamma$.
\end{itemize}

\noindent
{\small\verb%INST_TYPE[(%}$\sigma_1${\small\verb%,%}$\alpha_1${\small\verb%);%}$\ldots${\small\verb%;(%}$\sigma_n${\small\verb%,%}$\alpha_n${\small\verb%)] %}$th$
returns the result of instantiating each occurrence of $\alpha_i$ in the
theorem $th$ to $\sigma_i$ (for $1 \leq i \leq n$). Failure if:
\begin{myenumerate}
\item arguments of the wrong form (\eg\ an $\alpha_i$ is not a type variable);
\item $\alpha_i$
(for $1\leq i\leq n$) occurs in any assumption in $\Gamma$.
\end{myenumerate}

\bigskip

\subsubsection{Discharging an assumption}\index{discharging assumptions, in HOL logic@discharging assumptions, in \HOL\ logic!ML function for@\ML\ function for} 

 
\begin{boxed}\index{DISCH@\ml{DISCH}|pin}
\begin{verbatim}
   DISCH : term -> thm -> thm
\end{verbatim}\end{boxed}

\begin{center}
\begin{tabular}{c}
$\Gamma${\small\verb% |- %} $t_2$ \\ \hline
$\Gamma{-}\{t_1\}${\small\verb% |- %} $t_1${\small\verb% ==> %}$t_2$
\end{tabular}
\end{center}

\begin{itemize}
\item  $\Gamma{-}\{t_1\}$ denotes the set obtained by removing $t_1$ 
from $\Gamma$ (note that $t_1$ need not occur in $\Gamma$; in this case
$\Gamma{-}\{t_1\} = \Gamma$).
\end{itemize}

\noindent
{\small\verb%DISCH %}$t_1${\small\verb% %}$\Gamma${\small\verb% |- %}$t_2$
evaluates to the theorem
$\Gamma{-}\{t_1\}${\small\verb% |- %}$t_1${\small\verb% ==> %}$t_2$.
\ml{DISCH} fails if the term given as its first argument is not of 
type \ml{bool}.



\bigskip

\subsubsection{Modus Ponens}\index{Modus Ponens, in HOL logic@Modus Ponens, in \HOL\ logic!ML function for@\ML\ function for} 

 
\begin{boxed}\index{MP@\ml{MP}|pin}
\begin{verbatim}
   MP : thm -> thm -> thm
\end{verbatim}\end{boxed}

\begin{center}
\begin{tabular}{c}
$\Gamma_1${\small\verb% |- %}$t_1${\small\verb% ==> %}$t_2$ {\small\verb%     %} $\Gamma_2${\small\verb% |- %}$t_1$ \\
\hline
$\Gamma_1 \cup \Gamma_2${\small\verb% |- %}$t_2$ \\
\end{tabular}
\end{center}

\noindent
{\small\verb%MP%} takes two theorems (in the order shown above) and returns
the result of applying Modus Ponens; it fails if the arguments are not of the
right form.
\index{inference rules, of HOL logic@inference rules, of \HOL\ logic!primitive|)}

\subsection{Type abbreviations}\label{typeabbrev}\index{types, in HOL logic@types, in \HOL\ logic!abbreviation of}\index{type abbreviations!in HOL logic@in \HOL\ logic}\index{abbreviation of types, in HOL logic@abbreviation of types, in \HOL\ logic|(}
It is possible to introduce an abbreviation for a monomorphic type using the
function:

\begin{boxed}\index{new_type_abbrev@\ml{new\_type\_abbrev}|pin}
\begin{verbatim}
   new_type_abbrev : (string # type) -> void 
\end{verbatim}\end{boxed}

\noindent Evaluating \ml{new\_type\_abbrev(`}$name$\ml{`,":}$\sigma$\ml{")}
enables $name$ to be used in quotations instead of $\sigma$. The evaluation
fails
if $\sigma$ is polymorphic. Type abbreviations
are recorded in theory files, so that
when a theory is loaded, any type abbreviations made are
activated. The list of currently active abbreviations in a theory
is given by the function:

\begin{boxed}\index{type_abbrevs@\ml{type\_abbrevs}|pin}
\begin{verbatim}
   type_abbrevs : string -> (string # type) list
\end{verbatim}\end{boxed}


Note that abbreviation can also be made using antiquotation\index{antiquotation, in HOL logic terms@antiquotation, in \HOL\ logic terms}, without the
restriction to monomorphic types. Such \ML\ abbreviations are not, of course,
stored in theory files and so do not persist beyond a single session. 
The following session illustrates various ways of
abbreviating types:

\setcounter{sessioncount}{1}
\begin{session}\begin{verbatim}
#new_theory `numpair`;;
() : void

#new_type_abbrev(`numpair`, ":num#num");;
() : void

#let t1 = "x:numpair";;
t1 = "x" : term

#type_of t1;;
":num # num" : type

#":numpair" = ":num#num";;
true : bool
\end{verbatim}\end{session}

\noindent The alternative to introducing a type abbreviation is
to give an \ML\ name to the type, and then to use this name via antiquotation.
Continuing the session:\index{abbreviation of types, in HOL logic@abbreviation of types, in \HOL\ logic|)}

\begin{session}\begin{verbatim}
#let ty = ":num#num";;
ty = ":num # num" : type

#let t2 = "x:^ty";;
t2 = "x" : term

#t1 = t2;;
true : bool
\end{verbatim}\end{session}

\pagebreak[2]

\noindent The type abbreviation is stored in the theory file and so
persists across sessions. This can be seen by the result of printing
the theory \ml{numpair}:

\begin{session}\begin{verbatim}
#print_theory`numpair`;;
The Theory numpair
Parents --  HOL     
Type Abbreviations --  numpair ":num # num"     
******************** numpair ********************

() : void
\end{verbatim}\end{session}

\noindent If the session is then ended: 

\begin{session}\begin{verbatim}
#close_theory();;
() : void

#quit();;
\end{verbatim}\end{session}

\noindent and a new session is started in which the theory \ml{numpair} is
loaded:

\setcounter{sessioncount}{1}
\begin{session}\begin{verbatim}
#load_theory`numpair`;;
Theory numpair loaded
() : void

#"x:numpair";;
"x" : term

#type_abbrevs `-`;;
[(`numpair`, ":num # num")] : (string # type) list
\end{verbatim}\end{session}

\noindent then the type abbreviation persists.

Type abbreviations tend to be little used in practice; the antiquotation
method is usually sufficient.

\section{The ancestry of the theory {\tt HOL}}
\label{HOL-ancestry}

\index{theories, in HOL logic@theories, in \HOL\ logic!hierarchies of}
The ancestry\index{ancestry, of HOL system theories@ancestry, of \HOL\ system theories}
of the theory \ml{HOL}\index{HOL@\ml{HOL}} is:

\begin{center}\index{BASIC-HOL@\ml{BASIC-HOL}}\index{bool, the HOL theory@\ml{bool}, the \HOL\ theory}\index{ind, the theory@\ml{ind}, the theory}
\begin{picture}(65,115)

\thicklines


% -----------------------------------------------------------
% Lines in theory hierarchy graph
% -----------------------------------------------------------

\put(40,5){\line(-4,1){20}}      % HOL --> tydefs
\put(40,5){\line(0,1){5}}	 % HOL --> sum
\put(40,5){\line(4,1){20}}	 % HOL --> one

\put(20,15){\line(0,1){5}}	 % tydefs --> ltree
\put(40,15){\line(-2,3){10}}	 % sum    --> combin

\put(20,25){\line(-2,1){10}}	 % ltree --> tree
\put(20,25){\line(2,1){10}}	 % ltree --> combin

\put(10,35){\line(0,1){5}}	 % tree --> list
\put(10,45){\line(0,1){5}}	 % list --> arithmetic
\put(10,55){\line(0,1){5}}	 % arithmetics --> prim_rec
\put(10,65){\line(0,1){5}}	 % prim_rec --> num

\put(10,75){\line(4,1){20}}      % num --> BASIC-HOL

\put(30,85){\line(0,1){5}}	 % BASIC-HOL --> ind
\put(30,95){\line(0,1){5}}	 % ind --> bool
\put(30,105){\line(0,1){5}}	 % bool --> PPLAMB
\put(30,35){\line(0,1){45}}	 % combin --> BASIC-HOL
\put(60,20){\line(-1,2){30}}	 % one --> BASIC-HOL
\put(60,15){\line(0,1){5}}	 % one --> BASIC-HOL



% -----------------------------------------------------------
% Theory names:
% -----------------------------------------------------------

\put(40,2.5){\makebox(0,0){\verb!HOL!}}

\put(20,12.5){\makebox(0,0){\verb!tydefs!}}
\put(40,12.5){\makebox(0,0){\verb!sum!}}
\put(60,12.5){\makebox(0,0){\verb!one!}}

\put(20,22.5){\makebox(0,0){\verb!ltree!}}

\put(30,32.5){\makebox(0,0){\verb!combin!}}
\put(10,32.5){\makebox(0,0){\verb!tree!}}

\put(10,42.5){\makebox(0,0){\verb!list!}}
\put(10,52.5){\makebox(0,0){\verb!arithmetic!}}
\put(10,62.5){\makebox(0,0){\verb!prim\_rec!}}
\put(10,72.5){\makebox(0,0){\verb!num!}}
\put(30,82.5){\makebox(0,0){\verb!BASIC-HOL!}}
\put(30,92.5){\makebox(0,0){\verb!ind!}}
\put(30,102.5){\makebox(0,0){\verb!bool!}}
\put(30,112.5){\makebox(0,0){\verb!PPLAMB!}}

\end{picture}
\end{center}

\noindent In the rest of this section, each of the theories in  the ancestry of
\ml{HOL} is  briefly described.   A  complete list  of all  the definitions and
theorems in each theory is  not given  here; the sections  that follow provide
only an overview of the contents of each theory.  For a complete list of
all the built-in axioms, definitions and theorems in \HOL, see \REFERENCE.

\subsection{The theory {\tt PPLAMB}}

The most primitive theory is called \ml{PPLAMB}\index{PPLAMB@\ml{PPLAMB}} and is a stripped down
version of the theory underlying \LCF.\index{LCF@\LCF}  The \HOL\ theory \ml{PPLAMB}
does not represent any logical principles but is an interface between the \HOL\
and \LCF\ systems (it contains the declaration of the primitive 
type operator \ml{->}).\index{ function type operator, in HOL logic@\ml{->} (function type operator, in \HOL\ logic)}
For a while the two systems developed in parallel, upgrades in \LCF\ from
Gerard Huet\index{Huet, G.} of {\small INRIA} or Larry Paulson\index{Paulson, L.} of Cambridge resulting in
upgrades in \HOL.

\subsection{The theory {\tt bool}}\label{boolfull}

The theory \ml{bool}\index{bool, the HOL theory@\ml{bool}, the \HOL\ theory|(} has already been partly described in 
Section~\ref{boolthy}.
It contains the definitions of several sorts of constants:

\begin{myenumerate}


\item logical constants:\index{primitive constants, of HOL logic@primitive constants, of \HOL\ logic}\index{truth values, in HOL logic@truth values, in \HOL\ logic}\index{logical constants, in HOL logic@logical constants, in \HOL\ logic}\index{ implication, in HOL logic@{\small\verb+==>+} (implication, in \HOL\ logic)}\index{conjunction, in HOL logic@conjunction, in \HOL\ logic}\index{disjunction, in HOL logic@disjunction, in \HOL\ logic}%
\index{constants, in HOL logic@constants, in \HOL\ logic!logical}\index{ universal quantifier, in HOL logic@{\small\verb+"!+} (universal quantifier, in \HOL\ logic)}%
\index{ existential quantifier, in HOL logic@{\small\verb+?+} (existential quantifier, in \HOL\ logic)}%
\index{ conjunction, in HOL logic@{\small\verb+/\+} (conjunction, in \HOL\ logic)}%
\index{ disjunction, in HOL logic@{\small\verb+\/+} (disjunction, in \HOL\ logic)}%
\index{F@\ml{F}}\index{T@\ml{T}}%
\index{existential quantifier, in HOL logic@existential quantifier, in \HOL\ logic}%
\index{universal quantifier, in HOL logic@universal quantifier, in \HOL\ logic}
\index{ negation, in HOL logic@{\small\verb+~+} (negation, in \HOL\ logic)}
\index{ exists unique, in HOL logic@{\small\verb+?"!+} (exists unique, in \HOL\ logic)}%
\index{ choice function, in HOL logic@{\small\verb+"@+} (choice function, in \HOL\ logic)}%
\index{choice operator, in HOL logic@choice operator, in \HOL\ logic}%
\index{equality, in HOL logic@equality, in \HOL\ logic}%
\index{iff, in HOL logic@iff, in \HOL\ logic}%
\index{implication, in HOL logic@implication, in \HOL\ logic}%
\index{one-to-one predicate, in HOL logic@one-to-one predicate, in \HOL\ logic!in bool theory@in \ml{bool} theory}%
\index{onto predicate, in HOL logic@onto predicate, in \HOL\ logic!in bool theory@in \ml{bool} theory} \ml{T}, \ml{F}, {\small\verb!~!}, 
{\small\verb%/\%}, {\small\verb%\/%}, \ml{==>},
\ml{=}, \ml{!}, \ml{?}, \ml{?!} and \ml{@}.

\item system constants\index{constants, in HOL logic@constants, in \HOL\ logic!system}, which are used in coding \HOL\ theories as
\LCF\index{LCF@\LCF}\ theories. These constants are \ml{HOL\_DEFINITION}\index{HOL_DEFINITION@\ml{HOL\_DEFINITION}} and
\ml{BINDERS}\index{BINDERS@\ml{BINDERS}}. They have no logical significance 
and are part of the internal workings of the \HOL\ system.


\item miscellaneous constants\index{constants, in HOL logic@constants, in \HOL\ logic!abbreviational}%
\index{COND@\ml{COND}}%
\index{FCOND@\ml{FCOND}}%
\index{LET@\ml{LET}}%
\index{CURRY@\ml{CURRY}}%
\index{UNCURRY@\ml{UNCURRY}}%
\index{RES_FORALL@\ml{RES\_FORALL}}%
\index{RES_EXISTS@\ml{RES\_EXISTS}}%
\index{RES_SELECT@\ml{RES\_SELECT}}%
\index{RES_ABSTRACT@\ml{RES\_ABSTRACT}}%
\index{ARB@\ml{ARB}}, which support various special syntactic forms:
\ml{COND} (for conditionals, see Section~\ref{conditionals});
\ml{LET} (for \ml{let}-terms\index{let-terms, in HOL logic@\ml{let}-terms, in \HOL\ logic!constant for}, see Section~\ref{let-exp});
\ml{CURRY} and \ml{UNCURRY} (for paired abstractions, 
see Section~\ref{HOL-varstruct}); and
\ml{RES\_FORALL},
\ml{RES\_EXISTS},
\ml{RES\_SELECT},
\ml{RES\_ABSTRACT}
and \ml{ARB} (for restricted quantification, 
see Section~\ref{res-quant}).

\item the constant \ml{TYPE\_DEFINITION}\index{TYPE_DEFINITION@\ml{TYPE\_DEFINITION}}, which is used by the type definition mechanism\index{constants, in HOL logic@constants, in \HOL\ logic!for type definitions} (see Section~\ref{type-defs}).

\item constants associated with pairs:\index{constants, in HOL logic@constants, in \HOL\ logic!for pairs}
\index{MK_PAIR@\ml{MK\_PAIR}}
\index{IS_PAIR@\ml{IS\_PAIR}}
 \ml{,} (\ie\ the comma symbol), 
\ml{MK\_PAIR}, \ml{IS\_PAIR}, \ml{REP\_prod}, \ml{FST} and \ml{SND}
(see Section~\ref{prod} below).
\end{myenumerate}

\subsubsection{Pairs and the type {\tt prod}}
\label{prod}

\index{representing types, in HOL logic@representing types, in \HOL\ logic!pair example of|(}
\index{pairs, in HOL logic@pairs, in \HOL\ logic|(}
\index{product types!in HOL logic@in \HOL\ logic|(}
The Cartesian  product  type  operator\index{type operators, in HOL logic@type operators, in \HOL\ logic!for pairs}  \ml{prod}\index{prod@\ml{prod}} is  defined  in  the  theory \ml{bool}, although logically it should really  be in  a separate  theory.  The
reason for its  definition early  on is that certain  syntactic forms (\eg\
paired abstractions) presuppose pairs.  

Values of type
{\small\verb%(%}$\sigma_1${\small\verb%,%}$\sigma_2${\small\verb%)prod%} are
ordered pairs  whose  first  component  has  type  $\sigma_1$  and whose second
component has type $\sigma_2$.  The \HOL\ parser\index{parsing, of HOL logic@parsing, of \HOL\ logic!of pairs}
converts
type expressions of the 
form \ml{":}$\sigma_1${\small\verb%#%}$\sigma_2$\ml{"}\index{ product type operator, in HOL logic@{\small\verb+#+} (product
type operator, in \HOL\ logic)} into
\ml{(}$\sigma_1$\ml{,}$\sigma_2$\ml{)prod}\index{ pair constructor, in HOL
logic@\ml{,} (pair constructor, in \HOL\ logic)}, and   the   printer
inverts  this transformation. Pairs\index{pairing constructor, in HOL
logic@pairing constructor, in \HOL\ logic} are constructed with an infixed
comma symbol 


\begin{hol}\begin{verbatim}
   $, : * -> ** -> *#**
\end{verbatim}\end{hol}

\noindent so, for example, if $t_1$ and $t_2$ have types $\sigma_1$ and 
$\sigma_2$
respectively, then \ml{"}$t_1$\ml{,}$t_2$\ml{"} is a term with type
$\sigma_1${\small\verb%#%}$\sigma_2$. It is usual, but not necessary, to write
pairs within brackets:
\ml{"(}$t_1$\ml{,}$t_2$\ml{)"}. The comma symbol associates\index{pairing constructor, in HOL logic@pairing constructor, in \HOL\ logic!associativity of} to the right, so
 that
\ml{"(}$t_1$\ml{,}$t_2$\ml{,}$\ldots$\ml{,}$t_n$\ml{)"}
means
\ml{"(}$t_1$\ml{,(}$t_2$\ml{,}$\ldots$\ml{,}$t_n$\ml{))"}.
The constants 


\begin{hol}
\index{FST, the constant in HOL logic@\ml{FST}, the constant in \HOL\ logic}
\index{SND, the constant in HOL logic@\ml{SND}, the constant in \HOL\ logic}
\begin{verbatim}
   FST : * # ** -> *
   SND : * # ** -> **
\end{verbatim}\end{hol}

\noindent select the first and second components of pairs. 

Cartesian products are defined by representing a pair
{\small\verb%(%}$t_1${\small\verb%,%}$t_2${\small\verb%)%} by the function

\begin{hol}\begin{alltt}
   \verb!\!a b. (a=\m{t\sb{1}}) /\verb!\! (b=\m{t\sb{2}})
\end{alltt}\end{hol}

\noindent The
representing type of $\sigma_1${\small\verb%#%}$\sigma_2$ is thus
$\sigma_1${\small\verb%->%}$\sigma_2${\small\verb%->bool%}.  To define
pairs this way, the constants \ml{MK\_PAIR} and
\ml{IS\_PAIR}\index{IS_PAIR@\ml{IS\_PAIR}} are first defined.


\begin{hol}
\index{MK_PAIR_DEF@\ml{MK\_PAIR\_DEF}}
\index{IS_PAIR_DEF@\ml{IS\_PAIR\_DEF}}
\begin{verbatim}
   MK_PAIR_DEF   |- !x y. MK_PAIR x y = (\a b. (a = x) /\ (b = y))
 
   IS_PAIR_DEF   |- !p. IS_PAIR p = (?x y. p = MK_PAIR x y)
\end{verbatim}\end{hol}

\noindent From these two definitions it is easy to prove that:

\begin{hol}\begin{verbatim}
   |- ?p:*->**->bool. IS_PAIR p
\end{verbatim}\end{hol}

\noindent since {\small\verb%|- IS_PAIR(MK_PAIR x y)%} follows  easily from the
definition of  \ml{IS\_PAIR}.    The  existence  theorem shown  above is called
{\small\verb%PAIR_EXISTS%}\index{PAIR_EXISTS@\ml{PAIR\_EXISTS}}.
 Given this theorem, the type operator
{\small\verb%prod%} is defined by evaluating:

\begin{hol}\begin{verbatim}
   new_type_definition(`prod`, "IS_PAIR:(*->**->bool)->bool", PAIR_EXISTS)
\end{verbatim}\end{hol}

\noindent which results in the definitional axiom\index{axioms!non-primitive, of HOL logic@non-primitive, of \HOL\ logic}\index{axioms!in bool theory@in \ml{bool} theory} \ml{prod\_TY\_DEF} shown
below being asserted in the theory \ml{bool}.

\begin{hol}\begin{verbatim}
   prod_TY_DEF  |- ?rep. TYPE_DEFINITION IS_PAIR rep
\end{verbatim}\end{hol}

Next, a new constant {\small\verb%REP_prod%} is defined, which
maps a pair to its representation as a function:

\begin{hol}
\index{REP_prod@\ml{REP\_prod}}
\begin{verbatim}
   REP_prod    |- REP_prod =
                  (@rep : * # ** -> (* -> (** -> bool)).
                    (!p' p''. (rep p' = rep p'') ==> (p' = p'')) /\
                    (!p. IS_PAIR p = (?p'. p = rep p')))
\end{verbatim}\end{hol}

The infix constructor `{\small\verb%,%}'
and the selectors
{\small\verb%FST:*#**->*%} and {\small\verb%SND:*#**->**%} are then
defined by the equations shown below.



\begin{hol}\index{COMMA_DEF@\ml{COMMA\_DEF}}
\index{FST_DEF@\ml{FST\_DEF}}
\index{SND_DEF@\ml{SND\_DEF}}
\index{pairing constructor, in HOL logic@pairing constructor, in \HOL\ logic!definition of}
\index{FST, the constant in HOL logic@\ml{FST}, the constant in \HOL\ logic!definition of}
\index{selectors, in HOL logic@selectors, in \HOL\ logic}
\begin{verbatim}
   COMMA_DEF  |- !x y. x,y = (@p. REP_prod p = MK_PAIR x y)
 
   FST_DEF    |- !p. FST p = (@x. ?y. MK_PAIR x y = REP_prod p)

   SND_DEF    |- !p. SND p = (@y. ?x. MK_PAIR x y = REP_prod p)
\end{verbatim}\end{hol}

The following standard theorems about pairs follow easily from these
definitions and the axiom \ml{prod\_TY\_DEF}.  Although these theorems could
be derived by formal proof, they are (for implementation reasons) asserted as
axioms in the theory \ml{bool} .


\begin{hol}
\index{PAIR@\ml{PAIR}}
\index{FST, the axiom in HOL logic@\ml{FST}, the axiom in \HOL\ logic}
\index{SND, the axiom in HOL logic@\ml{SND}, the axiom in \HOL\ logic}
\index{PAIR_EQ@\ml{PAIR\_EQ}}
\begin{verbatim}
   PAIR     |- !x. (FST x,SND x) = x

   FST      |- !x y. FST(x,y) = x

   SND      |- !x y. SND(x,y) = y

   PAIR_EQ  |- !x y a b. (x,y = a,b)  =  (x = a) /\ (y = b)
\end{verbatim}\end{hol}
\index{pairs, in HOL logic@pairs, in \HOL\ logic|)}
\index{product types!in HOL logic@in \HOL\ logic|)}
\index{representing types, in HOL logic@representing types, in \HOL\ logic!pair example of|)}
\index{bool, the HOL theory@\ml{bool}, the \HOL\ theory|)}

\subsection{The theory {\tt BASIC-HOL}}

The theory \ml{BASIC-HOL}\index{BASIC-HOL@\ml{BASIC-HOL}} roughly corresponds to the theory
\theory{INIT}\index{initial theory, of HOL logic@initial theory, of \HOL\ logic}\index{INIT@\ml{INIT}!as BASIC_HOL@as \ml{BASIC\_HOL}} described in Section~\ref{INIT}. It consists of the data
in the theories \ml{bool} and \ml{ind}, together with one pre-proved theorem
called \ml{ABS\_REP\_THM}\index{ABS_REP_THM@\ml{ABS\_REP\_THM}}, which establishes various standard properties
of isomorphisms\index{isomorphism of types, in HOL logic@isomorphism of types, in \HOL\ logic} and is used for deriving consequences of type definitions (see 
Section~\ref{type-defs}).

The descendents of \ml{BASIC-HOL} are obtained by definitional extension.
There are, however, a few impurities in these extensions, with the result that
not all of them could be built purely by using the definitional mechanisms of
\HOL. The theory \ml{num}, for example, contains an infinite family of
constants \ml{0}, \ml{1}, \ml{2} \etc, but there is currently no 
mechanism that allows users to define such infinite families.

\subsection{The theory {\tt num}}

The theory \ml{num}\index{num, the theory in HOL logic@\ml{num}, the theory in \HOL\ logic}
defines the type \ml{num} of natural numbers to be
isomorphic to a countable subset of the primitive type \ml{ind}.  In this
theory, the constants \ml{0}\index{ zero, in HOL logic@\ml{0} ( zero, in \HOL\ logic)}
 and \ml{SUC} (the successor function) are defined
and Peano's axioms\index{axioms!in num theory@in \ml{num} theory}\index{Peano's axioms}\index{axioms!non-primitive, of HOL logic@non-primitive, of \HOL\ logic} pre-proved in the form:


\begin{hol}
\index{NOT_SUC@\ml{NOT\_SUC}}
\index{INV_SUC@\ml{INV\_SUC}}
\index{INDUCTION@\ml{INDUCTION}}
\begin{verbatim}
   NOT_SUC    |- !n. ~(SUC n = 0)
   INV_SUC    |- !m n. (SUC m = SUC n) ==> (m = n)
   INDUCTION  |- !P. P 0 /\ (!n. P n ==> P(SUC n)) ==> (!n. P n)
\end{verbatim}\end{hol}

In higher order logic, Peano's axioms are sufficient for developing number
theory because addition and multiplication can be defined. In first order
logic these must be taken as primitive.  Note also that
{\small\verb%INDUCTION%}\index{induction rule!for numbers, in HOL logic@for numbers, in \HOL\ logic} could not be stated as a single axiom in
first order logic because predicates (\eg\ {\small\verb%P%}) cannot be
quantified.

Uses of the theorem \ml{INDUCTION} are supported by the built-in derived
inference rule \ml{INDUCT}\index{INDUCT@\ml{INDUCT}}
and the built-in
tactic \ml{INDUCT\_TAC}\index{INDUCT_TAC@\ml{INDUCT\_TAC}}
(see the documentation on these functions in \REFERENCE\ for details).

\subsubsection{Numerals}

Associated with the theory \ml{num} are the numerals of type
\ml{:num}\index{num, the type in HOL logic@\ml{num}, the type in \HOL\ logic}, 
an infinite family of constants: \ml{1}, \ml{2}, \ml{3}, etc. These can
be regarded logically as an infinite collection of defined
constants, introduced by the infinite series of  definitional axioms:

\begin{hol}\begin{alltt}
   |- 1 = SUC 0{\rm ,  } |- 2 = SUC 1{\rm ,  } |- 3 = SUC 2{\rm ,\normalsize   etc.}
\end{alltt}\end{hol}

\noindent This infinite list of theorems cannot, of course, actually be 
stored in the theory \ml{num}.  \HOL\ therefore provides the \ML\ function:

\begin{boxed}
\index{num_CONV@\ml{num\_CONV}|pin}
\begin{verbatim}
   num_CONV : term -> thm
\end{verbatim}\end{boxed}

\noindent which can be used to generate the defining equation for any 
constant number of type \ml{num}.  For example:

\setcounter{sessioncount}{1}
\begin{session}\begin{verbatim}
#let thm1 = num_CONV "1";;
thm1 = |- 1 = SUC 0

#let thm2 = num_CONV "2";;
thm2 = |- 2 = SUC 1

#let thm3 = num_CONV "3141592653";;
thm3 = |- 3141592653 = SUC 3141592652
\end{verbatim}\end{session}

\noindent The defining equation for any numeral of type \ml{num} can likewise
be obtained using \ml{num\_CONV}.

\subsection{The theory {\tt prim\_rec}}
\label{prim_rec}

\index{primitive recursive definitions, in HOL logic@primitive recursive definitions, in \HOL\ logic!automated|(}
\index{primitive recursion theorem!for numbers|(}
\index{prim_rec@\ml{prim\_rec}|(}
In classical logic, unlike domain theory logics such as \PPL\index{PPlambda (same as PPLAMBDA), of LCF system@\ml{PP}$\lambda$ (same as \ml{PPLAMBDA}), of \ml{LCF} system},
arbitrary recursive definitions\index{recursive definitions, in classical logics} are not allowed. For example, there is no
function $f$ (of type \ml{num->num}) such that

\begin{hol}
{\small\verb%   !%}$x${\small\verb%. %}$f$ $x${\small\verb%  =  (%}$f$ $x${\small\verb%) + 1%}
\end{hol}

\noindent Certain restricted forms of recursive\index{primitive recursive
functions}
definition do, however, uniquely
define functions. An important example are the {\it primitive recursive\/}
functions.\footnote{In higher order logic, primitive recursion
is much more powerful than in first order logic;
for example, Ackermann's function can be defined
by primitive recursion in higher order logic.} For 
any $x$ and $f$ the {\it primitive
recursion theorem\/} tells us that there is a unique function
{\small\verb%fn%} such that:

\begin{hol}
{\small\verb%   %}\ml{fn}{\small\verb% 0 = %}$x${\small\verb%) /\ (!%}$n${\small\verb%.%}\ml{fn}{\small\verb%(%}\ml{SUC} $n${\small\verb%) = %}$f${\small\verb% (%}\ml{fn} $n${\small\verb%)%} $n${\small\verb%)%}
\end{hol}

The primitive recursion
 theorem follows from Peano's\index{Peano's axioms}
 axioms. When the \HOL\
system is built, the following theorem is proved and stored in the theory
{\small\verb%prim_rec%}:


\begin{hol}\index{num_Axiom@\ml{num\_Axiom}}
\index{characterizing theorem!for numbers}
\begin{verbatim}
   num_Axiom   |- !x f. ?!fn. (fn 0 = x) /\ (!n. fn(SUC n) = f (fn n) n)
\end{verbatim}\end{hol}

\noindent The theorem states the validity of primitive recursive
definitions on the natural numbers: for any \ml{x} and \ml{f} there exists a
corresponding total function \ml{fn} which satisfies
the primitive recursive definition whose form is determined by \ml{x} and
\ml{f}.

\subsubsection{Primitive recursive definitions}\label{num-prim-rec}

\index{type definitions, in HOL logic@type definitions, in \HOL\ logic!primitive recursive|(}
\index{recursive definitions, in HOL logic@recursive definitions, in \HOL\ logic!automated, for numbers|(}
\index{primitive recursion theorem!automated use of, in HOL system@automated use of, in \HOL\ system|(}
The primitive\index{primitive recursive definitions, in HOL logic@primitive recursive definitions, in \HOL\ logic!justification of} recursion theorem 
can be used to justify any  definition of a
function on the  natural numbers  by primitive  recursion.   For example, a
primitive recursive definition in higher order
logic of the form

\begin{hol}\begin{alltt}
   fun 0       x\(\sb{1}\) \m{\dots} x\(\sb{i}\) = \m{f\sb{1}[}x\(\sb{1}\)\m{,\ldots,\,} x\(\sb{i}]\) 
   fun (SUC n) x\(\sb{1}\) \m{\dots} x\(\sb{i}\) = \m{f\sb{2}[}fun n \m{t\sb{1} \dots t\sb{i},} n\m{,} x\(\sb{1}\)\m{,\ldots,\,}x\(\sb{i}]\)
\end{alltt}\end{hol}

\noindent where all the free variables in the  terms $t_1$,  
\dots, $t_i$ are contained in $\{$\ml{n}, $\ml{x}_1$, \dots, $\ml{x}_i\}$, 
is logically equivalent to:

\begin{hol}\begin{alltt}
   fun 0       = \verb!\!x\(\sb{1}\) \m{\dots} x\(\sb{i}\).\m{f\sb{1}[}x\(\sb{1}\)\m{,\ldots,\,}x\(\sb{i}]\)
   fun (SUC n) = \verb!\!x\(\sb{1}\) \m{\dots} x\(\sb{i}\).\m{f\sb{2}[}fun n \m{t\sb{1} \dots t\sb{i},} n\m{,}x\(\sb{1}\)\m{,\ldots,\,}x\(\sb{i}]\)
               = (\verb!\!f n x\(\sb{1}\) \m{\dots} x\(\sb{i}\).\m{f\sb{2}[}f \m{t\sb{1} \dots t\sb{i},} n\m{,} x\(\sb{1}\)\m{,\ldots,\,}x\(\sb{i}]\)) (fun n) n
\end{alltt}\end{hol}

The existence  of  a  recursive  function  \ml{fun} which  satisfies these two
equations follows directly from the primitive recursion theorem
\ml{num\_Axiom} shown above.   Specializing the  quantified variables \verb!x!
and \verb!f!  in  a suitably  type-instantiated version  of \ml{num\_Axiom} so
that

\begin{hol}\begin{alltt}
   x\m{=}\verb!\!x\(\sb{1}\) \(\dots\) x\(\sb{i}\).\m{f\sb{1}[}x\(\sb{1}\)\(,\ldots,\,\)x\(\sb{i}]\)  {\rm and}  f\(=\)\verb!\!f n x\(\sb{1}\) \(\dots\) x\(\sb{i}\).\m{f\sb{2}[}f \m{t\sb{1} \dots t\sb{i},} n\(,\) x\(\sb{1}\)\(,\ldots,\,\)x\(\sb{i}]\))
\end{alltt}\end{hol}

\noindent yields (ignoring the uniqueness of \ml{fn}) 
the existence theorem shown below:

\begin{hol}\begin{alltt}
   |- ?fn. fn 0       = \verb!\!x\(\sb{1}\) \(\dots\) x\(\sb{i}\).\m{f\sb{1}[}x\(\sb{1}\)\(,\ldots,\,\)x\(\sb{i}]\) /\verb!\!
           fn (SUC n) = (\verb!\!f n x\(\sb{1}\) \(\dots\) x\(\sb{i}\).\m{f\sb{2}[}f \m{t\sb{1} \dots t\sb{i},} n\(,\) x\(\sb{1}\)\(,\ldots,\,\)x\(\sb{i}]\)) (fn n) n
\end{alltt}\end{hol}

\noindent This theorem allows a constant \ml{fun} to be introduced (via the
definitional mechanism of constant specifications---see Section~\ref{conspec})
to denote the recursive function that satisfies the two equations in the body
of the theorem. Introducing a constant \ml{fun} to name the function asserted
to exist by the theorem shown above, and simplifying using $\beta$-reduction,
yields the following theorem:

\begin{hol}\begin{alltt}
   |- fun 0       = \verb!\!x\(\sb{1}\) \(\dots\) x\(\sb{i}\).\m{f\sb{1}[}x\(\sb{1}\)\(,\ldots,\,\)x\(\sb{i}]\) /\verb!\!
      fun (SUC n) = \verb!\!x\(\sb{1}\) \(\dots\) x\(\sb{i}\).\m{f\sb{2}[}fun n \m{t\sb{1} \dots t\sb{i},} n\(,\) x\(\sb{1}\)\(,\ldots,\,\)x\(\sb{i}]\)
\end{alltt}\end{hol}

\noindent It follows immediately from this theorem that the constant \ml{fun}
satisfies the primitive recursive defining equations given by the theorem shown
below:

\begin{hol}\begin{alltt}
   |- fun 0 x\(\sb{1}\) \(\dots\) x\(\sb{i}\) = \m{f\sb{1}[}x\(\sb{1}\)\(,\ldots,\,\)x\(\sb{i}]\)
      fun (SUC n) x\(\sb{1}\) \(\dots\) x\(\sb{i}\) = \m{f\sb{2}[}fun n \m{t\sb{1} \dots t\sb{i},} n\(,\) x\(\sb{1}\)\(,\ldots,\,\)x\(\sb{i}]\)
\end{alltt}\end{hol}

To automate the use of the primitive recursion theorem in deriving recursive
definitions of this kind, the \HOL\ system provides two functions which,
together, first do automatic proofs of the existence of primitive recursive
functions and then make constant specifications to introduce constants that
denote such functions:

\begin{boxed}
\index{new_prim_rec_definition@\ml{new\_prim\_rec\_definition}|pin}
\index{new_infix_prim_rec_definition@\ml{new\_infix\_prim\_rec\_definition}|pin}
\begin{verbatim}
   new_prim_rec_definition       : (string # term) -> thm
   new_infix_prim_rec_definition : (string # term) -> thm
\end{verbatim}\end{boxed}

\noindent Evaluating

\begin{hol}\begin{alltt}
   new_prim_rec_definition
    (`fun_DEF`,
     "(fun 0 x\(\sb{1}\) \(\dots\) x\(\sb{i}\) = \m{f\sb{1}[}x\(\sb{1}\)\(,\ldots,\,\)x\(\sb{i}]\) /\verb!\!
      (fun (SUC n) x\(\sb{1}\) \(\dots\) x\(\sb{i}\) = \m{f\sb{2}[}fun n \m{t\sb{1} \dots t\sb{i},} n\(,\) x\(\sb{1}\)\(,\ldots,\,\)x\(\sb{i}]\))");;
\end{alltt}\end{hol}

\noindent automatically proves the theorem:

\begin{hol}\begin{alltt}
   |-  ?fun. !x\(\sb{1}\) \(\dots\) x\(\sb{i}\). fun 0 x\(\sb{1}\) \(\dots\) x\(\sb{i}\) = \m{f\sb{1}[}x\(\sb{1}\)\(,\ldots,\,\)x\(\sb{i}]\) /\verb!\!
             !x\(\sb{1}\) \(\dots\) x\(\sb{i}\). fun (SUC n) x\(\sb{1}\) \(\dots\) x\(\sb{i}\) = \m{f\sb{2}[}fun n \m{t\sb{1} \dots t\sb{i},} n\(,\) x\(\sb{1}\)\(,\ldots,\,\)x\(\sb{i}]\)
\end{alltt}\end{hol}

\noindent and then declares a new constant \ml{fun} with this property as its
specification. This constant specification is returned as a theorem by 
\ml{new\_prim\_rec\_definition} and is saved with name \ml{fun\_DEF}\index{DEF@$\ldots$\ml{\_DEF}}
in the current theory segment. Failure occurs if:

\begin{myenumerate}
\item \HOL\ cannot prove there is a function satisfying the specification
(\ie\ if the term supplied to \ml{new\_prim\_rec\_definition} 
 is not a well-formed primitive recursive definition);
\item any other condition for making a constant specification is violated
(see the failure conditions for \ml{new\_specification} in 
Section~\ref{conspec}).
\end{myenumerate}

The \ML\  function \ml{new\_prim\_rec\_definition}  is, in  fact, slightly more
general than  is  indicated  by  the  example  application  shown  above.    In
particular, a  curried\index{currying, in ML@currying, in \ML!in primitive recursive definitions}
primitive  recursive  function defined  using this \ML\
function can be defined  by primitive  recursion on  any one  of its arguments.
For example, a curried  addition function  \ml{plus:num->num->num} can be
defined by primitive recursion on its first argument:

\setcounter{sessioncount}{1}
\begin{session}\begin{verbatim}
#let PLUS = new_prim_rec_definition           
#           (`PLUS`,
#            "(plus 0 n = n) /\                     
#             (plus (SUC m) n = SUC(plus m n))");;
PLUS = |- (!n. plus 0 n = n) /\ (!m n. plus(SUC m)n = SUC(plus m n))
\end{verbatim}\end{session}

\noindent or by primitive recursion on its second argument:

\setcounter{sessioncount}{1}
\begin{session}\begin{verbatim}
#let PLUS = new_prim_rec_definition
#            (`PLUS`,
#             "(plus m 0 = m) /\
#              (plus m (SUC n) = SUC(plus m n))");;
PLUS = |- (!m. plus m 0 = m) /\ (!m n. plus m(SUC n) = SUC(plus m n))
\end{verbatim}\end{session}

The \ML\ function \ml{new\_prim\_rec\_definition} also allows the user to
partially specify the value of a function defined (possibly recursively) on the
natural numbers by giving its value for only one of \ml{0} or \ml{SUC n}.  For
example, a decrement function \ml{DEC}, whose value is specified for only
positive natural numbers, can be defined using \ml{new\_prim\_rec\_definition}
as follows

\setcounter{sessioncount}{1}
\begin{session}\begin{verbatim}
#let DEC = new_prim_rec_definition
#            (`DEC`, "DEC (SUC n) = n");;
DEC = |- !n. DEC(SUC n) = n
\end{verbatim}\end{session}

\noindent This definition specifies the value of the function \ml{DEC} only for
positive natural numbers. In particular, the value of \ml{DEC 0} is left
unspecified, and the only non-trivial property that can be proved to hold of
the constant \ml{DEC} is the property stated by the theorem returned by the 
call to \ml{new\_prim\_rec\_definition} shown in the session above.

The function  \ml{new\_infix\_prim\_rec\_definition}\index{new_infix_prim_rec_definition@\ml{new\_infix\_prim\_rec\_definition}}
 can  be used  to define an
infixed\index{infixes, in HOL logic@infixes, in \HOL\ logic!primitive recursive definitions}
 function by primitive recursion on the natural numbers.  It takes its
arguments in the same form as \ml{new\_prim\_rec\_definition} and has similar
failure conditions; the only difference is that the resulting function constant
has infix status.  Here, for example, is the recursive definition of the
constant \ml{+} used by the system:

\begin{hol}\begin{verbatim}
   new_infix_prim_rec_definition
    (`ADD`,
     "($+ 0 n = n) /\
      ($+ (SUC m) n = SUC($+ m n))")
\end{verbatim}\end{hol}

\noindent The  {\small\verb%$%}'s  are  there (as documentation)
  to  indicate  that  the constant
{\small\verb%+%}\index{ addition, in HOL logic@\ml{+} (addition, in \HOL\ logic)}
is  being  declared  to  be  an  infix.   Evaluating this \ML\
expression will  create  the  following  constant specification  in the current
theory:

\begin{hol}\index{ADD@\ml{ADD}}
\begin{verbatim}
   ADD   |- (!n. 0 + n = n) /\ (!m n. (SUC m) + n = SUC(m + n))
\end{verbatim}\end{hol}

For further details about recursive definitions, see
Section~\ref{prim-rec-defs}, or the \REFERENCE\ documentation
on
\ml{new\_prim\_rec\_definition} and \ml{new\_infix\_prim\_rec\_definition}.
\index{prim_rec@\ml{prim\_rec}|)}
\index{primitive recursion theorem!automated use of, in HOL system@automated use of, in \HOL\ system|)}
\index{primitive recursion theorem!for numbers|)}
\index{primitive recursive definitions, in HOL logic@primitive recursive definitions, in \HOL\ logic!automated|)}
\index{recursive definitions, in HOL logic@recursive definitions, in \HOL\ logic!automated, for numbers|)}
\index{type definitions, in HOL logic@type definitions, in \HOL\ logic!primitive recursive|)}

\subsubsection{The less-than relation}

The less-than relation `{\small{\tt\verb+<+}}'\index{ less than, in HOL logic@\ml{<} (less than, in \HOL\ logic)}
  is most  naturally defined by
primitive recursion. However, it  is  needed for  
the proof of the primitive recursion theorem,
so  it  must  be  defined  
before definition  by primitive recursion is available.  
The theory \ml{prim\_rec} therefore  contains the following
non-recursive definition\index{less than, in HOL logic@less than, in \HOL\ logic} of \ml{<}:

\begin{hol}
\index{LESS@\ml{LESS}}
\begin{verbatim}
   LESS  |- !m n. m < n = (?P. (!n'. P(SUC n') ==> P n') /\ P m /\ ~P n)
\end{verbatim}\end{hol}

\noindent
This definition says that {\small\verb%"m < n%"} if there exists a set (with
characteristic function {\small\verb%P%}) that is downward
closed\footnote{A set of numbers is {\it downward closed\/} if whenever it
contains the successor of a number, it also contains the number.} and
contains {\small\verb%m%} but not {\small\verb%n%}.

\subsection{The theory {\tt arithmetic}}


The built-in theory {\small\verb%arithmetic%}\index{number theory, in HOL logic@number theory, in \HOL\ logic}
\index{arithmetic@\ml{arithmetic}} contains primitive recursive
definitions of following standard arithmetic operators.


\begin{hol}
\index{ADD@\ml{ADD}}
\index{SUB@\ml{SUB}}
\index{MULT@\ml{MULT}}
\index{EXP@\ml{EXP}}
\index{ subtraction, in HOL logic@\ml{-} (subtraction, in \HOL\ logic)}
\index{ multiplication, in HOL logic@\ml{*} (multiplication, in \HOL\ logic)}
\begin{verbatim}
   ADD            |- (!n. 0 + n = n) /\ 
                     (!m n. (SUC m) + n = SUC(m + n))

   SUB            |- (!m. 0 - m = 0) /\
                     (!m n. (SUC m) - n = (m < n => 0 | SUC(m - n)))

   MULT           |- (!n. 0 * n = 0) /\ 
                     (!m n. (SUC m) * n = (m * n) + n)

   EXP            |- (!m. m EXP 0 = 1) /\ 
                     (!m n. m EXP (SUC n) = m * (m EXP n))
\end{verbatim}\end{hol}

\noindent It also contains the following non-recursive definitions.

\begin{hol}
\index{arithmetic, in HOL logic@arithmetic, in \HOL\ logic}
\index{ greater than, in HOL logic@\ml{>} (greater than, in \HOL\ logic)}
\index{ less or equal, in HOL logic@\ml{<=} (less or equal, in \HOL\ logic)}
\index{ greater or equal, in HOL logic@\ml{>=} (greater or equal, in \HOL\ logic)}
\index{MOD@\ml{MOD}}
\index{DIV@\ml{DIV}}
\begin{verbatim}
   GREATER        |- !m n. m > n = n < m

   LESS_OR_EQ     |- !m n. m <= n = m < n \/ (m = n)

   GREATER_OR_EQ  |- !m n. m >= n = m > n \/ (m = n)

   DIVISION       |- !n. 0 < n ==> (!k. (k = ((k DIV n) * n) + (k MOD n)) /\ 
                                        (k MOD n) < n)
\end{verbatim}\end{hol}

An \adhoc\ but useful collection of over a hundred elementary theorems of
arithmetic are pre-proved when \HOL\ is built and stored in the theory
{\small\verb%arithmetic%}.  Each theorem will be autoloaded when its name is
first mentioned during any \HOL\ session. For a complete list of available
theorems, see \REFERENCE.

\subsection{The theory {\tt list}}\label{avra_list}\index{list, the type operator in HOL logic@\ml{list}, the type operator in \HOL\ logic} 

\index{recursive definitions, in HOL logic@recursive definitions, in \HOL\ logic!automated for lists|(}
\index{types, in HOL logic@types, in \HOL\ logic!tools for construction of}
\index{lists, in HOL logic@lists, in \HOL\ logic|(}
\index{list theory, in HOL logic@\ml{list} theory, in \HOL\ logic|(}
\index{ lists, in HOL logic@\ml{[} $\cdots$ \ml{;} $\cdots$ \ml{]} (lists, in \HOL\ logic)|(}
The theory \ml{list} introduces the unary type operator \ml{list} by a type
definition.\footnote{For details of the definition,
see~\cite{HOL-paper,Melham-banff}.}  The standard list processing functions
are then defined on this type:

\begin{hol}
\index{NIL@\ml{NIL}}
\index{CONS@\ml{CONS}}
\index{HD, the constant in HOL logic@\ml{HD}, the constant in \HOL\ logic}
\index{TL, the constant in HOL logic@\ml{TL}, the constant in \HOL\ logic}
\index{NULL, the constant in HOL logic@\ml{NULL}, the constant in \HOL\ logic}
\begin{verbatim}
   NIL  : (*)list 
   CONS : * -> (*)list -> (*)list
   HD   : (*)list -> *
   TL   : (*)list -> (*)list
   NULL : (*)list -> bool
\end{verbatim}\end{hol}

The \HOL\ parser\index{parsing, of HOL logic@parsing, of \HOL\ logic!of list expressions} has been specially  modified to  parse the expression
 {\small\verb%[]%} into
{\small\verb%NIL%} and to parse the expression
{\small\verb%[%}$t_1${\small\verb%;%}$t_2${\small\verb%;%}$\ldots${\small\verb%;%}$t_n${\small\verb%]%}
into {\small\verb%CONS %}$t_1${\small\verb% (CONS %}$t_2 \cdots\
${\small\verb%(CONS %}$t_n${\small\verb%  NIL)%}$\  \cdots\ ${\small\verb%)%}.
The \HOL\ printer\index{printing, in HOL logic@printing, in \HOL\ logic!of list expressions}
 reverses these transformations.

The functions \ml{NIL} and \ml{CONS} are defined in terms of the representing
type of lists. From their definitions, the following fundamental theorems about
lists\index{list theorems, in HOL logic@list theorems, in \HOL\ logic|(}
are proved and stored in the theory \ml{list}.

\begin{hol}
\index{list_Axiom@\ml{list\_Axiom}}
\index{axioms!non-primitive, of HOL logic@non-primitive, of \HOL\ logic}
\index{axioms!in list theory@in \ml{list} theory}
\index{list_INDUCT@\ml{list\_INDUCT}}
\index{list_CASES@\ml{list\_CASES}}
\index{CONS_11@\ml{CONS\_{11}}}
\index{NOT_NIL_CONS@\ml{NOT\_NIL\_CONS}}
\index{NOT_CONS_NIL@\ml{NOT\_CONS\_NIL}}
\index{characterizing theorem!for lists}
\begin{verbatim}
   list_Axiom    |- !x f. ?!fn.(fn[] = x) /\ (!h t. fn(CONS h t) = f(fn t)h t)

   list_INDUCT   |- !P. P[] /\ (!t. P t ==> (!h. P(CONS h t))) ==> (!l. P l)

   list_CASES    |- !l. (l = []) \/ (?t h. l = CONS h t)

   CONS_11       |- !h t h' t'. (CONS h t = CONS h' t') = (h = h') /\ (t = t')

   NOT_NIL_CONS  |- !h t. ~([] = CONS h t)

   NOT_CONS_NIL  |- !h t. ~(CONS h t = [])
\end{verbatim}\end{hol}

A derived rule\index{induction rule!for lists, in HOL logic@for lists, in \HOL\ logic}
 of structural induction called \ml{LIST\_INDUCT}\index{LIST_INDUCT@\ml{LIST\_INDUCT}}\index{LIST_INDUCT_TAC@\ml{LIST\_INDUCT\_TAC}} is provided,
together with an associated structural induction tactic \ml{LIST\_INDUCT\_TAC}.
These automate the use of the theorem \ml{list\_INDUCT}. See the \REFERENCE\ 
documentation  on these two functions for details.

The theorem  \ml{list\_Axiom}  shown  above  is  analogous   to  the  primitive
recursion theorem\index{primitive recursion theorem!for lists} on the
natural numbers discussed above in
Section~\ref{num-prim-rec}.  It  states  the  validity  of  primitive recursive
definitions on lists, and can be used to justify any such definition.  The \ML\
functions

\begin{boxed}
\index{new_list_rec_definition@\ml{new\_list\_rec\_definition}|pin}
\index{new_infix_list_rec_definition@\ml{new\_infix\_list\_rec\_definition}}
\begin{verbatim}
   new_list_rec_definition       : (string # term) -> thm
   new_infix_list_rec_definition : (string # term) -> thm
\end{verbatim}\end{boxed}

\noindent use this theorem to do automatic\index{primitive recursion theorem!automated use of, in HOL system@automated use of, in \HOL\ system}
 proofs of the existence of primitive
recursive functions on lists and then make constant specifications to introduce
constants that  denote  such  functions.   They are
analogous to the corresponding functions
\ml{new\_prim\_rec\_definition} and      \ml{new\_infix\_prim\_rec\_definition}
discussed in Section~\ref{num-prim-rec}.  For example, the \HOL\ system defines
a length function, \ml{LENGTH}, on lists  by 
the  primitive recursive  definition on lists
shown below:

\begin{hol}\begin{verbatim}
   new_list_rec_definition
     (`LENGTH`,
     "(LENGTH NIL = 0) /\
      (!h:*. !t. LENGTH (CONS h t) = SUC (LENGTH t))")
\end{verbatim}\end{hol}

\noindent When this \ML\
expression is evaluated, \HOL\ uses \ml{list\_Axiom} to prove existence 
of a function that satisfies the given primitive recursive definition, 
introduces a constant to name this function using a constant specification, and
stores the resulting theorem:


\begin{hol}\begin{verbatim}
    LENGTH   |- (LENGTH[] = 0) /\ (!h t. LENGTH(CONS h t) = SUC(LENGTH t))
\end{verbatim}\end{hol}

\noindent in the current theory (in this case, the theory \ml{list}).  

Using  \ml{new\_list\_rec\_definition},   the  predicate   \ml{NULL}  and  the
selectors \ml{HD} and  \ml{TL} are  defined\index{list definitions, in HOL logic@list definitions, in \HOL\ logic}
 in  the theory  \ml{list} by the
specifications:


\begin{hol}
\index{NULL, the definition in HOL logic@\ml{NULL}, the definition in \HOL\ logic}
\index{HD, the definition in HOL logic@\ml{HD}, the definition in \HOL\ logic}
\index{TL, the definition in HOL logic@\ml{TL}, the definition in \HOL\ logic}
\begin{verbatim}
   NULL |- NULL[] /\ (!h t. ~NULL(CONS h t))
 
   HD   |- !(h:*) t. HD(CONS h t) = h

   TL   |- !(h:*) t. TL(CONS h t) = t
\end{verbatim}\end{hol}

\noindent The following primitive recursive definitions of functions on lists 
are also made in the theory \ml{list}:


\begin{hol}
\index{SUM, the theorem in HOL logic@\ml{SUM}, the theorem in \HOL\ logic}
\index{APPEND, the theorem in HOL logic@\ml{APPEND}, the theorem in \HOL\ logic}
\index{concatenation, of lists!in HOL logic@in \HOL\ logic}
\index{FLAT, the theorem in HOL logic@\ml{FLAT}, the theorem in \HOL\ logic}
\index{LENGTH, the theorem in HOL logic@\ml{LENGTH}, the theorem in \HOL\ logic}
\index{MAP, the theorem in HOL logic@\ml{MAP}, the theorem in \HOL\ logic}
\index{EL, the theorem in HOL logic@\ml{EL}, the theorem in \HOL\ logic}

\index{SUM, the constant in HOL logic@\ml{SUM}, the constant in \HOL\ logic}
\index{APPEND, the constant in HOL logic@\ml{APPEND}, the constant in \HOL\ logic}
\index{FLAT, the constant in HOL logic@\ml{FLAT}, the constant in \HOL\ logic}
\index{LENGTH, the constant in HOL logic@\ml{LENGTH}, the constant in \HOL\ logic}
\index{MAP, the constant in HOL logic@\ml{MAP}, the constant in \HOL\ logic}
\index{EL, the constant in HOL logic@\ml{EL}, the constant in \HOL\ logic}
\index{EVERY, the HOL constant@\ml{EVERY}, the \HOL\ constant}
\index{EVERY_DEF@\ml{EVERY\_DEF}}
\begin{verbatim}
   SUM        |- (SUM[] = 0) /\ (!h t. SUM(CONS h t) = h + (SUM t))

   APPEND     |- (!l. APPEND[]l = l) /\
                 (!l1 l2 h. APPEND(CONS h l1)l2 = CONS h(APPEND l1 l2))

   FLAT       |- (FLAT[] = []) /\ (!h t. FLAT(CONS h t) = APPEND h(FLAT t))

   LENGTH     |- (LENGTH[] = 0) /\ (!h t. LENGTH(CONS h t) = SUC(LENGTH t))

   MAP        |- (!f. MAP f[] = []) /\
                 (!f h t. MAP f(CONS h t) = CONS(f h)(MAP f t))

   EL         |- (!l. EL 0 l = HD l) /\ (!l n. EL(SUC n)l = EL n(TL l))

   EVERY_DEF  |- (!P. EVERY P[] = T) /\
                 (!P h t. EVERY P(CONS h t) = P h /\ EVERY P t)
\end{verbatim}\end{hol}

\noindent There is also a selection of pre-proved theorems about lists stored
in the theory \ml{list}. These are autoloaded when their names are first
mentioned during any \HOL\ session. For a complete list of available theorems,
see \REFERENCE.

\index{list theorems, in HOL logic@list theorems, in \HOL\ logic|)} \index{
lists, in HOL logic@\ml{[} $\cdots$ \ml{;} $\cdots$ \ml{]} (lists, in \HOL\
logic)|)} \index{list theory, in HOL logic@\ml{list} theory, in \HOL\ logic|)}
\index{lists, in HOL logic@lists, in \HOL\ logic|)} \index{recursive
definitions, in HOL logic@recursive definitions, in \HOL\ logic!automated for
lists|)}

\subsection{The theory {\tt combin}}

\index{function composition, in HOL logic@function composition, in \HOL\
logic|(}

The theory \ml{combin}\index{combin@\ml{combin}}\index{combinators, in HOL
logic@combinators, in \HOL\ logic} contains the definitions of function
composition (infixed \ml{o})\index{ function composition operator, in HOL
logic@\ml{o} (function composition operator, in \HOL\ logic)|(}
 and the combinators \ml{S}\index{S, constant in HOL logic@\ml{S}, constant in
\HOL\ logic}, \ml{K}\index{K, the constant in HOL logic@\ml{K}, the constant in
\HOL\ logic}
 and \ml{I}\index{I, constant in HOL logic@\ml{I}, constant in \HOL\ logic}.


\begin{hol} \index{K_DEF@\ml{K\_DEF}} \index{S_DEF@\ml{S\_DEF}}
\index{I_DEF@\ml{I\_DEF}} \begin{verbatim}
   o_DEF |- !f g. f o g = (\x. f(g x))

   K_DEF |- K = (\x y. x)

   S_DEF |- S = (\f g x. f x(g x))

   I_DEF |- I = S K K \end{verbatim}\end{hol}


\noindent The following elementary properties are pre-proved in the theory
\ml{combin}:

\begin{hol} \index{K_THM@\ml{K\_THM}} \index{S_THM@\ml{S\_THM}}
\index{I_THM@\ml{I\_THM}} \index{I_o_ID@\ml{I\_o\_ID}} \begin{verbatim}
   o_THM |- !f g x. (f o g)x = f(g x)

   o_ASSOC |- !f g h. f o (g o h) = (f o g) o h

   K_THM |- !x y. K x y = x

   S_THM |- !f g x. S f g x = f x(g x)

   I_THM |- !x. I x = x

   I_o_ID |- !f. (I o f = f) /\ (f o I = f) \end{verbatim}\end{hol}

Having the symbols \ml{o}, \ml{S}, \ml{K} and \ml{I} as built-in
constants\index{variables, in HOL logic@variables, in \HOL\ logic!with constant
names} is sometimes inconvenient because they are often wanted as mnemonic
names for variables (\eg\ \ml{S} to range over sets and \ml{o} to range over
outputs).  These names may therefore be changed in future releases of the
system, or the theory \ml{combin} may be made into a library.  But variables
(though not constants) with these names can be used in the current system if
\ml{o}, \ml{S}, \ml{K} and \ml{I} are first hidden (see Section~\ref{hidden}).
\index{ function composition operator, in HOL logic@\ml{o} (function
composition operator, in \HOL\ logic)|)} \index{function composition, in HOL
logic@function composition, in \HOL\ logic|)}

\subsection{The theories {\tt tree} and {\tt ltree}} \index{recursive
definitions, in HOL logic@recursive definitions, in \HOL\ logic!automated, for
trees|(}

\index{labelled tree theory, in HOL logic@labelled \ml{tree} theory, in \HOL\
logic|(} The theories \ml{tree}\index{tree, the HOL theory@\ml{tree}, the \HOL\
theory}
 and \ml{ltree}\index{ltree, the HOL theory@\ml{ltree}, the \HOL\ theory|(}
 contain the definitions of two structurally-isomorphic types of
finitely-branching ordered trees.  The types defined in these theories are used
by Tom Melham's\index{Melham, T.} type definition package (see
Section~\ref{types-package}) to construct representations for arbitrary
concrete recursive types.  They are not intended for general use, and the
theorems stored in these two built-in theories are therefore not loaded into
the system at start-up.  The following is a summary of the main theorems which
are available in the theories \ml{tree} and \ml{ltree}, and which may be of use
in certain specialized applications.  For full details of the logical basis for
these two theories, see~\cite{Melham-banff}.

\subsubsection{The theory {\tt tree}}

In the theory \ml{tree}, a type \ml{tree}\index{tree, the HOL type@\ml{tree},
the \HOL\ type} is defined to denote the set of all ordered trees whose nodes
can branch any (finite) number of times.  A constructor function

\index{node@\ml{node}} \begin{hol}\begin{verbatim}
   node : (tree)list -> tree \end{verbatim}\end{hol}

\noindent is then defined in the theory \ml{tree}.  This function can be used
to construct any tree-structured value of type \ml{tree}.  The expression
\ml{"node []"} denotes the tree consisting of a single leaf node with no
subtrees.  If $tl\ml{:(tree)list}$ is a non-empty list of trees, then the term
$\ml{"node }tl\ml{"}$ denotes the tree whose immediate subtrees are the trees
in the list $tl$.  Using \ml{node}, it is possible to construct a tree of any
shape.  For example, the tree

\begin{center}
{\setlength{\unitlength}{0.75mm}
\begin{picture}(60,25)
\thicklines
\put(10,10){\makebox(0,0){$\bullet$}}
\put(30,10){\makebox(0,0){$\bullet$}}
\put(50,10){\makebox(0,0){$\bullet$}}
\put(30,20){\makebox(0,0){$\bullet$}}
\put(44,0){\makebox(0,0){$\bullet$}}
\put(56,0){\makebox(0,0){$\bullet$}}
\put(30,20){\line(0,-1){10}}
\put(30,20){\line(2,-1){20}}
\put(30,20){\line(-2,-1){20}}
\put(50,10){\line(3,-5){6}}
\put(50,10){\line(-3,-5){6}}
\end{picture}}
\end{center}

\noindent is denoted by the term 
\ml{"node[node[]; node[]; node[node[]; node[]]"}.

The next two theorems follow from the formal definition of \ml{node} and
are stored in the theory \ml{tree}:


\begin{hol}
\index{node_11@\ml{node\_{11}}}
\index{tree_Induct@\ml{tree\_Induct}}
\index{induction rule!for trees, in HOL logic@for \ml{trees}, in \HOL\ logic}
\begin{verbatim}
   node_11      |- !tl1 tl2. (node tl1 = node tl2) = (tl1 = tl2)
   tree_Induct  |- !P. (!tl. EVERY P tl ==> P(node tl)) ==> (!t. P t)
\end{verbatim}\end{hol}

\noindent These  two  theorems are  analogous to  the Peano\index{Peano's axioms}  postulates for the
natural numbers, and are used to prove the  following abstract characterization
of the defined type \ml{tree}.


\begin{hol}
\index{tree_Axiom@\ml{tree\_Axiom}}
\index{characterizing theorem!for finitely-branching ordered trees}
\begin{verbatim}
   tree_Axiom  |- !f. ?! fn. !tl. fn(node tl) = f(MAP fn tl)tl
\end{verbatim}\end{hol}

\noindent This theorem states the validity of general `primitive recursive'
definitions of functions over finitely-branching ordered trees.

\subsubsection{The theory {\tt ltree}}

In the theory \ml{ltree}\index{ltree@$\ldots$\ml{ltree}}, a type of {\it
labelled\/} trees (called \ml{(*)ltree}) is defined. Labelled trees have the
same sort of structure as values of the defined type \ml{tree} discussed above.
The only difference is that a tree of type \ml{(*)ltree} has a value or `label'
of type \ml{*} associated with each of its nodes.  A constructor

\begin{hol}
\index{Node@\ml{Node}}
\begin{verbatim}
   Node : * -> (*)ltree -> (*)ltree
\end{verbatim}\end{hol}

\noindent is defined in the theory \ml{ltree}.  The function \ml{Node}
constructs labelled trees by mapping a label of type \ml{*} and a list of
labelled subtrees to a labelled tree of type \ml{(*)ltree}.
The following theorems
 about labelled trees are pre-proved and stored in the
theory \ml{ltree}.


\begin{hol}
\index{Node_11@\ml{Node\_{11}}}
\index{ltree_Induct@\ml{ltree\_Induct}}
\index{ltree_Axiom@\ml{ltree\_Axiom}}
\begin{verbatim}
   Node_11       |- !v1 v2 trl1 trl2.
                    (Node v1 trl1 = Node v2 trl2) = (v1 = v2) /\ (trl1 = trl2)
   ltree_Induct  |- !P. (!t. EVERY P t ==> (!h. P(Node h t))) ==> (!l. P l)
   ltree_Axiom   |- !f. ?! fn. !v tl. fn(Node v tl) = f(MAP fn tl)v tl
\end{verbatim}\end{hol}

\noindent These  theorems  are  analogous to  their counterparts  in the theory
\ml{tree} discussed  above.    The theorems  \ml{Node\_{11}} 
and \ml{ltree\_Induct} amount to a Peano-type characterization of labelled
trees, and the theorem \ml{ltree\_Axiom} is a primitive recursion theorem for
labelled trees.
\index{labelled tree theory, in HOL logic@labelled \ml{tree} theory, in \HOL\ logic|)}
\index{ltree, the HOL theory@\ml{ltree}, the \HOL\ theory|)}
\index{recursive definitions, in HOL logic@recursive definitions, in \HOL\ logic!automated, for trees|)}

\subsection{The theory {\tt tydefs}}

The theory \ml{tydefs}\index{tydefs@\ml{tydefs}}
 is a  technical theory used
to support the type definition package described in
Section~\ref{types-package}.  The main result proved in \ml{tydefs} is a
theorem called \ml{TY\_DEF\_THM}\index{TY_DEF_THM@\ml{TY\_DEF\_THM}},
 which is used by the type definition package
to derive automatically abstract characterizations for
arbitrary concrete recursive types.  The interested reader can find the
details of the derivation of \ml{TY\_DEF\_THM} in~\cite{Melham-banff}.

\subsection{The theory {\tt sum}}
\label{sum}


The theory \ml{sum}\index{sum@\ml{sum}}
 defines the binary  disjoint union\index{disjoint union theory, in HOL
logic@disjoint union theory, in \HOL\ logic|(}  type operator \ml{sum}.
A type  {\small\verb%(%}$\sigma_1${\small\verb%,%}$\sigma_2${\small\verb%)sum%}
denotes the  disjoint  union  of  types  $\sigma_1$  and $\sigma_2$.   The type
operator {\small\verb%sum%} can be defined just as {\small\verb%prod%} was, but
the details are omitted here.\footnote{The definition of disjoint  unions in 
the
HOL system is due to Tom Melham. The technical details of this definition can 
be found in~\cite{Melham-banff}.}  The \HOL\ parser\index{parsing, of HOL logic@parsing, of \HOL\ logic!of sum types}
converts
\ml{":}$\sigma_1${\small\verb%+%}$\sigma_2$\ml{"}\index{ disjoint union
type operator, in HOL logic@\ml{+} (disjoint union
type operator, in HOL logic)} into
\ml{(}$\sigma_1$\ml{,}$\sigma_2$\ml{)sum}, and the printer inverts this.

The standard operations on sums are:


\begin{hol}
\index{disjoint union theory, in HOL logic@disjoint union theory, in \HOL\ logic|)}
\index{INL, the constant in HOL logic@\ml{INL}, the constant in \HOL\ logic}
\index{INR, the constant in HOL logic@\ml{INR}, the constant in \HOL\ logic}
\index{ISL, the constant in HOL logic@\ml{ISL}, the constant in \HOL\ logic}
\index{ISR, the constant in HOL logic@\ml{ISR}, the constant in \HOL\ logic}
\index{OUTL, the constant in HOL logic@\ml{OUTL}, the constant in \HOL\ logic}
\index{OUTR, the constant in HOL logic@\ml{OUTR}, the constant in \HOL\ logic}
\begin{verbatim}
   INL  : *      -> * + ** 
   INR  : **     -> * + **
   ISL  : * + ** -> bool 
   ISR  : * + ** -> bool
   OUTL : * + ** -> * 
   OUTR : * + ** -> **
\end{verbatim}\end{hol}

\noindent These are all defined as constants in the theory \ml{sum}.  The
constants \ml{INL} and \ml{INR} inject into the left and right summands,
respectively. The constants \ml{ISL} and \ml{ISR} test for membership of the
left and right summands, respectively. The constants \ml{OUTL} and \ml{OUTR}
project from a sum to the left and right summands, respectively.

The following two theorems, which are minor variants of each other, are
pre-proved in the built-in theory \ml{sum}. Each one, on its own, provides a
complete and abstract characterization of the disjoint sum type.

\begin{hol}
\index{sum_Axiom@\ml{sum\_Axiom}}
\index{sum_axiom@\ml{sum\_axiom}}
\begin{verbatim}
   sum_axiom   |- !f g. ?! h. (h o INL = f) /\ (h o INR = g)

   sum_Axiom = |- !f g. ?! h. (!x. h(INL x) = f x) /\ (!x. h(INR x) = g x)
\end{verbatim}\end{hol}

\noindent Also provided as built-in, are the following theorems having to
do with the discriminator functions \ml{ISL} and \ml{ISR}:

\begin{hol}
\index{ISL, the theorem in HOL logic@\ml{ISL}, the theorem in \HOL\ logic}
\index{ISR, the theorem in HOL logic@\ml{ISR}, the theorem in \HOL\ logic}
\index{ISL_OR_ISR@\ml{ISL\_OR\_ISR}}
\begin{verbatim}
   ISL         |- (!x. ISL(INL x)) /\ (!y. ~ISL(INR y))

   ISR         |- (!x. ISR(INR x)) /\ (!y. ~ISR(INL y))

   ISL_OR_ISR  |- !x. ISL x \/ ISR x
\end{verbatim}\end{hol}

\noindent The \ml{sum} theory also provides the following built-in theorems:

\begin{hol}
\index{OUTL, the theorem in HOL logic@\ml{OUTL}, the theorem in \HOL\ logic}
\index{OUTR, the theorem in HOL logic@\ml{OUTR}, the theorem in \HOL\ logic}
\index{INL, the theorem in HOL logic@\ml{INL}, the theorem in \HOL\ logic}
\index{INR, the theorem in HOL logic@\ml{INR}, the theorem in \HOL\ logic}
\begin{verbatim}
   OUTL        |- !x. OUTL(INL x) = x

   OUTR        |- !x. OUTR(INR x) = x

   INL         |- !x. ISL x ==> (INL(OUTL x) = x)

   INR         |- !x. ISR x ==> (INR(OUTR x) = x)
\end{verbatim}\end{hol}

\noindent which describe the projection functions \ml{OUTL} and \ml{OUTR}.

\subsection{The theory {\tt one}}%
\index{one, the HOL theory@\ml{one}, the \HOL\ theory}%
\index{one, the HOL type@\ml{one}, the \HOL\ type}%

The theory \ml{one} defines  the type  \ml{":one"} which  contains one element.
The constant  \ml{one}  is specified  to denote  this element.   The pre-proved
theorems in the theory \ml{one} are:

\begin{hol}
\index{one_axiom@\ml{one\_axiom}}
\index{one, the HOL theorem@\ml{one}, the \HOL\ theorem}
\index{one_Axiom@\ml{one\_Axiom}}
\begin{verbatim}
   one_axiom   |- !(f:* -> one) (g:* -> one). f = g
   one         |- !(v:one). v = one
   one_Axiom   |- !(e:*). ?!(fn:one->*). fn one = e
\end{verbatim}\end{hol}

\noindent These three theorems are equivalent characterizations of the type 
with only one value.

\section{The type definition package}\label{types-package}\index{extension, of HOL logic@extension, of \HOL\ logic!by type definition|(}
\index{type definition package, in HOL system@type definition package, in \HOL\ system|(}

In the \HOL\  system, new types and type operators can be introduced\index{extension, of HOL logic@extension, of \HOL\ logic}
using the  consistency-preserving definitional  mechanism  of  
type  definitions\index{type definition extension, in HOL logic@type definition extension, in \HOL\ logic|(} (see Sections~\ref{tydefs} and~\ref{type-defs}).  The \ML\
rule for introducing a new type is:

\begin{hol}
\index{new_type_definition@\ml{new\_type\_definition}}
\begin{verbatim}
   new_type_definition : (string # term # thm) -> thm
\end{verbatim}\end{hol}

\noindent This rule allows
axioms of a restricted form to be added to the primitive basis of the logic.
These axioms are analogous to definitional axioms for new constants: they
define new types in terms of other type expressions already present in the
logic. Like the rule \ml{new\_definition} for making constant definitions, 
the rule  \ml{new\_type\_definition}
 for type definitions
ensures that adding a new syntactic entity (in this case, a type or 
type operator) is a conservative extension of the logic. 

The basic idea behind \ml{new\_type\_definition} is  that a  type definition is
made by  adding an  axiom to  the logic  which asserts  that the  set of values
denoted by a  new type  is isomorphic\index{isomorphism of types, in HOL logic@isomorphism of types, in \HOL\ logic}  to an  appropriate subset  of the values
denoted by  a type  expression already  present in  the logic.   A definitional
axiom\index{definitional axioms} of this form merely states  
that a  new type  is isomorphic  to a particular
subset of an existing type.  From such type definition  axioms, it  is usual to
prove theorems that characterize newly-defined types more abstractly.  The idea
is to prove a collection of theorems that state  the essential  properties of a
new type without reference to how it is defined.   These  theorems then
constitute a derived `abstract axiomatization' of the new type, and 
once  they have  been proved they
become the basis for all further reasoning about it.  

With this approach, introducing a new type (or type operator) in \HOL\
involves two distinct steps:

\setcounter{myenumi}{1}
\begin{list}{\arabic{myenumi}.}{\usecounter{myenumi}
\setlength{\leftmargin}{10mm}
\setlength{\rightmargin}{5mm}
\setlength{\labelwidth}{3mm}
\setlength{\labelsep}{2mm}
\setlength{\listparindent}{0mm}
\setlength{\itemsep}{8pt plus1pt minus2pt}
\setlength{\topsep}{3mm}
\setlength{\parsep}{0mm}}
\setlength{\abovedisplayshortskip}{8pt plus1pt minus1pt} 
\setlength{\belowdisplayshortskip}{8pt plus1pt minus1pt}

\item Finding an appropriate representation for the new type, and making a type \mbox{definition} using \ml{new\_type\_definition} based
 on this representation.

\item Using the axiomatic definition of the new type and the properties of its
representation to prove a set of theorems that abstractly characterizes it.

\end{list}

Defining a new type using this approach can be hard work.  But a set of tools
is provided in the system which---for a certain class of commonly-used {\it
concrete recursive types\/}\index{types, in HOL logic@types, in \HOL\
logic!tools for construction of}\index{concrete recursive types, in HOL
logic@concrete recursive types, in \HOL\ logic}---automatically carries out all
the formal proofs necessary to define these types and derive abstract
characterizations from their definitions.  This section provides a user-level
overview of these tools.  Details of the formal proofs carried out by these
tools are discussed in~\cite{Melham-banff}.

\subsection{Defining types}

\index{type definition package, in HOL system@type definition package, in \HOL\ system!use of, in recursive type definition|(}
\index{recursive types, in HOL logic@recursive types, in \HOL\ logic!tools for construction of|(}
The main \ML\ function in the \HOL\ type definition package is

\begin{boxed}
\index{define_type@\ml{define\_type}|pin}
\begin{verbatim}
   define_type : string -> string -> thm
\end{verbatim}\end{boxed}

\noindent This function can be used to define any concrete recursive type in
the \HOL\ system.  These are types whose values are generated by a set of {\it
constructors\/} (i.e.\ functions) which yield concrete representations for
these values.  Examples include types which denote finite sets of atomic values
(enumerated types), types which denote sets of structured values (record types)
or finite disjoint unions of structured values (variant records), and types
which denote sets of recursive data structures (recursive types).

The two inputs to \ml{define\_type} are both strings.  The first string
is a name  under which the results of making
the type definition will be stored in the current theory segment. The second is
a user-supplied informal\footnote{ In this context, {\it informal\/} means not
in the language of higher order logic.} specification of the concrete
recursive type to be defined.  This type specification is written in 
a notation (explained below) which resembles
a data type declaration in functional programming languages like Standard
\ML~\cite{sml}.  It simply states the names of the new type's
constructors and the logical types of their \mbox{arguments.}  The output is a
theorem which abstractly characterizes the properties of
the desired recursive type---i.e.\ a 
derived `abstract axiomatization' of the type.

\subsubsection{Input syntax}

The type specification given as input\index{type definition package, in HOL system@type definition package, in \HOL\ system!input to|(} to \ml{define\_type}
must be an \ML\ string\index{strings, in ML@strings, in \ML!as input to HOL type definition package@as input to \HOL\ type definition package} (of \ML\ type \ml{string}) of the form:

{\def\op{{\normalsize\sl op}}
\begin{hol}\begin{alltt}
   `{\op} = \(C\sb{1}\;ty{}\sb{1}\sp{1}\;\ldots\;ty{}\sb{1}\sp{k\sb{1}} \) | \(\cdots\) | \(C\sb{m}\;ty{}\sb{m}\sp{1}\;\ldots\;ty{}\sb{m}\sp{k\sb{m}}\)`
\end{alltt}\end{hol}}

\noindent where each $ty_i^{j}$ is either a type expression already defined
as a type in the current theory (this type expression must not
contain \ty{op}) or is the name \ty{op} itself.  A string of this form
describes an $n$-ary type operator \ty{op},
where $n$ is the number of distinct type variables in the types 
$ty_i^{j}$ on the right hand side of the equation.
If $n = 0$ then \ty{op} is a type constant;
otherwise \ty{op} is an $n$-ary type operator.  The concrete 
type described has $m$
distinct constructors \m{C_1, \dots, C_m} where $m \geq 1$.
Each constructor \m{C_i} takes $k_i$ arguments, where $k_i \geq 0$;
and the types of these arguments are given by the type
expressions $ty_i^j$ for $1 \leq j \leq k_i$.  If one or more of the type
expressions $ty_i^{j}$ is the type \ty{op} itself, then the \mbox{equation}
specifies a {\it recursive\/} type.  In any specification of a recursive type,
at least one constructor must be non-recursive---i.e.\ all its arguments must
have types which already exist in the current theory.

The input parser for \ml{define\_type} treats type expressions exactly as the
\HOL\ quotation parser does, with precedences among the various built-in type
operators in force.\index{type definition package, in HOL system@type definition package, in \HOL\ system!input to|)}

\subsubsection{The type specified}

The logical type described by an input string of the form
shown above is intended
to denote the set of all values which can be finitely 
generated using the constructors \m{C_1, \dots, C_m}, 
where each constructor is one-to-one and any two
different constructors yield different values.   Every value of this 
type will be denoted by some term of the form:

\[ C_i\;x_i^1\;\ldots\;x_i^{k_i} \]

\noindent where $x_i^j$ is a term of type $ty_i^j$ for $1 \leq j \leq
k_i$. In addition, any two terms:

\[ C_i\;x_i^1\;\ldots\;x_i^{k_i} \qquad {\rm and} \qquad
   C_j\;x_j^1\;\ldots\;x_j^{k_j} \]

\noindent denote equal values exactly when their constructors are the same
(i.e.\ $i=j$) and these constructors are applied to equal arguments 
(i.e.\ $x_i^n = x_j^n\;\,{\rm for}\;\,1\leq n\leq k_i$).  

\subsubsection{The output}\label{define-type-output}
\index{type definition package, in HOL system@type definition package, in \HOL\ system!output of|(}

\noindent For any type specification 
in the form of an equation of the kind discussed above, executing:

{\def\op{{\normalsize\sl op}}
\begin{hol}
\index{define_type@\ml{define\_type}}
\begin{alltt}
   define\_type `\m{name}` `{\op} = \(C\sb{1}\;ty{}\sb{1}\sp{1}\;\ldots\;ty{}\sb{1}\sp{k\sb{1}} \) | \(\cdots\) | \(C\sb{m}\;ty{}\sb{m}\sp{1}\;\ldots\;ty{}\sb{m}\sp{k\sb{m}}\)`
\end{alltt}\end{hol}}

\noindent will make a formal definition for a  
type (or  type operator) \ty{op}
in the current theory segment, make appropriate definitions for
constants  \m{C_1, C_2,\dots, C_m},
and automatically prove a theorem which
provides an abstract
characterization\index{characterizing theorem!for defined types}\index{automated derivation!of characterizing theorems for recursive types} 
of the newly-defined type \ty{op}.  This theorem, which is
stored in the current theory segment under the name $name$ and also returned by
\ml{define\_type}, has the form shown below:

{\def\op{{\normalsize\sl op}}
\begin{hol}\begin{alltt}
   |- !f\(\sb{1}\:\cdots\:\)f\(\sb{m}\). ?!fn:{\op}->*.
         !x\(\sb{1}\sp{1}\;\,\cdots\,\;\)x\(\sb{1}\sp{k\sb{1}}\). fn(\m{C}\(\sb{1}\,\) x\(\sb{1}\sp{1}\;\,\ldots\,\;\)x\(\sb{1}\sp{k\sb{1}}\)) = f\(\sb{1}\) (fn x\(\sb{1}\sp{1}\))\(\;\ldots\;\)(fn x\(\sb{1}\sp{k\sb{1}}\)) x\(\sb{1}\sp{1}\;\ldots\;\)x\(\sb{1}\sp{k\sb{1}}\)
                                      \(\vdots\)
         !x\(\sb{m}\sp{1}\;\cdots\;\)x\(\sb{1}\sp{k\sb{m}}\!\). fn(\m{C}\(\sb{m}\) x\(\sb{m}\sp{1}\;\ldots\;\)x\(\sb{m}\sp{k\sb{m}}\)) = f\(\sb{m}\) (fn x\(\sb{m}\sp{1}\))\(\;\ldots\;\)(fn x\(\sb{m}\sp{k\sb{m}}\)) x\(\sb{m}\sp{1}\;\ldots\;\)x\(\sb{m}\sp{k\sb{m}}\)
\end{alltt}\end{hol}}     


\noindent where the right hand sides of the equations include recursive
applications `$\ml{fn}\;\ml{x}_i^j$' only for variables  $\ml{x}_i^j$ of type
\ty{op}.  (See the examples given below.) A theorem of this form asserts the
unique existence of primitive recursive functions defined by cases on the
constructors \m{C_1, C_2,\dots,C_m}.  This is a slight
extension of the {\it initiality\/}\index{initiality} property by which
structures of this kind are characterized in the `initial algebra' approach to
specifying abstract data types~\cite{goguen}.  This property provides an
abstract characterization of the type \ty{op} which is both succinct and
complete, in the sense that it completely determines the structure of the
values of \ty{op} up to isomorphism.

The call to \ml{define\_type} shown above fails if:

\begin{myenumerate}
 
\item not in draft mode\index{draft mode, in HOL system@draft mode, in \HOL\ system};

\item \ty{op} is already the name of a type constant or type operator in the
current theory;

\item any one of $C_1,\dots,C_{m}$ is already the name
of a constant in the current theory.

\item either \ty{op} or any one $C_{1},\dots,C_{m}$ is not a
legal identifier.  Identifiers must start with a letter (as defined by
\ml{is\_letter}) and contain only alphanumeric characters (as defined by
\ml{is\_alphanum})

\item $\ml{ABS\_}\ty{op}$\index{ABS_@\ml{ABS\_}$\ldots$}
 or $\ml{REP\_}\ty{op}$\index{REP_@\ml{REP\_}$\ldots$}
 are already constants in the
current theory;

\item there is already an axiom, definition, constant specification or type
definition stored under either the name
$\ty{op}\ml{\_TY\_DEF}$\index{TY_DEF@$\ldots$\ml{\_TY\_DEF}} or the name
$\ty{op}\ml{\_ISO\_DEF}$ in the current
theory segment.

\item there is already a theorem stored under the name \ml{`\m{name}`} in the
current theory segment.

\item the input type specification does not conform to the syntax described
above.

\end{myenumerate}
\index{recursive types, in HOL logic@recursive types, in \HOL\ logic!tools for construction of|)}\index{type definition extension, in HOL logic@type definition extension, in \HOL\ logic|)}
\index{type definition package, in HOL system@type definition package, in \HOL\ system!output of|)}
\index{type definition package, in HOL system@type definition package, in \HOL\ system!use of, in recursive type definition|)}

\subsubsection{Examples}\label{define-type-example}

\index{primitive recursion theorem!a degenerate case|(}
The session that follows illustrates the use of \ml{define\_type} in defining
a variety of simple concrete types.  It is assumed that the session begins
with the user in draft mode.

The first definition is simple, the definition of a type \ml{three} with
exactly three distinct values: \ml{ONE}, \ml{TWO}, and \ml{THREE}.

\setcounter{sessioncount}{1}\label{types-session}
\begin{session}\begin{verbatim}
#let three_Axiom = define_type `three_Axiom` `three = ONE | TWO | THREE`;;
three_Axiom = 
|- !e0 e1 e2. ?! fn. (fn ONE = e0) /\ (fn TWO = e1) /\ (fn THREE = e2)
\end{verbatim}\end{session}

\noindent The theorem returned by \ml{define\_type} provides a complete 
and abstract characterization of
a defined logical type \ml{three} which denotes a set of
exactly three elements.  This characterization takes the form of a
degenerate `primitive recursion'
 theorem for the concrete type \ml{three}. 
Since \ml{three} is an enumerated type with no recursive constructors, 
the theorem returned by \ml{define\_type} simply
states that any function defined by cases on the three constants  \ml{ONE},
\ml{TWO}, and \ml{THREE} exists and is uniquely defined. 

It follows immediately from this theorem that the type constant \ml{three}
denotes a set containing exactly three values: the fact that the function
\ml{fn} always exists implies that the constants \ml{ONE}, \ml{TWO}, and
\ml{THREE} denote distinct values of type \ml{three}, and the fact that \ml{fn}
is uniquely determined by its values for \ml{ONE}, \ml{TWO}, and \ml{THREE}
implies that these constants denote the only values of type \ml{three}.
\index{primitive recursion theorem!a degenerate case|)}

The next call to \ml{define\_type} defines a `record type' \ml{rec}, values of
which are records with three boolean fields (essentially 3-tuples):

\begin{session}\begin{verbatim}
#let rec_Axiom = define_type `rec_Axiom` `rec = REC bool bool bool`;;
rec_Axiom = |- !f. ?! fn. !b0 b1 b2. fn(REC b0 b1 b2) = f b0 b1 b2
\end{verbatim}\end{session}\label{rec-def}

\noindent Here, the resulting theorem states that a function \ml{fn} on
record values of type \ml{rec} can be
uniquely defined in terms of a function \ml{f} of the three components of
the record.

A more interesting {\it recursive\/}
  example is the type of natural 
numbers\index{number theory, in HOL logic@number theory, in \HOL\ logic!type definition package version of}
\index{type definition package, in HOL system@type definition package, in \HOL\ system!use of, to build number theory}, which can be defined using \ml{define\_type} as follows:

\begin{session}\begin{verbatim}
#let nat_Axiom = define_type `nat_Axiom` `nat = Z | Suc nat`;;
nat_Axiom = |- !e f. ?! fn. (fn Z = e) /\ (!n. fn(Suc n) = f(fn n)n)
\end{verbatim}\end{session}

\noindent Here, the input string describes a type \ml{nat} with two
constructors: \ml{Z}, which stands for zero; and \ml{Suc}, which is the
successor function on natural numbers.  (The names 
\ml{Z}, and \ml{Suc} are used here because \ml{0} and \ml{SUC} are already
constants in the built-in \HOL\ theory \ml{num}.)
The output theorem is just the primitive recursion 
theorem\footnote{See Section~\ref{prim_rec} for a discussion of
the primitive recursion theorem.}
for the natural numbers; it states that any primitive recursive definition on
the natural numbers (\ie\ on values of type \ml{nat})
uniquely defines a total function.

A recursive type of labelled binary trees\index{binary tree theory, in HOL logic@binary tree theory, in \HOL\ logic|(}, where labels of type \ml{*}
appear only on leaf nodes, can likewise be defined using \ml{define\_type}.
The input states that a binary tree is either a leaf node (\ml{LEAF})
labelled by a value of type \ml{*} or an internal node \ml{NODE} with
two binary trees as subtrees:

\begin{session}\begin{verbatim}
#let btree_Axiom = 
#    define_type `btree_Axiom` `btree = LEAF * | NODE btree btree`;;
btree_Axiom = 
|- !f0 f1.
    ?! fn.
     (!x. fn(LEAF x) = f0 x) /\
     (!b1 b2. fn(NODE b1 b2) = f1(fn b1)(fn b2)b1 b2)
\end{verbatim}\end{session}\label{btree-def}

\noindent The result returned by the call to {\small \verb!define_type!} is,
in this case, an abstract
characterization for a defined type {\small\verb!(*)btree!},
in the form of a `primitive recursion theorem' for the required
type of labelled binary trees.\index{binary tree theory, in HOL logic@binary tree theory, in \HOL\ logic|)}

Any simple  concrete  recursive  type  can  be  defined  automatically  from  a
user-supplied equation using \ml{define\_type} in exactly the same way.

\subsection{Defining recursive functions}\label{prim-rec-defs}

\index{type definition package, in HOL system@type definition package, in \HOL\ system!use of, in recursive function definition|(}
\index{recursive definitions, in HOL logic@recursive definitions, in \HOL\ logic!automated, for recursive types|(}
\index{primitive recursion theorem!for binary trees|(}
An important property of the characterizing theorems for concrete types
shown in the examples given above is that they
provide a formal
means for defining recursive functions on those types.
When a concrete 
recursive type  \ty{op} is
 characterized by a theorem of the kind returned by
\ml{define\_type}\index{types, in HOL logic@types, in \HOL\ logic!tools for construction of} (see Section~\ref{define-type-output}) this theorem
can be used to 
prove the existence of any 
{\it primitive recursive\/} function on \ty{op} and to
define constants which denote such functions.  

This is illustrated
for a particular
example by the method of defining primitive recursive functions on
the natural numbers  discussed in Section~\ref{num-prim-rec}.  In that section,
an \ML\ function \ml{new\_prim\_rec\_definition}\index{new_prim_rec_definition@\ml{new\_prim\_rec\_definition}}
 was described which automates
the logical inferences necessary to derive particular primitive recursive
definitions on the built-in defined type \ml{num} of natural numbers.  The
basis of this function is the primitive recursion theorem

\begin{hol}
\index{num_Axiom@\ml{num\_Axiom}}
\begin{verbatim}
   num_Axiom   |- !x f. ?!fn. (fn 0 = x) /\ (!n. fn(SUC n) = f (fn n) n)
\end{verbatim}\end{hol}

\noindent which is pre-proved and stored in the built-in theory \ml{prim\_rec}\index{prim_rec@\ml{prim\_rec}}
(see Section~\ref{prim_rec}).  The \ML\ function
\ml{new\_prim\_rec\_definition} uses \ml{num\_Axiom} to automate the
justification of any user-supplied primitive recursive definition on the
natural numbers.

The type definition package\index{primitive recursion theorem!automated use of, in HOL system@automated use of, in \HOL\ system|(} provides a similar function for defining 
primitive recursive functions on
arbitrary concrete recursive
types.\footnote{In fact, {\tt new\_prim\_rec\_definition} is defined in ML
using the more general tools provided by the type definition package.}
The \ML\ function

\begin{boxed}\index{new_recursive_definition@\ml{new\_recursive\_definition}|pin}
\begin{verbatim}
   new_recursive_definition : bool -> thm -> string -> term -> thm
\end{verbatim}\end{boxed}

\noindent automates the
inferences necessary to justify any given primitive recursive definition on a
concrete recursive type of the kind definable by \ml{define\_type}.
 It takes four arguments.  The first is a boolean
flag which indicates if the function to be defined will be an infix\index{infixes, in HOL logic@infixes, in \HOL\ logic!in recursive type definitions} or not.  
The second is the primitive recursion theorem for the concrete type in question
(\ie\ a theorem obtained from {\small\verb!define_type!}).\index{define_type@\ml{define\_type}}  The third
argument is a name under which the resulting definition will be saved in the
current theory segment.
The fourth argument is a term giving the desired primitive recursive
definition.  The value returned
by  {\small\verb!new_recursive_definition!} is a theorem
which states the primitive recursive definition requested by the
user.  This theorem is derived by formal proof from an instance of the general
primitive recursion theorem\index{automated derivation!of recursive definitions}
 given as the second argument.

If the \ML\ variable \ty{op}\ml{\_Axiom} is bound to a theorem of the form
returned by \ml{define\_type},
then evaluating:

{\def\op{{\normalsize\sl op}}
\begin{hol}\begin{alltt}
   new_recursive_definition 
     `\m{flag}` \op\_Axiom `\m{name}` "{\normalsize\it primitive recursive definition on \op}"
\end{alltt}\end{hol}}

\noindent  automatically proves the existence of the primitive recursive
function supplied as the fourth argument, 
and then declares a new constant in the current theory
with this definition as its
specification. This constant specification is returned as a theorem
and is saved in the current theory segment under the name
$name$.
If $flag$ is \ml{true}, the constant is given infix status.
Failure occurs if:

\begin{myenumerate}
\item \HOL\ cannot prove there is a function 
satisfying the defining equations supplied by the user 
(\ie\ the term supplied to \ml{new\_recursive\_definition} 
 is not a well-formed primitive recursive definition on values 
of type \ty{op});
\item any other condition for making a constant specification is violated
(see the failure conditions for \ml{new\_specification} in 
Section~\ref{conspec}).
\end{myenumerate}

Curried\index{currying, in ML@currying, in \ML!in recursive definitions}
functions defined using \ml{new\_recursive\_definition} can be
recursive on any one of their arguments.  Furthermore, defining equations need
not be given for all the constructors of the concrete type in question.  See
the examples given in the next section, or the examples of functions 
defined on \ml{num} given in Section~\ref{num-prim-rec} for more details.

The \ML\ function 

\begin{boxed}
\index{prove_rec_fn_exists@\ml{prove\_rec\_fn\_exists}|pin}
\begin{verbatim}
   prove_rec_fn_exists : thm -> term -> thm
\end{verbatim}\end{boxed}

\noindent is a version of \ml{new\_recursive\_definition} which proves only
that the required function exists; it does not make a constant specification.
The first argument is a theorem of the form returned by \ml{define\_type},
and the second is a user-supplied primitive recursive function definition.
The theorem which is returned asserts the existence of the recursively-defined
function in question (if it is primitive recursive over the type characterized
by the theorem given as the first argument). 
\index{recursive definitions, in HOL logic@recursive definitions, in \HOL\ logic!automated, for recursive types|)}
\index{type definition package, in HOL system@type definition package, in \HOL\ system!use of, in recursive function definition|)}
\index{primitive recursion theorem!automated use of, in HOL system@automated use of, in \HOL\ system|)}

\subsubsection{More examples}

Continuing the example session started above in Section~\ref{define-type-example},
the following interactions with the system show how the \ML\ function
\ml{new\_recursive\_definition} can be used to define functions on concrete types,
which have themselves been defined using \ml{define\_type}.

Given the characterizing theorem
\ml{btree\_Axiom} for the type of labelled binary trees
defined in Section~\ref{types-session}, a recursive function \ml{Leaves}, which
computes the number of leaf nodes in a binary tree, 
can be defined recursively in \HOL\ as shown below:

\begin{session}\begin{verbatim}
#let Leaves = 
#    new_recursive_definition false btree_Axiom `Leaves` 
#      "(Leaves (LEAF (x:*)) = 1) /\
#       (Leaves (NODE t1 t2) = (Leaves t1) + (Leaves t2))";;
Leaves = 
|- (!x. Leaves(LEAF x) = 1) /\
   (!t1 t2. Leaves(NODE t1 t2) = (Leaves t1) + (Leaves t2))
\end{verbatim}\end{session}

\noindent The result of the call to {\small\verb!new_recursive_definition!} is
a theorem which states that the constant {\small\verb!Leaves!} satisfies the
primitive-recursive defining equations supplied by the user.  This theorem is
derived automatically from an instance of the general primitive recursion
theorem for binary trees ({\small\verb!btree_Axiom!}) and an appropriate
constant specification for the constant {\small\verb!Leaves!}. 

The function defined using \ml{new\_recursive\_definition}\index{type
definition package, in HOL system@type definition package, in \HOL\
system!use of, in case definition} need not, in fact, be recursive.
Here is the definition of a predicate \ml{IsLeaf}, which is true of
binary trees which are leaves, but is false of the internal nodes in a
binary tree:

\begin{session}\begin{verbatim}
#let IsLeaf = 
#    new_recursive_definition false btree_Axiom `IsLeaf` 
#      "(IsLeaf (NODE t1 t2) = F) /\ (IsLeaf (LEAF (x:*)) = T)";;
IsLeaf = |- (!t1 t2. IsLeaf(NODE t1 t2) = F) /\ (!x. IsLeaf(LEAF x) = T)
\end{verbatim}\end{session}

\noindent Note that two equations defining a (recursive or non-recursive)
function on binary trees by cases can be given in either order.  Here, the
\ml{NODE} case is given first, and the \ml{LEAF} case second.  The reverse
order was used in the above definition of \ml{Leaves}.

The \ML\ function  {\small\verb!new_recursive_definition!} also allows the user
to partially specify\index{type definition package, in HOL system@type definition package, in \HOL\ system!use of, in partial definition} the value of a function defined on a concrete type, by
allowing defining equations for some of the constructors to be omitted.  Here,
for example, is the definition of a function \ml{Label} which extracts the
label from a leaf node.  The value of \ml{Label} applied to an internal node
is left unspecified:

\begin{session}\begin{verbatim}
#let Label = 
#    new_recursive_definition false btree_Axiom `Label` 
#      "Label (LEAF (x:*)) = x";;
Label = |- !x. Label(LEAF x) = x
\end{verbatim}\end{session}

\index{type definition package, in HOL system@type definition package, in \HOL\ system!use of, in curried infix definition|(} 
Curried functions can also be defined, and the recursion can be on any
argument.  The next definition defines an infix (curried)
function \ml{<<} which expresses the idea that one tree is a proper
subtree of another.

\begin{session}\begin{verbatim}
#let Subtree = 
#    new_recursive_definition true btree_Axiom `Subtree` 
#      "(<< (t:(*)btree) (LEAF (x:*)) = F) /\
#       (<< t (NODE t1 t2) = ((t=t1) \/ (t=t2) \/ (<< t t1) \/ (<< t t2)))";;
Subtree = 
|- (!t x. t << (LEAF x) = F) /\
   (!t t1 t2.
     t << (NODE t1 t2) = (t = t1) \/ (t = t2) \/ t << t1 \/ t << t2)
\end{verbatim}\end{session}

\noindent Note that the first argument to the \ML\ function is \ml{true}
(to indicate that the function being defined is to have infix status) and that
the constant \ml{<<} is an infix after the definition has been made.
Furthermore, the function \ml{<<} is recursive on its second argument\index{type definition package, in HOL system@type definition package, in \HOL\ system!use of, in curried infix definition|)}.

Finally, the function {\small\verb!new_recursive_definition!} can also be used
to define functions by cases on enumerated types.  For example, a predicate
\ml{One}, which is true of only the value \ml{ONE} of the three-valued type
\ml{three} defined above in Section~\ref{types-session}, can be defined as
follows:

\begin{session}\begin{verbatim}
#let One = new_recursive_definition false three_Axiom `One` 
#            "(One ONE = T) /\ (One TWO = F) /\ (One THREE = F)";;
One = |- (One ONE = T) /\ (One TWO = F) /\ (One THREE = F)
\end{verbatim}\end{session}

The existence only of
any function definable using \ml{new\_recursive\_definition} can be proved
using \ml{prove\_rec\_fn\_exists}.  For example:

\begin{session}\begin{verbatim}
#close_theory();;
() : void

#let exists = prove_rec_fn_exists three_Axiom 
#             "(f ONE = T) /\ (f TWO = F) /\ (f THREE = F)";;
exists = |- ?f. (f ONE = T) /\ (f TWO = F) /\ (f THREE = F)
\end{verbatim}\end{session}

\noindent The resulting theorem simply states the existence of the 
required function.  Here, a constant is not defined, and the user need
not be in draft mode.
\index{primitive recursion theorem!for binary trees|)}

\subsection{Structural induction}

\index{type definition package, in HOL system@type definition package, in \HOL\ system!use of, to build induction tools|(} 
\index{induction rule!structural, derivation of|(}
For any concrete recursive type definable 
 using the \HOL\ type definition package there is a structural induction
theorem which states the validity of proof by induction  
on the structure of the type's values.  The \ML\ function

\begin{boxed}
\index{prove_induction_thm@\ml{prove\_induction\_thm}|pin}
\begin{verbatim}
   prove_induction_thm : thm -> thm 
\end{verbatim}\end{boxed}


\noindent can be used to derive a structural induction\index{automated derivation!of structural induction theorems}\index{induction rule!for concrete recursive types}
theorem for any concrete
recursive type defined using \ml{define\_type}.  If the \ML\ 
variable \ty{op}\ml{\_Axiom} is bound to a theorem of the form
returned by \ml{define\_type}, 
then executing 

\[ \ml{prove\_induction\_thm}\;\ty{op}\ml{\_Axiom} \]

\noindent will prove  and  return a  structural induction  theorem for  
the concrete type
\ty{op}.  The `induction' theorem is degenerate in the case of non-recursive
types (see the examples given below). Failure occurs, or an unpredictable 
output theorem is returned, if the input theorem does not have the form
of a theorem  returned by \ml{define\_type}.

\subsubsection{Examples}

A structural induction theorem on the type of binary trees defined in the session
beginning on Section~\ref{types-session} can be proved by:

\begin{session}\begin{verbatim}
#let btree_Induct = prove_induction_thm btree_Axiom;;
btree_Induct =
|- !P.
    (!x. P(LEAF x)) /\ (!b1 b2. P b1 /\ P b2 ==> P(NODE b1 b2)) ==>
    (!b. P b)
\end{verbatim}\end{session}


\noindent The output theorem states that a predicate \ml{P} is true of all
binary trees if it is true of all labelled leaf nodes, and whenever it is true
of two binary trees \ml{b1} and \ml{b2} it is also true of the binary tree
\ml{NODE b1 b2}, in which \ml{b1} and \ml{b2} occur as immediate left and right
subtrees.

For non-recursive types, the induction theorem returned by
\ml{prove\_induction\_thm} is degenerate: there are no `step' cases in the
induction.  For the two types \ml{three} and \ml{rec} defined in the preceding
interactions of this session, the induction theorems are:

\begin{session}\begin{verbatim}
#let three_Induct = prove_induction_thm three_Axiom;;
three_Induct = |- !P. P ONE /\ P TWO /\ P THREE ==> (!t. P t)

#let rec_Induct = prove_induction_thm rec_Axiom;;
rec_Induct = |- !P. (!b0 b1 b2. P(REC b0 b1 b2)) ==> (!r. P r)
\end{verbatim}\end{session}

\noindent Here, induction simply reduces to the consideration of
cases,\index{case analysis, in HOL logic@case analysis, in \HOL\ logic!as instance  of induction} one for each of the constructors for the concrete type involved.
\index{induction rule!structural, derivation of|)}

\subsection{Structural induction tactics}
\label{avrasi}
%I added one paragraph because this section is so out of sequence. Avra 9/11/89.

\index{theorem continuations!use of, in derivation of induction tactics|(}
This section has been included here for reference
because it relates chiefly to the
type definition package, but it involves concepts not defined until
later, in Chapter~\ref{tactics-and-tacticals}. Tactics, goals
and subgoals are
defined in Section~\ref{tactics}; and theorem continuations, in
Section~\ref{asm-manip}. \ml{MAP\_EVERY} is defined in Section~\ref{avra_manip1}.
\ml{ASSUME\_TAC} is defined in Section~\ref{avra_builtin}.
\ml{MP\_TAC}  and \ml{INDUCT\_TAC} can be found in \REFERENCE.

The \ML\ function

\begin{boxed}
\index{INDUCT_THEN@\ml{INDUCT\_THEN}|pin}
\index{induction tactics!derivation of|(}
\begin{verbatim}
   INDUCT_THEN : thm -> (thm -> tactic) -> tactic
\end{verbatim}\end{boxed}

\noindent can be used to generate
a structural induction tactic\index{automated derivation!of structural induction tactics}
for any concrete types definable using \ml{define\_type}.\index{define_type@\ml{define\_type}}  The first argument
is an induction theorem of the form returned by the function
\ml{prove\_induction\_thm}\index{prove_induction_thm@\ml{prove\_induction\_thm}} discussed in the previous section.  The second
argument is a theorem continuation\index{characterizing theorem!use of, in deriving induction} (see
Chapter~\ref{tactics-and-tacticals}) that determines what is to be done with
the induction hypotheses when the resulting tactic is applied to a goal.

If $th$ is an induction theorem for a concrete type \ty{op} with
$m$ constructors  \mbox{$C_1$, \dots, $C_m$}
(\ie\ a theorem of the kind returned by
\ml{prove\_induction\_thm}) and $F$ is a theorem continuation, then the
tactic $\ml{INDUCT\_THEN}\;th\;F$ will reduce a goal 
{\small\verb%(%}$\Gamma${\small\verb%,"!%}$x{:}
\ty{op}${\small\verb%.%}$t[x]${\small\verb%")%} to the collection of $m$
induction subgoals generated by:

\[ \begin{array}[t]{@{}l@{}l}
 \ml{MAP\_EVERY } F \ml{ [}th_1^1\ml{;}\;\ldots\ml{;}\;th_1^{k_1}\ml{]} & 
\ml{ (}\Gamma\ml{, "}t[ C_1\;x_1^1\;\ldots\;x_1^{k_1}]\ml{")},\\
\qquad\qquad \vdots & \mbox{} \\
 \ml{MAP\_EVERY } F \ml{ [}th_m^1\ml{;}\;\ldots\ml{;}\;th_m^{k_m}\ml{]} & 
\ml{ (}\Gamma\ml{, "}t[ C_m\;x_m^1\;\ldots\;x_m^{k_m}]\ml{")}
 \end{array}
\]\index{MAP_EVERY@\ml{MAP\_EVERY}}

\noindent where $th_i^j$ is a theorem of the form $\ml{|- }t[x_i^j]$ asserting
the truth of $t[x_i^j]$ for the $j$th recursive argument (for non-recursive 
arguments, there will be no $th_i^j$ in the list) of the $i$th constructor
$C_i$ (for $1 \leq i \leq m$).

The most common use of \ml{INDUCT\_THEN} is in conjunction with the theorem
continuation \ml{ASSUME\_TAC}.  For example, the built-in
induction tactic \ml{INDUCT\_TAC} for mathematical induction on 
the natural numbers is defined in \ML\ by:

\begin{hol}
\index{INDUCT_TAC@\ml{INDUCT\_TAC}}
\begin{verbatim}
   let INDUCT_TAC = INDUCT_THEN INDUCTION ASSUME_TAC 
\end{verbatim}\end{hol}

\noindent This built-in tactic reduces a goal
 {\small\verb%(%}$\Gamma${\small\verb%,"!%}$n${\small\verb%.%}$t[n]${\small\verb%")%} to a basis subgoal
{\small\verb%(%}$\Gamma${\small\verb%,"%}$t[${\small\verb%0%}$]${\small\verb%")%} 
and a step subgoal 
{\small\verb%(%}$\Gamma\cup\{${\small\verb%"%}$t[n]${\small\verb%"%}$\}${\small\verb%,"%}$t[${\small\verb%SUC %}$n]${\small\verb%")%}.
The extra assumption  {\small\verb%"%}$t[n]${\small\verb%"%} (\ie\ the
induction hypothesis)
is added to the assumptions $\Gamma$ by \ml{ASSUME\_TAC}.  

By contrast, the
induction tactic \ml{INDUCT\_MP\_TAC} (which is not built-in) defined
by:

\begin{hol}\begin{verbatim}
   let INDUCT_MP_TAC = INDUCT_THEN INDUCTION MP_TAC
\end{verbatim}\end{hol}

\noindent reduces a goal
 {\small\verb%(%}$\Gamma${\small\verb%,"!%}$n${\small\verb%.%}$t[n]${\small\verb%")%} to a basis subgoal
{\small\verb%(%}$\Gamma${\small\verb%,"%}$t[${\small\verb%0%}$]${\small\verb%")%} 
and an induction step subgoal 
{\small\verb%(%}$\Gamma${\small\verb%, "%}$t[n]${\small\verb% ==> %}$t[${\small\verb%SUC %}$n]${\small\verb%")%}.
Here, the theorem continuation \ml{MP\_TAC} makes the induction hypothesis
an antecedent of the step subgoal, rather than an assumption.

As this example illustrates, the theorem continuation $F$ in 
an induction tactic

\[ \ml{INDUCT\_THEN }th\;\;F \]

\noindent generated using an induction theorem $th$ can be thought of as a
function which determines what is to be done with the induction hypotheses
corresponding to the recursive arguments of constructors in the step
cases of a proof by structural induction.  When $F$ is \ml{ASSUME\_TAC}, 
the induction hypotheses become assumptions in the subgoals generated; and when
$F$ is \ml{MP\_TAC}, the induction hypotheses become the antecedents of
implicative subgoals.  Other theorem continuations (for which, see
Chapter~\ref{tactics-and-tacticals} and \REFERENCE) can also be used\index{theorem continuations!use of, in derivation of induction tactics|)}.
\index{type definition package, in HOL system@type definition package, in \HOL\ system!use of, to build induction tools|)}\index{induction tactics!derivation of|)} 

\subsection{Other tools}


The function

\begin{boxed}
\index{prove_constructors_one_one@\ml{prove\_constructors\_one\_one}|pin}
\begin{verbatim}
   prove_constructors_one_one : thm -> thm
\end{verbatim}\end{boxed}

\noindent proves that the constructors\index{constructors, of concrete types in HOL logic@constructors, of concrete types in \HOL\ logic!proving one-to-one}
 of a concrete type which take arguments
are one-to-one\index{automated derivation!of one-to-one theorems}.  The argument to \ml{prove\_constructors\_one\_one} is a
theorem of the form returned by \ml{define\_type}.

The function 

\begin{boxed}
\index{prove_constructors_distinct@\ml{prove\_constructors\_distinct}|pin}
\begin{verbatim}
   prove_constructors_distinct : thm -> thm
\end{verbatim}\end{boxed}

\noindent proves that the constructors\index{constructors, of concrete types in HOL logic@constructors, of concrete types in \HOL\ logic!proving distinct}
 of a concrete type yield distinct\index{automated derivation!of
distinctness theorems} values.  The argument to
\ml{prove\_constructors\_distinct} is again 
a theorem of the form returned by \ml{define\_type}.

The function

\begin{boxed}
\index{prove_cases_thm@\ml{prove\_cases\_thm}|pin}
\begin{verbatim}
   prove_cases_thm : thm -> thm
\end{verbatim}\end{boxed}

\noindent proves a cases\index{automated derivation!of case analysis theorems}
 theorem\index{case analysis, in HOL logic@case analysis, in \HOL\ logic!theorems for} for any concrete type.  Such a theorem states that every
value can be constructed using one of the type's constructors.  This property
follows more easily (and therefore is faster to prove) from induction than from
primitive recursion, so the function \ml{prove\_cases\_thm} takes as an
argument an induction theorem of the kind returned by
\ml{prove\_induction\_thm}.\index{prove_induction_thm@\ml{prove\_induction\_thm}}

These auxiliary tools work for any concrete type definable using
\ml{define\_type}.

\subsubsection{Examples}

The following interactions with the system show the proof that the constructor
\ml{LEAF} for the type \ml{(*)btree}  is one-one,
and also that the constructor \ml{REC} for the type \ml{rec} is one-to-one.

\begin{session}\begin{verbatim}
#let LEAF_one_one = prove_constructors_one_one btree_Axiom;;
LEAF_one_one = 
|- (!x x'. (LEAF x = LEAF x') = (x = x')) /\
   (!b1 b2 b1' b2'.
     (NODE b1 b2 = NODE b1' b2') = (b1 = b1') /\ (b2 = b2'))

#let REC_one_one = prove_constructors_one_one rec_Axiom;;
REC_one_one = 
|- !b0 b1 b2 b0' b1' b2'.
    (REC b0 b1 b2 = REC b0' b1' b2') =
    (b0 = b0') /\ (b1 = b1') /\ (b2 = b2')
\end{verbatim}\end{session}

The function \ml{prove\_constructors\_one\_one} fails when the concrete 
type involved has no constructors that take arguments.  For example:

\begin{session}\begin{verbatim}
#let th = prove_constructors_one_one three_Axiom;;
evaluation failed     prove_constructors_one_one: invalid input theorem
\end{verbatim}\end{session}

The function \ml{prove\_constructors\_distinct} returns the theorem stating
that the constructors of a concrete type yield pair-wise distinct values.  For
example:

\begin{session}\begin{verbatim}
#let NOT_LEAF_NODE = prove_constructors_distinct btree_Axiom;;
NOT_LEAF_NODE = |- !x b1 b2. ~(LEAF x = NODE b1 b2)

#let three_distinct = prove_constructors_distinct three_Axiom;;
three_distinct = |- ~(ONE = TWO) /\ ~(ONE = THREE) /\ ~(TWO = THREE)
\end{verbatim}\end{session}

Cases theorems\index{case analysis, in HOL logic@case analysis, in \HOL\ logic!as instance  of induction} are proved from structural induction theorems. For the binary
tree example considered in the present session, here is the cases theorem:

\begin{session}\begin{verbatim}
#let btree_cases = prove_cases_thm btree_Induct;;
btree_cases = |- !b. (?x. b = LEAF x) \/ (?b1 b2. b = NODE b1 b2)
\end{verbatim}\end{session}

\noindent Note that the structural induction theorem for binary trees, 
\ml{btree\_Induct}, is used.
\index{extension, of HOL logic@extension, of \HOL\ logic!by type definition|)}
\index{type definition package, in HOL system@type definition package, in \HOL\ system|)}

\section{Miscellaneous system features}
\label{avramisc}

This section describes some of the features
that exist for managing the interface\index{HOL system@\HOL\ system!adjustment of user interface of} to the
\HOL\ system.  (Other system functions can be found in
Chapter~\ref{sysfuns}.)

\begin{itemize}
\item Flags for controlling the parsing and printing of terms.
\item A mechanism called {\it sticky types\/} allows default types of
variables to be established.
\item A facility called {\it interface maps\/} permits
a limited amount of overloading to be achieved. Interface maps also support
 the use of conventional logical characters on bit-mapped screens.
\item Functions for changing the {\small ASCII}
versions to $\lambda$ and $\vdash$ inside quotations
(the defaults are {\small\verb%\%} and
{\small\verb%|-%} respectively).
\item A method for hiding constants from the quotation parser, so that 
variables
with the same names as constants can be input by quotation.
\item A method for arranging for definitions and theorems (and so on)
to be loaded automatically when their names are encountered by the \ML\ parser.
\item Functions to control whether entire theories are kept in memory
(`cached') or not.
\item A function for adjusting the maximum depth to which terms and 
theorems are printed by the pretty printer (the default is 500).
\item Functions for counting the number of primitive inferences done in
an evaluation, and timing it.
\end{itemize}

\subsection{Flags for the HOL logic}
\label{HOLflags}

\index{HOL system@\HOL\ system!adjustment of user interface of|(}
See also Chapter~\ref{sysfuns} for a description  of the  flag mechanism which
is used  to  control  the  state  of the  \HOL\ system.   The  subset of flags\index{HOL system@\HOL\ system!flags in}\index{flags, in ML@flags, in \ML}
that control aspects of \HOL\ relating to the logic is summarized in the table
below.


\begin{center}
\index{counting inferences, in HOL proofs@counting inferences, in \HOL\ proofs}
\index{inferences, in HOL logic@inferences, in \HOL\ logic!counting of}
\index{printing, in HOL logic@printing, in \HOL\ logic!of types}
\index{types, in HOL logic@types, in \HOL\ logic!printing of}
\index{types, in HOL logic@types, in \HOL\ logic!default}
\index{theory files!pretty printing of}
\index{pretty printing!flags for, in HOL system@flags for, in \HOL\ system}
\index{type checking, in HOL logic@type checking, in \HOL\ logic!verbose errors in}
\index{interface maps}
\index{printing, in HOL logic@printing, in \HOL\ logic!of quantification}
\index{let-terms, in HOL logic@\ml{let}-terms, in \HOL\ logic!pretty printing of}
\index{infixes, in HOL logic@infixes, in \HOL\ logic!pretty printing of}
\index{printing, in HOL logic@printing, in \HOL\ logic!pretty printing}
%\index{printing, in HOL logic@printing, in \HOL\ logic!undischarging 
%IS_ASSUMPTION_OFs in@undischarging \ml{IS\_ASSUMPTION\_OF}s in}
%\index{IS_ASSUMPTION_OF@\ml{IS\_ASSUMPTION\_OF}}
\index{timing@\ml{timing}}
\index{show_types@\ml{show\_types}}
\index{sticky@\ml{sticky}}
\index{theory_pp@\ml{theory\_pp}}
\index{type_error@\ml{type\_error}}
\index{interface_print@\ml{interface\_print}}
\index{print_cond@\ml{print\_cond}}
\index{print_quant@\ml{print\_quant}}
\index{print_let@\ml{print\_let}}
\index{print_list@\ml{print\_list}}
\index{print_uncurry@\ml{print\_uncurry}}
\index{print_infix@\ml{print\_infix}}
\index{function abstraction, in HOL logic@function abstraction, in \HOL\ logic!paired}
\index{function abstraction, in HOL logic@function abstraction, in \HOL\ logic!pretty printing, of paired}
\begin{tabular}{|l|l|l|} \hline
\multicolumn{3}{|c|}{ } \\
\multicolumn{3}{|c|}{\bf Settable system flags} \\
\multicolumn{3}{|c|}{ } \\
{\it Flag} & {\it Function} & 
{\it Default value} \\ \hline
 & &  \\
\ml{timing} &    Print number of theorems proved& \ml{false}\\ \hline

\ml{show\_types} &    Prints types in quotations   &    \ml{false}\\ \hline

\ml{sticky}     &         Activates sticky types   &        \ml{false}\\ \hline


\ml{theory\_pp} & Pretty printing of theory files &   \ml{false} \\ \hline

\ml{type\_error} & Verbose type checking errors in quotations& \ml{true} \\ \hline

\ml{interface\_print}  &   Causes inverse of interface map &     \ml{true}\\[-1mm]
 &                       to be used when printing & \\ \hline

\ml{print\_cond} & Pretty print \HOL\ conditionals  &      \ml{true}\\ \hline

\ml{print\_quant} &   Pretty print \HOL\ quantifications &     \ml{true}\\ \hline

\ml{print\_let} &   Pretty print \HOL\ \ml{let}-expressions   &\ml{true}\\ \hline

\ml{print\_list}   &       Pretty print \HOL\ lists &           \ml{true}\\ \hline

\ml{print\_uncurry} & Pretty print \HOL\ paired abstractions & \ml{true}\\ \hline

\ml{print\_infix} &    Pretty print \HOL\ infixes & \ml{true}\\ \hline
\end{tabular}
\end{center}


\subsection{Sticky types and default types}
\label{stickytypes}

\index{sticky types, in HOL logic@sticky types, in \HOL\ logic|(}
\index{types, in HOL logic@types, in \HOL\ logic!default|(}
\index{types, in HOL logic@types, in \HOL\ logic!sticky|(}
\index{type checking, in HOL logic@type checking, in \HOL\ logic!sticky types in|(}
\index{HOL system@\HOL\ system!sticky types in|(}
\index{default types, in HOL logic@default types, in \HOL\ logic|(}
The quotation type checker  normally requires that there be enough information
in a quotation to fully determine the types of all subterms of the term being 
type checked. This information comes from two sources:

\begin{myenumerate}
\item the generic\index{types, in HOL logic@types, in \HOL\ logic!generic}
 types of constants, and 
\item explicit type\index{types, in HOL logic@types, in \HOL\ logic!explicit printing of}
 information given after a colon.
\end{myenumerate}

\noindent If sticky types are  activated (by  setting the  flag \ml{sticky} to
\ml{true}) then the last type a variable had in  a session  is remembered, and
this is used as a default type during type checking.   The sticky  type is only
used, however, if the variable in question is completely  unconstrained by its
context in the quotation.  If the context partially  determines the  type of a
variable, then sticky types are not used.  For example, in the term \ml{"f 1"}
the variable \ml{f} is constrained to have a function type, but the range type
is not  determined.    In  the quotation  \ml{"(f,1)"} the  variable \ml{f} is
completely unconstrained.   In  the latter  case an  (appropriate) sticky type
would resolve the typing, but in the former  it would  not.   Sticky types can
never cause  the type checking  of a  quotation to  fail when  it would succeed
without them.

\setcounter{sessioncount}{1}
\begin{session}\begin{verbatim}
#set_flag(`sticky`,true);;
false : bool

#"f:num->num";;
"f" : term

#"f 1";;
Indeterminate types:  "f:num -> ?"

evaluation failed     types indeterminate in quotation

#"f";;
"f" : term
\end{verbatim}\end{session}

A name can be given a sticky type explicity with the function:

\begin{boxed}
\index{set_sticky_type@\ml{set\_sticky\_type}|pin}
\begin{verbatim}
   set_sticky_type : string # type -> void
\end{verbatim}\end{boxed}

\noindent  This sets sticky types whether or not sticky
types are active.

Note that the flag \ml{sticky} controls whether types  are automatically stuck
onto names; it does not control  whether such  sticky types  are actually used
during type checking:  sticky types are always used if they are defined.

Sticky types can be removed with the function:

\begin{boxed}
\index{remove_sticky_type@\ml{remove\_sticky\_type}|pin}
\begin{verbatim}
   remove_sticky_type : string -> type
\end{verbatim}\end{boxed}

\noindent The sticky type is returned (failure if the variable does not 
have a sticky type). A function to return the sticky type of a variable
can be defined by:

\begin{hol}\begin{verbatim}
   let sticky_type v =
    let ty = remove_sticky_type v
    in
    (set_sticky_type(v,ty);ty)
\end{verbatim}\end{hol}

\noindent The list of sticky types active in a session is computed by the 
function:

\begin{boxed}
\index{sticky_list@\ml{sticky\_list}|pin}
\begin{verbatim}
   sticky_list : void -> (string # type) list
\end{verbatim}\end{boxed}\index{default types, in HOL logic@default types, in \HOL\ logic|)}\index{HOL system@\HOL\ system!sticky types in|)}\index{type checking, in HOL logic@type checking, in \HOL\ logic!sticky types in|)}
\index{types, in HOL logic@types, in \HOL\ logic!sticky|)}
\index{types, in HOL logic@types, in \HOL\ logic!default|)}
\index{sticky types, in HOL logic@sticky types, in \HOL\ logic|)}

\subsection{Interface maps}

An interface map\index{interface maps|(}\index{HOL system@\HOL\ system!interface maps in|(} is a list of pairs of strings:

\begin{hol}\begin{alltt}
   [`\m{a\sb{1}}`,`\m{c\sb{1}}`; \m{\ldots} ;`\m{a\sb{n}}`,`\m{c\sb{n}}`]
\end{alltt}\end{hol}


If such a map is active, then whenever $a_i$ (for $1\leq i \leq n$) occurs as a
constant or  variable  in  a quoted  term, it  is translated  (by the quotation
parser) to  $c_i$,  which  must  be  an  existing constant  (`$a$' is for
`abbreviation' and `$c$' for `constant').

The function:

\begin{boxed}
\index{set_interface_map@\ml{set\_interface\_map}|pin}
\begin{verbatim}
   set_interface_map : string list -> string list
\end{verbatim}\end{boxed}

\noindent installs an interface map (the previous map is undone and returned). 
The effect of executing:

\begin{hol}\begin{alltt}
   set_interface_map [`\m{a\sb{1}}`,`\m{c\sb{1}}`; \m{\ldots} ;`\m{a\sb{n}}`,`\m{c\sb{n}}`];;
\end{alltt}\end{hol}

\noindent is to install 
\ml{[`\m{a_1}`,`\m{c_1}`;\m{\ \ldots\ } ;`\m{a_n}`,`\m{c_n}`]}
as the current interface map.  Any
binder\index{binders, in HOL logic@binders, in \HOL\ logic!under interface maps} or infix\index{infixes, in HOL logic@infixes, in \HOL\ logic!under interface maps} status (including precedences)\index{precedence, in HOL logic@precedence, in \HOL\ logic!under interface maps} of $c_i$ is propagated 
to $a_i$ in the order:


\[ {\it status\/}(c_1)\;\;\leadsto\;\; a_1\;\; {\rm then}\;\;
   {\it status\/}(c_2)\;\;\leadsto\;\; a_2\;\; {\rm then}\;\;\;
    \ldots\;\;\;{\rm then}\;\; {\it status\/}(c_n)\;\;\leadsto\;\;a_n \]



\noindent This order can be important. For example, if $ix$ is the 
name of an
infixed constant and $c$ the name of a non-infixed 
constant, then executing:

{\def\con#1{\mbox{\normalsize\sf #1}}
\begin{hol}\begin{alltt}
   set\_interface\_map[`\m{c}`,`\m{ix}`; `\m{ix}`,`\m{c}`];;
\end{alltt}\end{hol}}


\noindent will result in both $c$ and $ix$ being infixes; but 
executing:

{\def\con#1{\mbox{\normalsize\sf #1}}
\begin{hol}\begin{alltt}
   set\_interface\_map[`\m{ix}`,`\m{c}`; `\m{c}`,`\m{ix}`];;
\end{alltt}\end{hol}}


\noindent results in neither $c$ nor $ix$ being an infix:

The current interface map is given by:


\begin{boxed}
\index{interface_map@\ml{interface\_map}|pin}
\begin{verbatim}
   interface_map : void -> string list
\end{verbatim}\end{boxed}

\index{printing, in HOL logic@printing, in \HOL\ logic!under interface maps|(}
To avoid parsing and printing ambiguities, maps must be  single valued (\ie\
one  abbreviation  cannot  abbreviate  two  constants)  and one-to-one (\ie\
different abbreviations must map to  different constants).   Furthermore, if
$a_i$ is already a constant  then it  must be  given an  abbreviation by the
map.  For example:

\begin{hol}\begin{verbatim}
   set_interface_map[`+`,`APPEND`];;
\end{verbatim}\end{hol}

\noindent is not allowed because it would make it unclear how to print 
pre-existing terms involving \ml{+}. To avoid this problem, an abbreviation 
for the old \ml{+} must also be provided.  

The flag \ml{interface\_print}\index{interface_print@\ml{interface\_print}}
 determines whether the inverse of the current
interface map is applied when printing.
This should be useful for debugging as
it shows what is `really there'\index{printing, in HOL logic@printing, in \HOL\ logic!under interface maps|)}.

The following functions are also provided:


\begin{boxed}
\index{is_constant@\ml{is\_constant}|pin}
\index{is_infix@\ml{is\_infix}|pin}
\index{is_binder@\ml{is\_binder}|pin}
\index{constants, in HOL logic@constants, in \HOL\ logic!indicator function for}
\begin{verbatim}
   is_constant : string -> bool
   is_infix    : string -> bool
   is_binder   : string -> bool
\end{verbatim}\end{boxed}

\noindent these tell whether a string is the name of a constant, infix\index{infixes, in HOL logic@infixes, in \HOL\ logic!indicator functions for} or 
binder\index{binders, in HOL logic@binders, in \HOL\ logic!indicator functions for} respectively (note: being an infix or binder entails being a constant).

The function

\begin{boxed}
\index{allowed_constant@\ml{allowed\_constant}|pin}
\begin{verbatim}
   allowed_constant : string -> bool
\end{verbatim}\end{boxed}

\noindent tests whether a string has the correct lexical structure to be a 
constant.

The function:

\begin{boxed}
\index{draft_mode@\ml{draft\_mode}|pin}
\begin{verbatim}
   draft_mode : void -> bool
\end{verbatim}\end{boxed}

\noindent returns \ml{true} in draft mode\index{draft mode, in HOL system@draft mode, in \HOL\ system}\footnote{See Section~\ref{theoryfns}
for an explanation of `draft mode'.} and \ml{false} otherwise.

The following sessions illustrate the use of interface maps (the comments are
provided by the author, not by the system). They
also show the great potential of interface maps for
generating confusion! The first session illustrates checking that
interface maps are well formed.

\setcounter{sessioncount}{1}
\begin{session}\begin{verbatim}
#set_interface_map[`+`,`APPEND`];;
evaluation failed     + would become hidden 

#set_interface_map[`+`,`APPEND`;`+`,`++`];;
evaluation failed     interface map not single valued 

#set_interface_map[`+`,`APPEND`;`++`,`+`];;
[] : (string # string) list
\end{verbatim}\end{session}

\noindent The next session shows the propagation of infix status by the interface map declared above:

\begin{session}\begin{verbatim}
#"1 ++ 2";;                           % ++ is not an infix. %
Badly typed application of:  "1"
   which has type:           ":num"
to the argument term:        "++"
   which has type:           ":num -> (num -> num)"

evaluation failed     mk_comb in quotation 

#"++ 1 2";;
"++ 1 2" : term

#set_interface_map[`++`,`+`; `+`,`APPEND`];;
[(`+`,`APPEND`); (`++`,`+`)] : (string # string) list

#"1 ++ 2";;
"1 ++ 2" : term
\end{verbatim}\end{session}

\noindent Setting the flag \ml{interface\_print} to \ml{false}
causes the true form of terms to be shown.

\begin{session}\begin{verbatim}
#set_flag(`interface_print`, false);;
true : bool

#"1 ++ 2";;
"1 + 2" : term

#dest_const "++";;           % This illustrates potential for confusion. %
`+`,":num -> (num -> num)" : (string # type)
\end{verbatim}\end{session}

\noindent Continuing:
\vfill
\newpage
\begin{session}\begin{verbatim}
#"[1]+[2]";;                 % APPEND is not an infix. %
Badly typed application of:  "[1]"
   which has type:           ":(num)list"
to the argument term:        "APPEND"
   which has type:           ":(?1)list -> ((?1)list -> (?1)list)"

evaluation failed     mk_comb in quotation 

#"+[1][2]";;
"APPEND[1][2]" : term

#"APPEND [1] [2]";;
"APPEND[1][2]" : term
\end{verbatim}\end{session}

\noindent Here is an example illustrating the kind of thing to avoid.

\begin{session}\begin{verbatim}
#ADD1;;                     % Built in theorem. %
Theorem ADD1 autoloaded from theory `arithmetic`.
ADD1 = |- !m. SUC m = m + 1

|- !m. SUC m = m + 1

#set_flag(`interface_print`, true);;
false : bool

#ADD1;;
|- !m. SUC m = m ++ 1

#set_interface_map[`+`,`-`; `-`,`+`];;
[`++`,`+`; `+`,`APPEND`] : (string # string) list

#ADD1;;
|- !m. SUC m = m - 1
\end{verbatim}\end{session}

There are some subtleties and rough edges to the current implementation
of interface maps. For example, any special parsing or printing properties
of special constants (\ml{!}, \ml{?}, {\small\verb%/\%}, {\small\verb%\/%},
\etc) are transferred to the names that abbreviate them. For example, notice the 
disappearing spaces in the next session.

\setcounter{sessioncount}{1}
\begin{session}\begin{verbatim}
#set_interface_map[`Forall`,`!`; `Exists`,`?`];;
[] : (string # string) list

#"Forall x. Exists y. x < y";;
"Forallx. Existsy. x < y" : term
\end{verbatim}\end{session}

\noindent This happens because the printer does not print spaces after
\ml{!} and \ml{?} and this behaviour gets transferred to \ml{Forall} and
\ml{Exists} by the interface map.
It would be straightforward, but rather messy, to have the printer insert 
spaces after \ml{Forall} and \ml{Exists}. This will be implemented, and other 
changes or additions, if experience indicates it is sensible.
Interface maps are still rather
experimental, and it is expected that various details will need 
modification as experience is gained. A feature 
not currently implemented, but possibly useful, would
allow the relative precedences of user-defined infixes to be adjusted.
\index{HOL system@\HOL\ system!interface maps in|)}
\index{interface maps|)}

\subsection{Changing the lambda symbol}
\label{change-lambda}

\index{lambda symbol in HOL logic, resetting@lambda symbol, in \HOL\ logic, resetting|(} 
\index{customization of HOL system@customization of \HOL\ system|(}
\index{function abstraction, in HOL logic@function abstraction, in \HOL\ logic!changing symbol for|(}
\index{HOL system@\HOL\ system!changeable symbols of|(}
\index{symbols in HOL logic, changeable@symbols in \HOL\ logic, changeable|(}

The \ML\ function:

\begin{boxed}
\index{set_lambda@\ml{set\_lambda}|pin}
\begin{verbatim}
   set_lambda : string -> string
\end{verbatim}\end{boxed}

\noindent allows  an  alternative symbol  (or string)  to be  used to represent
lambda ($\lambda$)  inside  quotations.\index{function abstraction, in HOL logic@function abstraction, in \HOL\ logic!changing symbol for}
The  previous $\lambda$-representing
string is returned.  Note that after calling \ml{set\_lambda}:

\begin{itemize}

\item  The symbol  {\small\verb%\%}\index{ function abstraction binder, in HOL logic@{\small\verb+\+} (function abstraction binder, in \HOL\ logic)}
 is  still available for input.

\item All abstractions will be printed with the new string.


\item It is necessary to use:
{\verb%set_lambda `\\`%}
to restore the alternative lambda to {\small\verb%\%}\index{ escape, in ML strings@{\small\verb+\+} (escape, in \ML\ strings)} 
(since {\small\verb%\%} is the escape character inside \ML\ strings).
\end{itemize}

\noindent For example:

\setcounter{sessioncount}{1}
\begin{session}\begin{verbatim}
#set_lambda `Lambda`;;
`\` : string

#"Lambda x.x+1";;
"Lambda x. x + 1" : term

#"\x.x+1";;
"Lambda x. x + 1" : term
\end{verbatim}\end{session}
\index{lambda symbol in HOL logic, resetting@lambda symbol, in \HOL\ logic, resetting|)} 

\subsection{Changing the turnstile symbol}
\label{turnstile}

The turnstile symbol {\small\verb%|-%}, which is used as an {\small ASCII}
approximation to $\vdash$ when printing  theorems, can  be changed  with the 
\ML\ function:

\begin{boxed}
\index{set_turnstile@\ml{set\_turnstile}|pin}
\begin{verbatim}
   set_turnstile : string -> string
\end{verbatim}\end{boxed}

\noindent The previous representation of turnstile is returned. For example:

\setcounter{sessioncount}{1}
\begin{session}\begin{verbatim}
#REFL "x:num";;
|- x = x

#set_turnstile `Proved! `;;
`|- ` : string

#REFL "x:num";;
Proved! x = x

#set_turnstile `       |-  `;;
`Proved! ` : string

#REFL "x:num";;
       |-  x = x
\end{verbatim}\end{session}
\index{customization of HOL system@customization of \HOL\ system|)}
\index{function abstraction, in HOL logic@function abstraction, in \HOL\ logic!changing symbol for|)}
\index{HOL system@\HOL\ system!changeable symbols of|)}
\index{symbols in HOL logic, changeable@symbols in \HOL\ logic, changeable|)}

\subsection{Hiding constants}
\label{hidden}

\index{parsing, of HOL logic@parsing, of \HOL\ logic!hiding constant status in|(}
\index{HOL system@\HOL\ system!hiding constants in|(}
The following function can be used to hide\index{constants, in HOL logic@constants, in \HOL\ logic!hiding status of|(} the constant  status of  a name from
the quotation parser.

\begin{boxed}
\index{hide_constant@\ml{hide\_constant}|pin}
\begin{verbatim}
   hide_constant : string -> void
\end{verbatim}\end{boxed}


\noindent Evaluating \ml{hide\_constant\ `}$x$\ml{`}
makes the quotation parser treat $x$ as a variable (lexical
rules permitting), even if $x$ is the name of a constant in the current theory
(constants and variables can have the same name).  
This is useful if one wants to use variables\index{variables, in HOL logic@variables, in \HOL\ logic!with constant names}  with the same names
as previously declared (or built-in) constants (\eg\ \ml{o}, \ml{I}, \ml{S} 
\etc). 
The name $x$ is still a
constant for the constructors, theories, etc; \ml{hide\_constant} 
affects only  parsing.

Hiding a constant and then attempting to declare it as a new
constant will fail (as it must, if the system is to remain sound).\index{soundness!of HOL logic@of \HOL\ logic}\index{constants, in HOL logic@constants, in \HOL\ logic!hiding status of|)}

The function

\begin{boxed}
\index{unhide_constant@\ml{unhide\_constant}|pin}
\begin{verbatim}
   unhide_constant : string -> void
\end{verbatim}\end{boxed}

\noindent undoes the hiding; it fails if its argument is not a previously 
hidden constant.

The function:

\begin{boxed}
\index{is_hidden@\ml{is\_hidden}|pin}
\begin{verbatim}
   is_hidden : string -> bool
\end{verbatim}\end{boxed}

\noindent tests whether a string is the name of a hidden constant.
\index{HOL system@\HOL\ system!adjustment of user interface of|)}
\index{HOL system@\HOL\ system!hiding constants in|)}
\index{parsing, of HOL logic@parsing, of \HOL\ logic!hiding constant status in|)}

\subsection{Autoloading of axioms, definitions and theorems}\index{axioms!autoloading of, in HOL system@autoloading of, in \HOL\ system}

It is possible to mark the name of an axiom, definition or  theorem so that
if it occurs in an \ML\ expression  then the  named item  will be automatically
loaded\index{loading, of HOL theories@loading, of \HOL\ theories}\index{automatic loading, of HOL theory components@automatic loading, of \HOL\ theory components} from  the appropriate  theory before  the \ML\  expression is evaluated.
This provides a kind of crude `paging'\index{theories, in HOL logic@theories, in \HOL\ logic!paging of} of theories.   Many standard definitions
and theorems are set up to autoload
 if they are used.

The function to set up an autoloading action is:

\begin{boxed}
\index{autoload_theory@\ml{autoload\_theory}|pin}
\begin{verbatim}
   autoload_theory : (string # string # string) -> void
\end{verbatim}\end{boxed}

\noindent Evaluating
\ml{autoload\_theory(`}$kind$\ml{`,`}$thy$\ml{`,`}$name$\ml{`)}, where   $kind$
is \ml{axiom}, \ml{definition} or \ml{theorem}, has the  side effect of setting
the name  $name$  so  that  when  it  is  encountered by  the  \ML\ parser the
appropriate sort of object will be autoloaded from the theory $thy$.   Note that
constant specifications\index{constant specifications, in HOL logic@constant specifications, in \HOL\ logic!autoloading of}\index{type definitions, in HOL logic@type definitions, in \HOL\ logic!autoloading of} and type definitions are  regarded as  special cases of
definitions.

An autoloading action set up with \ml{autoload\_theory} will only be done once,
namely the first time the name is encountered in the session.  Autoload actions
can be removed from a name using the function:

\begin{boxed}
\index{undo_autoload@\ml{undo\_autoload}|pin}
\begin{verbatim}
   undo_autoload : string -> bool
\end{verbatim}\end{boxed}

The value \ml{true} is returned
if an autoload action had been set up, \ml{false} is returned otherwise.

\subsection{Cached theories}

When a  theory  is  first  accessed  using   the  functions  \ml{load\_theory},
\ml{axiom}, \ml{definition}, \ml{theorem} \etc, the  whole theory  is read from
disk into a data-structure in memory called a {\it theory cache\/}.\index{theories, in HOL logic@theories, in \HOL\ logic!caching of}\index{caching}\index{theory caching}\index{HOL system@\HOL\ system!caching theories in}  Subsequent
accesses then refer to this in-memory cache  and are  therefore faster.   Theories,
however, can be very large, and on machines with limited memory,
this can  lead to a lot of
garbage collection, or even running out of space.  To deal with
this problem, the \ML\ function:

\begin{boxed}
\index{delete_cache@\ml{delete\_cache}|pin}
\begin{verbatim}
   delete_cache : string -> void
\end{verbatim}\end{boxed}


\noindent can be used to delete the theory cache (but not the theory 
file on disk), thereby 
freeing up some space (at the cost of making the next theory access slower). 
For example, a function that fetches a single theorem without 
bringing in the whole theory is:

\begin{hol}\begin{verbatim}
   let fetch_thm_without_caching thy thm =
       let th = theorem thy thm
       in  (delete_cache thy; th);;
\end{verbatim}\end{hol}

Whether  a theory has been cached or not can be discovered with the function:

\begin{boxed}
\index{cached_theories@\ml{cached\_theories}|pin}
\begin{verbatim}
   cached_theories : void -> (string # bool) list
\end{verbatim}\end{boxed}

\noindent This returns a list of pairs 
\ml{(}$thy$\ml{,}$b$\ml{)} where $thy$ is the name of 
a theory that has been loaded and
$b$ is a truth value that is \ml{true} if $thy$'s cache has been deleted with
\ml{delete\_cache} and \ml{false} otherwise.

\subsection{Adjusting the pretty-print depth}

\index{ML@\ML!pretty printer for|(}
The following \ML\ function  can be used to adjust the maximum depth of 
printing\index{printing, in HOL logic@printing, in \HOL\ logic!structural depth adjustment in}.

\begin{boxed}
\index{max_print_depth@\ml{max\_print\_depth}|pin}
\begin{verbatim}
   max_print_depth : int -> int
\end{verbatim}\end{boxed}

\noindent The default print depth\index{default print depth, for HOL logic@default print depth, for \HOL\ logic|(} is $500$. Evaluating
\ml{max\_print\_depth}$\ n$ sets the maximum to $n$ and returns 
the previous value
of the maximum. Subterms nested more deeply than 
the maximum print depth are printed as
{\small\verb%&%}. For example:

\setcounter{sessioncount}{1}
\begin{session}\begin{verbatim}
#ADD_CLAUSES;;
Theorem ADD_CLAUSES autoloaded from theory `arithmetic`.
ADD_CLAUSES = 
|- (0 + m = m) /\
   (m + 0 = m) /\
   ((SUC m) + n = SUC(m + n)) /\
   (m + (SUC n) = SUC(m + n))

|- (0 + m = m) /\
   (m + 0 = m) /\
   ((SUC m) + n = SUC(m + n)) /\
   (m + (SUC n) = SUC(m + n))

#max_print_depth 7;;
500 : int

#ADD_CLAUSES;;
|- (& + & = m) /\ (& + & = m) /\ ((& + & = &(&) /\ (& + (& = &(&)

#max_print_depth 5;;
7 : int

#ADD_CLAUSES;;
|- (& /\ (& /\ (& /\ (&

#max_print_depth 3;;
5 : int

#ADD_CLAUSES;;
|- &
\end{verbatim}\end{session}
\index{default print depth, for HOL logic@default print depth, for \HOL\ logic|)}

\noindent For more details about pretty printing in \ML, see
Section~\ref{pretty-print}.
\index{ML@\ML!pretty printer for|)}

\subsection{Timing and counting theorems}

Whenever \HOL\  performs  a  primitive  inference  (or  accepts   an  axiom  or
definition) a counter\index{inferences, in HOL logic@inferences, in \HOL\ logic!counting of}\index{timing of HOL evaluations@timing of \HOL\ evaluations}\index{HOL system@\HOL\ system!timing and counting inferences in}  is incremented.  The value of this counter is returned by
the function:

\begin{boxed}
\index{thm_count@\ml{thm\_count}|pin}
\index{counting inferences, in HOL proofs@counting inferences, in \HOL\ proofs}
\begin{verbatim}
   thm_count : void -> int 
\end{verbatim}\end{boxed}

\noindent This counter can be reset with the function:

\begin{boxed}
\index{set_thm_count@\ml{set\_thm\_count}|pin}
\begin{verbatim}
   set_thm_count : int -> int
\end{verbatim}\end{boxed}
 
\noindent The previous value of the counter is returned.

The following function is used to switch \ML\ into a  mode in  which the number
of primitive inferences done during each top-level interaction is  shown.  
Run-time and garbage collection time are also shown.

\begin{boxed}
\index{timer@\ml{timer}|pin}
\begin{verbatim}
   timer : bool -> bool
\end{verbatim}\end{boxed}

\noindent Executing \ml{timer true} causes  the number  of primitive inferences
and timings to be  printed; \ml{timer  false} switches  the printing  off.  The
previous setting  is  
returned.    Executing  \ml{timer}$\ b$  is equivalent to
setting the flag \ml{timing} to the value $b$ (see Section~\ref{flags}).