1.1 --- a/doc-src/HOL/HOL.tex Tue Aug 17 22:22:36 1999 +0200
1.2 +++ b/doc-src/HOL/HOL.tex Tue Aug 17 22:24:15 1999 +0200
1.3 @@ -59,13 +59,13 @@
1.4 \index{*"! symbol}\index{*"? symbol}
1.5 \index{*"?"! symbol}\index{*"E"X"! symbol}
1.6 \it symbol &\it name &\it meta-type & \it description \\
1.7 - \tt\at & \cdx{Eps} & $(\alpha\To bool)\To\alpha$ &
1.8 + \sdx{SOME} or \tt\at & \cdx{Eps} & $(\alpha\To bool)\To\alpha$ &
1.9 Hilbert description ($\varepsilon$) \\
1.10 - {\tt!~} or \sdx{ALL} & \cdx{All} & $(\alpha\To bool)\To bool$ &
1.11 + \sdx{ALL} or {\tt!~} & \cdx{All} & $(\alpha\To bool)\To bool$ &
1.12 universal quantifier ($\forall$) \\
1.13 - {\tt?~} or \sdx{EX} & \cdx{Ex} & $(\alpha\To bool)\To bool$ &
1.14 + \sdx{EX} or {\tt?~} & \cdx{Ex} & $(\alpha\To bool)\To bool$ &
1.15 existential quantifier ($\exists$) \\
1.16 - {\tt?!} or \texttt{EX!} & \cdx{Ex1} & $(\alpha\To bool)\To bool$ &
1.17 + \texttt{EX!} or {\tt?!} & \cdx{Ex1} & $(\alpha\To bool)\To bool$ &
1.18 unique existence ($\exists!$)\\
1.19 \texttt{LEAST} & \cdx{Least} & $(\alpha::ord \To bool)\To\alpha$ &
1.20 least element
1.21 @@ -99,6 +99,7 @@
1.22 \dquotes
1.23 \[\begin{array}{rclcl}
1.24 term & = & \hbox{expression of class~$term$} \\
1.25 + & | & "SOME~" id " . " formula
1.26 & | & "\at~" id " . " formula \\
1.27 & | &
1.28 \multicolumn{3}{l}{"let"~id~"="~term";"\dots";"~id~"="~term~"in"~term} \\
1.29 @@ -114,12 +115,12 @@
1.30 & | & formula " \& " formula \\
1.31 & | & formula " | " formula \\
1.32 & | & formula " --> " formula \\
1.33 - & | & "!~~~" id~id^* " . " formula
1.34 - & | & "ALL~" id~id^* " . " formula \\
1.35 - & | & "?~~~" id~id^* " . " formula
1.36 - & | & "EX~~" id~id^* " . " formula \\
1.37 - & | & "?!~~" id~id^* " . " formula
1.38 + & | & "ALL~" id~id^* " . " formula
1.39 + & | & "!~~~" id~id^* " . " formula \\
1.40 + & | & "EX~~" id~id^* " . " formula
1.41 + & | & "?~~~" id~id^* " . " formula \\
1.42 & | & "EX!~" id~id^* " . " formula
1.43 + & | & "?!~~" id~id^* " . " formula \\
1.44 \end{array}
1.45 \]
1.46 \caption{Full grammar for \HOL} \label{hol-grammar}
1.47 @@ -203,7 +204,7 @@
1.48 denote something, a description is always meaningful, but we do not
1.49 know its value unless $P$ defines it uniquely. We may write
1.50 descriptions as \cdx{Eps}($\lambda x. P[x]$) or use the syntax
1.51 -\hbox{\tt \at $x$.\ $P[x]$}.
1.52 +\hbox{\tt SOME~$x$.~$P[x]$}.
1.53
1.54 Existential quantification is defined by
1.55 \[ \exists x. P~x \;\equiv\; P(\varepsilon x. P~x). \]
1.56 @@ -213,16 +214,20 @@
1.57 $\exists!x. \exists!y. P\,x\,y$; note that this does not mean that there
1.58 exists a unique pair $(x,y)$ satisfying~$P\,x\,y$.
1.59
1.60 -\index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system}
1.61 -Quantifiers have two notations. As in Gordon's {\sc hol} system, \HOL\
1.62 -uses~{\tt!}\ and~{\tt?}\ to stand for $\forall$ and $\exists$. The
1.63 -existential quantifier must be followed by a space; thus {\tt?x} is an
1.64 -unknown, while \verb'? x. f x=y' is a quantification. Isabelle's usual
1.65 -notation for quantifiers, \sdx{ALL} and \sdx{EX}, is also
1.66 -available. Both notations are accepted for input. The {\ML} reference
1.67 -\ttindexbold{HOL_quantifiers} governs the output notation. If set to {\tt
1.68 -true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default. If set
1.69 -to \texttt{false}, then~\texttt{ALL} and~\texttt{EX} are displayed.
1.70 +\medskip
1.71 +
1.72 +\index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system} The
1.73 +basic Isabelle/HOL binders have two notations. Apart from the usual
1.74 +\texttt{ALL} and \texttt{EX} for $\forall$ and $\exists$, Isabelle/HOL also
1.75 +supports the original notation of Gordon's {\sc hol} system: \texttt{!}\
1.76 +and~\texttt{?}. In the latter case, the existential quantifier \emph{must} be
1.77 +followed by a space; thus {\tt?x} is an unknown, while \verb'? x. f x=y' is a
1.78 +quantification. Both notations are accepted for input. The print mode
1.79 +``\ttindexbold{HOL}'' governs the output notation. If enabled (e.g.\ by
1.80 +passing option \texttt{-m HOL} to the \texttt{isabelle} executable),
1.81 +then~{\tt!}\ and~{\tt?}\ are displayed.
1.82 +
1.83 +\medskip
1.84
1.85 If $\tau$ is a type of class \cldx{ord}, $P$ a formula and $x$ a
1.86 variable of type $\tau$, then the term \cdx{LEAST}~$x. P[x]$ is defined
1.87 @@ -517,10 +522,10 @@
1.88 \rm intersection \\
1.89 \sdx{UN}{\tt\ } $x$:$A$. $B[x]$ & UNION $A$ $\lambda x. B[x]$ &
1.90 \rm union \\
1.91 - \tt ! $x$:$A$. $P[x]$ or \sdx{ALL} $x$:$A$. $P[x]$ &
1.92 + \sdx{ALL} $x$:$A$. $P[x]$ or \sdx{!} $x$:$A$. $P[x]$ &
1.93 Ball $A$ $\lambda x. P[x]$ &
1.94 \rm bounded $\forall$ \\
1.95 - \sdx{?} $x$:$A$. $P[x]$ or \sdx{EX}{\tt\ } $x$:$A$. $P[x]$ &
1.96 + \sdx{EX}{\tt\ } $x$:$A$. $P[x]$ or \sdx{?} $x$:$A$. $P[x]$ &
1.97 Bex $A$ $\lambda x. P[x]$ & \rm bounded $\exists$
1.98 \end{tabular}
1.99 \end{center}
1.100 @@ -543,10 +548,10 @@
1.101 & | & term " : " term \\
1.102 & | & term " \ttilde: " term \\
1.103 & | & term " <= " term \\
1.104 - & | & "!~" id ":" term " . " formula
1.105 - & | & "ALL " id ":" term " . " formula \\
1.106 - & | & "?~" id ":" term " . " formula
1.107 + & | & "ALL " id ":" term " . " formula
1.108 + & | & "!~" id ":" term " . " formula \\
1.109 & | & "EX~~" id ":" term " . " formula
1.110 + & | & "?~" id ":" term " . " formula \\
1.111 \end{array}
1.112 \]
1.113 \subcaption{Full Grammar}
1.114 @@ -612,10 +617,9 @@
1.115 write\index{*"! symbol}\index{*"? symbol}
1.116 \index{*ALL symbol}\index{*EX symbol}
1.117 %
1.118 -\hbox{\tt !~$x$:$A$.\ $P[x]$} and \hbox{\tt ?~$x$:$A$.\ $P[x]$}. Isabelle's
1.119 -usual quantifier symbols, \sdx{ALL} and \sdx{EX}, are also accepted
1.120 -for input. As with the primitive quantifiers, the {\ML} reference
1.121 -\ttindex{HOL_quantifiers} specifies which notation to use for output.
1.122 +\hbox{\tt ALL~$x$:$A$.\ $P[x]$} and \hbox{\tt EX~$x$:$A$.\ $P[x]$}. The
1.123 +original notation of Gordon's {\sc hol} system is supported as well: \sdx{!}\
1.124 +and \sdx{?}.
1.125
1.126 Unions and intersections over sets, namely $\bigcup@{x\in A}B[x]$ and
1.127 $\bigcap@{x\in A}B[x]$, are written