Lines Matching refs:HOL
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"