\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{sec:system-terms}); the quotation, parsing, and printing of
logical types and terms (Section~\ref{quotation}); the representation of
theorems (Section~\ref{sec:theorems-in-ml}); the representation of theories
(Section~\ref{theoryfns}); the fundamental \HOL{} theory \texttt{bool}
(Section~\ref{boolfull}); the primitive rules of inference
(Section~\ref{rules}); and the methods for extending theories
(throughout Section~\ref{theoryfns} and also later in
Section~\ref{sec:bossLib}).  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 the \ML\ types \ml{hol\_type} and \ml{term}
which implement the types and terms of the \HOL{} logic, as defined in
\LOGIC. It also provides primitive \ML\ functions for creating and
manipulating values of these types. Upon this basis the \HOL{} logic
is implemented. 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 is 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{tokens|(}%
\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).  Using 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 name of a type variable
%
\index{type variables, in HOL logic@type variables, in \HOL{} logic!names of}
%
in the \HOL{} logic is formed by a prime (\ml{'}) followed by an
alphanumeric which itself contains no prime (see Section~\ref{tyvars}
for examples).  The name of a type constant or a term constant in the
\HOL{} logic can be any identifier, although some names are treated
specially by the HOL parser and printer and should therefore be
avoided.
%
\index{identifiers, in HOL logic@identifiers, in \HOL{} logic|)}

\subsection{Identifiers}\label{ident}

In addition to special forms already present in the relevant grammar,
a \HOL{} identifier can be of two forms:
\begin{myenumerate}
\item A finite sequence of \emph{alphanumerics} starting with a letter.  The
  underscore character is considered a digit character, and so can
  occur after an identifier's first letter.  Greek characters (roughly
  Unicode range \ml{U+0370} to \ml{U+03FF}) are also letters, except for
  $\lambda$~(\ml{U+03BB}), which is treated as a symbol. \HOL{} is
  case-sensitive: upper and lower case letters are considered to be
  different.

  Digits are the ASCII characters 0--9, the underscore character, and
  the Unicode subscripts and superscripts.  The apostrophe character
  is special.%
  \index{apostrophe, lexical handling of}
  %
  It is not a letter, but can appear as part of an alphanumeric term
  identifier after the first letter.  It must appear at the start of a
  type variable's name, and can also appear in the term context as a
  sequence of apostrophes on their own.

\item A \emph{symbolic} identifier, \ie, a finite sequence formed by
  any combination of the ASCII symbols and the Unicode symbols.  The
  basic ASCII symbols are
\begin{verbatim}
  #  ?  +  *  /  \  =  <  >  &  %  @  !  :  |  -  ^  `
\end{verbatim}
  Use of the caret and back-tick characters is complicated by the fact
  that these characters have special meaning in the quotation
  mechanism; see Section~\ref{sec:quotation-antiquotation}.  The ASCII
  grouping symbols (braces, brackets, and parentheses), and the
  tilde~(\holtxt{\symbol{126}}), full-stop~(\holtxt{.}),
  comma~(\holtxt{,}), semi-colon~(\holtxt{;}) and hyphen~(\holtxt{-})
  characters are called \emph{non-aggregating} characters. %
%
  \index{identifiers, in HOL logic@identifiers, in \HOL{} logic!non-aggregating characters}%
%
  Unless the desired token is already present in the grammar, these
  characters do not combine with themselves or other symbolic
  characters.  Thus, the string \holtxt{"(("} is viewed as \emph{two}
  tokens, as are \holtxt{"+;"} and \holtxt{"-+"}.

  \index{tokens!Unicode characters}
  \index{Unicode}
  Unicode code characters that are not letters or digits are regarded
  as symbolic.  None of these are non-aggregating.

\item A \emph{number} is a string of one or more digits. If not the
  initial digit, an underscore can be used within the sequence to
  provide spacing. In order to distinguish different kinds of numbers
  a single character suffix may be used: for example \holtxt{3n} is a
  natural number while \holtxt{3i} is an integer.  The \holtxt{0x} and
  \holtxt{0b} prefixes may also be used to change the base of the
  number. If the \holtxt{0x} prefix is used, hexadecimal `digits'
  \holtxt{a}--\holtxt{f} and \holtxt{A}--\holtxt{F} can also be
  used. See also Section~\ref{sec:numerals}.%
\end{myenumerate}
\index{variables, in HOL logic@variables, in \HOL{} logic!names of|)}


\paragraph{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)


\paragraph{Special identifiers}

The following valid identifiers are used by the grammar in the theory
of booleans, and thus in all descendent theories as well.  They should
not be used as the name of a variable or a constant unless the user is
very confident of their ability to mess with grammars.
%
\begin{verbatim}
   let  in  and  \  .  ;  =>  |    :  :=  with  updated_by   case   of
\end{verbatim}

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

The name of a type variable in the \HOL{} logic is a string
beginning with a prime (\ml{'}) followed by an alphanumeric which itself
contains no prime; for example all of the following are valid type
variable names except for the last:
%
\begin{hol}
\begin{verbatim}
   'a   'b   'cat   'A11   'g_a_p   'f'oo
\end{verbatim}
\end{hol}

\paragraph{User tokens}
In general, a \HOL{} user has a great deal of freedom to create their own syntax, involving special tokens quite apart from variables and names for constants.
For example, the if-then-else syntax for the conditional operator %
\index{conditionals, in HOL logic@conditionals, in \HOL{} logic!printing of}%
has special tokens (the ``if'', ``then'' and ``else'') that are not names for variables, nor constants (the underlying constant is actually called \holtxt{COND}).
In order to make sure that the operations of printing and parsing tokens are suitably inverse to each other, users should not create tokens that include whitespace, or the comment strings (\ml{(*} and \ml{*)}).
\index{tokens|)}

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

The allowed types 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{hol\_type}:
%
\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{holboxed}
\begin{verbatim}
   mk_vartype : string -> hol_type
   mk_thy_type : {Tyop:string, Thy:string, Args:hol_type list} -> hol_type
\end{verbatim}
\end{holboxed}
%
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 gives a warning if the name is not an allowable
type variable name (\ie\ not a \ml{'} followed by an alphanumeric).
The function \ml{mk\_thy\_type} constructs a compound type
%
\index{compound types, in HOL logic@compound types, in \HOL{} logic!constructors for}
%
from a record \ml{\lb Tyop,Thy,Args\rb{}} where \ml{Tyop} is a string
representing the name of the type operator, \ml{Thy} is a string
representing the theory that \ml{Tyop} was declared in, and \ml{Args}
is 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 \LOGIC, however, function types were not regarded as compound
types).

The evaluation of
$\ml{mk\_thy\_type}\{\ml{Tyop} = \mathit{name},\
\ml{Thy} = \mathit{thyname},\
\ml{Args} = [\sigma_1, \cdots ,\sigma_n]\}$
fails if
%
\begin{myenumerate}
\item $\mathit{name}$ is not a type operator of theory $\mathit{thyname}$;
\item $\mathit{name}$ is a type operator of theory $\mathit{thyname}$,
but its arity is not $n$.
\end{myenumerate}
%
For example, \ml{mk\_thy\_type\lb{}Tyop="bool", Thy="bool", Args=[]\rb{}}
\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 \ml{term} representing the type
\ty{bool}.
%
%\paragraph{Support for constructing types}

Type constants may be
bound to \ML\ values and need not be repeatedly constructed: \eg, the type built by
\ml{mk\_thy\_type\lb{}Tyop="bool", Thy="bool", Args=[]\rb{}} is abbreviated
by the \ML\ value \ml{bool}. Similarly, function types may be constructed
with the infix \ML\ function \ml{-->}. A few common type variables
have been constructed and bound to \ML{} identifers, \eg, \ml{alpha}
is the type variable \ml{'a} and \ml{beta} is the type variable
\ml{'b}.  Thus the \ML\ code \ml{alpha --> bool} is equal to, but much more concise than
%
\begin{hol}
\begin{verbatim}
  mk_thy_type{Tyop="fun", Thy="min",
              Args=[mk_vartype "'a",
                    mk_thy_type{Tyop="bool", Thy="bool", Args=[]}}
\end{verbatim}
\end{hol}

%\paragraph{Taking types apart}

\noindent
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{hol\_type}:
\begin{holboxed}
\index{function types, in HOL logic@function types, in \HOL{} logic!destructors for}
\index{dest_vartype@\ml{dest\_vartype}|pin}
\index{dest_thy_type@\ml{dest\_thy\_type}|pin}
\begin{verbatim}
  dest_vartype : hol_type -> string
  dest_thy_type : hol_type -> {Tyop:string, Thy:string, Args:hol_type list}
\end{verbatim}
\end{holboxed}

\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.  A compound type is destructed
by the function \ml{dest\_thy\_type} into the name of the type
operator, the name of the theory it was declared in, and a list of the
argument types; \ml{dest\_vartype} and \ml{dest\_thy\_type} are thus
the inverses of \ml{mk\_vartype} and \ml{mk\_thy\_type}, respectively.
The destructors fail on arguments of the wrong form.

\section{Terms}\label{sec:system-terms}

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

At any time, the terms that may be constructed depends 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{holboxed}
\index{mk_var@\ml{mk\_var}|pin}
\begin{verbatim}
   mk_var : (string * hol_type) -> term
\end{verbatim}
\end{holboxed}

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

\begin{holboxed}
\index{mk_thy_const@\ml{mk\_thy\_const}|pin}
\begin{verbatim}
   mk_thy_const : {Name:string, Thy:string, Ty:hol_type} -> term
\end{verbatim}
\end{holboxed}

\noindent $\mathtt{mk\_thy\_const}\{\mathtt{Name} = \mathit{c},\
\mathtt{Thy} = \mathit{thyname},\ \mathtt{Ty} = \sigma\}$
 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 theory $\mathit{thyname}$;
\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{holboxed}\index{mk_comb@\ml{mk\_comb}|pin}
\begin{verbatim}
   mk_comb : (term * term) -> term
\end{verbatim}
\end{holboxed}

\noindent\ml{mk\_comb($t_1$,$t_2$)}
%
\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{holboxed}
\index{mk_abs@\ml{mk\_abs}|pin}
\begin{verbatim}
   mk_abs : (term * term) -> term
\end{verbatim}
\end{holboxed}

\noindent\ml{mk\_abs($x$,$t$)} 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 functions on terms:
%
\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}
%

\begin{holboxed}

\index{dest_var@\ml{dest\_var}|pin}
\index{dest_thy_const@\ml{dest\_thy\_const}|pin}
\index{dest_comb@\ml{dest\_comb}|pin}
\index{dest_abs@\ml{dest\_abs}|pin}
\begin{verbatim}
   dest_var       : term -> (string * hol_type)
   dest_thy_const : term -> {Name:string, Thy:string, Ty:hol_type}
   dest_comb      : term -> (term * term)
   dest_abs       : term -> (term * term)
\end{verbatim}
\end{holboxed}

These are the inverses of \ml{mk\_var}, \ml{mk\_thy\_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{bvar}\index{bvar@\ml{bvar}},
\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{holboxed}\index{type_of@\ml{type\_of}|pin}
\begin{verbatim}
   type_of : term -> hol_type
\end{verbatim}
\end{holboxed}

\noindent returns the type
\index{types, in HOL logic@types, in \HOL{} logic!determination of}
of a term. The function

\begin{holboxed}\index{aconv@\ml{aconv}|pin}
\begin{verbatim}
   aconv : term -> term -> bool
\end{verbatim}
\end{holboxed}

\noindent implements the $\alpha$-convertibility test for
$\lambda$-calculus terms.
%
\index{$\alpha$-convertibility, in HOL logic@$\alpha$-convertibility, in \HOL{} logic!determination of}
%
From the point of view of the \HOL{} logic, $\alpha$-convertible terms
are identical. A variety of other functions are available for
performing $\beta$-reduction (\ml{beta\_conv}), $\eta$-reduction
(\ml{eta\_conv}), substitution (\ml{subst}), type instantiation (\ml{inst}), computation of free variables (\ml{free\_vars}) and
other common term operations.  See \REFERENCE{} for more details.


\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{\dq:$\cdots$\dq} (type quotes, in \ML)|(}
\index{ term quotes, in ML@\ml{\dq$\cdots$\dq} (term quotes, in \ML)|(}

It would be tedious to always have to input types and terms
using the constructor functions. The \HOL{} system, adapting the
approach taken in \LCF\index{LCF@\LCF}, has 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}%
parsers for \HOL{} types and terms which enable types and terms
to be input using a fairly standard syntax. For example, the \ML{}
expression $\holquote{\ml{:bool -> bool}}$ denotes exactly the same
value (of \ML\ type \ml{hol\_type}) as

\begin{hol}
\index{bool, the type in HOL logic@\ml{bool}, the type in \HOL{} logic}
\begin{verbatim}
   mk_thy_type{Tyop = "fun",Thy = "min",
               Args = [mk_thy_type{Tyop = "bool", Thy = "bool", Args = []},
                       mk_thy_type{Tyop = "bool", Thy = "bool", Args = []}]}
\end{verbatim}
\end{hol}

\noindent and the expression \holtxt{\holquote{\bs{}x.~x~+~1}}
%
\index{function abstraction, in HOL logic@function abstraction, in \HOL{} logic}
%
can be used instead of\footnote{In order to be processed successfully,
  this quotation requires the theory of arithmetic to have already
  been loaded, which can be accomplished in the interactive system by
  \ml{load "arithmeticTheory"}.}

\begin{hol}
\begin{verbatim}
  let val numty = mk_thy_type{Tyop="num",Thy="num",Args=[]}
  in
   mk_abs
    (mk_var("x",numty),
     mk_comb(mk_comb
      (mk_thy_const
        {Name="+",Thy="arithmetic",Ty=numty --> numty --> numty},
         mk_var("x", numty)),
       mk_comb(mk_thy_const{Name="NUMERAL",Thy="arithmetic",Ty=numty-->numty},
        mk_comb(mk_thy_const{Name="BIT1",Thy="arithmetic",Ty=numty-->numty},
                mk_thy_const{Name="ZERO",Thy="arithmetic",Ty=numty}))))
  end
\end{verbatim}
\end{hol}

The \HOL{} printer, which is integrated into the \ML{} toplevel loop,
also outputs types and terms using this syntax.
%
\index{printing, in HOL logic@printing, in \HOL{} logic!of quotation syntax}
%
Types are printed
%
\index{printing, in HOL logic@printing, in \HOL{} logic!of types}
%
in the form \holquote{\ml{:}\textit{type}}. For example, the \ML\ value
of type \ml{hol\_type} representing
$\alpha\fun(\ty{ind}\fun\ty{bool})$ would be printed out
as \ml{\holquote{:'a -> ind -> bool}}.
Similarly, terms are printed in the form \holquote{\textit{term}}.
Thus, the term representing $\uquant{x\ y}x<y \imp\equant{z}x+z = y$
would be printed as:
%
\[ \holquote{\ml{!x y. x < y ==> ?z. x + z = y}} \]
%
A leading colon is used to distinguish a type quotation from a term quotation:
the former have the form \holquote{\ml{:}~$\cdots$~} and the latter have
the form \holquote{~$\cdots$~}.
\index{quotation, in HOL logic@quotation, in \HOL{} logic|)}

Section~\ref{sec:parsing-printing} has more detailed information about
the capabilities of the term and type parsing and printing facilities
in the system.  The remainder of this section provides a brief
overview of what is possible.


\subsection{Type inference}
\index{type inference!in HOL parser@in \HOL{} parser|(}
%
Notice that there is no explicit type information in
\holtxt{\bs{}x.x+1}.  The \HOL{} type checker knows that \ml{1} has
type \holtxt{num} and \holtxt{+} has type \holtxt{num->(num->num)}.
From this information it can infer that both occurrences of \ml{x} in
\holtxt{\bs{}x.x+1} could have type \holtxt{num}.  This is not the
only possible type assignment; for example, the first occurrence of
\holtxt{x} could have type \holtxt{bool} and the second one have type
\holtxt{num}.  In that case there would be two \emph{different}
variables with name \holtxt{x}, namely \holtxt{x}$_{\holtxt{bool}}$ and
\holtxt{x}$_{\holtxt{num}\vphantom{l}}$, the second of which is free.  However, 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}{0}
\begin{session}
\begin{verbatim}
- ``x = (x = 1)``;
Type inference failure: unable to infer a type for the application of

$= (x :num)

which has type

:num -> bool

to

(x :num) = (1 :num)

which has type

:bool

unification failure message: unify failed
\end{verbatim}
\end{session}

The desired value can be directly constructed by the primitive constructor
functions:

\begin{session}
\begin{verbatim}
- mk_eq
   (mk_var("x",bool),
    mk_eq(mk_var("x",numty),
          mk_numeral (Arbnum.fromString "1")));
> val it = ``x <=> (x = 1)`` : term
\end{verbatim}
\end{session}

The original quotation type checker was designed and implemented by
<NAME>\index{Milner, R.}.  It employs heuristics like the one
above to infer a sensible type for all variables occurring in a term.

\index{type constraint!in HOL logic@in \HOL{} logic} At times, the
user may want to control the exact type of a subterm. To support such
functionality, types can be explicitly indicated by following any
subterm with a colon and then a type.  For example,
\holtxt{\dq{}f(x:num):bool\dq} will type check with \holtxt{f} and
\holtxt{x} getting types \holtxt{num->bool} and \holtxt{num}
respectively.  This treatment of types within quotations is inherited
from \LCF.
%
\index{LCF@\LCF}
\index{ type quotes, in ML@\ml{\dq:$\cdots$\dq} (type quotes, in \ML)|)}
\index{ term quotes, in ML@\ml{\dq$\cdots$\dq} (term quotes, in \ML)|)}
\index{type inference!in HOL parser@in \HOL{} parser|)}

\subsection{Viewing the grammar}

\index{parsing, of HOL logic@parsing, of \HOL{} logic!grammars for}
\index{printing, in HOL logic@printing, in \HOL{} logic!grammars for}
The behaviour of the \HOL{} quotation parser and printer is determined
by the current grammar. Thus, a familiarity with the basic vocabulary
of the standard collection of \HOL{} theories is important if one is
to use \HOL{} effectively. One can examine the current grammar used by
the parser with the functions \verb+type_grammar+ and
\verb+term_grammar+.

For example, in the following session, we see that the type grammar
used in the startup context of \HOL{} has the type operators
\verb+fun+, \verb+sum+, \verb+prod+, \verb+list+, \verb+recspace+,
\verb+num+, \verb+option+, \verb+one+, \verb+label+, \verb+ind+, and
\verb+bool+.

\setcounter{sessioncount}{0}
\begin{session}
\begin{verbatim}
- type_grammar();
> val it =
    Rules:
    (50)   TY  ::=  TY -> TY [fun] (R-associative)
    (60)   TY  ::=  TY + TY [sum] (R-associative)
    (70)   TY  ::=  TY # TY [prod] (R-associative)
    (100)  TY  ::=  TY list | TY recspace | num | (TY, TY)prod | TY option |
                    one | (TY, TY)sum | label | (TY, TY)fun | ind | bool
     : grammar
\end{verbatim}
\end{session}

Also, \verb+fun+, \verb+sum+, and \verb+prod+ have infix
notation (\verb+->+), (\verb|+|), and (\verb+#+), respectively, with
different binding strengths: \verb+#+ (with 70) binds stronger than
\verb|+| (60), which  binds stronger than \verb+->+ (50). All postfix
type operators (with 100) bind more strongly than the infixes.

The next session, in Figure~\ref{fig:term-grammar}, shows the
(abbreviated) output from invoking the \ml{term\_grammar} function in
the startup \HOL{} environment. The deleted output includes a listing
of all constants known to the system, including prefix operators,
along with all overloadings currrently in force. The portrayed grammar
ranges from binding operators at very low (0) binding strength,
through to function application (2000) and record selection (2500),
which bind very tightly.

\setcounter{sessioncount}{0}
\begin{figure}[htbp]
\begin{session}
\begin{verbatim}
- term_grammar();
> val it =
    (0)    TM  ::=  "LEAST" <..binders..>  "." TM |
                    "?!" <..binders..>  "." TM | "?" <..binders..>  "." TM |
                    "!" <..binders..>  "." TM | "@" <..binders..>  "." TM |
                    "\" <..binders..>  "." TM
    (2)    TM  ::=  "let" TM "in" TM  [let]
    (4)    TM  ::=  TM "::" TM (restricted quantification operator)
    (5)    TM  ::=  TM TM  (binder argument concatenation)
    (7)    TM  ::=  "case" TM "of" TM  [case__magic]
    (8)    TM  ::=  TM "|" TM  [case_split__magic]   (R-associative)
    (9)    TM  ::=  TM "and" TM   (L-associative)
    (10)   TM  ::=  TM "=>" TM  [case_arrow__magic]   (R-associative)
    (50)   TM  ::=  TM "##" TM | TM "," TM   (R-associative)
    (70)   TM  ::=  "if" TM "then" TM "else" TM  [COND]
    (80)   TM  ::=  TM ":-" TM   (non-associative)
    (100)  TM  ::=  TM "=" TM   (non-associative)
    (200)  TM  ::=  TM "==>" TM   (R-associative)
    (300)  TM  ::=  TM "\/" TM   (R-associative)
    (400)  TM  ::=  TM "/\" TM   (R-associative)
    (425)  TM  ::=  TM "IN" TM   (non-associative)
    (440)  TM  ::=  TM "++" TM   (L-associative)
    (450)  TM  ::=  TM "::" TM  [CONS] | TM ">=;" TM | TM "<=" TM |
                    TM ">" TM | TM "<;" TM | TM ">=" TM | TM "<=" TM |
                    TM ">" TM | TM "<" TM | TM "LEX" TM | TM "RSUBSET" TM |
                    TM ":=" TM  [record field update] |
                    TM "updated_by" TM  [functional record update] |
                    TM "with" TM  [record update]
                    (R-associative)
    (500)  TM  ::=  TM "-" TM | TM "+" TM | TM "RUNION" TM   (L-associative)
    (600)  TM  ::=  TM "DIV" TM | TM "*" TM | TM "RINTER" TM
                    (L-associative)
    (650)  TM  ::=  TM "MOD" TM   (L-associative)
    (700)  TM  ::=  TM "**" TM | TM "EXP" TM   (R-associative)
    (800)  TM  ::=  TM "O" TM | TM "o" TM   (R-associative)
    (900)  TM  ::=  "~" TM
    (1000) TM  ::=  TM ":" TY  (type annotation)
    (2000) TM  ::=  TM TM  (function application) |    (L-associative)
    (2500) TM  ::=  TM "." TM  [record field selection]   (L-associative)
           TM  ::=  "[" ... "]"  (separator = ";") |
                    "<|" ... "|>"  (separator = ";")
           TM  ::=  "(" ")"  [one] |
                    "(" TM ")"  [just parentheses, no term produced]
    ... <further output omitted>
  : grammar
\end{verbatim}
\end{session}
\caption{Result of a call to \ml{term\_grammar()}}
\label{fig:term-grammar}
\end{figure}

\subsection{Namespace control}

In order to provide convenience, the parser deals with overloading and
ambiguity. Overloading of numeric literals is discussed in
Section~\ref{arith-overloading}, although any symbol may be
overloaded, not just numerals. At times such flexibility is quite
useful; however, it can happen that one wishes to explicitly designate
a particular constant. In that case, the notation
$\mathit{thy}\holtxt{\$}\mathit{const}$ may be used in the parser to
designate the constant $\mathit{const}$ declared in theory
$\mathit{thy}$. In the following example, the less-than operator is
explicitly specified.

\setcounter{sessioncount}{0}
\begin{session}
\begin{verbatim}
- ``prim_rec$< x y``
> val it = ``x < y`` : term
\end{verbatim}
\end{session}
Note how the \holtxt{<} symbol is not treated as an infix by the
parser when given in ``fully-qualified'' form.  Syntactically, such
tokens are never given special treatment by the parser of \HOL's
concrete syntax.
%
\index{constants, in HOL logic@constants, in \HOL{} logic!fully-qualified names of}

\section{Ways to Construct Types and Terms}

\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{'a,\,'b,\,}$\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}}
\index{type quotes, in ML@\ml{`:$\cdots$`} (type quotes, in \ML)}
\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+:'+}$\mathit{alphanum}$ & {\small\holtxt{mk\_vartype("'}}$\mathit{alphanum}${\small\holtxt{")}}   \\ \hline
Type constant & {\small\verb+:+}$\mathit{op}$ & {\small\verb+mk_type("+}$\mathit{op}${\small\verb+",[])+}   \\ \hline
 & {\small\verb+:+}$\mathit{thy}${\small\verb+$+}$\mathit{op}$
  & \parbox{7cm}
   {{\small\holtxt{mk\_thy\_type\lb{}Thy="}}$\mathit{thy}${\small\holtxt{",}} \newline
    {\small\holtxt{\quad Tyop="}}$\mathit{op}${\small\holtxt{",Args=[]\rb{}}}}   \\ \hline
Function type & {\small\verb+:+}$\sigma_1${\small\verb+->+}$\sigma_2$ &
$\sigma_1${\small\verb+-->+}$\sigma_2$ \\
\hline
Compound type &
{\small\verb+:(+}$\sigma_1${\small\holtxt{,\ldots,}}$\sigma_n${\small\verb+)+}$\mathit{op}$ &
{\small\holtxt{mk\_type("}}$\mathit{op}${\small\holtxt{",[}}%
 $\sigma_1${\small\holtxt{,\ldots,}}$\sigma_n${\small\holtxt{])}}
\\
\hline
& {\small\verb+:(+}$\sigma_1${\small\holtxt{,\ldots,}}$\sigma_n${\small\verb+)+}$\mathit{thy}${\small\verb+$+}$\mathit{op}$
& \parbox{7cm}
   {{\small\holtxt{mk\_thy\_type\lb{}Thy="}}$\mathit{thy}${\small\holtxt{",}} \newline
    {\small\holtxt{\quad Tyop="}}$\mathit{op}${\small\holtxt{",Args=[}}%
 $\sigma_1{\small\holtxt{,\ldots,}}\sigma_n${\small\holtxt{]\rb{}}}} \\ \hline
\end{tabular}
\end{center}


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 & $\mathit{var}${\small\verb+:+}$\sigma$ &
{\small\verb+mk_var("+}$\mathit{var}${\small\verb+",+}$\sigma${\small\verb+)+} \\ \hline
%
Constant & $\mathit{const}${\small\verb+:+}$\sigma$ &
{\small\verb+mk_const("+}$\mathit{const}${\small\verb+",+}$\sigma${\small\verb+)+} \\ \hline
%
Constant & $\mathit{thy}${\small\verb+$+}$\mathit{const}${\small\verb+:+}$\sigma$ &
{\small\verb+mk_thy_const{Name="+}$\mathit{const}${\small\verb+",Thy="+}$\mathit{thy}${\small\verb+",Ty=+}$\sigma${\small\verb+}+} \\ \hline
%
Combination & $t_1\ t_2$ &
{\small\verb+mk_comb(+}$t_1${\small\verb+,+}$t_2${\small\verb+)+} \\ \hline
%
Abstraction & {\small\holtxt{\bs}}$x${\small\holtxt{.}}$t$ &
{\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|)}

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
 & &  \\
$t\ t_1 \cdots t_n$ &
{\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\holtxt{,\ldots,}}$t_n${\small\verb+])+} \\ \hline
{\small\verb+\+}$x_1\cdots x_n${\small\verb+.+}$t$ &
{\small\holtxt{\bs}}$x_1${\small\verb+.+}$\cdots${\small\holtxt{\bs}}$x_n${\small\verb+.+}$t$ &
{\small\verb+list_mk_abs([+}$x_1${\small\holtxt{,\ldots,}}$x_n${\small\verb+],+}$t${\small\verb+)+}
\\ \hline
\end{tabular}
\end{center}


\section{Theorems}
\label{sec:theorems-in-ml}

In \LOGIC, the notion of deduction was introduced in terms of
\textit{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 \textit{deductive
  system}:
\index{natural deduction}%
\index{deductive systems}%
%
a set of pairs, whose second component is a sequent, and whose first
component is a set of sequents.\footnote{Note that these sequents form
  a list, not a set; that is, are ordered.}  The concept of a sequent
\textit{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.

\index{turnstile notation|(} 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 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 \textit{theorem} of that deductive system.  That
is, a theorem
%
\index{theorems, in natural deduction}
%
is the last element of a \textit{proof}
%
\index{proof!in natural deduction}
%
(in the sense of \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
\textit{axiom}\index{axioms!in natural deduction}.  Any pair
$(L,(\Gamma,t))$ belonging to a deductive system is called a
\textit{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 \holtxt{:bool}.  Therefore, a term
%
\index{terms, in HOL logic@terms, in \HOL{} logic!as logical formulas}
%
of type \holtxt{: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 an implementation of
the \ML{} signature \ml{HOLset} supporting operations such as
\ml{member} and \ml{union}.
%
\index{sequents!representation of, in HOL logic@representation of, in \HOL{} logic}

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

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

\noindent which returns a pair consisting of a list of the
hypotheses
\index{hypotheses!of theorems}
and the conclusion,
\index{conclusions!of theorems}
%
respectively, of a theorem.  The order of assumptions in the list
should not be relied on.  A theorem's hypotheses are also available in
the set form with the function

\begin{holboxed}
\index{hyp_set@\ml{hyp\_set}}
\begin{verbatim}
   hyp_set : thm -> term HOLset.set
\end{verbatim}
\end{holboxed}

Using \ml{dest\_thm}, two further destructor
\index{theorems, in HOL logic@theorems, in \HOL{} logic!destructors for}
functions are derived

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

\noindent for extracting the hypothesis list and the conclusion, respectively,
of a theorem. The \ML\ type \ml{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 in Section~\ref{rules}.)
%% derived-rules reference is dead for the moment (until we
%% resuscitate drules.tex)
%, and further in Chapter\ref{derived-rules}.)

It was mentioned in \LOGIC{} that the deductive system of \HOL{}
includes four axioms.\footnote{This is a simplification: in fact the
  various axioms are an extension of the basic logic.}  In that
manual, the axioms were presented in abstract form.  Concretely,
axioms are just theorem values that are introduced through the use of
the \ML{} function \ml{new\_axiom} (see Section~\ref{theoryprims}
below).  For example, the axiom \ml{BOOL\_CASES\_AX} mentioned in
\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 (falsity), the HOL constant@\holtxt{F} (falsity), the \HOL{} constant!axiom for}
\begin{verbatim}
   |- !t. (t = T) \/ (t = F) : thm
\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 \ml{thm} status; as well as the
absence of \HOL{} quotation marks
%
\index{ theorem marker, in HOL logic@\ml{"|-} (theorem marker, in \HOL{} logic)}
%
in the \ml{|-} context.  The session below illustrates the use of the
destructor functions:

\setcounter{sessioncount}{0}
\begin{session}
\begin{verbatim}
   - val th = BOOL_CASES_AX;
   > val th = |- !t. (t = T) \/ (t = F) : thm

   - hyp th;
   > val it = [] : term list

   - concl th;
   > val it = ``!t. (t = T) \/ (t = F)`` : term

   - type_of it;
   > val it = ``:bool`` : hol_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 flag \ml{show\_assums}
\index{show_assums@\ml{show\_assums}} allows theorems
to be printed with hypotheses shown in full. These points are illustrated with a
theorem inferred, for example purposes, from another axiom mentioned
in \LOGIC, \ml{SELECT\_AX}.

\begin{session}
\begin{verbatim}
- val th = UNDISCH (SPEC_ALL SELECT_AX);
> val th =  [.] |- P ($@ P) : thm

- show_assums := true;
> val it = () : unit

- th;
> val it =  [P x] |- P ($@ P) : thm
\end{verbatim}
\end{session}
\index{theorem notation, in HOL logic@theorem notation, in \HOL{} logic|)}

\section{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 \LOGIC. The descriptions relied on meta-variables $t$,
$t_1$, $t_2$, and so on.  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 \LOGIC{}'s rules 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 type)@\ml{thm} (\ML{} type)}
%
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{inferences, in HOL logic@inferences, in \HOL{} logic!notation for}
%
is used here as in \LOGIC: 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.

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

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

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

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

\bigskip

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

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

\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

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

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

\begin{center}
\begin{tabular}{c}
  \\ \hline
\holtxt{ |- (\bs$x$.$t_1$)$t_2$ = $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}

%'' below makes latex font-locking cope with the "unbalanced" double
%back-tick quotations.
\noindent \ml{BETA\_CONV ``(\bs$x$.$t_1$)$t_2$``} %''
evaluates to the theorem \ml{|- (\bs$x$.$t_1$)$t_2$ = $t_1[t_2/x]$}.
Failure occurs if the argument to \ml{BETA\_CONV} is not a $\beta$-redex
(\ie\ is not of the form \holtxt{(\bs$x$.$t_1$)$t_2$}.

\bigskip

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

\begin{holboxed}
\begin{verbatim}
   SUBST : (thm * term) list -> term -> thm -> thm
\end{verbatim}
\end{holboxed}

\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 occurs 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|)}

\subsection{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{holboxed}\index{ABS@\ml{ABS}|pin}
\begin{verbatim}
   ABS : term -> thm -> thm
\end{verbatim}
\end{holboxed}


\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 occurs if $x$ is not a variable, or $x$
 occurs free in any assumption in $\Gamma$.


\bigskip

\subsection{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{holboxed}\index{INST_TYPE@\ml{INST\_TYPE}|pin}
\begin{verbatim}
   INST_TYPE : {redex : hol_type, residue : hol_type} list -> thm -> thm
\end{verbatim}
\end{holboxed}

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

\bigskip

\begin{itemize}
\item where $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 the term $t$.  Similarly, $\Gamma[\sigma_1,\ \ldots\
,\sigma_n/\alpha_1,\ \ldots\ ,\alpha_n]$ denotes the result of
performing the same substitution to all of the hypotheses in the set
$\Gamma$.
\end{itemize}

\noindent
\ml{INST\_TYPE[$\alpha_1$~|->~$\sigma_1$%
  ,$\ldots$,$\alpha_n$~|->~$\sigma_n$]~$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 occurs if an $\alpha_i$ is
not a type variable.

The polymorphic \ML{} infix function {\small\verb+|->+} is used to
construct values of the record type \ml{redex-residue}.  It is defined
\begin{verbatim}
   fun ((x:'a) |-> (y:'b)) = {redex = x, residue = y}
\end{verbatim}

\bigskip

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


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

\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

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


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

\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|)}

\section{Oracles}

\HOL{} extends the \LCF\ tradition by allowing the use of an
\emph{oracle} mechanism, enabling arbitrary formulas to become
elements of the \ml{thm} type. By use of this mechanism, \HOL{} can
utilize the results of arbitrary proof procedures. In spite of such
liberalness, one can still make strong assertions about the security
of ML objects of type \ml{thm}.

To avoid unsoundness, a \emph{tag} is attached to any theorem coming
from an oracle. This tag is propagated through every inference that
the theorem participates in (much as ordinary assumptions are
propagated in the inference rule \ml{MP}). If it happens that falsity
becomes derived, the offending oracle can be found by examining the
tags component of the theorem. A theorem proved without use of any
oracle will have an empty tag, and can thus be considered to have been
proved solely by deductive steps in the HOL logic.

A tagged theorem can be created via

\begin{holboxed}
\index{mk_oracle_thm@\ml{mk\_oracle\_thm}!type of}
\begin{verbatim}
   mk_oracle_thm : string -> term list * term -> thm
\end{verbatim}
\end{holboxed}

\noindent which directly creates the requested theorem and attaches the given
tag to it. The tag is created with a call to

\begin{holboxed}
\index{Tag.read@\ml{Tag.read}!making tags}
\begin{verbatim}
   Tag.read : string -> tag
\end{verbatim}
\end{holboxed}

As well as providing principled access to the results of external
reasoners, tags are used to implement some useful `system' operations
on theorems. For example, one can directly create a theorem via the
function \ml{mk\_thm}. The tag \verb+MK_THM+ gets attached to each
theorem created with this call. This allows users to directly create
useful theorems, \eg, to use as test data for derived rules of
inference.  Another tag is used to implement so-called `validity
checking' for tactics.

The tags in a theorem can be viewed by setting \verb+Globals.show_tags+ to
true.

\setcounter{sessioncount}{0}
\begin{session}
\begin{verbatim}
   - Globals.show_tags := true;
   > val it = () : unit

   - mk_thm([], Term `F`);;
   > val it = [oracles: MK_THM] [axioms: ] [] |- F : thm
\end{verbatim}
\end{session}\index{mk_thm@\ml{mk\_thm}}

There are three elements to the left of the turnstile in the fully printed
representation of a theorem: the first two\footnote{Tags are also used for
tracking the use of axioms in proofs.} comprise the tags component and the
third is the standard assumption list. The tag component of a theorem
can be extracted by

\begin{holboxed}
\begin{verbatim}
   Thm.tag : thm -> tag
\end{verbatim}
\end{holboxed}

\noindent and prettyprinted by

\begin{holboxed}
\begin{verbatim}
   Tag.pp : ppstream -> tag -> unit.
\end{verbatim}
\end{holboxed}


\section{Theories}
\label{theoryfns}

\index{theories, in HOL logic@theories, in \HOL{} logic!representation of|(}
%
In \LOGIC{} a theory is described as 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}

In the implementation of \HOL, theories are structured hierarchically
to represent sequences of extensions called
\emph{segments}
%
\index{theory segments}
%
of an initial theory called \ml{min}\index{min@\ml{min}}. A theory
segment is not really a logical concept, but rather a means of
representating theories in the \HOL{} system. Each segment records
some types, constants, axioms and theorems, together with pointers to
other segments called its \emph{parents}.
%
\index{parents, of HOL theories@parents, of \HOL{} theories}
%
The theory represented by a segment is obtained by taking the union of
all the types, constants, axioms and theorems in the segment, together
with the types, constants, axioms and theorems in all the segments
reachable by following pointers to parents. This collection of
reachable segments is called the \emph{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 segment.

\index{theories, in HOL logic@theories, in \HOL{} logic!representation of|)}

\subsection{ML functions for theory operations}
\label{theoryprims}

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 importing some existing theory
segments, making a number of definitions, and perhaps proving and
storing some theorems in the current segment. Then the current segment
(named $name$ say) is exported. The concrete result will be an \ML\
module $name$\ml{Theory} whose contents is the current theory segment
created during the session and whose ancestry represents the desired
logical theory ${\cal T}$. Subsequent work sessions can access the
definitions and theorems of ${\cal T}$ by importing $name$\ml{Theory};
this avoids having to load the tools and replay
the proofs that created $name$\ml{Theory} in the first place.

The naming of data in theories is based on the names given to segments.
Specifically an axiom, definition, specification or theorem is
accessed\index{theories, in HOL logic@theories, in \HOL{} logic!naming of}
by an \ML\ long identifier $thy${\small\verb+Theory.+}$name$, 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.
Thus each theory segment provides a separate namespace of ML bindings of
\HOL{} items.

Various additional pieces of information are stored in a theory
segment, including the parsing status of the constants (\eg\ whether
they are infixes or binders).

\paragraph {Determining the context}

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

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

  When an interactive \HOL{} session begins, some theories will
  already be in the logical context. The exact set of theories in
  context will vary.  If the executable used is \texttt{hol.bare},
  then only \theoryimp{min} and \theoryimp{bool} will be loaded.  When
  the \texttt{hol} executable is used, a richer context is loaded.

The exact set of theories loaded can be determined with the
\ml{ancestry} command.
%
\begin{holboxed}
\index{ancestry@\ml{ancestry}|pin}
\begin{verbatim}
  ancestry : string -> string list
\end{verbatim}
\end{holboxed}

This function provides a general mechanism for examining the structure
of the theory hierarchy.  The argument is the name of a theory (or
\texttt{"-"} as an abbreviation for the current theory), to which
\texttt{ancestry} will respond with a list of the argument's ancestors
in the theory hierarchy.

\begin{holboxed}
{\small
\begin{verbatim}
   - ancestry "-";
   > val it =
      ["num", "prim_rec", "normalForms", "relation", "pair",
        "arithmetic", "while", "numeral", "label", "combin", "sum", "min",
        "bool", "marker", "one", "option", "ind_type", "list"] : string list
\end{verbatim}
}
\end{holboxed}


\paragraph{Creating a theory segment}

\index{theories, in HOL logic@theories, in \HOL{} logic!creation of|(}
%
New theory segment is created by a call to \ml{new\_theory}.
%
\begin{holboxed}
\index{new_theory@\ml{new\_theory}|pin}
\begin{verbatim}
   new_theory : string -> unit
\end{verbatim}
\end{holboxed}
%
This allocates a new `area' where subsequent theory
operations take effect. If the current theory ($thy_1$ say) at the time
of a call to {\small\verb+new_theory +}$thy_2$ is non-empty, \ie, has
had an axiom, definition, or theorem stored in it, then $thy_1$ is
exported before $thy_2$ is allocated. Furthermore, $thy_2$ will obtain
$thy_1$ as a parent. If {\small\verb+new_theory +}$thy$ is called when
the current theory segment is already named $thy$, then that is
interpreted as a request merely to clear the current theory segment
(nothing will be exported).

A call to \ml{new\_theory "$\mathit{name}$"} fails if:
\begin{itemize}
\item $name$ is not an alphanumeric starting with a letter.

\item there is a theory already named $name$ in the ancestry of the
current segment.

\item if it is necessary to export the current segment before creating
the new theory and the export attempt fails.
\end{itemize}

On startup, the current theory segment of \HOL{} is named \ml{scratch},
which is an empty theory, having a useful collection of theories in
its ancestry. Typically, a user would begin by loading whatever extra
logical context is required for the work at hand.

The current theory segment acts as a kind of scratchpad. Elements stored
in the current segment may be overwritten by subsequent additions, or
deleted outright. Any theory elements that were built from overwritten
or deleted elements would then be held to be {\it out-of-date}, and would not
be included in the theory when it is finally exported.  Out-of-date
constants and types are detected by the \HOL{} printer, which will print
them surrounded by odd-looking syntax to alert the user.

In contrast to the current segment, (proper) ancestor segments may not
be altered.
%
\index{theories, in HOL logic@theories, in \HOL{} logic!creation of|)}


\paragraph{Loading prebuilt theories}

Since \HOL{} theories are represented by \ML\ modules, one imports an
existing theory segment by simply importing the corresponding module.

\begin{holboxed}
\index{load (ML function)@\ml{load} (\ML{} function)|pin}
\begin{verbatim}
   load : string -> unit
\end{verbatim}
\end{holboxed}

\noindent
Executing {\small\verb+load +}$name${\small\verb+Theory+} imports the
first file named $name${\small\verb+Theory.uo+} found along the
{\small\verb+loadPath+} into the session. Any unloaded ancestors of
$name$ will be loaded before loading of $name${\small\verb+Theory+}
continues.  Note that {\small\verb+load+} can not be used in ML files
that are to be compiled; it can only be used in the interactive
system.

\paragraph{Adding to the current theory}

The following \ML{} functions add types and terms to the current
theory segment. In typical usage, these functions will not be
needed since higher-level definition facilities will invoke these as
necessary. However, these functions can be useful for those writing
proof tools and derived definition principles.

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


\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. If
\ty{op} is not an allowed name for a type, a warning will be issued.


\begin{holboxed}
\index{new_constant@\ml{new\_constant}|pin}
\begin{verbatim}
   new_constant : (string * type) -> unit
\end{verbatim}
\end{holboxed}

\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$.
If $c$ is not an allowed name for a constant, a warning will be issued.

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

\noindent Executing \ml{new\_axiom("}$name$\ml{",}$t$\ml{)} declares the
sequent
\ml{(\lb\rb{},$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 occurs if:
\begin{myenumerate}
\item the type of $t$ is not \verb+bool+;

\item $t$ contains out-of-date constants or types, \ie, constants or
  types that have been re-declared after $t$ was built.
\end{myenumerate}

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

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

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

\paragraph{Exporting a theory}

Once a theory segment has been constructed, it can be written out to a
file, which, after compilation, can be imported into future sessions.

\begin{holboxed}
\index{export_theory@\ml{export\_theory}|pin}
\begin{verbatim}
   export_theory : unit -> unit
\end{verbatim}
\end{holboxed}

When {\small\verb+export_theory+} is called, all out-of-date entities
are removed from the current segment. Also, the parenthood of the
theory is computed. The current theory segment is written to file
$name${\small{\tt Theory.sml}} in the current working directory.  The
file $name${\small{\tt Theory.sig}}, which documents the contents of
$name$, is also written to the current working directory.  Notice that
the exported theory is not compiled by \HOL. That is left to an
external tool, \holmake{} (see section~\ref{Holmake}), which maintains
dependencies among collections of \HOL{} theory segments.


\subsection{ML functions 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 \ml{string} to \ml{new\_axiom},
\ml{new\_definition}, \etc, are the names of the corresponding axioms
and definitions. These names are used when accessing theories with the
functions \ml{axiom}, \ml{definition}, \etc, described below.

The current theory
%
\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 in the ancestry of the current theory
cannot be extended in this way; they can be thought of as
\emph{frozen}.

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

\begin{holboxed}
\index{parents@\ml{parents}|pin}
\index{types@\ml{types}|pin}
\index{constants@\ml{constants}|pin}
\begin{verbatim}
   parents     : string -> string list
   types       : string -> (int * string) list
   constants   : string -> term list
\end{verbatim}
\end{holboxed}

\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.
Individual axioms, definitions and theorems can be read from the
current theory using the following \ML\ functions:

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

\noindent The first argument is the user supplied name of the axiom,
definition or theorem in the current theory.  Further, a list of all
of a theory's axioms, definitions and theorems can be retreived with
the \ML{} functions:

\begin{holboxed}
\index{axioms@\ml{axioms}|pin}
\index{theorems@\ml{theorems}|pin}
\index{definitions@\ml{definitions}|pin}
\begin{verbatim}
   axioms      : string -> (string * thm) list
   definitions : string -> (string * thm) list
   theorems    : string -> (string * thm) list
\end{verbatim}
\end{holboxed}

The contents of the current theory can be printed in a readable format
using the function \ml{print\_theory}.
%
\index{printing, in HOL logic@printing, in \HOL{} logic!of theories}
\index{print_theory@\ml{print\_theory}}
\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{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|(}

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

\subsubsection{Constant definitions}
\label{sec:constant-definitions}

In \LOGIC{} 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 \LOGIC{} 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{holboxed}
\index{new_definition@\ml{new\_definition}|pin}
\begin{verbatim}
   new_definition : (string * term) -> thm
\end{verbatim}
\end{holboxed}


\noindent Evaluating
 \ml{new\_definition("$name$", \holquote{$c\ v_1\ \cdots\ v_n\ =\ t$})},
declares the sequent
\ml{(\lb\rb{},$c = \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 occurs if:
\begin{myenumerate}
\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}

\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 \LOGIC{} 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
\]
such that:

\begin{myenumerate}
\item $c_1$, $\dots$, $c_n$ are distinct names;
\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{holboxed}
\index{new_specification@\ml{new\_specification}|pin}
\begin{verbatim}
   new_specification : string * string list * thm -> thm
\end{verbatim}
\end{holboxed}
%
Evaluating:
{
\newcommand{\cone}{\ensuremath{c_1}}
\newcommand{\cn}{\ensuremath{c_n}}
\newcommand{\xone}{\ensuremath{x_1}}
\newcommand{\xn}{\ensuremath{x_n}}
\begin{alltt}
   new_specification("\(\mathit{name}\)", ["\cone", ..., "\cn"],
                     |- ?\xone ... \xn. \(t\)[\xone, ..., \xn])
\end{alltt}
}
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 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 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 the type of some $c_i$ does not contain all the type
variables which occur in the term
\holtxt{\bs$x_1\ \cdots\ x_n$. $t$[$x_1$, $\ldots$, $x_n$]}.
\end{myenumerate}
%
\index{specification of constants, in HOL logic@specification of constants, in \HOL{} logic|)}

\subsubsection{Type definitions}
\label{type-defs}

\index{extension, of HOL logic@extension, of \HOL{} logic!by type definition|(}
%
\index{type definitions, in HOL logic@type definitions, in \HOL{} logic|(}
%
In \LOGIC{} 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{holboxed}
\index{new_type_definition@\ml{new\_type\_definition}|pin}
\begin{verbatim}
   new_type_definition : (string * thm) -> thm
\end{verbatim}\end{holboxed}

\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}", |- ?\(x\). \(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}}. 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:'a->bool) (rep:'b->'a) =
       (!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}", |- ?}$x$\ml{.}\ $t\ x$\ml{)} fails if:
\begin{myenumerate}
\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|)}

\paragraph{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{holboxed}
\index{define_new_type_bijections@\ml{define\_new\_type\_bijections}|pin}
\begin{verbatim}
   define_new_type_bijections
      : {name:string, ABS:string, REP:string, tyax:thm} -> thm
\end{verbatim}\end{holboxed}

\noindent This function takes a record {\small\verb+{ABS, REP, name, tyax}+}.
The {\verb+tyax+} argument must be a definitional axiom of the form returned by
\ml{new\_type\_definition}.  The {\verb+name+} 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 {\small\verb+ABS+} and {\small\verb+REP+} 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
       \lb{}name="\m{name}", ABS="\m{abs}", REP="\m{rep}",
        tyax = |- ?rep:newty->ty. TYPE\_DEFINITION \m{P} rep\rb{}
\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 $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|)}

\paragraph{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\_bijections} are injective (one-to-one)
and surjective (onto):

\begin{holboxed}
\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{holboxed}

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

\begin{hol}
\begin{alltt}
   |- (!a. \m{abs}(\m{rep} a) = a) /\bs (!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}:

\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:

\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:

\begin{hol}
\begin{alltt}
   |- !a. ?r. (a = \m{abs} r) /\bs \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 in the current theory.

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


%\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{holboxed}\index{new_type_abbrev@\ml{new\_type\_abbrev}|pin}
%\begin{verbatim}
%   new_type_abbrev : (string * type) -> unit
%\end{verbatim}\end{holboxed}
%
%\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{holboxed}\index{type_abbrevs@\ml{type\_abbrevs}|pin}
%\begin{verbatim}
%   type_abbrevs : string -> (string * type) list
%\end{verbatim}\end{holboxed}
%
%
%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`;;
%() : unit
%
%#new_type_abbrev(`numpair`, ":num*num");;
%() : unit
%
%#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 ********************
%
%() : unit
%\end{verbatim}\end{session}
%
%\noindent If the session is then ended:
%
%\begin{session}\begin{verbatim}
%#close_theory();;
%() : unit
%
%#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
%() : unit
%
%#"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.


%%% Local Variables:
%%% mode: latex
%%% TeX-master: "description"
%%% End:
