--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu May 26 21:39:02 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu May 26 22:42:52 2011 +0200
@@ -22,6 +22,62 @@
}
\isamarkuptrue%
%
+\isamarkupsection{Higher-Order Logic%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Isabelle/HOL is based on Higher-Order Logic, a polymorphic
+ version of Church's Simple Theory of Types. HOL can be best
+ understood as a simply-typed version of classical set theory. The
+ logic was first implemented in Gordon's HOL system
+ \cite{mgordon-hol}. It extends Church's original logic
+ \cite{church40} by explicit type variables (naive polymorphism) and
+ a sound axiomatization scheme for new types based on subsets of
+ existing types.
+
+ Andrews's book \cite{andrews86} is a full description of the
+ original Church-style higher-order logic, with proofs of correctness
+ and completeness wrt.\ certain set-theoretic interpretations. The
+ particular extensions of Gordon-style HOL are explained semantically
+ in two chapters of the 1993 HOL book \cite{pitts93}.
+
+ Experience with HOL over decades has demonstrated that higher-order
+ logic is widely applicable in many areas of mathematics and computer
+ science. In a sense, Higher-Order Logic is simpler than First-Order
+ Logic, because there are fewer restrictions and special cases. Note
+ that HOL is \emph{weaker} than FOL with axioms for ZF set theory,
+ which is traditionally considered the standard foundation of regular
+ mathematics, but for most applications this does not matter. If you
+ prefer ML to Lisp, you will probably prefer HOL to ZF.
+
+ \medskip The syntax of HOL follows \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}{\isaliteral{22}{\isachardoublequote}}}-calculus and
+ functional programming. Function application is curried. To apply
+ the function \isa{f} of type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{3}}{\isaliteral{22}{\isachardoublequote}}} to the
+ arguments \isa{a} and \isa{b} in HOL, you simply write \isa{{\isaliteral{22}{\isachardoublequote}}f\ a\ b{\isaliteral{22}{\isachardoublequote}}} (as in ML or Haskell). There is no ``apply'' operator; the
+ existing application of the Pure \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}{\isaliteral{22}{\isachardoublequote}}}-calculus is re-used.
+ Note that in HOL \isa{{\isaliteral{22}{\isachardoublequote}}f\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} means ``\isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{22}{\isachardoublequote}}} applied to
+ the pair \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} (which is notation for \isa{{\isaliteral{22}{\isachardoublequote}}Pair\ a\ b{\isaliteral{22}{\isachardoublequote}}}). The latter typically introduces extra formal efforts that can
+ be avoided by currying functions by default. Explicit tuples are as
+ infrequent in HOL formalizations as in good ML or Haskell programs.
+
+ \medskip Isabelle/HOL has a distinct feel, compared to other
+ object-logics like Isabelle/ZF. It identifies object-level types
+ with meta-level types, taking advantage of the default
+ type-inference mechanism of Isabelle/Pure. HOL fully identifies
+ object-level functions with meta-level functions, with native
+ abstraction and application.
+
+ These identifications allow Isabelle to support HOL particularly
+ nicely, but they also mean that HOL requires some sophistication
+ from the user. In particular, an understanding of Hindley-Milner
+ type-inference with type-classes, which are both used extensively in
+ the standard libraries and applications. Beginners can set
+ \hyperlink{attribute.show-types}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}types}}} or even \hyperlink{attribute.show-sorts}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}sorts}}} to get more
+ explicit information about the result of type-inference.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsection{Inductive and coinductive definitions \label{sec:hol-inductive}%
}
\isamarkuptrue%