# HG changeset patch # User wenzelm # Date 1306442572 -7200 # Node ID e6ed6b951201ab87749d80401ebc75c71e60076a # Parent 68bc69bdce8828d243bd6c45c04ef4305daed3aa moved/updated basic HOL overview; diff -r 68bc69bdce88 -r e6ed6b951201 doc-src/HOL/HOL.tex --- 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 \\ diff -r 68bc69bdce88 -r e6ed6b951201 doc-src/IsarRef/Thy/HOL_Specific.thy --- 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 "\"}-calculus and + functional programming. Function application is curried. To apply + the function @{text f} of type @{text "\\<^sub>1 \ \\<^sub>2 \ \\<^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 "\"}-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 diff -r 68bc69bdce88 -r e6ed6b951201 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- 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%