Manual/Tutorial/logic.tex

1 \chapter{The \HOL{} Logic}\label{HOLlogic}
3 The \HOL{}  system  supports \emph{higher order logic}.
12 In this chapter, we will give a brief overview of the notation used to write expressions of the \HOL{} logic in \ML{}, and also discuss some fundamental  \HOL{} proof techniques.
14 The syntax and semantics of the particular logical system supported by \HOL{} is described in detail in \DESCRIPTION.
15 Readers who wish to see \HOL{} in action, without the introduction to the finer details of \HOL's fundamentals, might like to skip ahead to Chapter~\ref{chap:euclid}.
18 The table below summarizes a useful subset of the (ASCII) notation used in \HOL.
23 \multicolumn{4}{|c|}{\bf Terms of the HOL Logic} \\
25 {\it Kind of term} & {\it \HOL{} notation} &
53 Terms of the \HOL{} logic are represented in \ML{} by an \emph{abstract type} called {\small\verb|term|}.
75 Terms of the \HOL{} logic are quite similar to \ML{} expressions, and this can at first be confusing.
78 The \HOL{} type of this term is \holtxt{num \# num}.
81 \paragraph{Syntax of \HOL\ types}
83 The types of \HOL{} terms form an \ML{} type called \ml{hol_type}.
103 To try to minimise confusion between the logical types of \HOL{} terms and the \ML{} types of \ML{} expressions, the former will be referred to as \emph{object language types} and the latter as \emph{meta-language types}.
117 \HOL{} terms can be input, as above, by using explicit \emph{quotation}, or they can be constructed by calling \ML{} constructor functions.
134 A large collection of term constructors and destructors is available for the core theories in \HOL.
145 There are actually only four different kinds of term in \HOL: variables, constants, function applications (\ml{``$t_1$ $t_2$``}), and lambda abstractions (\ml{``\bs$x$.$t$``}).
150 When a quotation is entered into \HOL{}, the type checking algorithm uses the types of constants to infer the types of variables in the same quotation.
151 For example, in the following case, the \HOL{} type checker used the known type \holtxt{bool->bool} of boolean negation (\holtxt{\td}) to deduce that the variable \holtxt{x} must have type \holtxt{bool}.
168 <<HOL message: inventing new type variable names: 'a.>>
175 <<HOL message: inventing new type variable names: 'a, 'b.>>
332 \section{Basic Proof in \HOL{}}
341 This section discusses the nature of proof in \HOL{}.
345 Theorems are represented in \HOL{} by values of an abstract type \ml{thm}.
347 In \HOL, following \LCF, this consists in applying \ML{} functions representing \emph{rules of inference} to axioms or previously generated theorems.
350 There are five axioms of the \HOL{} logic and eight primitive inference rules.
378 \footnote{\ml{SPEC} is not a primitive rule of inference in the HOL logic, but is a derived rule.
403 When one of the standard \ml{HOL\_ERR} exceptions is raised, more information about the failure can often be gained by using the \ml{Raise} function.%
405 However, when passed a \ml{HOL\_ERR} exception, it prints out some useful information before passing the exception on to the next level.}
424 A proof in the \HOL{} system is constructed by repeatedly applying inference rules to axioms or to previously proved theorems.
426 The proof generating tools in the \HOL{} system are just those of \LCF, and are described later.
434 The five axioms and eight primitive inference rules of the \HOL{} logic are described in detail in the document \DESCRIPTION.
435 Every value of type \ml{thm} in the \HOL{} system can be obtained by repeatedly applying primitive inference rules to axioms.
436 When the \HOL{} system is built, the eight primitive rules of inference are defined and the five axioms are bound to their \ML{} names.
446 Three of the primitive inference rules of the \HOL{} logic are
494 In \HOL\, the rule \ml{MP} of Modus Ponens is specified in conventional notation by:
502 of \ml{MP} and also a common error, namely not supplying the \HOL\
508 <<HOL message: inventing new type variable names: 'a.>>
512 <<HOL message: inventing new type variable names: 'a.>>
538 \HOL{} can be made to print out hypotheses of theorems explicitly by setting the global flag \ml{show\_assums} to true.
567 The sequence of theorems: \ml{Th3}, \ml{Th5}, \ml{Th6}, \ml{Th7}, \ml{Th8} constitutes a proof in \HOL{} of the theorem \ml{|-\ t1 ==> (t1 ==> t2) ==> t2}.
690 defined when the \HOL{} system is built. For a description of the main
742 \ml{REWRITE\_RULE} is not a primitive in \HOL, but is a derived rule.
753 There are elaborate facilities in \HOL{} for producing customized rewriting tools which scan through terms in user programmed orders; \ml{REWRITE\_RULE} is the tip of an iceberg, see \DESCRIPTION\ for more details.
770   is usually primitive.  In HOL the rule is called {\tt CONJ} and its
778 \noindent In \HOL,  $\wedge$-introduction is  represented by  the \ML{} function
816 A \emph{goal} in \HOL{} is a pair \ml{([$t_1$,\ldots,$t_n$],$t$)} of \ML{} type \ml{term list~*~term}.
849 theorem in \HOL, called \ml{TRUTH}, that achieves this goal:
1090 \HOL{} provides a package for building and traversing the tree of subgoals, stacking the justification functions and applying them properly; this package was originally implemented for \LCF\ by Larry Paulson.
1102 Some important tacticals in the \HOL{} system are listed below.
1170 theory \ml{arithmetic} \HOL{} is made.
1208 \noindent These proofs are performed when the \HOL{} system is made and the
1276 \subsection{Some tactics built into \HOL{}}
1279 \HOL{} system (including those already discussed).  The tactics given
1318   defined by \HOL{} include \ml{bossLib.std\_ss}, which has basic