--- a/doc-src/HOL/HOL.tex Thu May 26 21:39:02 2011 +0200
+++ b/doc-src/HOL/HOL.tex Thu May 26 22:42:52 2011 +0200
@@ -2,38 +2,6 @@
\index{higher-order logic|(}
\index{HOL system@{\sc hol} system}
-The theory~\thydx{HOL} implements higher-order logic. It is based on
-Gordon's~{\sc hol} system~\cite{mgordon-hol}, which itself is based on
-Church's original paper~\cite{church40}. Andrews's book~\cite{andrews86} is a
-full description of the original Church-style higher-order logic. Experience
-with the {\sc hol} system has demonstrated that higher-order logic is widely
-applicable in many areas of mathematics and computer science, not just
-hardware verification, {\sc hol}'s original \textit{raison d'{\^e}tre\/}. It
-is weaker than ZF set theory but for most applications this does not matter.
-If you prefer {\ML} to Lisp, you will probably prefer HOL to~ZF.
-
-The syntax of HOL\footnote{Earlier versions of Isabelle's HOL used a different
- syntax. Ancient releases of Isabelle included still another version of~HOL,
- with explicit type inference rules~\cite{paulson-COLOG}. This version no
- longer exists, but \thydx{ZF} supports a similar style of reasoning.}
-follows $\lambda$-calculus and functional programming. Function application
-is curried. To apply the function~$f$ of type $\tau@1\To\tau@2\To\tau@3$ to
-the arguments~$a$ and~$b$ in HOL, you simply write $f\,a\,b$. There is no
-`apply' operator as in \thydx{ZF}. Note that $f(a,b)$ means ``$f$ applied to
-the pair $(a,b)$'' in HOL. We write ordered pairs as $(a,b)$, not $\langle
-a,b\rangle$ as in ZF.
-
-HOL has a distinct feel, compared with ZF and CTT. It identifies object-level
-types with meta-level types, taking advantage of Isabelle's built-in
-type-checker. It identifies object-level functions with meta-level functions,
-so it uses Isabelle's operations for abstraction and application.
-
-These identifications allow Isabelle to support HOL particularly nicely, but
-they also mean that HOL requires more sophistication from the user --- in
-particular, an understanding of Isabelle's type system. Beginners should work
-with \texttt{show_types} (or even \texttt{show_sorts}) set to \texttt{true}.
-
-
\begin{figure}
\begin{constants}
\it name &\it meta-type & \it description \\
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Thu May 26 21:39:02 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Thu May 26 22:42:52 2011 +0200
@@ -4,6 +4,60 @@
chapter {* Isabelle/HOL \label{ch:hol} *}
+section {* Higher-Order Logic *}
+
+text {* 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 @{text "\<lambda>"}-calculus and
+ functional programming. Function application is curried. To apply
+ the function @{text f} of type @{text "\<tau>\<^sub>1 \<Rightarrow> \<tau>\<^sub>2 \<Rightarrow> \<tau>\<^sub>3"} to the
+ arguments @{text a} and @{text b} in HOL, you simply write @{text "f
+ a b"} (as in ML or Haskell). There is no ``apply'' operator; the
+ existing application of the Pure @{text "\<lambda>"}-calculus is re-used.
+ Note that in HOL @{text "f (a, b)"} means ``@{text "f"} applied to
+ the pair @{text "(a, b)"} (which is notation for @{text "Pair a
+ b"}). 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
+ @{attribute show_types} or even @{attribute show_sorts} to get more
+ explicit information about the result of type-inference. *}
+
+
section {* Inductive and coinductive definitions \label{sec:hol-inductive} *}
text {* An \emph{inductive definition} specifies the least predicate
--- 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%