# HG changeset patch # User wenzelm # Date 863448367 -7200 # Node ID 08e364dfe518dc748718ecc2862c5684f2ac7259 # Parent 22ebe2bd5e455f328cb0c594e4c40b122e153405 minor tuning; diff -r 22ebe2bd5e45 -r 08e364dfe518 doc-src/Logics/HOL.tex --- a/doc-src/Logics/HOL.tex Mon May 12 16:44:58 1997 +0200 +++ b/doc-src/Logics/HOL.tex Mon May 12 16:46:07 1997 +0200 @@ -197,7 +197,8 @@ \subsection{Binders} -Hilbert's {\bf description} operator~$\varepsilon x.P\,x$ stands for + +Hilbert's {\bf description} operator~$\varepsilon x.P[x]$ stands for some~$x$ satisfying~$P$, if such exists. Since all terms in \HOL\ denote something, a description is always meaningful, but we do not know its value unless $P$ defines it uniquely. We may write @@ -209,8 +210,8 @@ The unique existence quantifier, $\exists!x.P$, is defined in terms of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested quantifications. For instance, $\exists!x\,y.P\,x\,y$ abbreviates -$\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$. +$\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{HOL system@{\sc hol} system} Quantifiers have two notations. As in Gordon's {\sc hol} system, \HOL\ @@ -227,11 +228,10 @@ variable of type $\tau$, then the term \cdx{LEAST}~$x.P[x]$ is defined to be the least (w.r.t.\ $\le$) $x$ such that $P~x$ holds (see Fig.~\ref{hol-defs}). The definition uses Hilbert's $\varepsilon$ -choice operator. So this is always meaningful, but may yield nothing -useful in case there is not a unique least element satisfying -$P$.\footnote{Note that class $ord$ does not require much of its - instances, so $\le$ need not be a well-ordering, not even an order - at all!} +choice operator, so \texttt{Least} is always meaningful, but may yield +nothing useful in case there is not a unique least element satisfying +$P$.\footnote{Class $ord$ does not require much of its instances, so + $\le$ need not be a well-ordering, not even an order at all!} \medskip All these binders have priority 10. @@ -281,8 +281,9 @@ \caption{The {\tt HOL} rules} \label{hol-rules} \end{figure} -Figure~\ref{hol-rules} shows the inference rules of~\HOL{}, with their~{\ML} -names. Some of the rules deserve additional comments: +Figure~\ref{hol-rules} shows the primitive inference rules of~\HOL{}, +with their~{\ML} names. Some of the rules deserve additional +comments: \begin{ttdescription} \item[\tdx{ext}] expresses extensionality of functions. \item[\tdx{iff}] asserts that logically equivalent formulae are @@ -449,7 +450,7 @@ & insertion of element \\ \cdx{Collect} & $(\alpha\To bool)\To\alpha\,set$ & comprehension \\ - \cdx{Compl} & $(\alpha\,set)\To\alpha\,set$ + \cdx{Compl} & $\alpha\,set\To\alpha\,set$ & complement \\ \cdx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$ & intersection over a set\\ @@ -1177,7 +1178,7 @@ \subsection{The type of natural numbers, {\tt nat}} The theory \thydx{NatDef} defines the natural numbers in a roundabout -but traditional way. The axiom of infinity postulates an +but traditional way. The axiom of infinity postulates a type~\tydx{ind} of individuals, which is non-empty and closed under an injective operation. The natural numbers are inductively generated by choosing an arbitrary individual for~0 and using the injective @@ -1402,13 +1403,14 @@ Types in \HOL\ must be non-empty; otherwise the quantifier rules would be unsound, because $\exists x. x=x$ is a theorem \cite[\S7]{paulson-COLOG}. \end{warn} -A \bfindex{type definition} identifies the new type with a subset of an -existing type. More precisely, the new type is defined by exhibiting an -existing type~$\tau$, a set~$A::(\tau)set$, and a theorem of the form $x:A$. -Thus~$A$ is a non-empty subset of~$\tau$, and the new type denotes this -subset. New functions are defined that establish an isomorphism between the -new type and the subset. If type~$\tau$ involves type variables $\alpha@1$, -\ldots, $\alpha@n$, then the type definition creates a type constructor +A \bfindex{type definition} identifies the new type with a subset of +an existing type. More precisely, the new type is defined by +exhibiting an existing type~$\tau$, a set~$A::\tau\,set$, and a +theorem of the form $x:A$. Thus~$A$ is a non-empty subset of~$\tau$, +and the new type denotes this subset. New functions are defined that +establish an isomorphism between the new type and the subset. If +type~$\tau$ involves type variables $\alpha@1$, \ldots, $\alpha@n$, +then the type definition creates a type constructor $(\alpha@1,\ldots,\alpha@n)ty$ rather than a particular type. \begin{figure}[htbp] @@ -1442,7 +1444,7 @@ `typevarlist', no extra type variables in `set', and no free term variables in `set'), the following components are added to the theory: \begin{itemize} -\item a type $ty :: (term,\dots)term$; +\item a type $ty :: (term,\dots,term)term$ \item constants \begin{eqnarray*} T &::& \tau\;set \\ @@ -1461,8 +1463,8 @@ stating that $(\alpha@1,\dots,\alpha@n)ty$ is isomorphic to $A$ by $Rep_T$ and its inverse $Abs_T$. \end{itemize} -Below are two simple examples of \HOL\ type definitions. Emptiness is -proved automatically here. +Below are two simple examples of \HOL\ type definitions. Non-emptiness +is proved automatically here. \begin{ttbox} typedef unit = "{\ttlbrace}True{\ttrbrace}" @@ -1498,12 +1500,13 @@ \label{sec:HOL:datatype} \index{*datatype|(} -Inductive datatypes similar to those of \ML{} frequently appear in +Inductive datatypes, similar to those of \ML, frequently appear in non-trivial applications of \HOL. In principle, such types could be defined by hand via \texttt{typedef} (see \S\ref{sec:typedef}), but this would be far too tedious. The \ttindex{datatype} definition -package of \HOL\ automates such chores. It generates freeness and -induction rules from a very simple description provided by the user. +package of \HOL\ automates such chores. It generates freeness theorems +and induction rules from a very simple description of the new type +provided by the user. \subsection{Basics} @@ -1527,7 +1530,7 @@ \item the newly defined type $(\alpha@1, \dots, \alpha@n) \, t$. \end{itemize} Recursive occurences of $(\alpha@1, \dots, \alpha@n) \, t$ are quite -restricted. To ensure that the new type is not empty, at least one +restricted. To ensure that the new type is non-empty, at least one constructor must consist of only non-recursive type components. If you would like one of the $\tau@{ij}$ to be a complex type expression $\tau$ you need to declare a new type synonym $syn = \tau$ first and @@ -1538,35 +1541,31 @@ The constructors are automatically defined as functions of their respective type: -\[ C@j : [\tau@{j1},\dots,\tau@{jk@j}] \To (\alpha@1,\dots,\alpha@n)t \] -These functions have certain {\em freeness} properties: -\begin{itemize} - -\item They are distinct: - \[ - C@i~x@1~\dots~x@{k@i} \neq C@j~y@1~\dots~y@{k@j} \qquad - \mbox{for all}~ i \neq j. - \] - -\item They are injective: - \[ - (C@j~x@1~\dots~x@{k@j} = C@j~y@1~\dots~y@{k@j}) = - (x@1 = y@1 \land \dots \land x@{k@j} = y@{k@j}) - \] -\end{itemize} +\[ C@j :: [\tau@{j1},\dots,\tau@{jk@j}] \To (\alpha@1,\dots,\alpha@n)t \] +These functions have certain {\em freeness} properties --- they are +distinct: +\[ +C@i~x@1~\dots~x@{k@i} \neq C@j~y@1~\dots~y@{k@j} \qquad +\mbox{for all}~ i \neq j. +\] +and they are injective: +\[ +(C@j~x@1~\dots~x@{k@j} = C@j~y@1~\dots~y@{k@j}) = +(x@1 = y@1 \land \dots \land x@{k@j} = y@{k@j}) +\] Because the number of inequalities is quadratic in the number of constructors, a different representation is used if there are $7$ or more of them. In that case every constructor term is mapped to a natural number: \[ -t_ord \, (C@i \, x@1 \, \dots \, x@{k@1}) = i - 1 +t_ord \, (C@i \, x@1 \, \dots \, x@{k@i}) = i - 1 \] Then distinctness of constructor terms is expressed by: \[ t_ord \, x \neq t_ord \, y \Imp x \neq y. \] -\medskip Furthermore, the following structural induction rule is +\medskip Generally, the following structural induction rule is provided: \[ \infer{P \, x} @@ -1584,7 +1583,7 @@ = (\alpha@1,\dots,\alpha@n)t \}$, i.e.\ the property $P$ can be assumed for all arguments of the recursive type. -The type also comes with an \ML-like \sdx{case}-construct: +\medskip The type also comes with an \ML-like \sdx{case}-construct: \[ \begin{array}{rrcl} \mbox{\tt case}~e~\mbox{\tt of} & C@1~x@{11}~\dots~x@{1k@1} & \To & e@1 \\ @@ -1663,7 +1662,7 @@ \subsubsection{The datatype $\alpha~list$} We want to define the type $\alpha~list$.\footnote{This is just an - example. There is already a list type in \HOL, of course.} To do + example, there is already a list type in \HOL, of course.} To do this we have to build a new theory that contains the type definition. We start from the basic {\tt HOL} theory. \begin{ttbox} @@ -1671,8 +1670,10 @@ datatype 'a list = Nil | Cons 'a ('a list) end \end{ttbox} -After loading the theory (\verb$use_thy "MyList"$), we can prove -$Cons~x~xs\neq xs$. +After loading the theory (with \verb$use_thy "MyList"$), we can prove +$Cons~x~xs\neq xs$. To ease the induction applied below, we state the +goal with $x$ quantified at the object-level. This will be stripped +later using \ttindex{qed_spec_mp}. \begin{ttbox} goal MyList.thy "!x. Cons x xs ~= xs"; {\out Level 0} @@ -1706,9 +1707,12 @@ {\out Level 3} {\out ! x. Cons x xs ~= xs} {\out No subgoals!} +\ttbreak +qed_spec_mp "not_Cons_self"; +{\out val not_Cons_self = "Cons x xs ~= xs";} \end{ttbox} -Because both subgoals were proved by almost the same tactic we could have -done that in one step using +Because both subgoals could have been proved by \texttt{Asm_simp_tac} +we could have done that in one step: \begin{ttbox} by (ALLGOALS Asm_simp_tac); \end{ttbox} @@ -1736,16 +1740,16 @@ This example shows a datatype that consists of 7 constructors: \begin{ttbox} Days = Arith + - datatype days = Mo | Tu | We | Th | Fr | Sa | So + datatype days = Mon | Tue | Wed | Thu | Fri | Sat | Sun end \end{ttbox} -Because there are more than 6 constructors, the theory must be based on -{\tt Arith}. Inequality is defined via a function \verb|days_ord|. The -theorem \verb|Mo ~= Tu| is not directly contained among the distinctness -theorems, but the simplifier can prove it thanks to rewrite rules inherited -from theory {\tt Arith}. +Because there are more than 6 constructors, the theory must be based +on {\tt Arith}. Inequality is expressed via a function +\verb|days_ord|. The theorem \verb|Mon ~= Tue| is not directly +contained among the distinctness theorems, but the simplifier can +prove it thanks to rewrite rules inherited from theory {\tt Arith}: \begin{ttbox} -goal Days.thy "Mo ~= Tu"; +goal Days.thy "Mon ~= Tue"; by (Simp_tac 1); \end{ttbox} You need not derive such inequalities explicitly: the simplifier will dispose @@ -1763,7 +1767,7 @@ new axioms, e.g.\ \begin{ttbox} Append = MyList + -consts app :: ['a list,'a list] => 'a list +consts app :: ['a list, 'a list] => 'a list rules app_Nil "app [] ys = ys" app_Cons "app (x#xs) ys = x#app xs ys" @@ -1776,7 +1780,7 @@ functions on datatypes --- \ttindex{primrec}: \begin{ttbox} Append = MyList + -consts app :: ['a list,'a list] => 'a list +consts app :: ['a list, 'a list] => 'a list primrec app MyList.list "app [] ys = ys" "app (x#xs) ys = x#app xs ys" @@ -1827,7 +1831,7 @@ The primitive recursive function can have infix or mixfix syntax: \begin{ttbox}\underscoreon Append = MyList + -consts "@" :: ['a list,'a list] => 'a list (infixr 60) +consts "@" :: ['a list, 'a list] => 'a list (infixr 60) primrec "op @" MyList.list "[] @ ys = ys" "(x#xs) @ ys = x#(xs @ ys)"