Logics/document/HOL.tex

3 \index{HOL system@{\sc hol} system}
6 polymorphic version of Church's Simple Theory of Types.  HOL can be best
8 \emph{Isabelle/HOL --- A Proof Assistant for Higher-Order Logic} provides a
9 gentle introduction on using Isabelle/HOL in practice.
59 \caption{Syntax of \texttt{HOL}} \label{hol-constants}
93 \caption{Full grammar for HOL} \label{hol-grammar}
105   HOL has no if-and-only-if connective; logical equivalence is expressed using
125 HOL allows new types to be declared as subsets of existing types,
127 \texttt{datatype} (see~{\S}\ref{sec:HOL:datatype}).
188 satisfying~$P$, if such exists.  Since all terms in HOL denote something, a
203 \index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system} The
204 basic Isabelle/HOL binders have two notations.  Apart from the usual
205 \texttt{ALL} and \texttt{EX} for $\forall$ and $\exists$, Isabelle/HOL also
210 ``\ttindexbold{HOL}'' governs the output notation.  If enabled (e.g.\ by
211 passing option \texttt{-m HOL} to the \texttt{isabelle} executable),
240 HOL also defines the basic syntax
247 (see~{\S}\ref{sec:HOL:datatype}).
270 \caption{The \texttt{HOL} rules} \label{hol-rules}
273 Figure~\ref{hol-rules} shows the primitive inference rules of~HOL, with
305 \caption{The \texttt{HOL} definitions} \label{hol-defs}
309 HOL follows standard practice in higher-order logic: only a few connectives
314 logic may equate formulae and even functions over formulae.  But theory~HOL,
364 \caption{Derived rules for HOL} \label{hol-lemmas1}
563 Finite unions and intersections have the same behaviour in HOL as they do
564 in~ZF.  In HOL the intersection of the empty set is well-defined, denoting the
568 HOL's set theory is called \thydx{Set}.  The type $\alpha\,set$ is essentially
838 fashion of \tdx{iffCE}.  See the file \texttt{HOL/Set.ML} for proofs
844 reasoning about the membership relation.  See the file \texttt{HOL/subset.ML}.
849 HOL/equalities.ML}.
875 \caption{Theory \thydx{Fun}} \label{fig:HOL:Fun}
879 Figure~\ref{fig:HOL:Fun} presents a theory of simple properties of functions.
881 of~$f$.  See the file \texttt{HOL/Fun.ML} for a complete listing of the derived
886 on sets in the file \texttt{HOL/mono.ML}.
896 the file \texttt{HOL/simpdata.ML} for a complete listing of the basic
931 HOL provides the tactic \ttindex{hyp_subst_tac}, which substitutes for an
932 equality throughout a subgoal and its hypotheses.  This tactic uses HOL's
936 \label{subsec:HOL:case:splitting}
938 HOL also provides convenient means for case splitting during rewriting. Goals
993 \section{Types}\label{sec:HOL:Types}
994 This section describes HOL's basic predefined types ($\alpha \times \beta$,
997 \texttt{datatype}, is treated separately in {\S}\ref{sec:HOL:datatype}.
1218 see {\S}\ref{sec:HOL:recursive}.  A simple example is addition.
1255 The integers (type \tdx{int}) are also available in HOL, and the reals (type
1256 \tdx{real}) are available in the logic image \texttt{HOL-Complex}.  They support
1282 Reasoning about arithmetic inequalities can be tedious.  Fortunately, HOL
1393 \label{fig:HOL:list-simps}
1420 \label{fig:HOL:list-simps2}
1437 is defined by translation.  For details see~{\S}\ref{sec:HOL:datatype}. There
1448 \texttt{split_if} (see~{\S}\ref{subsec:HOL:case:splitting}).
1452 are shown in Figs.\ts\ref{fig:HOL:list-simps} and~\ref{fig:HOL:list-simps2}.
1458 \label{sec:HOL:datatype}
1462 applications of Isabelle/HOL.  In principle, such types could be defined by
1464 tedious.  The \ttindex{datatype} definition package of Isabelle/HOL (cf.\
1544 Types in HOL must be non-empty. Each of the new datatypes
1624 above, things are a bit more complicated.  Conceptually, Isabelle/HOL unfolds
1699 (see~{\S}\ref{subsec:HOL:case:splitting}).
1715 \subsubsection{The function \cdx{size}}\label{sec:HOL:size}
1800 \section{Old-style recursive function definitions}\label{sec:HOL:recursive}
1854 Proving well-foundedness can be tricky, so Isabelle/HOL provides a collection
1868   and is defined on all datatypes (see {\S}\ref{sec:HOL:size}).
1906 \item \textit{rel} is a HOL expression for the well-founded termination
1929 With the definition of \texttt{gcd} shown above, Isabelle/HOL is unable to
1938 The theory \texttt{HOL/ex/Primes} illustrates how to prove termination
1951 elements of \texttt{gcd.simps}.  Theory \texttt{HOL/Subst/Unify} is a much
1956 Isabelle/HOL can prove the \texttt{gcd} function's termination condition
2002 The Isabelle proof uses HOL's set theory, with the type $\alpha\,set$ and
2073 rules for most of the constructs of HOL's set theory.  We must augment it with
2095 %%% TeX-master: "logics-HOL"