1.1 --- a/doc-src/Logics/Old_HOL.tex Fri Apr 15 12:54:22 1994 +0200
1.2 +++ b/doc-src/Logics/Old_HOL.tex Fri Apr 15 13:02:22 1994 +0200
1.3 @@ -1,96 +1,86 @@
1.4 %% $Id$
1.5 -\chapter{Higher-Order logic}
1.6 -The directory~\ttindexbold{HOL} contains a theory for higher-order logic.
1.7 +\chapter{Higher-Order Logic}
1.8 +\index{higher-order logic|(}
1.9 +\index{HOL system@{\sc hol} system}
1.10 +
1.11 +The theory~\thydx{HOL} implements higher-order logic.
1.12 It is based on Gordon's~{\sc hol} system~\cite{mgordon88a}, which itself is
1.13 -based on Church~\cite{church40}. Andrews~\cite{andrews86} is a full
1.14 -description of higher-order logic. Gordon's work has demonstrated that
1.15 -higher-order logic is useful for hardware verification; beyond this, it is
1.16 -widely applicable in many areas of mathematics. It is weaker than {\ZF}
1.17 -set theory but for most applications this does not matter. If you prefer
1.18 -{\ML} to Lisp, you will probably prefer \HOL\ to~{\ZF}.
1.19 +based on Church's original paper~\cite{church40}. Andrews's
1.20 +book~\cite{andrews86} is a full description of higher-order logic.
1.21 +Experience with the {\sc hol} system has demonstrated that higher-order
1.22 +logic is useful for hardware verification; beyond this, it is widely
1.23 +applicable in many areas of mathematics. It is weaker than {\ZF} set
1.24 +theory but for most applications this does not matter. If you prefer {\ML}
1.25 +to Lisp, you will probably prefer \HOL\ to~{\ZF}.
1.26
1.27 -Previous releases of Isabelle included a completely different version
1.28 -of~\HOL, with explicit type inference rules~\cite{paulson-COLOG}. This
1.29 -version no longer exists, but \ttindex{ZF} supports a similar style of
1.30 -reasoning.
1.31 +Previous releases of Isabelle included a different version of~\HOL, with
1.32 +explicit type inference rules~\cite{paulson-COLOG}. This version no longer
1.33 +exists, but \thydx{ZF} supports a similar style of reasoning.
1.34
1.35 \HOL\ has a distinct feel, compared with {\ZF} and {\CTT}. It
1.36 identifies object-level types with meta-level types, taking advantage of
1.37 Isabelle's built-in type checker. It identifies object-level functions
1.38 with meta-level functions, so it uses Isabelle's operations for abstraction
1.39 -and application. There is no ``apply'' operator: function applications are
1.40 +and application. There is no `apply' operator: function applications are
1.41 written as simply~$f(a)$ rather than $f{\tt`}a$.
1.42
1.43 These identifications allow Isabelle to support \HOL\ particularly nicely,
1.44 but they also mean that \HOL\ requires more sophistication from the user
1.45 --- in particular, an understanding of Isabelle's type system. Beginners
1.46 -should gain experience by working in first-order logic, before attempting
1.47 -to use higher-order logic. This chapter assumes familiarity with~{\FOL{}}.
1.48 +should work with {\tt show_types} set to {\tt true}. Gain experience by
1.49 +working in first-order logic before attempting to use higher-order logic.
1.50 +This chapter assumes familiarity with~{\FOL{}}.
1.51
1.52
1.53 \begin{figure}
1.54 \begin{center}
1.55 \begin{tabular}{rrr}
1.56 \it name &\it meta-type & \it description \\
1.57 - \idx{Trueprop}& $bool\To prop$ & coercion to $prop$\\
1.58 - \idx{not} & $bool\To bool$ & negation ($\neg$) \\
1.59 - \idx{True} & $bool$ & tautology ($\top$) \\
1.60 - \idx{False} & $bool$ & absurdity ($\bot$) \\
1.61 - \idx{if} & $[bool,\alpha,\alpha]\To\alpha::term$ & conditional \\
1.62 - \idx{Inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & function inversion\\
1.63 - \idx{Let} & $[\alpha,\alpha\To\beta]\To\beta$ & let binder
1.64 + \cdx{Trueprop}& $bool\To prop$ & coercion to $prop$\\
1.65 + \cdx{not} & $bool\To bool$ & negation ($\neg$) \\
1.66 + \cdx{True} & $bool$ & tautology ($\top$) \\
1.67 + \cdx{False} & $bool$ & absurdity ($\bot$) \\
1.68 + \cdx{if} & $[bool,\alpha,\alpha]\To\alpha::term$ & conditional \\
1.69 + \cdx{Inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & function inversion\\
1.70 + \cdx{Let} & $[\alpha,\alpha\To\beta]\To\beta$ & let binder
1.71 \end{tabular}
1.72 \end{center}
1.73 \subcaption{Constants}
1.74
1.75 \begin{center}
1.76 -\index{"@@{\tt\at}|bold}
1.77 -\index{*"!|bold}
1.78 -\index{*"?"!|bold}
1.79 +\index{"@@{\tt\at} symbol}
1.80 +\index{*"! symbol}\index{*"? symbol}
1.81 +\index{*"?"! symbol}\index{*"E"X"! symbol}
1.82 \begin{tabular}{llrrr}
1.83 - \it symbol &\it name &\it meta-type & \it prec & \it description \\
1.84 - \tt\at & \idx{Eps} & $(\alpha\To bool)\To\alpha::term$ & 10 &
1.85 + \it symbol &\it name &\it meta-type & \it description \\
1.86 + \tt\at & \cdx{Eps} & $(\alpha\To bool)\To\alpha::term$ &
1.87 Hilbert description ($\epsilon$) \\
1.88 - \tt! & \idx{All} & $(\alpha::term\To bool)\To bool$ & 10 &
1.89 + {\tt!~} or \sdx{ALL} & \cdx{All} & $(\alpha::term\To bool)\To bool$ &
1.90 universal quantifier ($\forall$) \\
1.91 - \idx{?} & \idx{Ex} & $(\alpha::term\To bool)\To bool$ & 10 &
1.92 + {\tt?~} or \sdx{EX} & \cdx{Ex} & $(\alpha::term\To bool)\To bool$ &
1.93 existential quantifier ($\exists$) \\
1.94 - \tt?! & \idx{Ex1} & $(\alpha::term\To bool)\To bool$ & 10 &
1.95 + {\tt?!} or {\tt EX!} & \cdx{Ex1} & $(\alpha::term\To bool)\To bool$ &
1.96 unique existence ($\exists!$)
1.97 \end{tabular}
1.98 \end{center}
1.99 \subcaption{Binders}
1.100
1.101 \begin{center}
1.102 -\index{*"E"X"!|bold}
1.103 -\begin{tabular}{llrrr}
1.104 - \it symbol &\it name &\it meta-type & \it prec & \it description \\
1.105 - \idx{ALL} & \idx{All} & $(\alpha::term\To bool)\To bool$ & 10 &
1.106 - universal quantifier ($\forall$) \\
1.107 - \idx{EX} & \idx{Ex} & $(\alpha::term\To bool)\To bool$ & 10 &
1.108 - existential quantifier ($\exists$) \\
1.109 - \tt EX! & \idx{Ex1} & $(\alpha::term\To bool)\To bool$ & 10 &
1.110 - unique existence ($\exists!$)
1.111 -\end{tabular}
1.112 -\end{center}
1.113 -\subcaption{Alternative quantifiers}
1.114 -
1.115 -\begin{center}
1.116 -\indexbold{*"=}
1.117 -\indexbold{&@{\tt\&}}
1.118 -\indexbold{*"|}
1.119 -\indexbold{*"-"-">}
1.120 +\index{*"= symbol}
1.121 +\index{&@{\tt\&} symbol}
1.122 +\index{*"| symbol}
1.123 +\index{*"-"-"> symbol}
1.124 \begin{tabular}{rrrr}
1.125 - \it symbol & \it meta-type & \it precedence & \it description \\
1.126 - \idx{o} & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ &
1.127 + \it symbol & \it meta-type & \it priority & \it description \\
1.128 + \sdx{o} & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ &
1.129 Right 50 & composition ($\circ$) \\
1.130 \tt = & $[\alpha::term,\alpha]\To bool$ & Left 50 & equality ($=$) \\
1.131 + \tt < & $[\alpha::ord,\alpha]\To bool$ & Left 50 & less than ($<$) \\
1.132 + \tt <= & $[\alpha::ord,\alpha]\To bool$ & Left 50 &
1.133 + less than or equals ($\leq$)\\
1.134 \tt \& & $[bool,bool]\To bool$ & Right 35 & conjunction ($\conj$) \\
1.135 \tt | & $[bool,bool]\To bool$ & Right 30 & disjunction ($\disj$) \\
1.136 - \tt --> & $[bool,bool]\To bool$ & Right 25 & implication ($\imp$) \\
1.137 - \tt < & $[\alpha::ord,\alpha]\To bool$ & Left 50 & less than ($<$) \\
1.138 - \tt <= & $[\alpha::ord,\alpha]\To bool$ & Left 50 &
1.139 - less than or equals ($\leq$)
1.140 + \tt --> & $[bool,bool]\To bool$ & Right 25 & implication ($\imp$)
1.141 \end{tabular}
1.142 \end{center}
1.143 \subcaption{Infixes}
1.144 @@ -99,13 +89,15 @@
1.145
1.146
1.147 \begin{figure}
1.148 -\indexbold{*let}
1.149 -\indexbold{*in}
1.150 +\index{*let symbol}
1.151 +\index{*in symbol}
1.152 \dquotes
1.153 -\[\begin{array}{rcl}
1.154 +\[\begin{array}{rclcl}
1.155 term & = & \hbox{expression of class~$term$} \\
1.156 - & | & "\at~~" id~id^* " . " formula \\
1.157 - & | & "let"~id~"="~term";"\dots";"~id~"="~term~"in"~term \\[2ex]
1.158 + & | & "\at~" id~id^* " . " formula \\
1.159 + & | &
1.160 + \multicolumn{3}{l}{"let"~id~"="~term";"\dots";"~id~"="~term~"in"~term}
1.161 + \\[2ex]
1.162 formula & = & \hbox{expression of type~$bool$} \\
1.163 & | & term " = " term \\
1.164 & | & term " \ttilde= " term \\
1.165 @@ -115,46 +107,58 @@
1.166 & | & formula " \& " formula \\
1.167 & | & formula " | " formula \\
1.168 & | & formula " --> " formula \\
1.169 - & | & "!~~~" id~id^* " . " formula \\
1.170 - & | & "?~~~" id~id^* " . " formula \\
1.171 - & | & "?!~~" id~id^* " . " formula \\
1.172 + & | & "!~~~" id~id^* " . " formula
1.173 & | & "ALL~" id~id^* " . " formula \\
1.174 + & | & "?~~~" id~id^* " . " formula
1.175 & | & "EX~~" id~id^* " . " formula \\
1.176 + & | & "?!~~" id~id^* " . " formula
1.177 & | & "EX!~" id~id^* " . " formula
1.178 \end{array}
1.179 \]
1.180 -\subcaption{Grammar}
1.181 \caption{Full grammar for \HOL} \label{hol-grammar}
1.182 \end{figure}
1.183
1.184
1.185 \section{Syntax}
1.186 -Type inference is automatic, exploiting Isabelle's type classes. The class
1.187 -of higher-order terms is called {\it term\/}; type variables range over
1.188 -this class by default. The equality symbol and quantifiers are polymorphic
1.189 -over class {\it term}.
1.190 +The type class of higher-order terms is called~\cldx{term}. Type variables
1.191 +range over this class by default. The equality symbol and quantifiers are
1.192 +polymorphic over class {\tt term}.
1.193
1.194 -Class {\it ord\/} consists of all ordered types; the relations $<$ and
1.195 +Class \cldx{ord} consists of all ordered types; the relations $<$ and
1.196 $\leq$ are polymorphic over this class, as are the functions
1.197 -\ttindex{mono}, \ttindex{min} and \ttindex{max}. Three other
1.198 -type classes --- {\it plus}, {\it minus\/} and {\it times} --- permit
1.199 +\cdx{mono}, \cdx{min} and \cdx{max}. Three other
1.200 +type classes --- \cldx{plus}, \cldx{minus} and \cldx{times} --- permit
1.201 overloading of the operators {\tt+}, {\tt-} and {\tt*}. In particular,
1.202 {\tt-} is overloaded for set difference and subtraction.
1.203 -\index{*"+}\index{-@{\tt-}}\index{*@{\tt*}}
1.204 +\index{*"+ symbol}
1.205 +\index{*"- symbol}
1.206 +\index{*"* symbol}
1.207
1.208 Figure~\ref{hol-constants} lists the constants (including infixes and
1.209 -binders), while Fig.\ts \ref{hol-grammar} presents the grammar of
1.210 +binders), while Fig.\ts\ref{hol-grammar} presents the grammar of
1.211 higher-order logic. Note that $a$\verb|~=|$b$ is translated to
1.212 -\verb|~(|$a$=$b$\verb|)|.
1.213 +$\neg(a=b)$.
1.214 +
1.215 +\begin{warn}
1.216 + \HOL\ has no if-and-only-if connective; logical equivalence is expressed
1.217 + using equality. But equality has a high priority, as befitting a
1.218 + relation, while if-and-only-if typically has the lowest priority. Thus,
1.219 + $\neg\neg P=P$ abbreviates $\neg\neg (P=P)$ and not $(\neg\neg P)=P$.
1.220 + When using $=$ to mean logical equivalence, enclose both operands in
1.221 + parentheses.
1.222 +\end{warn}
1.223
1.224 \subsection{Types}\label{HOL-types}
1.225 -The type of formulae, {\it bool} belongs to class {\it term}; thus,
1.226 -formulae are terms. The built-in type~$fun$, which constructs function
1.227 -types, is overloaded such that $\sigma\To\tau$ belongs to class~$term$ if
1.228 -$\sigma$ and~$\tau$ do; this allows quantification over functions. Types
1.229 -in \HOL\ must be non-empty; otherwise the quantifier rules would be
1.230 -unsound~\cite[\S7]{paulson-COLOG}.
1.231 +The type of formulae, \tydx{bool}, belongs to class \cldx{term}; thus,
1.232 +formulae are terms. The built-in type~\tydx{fun}, which constructs function
1.233 +types, is overloaded with arity {\tt(term,term)term}. Thus, $\sigma\To\tau$
1.234 +belongs to class~{\tt term} if $\sigma$ and~$\tau$ do, allowing quantification
1.235 +over functions.
1.236
1.237 +Types in \HOL\ must be non-empty; otherwise the quantifier rules would be
1.238 +unsound. I have commented on this elsewhere~\cite[\S7]{paulson-COLOG}.
1.239 +
1.240 +\index{type definitions}
1.241 Gordon's {\sc hol} system supports {\bf type definitions}. A type is
1.242 defined by exhibiting an existing type~$\sigma$, a predicate~$P::\sigma\To
1.243 bool$, and a theorem of the form $\exists x::\sigma.P(x)$. Thus~$P$
1.244 @@ -166,9 +170,9 @@
1.245 type.
1.246
1.247 Isabelle does not support type definitions at present. Instead, they are
1.248 -mimicked by explicit definitions of isomorphism functions. These should be
1.249 -accompanied by theorems of the form $\exists x::\sigma.P(x)$, but this is
1.250 -not checked.
1.251 +mimicked by explicit definitions of isomorphism functions. The definitions
1.252 +should be supported by theorems of the form $\exists x::\sigma.P(x)$, but
1.253 +Isabelle cannot enforce this.
1.254
1.255
1.256 \subsection{Binders}
1.257 @@ -176,116 +180,166 @@
1.258 satisfying~$P[a]$, if such exists. Since all terms in \HOL\ denote
1.259 something, a description is always meaningful, but we do not know its value
1.260 unless $P[x]$ defines it uniquely. We may write descriptions as
1.261 -\ttindexbold{Eps}($P$) or use the syntax
1.262 -\hbox{\tt \at $x$.$P[x]$}. Existential quantification is defined
1.263 -by
1.264 -\[ \exists x.P(x) \equiv P(\epsilon x.P(x)) \]
1.265 +\cdx{Eps}($P$) or use the syntax
1.266 +\hbox{\tt \at $x$.$P[x]$}.
1.267 +
1.268 +Existential quantification is defined by
1.269 +\[ \exists x.P(x) \;\equiv\; P(\epsilon x.P(x)). \]
1.270 The unique existence quantifier, $\exists!x.P[x]$, is defined in terms
1.271 of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested
1.272 quantifications. For instance, $\exists!x y.P(x,y)$ abbreviates
1.273 $\exists!x. \exists!y.P(x,y)$; note that this does not mean that there
1.274 exists a unique pair $(x,y)$ satisfying~$P(x,y)$.
1.275
1.276 -\index{*"!}\index{*"?}
1.277 +\index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system}
1.278 Quantifiers have two notations. As in Gordon's {\sc hol} system, \HOL\
1.279 uses~{\tt!}\ and~{\tt?}\ to stand for $\forall$ and $\exists$. The
1.280 existential quantifier must be followed by a space; thus {\tt?x} is an
1.281 unknown, while \verb'? x.f(x)=y' is a quantification. Isabelle's usual
1.282 -notation for quantifiers, \ttindex{ALL} and \ttindex{EX}, is also
1.283 +notation for quantifiers, \sdx{ALL} and \sdx{EX}, is also
1.284 available. Both notations are accepted for input. The {\ML} reference
1.285 \ttindexbold{HOL_quantifiers} governs the output notation. If set to {\tt
1.286 true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default. If set
1.287 to {\tt false}, then~{\tt ALL} and~{\tt EX} are displayed.
1.288
1.289 -\begin{warn}
1.290 -Although the description operator does not usually allow iteration of the
1.291 -form \hbox{\tt \at $x@1 \dots x@n$.$P[x@1,\dots,x@n]$}, there are cases where
1.292 -this is legal. If \hbox{\tt \at $y$.$P[x,y]$} is of type~{\it bool},
1.293 -then \hbox{\tt \at $x\,y$.$P[x,y]$} is legal. The pretty printer will
1.294 -display \hbox{\tt \at $x$.\at $y$.$P[x,y]$} as
1.295 -\hbox{\tt \at $x\,y$.$P[x,y]$}.
1.296 -\end{warn}
1.297 +All these binders have priority 10.
1.298
1.299 -\subsection{\idx{let} and \idx{case}}
1.300 -Local abbreviations can be introduced via a \ttindex{let}-construct whose
1.301 -syntax is shown in Fig.~\ref{hol-grammar}. Internally it is translated into
1.302 -the constant \ttindex{Let} and can be expanded by rewriting with its
1.303 -definition \ttindex{Let_def}.
1.304
1.305 -\HOL\ also defines the basic syntax {\dquotes$"case"~e~"of"~c@1~"=>"~e@1~"|"
1.306 - \dots "|"~c@n~"=>"~e@n$} for {\tt case}-constructs, which means that {\tt
1.307 - case} and \ttindex{of} are reserved words. However, so far this is mere
1.308 -syntax and has no logical meaning. In order to be useful it needs to be
1.309 -filled with life by translating certain case constructs into meaningful
1.310 -terms. For an example see the case construct for the type of lists below.
1.311 +\subsection{The \sdx{let} and \sdx{case} constructions}
1.312 +Local abbreviations can be introduced by a {\tt let} construct whose
1.313 +syntax appears in Fig.\ts\ref{hol-grammar}. Internally it is translated into
1.314 +the constant~\cdx{Let}. It can be expanded by rewriting with its
1.315 +definition, \tdx{Let_def}.
1.316 +
1.317 +\HOL\ also defines the basic syntax
1.318 +\[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n\]
1.319 +as a uniform means of expressing {\tt case} constructs. Therefore {\tt
1.320 + case} and \sdx{of} are reserved words. However, so far this is mere
1.321 +syntax and has no logical meaning. By declaring translations, you can
1.322 +cause instances of the {\tt case} construct to denote applications of
1.323 +particular case operators. The patterns supplied for $c@1$,~\ldots,~$c@n$
1.324 +distinguish among the different case operators. For an example, see the
1.325 +case construct for lists on page~\pageref{hol-list} below.
1.326
1.327
1.328 \begin{figure}
1.329 \begin{ttbox}\makeatother
1.330 -\idx{refl} t = t::'a
1.331 -\idx{subst} [| s=t; P(s) |] ==> P(t::'a)
1.332 -\idx{ext} (!!x::'a. f(x)::'b = g(x)) ==> (\%x.f(x)) = (\%x.g(x))
1.333 -\idx{impI} (P ==> Q) ==> P-->Q
1.334 -\idx{mp} [| P-->Q; P |] ==> Q
1.335 -\idx{iff} (P-->Q) --> (Q-->P) --> (P=Q)
1.336 -\idx{selectI} P(x::'a) ==> P(@x.P(x))
1.337 -\idx{True_or_False} (P=True) | (P=False)
1.338 -\subcaption{basic rules}
1.339 +\tdx{refl} t = t::'a
1.340 +\tdx{subst} [| s=t; P(s) |] ==> P(t::'a)
1.341 +\tdx{ext} (!!x::'a. f(x)::'b = g(x)) ==> (\%x.f(x)) = (\%x.g(x))
1.342 +\tdx{impI} (P ==> Q) ==> P-->Q
1.343 +\tdx{mp} [| P-->Q; P |] ==> Q
1.344 +\tdx{iff} (P-->Q) --> (Q-->P) --> (P=Q)
1.345 +\tdx{selectI} P(x::'a) ==> P(@x.P(x))
1.346 +\tdx{True_or_False} (P=True) | (P=False)
1.347 +\end{ttbox}
1.348 +\caption{The {\tt HOL} rules} \label{hol-rules}
1.349 +\end{figure}
1.350
1.351 -\idx{True_def} True = ((\%x.x)=(\%x.x))
1.352 -\idx{All_def} All = (\%P. P = (\%x.True))
1.353 -\idx{Ex_def} Ex = (\%P. P(@x.P(x)))
1.354 -\idx{False_def} False = (!P.P)
1.355 -\idx{not_def} not = (\%P. P-->False)
1.356 -\idx{and_def} op & = (\%P Q. !R. (P-->Q-->R) --> R)
1.357 -\idx{or_def} op | = (\%P Q. !R. (P-->R) --> (Q-->R) --> R)
1.358 -\idx{Ex1_def} Ex1 = (\%P. ? x. P(x) & (! y. P(y) --> y=x))
1.359 -\subcaption{Definitions of the logical constants}
1.360
1.361 -\idx{Inv_def} Inv = (\%(f::'a=>'b) y. @x. f(x)=y)
1.362 -\idx{o_def} op o = (\%(f::'b=>'c) g (x::'a). f(g(x)))
1.363 -\idx{if_def} if = (\%P x y.@z::'a.(P=True --> z=x) & (P=False --> z=y))
1.364 -\idx{Let_def} Let(s,f) = f(s)
1.365 -\subcaption{Further definitions}
1.366 +\begin{figure}
1.367 +\begin{ttbox}\makeatother
1.368 +\tdx{True_def} True = ((\%x.x)=(\%x.x))
1.369 +\tdx{All_def} All = (\%P. P = (\%x.True))
1.370 +\tdx{Ex_def} Ex = (\%P. P(@x.P(x)))
1.371 +\tdx{False_def} False = (!P.P)
1.372 +\tdx{not_def} not = (\%P. P-->False)
1.373 +\tdx{and_def} op & = (\%P Q. !R. (P-->Q-->R) --> R)
1.374 +\tdx{or_def} op | = (\%P Q. !R. (P-->R) --> (Q-->R) --> R)
1.375 +\tdx{Ex1_def} Ex1 = (\%P. ? x. P(x) & (! y. P(y) --> y=x))
1.376 +
1.377 +\tdx{Inv_def} Inv = (\%(f::'a=>'b) y. @x. f(x)=y)
1.378 +\tdx{o_def} op o = (\%(f::'b=>'c) g (x::'a). f(g(x)))
1.379 +\tdx{if_def} if = (\%P x y.@z::'a.(P=True --> z=x) & (P=False --> z=y))
1.380 +\tdx{Let_def} Let(s,f) = f(s)
1.381 \end{ttbox}
1.382 -\caption{Rules of {\tt HOL}} \label{hol-rules}
1.383 +\caption{The {\tt HOL} definitions} \label{hol-defs}
1.384 \end{figure}
1.385
1.386
1.387 +\section{Rules of inference}
1.388 +Figure~\ref{hol-rules} shows the inference rules of~\HOL{}, with
1.389 +their~{\ML} names. Some of the rules deserve additional comments:
1.390 +\begin{ttdescription}
1.391 +\item[\tdx{ext}] expresses extensionality of functions.
1.392 +\item[\tdx{iff}] asserts that logically equivalent formulae are
1.393 + equal.
1.394 +\item[\tdx{selectI}] gives the defining property of the Hilbert
1.395 + $\epsilon$-operator. It is a form of the Axiom of Choice. The derived rule
1.396 + \tdx{select_equality} (see below) is often easier to use.
1.397 +\item[\tdx{True_or_False}] makes the logic classical.\footnote{In
1.398 + fact, the $\epsilon$-operator already makes the logic classical, as
1.399 + shown by Diaconescu; see Paulson~\cite{paulson-COLOG} for details.}
1.400 +\end{ttdescription}
1.401 +
1.402 +\HOL{} follows standard practice in higher-order logic: only a few
1.403 +connectives are taken as primitive, with the remainder defined obscurely
1.404 +(Fig.\ts\ref{hol-defs}). Unusually, the definitions are expressed using
1.405 +object-equality~({\tt=}) rather than meta-equality~({\tt==}). This is
1.406 +possible because equality in higher-order logic may equate formulae and
1.407 +even functions over formulae. On the other hand, meta-equality is
1.408 +Isabelle's usual symbol for making definitions. Take care to note which
1.409 +form of equality is used before attempting a proof.
1.410 +
1.411 +Some of the rules mention type variables; for example, {\tt refl} mentions
1.412 +the type variable~{\tt'a}. This allows you to instantiate type variables
1.413 +explicitly by calling {\tt res_inst_tac}. By default, explicit type
1.414 +variables have class \cldx{term}.
1.415 +
1.416 +Include type constraints whenever you state a polymorphic goal. Type
1.417 +inference may otherwise make the goal more polymorphic than you intended,
1.418 +with confusing results.
1.419 +
1.420 +\begin{warn}
1.421 + If resolution fails for no obvious reason, try setting
1.422 + \ttindex{show_types} to {\tt true}, causing Isabelle to display types of
1.423 + terms. Possibly set \ttindex{show_sorts} to {\tt true} as well, causing
1.424 + Isabelle to display sorts.
1.425 +
1.426 + \index{unification!incompleteness of}
1.427 + Where function types are involved, Isabelle's unification code does not
1.428 + guarantee to find instantiations for type variables automatically. Be
1.429 + prepared to use \ttindex{res_inst_tac} instead of {\tt resolve_tac},
1.430 + possibly instantiating type variables. Setting
1.431 + \ttindex{Unify.trace_types} to {\tt true} causes Isabelle to report
1.432 + omitted search paths during unification.\index{tracing!of unification}
1.433 +\end{warn}
1.434 +
1.435 +
1.436 \begin{figure}
1.437 \begin{ttbox}
1.438 -\idx{sym} s=t ==> t=s
1.439 -\idx{trans} [| r=s; s=t |] ==> r=t
1.440 -\idx{ssubst} [| t=s; P(s) |] ==> P(t::'a)
1.441 -\idx{box_equals} [| a=b; a=c; b=d |] ==> c=d
1.442 -\idx{arg_cong} s=t ==> f(s)=f(t)
1.443 -\idx{fun_cong} s::'a=>'b = t ==> s(x)=t(x)
1.444 +\tdx{sym} s=t ==> t=s
1.445 +\tdx{trans} [| r=s; s=t |] ==> r=t
1.446 +\tdx{ssubst} [| t=s; P(s) |] ==> P(t::'a)
1.447 +\tdx{box_equals} [| a=b; a=c; b=d |] ==> c=d
1.448 +\tdx{arg_cong} s=t ==> f(s)=f(t)
1.449 +\tdx{fun_cong} s::'a=>'b = t ==> s(x)=t(x)
1.450 \subcaption{Equality}
1.451
1.452 -\idx{TrueI} True
1.453 -\idx{FalseE} False ==> P
1.454 +\tdx{TrueI} True
1.455 +\tdx{FalseE} False ==> P
1.456
1.457 -\idx{conjI} [| P; Q |] ==> P&Q
1.458 -\idx{conjunct1} [| P&Q |] ==> P
1.459 -\idx{conjunct2} [| P&Q |] ==> Q
1.460 -\idx{conjE} [| P&Q; [| P; Q |] ==> R |] ==> R
1.461 +\tdx{conjI} [| P; Q |] ==> P&Q
1.462 +\tdx{conjunct1} [| P&Q |] ==> P
1.463 +\tdx{conjunct2} [| P&Q |] ==> Q
1.464 +\tdx{conjE} [| P&Q; [| P; Q |] ==> R |] ==> R
1.465
1.466 -\idx{disjI1} P ==> P|Q
1.467 -\idx{disjI2} Q ==> P|Q
1.468 -\idx{disjE} [| P | Q; P ==> R; Q ==> R |] ==> R
1.469 +\tdx{disjI1} P ==> P|Q
1.470 +\tdx{disjI2} Q ==> P|Q
1.471 +\tdx{disjE} [| P | Q; P ==> R; Q ==> R |] ==> R
1.472
1.473 -\idx{notI} (P ==> False) ==> ~ P
1.474 -\idx{notE} [| ~ P; P |] ==> R
1.475 -\idx{impE} [| P-->Q; P; Q ==> R |] ==> R
1.476 +\tdx{notI} (P ==> False) ==> ~ P
1.477 +\tdx{notE} [| ~ P; P |] ==> R
1.478 +\tdx{impE} [| P-->Q; P; Q ==> R |] ==> R
1.479 \subcaption{Propositional logic}
1.480
1.481 -\idx{iffI} [| P ==> Q; Q ==> P |] ==> P=Q
1.482 -\idx{iffD1} [| P=Q; P |] ==> Q
1.483 -\idx{iffD2} [| P=Q; Q |] ==> P
1.484 -\idx{iffE} [| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R
1.485 +\tdx{iffI} [| P ==> Q; Q ==> P |] ==> P=Q
1.486 +\tdx{iffD1} [| P=Q; P |] ==> Q
1.487 +\tdx{iffD2} [| P=Q; Q |] ==> P
1.488 +\tdx{iffE} [| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R
1.489
1.490 -\idx{eqTrueI} P ==> P=True
1.491 -\idx{eqTrueE} P=True ==> P
1.492 +\tdx{eqTrueI} P ==> P=True
1.493 +\tdx{eqTrueE} P=True ==> P
1.494 \subcaption{Logical equivalence}
1.495
1.496 \end{ttbox}
1.497 @@ -295,106 +349,51 @@
1.498
1.499 \begin{figure}
1.500 \begin{ttbox}\makeatother
1.501 -\idx{allI} (!!x::'a. P(x)) ==> !x. P(x)
1.502 -\idx{spec} !x::'a.P(x) ==> P(x)
1.503 -\idx{allE} [| !x.P(x); P(x) ==> R |] ==> R
1.504 -\idx{all_dupE} [| !x.P(x); [| P(x); !x.P(x) |] ==> R |] ==> R
1.505 +\tdx{allI} (!!x::'a. P(x)) ==> !x. P(x)
1.506 +\tdx{spec} !x::'a.P(x) ==> P(x)
1.507 +\tdx{allE} [| !x.P(x); P(x) ==> R |] ==> R
1.508 +\tdx{all_dupE} [| !x.P(x); [| P(x); !x.P(x) |] ==> R |] ==> R
1.509
1.510 -\idx{exI} P(x) ==> ? x::'a.P(x)
1.511 -\idx{exE} [| ? x::'a.P(x); !!x. P(x) ==> Q |] ==> Q
1.512 +\tdx{exI} P(x) ==> ? x::'a.P(x)
1.513 +\tdx{exE} [| ? x::'a.P(x); !!x. P(x) ==> Q |] ==> Q
1.514
1.515 -\idx{ex1I} [| P(a); !!x. P(x) ==> x=a |] ==> ?! x. P(x)
1.516 -\idx{ex1E} [| ?! x.P(x); !!x. [| P(x); ! y. P(y) --> y=x |] ==> R
1.517 +\tdx{ex1I} [| P(a); !!x. P(x) ==> x=a |] ==> ?! x. P(x)
1.518 +\tdx{ex1E} [| ?! x.P(x); !!x. [| P(x); ! y. P(y) --> y=x |] ==> R
1.519 |] ==> R
1.520
1.521 -\idx{select_equality} [| P(a); !!x. P(x) ==> x=a |] ==> (@x.P(x)) = a
1.522 +\tdx{select_equality} [| P(a); !!x. P(x) ==> x=a |] ==> (@x.P(x)) = a
1.523 \subcaption{Quantifiers and descriptions}
1.524
1.525 -\idx{ccontr} (~P ==> False) ==> P
1.526 -\idx{classical} (~P ==> P) ==> P
1.527 -\idx{excluded_middle} ~P | P
1.528 +\tdx{ccontr} (~P ==> False) ==> P
1.529 +\tdx{classical} (~P ==> P) ==> P
1.530 +\tdx{excluded_middle} ~P | P
1.531
1.532 -\idx{disjCI} (~Q ==> P) ==> P|Q
1.533 -\idx{exCI} (! x. ~ P(x) ==> P(a)) ==> ? x.P(x)
1.534 -\idx{impCE} [| P-->Q; ~ P ==> R; Q ==> R |] ==> R
1.535 -\idx{iffCE} [| P=Q; [| P; Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R
1.536 -\idx{notnotD} ~~P ==> P
1.537 -\idx{swap} ~P ==> (~Q ==> P) ==> Q
1.538 +\tdx{disjCI} (~Q ==> P) ==> P|Q
1.539 +\tdx{exCI} (! x. ~ P(x) ==> P(a)) ==> ? x.P(x)
1.540 +\tdx{impCE} [| P-->Q; ~ P ==> R; Q ==> R |] ==> R
1.541 +\tdx{iffCE} [| P=Q; [| P;Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R
1.542 +\tdx{notnotD} ~~P ==> P
1.543 +\tdx{swap} ~P ==> (~Q ==> P) ==> Q
1.544 \subcaption{Classical logic}
1.545
1.546 -\idx{if_True} if(True,x,y) = x
1.547 -\idx{if_False} if(False,x,y) = y
1.548 -\idx{if_P} P ==> if(P,x,y) = x
1.549 -\idx{if_not_P} ~ P ==> if(P,x,y) = y
1.550 -\idx{expand_if} P(if(Q,x,y)) = ((Q --> P(x)) & (~Q --> P(y)))
1.551 +\tdx{if_True} if(True,x,y) = x
1.552 +\tdx{if_False} if(False,x,y) = y
1.553 +\tdx{if_P} P ==> if(P,x,y) = x
1.554 +\tdx{if_not_P} ~ P ==> if(P,x,y) = y
1.555 +\tdx{expand_if} P(if(Q,x,y)) = ((Q --> P(x)) & (~Q --> P(y)))
1.556 \subcaption{Conditionals}
1.557 \end{ttbox}
1.558 \caption{More derived rules} \label{hol-lemmas2}
1.559 \end{figure}
1.560
1.561
1.562 -\section{Rules of inference}
1.563 -The basic theory has the {\ML} identifier \ttindexbold{HOL.thy}. However,
1.564 -many further theories are defined, introducing product and sum types, the
1.565 -natural numbers, etc.
1.566 -
1.567 -Figure~\ref{hol-rules} shows the inference rules with their~{\ML} names.
1.568 -They follow standard practice in higher-order logic: only a few connectives
1.569 -are taken as primitive, with the remainder defined obscurely.
1.570 -
1.571 -Unusually, the definitions are expressed using object-equality~({\tt=})
1.572 -rather than meta-equality~({\tt==}). This is possible because equality in
1.573 -higher-order logic may equate formulae and even functions over formulae.
1.574 -On the other hand, meta-equality is Isabelle's usual symbol for making
1.575 -definitions. Take care to note which form of equality is used before
1.576 -attempting a proof.
1.577 -
1.578 -Some of the rules mention type variables; for example, {\tt refl} mentions
1.579 -the type variable~{\tt'a}. This facilitates explicit instantiation of the
1.580 -type variables. By default, such variables range over class {\it term}.
1.581 -
1.582 -\begin{warn}
1.583 -Where function types are involved, Isabelle's unification code does not
1.584 -guarantee to find instantiations for type variables automatically. If
1.585 -resolution fails for no obvious reason, try setting \ttindex{show_types} to
1.586 -{\tt true}, causing Isabelle to display types of terms. (Possibly, set
1.587 -\ttindex{show_sorts} to {\tt true} also, causing Isabelle to display sorts.)
1.588 -Be prepared to use \ttindex{res_inst_tac} instead of {\tt resolve_tac}.
1.589 -Setting \ttindex{Unify.trace_types} to {\tt true} causes Isabelle to
1.590 -report omitted search paths during unification.
1.591 -\end{warn}
1.592 -
1.593 -Here are further comments on the rules:
1.594 -\begin{description}
1.595 -\item[\ttindexbold{ext}]
1.596 -expresses extensionality of functions.
1.597 -\item[\ttindexbold{iff}]
1.598 -asserts that logically equivalent formulae are equal.
1.599 -\item[\ttindexbold{selectI}]
1.600 -gives the defining property of the Hilbert $\epsilon$-operator. The
1.601 -derived rule \ttindexbold{select_equality} (see below) is often easier to use.
1.602 -\item[\ttindexbold{True_or_False}]
1.603 -makes the logic classical.\footnote{In fact, the $\epsilon$-operator
1.604 -already makes the logic classical, as shown by Diaconescu;
1.605 -see Paulson~\cite{paulson-COLOG} for details.}
1.606 -\end{description}
1.607 -
1.608 -\begin{warn}
1.609 -\HOL\ has no if-and-only-if connective; logical equivalence is expressed
1.610 -using equality. But equality has a high precedence, as befitting a
1.611 -relation, while if-and-only-if typically has the lowest precedence. Thus,
1.612 -$\neg\neg P=P$ abbreviates $\neg\neg (P=P)$ and not $(\neg\neg P)=P$. When
1.613 -using $=$ to mean logical equivalence, enclose both operands in
1.614 -parentheses.
1.615 -\end{warn}
1.616 -
1.617 Some derived rules are shown in Figures~\ref{hol-lemmas1}
1.618 and~\ref{hol-lemmas2}, with their {\ML} names. These include natural rules
1.619 for the logical connectives, as well as sequent-style elimination rules for
1.620 conjunctions, implications, and universal quantifiers.
1.621
1.622 -Note the equality rules: \ttindexbold{ssubst} performs substitution in
1.623 -backward proofs, while \ttindexbold{box_equals} supports reasoning by
1.624 +Note the equality rules: \tdx{ssubst} performs substitution in
1.625 +backward proofs, while \tdx{box_equals} supports reasoning by
1.626 simplifying both sides of an equation.
1.627
1.628 See the files {\tt HOL/hol.thy} and
1.629 @@ -408,7 +407,7 @@
1.630 \begin{itemize}
1.631 \item
1.632 Because it includes a general substitution rule, \HOL\ instantiates the
1.633 -tactic \ttindex{hyp_subst_tac}, which substitutes for an equality
1.634 +tactic {\tt hyp_subst_tac}, which substitutes for an equality
1.635 throughout a subgoal and its hypotheses.
1.636 \item
1.637 It instantiates the simplifier, defining~\ttindexbold{HOL_ss} as the
1.638 @@ -426,31 +425,31 @@
1.639 \begin{center}
1.640 \begin{tabular}{rrr}
1.641 \it name &\it meta-type & \it description \\
1.642 -\index{"{"}@{\tt\{\}}}
1.643 - {\tt\{\}} & $\alpha\,set$ & the empty set \\
1.644 - \idx{insert} & $[\alpha,\alpha\,set]\To \alpha\,set$
1.645 +\index{{}@\verb'{}' symbol}
1.646 + \verb|{}| & $\alpha\,set$ & the empty set \\
1.647 + \cdx{insert} & $[\alpha,\alpha\,set]\To \alpha\,set$
1.648 & insertion of element \\
1.649 - \idx{Collect} & $(\alpha\To bool)\To\alpha\,set$
1.650 + \cdx{Collect} & $(\alpha\To bool)\To\alpha\,set$
1.651 & comprehension \\
1.652 - \idx{Compl} & $(\alpha\,set)\To\alpha\,set$
1.653 + \cdx{Compl} & $(\alpha\,set)\To\alpha\,set$
1.654 & complement \\
1.655 - \idx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
1.656 + \cdx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
1.657 & intersection over a set\\
1.658 - \idx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
1.659 + \cdx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
1.660 & union over a set\\
1.661 - \idx{Inter} & $((\alpha\,set)set)\To\alpha\,set$
1.662 + \cdx{Inter} & $((\alpha\,set)set)\To\alpha\,set$
1.663 &set of sets intersection \\
1.664 - \idx{Union} & $((\alpha\,set)set)\To\alpha\,set$
1.665 + \cdx{Union} & $((\alpha\,set)set)\To\alpha\,set$
1.666 &set of sets union \\
1.667 - \idx{range} & $(\alpha\To\beta )\To\beta\,set$
1.668 + \cdx{range} & $(\alpha\To\beta )\To\beta\,set$
1.669 & range of a function \\[1ex]
1.670 - \idx{Ball}~~\idx{Bex} & $[\alpha\,set,\alpha\To bool]\To bool$
1.671 + \cdx{Ball}~~\cdx{Bex} & $[\alpha\,set,\alpha\To bool]\To bool$
1.672 & bounded quantifiers \\
1.673 - \idx{mono} & $(\alpha\,set\To\beta\,set)\To bool$
1.674 + \cdx{mono} & $(\alpha\,set\To\beta\,set)\To bool$
1.675 & monotonicity \\
1.676 - \idx{inj}~~\idx{surj}& $(\alpha\To\beta )\To bool$
1.677 + \cdx{inj}~~\cdx{surj}& $(\alpha\To\beta )\To bool$
1.678 & injective/surjective \\
1.679 - \idx{inj_onto} & $[\alpha\To\beta ,\alpha\,set]\To bool$
1.680 + \cdx{inj_onto} & $[\alpha\To\beta ,\alpha\,set]\To bool$
1.681 & injective over subset
1.682 \end{tabular}
1.683 \end{center}
1.684 @@ -458,26 +457,26 @@
1.685
1.686 \begin{center}
1.687 \begin{tabular}{llrrr}
1.688 - \it symbol &\it name &\it meta-type & \it prec & \it description \\
1.689 - \idx{INT} & \idx{INTER1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 &
1.690 + \it symbol &\it name &\it meta-type & \it priority & \it description \\
1.691 + \sdx{INT} & \cdx{INTER1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 &
1.692 intersection over a type\\
1.693 - \idx{UN} & \idx{UNION1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 &
1.694 + \sdx{UN} & \cdx{UNION1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 &
1.695 union over a type
1.696 \end{tabular}
1.697 \end{center}
1.698 \subcaption{Binders}
1.699
1.700 \begin{center}
1.701 -\indexbold{*"`"`}
1.702 -\indexbold{*":}
1.703 -\indexbold{*"<"=}
1.704 +\index{*"`"` symbol}
1.705 +\index{*": symbol}
1.706 +\index{*"<"= symbol}
1.707 \begin{tabular}{rrrr}
1.708 - \it symbol & \it meta-type & \it precedence & \it description \\
1.709 + \it symbol & \it meta-type & \it priority & \it description \\
1.710 \tt `` & $[\alpha\To\beta ,\alpha\,set]\To (\beta\,set)$
1.711 & Left 90 & image \\
1.712 - \idx{Int} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$
1.713 + \sdx{Int} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$
1.714 & Left 70 & intersection ($\inter$) \\
1.715 - \idx{Un} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$
1.716 + \sdx{Un} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$
1.717 & Left 65 & union ($\union$) \\
1.718 \tt: & $[\alpha ,\alpha\,set]\To bool$
1.719 & Left 50 & membership ($\in$) \\
1.720 @@ -486,38 +485,34 @@
1.721 \end{tabular}
1.722 \end{center}
1.723 \subcaption{Infixes}
1.724 -\caption{Syntax of \HOL's set theory} \label{hol-set-syntax}
1.725 +\caption{Syntax of the theory {\tt Set}} \label{hol-set-syntax}
1.726 \end{figure}
1.727
1.728
1.729 \begin{figure}
1.730 \begin{center} \tt\frenchspacing
1.731 -\index{*"!|bold}
1.732 +\index{*"! symbol}
1.733 \begin{tabular}{rrr}
1.734 \it external & \it internal & \it description \\
1.735 - $a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm negated membership\\
1.736 - \{$a@1$, $\ldots$, $a@n$\} & insert($a@1$,$\cdots$,insert($a@n$,\{\})) &
1.737 - \rm finite set \\
1.738 + $a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm non-membership\\
1.739 + \{$a@1$, $\ldots$\} & insert($a@1$, $\ldots$\{\}) & \rm finite set \\
1.740 \{$x$.$P[x]$\} & Collect($\lambda x.P[x]$) &
1.741 \rm comprehension \\
1.742 - \idx{INT} $x$:$A$.$B[x]$ & INTER($A$,$\lambda x.B[x]$) &
1.743 - \rm intersection over a set \\
1.744 - \idx{UN} $x$:$A$.$B[x]$ & UNION($A$,$\lambda x.B[x]$) &
1.745 - \rm union over a set \\
1.746 - \tt ! $x$:$A$.$P[x]$ & Ball($A$,$\lambda x.P[x]$) &
1.747 + \sdx{INT} $x$:$A$.$B[x]$ & INTER($A$,$\lambda x.B[x]$) &
1.748 + \rm intersection \\
1.749 + \sdx{UN}{\tt\ } $x$:$A$.$B[x]$ & UNION($A$,$\lambda x.B[x]$) &
1.750 + \rm union \\
1.751 + \tt ! $x$:$A$.$P[x]$ or \sdx{ALL} $x$:$A$.$P[x]$ &
1.752 + Ball($A$,$\lambda x.P[x]$) &
1.753 \rm bounded $\forall$ \\
1.754 - \idx{?} $x$:$A$.$P[x]$ & Bex($A$,$\lambda x.P[x]$) &
1.755 - \rm bounded $\exists$ \\[1ex]
1.756 - \idx{ALL} $x$:$A$.$P[x]$ & Ball($A$,$\lambda x.P[x]$) &
1.757 - \rm bounded $\forall$ \\
1.758 - \idx{EX} $x$:$A$.$P[x]$ & Bex($A$,$\lambda x.P[x]$) &
1.759 - \rm bounded $\exists$
1.760 + \sdx{?} $x$:$A$.$P[x]$ or \sdx{EX}{\tt\ } $x$:$A$.$P[x]$ &
1.761 + Bex($A$,$\lambda x.P[x]$) & \rm bounded $\exists$
1.762 \end{tabular}
1.763 \end{center}
1.764 \subcaption{Translations}
1.765
1.766 \dquotes
1.767 -\[\begin{array}{rcl}
1.768 +\[\begin{array}{rclcl}
1.769 term & = & \hbox{other terms\ldots} \\
1.770 & | & "\{\}" \\
1.771 & | & "\{ " term\; ("," term)^* " \}" \\
1.772 @@ -533,130 +528,17 @@
1.773 & | & term " : " term \\
1.774 & | & term " \ttilde: " term \\
1.775 & | & term " <= " term \\
1.776 - & | & "!~~~" id ":" term " . " formula \\
1.777 - & | & "?~~~" id ":" term " . " formula \\
1.778 + & | & "!~" id ":" term " . " formula
1.779 & | & "ALL " id ":" term " . " formula \\
1.780 + & | & "?~" id ":" term " . " formula
1.781 & | & "EX~~" id ":" term " . " formula
1.782 \end{array}
1.783 \]
1.784 \subcaption{Full Grammar}
1.785 -\caption{Syntax of \HOL's set theory (continued)} \label{hol-set-syntax2}
1.786 +\caption{Syntax of the theory {\tt Set} (continued)} \label{hol-set-syntax2}
1.787 \end{figure}
1.788
1.789
1.790 -\begin{figure} \underscoreon
1.791 -\begin{ttbox}
1.792 -\idx{mem_Collect_eq} (a : \{x.P(x)\}) = P(a)
1.793 -\idx{Collect_mem_eq} \{x.x:A\} = A
1.794 -\subcaption{Isomorphisms between predicates and sets}
1.795 -
1.796 -\idx{empty_def} \{\} == \{x.x=False\}
1.797 -\idx{insert_def} insert(a,B) == \{x.x=a\} Un B
1.798 -\idx{Ball_def} Ball(A,P) == ! x. x:A --> P(x)
1.799 -\idx{Bex_def} Bex(A,P) == ? x. x:A & P(x)
1.800 -\idx{subset_def} A <= B == ! x:A. x:B
1.801 -\idx{Un_def} A Un B == \{x.x:A | x:B\}
1.802 -\idx{Int_def} A Int B == \{x.x:A & x:B\}
1.803 -\idx{set_diff_def} A - B == \{x.x:A & x~:B\}
1.804 -\idx{Compl_def} Compl(A) == \{x. ~ x:A\}
1.805 -\idx{INTER_def} INTER(A,B) == \{y. ! x:A. y: B(x)\}
1.806 -\idx{UNION_def} UNION(A,B) == \{y. ? x:A. y: B(x)\}
1.807 -\idx{INTER1_def} INTER1(B) == INTER(\{x.True\}, B)
1.808 -\idx{UNION1_def} UNION1(B) == UNION(\{x.True\}, B)
1.809 -\idx{Inter_def} Inter(S) == (INT x:S. x)
1.810 -\idx{Union_def} Union(S) == (UN x:S. x)
1.811 -\idx{image_def} f``A == \{y. ? x:A. y=f(x)\}
1.812 -\idx{range_def} range(f) == \{y. ? x. y=f(x)\}
1.813 -\idx{mono_def} mono(f) == !A B. A <= B --> f(A) <= f(B)
1.814 -\idx{inj_def} inj(f) == ! x y. f(x)=f(y) --> x=y
1.815 -\idx{surj_def} surj(f) == ! y. ? x. y=f(x)
1.816 -\idx{inj_onto_def} inj_onto(f,A) == !x:A. !y:A. f(x)=f(y) --> x=y
1.817 -\subcaption{Definitions}
1.818 -\end{ttbox}
1.819 -\caption{Rules of \HOL's set theory} \label{hol-set-rules}
1.820 -\end{figure}
1.821 -
1.822 -
1.823 -\begin{figure} \underscoreon
1.824 -\begin{ttbox}
1.825 -\idx{CollectI} [| P(a) |] ==> a : \{x.P(x)\}
1.826 -\idx{CollectD} [| a : \{x.P(x)\} |] ==> P(a)
1.827 -\idx{CollectE} [| a : \{x.P(x)\}; P(a) ==> W |] ==> W
1.828 -\idx{Collect_cong} [| !!x. P(x)=Q(x) |] ==> \{x. P(x)\} = \{x. Q(x)\}
1.829 -\subcaption{Comprehension}
1.830 -
1.831 -\idx{ballI} [| !!x. x:A ==> P(x) |] ==> ! x:A. P(x)
1.832 -\idx{bspec} [| ! x:A. P(x); x:A |] ==> P(x)
1.833 -\idx{ballE} [| ! x:A. P(x); P(x) ==> Q; ~ x:A ==> Q |] ==> Q
1.834 -\idx{ball_cong} [| A=A'; !!x. x:A' ==> P(x) = P'(x) |] ==>
1.835 - (! x:A. P(x)) = (! x:A'. P'(x))
1.836 -
1.837 -\idx{bexI} [| P(x); x:A |] ==> ? x:A. P(x)
1.838 -\idx{bexCI} [| ! x:A. ~ P(x) ==> P(a); a:A |] ==> ? x:A.P(x)
1.839 -\idx{bexE} [| ? x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q
1.840 -\subcaption{Bounded quantifiers}
1.841 -
1.842 -\idx{subsetI} (!!x.x:A ==> x:B) ==> A <= B
1.843 -\idx{subsetD} [| A <= B; c:A |] ==> c:B
1.844 -\idx{subsetCE} [| A <= B; ~ (c:A) ==> P; c:B ==> P |] ==> P
1.845 -
1.846 -\idx{subset_refl} A <= A
1.847 -\idx{subset_antisym} [| A <= B; B <= A |] ==> A = B
1.848 -\idx{subset_trans} [| A<=B; B<=C |] ==> A<=C
1.849 -
1.850 -\idx{set_ext} [| !!x. (x:A) = (x:B) |] ==> A = B
1.851 -\idx{equalityD1} A = B ==> A<=B
1.852 -\idx{equalityD2} A = B ==> B<=A
1.853 -\idx{equalityE} [| A = B; [| A<=B; B<=A |] ==> P |] ==> P
1.854 -
1.855 -\idx{equalityCE} [| A = B; [| c:A; c:B |] ==> P;
1.856 - [| ~ c:A; ~ c:B |] ==> P
1.857 - |] ==> P
1.858 -\subcaption{The subset and equality relations}
1.859 -\end{ttbox}
1.860 -\caption{Derived rules for set theory} \label{hol-set1}
1.861 -\end{figure}
1.862 -
1.863 -
1.864 -\begin{figure} \underscoreon
1.865 -\begin{ttbox}
1.866 -\idx{emptyE} a : \{\} ==> P
1.867 -
1.868 -\idx{insertI1} a : insert(a,B)
1.869 -\idx{insertI2} a : B ==> a : insert(b,B)
1.870 -\idx{insertE} [| a : insert(b,A); a=b ==> P; a:A ==> P |] ==> P
1.871 -
1.872 -\idx{ComplI} [| c:A ==> False |] ==> c : Compl(A)
1.873 -\idx{ComplD} [| c : Compl(A) |] ==> ~ c:A
1.874 -
1.875 -\idx{UnI1} c:A ==> c : A Un B
1.876 -\idx{UnI2} c:B ==> c : A Un B
1.877 -\idx{UnCI} (~c:B ==> c:A) ==> c : A Un B
1.878 -\idx{UnE} [| c : A Un B; c:A ==> P; c:B ==> P |] ==> P
1.879 -
1.880 -\idx{IntI} [| c:A; c:B |] ==> c : A Int B
1.881 -\idx{IntD1} c : A Int B ==> c:A
1.882 -\idx{IntD2} c : A Int B ==> c:B
1.883 -\idx{IntE} [| c : A Int B; [| c:A; c:B |] ==> P |] ==> P
1.884 -
1.885 -\idx{UN_I} [| a:A; b: B(a) |] ==> b: (UN x:A. B(x))
1.886 -\idx{UN_E} [| b: (UN x:A. B(x)); !!x.[| x:A; b:B(x) |] ==> R |] ==> R
1.887 -
1.888 -\idx{INT_I} (!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))
1.889 -\idx{INT_D} [| b: (INT x:A. B(x)); a:A |] ==> b: B(a)
1.890 -\idx{INT_E} [| b: (INT x:A. B(x)); b: B(a) ==> R; ~ a:A ==> R |] ==> R
1.891 -
1.892 -\idx{UnionI} [| X:C; A:X |] ==> A : Union(C)
1.893 -\idx{UnionE} [| A : Union(C); !!X.[| A:X; X:C |] ==> R |] ==> R
1.894 -
1.895 -\idx{InterI} [| !!X. X:C ==> A:X |] ==> A : Inter(C)
1.896 -\idx{InterD} [| A : Inter(C); X:C |] ==> A:X
1.897 -\idx{InterE} [| A : Inter(C); A:X ==> R; ~ X:C ==> R |] ==> R
1.898 -\end{ttbox}
1.899 -\caption{Further derived rules for set theory} \label{hol-set2}
1.900 -\end{figure}
1.901 -
1.902 -
1.903 \section{A formulation of set theory}
1.904 Historically, higher-order logic gives a foundation for Russell and
1.905 Whitehead's theory of classes. Let us use modern terminology and call them
1.906 @@ -677,100 +559,219 @@
1.907 do in~{\ZF}. In \HOL\ the intersection of the empty set is well-defined,
1.908 denoting the universal set for the given type.
1.909
1.910 -\subsection{Syntax of set theory}
1.911 -The type $\alpha\,set$ is essentially the same as $\alpha\To bool$. The
1.912 -new type is defined for clarity and to avoid complications involving
1.913 -function types in unification. Since Isabelle does not support type
1.914 -definitions (as mentioned in \S\ref{HOL-types}), the isomorphisms between
1.915 -the two types are declared explicitly. Here they are natural: {\tt
1.916 - Collect} maps $\alpha\To bool$ to $\alpha\,set$, while \hbox{\tt op :}
1.917 -maps in the other direction (ignoring argument order).
1.918 +
1.919 +\subsection{Syntax of set theory}\index{*set type}
1.920 +\HOL's set theory is called \thydx{Set}. The type $\alpha\,set$ is
1.921 +essentially the same as $\alpha\To bool$. The new type is defined for
1.922 +clarity and to avoid complications involving function types in unification.
1.923 +Since Isabelle does not support type definitions (as mentioned in
1.924 +\S\ref{HOL-types}), the isomorphisms between the two types are declared
1.925 +explicitly. Here they are natural: {\tt Collect} maps $\alpha\To bool$ to
1.926 +$\alpha\,set$, while \hbox{\tt op :} maps in the other direction (ignoring
1.927 +argument order).
1.928
1.929 Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax
1.930 translations. Figure~\ref{hol-set-syntax2} presents the grammar of the new
1.931 constructs. Infix operators include union and intersection ($A\union B$
1.932 and $A\inter B$), the subset and membership relations, and the image
1.933 -operator~{\tt``}. Note that $a$\verb|~:|$b$ is translated to
1.934 -\verb|~(|$a$:$b$\verb|)|. The {\tt\{\ldots\}} notation abbreviates finite
1.935 -sets constructed in the obvious manner using~{\tt insert} and~$\{\}$ (the
1.936 -empty set):
1.937 +operator~{\tt``}\@. Note that $a$\verb|~:|$b$ is translated to
1.938 +$\neg(a\in b)$.
1.939 +
1.940 +The {\tt\{\ldots\}} notation abbreviates finite sets constructed in the
1.941 +obvious manner using~{\tt insert} and~$\{\}$:
1.942 \begin{eqnarray*}
1.943 - \{a,b,c\} & \equiv & {\tt insert}(a,{\tt insert}(b,{\tt insert}(c,\{\})))
1.944 + \{a@1, \ldots, a@n\} & \equiv &
1.945 + {\tt insert}(a@1,\ldots,{\tt insert}(a@n,\{\}))
1.946 \end{eqnarray*}
1.947
1.948 The set \hbox{\tt\{$x$.$P[x]$\}} consists of all $x$ (of suitable type)
1.949 that satisfy~$P[x]$, where $P[x]$ is a formula that may contain free
1.950 -occurrences of~$x$. This syntax expands to \ttindexbold{Collect}$(\lambda
1.951 -x.P[x])$.
1.952 +occurrences of~$x$. This syntax expands to \cdx{Collect}$(\lambda
1.953 +x.P[x])$. It defines sets by absolute comprehension, which is impossible
1.954 +in~{\ZF}; the type of~$x$ implicitly restricts the comprehension.
1.955
1.956 The set theory defines two {\bf bounded quantifiers}:
1.957 \begin{eqnarray*}
1.958 - \forall x\in A.P[x] &\hbox{which abbreviates}& \forall x. x\in A\imp P[x] \\
1.959 - \exists x\in A.P[x] &\hbox{which abbreviates}& \exists x. x\in A\conj P[x]
1.960 + \forall x\in A.P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\
1.961 + \exists x\in A.P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x]
1.962 \end{eqnarray*}
1.963 -The constants~\ttindexbold{Ball} and~\ttindexbold{Bex} are defined
1.964 +The constants~\cdx{Ball} and~\cdx{Bex} are defined
1.965 accordingly. Instead of {\tt Ball($A$,$P$)} and {\tt Bex($A$,$P$)} we may
1.966 -write\index{*"!}\index{*"?}\index{*ALL}\index{*EX}
1.967 -\hbox{\tt !~$x$:$A$.$P[x]$} and \hbox{\tt ?~$x$:$A$.$P[x]$}.
1.968 -Isabelle's usual notation, \ttindex{ALL} and \ttindex{EX}, is also
1.969 -available. As with
1.970 -ordinary quantifiers, the contents of \ttindexbold{HOL_quantifiers} specifies
1.971 -which notation should be used for output.
1.972 +write\index{*"! symbol}\index{*"? symbol}
1.973 +\index{*ALL symbol}\index{*EX symbol}
1.974 +%
1.975 +\hbox{\tt !~$x$:$A$.$P[x]$} and \hbox{\tt ?~$x$:$A$.$P[x]$}. Isabelle's
1.976 +usual quantifier symbols, \sdx{ALL} and \sdx{EX}, are also accepted
1.977 +for input. As with the primitive quantifiers, the {\ML} reference
1.978 +\ttindex{HOL_quantifiers} specifies which notation to use for output.
1.979
1.980 Unions and intersections over sets, namely $\bigcup@{x\in A}B[x]$ and
1.981 $\bigcap@{x\in A}B[x]$, are written
1.982 -\ttindexbold{UN}~\hbox{\tt$x$:$A$.$B[x]$} and
1.983 -\ttindexbold{INT}~\hbox{\tt$x$:$A$.$B[x]$}.
1.984 -Unions and intersections over types, namely $\bigcup@x B[x]$ and
1.985 -$\bigcap@x B[x]$, are written
1.986 -\ttindexbold{UN}~\hbox{\tt$x$.$B[x]$} and
1.987 -\ttindexbold{INT}~\hbox{\tt$x$.$B[x]$}; they are equivalent to the previous
1.988 -union/intersection operators when $A$ is the universal set.
1.989 -The set of set union and intersection operators ($\bigcup A$ and $\bigcap
1.990 -A$) are not binders, but equals $\bigcup@{x\in A}x$ and $\bigcap@{x\in
1.991 - A}x$, respectively.
1.992 +\sdx{UN}~\hbox{\tt$x$:$A$.$B[x]$} and
1.993 +\sdx{INT}~\hbox{\tt$x$:$A$.$B[x]$}.
1.994
1.995 -\subsection{Axioms and rules of set theory}
1.996 -The axioms \ttindexbold{mem_Collect_eq} and
1.997 -\ttindexbold{Collect_mem_eq} assert that the functions {\tt Collect} and
1.998 -\hbox{\tt op :} are isomorphisms.
1.999 -All the other axioms are definitions; see Fig.\ts \ref{hol-set-rules}.
1.1000 -These include straightforward properties of functions: image~({\tt``}) and
1.1001 -{\tt range}, and predicates concerning monotonicity, injectiveness, etc.
1.1002 +Unions and intersections over types, namely $\bigcup@x B[x]$ and $\bigcap@x
1.1003 +B[x]$, are written \sdx{UN}~\hbox{\tt$x$.$B[x]$} and
1.1004 +\sdx{INT}~\hbox{\tt$x$.$B[x]$}. They are equivalent to the previous
1.1005 +union and intersection operators when $A$ is the universal set.
1.1006
1.1007 -\HOL's set theory has the {\ML} identifier \ttindexbold{Set.thy}.
1.1008 +The operators $\bigcup A$ and $\bigcap A$ act upon sets of sets. They are
1.1009 +not binders, but are equal to $\bigcup@{x\in A}x$ and $\bigcap@{x\in A}x$,
1.1010 +respectively.
1.1011 +
1.1012
1.1013 \begin{figure} \underscoreon
1.1014 \begin{ttbox}
1.1015 -\idx{imageI} [| x:A |] ==> f(x) : f``A
1.1016 -\idx{imageE} [| b : f``A; !!x.[| b=f(x); x:A |] ==> P |] ==> P
1.1017 +\tdx{mem_Collect_eq} (a : \{x.P(x)\}) = P(a)
1.1018 +\tdx{Collect_mem_eq} \{x.x:A\} = A
1.1019
1.1020 -\idx{rangeI} f(x) : range(f)
1.1021 -\idx{rangeE} [| b : range(f); !!x.[| b=f(x) |] ==> P |] ==> P
1.1022 +\tdx{empty_def} \{\} == \{x.x=False\}
1.1023 +\tdx{insert_def} insert(a,B) == \{x.x=a\} Un B
1.1024 +\tdx{Ball_def} Ball(A,P) == ! x. x:A --> P(x)
1.1025 +\tdx{Bex_def} Bex(A,P) == ? x. x:A & P(x)
1.1026 +\tdx{subset_def} A <= B == ! x:A. x:B
1.1027 +\tdx{Un_def} A Un B == \{x.x:A | x:B\}
1.1028 +\tdx{Int_def} A Int B == \{x.x:A & x:B\}
1.1029 +\tdx{set_diff_def} A - B == \{x.x:A & x~:B\}
1.1030 +\tdx{Compl_def} Compl(A) == \{x. ~ x:A\}
1.1031 +\tdx{INTER_def} INTER(A,B) == \{y. ! x:A. y: B(x)\}
1.1032 +\tdx{UNION_def} UNION(A,B) == \{y. ? x:A. y: B(x)\}
1.1033 +\tdx{INTER1_def} INTER1(B) == INTER(\{x.True\}, B)
1.1034 +\tdx{UNION1_def} UNION1(B) == UNION(\{x.True\}, B)
1.1035 +\tdx{Inter_def} Inter(S) == (INT x:S. x)
1.1036 +\tdx{Union_def} Union(S) == (UN x:S. x)
1.1037 +\tdx{image_def} f``A == \{y. ? x:A. y=f(x)\}
1.1038 +\tdx{range_def} range(f) == \{y. ? x. y=f(x)\}
1.1039 +\tdx{mono_def} mono(f) == !A B. A <= B --> f(A) <= f(B)
1.1040 +\tdx{inj_def} inj(f) == ! x y. f(x)=f(y) --> x=y
1.1041 +\tdx{surj_def} surj(f) == ! y. ? x. y=f(x)
1.1042 +\tdx{inj_onto_def} inj_onto(f,A) == !x:A. !y:A. f(x)=f(y) --> x=y
1.1043 +\end{ttbox}
1.1044 +\caption{Rules of the theory {\tt Set}} \label{hol-set-rules}
1.1045 +\end{figure}
1.1046
1.1047 -\idx{monoI} [| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)
1.1048 -\idx{monoD} [| mono(f); A <= B |] ==> f(A) <= f(B)
1.1049
1.1050 -\idx{injI} [| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)
1.1051 -\idx{inj_inverseI} (!!x. g(f(x)) = x) ==> inj(f)
1.1052 -\idx{injD} [| inj(f); f(x) = f(y) |] ==> x=y
1.1053 +\begin{figure} \underscoreon
1.1054 +\begin{ttbox}
1.1055 +\tdx{CollectI} [| P(a) |] ==> a : \{x.P(x)\}
1.1056 +\tdx{CollectD} [| a : \{x.P(x)\} |] ==> P(a)
1.1057 +\tdx{CollectE} [| a : \{x.P(x)\}; P(a) ==> W |] ==> W
1.1058
1.1059 -\idx{Inv_f_f} inj(f) ==> Inv(f,f(x)) = x
1.1060 -\idx{f_Inv_f} y : range(f) ==> f(Inv(f,y)) = y
1.1061 +\tdx{ballI} [| !!x. x:A ==> P(x) |] ==> ! x:A. P(x)
1.1062 +\tdx{bspec} [| ! x:A. P(x); x:A |] ==> P(x)
1.1063 +\tdx{ballE} [| ! x:A. P(x); P(x) ==> Q; ~ x:A ==> Q |] ==> Q
1.1064
1.1065 -\idx{Inv_injective}
1.1066 - [| Inv(f,x)=Inv(f,y); x: range(f); y: range(f) |] ==> x=y
1.1067 +\tdx{bexI} [| P(x); x:A |] ==> ? x:A. P(x)
1.1068 +\tdx{bexCI} [| ! x:A. ~ P(x) ==> P(a); a:A |] ==> ? x:A.P(x)
1.1069 +\tdx{bexE} [| ? x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q
1.1070 +\subcaption{Comprehension and Bounded quantifiers}
1.1071
1.1072 -\idx{inj_ontoI}
1.1073 - (!! x y. [| f(x) = f(y); x:A; y:A |] ==> x=y) ==> inj_onto(f,A)
1.1074 +\tdx{subsetI} (!!x.x:A ==> x:B) ==> A <= B
1.1075 +\tdx{subsetD} [| A <= B; c:A |] ==> c:B
1.1076 +\tdx{subsetCE} [| A <= B; ~ (c:A) ==> P; c:B ==> P |] ==> P
1.1077
1.1078 -\idx{inj_onto_inverseI}
1.1079 +\tdx{subset_refl} A <= A
1.1080 +\tdx{subset_antisym} [| A <= B; B <= A |] ==> A = B
1.1081 +\tdx{subset_trans} [| A<=B; B<=C |] ==> A<=C
1.1082 +
1.1083 +\tdx{set_ext} [| !!x. (x:A) = (x:B) |] ==> A = B
1.1084 +\tdx{equalityD1} A = B ==> A<=B
1.1085 +\tdx{equalityD2} A = B ==> B<=A
1.1086 +\tdx{equalityE} [| A = B; [| A<=B; B<=A |] ==> P |] ==> P
1.1087 +
1.1088 +\tdx{equalityCE} [| A = B; [| c:A; c:B |] ==> P;
1.1089 + [| ~ c:A; ~ c:B |] ==> P
1.1090 + |] ==> P
1.1091 +\subcaption{The subset and equality relations}
1.1092 +\end{ttbox}
1.1093 +\caption{Derived rules for set theory} \label{hol-set1}
1.1094 +\end{figure}
1.1095 +
1.1096 +
1.1097 +\begin{figure} \underscoreon
1.1098 +\begin{ttbox}
1.1099 +\tdx{emptyE} a : \{\} ==> P
1.1100 +
1.1101 +\tdx{insertI1} a : insert(a,B)
1.1102 +\tdx{insertI2} a : B ==> a : insert(b,B)
1.1103 +\tdx{insertE} [| a : insert(b,A); a=b ==> P; a:A ==> P |] ==> P
1.1104 +
1.1105 +\tdx{ComplI} [| c:A ==> False |] ==> c : Compl(A)
1.1106 +\tdx{ComplD} [| c : Compl(A) |] ==> ~ c:A
1.1107 +
1.1108 +\tdx{UnI1} c:A ==> c : A Un B
1.1109 +\tdx{UnI2} c:B ==> c : A Un B
1.1110 +\tdx{UnCI} (~c:B ==> c:A) ==> c : A Un B
1.1111 +\tdx{UnE} [| c : A Un B; c:A ==> P; c:B ==> P |] ==> P
1.1112 +
1.1113 +\tdx{IntI} [| c:A; c:B |] ==> c : A Int B
1.1114 +\tdx{IntD1} c : A Int B ==> c:A
1.1115 +\tdx{IntD2} c : A Int B ==> c:B
1.1116 +\tdx{IntE} [| c : A Int B; [| c:A; c:B |] ==> P |] ==> P
1.1117 +
1.1118 +\tdx{UN_I} [| a:A; b: B(a) |] ==> b: (UN x:A. B(x))
1.1119 +\tdx{UN_E} [| b: (UN x:A. B(x)); !!x.[| x:A; b:B(x) |] ==> R |] ==> R
1.1120 +
1.1121 +\tdx{INT_I} (!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))
1.1122 +\tdx{INT_D} [| b: (INT x:A. B(x)); a:A |] ==> b: B(a)
1.1123 +\tdx{INT_E} [| b: (INT x:A. B(x)); b: B(a) ==> R; ~ a:A ==> R |] ==> R
1.1124 +
1.1125 +\tdx{UnionI} [| X:C; A:X |] ==> A : Union(C)
1.1126 +\tdx{UnionE} [| A : Union(C); !!X.[| A:X; X:C |] ==> R |] ==> R
1.1127 +
1.1128 +\tdx{InterI} [| !!X. X:C ==> A:X |] ==> A : Inter(C)
1.1129 +\tdx{InterD} [| A : Inter(C); X:C |] ==> A:X
1.1130 +\tdx{InterE} [| A : Inter(C); A:X ==> R; ~ X:C ==> R |] ==> R
1.1131 +\end{ttbox}
1.1132 +\caption{Further derived rules for set theory} \label{hol-set2}
1.1133 +\end{figure}
1.1134 +
1.1135 +
1.1136 +\subsection{Axioms and rules of set theory}
1.1137 +Figure~\ref{hol-set-rules} presents the rules of theory \thydx{Set}. The
1.1138 +axioms \tdx{mem_Collect_eq} and \tdx{Collect_mem_eq} assert
1.1139 +that the functions {\tt Collect} and \hbox{\tt op :} are isomorphisms. Of
1.1140 +course, \hbox{\tt op :} also serves as the membership relation.
1.1141 +
1.1142 +All the other axioms are definitions. They include the empty set, bounded
1.1143 +quantifiers, unions, intersections, complements and the subset relation.
1.1144 +They also include straightforward properties of functions: image~({\tt``}) and
1.1145 +{\tt range}, and predicates concerning monotonicity, injectiveness and
1.1146 +surjectiveness.
1.1147 +
1.1148 +The predicate \cdx{inj_onto} is used for simulating type definitions.
1.1149 +The statement ${\tt inj_onto}(f,A)$ asserts that $f$ is injective on the
1.1150 +set~$A$, which specifies a subset of its domain type. In a type
1.1151 +definition, $f$ is the abstraction function and $A$ is the set of valid
1.1152 +representations; we should not expect $f$ to be injective outside of~$A$.
1.1153 +
1.1154 +\begin{figure} \underscoreon
1.1155 +\begin{ttbox}
1.1156 +\tdx{Inv_f_f} inj(f) ==> Inv(f,f(x)) = x
1.1157 +\tdx{f_Inv_f} y : range(f) ==> f(Inv(f,y)) = y
1.1158 +
1.1159 +%\tdx{Inv_injective}
1.1160 +% [| Inv(f,x)=Inv(f,y); x: range(f); y: range(f) |] ==> x=y
1.1161 +%
1.1162 +\tdx{imageI} [| x:A |] ==> f(x) : f``A
1.1163 +\tdx{imageE} [| b : f``A; !!x.[| b=f(x); x:A |] ==> P |] ==> P
1.1164 +
1.1165 +\tdx{rangeI} f(x) : range(f)
1.1166 +\tdx{rangeE} [| b : range(f); !!x.[| b=f(x) |] ==> P |] ==> P
1.1167 +
1.1168 +\tdx{monoI} [| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)
1.1169 +\tdx{monoD} [| mono(f); A <= B |] ==> f(A) <= f(B)
1.1170 +
1.1171 +\tdx{injI} [| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)
1.1172 +\tdx{inj_inverseI} (!!x. g(f(x)) = x) ==> inj(f)
1.1173 +\tdx{injD} [| inj(f); f(x) = f(y) |] ==> x=y
1.1174 +
1.1175 +\tdx{inj_ontoI} (!!x y. [| f(x)=f(y); x:A; y:A |] ==> x=y) ==> inj_onto(f,A)
1.1176 +\tdx{inj_ontoD} [| inj_onto(f,A); f(x)=f(y); x:A; y:A |] ==> x=y
1.1177 +
1.1178 +\tdx{inj_onto_inverseI}
1.1179 (!!x. x:A ==> g(f(x)) = x) ==> inj_onto(f,A)
1.1180 -
1.1181 -\idx{inj_ontoD}
1.1182 - [| inj_onto(f,A); f(x)=f(y); x:A; y:A |] ==> x=y
1.1183 -
1.1184 -\idx{inj_onto_contraD}
1.1185 +\tdx{inj_onto_contraD}
1.1186 [| inj_onto(f,A); x~=y; x:A; y:A |] ==> ~ f(x)=f(y)
1.1187 \end{ttbox}
1.1188 \caption{Derived rules involving functions} \label{hol-fun}
1.1189 @@ -779,406 +780,431 @@
1.1190
1.1191 \begin{figure} \underscoreon
1.1192 \begin{ttbox}
1.1193 -\idx{Union_upper} B:A ==> B <= Union(A)
1.1194 -\idx{Union_least} [| !!X. X:A ==> X<=C |] ==> Union(A) <= C
1.1195 +\tdx{Union_upper} B:A ==> B <= Union(A)
1.1196 +\tdx{Union_least} [| !!X. X:A ==> X<=C |] ==> Union(A) <= C
1.1197
1.1198 -\idx{Inter_lower} B:A ==> Inter(A) <= B
1.1199 -\idx{Inter_greatest} [| !!X. X:A ==> C<=X |] ==> C <= Inter(A)
1.1200 +\tdx{Inter_lower} B:A ==> Inter(A) <= B
1.1201 +\tdx{Inter_greatest} [| !!X. X:A ==> C<=X |] ==> C <= Inter(A)
1.1202
1.1203 -\idx{Un_upper1} A <= A Un B
1.1204 -\idx{Un_upper2} B <= A Un B
1.1205 -\idx{Un_least} [| A<=C; B<=C |] ==> A Un B <= C
1.1206 +\tdx{Un_upper1} A <= A Un B
1.1207 +\tdx{Un_upper2} B <= A Un B
1.1208 +\tdx{Un_least} [| A<=C; B<=C |] ==> A Un B <= C
1.1209
1.1210 -\idx{Int_lower1} A Int B <= A
1.1211 -\idx{Int_lower2} A Int B <= B
1.1212 -\idx{Int_greatest} [| C<=A; C<=B |] ==> C <= A Int B
1.1213 +\tdx{Int_lower1} A Int B <= A
1.1214 +\tdx{Int_lower2} A Int B <= B
1.1215 +\tdx{Int_greatest} [| C<=A; C<=B |] ==> C <= A Int B
1.1216 \end{ttbox}
1.1217 \caption{Derived rules involving subsets} \label{hol-subset}
1.1218 \end{figure}
1.1219
1.1220
1.1221 -\begin{figure} \underscoreon
1.1222 +\begin{figure} \underscoreon \hfuzz=4pt%suppress "Overfull \hbox" message
1.1223 \begin{ttbox}
1.1224 -\idx{Int_absorb} A Int A = A
1.1225 -\idx{Int_commute} A Int B = B Int A
1.1226 -\idx{Int_assoc} (A Int B) Int C = A Int (B Int C)
1.1227 -\idx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C)
1.1228 +\tdx{Int_absorb} A Int A = A
1.1229 +\tdx{Int_commute} A Int B = B Int A
1.1230 +\tdx{Int_assoc} (A Int B) Int C = A Int (B Int C)
1.1231 +\tdx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C)
1.1232
1.1233 -\idx{Un_absorb} A Un A = A
1.1234 -\idx{Un_commute} A Un B = B Un A
1.1235 -\idx{Un_assoc} (A Un B) Un C = A Un (B Un C)
1.1236 -\idx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C)
1.1237 +\tdx{Un_absorb} A Un A = A
1.1238 +\tdx{Un_commute} A Un B = B Un A
1.1239 +\tdx{Un_assoc} (A Un B) Un C = A Un (B Un C)
1.1240 +\tdx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C)
1.1241
1.1242 -\idx{Compl_disjoint} A Int Compl(A) = \{x.False\}
1.1243 -\idx{Compl_partition} A Un Compl(A) = \{x.True\}
1.1244 -\idx{double_complement} Compl(Compl(A)) = A
1.1245 -\idx{Compl_Un} Compl(A Un B) = Compl(A) Int Compl(B)
1.1246 -\idx{Compl_Int} Compl(A Int B) = Compl(A) Un Compl(B)
1.1247 +\tdx{Compl_disjoint} A Int Compl(A) = \{x.False\}
1.1248 +\tdx{Compl_partition} A Un Compl(A) = \{x.True\}
1.1249 +\tdx{double_complement} Compl(Compl(A)) = A
1.1250 +\tdx{Compl_Un} Compl(A Un B) = Compl(A) Int Compl(B)
1.1251 +\tdx{Compl_Int} Compl(A Int B) = Compl(A) Un Compl(B)
1.1252
1.1253 -\idx{Union_Un_distrib} Union(A Un B) = Union(A) Un Union(B)
1.1254 -\idx{Int_Union} A Int Union(B) = (UN C:B. A Int C)
1.1255 -\idx{Un_Union_image}
1.1256 - (UN x:C. A(x) Un B(x)) = Union(A``C) Un Union(B``C)
1.1257 +\tdx{Union_Un_distrib} Union(A Un B) = Union(A) Un Union(B)
1.1258 +\tdx{Int_Union} A Int Union(B) = (UN C:B. A Int C)
1.1259 +\tdx{Un_Union_image} (UN x:C. A(x) Un B(x)) = Union(A``C) Un Union(B``C)
1.1260
1.1261 -\idx{Inter_Un_distrib} Inter(A Un B) = Inter(A) Int Inter(B)
1.1262 -\idx{Un_Inter} A Un Inter(B) = (INT C:B. A Un C)
1.1263 -\idx{Int_Inter_image}
1.1264 - (INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)
1.1265 +\tdx{Inter_Un_distrib} Inter(A Un B) = Inter(A) Int Inter(B)
1.1266 +\tdx{Un_Inter} A Un Inter(B) = (INT C:B. A Un C)
1.1267 +\tdx{Int_Inter_image} (INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)
1.1268 \end{ttbox}
1.1269 \caption{Set equalities} \label{hol-equalities}
1.1270 \end{figure}
1.1271
1.1272
1.1273 -\subsection{Derived rules for sets}
1.1274 -Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules. Most
1.1275 -are obvious and resemble rules of Isabelle's {\ZF} set theory. The
1.1276 -rules named $XXX${\tt_cong} break down equalities. Certain rules, such as
1.1277 -\ttindexbold{subsetCE}, \ttindexbold{bexCI} and \ttindexbold{UnCI}, are
1.1278 -designed for classical reasoning; the more natural rules \ttindexbold{subsetD},
1.1279 -\ttindexbold{bexI}, \ttindexbold{Un1} and~\ttindexbold{Un2} are not
1.1280 -strictly necessary. Similarly, \ttindexbold{equalityCE} supports classical
1.1281 -reasoning about extensionality, after the fashion of \ttindex{iffCE}. See
1.1282 -the file {\tt HOL/set.ML} for proofs pertaining to set theory.
1.1283 +Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules. Most are
1.1284 +obvious and resemble rules of Isabelle's {\ZF} set theory. Certain rules,
1.1285 +such as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI},
1.1286 +are designed for classical reasoning; the rules \tdx{subsetD},
1.1287 +\tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are not
1.1288 +strictly necessary but yield more natural proofs. Similarly,
1.1289 +\tdx{equalityCE} supports classical reasoning about extensionality,
1.1290 +after the fashion of \tdx{iffCE}. See the file {\tt HOL/set.ML} for
1.1291 +proofs pertaining to set theory.
1.1292
1.1293 -Figure~\ref{hol-fun} presents derived inference rules involving functions. See
1.1294 -the file {\tt HOL/fun.ML} for a complete listing.
1.1295 +Figure~\ref{hol-fun} presents derived inference rules involving functions.
1.1296 +They also include rules for \cdx{Inv}, which is defined in theory~{\tt
1.1297 + HOL}; note that ${\tt Inv}(f)$ applies the Axiom of Choice to yield an
1.1298 +inverse of~$f$. They also include natural deduction rules for the image
1.1299 +and range operators, and for the predicates {\tt inj} and {\tt inj_onto}.
1.1300 +Reasoning about function composition (the operator~\sdx{o}) and the
1.1301 +predicate~\cdx{surj} is done simply by expanding the definitions. See
1.1302 +the file {\tt HOL/fun.ML} for a complete listing of the derived rules.
1.1303
1.1304 Figure~\ref{hol-subset} presents lattice properties of the subset relation.
1.1305 -See the file {\tt HOL/subset.ML}.
1.1306 +Unions form least upper bounds; non-empty intersections form greatest lower
1.1307 +bounds. Reasoning directly about subsets often yields clearer proofs than
1.1308 +reasoning about the membership relation. See the file {\tt HOL/subset.ML}.
1.1309
1.1310 -Figure~\ref{hol-equalities} presents set equalities. See
1.1311 -{\tt HOL/equalities.ML}.
1.1312 +Figure~\ref{hol-equalities} presents many common set equalities. They
1.1313 +include commutative, associative and distributive laws involving unions,
1.1314 +intersections and complements. The proofs are mostly trivial, using the
1.1315 +classical reasoner; see file {\tt HOL/equalities.ML}.
1.1316
1.1317
1.1318 \begin{figure}
1.1319 -\begin{center}
1.1320 -\begin{tabular}{rrr}
1.1321 - \it name &\it meta-type & \it description \\
1.1322 - \idx{Pair} & $[\alpha,\beta]\To \alpha\times\beta$
1.1323 - & ordered pairs $\langle a,b\rangle$ \\
1.1324 - \idx{fst} & $\alpha\times\beta \To \alpha$ & first projection\\
1.1325 - \idx{snd} & $\alpha\times\beta \To \beta$ & second projection\\
1.1326 - \idx{split} & $[\alpha\times\beta, [\alpha,\beta]\To\gamma] \To \gamma$
1.1327 - & generalized projection\\
1.1328 - \idx{Sigma} &
1.1329 +\begin{constants}
1.1330 + \cdx{Pair} & $[\alpha,\beta]\To \alpha\times\beta$
1.1331 + & & ordered pairs $\langle a,b\rangle$ \\
1.1332 + \cdx{fst} & $\alpha\times\beta \To \alpha$ & & first projection\\
1.1333 + \cdx{snd} & $\alpha\times\beta \To \beta$ & & second projection\\
1.1334 + \cdx{split} & $[\alpha\times\beta, [\alpha,\beta]\To\gamma] \To \gamma$
1.1335 + & & generalized projection\\
1.1336 + \cdx{Sigma} &
1.1337 $[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ &
1.1338 - general sum of sets
1.1339 -\end{tabular}
1.1340 -\end{center}
1.1341 -\subcaption{Constants}
1.1342 + & general sum of sets
1.1343 +\end{constants}
1.1344 +\begin{ttbox}\makeatletter
1.1345 +\tdx{fst_def} fst(p) == @a. ? b. p = <a,b>
1.1346 +\tdx{snd_def} snd(p) == @b. ? a. p = <a,b>
1.1347 +\tdx{split_def} split(p,c) == c(fst(p),snd(p))
1.1348 +\tdx{Sigma_def} Sigma(A,B) == UN x:A. UN y:B(x). \{<x,y>\}
1.1349
1.1350 -\begin{ttbox}\makeatletter
1.1351 -\idx{fst_def} fst(p) == @a. ? b. p = <a,b>
1.1352 -\idx{snd_def} snd(p) == @b. ? a. p = <a,b>
1.1353 -\idx{split_def} split(p,c) == c(fst(p),snd(p))
1.1354 -\idx{Sigma_def} Sigma(A,B) == UN x:A. UN y:B(x). \{<x,y>\}
1.1355 -\subcaption{Definitions}
1.1356
1.1357 -\idx{Pair_inject} [| <a, b> = <a',b'>; [| a=a'; b=b' |] ==> R |] ==> R
1.1358 +\tdx{Pair_inject} [| <a, b> = <a',b'>; [| a=a'; b=b' |] ==> R |] ==> R
1.1359 +\tdx{fst} fst(<a,b>) = a
1.1360 +\tdx{snd} snd(<a,b>) = b
1.1361 +\tdx{split} split(<a,b>, c) = c(a,b)
1.1362
1.1363 -\idx{fst} fst(<a,b>) = a
1.1364 -\idx{snd} snd(<a,b>) = b
1.1365 -\idx{split} split(<a,b>, c) = c(a,b)
1.1366 +\tdx{surjective_pairing} p = <fst(p),snd(p)>
1.1367
1.1368 -\idx{surjective_pairing} p = <fst(p),snd(p)>
1.1369 +\tdx{SigmaI} [| a:A; b:B(a) |] ==> <a,b> : Sigma(A,B)
1.1370
1.1371 -\idx{SigmaI} [| a:A; b:B(a) |] ==> <a,b> : Sigma(A,B)
1.1372 -
1.1373 -\idx{SigmaE} [| c: Sigma(A,B);
1.1374 +\tdx{SigmaE} [| c: Sigma(A,B);
1.1375 !!x y.[| x:A; y:B(x); c=<x,y> |] ==> P |] ==> P
1.1376 -\subcaption{Derived rules}
1.1377 \end{ttbox}
1.1378 -\caption{Type $\alpha\times\beta$}
1.1379 -\label{hol-prod}
1.1380 +\caption{Type $\alpha\times\beta$}\label{hol-prod}
1.1381 \end{figure}
1.1382
1.1383
1.1384 \begin{figure}
1.1385 -\begin{center}
1.1386 -\begin{tabular}{rrr}
1.1387 - \it name &\it meta-type & \it description \\
1.1388 - \idx{Inl} & $\alpha \To \alpha+\beta$ & first injection\\
1.1389 - \idx{Inr} & $\beta \To \alpha+\beta$ & second injection\\
1.1390 - \idx{sum_case} & $[\alpha+\beta, \alpha\To\gamma, \beta\To\gamma] \To\gamma$
1.1391 - & conditional
1.1392 -\end{tabular}
1.1393 -\end{center}
1.1394 -\subcaption{Constants}
1.1395 +\begin{constants}
1.1396 + \cdx{Inl} & $\alpha \To \alpha+\beta$ & & first injection\\
1.1397 + \cdx{Inr} & $\beta \To \alpha+\beta$ & & second injection\\
1.1398 + \cdx{sum_case} & $[\alpha+\beta, \alpha\To\gamma, \beta\To\gamma] \To\gamma$
1.1399 + & & conditional
1.1400 +\end{constants}
1.1401 +\begin{ttbox}\makeatletter
1.1402 +\tdx{sum_case_def} sum_case == (\%p f g. @z. (!x. p=Inl(x) --> z=f(x)) &
1.1403 + (!y. p=Inr(y) --> z=g(y)))
1.1404
1.1405 -\begin{ttbox}\makeatletter
1.1406 -\idx{sum_case_def} sum_case == (\%p f g. @z. (!x. p=Inl(x) --> z=f(x)) &
1.1407 - (!y. p=Inr(y) --> z=g(y)))
1.1408 -\subcaption{Definition}
1.1409 +\tdx{Inl_not_Inr} ~ Inl(a)=Inr(b)
1.1410
1.1411 -\idx{Inl_not_Inr} ~ Inl(a)=Inr(b)
1.1412 +\tdx{inj_Inl} inj(Inl)
1.1413 +\tdx{inj_Inr} inj(Inr)
1.1414
1.1415 -\idx{inj_Inl} inj(Inl)
1.1416 -\idx{inj_Inr} inj(Inr)
1.1417 +\tdx{sumE} [| !!x::'a. P(Inl(x)); !!y::'b. P(Inr(y)) |] ==> P(s)
1.1418
1.1419 -\idx{sumE} [| !!x::'a. P(Inl(x)); !!y::'b. P(Inr(y)) |] ==> P(s)
1.1420 +\tdx{sum_case_Inl} sum_case(Inl(x), f, g) = f(x)
1.1421 +\tdx{sum_case_Inr} sum_case(Inr(x), f, g) = g(x)
1.1422
1.1423 -\idx{sum_case_Inl} sum_case(Inl(x), f, g) = f(x)
1.1424 -\idx{sum_case_Inr} sum_case(Inr(x), f, g) = g(x)
1.1425 -
1.1426 -\idx{surjective_sum} sum_case(s, %x::'a. f(Inl(x)), %y::'b. f(Inr(y))) = f(s)
1.1427 -\subcaption{Derived rules}
1.1428 +\tdx{surjective_sum} sum_case(s, \%x::'a. f(Inl(x)), \%y::'b. f(Inr(y))) = f(s)
1.1429 \end{ttbox}
1.1430 -\caption{Rules for type $\alpha+\beta$}
1.1431 -\label{hol-sum}
1.1432 +\caption{Type $\alpha+\beta$}\label{hol-sum}
1.1433 \end{figure}
1.1434
1.1435
1.1436 \section{Types}
1.1437 The basic higher-order logic is augmented with a tremendous amount of
1.1438 -material, including support for recursive function and type definitions.
1.1439 -Space does not permit a detailed discussion. The present section describes
1.1440 -product, sum, natural number and list types.
1.1441 +material, including support for recursive function and type definitions. A
1.1442 +detailed discussion appears elsewhere~\cite{paulson-coind}. The simpler
1.1443 +definitions are the same as those used the {\sc hol} system, but my
1.1444 +treatment of recursive types differs from Melham's~\cite{melham89}. The
1.1445 +present section describes product, sum, natural number and list types.
1.1446
1.1447 -\subsection{Product and sum types}
1.1448 -\HOL\ defines the product type $\alpha\times\beta$ and the sum type
1.1449 -$\alpha+\beta$, with the ordered pair syntax {\tt<$a$,$b$>}, using fairly
1.1450 -standard constructions (Figs.~\ref{hol-prod} and~\ref{hol-sum}). Because
1.1451 -Isabelle does not support abstract type definitions, the isomorphisms
1.1452 -between these types and their representations are made explicitly.
1.1453 +\subsection{Product and sum types}\index{*"* type}\index{*"+ type}
1.1454 +Theory \thydx{Prod} defines the product type $\alpha\times\beta$, with
1.1455 +the ordered pair syntax {\tt<$a$,$b$>}. Theory \thydx{Sum} defines the
1.1456 +sum type $\alpha+\beta$. These use fairly standard constructions; see
1.1457 +Figs.\ts\ref{hol-prod} and~\ref{hol-sum}. Because Isabelle does not
1.1458 +support abstract type definitions, the isomorphisms between these types and
1.1459 +their representations are made explicitly.
1.1460
1.1461 Most of the definitions are suppressed, but observe that the projections
1.1462 and conditionals are defined as descriptions. Their properties are easily
1.1463 -proved using \ttindex{select_equality}. See {\tt HOL/prod.thy} and
1.1464 +proved using \tdx{select_equality}. See {\tt HOL/prod.thy} and
1.1465 {\tt HOL/sum.thy} for details.
1.1466
1.1467 \begin{figure}
1.1468 -\indexbold{*"<}
1.1469 -\begin{center}
1.1470 -\begin{tabular}{rrr}
1.1471 - \it symbol & \it meta-type & \it description \\
1.1472 - \idx{0} & $nat$ & zero \\
1.1473 - \idx{Suc} & $nat \To nat$ & successor function\\
1.1474 - \idx{nat_case} & $[nat, \alpha, nat\To\alpha] \To\alpha$
1.1475 - & conditional\\
1.1476 - \idx{nat_rec} & $[nat, \alpha, [nat, \alpha]\To\alpha] \To \alpha$
1.1477 - & primitive recursor\\
1.1478 - \idx{pred_nat} & $(nat\times nat) set$ & predecessor relation
1.1479 -\end{tabular}
1.1480 -\end{center}
1.1481 -
1.1482 -\begin{center}
1.1483 -\indexbold{*"+}
1.1484 -\index{*@{\tt*}|bold}
1.1485 -\index{/@{\tt/}|bold}
1.1486 -\index{//@{\tt//}|bold}
1.1487 -\index{+@{\tt+}|bold}
1.1488 -\index{-@{\tt-}|bold}
1.1489 -\begin{tabular}{rrrr}
1.1490 - \it symbol & \it meta-type & \it precedence & \it description \\
1.1491 +\index{*"< symbol}
1.1492 +\index{*"* symbol}
1.1493 +\index{/@{\tt/} symbol}
1.1494 +\index{//@{\tt//} symbol}
1.1495 +\index{*"+ symbol}
1.1496 +\index{*"- symbol}
1.1497 +\begin{constants}
1.1498 + \it symbol & \it meta-type & \it priority & \it description \\
1.1499 + \cdx{0} & $nat$ & & zero \\
1.1500 + \cdx{Suc} & $nat \To nat$ & & successor function\\
1.1501 + \cdx{nat_case} & $[nat, \alpha, nat\To\alpha] \To\alpha$
1.1502 + & & conditional\\
1.1503 + \cdx{nat_rec} & $[nat, \alpha, [nat, \alpha]\To\alpha] \To \alpha$
1.1504 + & & primitive recursor\\
1.1505 + \cdx{pred_nat} & $(nat\times nat) set$ & & predecessor relation\\
1.1506 \tt * & $[nat,nat]\To nat$ & Left 70 & multiplication \\
1.1507 \tt / & $[nat,nat]\To nat$ & Left 70 & division\\
1.1508 \tt // & $[nat,nat]\To nat$ & Left 70 & modulus\\
1.1509 \tt + & $[nat,nat]\To nat$ & Left 65 & addition\\
1.1510 \tt - & $[nat,nat]\To nat$ & Left 65 & subtraction
1.1511 -\end{tabular}
1.1512 -\end{center}
1.1513 +\end{constants}
1.1514 \subcaption{Constants and infixes}
1.1515
1.1516 \begin{ttbox}\makeatother
1.1517 -\idx{nat_case_def} nat_case == (\%n a f. @z. (n=0 --> z=a) &
1.1518 +\tdx{nat_case_def} nat_case == (\%n a f. @z. (n=0 --> z=a) &
1.1519 (!x. n=Suc(x) --> z=f(x)))
1.1520 -\idx{pred_nat_def} pred_nat == \{p. ? n. p = <n, Suc(n)>\}
1.1521 -\idx{less_def} m<n == <m,n>:pred_nat^+
1.1522 -\idx{nat_rec_def} nat_rec(n,c,d) ==
1.1523 +\tdx{pred_nat_def} pred_nat == \{p. ? n. p = <n, Suc(n)>\}
1.1524 +\tdx{less_def} m<n == <m,n>:pred_nat^+
1.1525 +\tdx{nat_rec_def} nat_rec(n,c,d) ==
1.1526 wfrec(pred_nat, n, \%l g.nat_case(l, c, \%m.d(m,g(m))))
1.1527
1.1528 -\idx{add_def} m+n == nat_rec(m, n, \%u v.Suc(v))
1.1529 -\idx{diff_def} m-n == nat_rec(n, m, \%u v. nat_rec(v, 0, \%x y.x))
1.1530 -\idx{mult_def} m*n == nat_rec(m, 0, \%u v. n + v)
1.1531 -\idx{mod_def} m//n == wfrec(trancl(pred_nat), m, \%j f. if(j<n,j,f(j-n)))
1.1532 -\idx{quo_def} m/n == wfrec(trancl(pred_nat),
1.1533 +\tdx{add_def} m+n == nat_rec(m, n, \%u v.Suc(v))
1.1534 +\tdx{diff_def} m-n == nat_rec(n, m, \%u v. nat_rec(v, 0, \%x y.x))
1.1535 +\tdx{mult_def} m*n == nat_rec(m, 0, \%u v. n + v)
1.1536 +\tdx{mod_def} m//n == wfrec(trancl(pred_nat), m, \%j f. if(j<n,j,f(j-n)))
1.1537 +\tdx{quo_def} m/n == wfrec(trancl(pred_nat),
1.1538 m, \%j f. if(j<n,0,Suc(f(j-n))))
1.1539 \subcaption{Definitions}
1.1540 \end{ttbox}
1.1541 -\caption{Defining $nat$, the type of natural numbers} \label{hol-nat1}
1.1542 +\caption{Defining {\tt nat}, the type of natural numbers} \label{hol-nat1}
1.1543 \end{figure}
1.1544
1.1545
1.1546 \begin{figure} \underscoreon
1.1547 \begin{ttbox}
1.1548 -\idx{nat_induct} [| P(0); !!k. [| P(k) |] ==> P(Suc(k)) |] ==> P(n)
1.1549 +\tdx{nat_induct} [| P(0); !!k. [| P(k) |] ==> P(Suc(k)) |] ==> P(n)
1.1550
1.1551 -\idx{Suc_not_Zero} Suc(m) ~= 0
1.1552 -\idx{inj_Suc} inj(Suc)
1.1553 -\idx{n_not_Suc_n} n~=Suc(n)
1.1554 +\tdx{Suc_not_Zero} Suc(m) ~= 0
1.1555 +\tdx{inj_Suc} inj(Suc)
1.1556 +\tdx{n_not_Suc_n} n~=Suc(n)
1.1557 \subcaption{Basic properties}
1.1558
1.1559 -\idx{pred_natI} <n, Suc(n)> : pred_nat
1.1560 -\idx{pred_natE}
1.1561 +\tdx{pred_natI} <n, Suc(n)> : pred_nat
1.1562 +\tdx{pred_natE}
1.1563 [| p : pred_nat; !!x n. [| p = <n, Suc(n)> |] ==> R |] ==> R
1.1564
1.1565 -\idx{nat_case_0} nat_case(0, a, f) = a
1.1566 -\idx{nat_case_Suc} nat_case(Suc(k), a, f) = f(k)
1.1567 +\tdx{nat_case_0} nat_case(0, a, f) = a
1.1568 +\tdx{nat_case_Suc} nat_case(Suc(k), a, f) = f(k)
1.1569
1.1570 -\idx{wf_pred_nat} wf(pred_nat)
1.1571 -\idx{nat_rec_0} nat_rec(0,c,h) = c
1.1572 -\idx{nat_rec_Suc} nat_rec(Suc(n), c, h) = h(n, nat_rec(n,c,h))
1.1573 +\tdx{wf_pred_nat} wf(pred_nat)
1.1574 +\tdx{nat_rec_0} nat_rec(0,c,h) = c
1.1575 +\tdx{nat_rec_Suc} nat_rec(Suc(n), c, h) = h(n, nat_rec(n,c,h))
1.1576 \subcaption{Case analysis and primitive recursion}
1.1577
1.1578 -\idx{less_trans} [| i<j; j<k |] ==> i<k
1.1579 -\idx{lessI} n < Suc(n)
1.1580 -\idx{zero_less_Suc} 0 < Suc(n)
1.1581 +\tdx{less_trans} [| i<j; j<k |] ==> i<k
1.1582 +\tdx{lessI} n < Suc(n)
1.1583 +\tdx{zero_less_Suc} 0 < Suc(n)
1.1584
1.1585 -\idx{less_not_sym} n<m --> ~ m<n
1.1586 -\idx{less_not_refl} ~ n<n
1.1587 -\idx{not_less0} ~ n<0
1.1588 +\tdx{less_not_sym} n<m --> ~ m<n
1.1589 +\tdx{less_not_refl} ~ n<n
1.1590 +\tdx{not_less0} ~ n<0
1.1591
1.1592 -\idx{Suc_less_eq} (Suc(m) < Suc(n)) = (m<n)
1.1593 -\idx{less_induct} [| !!n. [| ! m. m<n --> P(m) |] ==> P(n) |] ==> P(n)
1.1594 +\tdx{Suc_less_eq} (Suc(m) < Suc(n)) = (m<n)
1.1595 +\tdx{less_induct} [| !!n. [| ! m. m<n --> P(m) |] ==> P(n) |] ==> P(n)
1.1596
1.1597 -\idx{less_linear} m<n | m=n | n<m
1.1598 +\tdx{less_linear} m<n | m=n | n<m
1.1599 \subcaption{The less-than relation}
1.1600 \end{ttbox}
1.1601 \caption{Derived rules for~$nat$} \label{hol-nat2}
1.1602 \end{figure}
1.1603
1.1604
1.1605 -\subsection{The type of natural numbers, $nat$}
1.1606 -\HOL\ defines the natural numbers in a roundabout but traditional way.
1.1607 -The axiom of infinity postulates an type~$ind$ of individuals, which is
1.1608 -non-empty and closed under an injective operation. The natural numbers are
1.1609 -inductively generated by choosing an arbitrary individual for~0 and using
1.1610 -the injective operation to take successors. As usual, the isomorphisms
1.1611 -between~$nat$ and its representation are made explicitly.
1.1612 +\subsection{The type of natural numbers, {\tt nat}}
1.1613 +The theory \thydx{Nat} defines the natural numbers in a roundabout but
1.1614 +traditional way. The axiom of infinity postulates an type~\tydx{ind} of
1.1615 +individuals, which is non-empty and closed under an injective operation.
1.1616 +The natural numbers are inductively generated by choosing an arbitrary
1.1617 +individual for~0 and using the injective operation to take successors. As
1.1618 +usual, the isomorphisms between~$nat$ and its representation are made
1.1619 +explicitly.
1.1620
1.1621 -The definition makes use of a least fixed point operator \ttindex{lfp},
1.1622 -defined using the Knaster-Tarski theorem. This in turn defines an operator
1.1623 -\ttindex{trancl} for taking the transitive closure of a relation. See
1.1624 -files {\tt HOL/lfp.thy} and {\tt HOL/trancl.thy} for
1.1625 -details. The definition of~$nat$ resides on {\tt HOL/nat.thy}.
1.1626 +The definition makes use of a least fixed point operator \cdx{lfp},
1.1627 +defined using the Knaster-Tarski theorem. This is used to define the
1.1628 +operator \cdx{trancl}, for taking the transitive closure of a relation.
1.1629 +Primitive recursion makes use of \cdx{wfrec}, an operator for recursion
1.1630 +along arbitrary well-founded relations. The corresponding theories are
1.1631 +called {\tt Lfp}, {\tt Trancl} and {\tt WF}\@. Elsewhere I have described
1.1632 +similar constructions in the context of set theory~\cite{paulson-set-II}.
1.1633
1.1634 -Type $nat$ is postulated to belong to class~$ord$, which overloads $<$ and
1.1635 -$\leq$ on the natural numbers. As of this writing, Isabelle provides no
1.1636 -means of verifying that such overloading is sensible. On the other hand,
1.1637 -the \HOL\ theory includes no polymorphic axioms stating general properties
1.1638 -of $<$ and $\leq$.
1.1639 +Type~\tydx{nat} is postulated to belong to class~\cldx{ord}, which
1.1640 +overloads $<$ and $\leq$ on the natural numbers. As of this writing,
1.1641 +Isabelle provides no means of verifying that such overloading is sensible;
1.1642 +there is no means of specifying the operators' properties and verifying
1.1643 +that instances of the operators satisfy those properties. To be safe, the
1.1644 +\HOL\ theory includes no polymorphic axioms asserting general properties of
1.1645 +$<$ and~$\leq$.
1.1646
1.1647 -File {\tt HOL/arith.ML} develops arithmetic on the natural numbers.
1.1648 -It defines addition, multiplication, subtraction, division, and remainder,
1.1649 -proving the theorem $a \bmod b + (a/b)\times b = a$. Division and
1.1650 -remainder are defined by repeated subtraction, which requires well-founded
1.1651 -rather than primitive recursion.
1.1652 +Theory \thydx{Arith} develops arithmetic on the natural numbers. It
1.1653 +defines addition, multiplication, subtraction, division, and remainder.
1.1654 +Many of their properties are proved: commutative, associative and
1.1655 +distributive laws, identity and cancellation laws, etc. The most
1.1656 +interesting result is perhaps the theorem $a \bmod b + (a/b)\times b = a$.
1.1657 +Division and remainder are defined by repeated subtraction, which requires
1.1658 +well-founded rather than primitive recursion. See Figs.\ts\ref{hol-nat1}
1.1659 +and~\ref{hol-nat2}.
1.1660
1.1661 -Primitive recursion makes use of \ttindex{wfrec}, an operator for recursion
1.1662 -along arbitrary well-founded relations; see {\tt HOL/wf.ML} for the
1.1663 -development. The predecessor relation, \ttindexbold{pred_nat}, is shown to
1.1664 -be well-founded; recursion along this relation is primitive recursion,
1.1665 -while its transitive closure is~$<$.
1.1666 +The predecessor relation, \cdx{pred_nat}, is shown to be well-founded.
1.1667 +Recursion along this relation resembles primitive recursion, but is
1.1668 +stronger because we are in higher-order logic; using primitive recursion to
1.1669 +define a higher-order function, we can easily Ackermann's function, which
1.1670 +is not primitive recursive \cite[page~104]{thompson91}.
1.1671 +The transitive closure of \cdx{pred_nat} is~$<$. Many functions on the
1.1672 +natural numbers are most easily expressed using recursion along~$<$.
1.1673 +
1.1674 +The tactic {\tt\ttindex{nat_ind_tac} "$n$" $i$} performs induction over the
1.1675 +variable~$n$ in subgoal~$i$.
1.1676
1.1677 \begin{figure}
1.1678 -\begin{center}
1.1679 -\begin{tabular}{rrr}
1.1680 - \it symbol & \it meta-type & \it description \\
1.1681 - \idx{Nil} & $\alpha list$ & empty list\\
1.1682 - \idx{null} & $\alpha list \To bool$ & emptyness test\\
1.1683 - \idx{hd} & $\alpha list \To \alpha$ & head \\
1.1684 - \idx{tl} & $\alpha list \To \alpha list$ & tail \\
1.1685 - \idx{ttl} & $\alpha list \To \alpha list$ & total tail \\
1.1686 - \idx{map} & $(\alpha\To\beta) \To (\alpha list \To \beta list)$
1.1687 - & mapping functional\\
1.1688 - \idx{list_all}& $(\alpha \To bool) \To (\alpha list \To bool)$
1.1689 - & forall functional\\
1.1690 - \idx{filter} & $(\alpha \To bool) \To (\alpha list \To \alpha list)$
1.1691 - & filter functional\\
1.1692 - \idx{list_rec} & $[\alpha list, \beta, [\alpha ,\alpha list,
1.1693 +\index{#@{\tt\#} symbol}
1.1694 +\index{"@@{\tt\at} symbol}
1.1695 +\begin{constants}
1.1696 + \it symbol & \it meta-type & \it priority & \it description \\
1.1697 + \cdx{Nil} & $\alpha list$ & & empty list\\
1.1698 + \tt \# & $[\alpha,\alpha list]\To \alpha list$ & Right 65 &
1.1699 + list constructor \\
1.1700 + \cdx{null} & $\alpha list \To bool$ & & emptyness test\\
1.1701 + \cdx{hd} & $\alpha list \To \alpha$ & & head \\
1.1702 + \cdx{tl} & $\alpha list \To \alpha list$ & & tail \\
1.1703 + \cdx{ttl} & $\alpha list \To \alpha list$ & & total tail \\
1.1704 + \tt\at & $[\alpha list,\alpha list]\To \alpha list$ & Left 65 & append \\
1.1705 + \sdx{mem} & $[\alpha,\alpha list]\To bool$ & Left 55 & membership\\
1.1706 + \cdx{map} & $(\alpha\To\beta) \To (\alpha list \To \beta list)$
1.1707 + & & mapping functional\\
1.1708 + \cdx{filter} & $(\alpha \To bool) \To (\alpha list \To \alpha list)$
1.1709 + & & filter functional\\
1.1710 + \cdx{list_all}& $(\alpha \To bool) \To (\alpha list \To bool)$
1.1711 + & & forall functional\\
1.1712 + \cdx{list_rec} & $[\alpha list, \beta, [\alpha ,\alpha list,
1.1713 \beta]\To\beta] \To \beta$
1.1714 - & list recursor
1.1715 -\end{tabular}
1.1716 -\end{center}
1.1717 -
1.1718 -\begin{center}
1.1719 -\index{"# @{\tt\#}|bold}
1.1720 -\index{"@@{\tt\at}|bold}
1.1721 -\begin{tabular}{rrrr}
1.1722 - \it symbol & \it meta-type & \it precedence & \it description \\
1.1723 - \tt \# & $[\alpha,\alpha list]\To \alpha list$ & Right 65 & cons \\
1.1724 - \tt\at & $[\alpha list,\alpha list]\To \alpha list$ & Left 65 & append \\
1.1725 - \idx{mem} & $[\alpha,\alpha list]\To bool$ & Left 55 & membership
1.1726 -\end{tabular}
1.1727 -\end{center}
1.1728 + & & list recursor
1.1729 +\end{constants}
1.1730 \subcaption{Constants and infixes}
1.1731
1.1732 \begin{center} \tt\frenchspacing
1.1733 \begin{tabular}{rrr}
1.1734 - \it external & \it internal & \it description \\{}
1.1735 - \idx{[]} & Nil & empty list \\{}
1.1736 - [$x@1$, $\dots$, $x@n$] & $x@1$\#$\cdots$\#$x@n$\#[] &
1.1737 + \it external & \it internal & \it description \\{}
1.1738 + \sdx{[]} & Nil & \rm empty list \\{}
1.1739 + [$x@1$, $\dots$, $x@n$] & $x@1$ \# $\cdots$ \# $x@n$ \# [] &
1.1740 \rm finite list \\{}
1.1741 - [$x$:$xs$ . $P$] & filter(\%$x$.$P$,$xs$) & list comprehension\\
1.1742 - \begin{tabular}{r@{}l}
1.1743 - \idx{case} $e$ of&\ [] => $a$\\
1.1744 - |&\ $x$\#$xs$ => $b$
1.1745 - \end{tabular} & list_case($e$,$a$,\%$x~xs$.$b$)
1.1746 - & case analysis
1.1747 + [$x$:$l$. $P[x]$] & filter($\lambda x.P[x]$, $l$) &
1.1748 + \rm list comprehension
1.1749 \end{tabular}
1.1750 \end{center}
1.1751 \subcaption{Translations}
1.1752
1.1753 \begin{ttbox}
1.1754 -\idx{list_induct} [| P([]); !!x xs. [| P(xs) |] ==> P(x#xs)) |] ==> P(l)
1.1755 +\tdx{list_induct} [| P([]); !!x xs. [| P(xs) |] ==> P(x#xs)) |] ==> P(l)
1.1756
1.1757 -\idx{Cons_not_Nil} (x # xs) ~= []
1.1758 -\idx{Cons_Cons_eq} ((x # xs) = (y # ys)) = (x=y & xs=ys)
1.1759 +\tdx{Cons_not_Nil} (x # xs) ~= []
1.1760 +\tdx{Cons_Cons_eq} ((x # xs) = (y # ys)) = (x=y & xs=ys)
1.1761 \subcaption{Induction and freeness}
1.1762 \end{ttbox}
1.1763 -\caption{The type of lists and its operations} \label{hol-list}
1.1764 +\caption{The theory \thydx{List}} \label{hol-list}
1.1765 \end{figure}
1.1766
1.1767 \begin{figure}
1.1768 \begin{ttbox}\makeatother
1.1769 -list_rec([],c,h) = c list_rec(a \# l, c, h) = h(a, l, list_rec(l,c,h))
1.1770 -list_case([],c,h) = c list_case(x # xs, c, h) = h(x, xs)
1.1771 -map(f,[]) = [] map(f, x \# xs) = f(x) \# map(f,xs)
1.1772 -null([]) = True null(x # xs) = False
1.1773 -hd(x # xs) = x tl(x # xs) = xs
1.1774 -ttl([]) = [] ttl(x # xs) = xs
1.1775 -[] @ ys = ys (x # xs) \at ys = x # xs \at ys
1.1776 -x mem [] = False x mem y # ys = if(y = x, True, x mem ys)
1.1777 -filter(P, []) = [] filter(P,x#xs) = if(P(x),x#filter(P,xs),filter(P,xs))
1.1778 -list_all(P,[]) = True list_all(P, x # xs) = (P(x) & list_all(P, xs))
1.1779 +\tdx{list_rec_Nil} list_rec([],c,h) = c
1.1780 +\tdx{list_rec_Cons} list_rec(a \# l, c, h) = h(a, l, list_rec(l,c,h))
1.1781 +
1.1782 +\tdx{list_case_Nil} list_case([],c,h) = c
1.1783 +\tdx{list_case_Cons} list_case(x # xs, c, h) = h(x, xs)
1.1784 +
1.1785 +\tdx{map_Nil} map(f,[]) = []
1.1786 +\tdx{map_Cons} map(f, x \# xs) = f(x) \# map(f,xs)
1.1787 +
1.1788 +\tdx{null_Nil} null([]) = True
1.1789 +\tdx{null_Cons} null(x # xs) = False
1.1790 +
1.1791 +\tdx{hd_Cons} hd(x # xs) = x
1.1792 +\tdx{tl_Cons} tl(x # xs) = xs
1.1793 +
1.1794 +\tdx{ttl_Nil} ttl([]) = []
1.1795 +\tdx{ttl_Cons} ttl(x # xs) = xs
1.1796 +
1.1797 +\tdx{append_Nil} [] @ ys = ys
1.1798 +\tdx{append_Cons} (x # xs) \at ys = x # xs \at ys
1.1799 +
1.1800 +\tdx{mem_Nil} x mem [] = False
1.1801 +\tdx{mem_Cons} x mem y # ys = if(y = x, True, x mem ys)
1.1802 +
1.1803 +\tdx{filter_Nil} filter(P, []) = []
1.1804 +\tdx{filter_Cons} filter(P,x#xs) = if(P(x),x#filter(P,xs),filter(P,xs))
1.1805 +
1.1806 +\tdx{list_all_Nil} list_all(P,[]) = True
1.1807 +\tdx{list_all_Cons} list_all(P, x # xs) = (P(x) & list_all(P, xs))
1.1808 \end{ttbox}
1.1809 \caption{Rewrite rules for lists} \label{hol-list-simps}
1.1810 \end{figure}
1.1811
1.1812 -\subsection{The type constructor for lists, $\alpha\,list$}
1.1813 +
1.1814 +\subsection{The type constructor for lists, {\tt list}}
1.1815 +\index{*list type}
1.1816 +
1.1817 \HOL's definition of lists is an example of an experimental method for
1.1818 -handling recursive data types. The details need not concern us here; see the
1.1819 -file {\tt HOL/list.ML}. Figure~\ref{hol-list} presents the basic list
1.1820 -operations, with their types and properties. In particular,
1.1821 -\ttindexbold{list_rec} is a primitive recursion operator for lists, in the
1.1822 -style of Martin-L\"of type theory. It is derived from well-founded
1.1823 -recursion, a general principle that can express arbitrary total recursive
1.1824 -functions. The basic rewrite rules shown in Fig.~\ref{hol-list-simps} are
1.1825 -contained, together with additional useful lemmas, in the simpset {\tt
1.1826 - list_ss}. Induction over the variable $xs$ in subgoal $i$ is performed by
1.1827 -{\tt list_ind_tac "$xs$" $i$}.
1.1828 +handling recursive data types. Figure~\ref{hol-list} presents the theory
1.1829 +\thydx{List}: the basic list operations with their types and properties.
1.1830
1.1831 +The \sdx{case} construct is defined by the following translation
1.1832 +(omitted from the figure due to lack of space):
1.1833 +{\dquotes
1.1834 +\begin{eqnarray*}
1.1835 + \begin{array}[t]{r@{\;}l@{}l}
1.1836 + "case " e " of" & "[]" & " => " a\\
1.1837 + "|" & x"\#"xs & " => " b
1.1838 + \end{array}
1.1839 + & \equiv &
1.1840 + "list_case"(e, a, \lambda x\;xs.b[x,xs])
1.1841 +\end{eqnarray*}}
1.1842 +The theory includes \cdx{list_rec}, a primitive recursion operator
1.1843 +for lists. It is derived from well-founded recursion, a general principle
1.1844 +that can express arbitrary total recursive functions.
1.1845
1.1846 -\subsection{The type constructor for lazy lists, $\alpha\,llist$}
1.1847 +The simpset \ttindex{list_ss} contains, along with additional useful lemmas,
1.1848 +the basic rewrite rules that appear in Fig.\ts\ref{hol-list-simps}.
1.1849 +
1.1850 +The tactic {\tt\ttindex{list_ind_tac} "$xs$" $i$} performs induction over the
1.1851 +variable~$xs$ in subgoal~$i$.
1.1852 +
1.1853 +
1.1854 +\subsection{The type constructor for lazy lists, {\tt llist}}
1.1855 +\index{*llist type}
1.1856 +
1.1857 The definition of lazy lists demonstrates methods for handling infinite
1.1858 -data structures and co-induction in higher-order logic. It defines an
1.1859 -operator for co-recursion on lazy lists, which is used to define a few
1.1860 -simple functions such as map and append. Co-recursion cannot easily define
1.1861 +data structures and coinduction in higher-order logic. It defines an
1.1862 +operator for corecursion on lazy lists, which is used to define a few
1.1863 +simple functions such as map and append. Corecursion cannot easily define
1.1864 operations such as filter, which can compute indefinitely before yielding
1.1865 -the next element (if any!) of the lazy list. A co-induction principle is
1.1866 -defined for proving equations on lazy lists. See the files
1.1867 -{\tt HOL/llist.thy} and {\tt HOL/llist.ML} for the formal
1.1868 -derivations. I have written a report discussing the treatment of lazy
1.1869 -lists, and finite lists also~\cite{paulson-coind}.
1.1870 +the next element (if any!) of the lazy list. A coinduction principle is
1.1871 +defined for proving equations on lazy lists. See the files {\tt
1.1872 + HOL/llist.thy} and {\tt HOL/llist.ML} for the formal derivations.
1.1873 +
1.1874 +I have written a paper discussing the treatment of lazy lists; it also
1.1875 +covers finite lists~\cite{paulson-coind}.
1.1876
1.1877
1.1878 \section{Classical proof procedures} \label{hol-cla-prover}
1.1879 \HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as
1.1880 well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
1.1881 -rule (Fig.~\ref{hol-lemmas2}).
1.1882 +rule; recall Fig.\ts\ref{hol-lemmas2} above.
1.1883
1.1884 -The classical reasoning module is set up for \HOL, as the structure
1.1885 -\ttindexbold{Classical}. This structure is open, so {\ML} identifiers such
1.1886 +The classical reasoner is set up for \HOL, as the structure
1.1887 +{\tt Classical}. This structure is open, so {\ML} identifiers such
1.1888 as {\tt step_tac}, {\tt fast_tac}, {\tt best_tac}, etc., refer to it.
1.1889
1.1890 \HOL\ defines the following classical rule sets:
1.1891 @@ -1188,80 +1214,84 @@
1.1892 HOL_dup_cs : claset
1.1893 set_cs : claset
1.1894 \end{ttbox}
1.1895 -\begin{description}
1.1896 +\begin{ttdescription}
1.1897 \item[\ttindexbold{prop_cs}] contains the propositional rules, namely
1.1898 those for~$\top$, $\bot$, $\conj$, $\disj$, $\neg$, $\imp$ and~$\bimp$,
1.1899 -along with the rule~\ttindex{refl}.
1.1900 +along with the rule~{\tt refl}.
1.1901
1.1902 -\item[\ttindexbold{HOL_cs}]
1.1903 -extends {\tt prop_cs} with the safe rules \ttindex{allI} and~\ttindex{exE}
1.1904 -and the unsafe rules \ttindex{allE} and~\ttindex{exI}, as well as rules for
1.1905 -unique existence. Search using this is incomplete since quantified
1.1906 -formulae are used at most once.
1.1907 +\item[\ttindexbold{HOL_cs}] extends {\tt prop_cs} with the safe rules
1.1908 + {\tt allI} and~{\tt exE} and the unsafe rules {\tt allE}
1.1909 + and~{\tt exI}, as well as rules for unique existence. Search using
1.1910 + this classical set is incomplete: quantified formulae are used at most
1.1911 + once.
1.1912
1.1913 -\item[\ttindexbold{HOL_dup_cs}]
1.1914 -extends {\tt prop_cs} with the safe rules \ttindex{allI} and~\ttindex{exE}
1.1915 -and the unsafe rules \ttindex{all_dupE} and~\ttindex{exCI}, as well as
1.1916 -rules for unique existence. Search using this is complete --- quantified
1.1917 -formulae may be duplicated --- but frequently fails to terminate. It is
1.1918 -generally unsuitable for depth-first search.
1.1919 +\item[\ttindexbold{HOL_dup_cs}] extends {\tt prop_cs} with the safe rules
1.1920 + {\tt allI} and~{\tt exE} and the unsafe rules \tdx{all_dupE}
1.1921 + and~\tdx{exCI}, as well as rules for unique existence. Search using
1.1922 + this is complete --- quantified formulae may be duplicated --- but
1.1923 + frequently fails to terminate. It is generally unsuitable for
1.1924 + depth-first search.
1.1925
1.1926 -\item[\ttindexbold{set_cs}]
1.1927 -extends {\tt HOL_cs} with rules for the bounded quantifiers, subsets,
1.1928 -comprehensions, unions/intersections, complements, finite setes, images and
1.1929 -ranges.
1.1930 -\end{description}
1.1931 +\item[\ttindexbold{set_cs}] extends {\tt HOL_cs} with rules for the bounded
1.1932 + quantifiers, subsets, comprehensions, unions and intersections,
1.1933 + complements, finite sets, images and ranges.
1.1934 +\end{ttdescription}
1.1935 \noindent
1.1936 -See the {\em Reference Manual} for more discussion of classical proof
1.1937 -methods.
1.1938 +See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
1.1939 + {Chap.\ts\ref{chap:classical}}
1.1940 +for more discussion of classical proof methods.
1.1941
1.1942
1.1943 \section{The examples directories}
1.1944 -Directory {\tt Subst} contains Martin Coen's mechanization of a theory of
1.1945 +Directory {\tt HOL/Subst} contains Martin Coen's mechanization of a theory of
1.1946 substitutions and unifiers. It is based on Paulson's previous
1.1947 mechanization in {\LCF}~\cite{paulson85} of Manna and Waldinger's
1.1948 theory~\cite{mw81}.
1.1949
1.1950 -Directory {\tt ex} contains other examples and experimental proofs in
1.1951 -\HOL. Here is an overview of the more interesting files.
1.1952 -\begin{description}
1.1953 -\item[{\tt HOL/ex/meson.ML}]
1.1954 -contains an experimental implementation of the MESON proof procedure,
1.1955 -inspired by Plaisted~\cite{plaisted90}. It is much more powerful than
1.1956 -Isabelle's classical module.
1.1957 +Directory {\tt HOL/ex} contains other examples and experimental proofs in
1.1958 +{\HOL}. Here is an overview of the more interesting files.
1.1959 +\begin{ttdescription}
1.1960 +\item[HOL/ex/meson.ML] contains an experimental implementation of the {\sc
1.1961 + meson} proof procedure, inspired by Plaisted~\cite{plaisted90}. It is
1.1962 + much more powerful than Isabelle's classical reasoner. But it is less
1.1963 + useful in practice because it works only for pure logic; it does not
1.1964 + accept derived rules for the set theory primitives, for example.
1.1965
1.1966 -\item[{\tt HOL/ex/mesontest.ML}]
1.1967 -contains test data for the MESON proof procedure.
1.1968 +\item[HOL/ex/mesontest.ML] contains test data for the {\sc meson} proof
1.1969 + procedure. These are mostly taken from Pelletier \cite{pelletier86}.
1.1970
1.1971 -\item[{\tt HOL/ex/set.ML}]
1.1972 - proves Cantor's Theorem, which is presented below, and the
1.1973 - Schr\"oder-Bernstein Theorem.
1.1974 +\item[HOL/ex/set.ML] proves Cantor's Theorem, which is presented in
1.1975 + \S\ref{sec:hol-cantor} below, and the Schr\"oder-Bernstein Theorem.
1.1976
1.1977 -\item[{\tt HOL/ex/pl.ML}]
1.1978 -proves the soundness and completeness of classical propositional logic,
1.1979 -given a truth table semantics. The only connective is $\imp$. A
1.1980 -Hilbert-style axiom system is specified, and its set of theorems defined
1.1981 -inductively.
1.1982 +\item[HOL/ex/insort.ML] and {\tt HOL/ex/qsort.ML} contain correctness
1.1983 + proofs about insertion sort and quick sort.
1.1984
1.1985 -\item[{\tt HOL/ex/term.ML}]
1.1986 +\item[HOL/ex/pl.ML] proves the soundness and completeness of classical
1.1987 + propositional logic, given a truth table semantics. The only connective
1.1988 + is $\imp$. A Hilbert-style axiom system is specified, and its set of
1.1989 + theorems defined inductively.
1.1990 +
1.1991 +\item[HOL/ex/term.ML]
1.1992 contains proofs about an experimental recursive type definition;
1.1993 - the recursion goes through the type constructor~$list$.
1.1994 + the recursion goes through the type constructor~\tydx{list}.
1.1995
1.1996 -\item[{\tt HOL/ex/simult.ML}]
1.1997 -defines primitives for solving mutually recursive equations over sets.
1.1998 -It constructs sets of trees and forests as an example, including induction
1.1999 -and recursion rules that handle the mutual recursion.
1.2000 +\item[HOL/ex/simult.ML] defines primitives for solving mutually recursive
1.2001 + equations over sets. It constructs sets of trees and forests as an
1.2002 + example, including induction and recursion rules that handle the mutual
1.2003 + recursion.
1.2004
1.2005 -\item[{\tt HOL/ex/mt.ML}]
1.2006 -contains Jacob Frost's formalization~\cite{frost93} of a co-induction
1.2007 -example by Milner and Tofte~\cite{milner-coind}.
1.2008 -\end{description}
1.2009 +\item[HOL/ex/mt.ML] contains Jacob Frost's formalization~\cite{frost93} of
1.2010 + Milner and Tofte's coinduction example~\cite{milner-coind}. This
1.2011 + substantial proof concerns the soundness of a type system for a simple
1.2012 + functional language. The semantics of recursion is given by a cyclic
1.2013 + environment, which makes a coinductive argument appropriate.
1.2014 +\end{ttdescription}
1.2015
1.2016
1.2017 \section{Example: deriving the conjunction rules}
1.2018 -\HOL\ comes with a body of derived rules, ranging from simple properties
1.2019 -of the logical constants and set theory to well-founded recursion. Many of
1.2020 -them are worth studying.
1.2021 +The theory {\HOL} comes with a body of derived rules, ranging from simple
1.2022 +properties of the logical constants and set theory to well-founded
1.2023 +recursion. Many of them are worth studying.
1.2024
1.2025 Deriving natural deduction rules for the logical constants from their
1.2026 definitions is an archetypal example of higher-order reasoning. Let us
1.2027 @@ -1281,9 +1311,9 @@
1.2028 {\out val prems = ["P [P]", "Q [Q]"] : thm list}
1.2029 \end{ttbox}
1.2030 The next step is to unfold the definition of conjunction. But
1.2031 -\ttindex{and_def} uses \HOL's internal equality, so
1.2032 +\tdx{and_def} uses \HOL's internal equality, so
1.2033 \ttindex{rewrite_goals_tac} is unsuitable.
1.2034 -Instead, we perform substitution using the rule \ttindex{ssubst}:
1.2035 +Instead, we perform substitution using the rule \tdx{ssubst}:
1.2036 \begin{ttbox}
1.2037 by (resolve_tac [and_def RS ssubst] 1);
1.2038 {\out Level 1}
1.2039 @@ -1303,8 +1333,8 @@
1.2040 {\out 1. !!R. P --> Q --> R ==> R}
1.2041 \end{ttbox}
1.2042 The assumption is a nested implication, which may be eliminated
1.2043 -using~\ttindex{mp} resolved with itself. Elim-resolution, here, performs
1.2044 -backwards chaining. More straightforward would be to use~\ttindex{impE}
1.2045 +using~\tdx{mp} resolved with itself. Elim-resolution, here, performs
1.2046 +backwards chaining. More straightforward would be to use~\tdx{impE}
1.2047 twice.
1.2048 \index{*RS}
1.2049 \begin{ttbox}
1.2050 @@ -1335,7 +1365,7 @@
1.2051 \end{ttbox}
1.2052 Working with premises that involve defined constants can be tricky. We
1.2053 must expand the definition of conjunction in the meta-assumption $P\conj
1.2054 -Q$. The rule \ttindex{subst} performs substitution in forward proofs.
1.2055 +Q$. The rule \tdx{subst} performs substitution in forward proofs.
1.2056 We get {\it two\/} resolvents since the vacuous substitution is valid:
1.2057 \begin{ttbox}
1.2058 prems RL [and_def RS subst];
1.2059 @@ -1363,7 +1393,7 @@
1.2060 {\out 1. P --> Q --> P}
1.2061 \end{ttbox}
1.2062 The subgoal is a trivial implication. Recall that \ttindex{ares_tac} is a
1.2063 -combination of \ttindex{assume_tac} and \ttindex{resolve_tac}.
1.2064 +combination of {\tt assume_tac} and {\tt resolve_tac}.
1.2065 \begin{ttbox}
1.2066 by (REPEAT (ares_tac [impI] 1));
1.2067 {\out Level 2}
1.2068 @@ -1372,27 +1402,28 @@
1.2069 \end{ttbox}
1.2070
1.2071
1.2072 -\section{Example: Cantor's Theorem}
1.2073 +\section{Example: Cantor's Theorem}\label{sec:hol-cantor}
1.2074 Cantor's Theorem states that every set has more subsets than it has
1.2075 elements. It has become a favourite example in higher-order logic since
1.2076 it is so easily expressed:
1.2077 \[ \forall f::[\alpha,\alpha]\To bool. \exists S::\alpha\To bool.
1.2078 \forall x::\alpha. f(x) \not= S
1.2079 \]
1.2080 +%
1.2081 Viewing types as sets, $\alpha\To bool$ represents the powerset
1.2082 of~$\alpha$. This version states that for every function from $\alpha$ to
1.2083 -its powerset, some subset is outside its range.
1.2084 -The Isabelle proof uses \HOL's set theory, with the type $\alpha\,set$ and
1.2085 -the operator \ttindex{range}. Since it avoids quantification, we may
1.2086 -inspect the subset found by the proof.
1.2087 +its powerset, some subset is outside its range. The Isabelle proof uses
1.2088 +\HOL's set theory, with the type $\alpha\,set$ and the operator
1.2089 +\cdx{range}. The set~$S$ is given as an unknown instead of a
1.2090 +quantified variable so that we may inspect the subset found by the proof.
1.2091 \begin{ttbox}
1.2092 goal Set.thy "~ ?S : range(f :: 'a=>'a set)";
1.2093 {\out Level 0}
1.2094 {\out ~ ?S : range(f)}
1.2095 {\out 1. ~ ?S : range(f)}
1.2096 \end{ttbox}
1.2097 -The first two steps are routine. The rule \ttindex{rangeE} reasons that,
1.2098 -since $\Var{S}\in range(f)$, we have $\Var{S}=f(x)$ for some~$x$.
1.2099 +The first two steps are routine. The rule \tdx{rangeE} replaces
1.2100 +$\Var{S}\in {\tt range}(f)$ by $\Var{S}=f(x)$ for some~$x$.
1.2101 \begin{ttbox}
1.2102 by (resolve_tac [notI] 1);
1.2103 {\out Level 1}
1.2104 @@ -1404,7 +1435,7 @@
1.2105 {\out ~ ?S : range(f)}
1.2106 {\out 1. !!x. ?S = f(x) ==> False}
1.2107 \end{ttbox}
1.2108 -Next, we apply \ttindex{equalityCE}, reasoning that since $\Var{S}=f(x)$,
1.2109 +Next, we apply \tdx{equalityCE}, reasoning that since $\Var{S}=f(x)$,
1.2110 we have $\Var{c}\in \Var{S}$ if and only if $\Var{c}\in f(x)$ for
1.2111 any~$\Var{c}$.
1.2112 \begin{ttbox}
1.2113 @@ -1414,9 +1445,10 @@
1.2114 {\out 1. !!x. [| ?c3(x) : ?S; ?c3(x) : f(x) |] ==> False}
1.2115 {\out 2. !!x. [| ~ ?c3(x) : ?S; ~ ?c3(x) : f(x) |] ==> False}
1.2116 \end{ttbox}
1.2117 -Now we use a bit of creativity. Suppose that $\Var{S}$ has the form of a
1.2118 +Now we use a bit of creativity. Suppose that~$\Var{S}$ has the form of a
1.2119 comprehension. Then $\Var{c}\in\{x.\Var{P}(x)\}$ implies
1.2120 -$\Var{P}(\Var{c})\}$.\index{*CollectD}
1.2121 +$\Var{P}(\Var{c})$. Destruct-resolution using \tdx{CollectD}
1.2122 +instantiates~$\Var{S}$ and creates the new assumption.
1.2123 \begin{ttbox}
1.2124 by (dresolve_tac [CollectD] 1);
1.2125 {\out Level 4}
1.2126 @@ -1433,7 +1465,7 @@
1.2127 {\out ~ \{x. ~ x : f(x)\} : range(f)}
1.2128 {\out 1. !!x. [| ~ x : \{x. ~ x : f(x)\}; ~ x : f(x) |] ==> False}
1.2129 \end{ttbox}
1.2130 -The rest should be easy. To apply \ttindex{CollectI} to the negated
1.2131 +The rest should be easy. To apply \tdx{CollectI} to the negated
1.2132 assumption, we employ \ttindex{swap_res_tac}:
1.2133 \begin{ttbox}
1.2134 by (swap_res_tac [CollectI] 1);
1.2135 @@ -1448,10 +1480,11 @@
1.2136 \end{ttbox}
1.2137 How much creativity is required? As it happens, Isabelle can prove this
1.2138 theorem automatically. The classical set \ttindex{set_cs} contains rules
1.2139 -for most of the constructs of \HOL's set theory. We augment it with
1.2140 -\ttindex{equalityCE} --- set equalities are not broken up by default ---
1.2141 -and apply best-first search. Depth-first search would diverge, but
1.2142 -best-first search successfully navigates through the large search space.
1.2143 +for most of the constructs of \HOL's set theory. We must augment it with
1.2144 +\tdx{equalityCE} to break up set equalities, and then apply best-first
1.2145 +search. Depth-first search would diverge, but best-first search
1.2146 +successfully navigates through the large search space.
1.2147 +\index{search!best-first}
1.2148 \begin{ttbox}
1.2149 choplev 0;
1.2150 {\out Level 0}
1.2151 @@ -1463,3 +1496,5 @@
1.2152 {\out ~ \{x. ~ x : f(x)\} : range(f)}
1.2153 {\out No subgoals!}
1.2154 \end{ttbox}
1.2155 +
1.2156 +\index{higher-order logic|)}