# HG changeset patch # User wenzelm # Date 934921455 -7200 # Node ID 65ccac4e1f3f5f0b1992b98ba8ccdd24f441a940 # Parent ad714526c23e00be700a6d072f3bce2453cc86d0 eliminated HOL_quantifiers (replaced by "HOL" print mode); diff -r ad714526c23e -r 65ccac4e1f3f doc-src/HOL/HOL.tex --- a/doc-src/HOL/HOL.tex Tue Aug 17 22:22:36 1999 +0200 +++ b/doc-src/HOL/HOL.tex Tue Aug 17 22:24:15 1999 +0200 @@ -59,13 +59,13 @@ \index{*"! symbol}\index{*"? symbol} \index{*"?"! symbol}\index{*"E"X"! symbol} \it symbol &\it name &\it meta-type & \it description \\ - \tt\at & \cdx{Eps} & $(\alpha\To bool)\To\alpha$ & + \sdx{SOME} or \tt\at & \cdx{Eps} & $(\alpha\To bool)\To\alpha$ & Hilbert description ($\varepsilon$) \\ - {\tt!~} or \sdx{ALL} & \cdx{All} & $(\alpha\To bool)\To bool$ & + \sdx{ALL} or {\tt!~} & \cdx{All} & $(\alpha\To bool)\To bool$ & universal quantifier ($\forall$) \\ - {\tt?~} or \sdx{EX} & \cdx{Ex} & $(\alpha\To bool)\To bool$ & + \sdx{EX} or {\tt?~} & \cdx{Ex} & $(\alpha\To bool)\To bool$ & existential quantifier ($\exists$) \\ - {\tt?!} or \texttt{EX!} & \cdx{Ex1} & $(\alpha\To bool)\To bool$ & + \texttt{EX!} or {\tt?!} & \cdx{Ex1} & $(\alpha\To bool)\To bool$ & unique existence ($\exists!$)\\ \texttt{LEAST} & \cdx{Least} & $(\alpha::ord \To bool)\To\alpha$ & least element @@ -99,6 +99,7 @@ \dquotes \[\begin{array}{rclcl} term & = & \hbox{expression of class~$term$} \\ + & | & "SOME~" id " . " formula & | & "\at~" id " . " formula \\ & | & \multicolumn{3}{l}{"let"~id~"="~term";"\dots";"~id~"="~term~"in"~term} \\ @@ -114,12 +115,12 @@ & | & formula " \& " formula \\ & | & formula " | " formula \\ & | & formula " --> " formula \\ - & | & "!~~~" id~id^* " . " formula - & | & "ALL~" id~id^* " . " formula \\ - & | & "?~~~" id~id^* " . " formula - & | & "EX~~" id~id^* " . " formula \\ - & | & "?!~~" id~id^* " . " formula + & | & "ALL~" id~id^* " . " formula + & | & "!~~~" id~id^* " . " formula \\ + & | & "EX~~" id~id^* " . " formula + & | & "?~~~" id~id^* " . " formula \\ & | & "EX!~" id~id^* " . " formula + & | & "?!~~" id~id^* " . " formula \\ \end{array} \] \caption{Full grammar for \HOL} \label{hol-grammar} @@ -203,7 +204,7 @@ denote something, a description is always meaningful, but we do not know its value unless $P$ defines it uniquely. We may write descriptions as \cdx{Eps}($\lambda x. P[x]$) or use the syntax -\hbox{\tt \at $x$.\ $P[x]$}. +\hbox{\tt SOME~$x$.~$P[x]$}. Existential quantification is defined by \[ \exists x. P~x \;\equiv\; P(\varepsilon x. P~x). \] @@ -213,16 +214,20 @@ $\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\ -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 -notation for quantifiers, \sdx{ALL} and \sdx{EX}, is also -available. Both notations are accepted for input. The {\ML} reference -\ttindexbold{HOL_quantifiers} governs the output notation. If set to {\tt -true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default. If set -to \texttt{false}, then~\texttt{ALL} and~\texttt{EX} are displayed. +\medskip + +\index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system} The +basic Isabelle/HOL binders have two notations. Apart from the usual +\texttt{ALL} and \texttt{EX} for $\forall$ and $\exists$, Isabelle/HOL also +supports the original notation of Gordon's {\sc hol} system: \texttt{!}\ +and~\texttt{?}. In the latter case, the existential quantifier \emph{must} be +followed by a space; thus {\tt?x} is an unknown, while \verb'? x. f x=y' is a +quantification. Both notations are accepted for input. The print mode +``\ttindexbold{HOL}'' governs the output notation. If enabled (e.g.\ by +passing option \texttt{-m HOL} to the \texttt{isabelle} executable), +then~{\tt!}\ and~{\tt?}\ are displayed. + +\medskip If $\tau$ is a type of class \cldx{ord}, $P$ a formula and $x$ a variable of type $\tau$, then the term \cdx{LEAST}~$x. P[x]$ is defined @@ -517,10 +522,10 @@ \rm intersection \\ \sdx{UN}{\tt\ } $x$:$A$. $B[x]$ & UNION $A$ $\lambda x. B[x]$ & \rm union \\ - \tt ! $x$:$A$. $P[x]$ or \sdx{ALL} $x$:$A$. $P[x]$ & + \sdx{ALL} $x$:$A$. $P[x]$ or \sdx{!} $x$:$A$. $P[x]$ & Ball $A$ $\lambda x. P[x]$ & \rm bounded $\forall$ \\ - \sdx{?} $x$:$A$. $P[x]$ or \sdx{EX}{\tt\ } $x$:$A$. $P[x]$ & + \sdx{EX}{\tt\ } $x$:$A$. $P[x]$ or \sdx{?} $x$:$A$. $P[x]$ & Bex $A$ $\lambda x. P[x]$ & \rm bounded $\exists$ \end{tabular} \end{center} @@ -543,10 +548,10 @@ & | & term " : " term \\ & | & term " \ttilde: " term \\ & | & term " <= " term \\ - & | & "!~" id ":" term " . " formula - & | & "ALL " id ":" term " . " formula \\ - & | & "?~" id ":" term " . " formula + & | & "ALL " id ":" term " . " formula + & | & "!~" id ":" term " . " formula \\ & | & "EX~~" id ":" term " . " formula + & | & "?~" id ":" term " . " formula \\ \end{array} \] \subcaption{Full Grammar} @@ -612,10 +617,9 @@ write\index{*"! symbol}\index{*"? symbol} \index{*ALL symbol}\index{*EX symbol} % -\hbox{\tt !~$x$:$A$.\ $P[x]$} and \hbox{\tt ?~$x$:$A$.\ $P[x]$}. Isabelle's -usual quantifier symbols, \sdx{ALL} and \sdx{EX}, are also accepted -for input. As with the primitive quantifiers, the {\ML} reference -\ttindex{HOL_quantifiers} specifies which notation to use for output. +\hbox{\tt ALL~$x$:$A$.\ $P[x]$} and \hbox{\tt EX~$x$:$A$.\ $P[x]$}. The +original notation of Gordon's {\sc hol} system is supported as well: \sdx{!}\ +and \sdx{?}. Unions and intersections over sets, namely $\bigcup@{x\in A}B[x]$ and $\bigcap@{x\in A}B[x]$, are written