# HG changeset patch # User clasohm # Date 804420524 -7200 # Node ID 7be0684950a3227090d338df5cdc79ba0a4df4db # Parent 1831ba01c90c1bbaace21eb34572e05041dd0647 changes made by Lawrence Paulson diff -r 1831ba01c90c -r 7be0684950a3 doc-src/Logics/CHOL.tex --- a/doc-src/Logics/CHOL.tex Thu Jun 29 10:43:07 1995 +0200 +++ b/doc-src/Logics/CHOL.tex Thu Jun 29 12:08:44 1995 +0200 @@ -1,37 +1,36 @@ %% $Id$ \chapter{Higher-Order Logic} \index{higher-order logic|(} -\index{CHOL system@{\sc chol} system} +\index{HOL system@{\sc chol} 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 higher-order logic. Experience with the {\sc hol} system +has demonstrated that higher-order logic is useful for hardware verification; +beyond this, it is widely applicable in many areas of mathematics. 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 theory~\thydx{CHOL} implements higher-order logic with curried -function application. 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 higher-order logic. Experience with the {\sc hol} -system has demonstrated that higher-order logic is useful for hardware -verification; beyond this, it is widely applicable in many areas of -mathematics. 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 \CHOL\ to~{\ZF}. +The syntax of Isabelle's \HOL\ has recently been changed to look more like the +traditional syntax of higher-order logic. Function application is now +curried. To apply the function~$f$ to the arguments~$a$ and~$b$ in \HOL, you +must write $f\,a\,b$. 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} and earlier versions of \HOL. Early 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. -\CHOL\ is a modified version of Isabelle's \HOL\ and uses curried function -application. Therefore the expression $f(a,b)$ (which in \HOL\ means -``f applied to the two arguments $a$ and $b$'') means ``f applied to -the pair $(a,b)$'' in \CHOL. N.B. that ordered pairs in \HOL\ are written as -$$ while in \CHOL\ the syntax $(a,b)$ is used. Previous -releases of Isabelle also included a different 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. - -\CHOL\ has a distinct feel, compared with {\ZF} and {\CTT}. It +\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. There is no `apply' operator: function applications are written as simply~$f~a$ rather than $f{\tt`}a$. -These identifications allow Isabelle to support \CHOL\ particularly nicely, -but they also mean that \CHOL\ requires more sophistication from the user +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 {\tt show_types} set to {\tt true}. Gain experience by working in first-order logic before attempting to use higher-order logic. @@ -122,7 +121,7 @@ & | & "EX!~" id~id^* " . " formula \end{array} \] -\caption{Full grammar for \CHOL} \label{chol-grammar} +\caption{Full grammar for \HOL} \label{chol-grammar} \end{figure} @@ -147,7 +146,7 @@ $\neg(a=b)$. \begin{warn} - \CHOL\ has no if-and-only-if connective; logical equivalence is expressed + \HOL\ has no if-and-only-if connective; logical equivalence is expressed using equality. But equality has a high priority, as befitting a relation, while if-and-only-if typically has the lowest priority. Thus, $\neg\neg P=P$ abbreviates $\neg\neg (P=P)$ and not $(\neg\neg P)=P$. @@ -155,14 +154,14 @@ parentheses. \end{warn} -\subsection{Types}\label{CHOL-types} +\subsection{Types}\label{HOL-types} The type of formulae, \tydx{bool}, belongs to class \cldx{term}; thus, formulae are terms. The built-in type~\tydx{fun}, which constructs function types, is overloaded with arity {\tt(term,term)term}. Thus, $\sigma\To\tau$ belongs to class~{\tt term} if $\sigma$ and~$\tau$ do, allowing quantification over functions. -Types in \CHOL\ must be non-empty; otherwise the quantifier rules would be +Types in \HOL\ must be non-empty; otherwise the quantifier rules would be unsound. I have commented on this elsewhere~\cite[\S7]{paulson-COLOG}. \index{type definitions} @@ -185,7 +184,7 @@ \subsection{Binders} Hilbert's {\bf description} operator~$\epsilon x.P[x]$ stands for some~$a$ -satisfying~$P[a]$, if such exists. Since all terms in \CHOL\ denote +satisfying~$P[a]$, if such exists. Since all terms in \HOL\ denote something, a description is always meaningful, but we do not know its value unless $P[x]$ defines it uniquely. We may write descriptions as \cdx{Eps}($P$) or use the syntax @@ -199,8 +198,8 @@ $\exists!x. \exists!y.P~x~y$; note that this does not mean that there exists a unique pair $(x,y)$ satisfying~$P~x~y$. -\index{*"! symbol}\index{*"? symbol}\index{CHOL system@{\sc hol} system} -Quantifiers have two notations. As in Gordon's {\sc hol} system, \CHOL\ +\index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system} +Quantifiers have two notations. As in Gordon's {\sc hol} system, \HOL\ uses~{\tt!}\ and~{\tt?}\ to stand for $\forall$ and $\exists$. The existential quantifier must be followed by a space; thus {\tt?x} is an unknown, while \verb'? x.f x=y' is a quantification. Isabelle's usual @@ -219,7 +218,7 @@ the constant~\cdx{Let}. It can be expanded by rewriting with its definition, \tdx{Let_def}. -\CHOL\ also defines the basic syntax +\HOL\ also defines the basic syntax \[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n\] as a uniform means of expressing {\tt case} constructs. Therefore {\tt case} and \sdx{of} are reserved words. However, so far this is mere @@ -240,7 +239,7 @@ \tdx{selectI} P(x::'a) ==> P(@x.P x) \tdx{True_or_False} (P=True) | (P=False) \end{ttbox} -\caption{The {\tt CHOL} rules} \label{chol-rules} +\caption{The {\tt HOL} rules} \label{chol-rules} \end{figure} @@ -260,12 +259,12 @@ \tdx{if_def} If P x y == (\%P x y.@z::'a.(P=True --> z=x) & (P=False --> z=y)) \tdx{Let_def} Let s f == f s \end{ttbox} -\caption{The {\tt CHOL} definitions} \label{chol-defs} +\caption{The {\tt HOL} definitions} \label{chol-defs} \end{figure} \section{Rules of inference} -Figure~\ref{chol-rules} shows the inference rules of~\CHOL{}, with +Figure~\ref{chol-rules} shows the inference rules of~\HOL{}, with their~{\ML} names. Some of the rules deserve additional comments: \begin{ttdescription} \item[\tdx{ext}] expresses extensionality of functions. @@ -279,13 +278,13 @@ shown by Diaconescu; see Paulson~\cite{paulson-COLOG} for details.} \end{ttdescription} -\CHOL{} follows standard practice in higher-order logic: only a few +\HOL{} follows standard practice in higher-order logic: only a few connectives are taken as primitive, with the remainder defined obscurely (Fig.\ts\ref{chol-defs}). Gordon's {\sc hol} system expresses the corresponding definitions \cite[page~270]{mgordon-hol} using object-equality~({\tt=}), which is possible because equality in higher-order logic may equate formulae and even functions over formulae. -But theory~\CHOL{}, like all other Isabelle theories, uses +But theory~\HOL{}, like all other Isabelle theories, uses meta-equality~({\tt==}) for definitions. Some of the rules mention type variables; for example, {\tt refl} @@ -350,7 +349,7 @@ \subcaption{Logical equivalence} \end{ttbox} -\caption{Derived rules for \CHOL} \label{chol-lemmas1} +\caption{Derived rules for \HOL} \label{chol-lemmas1} \end{figure} @@ -540,17 +539,17 @@ Although sets may contain other sets as elements, the containing set must have a more complex type. \end{itemize} -Finite unions and intersections have the same behaviour in \CHOL\ as they -do in~{\ZF}. In \CHOL\ the intersection of the empty set is well-defined, +Finite unions and intersections have the same behaviour in \HOL\ as they +do in~{\ZF}. In \HOL\ the intersection of the empty set is well-defined, denoting the universal set for the given type. \subsection{Syntax of set theory}\index{*set type} -\CHOL's set theory is called \thydx{Set}. The type $\alpha\,set$ is +\HOL's set theory is called \thydx{Set}. The type $\alpha\,set$ is essentially the same as $\alpha\To bool$. The new type is defined for clarity and to avoid complications involving function types in unification. Since Isabelle does not support type definitions (as mentioned in -\S\ref{CHOL-types}), the isomorphisms between the two types are declared +\S\ref{HOL-types}), the isomorphisms between the two types are declared explicitly. Here they are natural: {\tt Collect} maps $\alpha\To bool$ to $\alpha\,set$, while \hbox{\tt op :} maps in the other direction (ignoring argument order). @@ -823,27 +822,27 @@ \tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are not strictly necessary but yield more natural proofs. Similarly, \tdx{equalityCE} supports classical reasoning about extensionality, -after the fashion of \tdx{iffCE}. See the file {\tt CHOL/Set.ML} for +after the fashion of \tdx{iffCE}. See the file {\tt HOL/Set.ML} for proofs pertaining to set theory. Figure~\ref{chol-fun} presents derived inference rules involving functions. They also include rules for \cdx{Inv}, which is defined in theory~{\tt - CHOL}; note that ${\tt Inv}~f$ applies the Axiom of Choice to yield an + HOL}; note that ${\tt Inv}~f$ applies the Axiom of Choice to yield an inverse of~$f$. They also include natural deduction rules for the image and range operators, and for the predicates {\tt inj} and {\tt inj_onto}. Reasoning about function composition (the operator~\sdx{o}) and the predicate~\cdx{surj} is done simply by expanding the definitions. See -the file {\tt CHOL/fun.ML} for a complete listing of the derived rules. +the file {\tt HOL/fun.ML} for a complete listing of the derived rules. Figure~\ref{chol-subset} presents lattice properties of the subset relation. Unions form least upper bounds; non-empty intersections form greatest lower bounds. Reasoning directly about subsets often yields clearer proofs than -reasoning about the membership relation. See the file {\tt CHOL/subset.ML}. +reasoning about the membership relation. See the file {\tt HOL/subset.ML}. Figure~\ref{chol-equalities} presents many common set equalities. They include commutative, associative and distributive laws involving unions, intersections and complements. The proofs are mostly trivial, using the -classical reasoner; see file {\tt CHOL/equalities.ML}. +classical reasoner; see file {\tt HOL/equalities.ML}. \begin{figure} @@ -911,23 +910,23 @@ \section{Generic packages and classical reasoning} -\CHOL\ instantiates most of Isabelle's generic packages; -see {\tt CHOL/ROOT.ML} for details. +\HOL\ instantiates most of Isabelle's generic packages; +see {\tt HOL/ROOT.ML} for details. \begin{itemize} \item -Because it includes a general substitution rule, \CHOL\ instantiates the +Because it includes a general substitution rule, \HOL\ instantiates the tactic {\tt hyp_subst_tac}, which substitutes for an equality throughout a subgoal and its hypotheses. \item It instantiates the simplifier, defining~\ttindexbold{HOL_ss} as the simplification set for higher-order logic. Equality~($=$), which also expresses logical equivalence, may be used for rewriting. See the file -{\tt CHOL/simpdata.ML} for a complete listing of the simplification +{\tt HOL/simpdata.ML} for a complete listing of the simplification rules. \item It instantiates the classical reasoner, as described below. \end{itemize} -\CHOL\ derives classical introduction rules for $\disj$ and~$\exists$, as +\HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule; recall Fig.\ts\ref{chol-lemmas2} above. @@ -1087,7 +1086,7 @@ Isabelle provides no means of verifying that such overloading is sensible; there is no means of specifying the operators' properties and verifying that instances of the operators satisfy those properties. To be safe, the -\CHOL\ theory includes no polymorphic axioms asserting general properties of +\HOL\ theory includes no polymorphic axioms asserting general properties of $<$ and~$\leq$. Theory \thydx{Arith} develops arithmetic on the natural numbers. It @@ -1161,22 +1160,22 @@ \begin{figure} \begin{ttbox}\makeatother \tdx{list_rec_Nil} list_rec [] c h = c -\tdx{list_rec_Cons} list_rec a#l c h = h a l (list_rec l c h) +\tdx{list_rec_Cons} list_rec (a#l) c h = h a l (list_rec l c h) \tdx{list_case_Nil} list_case c h [] = c -\tdx{list_case_Cons} list_case c h x#xs = h x xs +\tdx{list_case_Cons} list_case c h (x#xs) = h x xs \tdx{map_Nil} map f [] = [] -\tdx{map_Cons} map f x \# xs = f x \# map f xs +\tdx{map_Cons} map f (x#xs) = f x # map f xs \tdx{null_Nil} null [] = True -\tdx{null_Cons} null x#xs = False +\tdx{null_Cons} null (x#xs) = False -\tdx{hd_Cons} hd x#xs = x -\tdx{tl_Cons} tl x#xs = xs +\tdx{hd_Cons} hd (x#xs) = x +\tdx{tl_Cons} tl (x#xs) = xs \tdx{ttl_Nil} ttl [] = [] -\tdx{ttl_Cons} ttl x#xs = xs +\tdx{ttl_Cons} ttl (x#xs) = xs \tdx{append_Nil} [] @ ys = ys \tdx{append_Cons} (x#xs) \at ys = x # xs \at ys @@ -1185,10 +1184,10 @@ \tdx{mem_Cons} x mem (y#ys) = if y=x then True else x mem ys \tdx{filter_Nil} filter P [] = [] -\tdx{filter_Cons} filter P x#xs = if P x then x#filter P xs else filter P xs +\tdx{filter_Cons} filter P (x#xs) = if P x then x#filter P xs else filter P xs \tdx{list_all_Nil} list_all P [] = True -\tdx{list_all_Cons} list_all P x#xs = (P x & list_all P xs) +\tdx{list_all_Cons} list_all P (x#xs) = (P x & list_all P xs) \end{ttbox} \caption{Rewrite rules for lists} \label{chol-list-simps} \end{figure} @@ -1197,7 +1196,7 @@ \subsection{The type constructor for lists, {\tt list}} \index{*list type} -\CHOL's definition of lists is an example of an experimental method for +\HOL's definition of lists is an example of an experimental method for handling recursive data types. Figure~\ref{chol-list} presents the theory \thydx{List}: the basic list operations with their types and properties. @@ -1374,10 +1373,10 @@ \subsubsection{The datatype $\alpha~list$} We want to define the type $\alpha~list$.\footnote{Of course there is a list - type in CHOL already. This is only an example.} To do this we have to build -a new theory that contains the type definition. We start from {\tt CHOL}. + type in HOL already. This is only an example.} To do this we have to build +a new theory that contains the type definition. We start from {\tt HOL}. \begin{ttbox} -MyList = CHOL + +MyList = HOL + datatype 'a list = Nil | Cons 'a ('a list) end \end{ttbox} @@ -1431,7 +1430,7 @@ \verb|#| instead of {\tt Cons}. To do this we simply add mixfix annotations after the constructor declarations as follows: \begin{ttbox} -MyList = CHOL + +MyList = HOL + datatype 'a list = "[]" ("[]") | "#" 'a ('a list) (infixr 70) end @@ -1473,7 +1472,7 @@ consts app :: "['a list,'a list] => 'a list" rules app_Nil "app [] ys = ys" - app_Cons "app x#xs ys = x#app xs ys" + app_Cons "app (x#xs) ys = x#app xs ys" end \end{ttbox} this carries with it the danger of accidentally asserting an inconsistency, @@ -1484,7 +1483,7 @@ consts app :: "'['a list,'a list] => 'a list" primrec app MyList.list app_Nil "app [] ys = ys" - app_Cons "app x#xs ys = x#app xs ys" + app_Cons "app (x#xs) ys = x#app xs ys" end \end{ttbox} The system will now check that the two rules \verb$app_Nil$ and @@ -1590,7 +1589,7 @@ This package is derived from the ZF one, described in a separate paper,\footnote{It appeared in CADE~\cite{paulson-CADE} and a longer version is distributed with Isabelle.} which you should refer to -in case of difficulties. The package is simpler than ZF's, thanks to CHOL's +in case of difficulties. The package is simpler than ZF's, thanks to HOL's automatic type-checking. The type of the (co)inductive determines the domain of the fixedpoint definition, and the package does not use inference rules for type-checking. @@ -1728,27 +1727,27 @@ monos "[Pow_mono]" end \end{ttbox} -The CHOL distribution contains many other inductive definitions, such as the -theory {\tt CHOL/ex/PropLog.thy} and the directory {\tt CHOL/IMP}. The -theory {\tt CHOL/ex/LList.thy} contains coinductive definitions. +The HOL distribution contains many other inductive definitions, such as the +theory {\tt HOL/ex/PropLog.thy} and the directory {\tt HOL/IMP}. The +theory {\tt HOL/ex/LList.thy} contains coinductive definitions. \index{*coinductive|)} \index{*inductive|)} \underscoreoff \section{The examples directories} -Directory {\tt CHOL/Subst} contains Martin Coen's mechanisation of a theory of +Directory {\tt HOL/Subst} contains Martin Coen's mechanisation of a theory of substitutions and unifiers. It is based on Paulson's previous mechanisation in {\LCF}~\cite{paulson85} of Manna and Waldinger's theory~\cite{mw81}. -Directory {\tt CHOL/IMP} contains a mechanised version of a semantic +Directory {\tt HOL/IMP} contains a mechanised version of a semantic equivalence proof taken from Winskel~\cite{winskel93}. It formalises the denotational and operational semantics of a simple while-language, then proves the two equivalent. It contains several datatype and inductive definitions, and demonstrates their use. -Directory {\tt CHOL/ex} contains other examples and experimental proofs in -{\CHOL}. Here is an overview of the more interesting files. +Directory {\tt HOL/ex} contains other examples and experimental proofs in +{\HOL}. Here is an overview of the more interesting files. \begin{itemize} \item File {\tt cla.ML} demonstrates the classical reasoner on over sixty predicate calculus theorems, ranging from simple tautologies to @@ -1811,7 +1810,7 @@ of~$\alpha$. This version states that for every function from $\alpha$ to its powerset, some subset is outside its range. -The Isabelle proof uses \CHOL's set theory, with the type $\alpha\,set$ and +The Isabelle proof uses \HOL's set theory, with the type $\alpha\,set$ and the operator \cdx{range}. The set~$S$ is given as an unknown instead of a quantified variable so that we may inspect the subset found by the proof. \begin{ttbox} @@ -1878,7 +1877,7 @@ \end{ttbox} How much creativity is required? As it happens, Isabelle can prove this theorem automatically. The classical set \ttindex{set_cs} contains rules -for most of the constructs of \CHOL's set theory. We must augment it with +for most of the constructs of \HOL's set theory. We must augment it with \tdx{equalityCE} to break up set equalities, and then apply best-first search. Depth-first search would diverge, but best-first search successfully navigates through the large search space. diff -r 1831ba01c90c -r 7be0684950a3 doc-src/Logics/HOL.tex --- a/doc-src/Logics/HOL.tex Thu Jun 29 10:43:07 1995 +0200 +++ b/doc-src/Logics/HOL.tex Thu Jun 29 12:08:44 1995 +0200 @@ -1,37 +1,36 @@ %% $Id$ \chapter{Higher-Order Logic} \index{higher-order logic|(} -\index{CHOL system@{\sc chol} system} +\index{HOL system@{\sc chol} 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 higher-order logic. Experience with the {\sc hol} system +has demonstrated that higher-order logic is useful for hardware verification; +beyond this, it is widely applicable in many areas of mathematics. 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 theory~\thydx{CHOL} implements higher-order logic with curried -function application. 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 higher-order logic. Experience with the {\sc hol} -system has demonstrated that higher-order logic is useful for hardware -verification; beyond this, it is widely applicable in many areas of -mathematics. 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 \CHOL\ to~{\ZF}. +The syntax of Isabelle's \HOL\ has recently been changed to look more like the +traditional syntax of higher-order logic. Function application is now +curried. To apply the function~$f$ to the arguments~$a$ and~$b$ in \HOL, you +must write $f\,a\,b$. 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} and earlier versions of \HOL. Early 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. -\CHOL\ is a modified version of Isabelle's \HOL\ and uses curried function -application. Therefore the expression $f(a,b)$ (which in \HOL\ means -``f applied to the two arguments $a$ and $b$'') means ``f applied to -the pair $(a,b)$'' in \CHOL. N.B. that ordered pairs in \HOL\ are written as -$$ while in \CHOL\ the syntax $(a,b)$ is used. Previous -releases of Isabelle also included a different 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. - -\CHOL\ has a distinct feel, compared with {\ZF} and {\CTT}. It +\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. There is no `apply' operator: function applications are written as simply~$f~a$ rather than $f{\tt`}a$. -These identifications allow Isabelle to support \CHOL\ particularly nicely, -but they also mean that \CHOL\ requires more sophistication from the user +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 {\tt show_types} set to {\tt true}. Gain experience by working in first-order logic before attempting to use higher-order logic. @@ -122,7 +121,7 @@ & | & "EX!~" id~id^* " . " formula \end{array} \] -\caption{Full grammar for \CHOL} \label{chol-grammar} +\caption{Full grammar for \HOL} \label{chol-grammar} \end{figure} @@ -147,7 +146,7 @@ $\neg(a=b)$. \begin{warn} - \CHOL\ has no if-and-only-if connective; logical equivalence is expressed + \HOL\ has no if-and-only-if connective; logical equivalence is expressed using equality. But equality has a high priority, as befitting a relation, while if-and-only-if typically has the lowest priority. Thus, $\neg\neg P=P$ abbreviates $\neg\neg (P=P)$ and not $(\neg\neg P)=P$. @@ -155,14 +154,14 @@ parentheses. \end{warn} -\subsection{Types}\label{CHOL-types} +\subsection{Types}\label{HOL-types} The type of formulae, \tydx{bool}, belongs to class \cldx{term}; thus, formulae are terms. The built-in type~\tydx{fun}, which constructs function types, is overloaded with arity {\tt(term,term)term}. Thus, $\sigma\To\tau$ belongs to class~{\tt term} if $\sigma$ and~$\tau$ do, allowing quantification over functions. -Types in \CHOL\ must be non-empty; otherwise the quantifier rules would be +Types in \HOL\ must be non-empty; otherwise the quantifier rules would be unsound. I have commented on this elsewhere~\cite[\S7]{paulson-COLOG}. \index{type definitions} @@ -185,7 +184,7 @@ \subsection{Binders} Hilbert's {\bf description} operator~$\epsilon x.P[x]$ stands for some~$a$ -satisfying~$P[a]$, if such exists. Since all terms in \CHOL\ denote +satisfying~$P[a]$, if such exists. Since all terms in \HOL\ denote something, a description is always meaningful, but we do not know its value unless $P[x]$ defines it uniquely. We may write descriptions as \cdx{Eps}($P$) or use the syntax @@ -199,8 +198,8 @@ $\exists!x. \exists!y.P~x~y$; note that this does not mean that there exists a unique pair $(x,y)$ satisfying~$P~x~y$. -\index{*"! symbol}\index{*"? symbol}\index{CHOL system@{\sc hol} system} -Quantifiers have two notations. As in Gordon's {\sc hol} system, \CHOL\ +\index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system} +Quantifiers have two notations. As in Gordon's {\sc hol} system, \HOL\ uses~{\tt!}\ and~{\tt?}\ to stand for $\forall$ and $\exists$. The existential quantifier must be followed by a space; thus {\tt?x} is an unknown, while \verb'? x.f x=y' is a quantification. Isabelle's usual @@ -219,7 +218,7 @@ the constant~\cdx{Let}. It can be expanded by rewriting with its definition, \tdx{Let_def}. -\CHOL\ also defines the basic syntax +\HOL\ also defines the basic syntax \[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n\] as a uniform means of expressing {\tt case} constructs. Therefore {\tt case} and \sdx{of} are reserved words. However, so far this is mere @@ -240,7 +239,7 @@ \tdx{selectI} P(x::'a) ==> P(@x.P x) \tdx{True_or_False} (P=True) | (P=False) \end{ttbox} -\caption{The {\tt CHOL} rules} \label{chol-rules} +\caption{The {\tt HOL} rules} \label{chol-rules} \end{figure} @@ -260,12 +259,12 @@ \tdx{if_def} If P x y == (\%P x y.@z::'a.(P=True --> z=x) & (P=False --> z=y)) \tdx{Let_def} Let s f == f s \end{ttbox} -\caption{The {\tt CHOL} definitions} \label{chol-defs} +\caption{The {\tt HOL} definitions} \label{chol-defs} \end{figure} \section{Rules of inference} -Figure~\ref{chol-rules} shows the inference rules of~\CHOL{}, with +Figure~\ref{chol-rules} shows the inference rules of~\HOL{}, with their~{\ML} names. Some of the rules deserve additional comments: \begin{ttdescription} \item[\tdx{ext}] expresses extensionality of functions. @@ -279,13 +278,13 @@ shown by Diaconescu; see Paulson~\cite{paulson-COLOG} for details.} \end{ttdescription} -\CHOL{} follows standard practice in higher-order logic: only a few +\HOL{} follows standard practice in higher-order logic: only a few connectives are taken as primitive, with the remainder defined obscurely (Fig.\ts\ref{chol-defs}). Gordon's {\sc hol} system expresses the corresponding definitions \cite[page~270]{mgordon-hol} using object-equality~({\tt=}), which is possible because equality in higher-order logic may equate formulae and even functions over formulae. -But theory~\CHOL{}, like all other Isabelle theories, uses +But theory~\HOL{}, like all other Isabelle theories, uses meta-equality~({\tt==}) for definitions. Some of the rules mention type variables; for example, {\tt refl} @@ -350,7 +349,7 @@ \subcaption{Logical equivalence} \end{ttbox} -\caption{Derived rules for \CHOL} \label{chol-lemmas1} +\caption{Derived rules for \HOL} \label{chol-lemmas1} \end{figure} @@ -540,17 +539,17 @@ Although sets may contain other sets as elements, the containing set must have a more complex type. \end{itemize} -Finite unions and intersections have the same behaviour in \CHOL\ as they -do in~{\ZF}. In \CHOL\ the intersection of the empty set is well-defined, +Finite unions and intersections have the same behaviour in \HOL\ as they +do in~{\ZF}. In \HOL\ the intersection of the empty set is well-defined, denoting the universal set for the given type. \subsection{Syntax of set theory}\index{*set type} -\CHOL's set theory is called \thydx{Set}. The type $\alpha\,set$ is +\HOL's set theory is called \thydx{Set}. The type $\alpha\,set$ is essentially the same as $\alpha\To bool$. The new type is defined for clarity and to avoid complications involving function types in unification. Since Isabelle does not support type definitions (as mentioned in -\S\ref{CHOL-types}), the isomorphisms between the two types are declared +\S\ref{HOL-types}), the isomorphisms between the two types are declared explicitly. Here they are natural: {\tt Collect} maps $\alpha\To bool$ to $\alpha\,set$, while \hbox{\tt op :} maps in the other direction (ignoring argument order). @@ -823,27 +822,27 @@ \tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are not strictly necessary but yield more natural proofs. Similarly, \tdx{equalityCE} supports classical reasoning about extensionality, -after the fashion of \tdx{iffCE}. See the file {\tt CHOL/Set.ML} for +after the fashion of \tdx{iffCE}. See the file {\tt HOL/Set.ML} for proofs pertaining to set theory. Figure~\ref{chol-fun} presents derived inference rules involving functions. They also include rules for \cdx{Inv}, which is defined in theory~{\tt - CHOL}; note that ${\tt Inv}~f$ applies the Axiom of Choice to yield an + HOL}; note that ${\tt Inv}~f$ applies the Axiom of Choice to yield an inverse of~$f$. They also include natural deduction rules for the image and range operators, and for the predicates {\tt inj} and {\tt inj_onto}. Reasoning about function composition (the operator~\sdx{o}) and the predicate~\cdx{surj} is done simply by expanding the definitions. See -the file {\tt CHOL/fun.ML} for a complete listing of the derived rules. +the file {\tt HOL/fun.ML} for a complete listing of the derived rules. Figure~\ref{chol-subset} presents lattice properties of the subset relation. Unions form least upper bounds; non-empty intersections form greatest lower bounds. Reasoning directly about subsets often yields clearer proofs than -reasoning about the membership relation. See the file {\tt CHOL/subset.ML}. +reasoning about the membership relation. See the file {\tt HOL/subset.ML}. Figure~\ref{chol-equalities} presents many common set equalities. They include commutative, associative and distributive laws involving unions, intersections and complements. The proofs are mostly trivial, using the -classical reasoner; see file {\tt CHOL/equalities.ML}. +classical reasoner; see file {\tt HOL/equalities.ML}. \begin{figure} @@ -911,23 +910,23 @@ \section{Generic packages and classical reasoning} -\CHOL\ instantiates most of Isabelle's generic packages; -see {\tt CHOL/ROOT.ML} for details. +\HOL\ instantiates most of Isabelle's generic packages; +see {\tt HOL/ROOT.ML} for details. \begin{itemize} \item -Because it includes a general substitution rule, \CHOL\ instantiates the +Because it includes a general substitution rule, \HOL\ instantiates the tactic {\tt hyp_subst_tac}, which substitutes for an equality throughout a subgoal and its hypotheses. \item It instantiates the simplifier, defining~\ttindexbold{HOL_ss} as the simplification set for higher-order logic. Equality~($=$), which also expresses logical equivalence, may be used for rewriting. See the file -{\tt CHOL/simpdata.ML} for a complete listing of the simplification +{\tt HOL/simpdata.ML} for a complete listing of the simplification rules. \item It instantiates the classical reasoner, as described below. \end{itemize} -\CHOL\ derives classical introduction rules for $\disj$ and~$\exists$, as +\HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule; recall Fig.\ts\ref{chol-lemmas2} above. @@ -1087,7 +1086,7 @@ Isabelle provides no means of verifying that such overloading is sensible; there is no means of specifying the operators' properties and verifying that instances of the operators satisfy those properties. To be safe, the -\CHOL\ theory includes no polymorphic axioms asserting general properties of +\HOL\ theory includes no polymorphic axioms asserting general properties of $<$ and~$\leq$. Theory \thydx{Arith} develops arithmetic on the natural numbers. It @@ -1161,22 +1160,22 @@ \begin{figure} \begin{ttbox}\makeatother \tdx{list_rec_Nil} list_rec [] c h = c -\tdx{list_rec_Cons} list_rec a#l c h = h a l (list_rec l c h) +\tdx{list_rec_Cons} list_rec (a#l) c h = h a l (list_rec l c h) \tdx{list_case_Nil} list_case c h [] = c -\tdx{list_case_Cons} list_case c h x#xs = h x xs +\tdx{list_case_Cons} list_case c h (x#xs) = h x xs \tdx{map_Nil} map f [] = [] -\tdx{map_Cons} map f x \# xs = f x \# map f xs +\tdx{map_Cons} map f (x#xs) = f x # map f xs \tdx{null_Nil} null [] = True -\tdx{null_Cons} null x#xs = False +\tdx{null_Cons} null (x#xs) = False -\tdx{hd_Cons} hd x#xs = x -\tdx{tl_Cons} tl x#xs = xs +\tdx{hd_Cons} hd (x#xs) = x +\tdx{tl_Cons} tl (x#xs) = xs \tdx{ttl_Nil} ttl [] = [] -\tdx{ttl_Cons} ttl x#xs = xs +\tdx{ttl_Cons} ttl (x#xs) = xs \tdx{append_Nil} [] @ ys = ys \tdx{append_Cons} (x#xs) \at ys = x # xs \at ys @@ -1185,10 +1184,10 @@ \tdx{mem_Cons} x mem (y#ys) = if y=x then True else x mem ys \tdx{filter_Nil} filter P [] = [] -\tdx{filter_Cons} filter P x#xs = if P x then x#filter P xs else filter P xs +\tdx{filter_Cons} filter P (x#xs) = if P x then x#filter P xs else filter P xs \tdx{list_all_Nil} list_all P [] = True -\tdx{list_all_Cons} list_all P x#xs = (P x & list_all P xs) +\tdx{list_all_Cons} list_all P (x#xs) = (P x & list_all P xs) \end{ttbox} \caption{Rewrite rules for lists} \label{chol-list-simps} \end{figure} @@ -1197,7 +1196,7 @@ \subsection{The type constructor for lists, {\tt list}} \index{*list type} -\CHOL's definition of lists is an example of an experimental method for +\HOL's definition of lists is an example of an experimental method for handling recursive data types. Figure~\ref{chol-list} presents the theory \thydx{List}: the basic list operations with their types and properties. @@ -1374,10 +1373,10 @@ \subsubsection{The datatype $\alpha~list$} We want to define the type $\alpha~list$.\footnote{Of course there is a list - type in CHOL already. This is only an example.} To do this we have to build -a new theory that contains the type definition. We start from {\tt CHOL}. + type in HOL already. This is only an example.} To do this we have to build +a new theory that contains the type definition. We start from {\tt HOL}. \begin{ttbox} -MyList = CHOL + +MyList = HOL + datatype 'a list = Nil | Cons 'a ('a list) end \end{ttbox} @@ -1431,7 +1430,7 @@ \verb|#| instead of {\tt Cons}. To do this we simply add mixfix annotations after the constructor declarations as follows: \begin{ttbox} -MyList = CHOL + +MyList = HOL + datatype 'a list = "[]" ("[]") | "#" 'a ('a list) (infixr 70) end @@ -1473,7 +1472,7 @@ consts app :: "['a list,'a list] => 'a list" rules app_Nil "app [] ys = ys" - app_Cons "app x#xs ys = x#app xs ys" + app_Cons "app (x#xs) ys = x#app xs ys" end \end{ttbox} this carries with it the danger of accidentally asserting an inconsistency, @@ -1484,7 +1483,7 @@ consts app :: "'['a list,'a list] => 'a list" primrec app MyList.list app_Nil "app [] ys = ys" - app_Cons "app x#xs ys = x#app xs ys" + app_Cons "app (x#xs) ys = x#app xs ys" end \end{ttbox} The system will now check that the two rules \verb$app_Nil$ and @@ -1590,7 +1589,7 @@ This package is derived from the ZF one, described in a separate paper,\footnote{It appeared in CADE~\cite{paulson-CADE} and a longer version is distributed with Isabelle.} which you should refer to -in case of difficulties. The package is simpler than ZF's, thanks to CHOL's +in case of difficulties. The package is simpler than ZF's, thanks to HOL's automatic type-checking. The type of the (co)inductive determines the domain of the fixedpoint definition, and the package does not use inference rules for type-checking. @@ -1728,27 +1727,27 @@ monos "[Pow_mono]" end \end{ttbox} -The CHOL distribution contains many other inductive definitions, such as the -theory {\tt CHOL/ex/PropLog.thy} and the directory {\tt CHOL/IMP}. The -theory {\tt CHOL/ex/LList.thy} contains coinductive definitions. +The HOL distribution contains many other inductive definitions, such as the +theory {\tt HOL/ex/PropLog.thy} and the directory {\tt HOL/IMP}. The +theory {\tt HOL/ex/LList.thy} contains coinductive definitions. \index{*coinductive|)} \index{*inductive|)} \underscoreoff \section{The examples directories} -Directory {\tt CHOL/Subst} contains Martin Coen's mechanisation of a theory of +Directory {\tt HOL/Subst} contains Martin Coen's mechanisation of a theory of substitutions and unifiers. It is based on Paulson's previous mechanisation in {\LCF}~\cite{paulson85} of Manna and Waldinger's theory~\cite{mw81}. -Directory {\tt CHOL/IMP} contains a mechanised version of a semantic +Directory {\tt HOL/IMP} contains a mechanised version of a semantic equivalence proof taken from Winskel~\cite{winskel93}. It formalises the denotational and operational semantics of a simple while-language, then proves the two equivalent. It contains several datatype and inductive definitions, and demonstrates their use. -Directory {\tt CHOL/ex} contains other examples and experimental proofs in -{\CHOL}. Here is an overview of the more interesting files. +Directory {\tt HOL/ex} contains other examples and experimental proofs in +{\HOL}. Here is an overview of the more interesting files. \begin{itemize} \item File {\tt cla.ML} demonstrates the classical reasoner on over sixty predicate calculus theorems, ranging from simple tautologies to @@ -1811,7 +1810,7 @@ of~$\alpha$. This version states that for every function from $\alpha$ to its powerset, some subset is outside its range. -The Isabelle proof uses \CHOL's set theory, with the type $\alpha\,set$ and +The Isabelle proof uses \HOL's set theory, with the type $\alpha\,set$ and the operator \cdx{range}. The set~$S$ is given as an unknown instead of a quantified variable so that we may inspect the subset found by the proof. \begin{ttbox} @@ -1878,7 +1877,7 @@ \end{ttbox} How much creativity is required? As it happens, Isabelle can prove this theorem automatically. The classical set \ttindex{set_cs} contains rules -for most of the constructs of \CHOL's set theory. We must augment it with +for most of the constructs of \HOL's set theory. We must augment it with \tdx{equalityCE} to break up set equalities, and then apply best-first search. Depth-first search would diverge, but best-first search successfully navigates through the large search space.