5 This chapter describes Isabelle's formalization of Higher-Order Logic, a
6 polymorphic version of Church's Simple Theory of Types.  HOL can be best
7 understood as a simply-typed version of classical set theory.  The monograph
10 All of this material is mainly of historical interest!
59 \caption{Syntax of \texttt{HOL}} \label{hol-constants}
68     term & = & \hbox{expression of class~$term$} \\
76  formula & = & \hbox{expression of type~$bool$} \\
100 binders), while Fig.\ts\ref{hol-grammar} presents the grammar of
113 The universal type class of higher-order terms is called~\cldx{term}.
118 The type of formulae, \tydx{bool}, belongs to class \cldx{term}; thus,
125 HOL allows new types to be declared as subsets of existing types,
131 \cldx{power} --- permit overloading of the operators {\tt+},\index{*"+
139 denote exponentiation of relations (iterated composition).  Unary minus is
143 The constant \cdx{0} is also overloaded.  It serves as the zero element of
144 several types, of which the most important is \tdx{nat} (the natural
151 Theory \thydx{Ord} defines the syntactic class \cldx{ord} of order
155 \cldx{order} of \cldx{ord} which axiomatizes the types that are partially
156 ordered with respect to~$\leq$.  A further subclass \cldx{linorder} of
172   types of terms.  Possibly set \ttindex{show_sorts} to \texttt{true} as
175   \index{unification!incompleteness of}
178   prepared to use \ttindex{res_inst_tac} instead of \texttt{resolve_tac},
181   omitted search paths during unification.\index{tracing!of unification}
196 of~$\exists$ and~$\forall$.  An Isabelle binder, it admits nested
206 supports the original notation of Gordon's {\sc hol} system: \texttt{!}\ 
216 If $\tau$ is a type of class \cldx{ord}, $P$ a formula and $x$ a
217 variable of type $\tau$, then the term \cdx{LEAST}~$x. P[x]$ is defined
222 $P$.\footnote{Class $ord$ does not require much of its instances, so
228 The low priority of binders means that they need to be enclosed in
229 parenthesis when they occur in the context of other operations.  For example,
230 instead of $P \land \forall x. Q$ you need to write $P \land (\forall x. Q)$.
241 \[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n\] 
242 as a uniform means of expressing \texttt{case} constructs.  Therefore \texttt{case}
243 and \sdx{of} are reserved words.  Initially, this is mere syntax and has no
244 logical meaning.  By declaring translations, you can cause instances of the
245 \texttt{case} construct to denote applications of particular case operators.
252 of most other operations.  For example, instead of $f~x = {\tt if\dots
257 \section{Rules of inference}
273 Figure~\ref{hol-rules} shows the primitive inference rules of~HOL, with
274 their~{\ML} names.  Some of the rules deserve additional comments:
276 \item[\tdx{ext}] expresses extensionality of functions.
279 \item[\tdx{someI}] gives the defining property of the Hilbert
280   $\varepsilon$-operator.  It is a form of the Axiom of Choice.  The derived rule
319 only.  Instead users should reason in terms of the derived rules shown below
323 Some of the rules mention type variables; for example, \texttt{refl}
415 simplifying both sides of an equation.
427   from an induction hypothesis. As a generalization of \texttt{mp_tac}, 
429   $P \vec{a}$, ($\vec{x}$ being a vector of $j$ variables)
442         & insertion of element \\
450         &set of sets intersection \\
452         &set of sets union \\
456         & range of a function \\[1ex]
493 \caption{Syntax of the theory \texttt{Set}} \label{hol-set-syntax}
543 \caption{Syntax of the theory \texttt{Set} (continued)} \label{hol-set-syntax2}
547 \section{A formulation of set theory}
549 Whitehead's theory of classes.  Let us use modern terminology and call them
550 {\bf sets}, but note that these sets are distinct from those of ZF set theory,
564 in~ZF.  In HOL the intersection of the empty set is well-defined, denoting the
567 \subsection{Syntax of set theory}\index{*set type}
576 translations.  Figure~\ref{hol-set-syntax2} presents the grammar of the new
589 The set \hbox{\tt{\ttlbrace}$x$.\ $P[x]${\ttrbrace}} consists of all $x$ (of
591 free occurrences of~$x$.  This syntax expands to \cdx{Collect}$(\lambda x.
593 the type of~$x$ implicitly restricts the comprehension.
601 accordingly.  Instead of \texttt{Ball $A$ $P$} and \texttt{Bex $A$ $P$} we may
606 original notation of Gordon's {\sc hol} system is supported as well:
619 The operators $\bigcup A$ and $\bigcap A$ act upon sets of sets.  They are
649 \caption{Rules of the theory \texttt{Set}} \label{hol-set-rules}
737 \subsection{Axioms and rules of set theory}
738 Figure~\ref{hol-set-rules} presents the rules of theory \thydx{Set}.  The
750 %set~$A$, which specifies a subset of its domain type.  In a type
751 %definition, $f$ is the abstraction function and $A$ is the set of valid
752 %representations; we should not expect $f$ to be injective outside of~$A$.
833 obvious and resemble rules of Isabelle's ZF set theory.  Certain rules, such
838 fashion of \tdx{iffCE}.  See the file \texttt{HOL/Set.ML} for proofs
841 Figure~\ref{hol-subset} presents lattice properties of the subset relation.
878 \subsection{Properties of functions}\nopagebreak
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
885 There is also a large collection of monotonicity theorems for constructions
896 the file \texttt{HOL/simpdata.ML} for a complete listing of the basic
900 {Chaps.\ts\ref{substitution} and~\ref{simp-chap}} for details of substitution
903 \begin{warn}\index{simplification!of conjunctions}%
905   left part of a conjunction helps in simplifying the right part.  This effect
910 \begin{warn}\index{simplification!of \texttt{if}}\label{if-simp}%
911   By default only the condition of an \ttindex{if} is simplified but not the
914   full simplification of all parts of a conditional you must remove
919 of nontermination or because its left-hand side is too flexible ---
922 \item[\ttindexbold{stac} $thm$ $i,$] where $thm$ is of the form $lhs = rhs$,
923   replaces in subgoal $i$ instances of $lhs$ by corresponding instances of
924   $rhs$.  In case of multiple instances of $lhs$ in subgoal $i$, backtracking
939 containing a subterm of the form \texttt{if}~$b$~{\tt then\dots else\dots}
947 For example, a simple instance of $(*)$ is
953 left-hand side is not a higher-order pattern in the sense of
956 \ttindexbold{addsplits} of type \texttt{simpset * thm list -> simpset}
962 The effect is that after each round of simplification, one occurrence of
963 \texttt{if} is split acording to \texttt{split_if}, until all occurrences of
969 the inverse of \texttt{addsplits}:
974 In general, \texttt{addsplits} accepts rules of the form
978 where $c$ is a constant and $rhs$ is arbitrary. Note that $(*)$ is of the
985 imperative versions of \texttt{addsplits} and \texttt{delsplits}
1014         & general sum of sets
1068   by the parser and printer.  Thus the internal and external form of a term
1087   {\tt!!}-quantified variables of product type by individual variables for
1107 The definition of products and sums in terms of existing types is not
1168 \caption{The type of natural numbers, \tydx{nat}} \label{hol-nat1}
1193 \subsection{The type of natural numbers, \textit{nat}}
1197 traditional way.  The axiom of infinity postulates a type~\tydx{ind} of
1203 Type~\tydx{nat} is an instance of class~\cldx{ord}, which makes the overloaded
1204 functions of this class (especially \cdx{<} and \cdx{<=}, but also \cdx{min},
1207 also an instance of class \cldx{linorder}.
1215 \texttt{nat} are part of the default simpset.
1219 Here, \texttt{op +} is the name of the infix operator~\texttt{+}, following
1227 of the form
1229 case \(e\) of 0 => \(a\) | Suc \(m\) => \(b\)
1232 the order of the two cases.
1242 %The transitive closure of \cdx{pred_nat} is~$<$.  Many functions on the
1257 the expected operations of addition (\texttt{+}), subtraction (\texttt{-}) and
1261 they inherit the relational operators and all the usual properties of linear
1265 All three numeric types admit numerals of the form \texttt{$sd\ldots d$},
1266 where $s$ is an optional minus sign and $d\ldots d$ is a string of digits.
1269 integer division of \texttt{54342339} by \texttt{3452} takes about five
1271 of relational operators (reducing \texttt{z+x<x+y} to \texttt{z<y}, for
1276 match a pattern of the form \texttt{Suc $k$}.  You can re-arrange the form of
1284 addition and subtraction. The simplifier invokes a weak version of this
1291 existential. The running time is exponential in the number of
1292 occurrences of {\tt min}, {\tt max}, and {\tt-} because they require case
1408 take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)
1411 drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)
1433 lists.  A \sdx{case} construct of the form
1435 case $e$ of [] => $a$  |  \(x\)\#\(xs\) => b
1441 P(\mathtt{case}~e~\mathtt{of}~\texttt{[] =>}~a ~\texttt{|}~
1450 \texttt{List} provides a basic library of list processing functions defined by
1461 Inductive datatypes, similar to those of \ML, frequently appear in
1462 applications of Isabelle/HOL.  In principle, such types could be defined by
1464 tedious.  The \ttindex{datatype} definition package of Isabelle/HOL (cf.\ 
1469 specification of new inductive types using a notation similar to {\ML} or
1474 of a more uniform view on standard theories.
1480 A general \texttt{datatype} definition is of the following form:
1492 where $\vec{\alpha} = (\alpha@1,\ldots,\alpha@h)$ is a list of type variables,
1498 \item $\tau$ is non-recursive, i.e.\ $\tau$ does not contain any of the
1502 the type constructor of an already existing datatype and $\tau'@1,\ldots,\tau'@{h'}$
1505 type and $\sigma$ is non-recursive (i.e. the occurrences of the newly defined
1509 of the form
1514 example of a datatype is the type \texttt{list}, which can be defined by
1544 Types in HOL must be non-empty. Each of the new datatypes
1547 $\tau^j@{i,i'}$ of the form $(\vec{\alpha})t@{j'}$ the datatype
1550 If there are no nested occurrences of the newly defined datatypes, obviously
1551 at least one of the newly defined datatypes $(\vec{\alpha})t@j$
1559 \subsubsection{Freeness of the constructors}
1561 The datatype constructors are automatically defined as functions of their
1575 Since the number of distinctness inequalities is quadratic in the number of
1579 of the default simpset, may be referred to by the ML identifier
1585 datatypes without nested recursion, this is of the following form:
1655 is of the form
1672 \mbox{\tt case}~e~\mbox{\tt of} & C^j@1~x@{1,1}~\dots~x@{1,m^j@1} & \To & e@1 \\
1681   are not supported (with the exception of tuples).  Violating this
1697 where $t@j$\texttt{_case} is the internal name of the \texttt{case}-construct.
1705 \begin{warn}\index{simplification!of \texttt{case}}%
1708   page~\pageref{if-simp}). Only if that reduces to a constructor is one of
1709   the arms of the \texttt{case}-construct exposed and simplified. To ensure
1710   full simplification of all parts of a \texttt{case}-construct for datatype
1717 Theory \texttt{NatArith} declares a generic function \texttt{size} of type
1718 $\alpha\To nat$.  Each datatype defines a particular instance of \texttt{size}
1733 size of a leaf is 0 and the size of a node is the sum of the sizes of its
1744 Most of the theorems about datatypes become part of the default simpset and
1750  type of $x$ is a datatype.
1754   is the canonical way to prove properties of mutually recursive datatypes
1759 constructors of the datatype suffices.
1769 among the premises of the subgoal. Case distinction applies to arbitrary terms.
1793 inequalities in both directions.  The reduction rules of the {\tt
1796 In case of mutually recursive datatypes, \texttt{recs}, \texttt{size}, \texttt{induct}
1835 disambiguates overlapping patterns by taking the order of rules into account.
1838 %For example, here is a declaration of the list function \cdx{hd}:
1847 The well-founded relation defines a notion of ``smaller'' for the function's
1855 of operators for building well-founded relations.  The package recognises
1857 well-founded.  Here are those operators, in order of importance:
1866   returns a result expressed in terms of the function \texttt{size}.  It is
1870 \item $\mathop{\mathtt{inv_image}} R\;f$ is a generalisation of
1876 \item $R@1\texttt{<*lex*>}R@2$ is the lexicographic product of two relations.
1894 The general form of a well-founded recursive definition is
1903 \item \textit{function} is the name of the function, either as an \textit{id}
1914     conditions}: assertions that arguments of recursive calls decrease under
1921   is a tuple of distinct variables.  If more than one equation is present then
1922   $f$ is defined by pattern-matching on components of its argument whose type
1926   a list of theorems.
1929 With the definition of \texttt{gcd} shown above, Isabelle/HOL is unable to
1930 prove one termination condition.  It remains as a precondition of the
1942 proof of the termination conditions:
1951 elements of \texttt{gcd.simps}.  Theory \texttt{HOL/Subst/Unify} is a much
1952 more complicated example of this process, where the termination conditions can
1969 which returns a list of theorems. Thus you can, for example, remove specific
1970 clauses from the simpset. Note that a single clause may give rise to a set of
1984 remain unproved, they will become additional premises of this rule.
1999 of~$\alpha$.  This version states that for every function from $\alpha$ to
2007 The set~$S$ is given as an unknown instead of a
2038 Now we use a bit of creativity.  Suppose that~$\Var{S}$ has the form of a
2049 Forcing a contradiction between the two assumptions of subgoal~1
2050 completes the instantiation of~$S$.  It is now the set $\{x. x\not\in
2073 rules for most of the constructs of HOL's set theory.  We must augment it with

Indexes created Sun Jun 23 19:15:37 MDT 2024