1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/HOL/HOL.tex Tue May 04 18:03:56 1999 +0200
1.3 @@ -0,0 +1,2981 @@
1.4 +%% $Id$
1.5 +\chapter{Higher-Order Logic}
1.6 +\index{higher-order logic|(}
1.7 +\index{HOL system@{\sc hol} system}
1.8 +
1.9 +The theory~\thydx{HOL} implements higher-order logic. It is based on
1.10 +Gordon's~{\sc hol} system~\cite{mgordon-hol}, which itself is based on
1.11 +Church's original paper~\cite{church40}. Andrews's
1.12 +book~\cite{andrews86} is a full description of the original
1.13 +Church-style higher-order logic. Experience with the {\sc hol} system
1.14 +has demonstrated that higher-order logic is widely applicable in many
1.15 +areas of mathematics and computer science, not just hardware
1.16 +verification, {\sc hol}'s original \textit{raison d'\^etre\/}. It is
1.17 +weaker than {\ZF} set theory but for most applications this does not
1.18 +matter. If you prefer {\ML} to Lisp, you will probably prefer \HOL\
1.19 +to~{\ZF}.
1.20 +
1.21 +The syntax of \HOL\footnote{Earlier versions of Isabelle's \HOL\ used a
1.22 +different syntax. Ancient releases of Isabelle included still another version
1.23 +of~\HOL, with explicit type inference rules~\cite{paulson-COLOG}. This
1.24 +version no longer exists, but \thydx{ZF} supports a similar style of
1.25 +reasoning.} follows $\lambda$-calculus and functional programming. Function
1.26 +application is curried. To apply the function~$f$ of type
1.27 +$\tau@1\To\tau@2\To\tau@3$ to the arguments~$a$ and~$b$ in \HOL, you simply
1.28 +write $f\,a\,b$. There is no `apply' operator as in \thydx{ZF}. Note that
1.29 +$f(a,b)$ means ``$f$ applied to the pair $(a,b)$'' in \HOL. We write ordered
1.30 +pairs as $(a,b)$, not $\langle a,b\rangle$ as in {\ZF}.
1.31 +
1.32 +\HOL\ has a distinct feel, compared with {\ZF} and {\CTT}. It
1.33 +identifies object-level types with meta-level types, taking advantage of
1.34 +Isabelle's built-in type-checker. It identifies object-level functions
1.35 +with meta-level functions, so it uses Isabelle's operations for abstraction
1.36 +and application.
1.37 +
1.38 +These identifications allow Isabelle to support \HOL\ particularly
1.39 +nicely, but they also mean that \HOL\ requires more sophistication
1.40 +from the user --- in particular, an understanding of Isabelle's type
1.41 +system. Beginners should work with \texttt{show_types} (or even
1.42 +\texttt{show_sorts}) set to \texttt{true}.
1.43 +% Gain experience by
1.44 +%working in first-order logic before attempting to use higher-order logic.
1.45 +%This chapter assumes familiarity with~{\FOL{}}.
1.46 +
1.47 +
1.48 +\begin{figure}
1.49 +\begin{constants}
1.50 + \it name &\it meta-type & \it description \\
1.51 + \cdx{Trueprop}& $bool\To prop$ & coercion to $prop$\\
1.52 + \cdx{Not} & $bool\To bool$ & negation ($\neg$) \\
1.53 + \cdx{True} & $bool$ & tautology ($\top$) \\
1.54 + \cdx{False} & $bool$ & absurdity ($\bot$) \\
1.55 + \cdx{If} & $[bool,\alpha,\alpha]\To\alpha$ & conditional \\
1.56 + \cdx{Let} & $[\alpha,\alpha\To\beta]\To\beta$ & let binder
1.57 +\end{constants}
1.58 +\subcaption{Constants}
1.59 +
1.60 +\begin{constants}
1.61 +\index{"@@{\tt\at} symbol}
1.62 +\index{*"! symbol}\index{*"? symbol}
1.63 +\index{*"?"! symbol}\index{*"E"X"! symbol}
1.64 + \it symbol &\it name &\it meta-type & \it description \\
1.65 + \tt\at & \cdx{Eps} & $(\alpha\To bool)\To\alpha$ &
1.66 + Hilbert description ($\varepsilon$) \\
1.67 + {\tt!~} or \sdx{ALL} & \cdx{All} & $(\alpha\To bool)\To bool$ &
1.68 + universal quantifier ($\forall$) \\
1.69 + {\tt?~} or \sdx{EX} & \cdx{Ex} & $(\alpha\To bool)\To bool$ &
1.70 + existential quantifier ($\exists$) \\
1.71 + {\tt?!} or \texttt{EX!} & \cdx{Ex1} & $(\alpha\To bool)\To bool$ &
1.72 + unique existence ($\exists!$)\\
1.73 + \texttt{LEAST} & \cdx{Least} & $(\alpha::ord \To bool)\To\alpha$ &
1.74 + least element
1.75 +\end{constants}
1.76 +\subcaption{Binders}
1.77 +
1.78 +\begin{constants}
1.79 +\index{*"= symbol}
1.80 +\index{&@{\tt\&} symbol}
1.81 +\index{*"| symbol}
1.82 +\index{*"-"-"> symbol}
1.83 + \it symbol & \it meta-type & \it priority & \it description \\
1.84 + \sdx{o} & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ &
1.85 + Left 55 & composition ($\circ$) \\
1.86 + \tt = & $[\alpha,\alpha]\To bool$ & Left 50 & equality ($=$) \\
1.87 + \tt < & $[\alpha::ord,\alpha]\To bool$ & Left 50 & less than ($<$) \\
1.88 + \tt <= & $[\alpha::ord,\alpha]\To bool$ & Left 50 &
1.89 + less than or equals ($\leq$)\\
1.90 + \tt \& & $[bool,bool]\To bool$ & Right 35 & conjunction ($\conj$) \\
1.91 + \tt | & $[bool,bool]\To bool$ & Right 30 & disjunction ($\disj$) \\
1.92 + \tt --> & $[bool,bool]\To bool$ & Right 25 & implication ($\imp$)
1.93 +\end{constants}
1.94 +\subcaption{Infixes}
1.95 +\caption{Syntax of \texttt{HOL}} \label{hol-constants}
1.96 +\end{figure}
1.97 +
1.98 +
1.99 +\begin{figure}
1.100 +\index{*let symbol}
1.101 +\index{*in symbol}
1.102 +\dquotes
1.103 +\[\begin{array}{rclcl}
1.104 + term & = & \hbox{expression of class~$term$} \\
1.105 + & | & "\at~" id " . " formula \\
1.106 + & | &
1.107 + \multicolumn{3}{l}{"let"~id~"="~term";"\dots";"~id~"="~term~"in"~term} \\
1.108 + & | &
1.109 + \multicolumn{3}{l}{"if"~formula~"then"~term~"else"~term} \\
1.110 + & | & "LEAST"~ id " . " formula \\[2ex]
1.111 + formula & = & \hbox{expression of type~$bool$} \\
1.112 + & | & term " = " term \\
1.113 + & | & term " \ttilde= " term \\
1.114 + & | & term " < " term \\
1.115 + & | & term " <= " term \\
1.116 + & | & "\ttilde\ " formula \\
1.117 + & | & formula " \& " formula \\
1.118 + & | & formula " | " formula \\
1.119 + & | & formula " --> " formula \\
1.120 + & | & "!~~~" id~id^* " . " formula
1.121 + & | & "ALL~" id~id^* " . " formula \\
1.122 + & | & "?~~~" id~id^* " . " formula
1.123 + & | & "EX~~" id~id^* " . " formula \\
1.124 + & | & "?!~~" id~id^* " . " formula
1.125 + & | & "EX!~" id~id^* " . " formula
1.126 + \end{array}
1.127 +\]
1.128 +\caption{Full grammar for \HOL} \label{hol-grammar}
1.129 +\end{figure}
1.130 +
1.131 +
1.132 +\section{Syntax}
1.133 +
1.134 +Figure~\ref{hol-constants} lists the constants (including infixes and
1.135 +binders), while Fig.\ts\ref{hol-grammar} presents the grammar of
1.136 +higher-order logic. Note that $a$\verb|~=|$b$ is translated to
1.137 +$\neg(a=b)$.
1.138 +
1.139 +\begin{warn}
1.140 + \HOL\ has no if-and-only-if connective; logical equivalence is expressed
1.141 + using equality. But equality has a high priority, as befitting a
1.142 + relation, while if-and-only-if typically has the lowest priority. Thus,
1.143 + $\neg\neg P=P$ abbreviates $\neg\neg (P=P)$ and not $(\neg\neg P)=P$.
1.144 + When using $=$ to mean logical equivalence, enclose both operands in
1.145 + parentheses.
1.146 +\end{warn}
1.147 +
1.148 +\subsection{Types and classes}
1.149 +The universal type class of higher-order terms is called~\cldx{term}.
1.150 +By default, explicit type variables have class \cldx{term}. In
1.151 +particular the equality symbol and quantifiers are polymorphic over
1.152 +class \texttt{term}.
1.153 +
1.154 +The type of formulae, \tydx{bool}, belongs to class \cldx{term}; thus,
1.155 +formulae are terms. The built-in type~\tydx{fun}, which constructs
1.156 +function types, is overloaded with arity {\tt(term,\thinspace
1.157 + term)\thinspace term}. Thus, $\sigma\To\tau$ belongs to class~{\tt
1.158 + term} if $\sigma$ and~$\tau$ do, allowing quantification over
1.159 +functions.
1.160 +
1.161 +\HOL\ offers various methods for introducing new types.
1.162 +See~\S\ref{sec:HOL:Types} and~\S\ref{sec:HOL:datatype}.
1.163 +
1.164 +Theory \thydx{Ord} defines the syntactic class \cldx{ord} of order
1.165 +signatures; the relations $<$ and $\leq$ are polymorphic over this
1.166 +class, as are the functions \cdx{mono}, \cdx{min} and \cdx{max}, and
1.167 +the \cdx{LEAST} operator. \thydx{Ord} also defines a subclass
1.168 +\cldx{order} of \cldx{ord} which axiomatizes partially ordered types
1.169 +(w.r.t.\ $\le$).
1.170 +
1.171 +Three other syntactic type classes --- \cldx{plus}, \cldx{minus} and
1.172 +\cldx{times} --- permit overloading of the operators {\tt+},\index{*"+
1.173 + symbol} {\tt-}\index{*"- symbol} and {\tt*}.\index{*"* symbol} In
1.174 +particular, {\tt-} is instantiated for set difference and subtraction
1.175 +on natural numbers.
1.176 +
1.177 +If you state a goal containing overloaded functions, you may need to include
1.178 +type constraints. Type inference may otherwise make the goal more
1.179 +polymorphic than you intended, with confusing results. For example, the
1.180 +variables $i$, $j$ and $k$ in the goal $i \le j \Imp i \le j+k$ have type
1.181 +$\alpha::\{ord,plus\}$, although you may have expected them to have some
1.182 +numeric type, e.g. $nat$. Instead you should have stated the goal as
1.183 +$(i::nat) \le j \Imp i \le j+k$, which causes all three variables to have
1.184 +type $nat$.
1.185 +
1.186 +\begin{warn}
1.187 + If resolution fails for no obvious reason, try setting
1.188 + \ttindex{show_types} to \texttt{true}, causing Isabelle to display
1.189 + types of terms. Possibly set \ttindex{show_sorts} to \texttt{true} as
1.190 + well, causing Isabelle to display type classes and sorts.
1.191 +
1.192 + \index{unification!incompleteness of}
1.193 + Where function types are involved, Isabelle's unification code does not
1.194 + guarantee to find instantiations for type variables automatically. Be
1.195 + prepared to use \ttindex{res_inst_tac} instead of \texttt{resolve_tac},
1.196 + possibly instantiating type variables. Setting
1.197 + \ttindex{Unify.trace_types} to \texttt{true} causes Isabelle to report
1.198 + omitted search paths during unification.\index{tracing!of unification}
1.199 +\end{warn}
1.200 +
1.201 +
1.202 +\subsection{Binders}
1.203 +
1.204 +Hilbert's {\bf description} operator~$\varepsilon x. P[x]$ stands for
1.205 +some~$x$ satisfying~$P$, if such exists. Since all terms in \HOL\
1.206 +denote something, a description is always meaningful, but we do not
1.207 +know its value unless $P$ defines it uniquely. We may write
1.208 +descriptions as \cdx{Eps}($\lambda x. P[x]$) or use the syntax
1.209 +\hbox{\tt \at $x$.\ $P[x]$}.
1.210 +
1.211 +Existential quantification is defined by
1.212 +\[ \exists x. P~x \;\equiv\; P(\varepsilon x. P~x). \]
1.213 +The unique existence quantifier, $\exists!x. P$, is defined in terms
1.214 +of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested
1.215 +quantifications. For instance, $\exists!x\,y. P\,x\,y$ abbreviates
1.216 +$\exists!x. \exists!y. P\,x\,y$; note that this does not mean that there
1.217 +exists a unique pair $(x,y)$ satisfying~$P\,x\,y$.
1.218 +
1.219 +\index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system}
1.220 +Quantifiers have two notations. As in Gordon's {\sc hol} system, \HOL\
1.221 +uses~{\tt!}\ and~{\tt?}\ to stand for $\forall$ and $\exists$. The
1.222 +existential quantifier must be followed by a space; thus {\tt?x} is an
1.223 +unknown, while \verb'? x. f x=y' is a quantification. Isabelle's usual
1.224 +notation for quantifiers, \sdx{ALL} and \sdx{EX}, is also
1.225 +available. Both notations are accepted for input. The {\ML} reference
1.226 +\ttindexbold{HOL_quantifiers} governs the output notation. If set to {\tt
1.227 +true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default. If set
1.228 +to \texttt{false}, then~\texttt{ALL} and~\texttt{EX} are displayed.
1.229 +
1.230 +If $\tau$ is a type of class \cldx{ord}, $P$ a formula and $x$ a
1.231 +variable of type $\tau$, then the term \cdx{LEAST}~$x. P[x]$ is defined
1.232 +to be the least (w.r.t.\ $\le$) $x$ such that $P~x$ holds (see
1.233 +Fig.~\ref{hol-defs}). The definition uses Hilbert's $\varepsilon$
1.234 +choice operator, so \texttt{Least} is always meaningful, but may yield
1.235 +nothing useful in case there is not a unique least element satisfying
1.236 +$P$.\footnote{Class $ord$ does not require much of its instances, so
1.237 + $\le$ need not be a well-ordering, not even an order at all!}
1.238 +
1.239 +\medskip All these binders have priority 10.
1.240 +
1.241 +\begin{warn}
1.242 +The low priority of binders means that they need to be enclosed in
1.243 +parenthesis when they occur in the context of other operations. For example,
1.244 +instead of $P \land \forall x. Q$ you need to write $P \land (\forall x. Q)$.
1.245 +\end{warn}
1.246 +
1.247 +
1.248 +\subsection{The \sdx{let} and \sdx{case} constructions}
1.249 +Local abbreviations can be introduced by a \texttt{let} construct whose
1.250 +syntax appears in Fig.\ts\ref{hol-grammar}. Internally it is translated into
1.251 +the constant~\cdx{Let}. It can be expanded by rewriting with its
1.252 +definition, \tdx{Let_def}.
1.253 +
1.254 +\HOL\ also defines the basic syntax
1.255 +\[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n\]
1.256 +as a uniform means of expressing \texttt{case} constructs. Therefore \texttt{case}
1.257 +and \sdx{of} are reserved words. Initially, this is mere syntax and has no
1.258 +logical meaning. By declaring translations, you can cause instances of the
1.259 +\texttt{case} construct to denote applications of particular case operators.
1.260 +This is what happens automatically for each \texttt{datatype} definition
1.261 +(see~\S\ref{sec:HOL:datatype}).
1.262 +
1.263 +\begin{warn}
1.264 +Both \texttt{if} and \texttt{case} constructs have as low a priority as
1.265 +quantifiers, which requires additional enclosing parentheses in the context
1.266 +of most other operations. For example, instead of $f~x = {\tt if\dots
1.267 +then\dots else}\dots$ you need to write $f~x = ({\tt if\dots then\dots
1.268 +else\dots})$.
1.269 +\end{warn}
1.270 +
1.271 +\section{Rules of inference}
1.272 +
1.273 +\begin{figure}
1.274 +\begin{ttbox}\makeatother
1.275 +\tdx{refl} t = (t::'a)
1.276 +\tdx{subst} [| s = t; P s |] ==> P (t::'a)
1.277 +\tdx{ext} (!!x::'a. (f x :: 'b) = g x) ==> (\%x. f x) = (\%x. g x)
1.278 +\tdx{impI} (P ==> Q) ==> P-->Q
1.279 +\tdx{mp} [| P-->Q; P |] ==> Q
1.280 +\tdx{iff} (P-->Q) --> (Q-->P) --> (P=Q)
1.281 +\tdx{selectI} P(x::'a) ==> P(@x. P x)
1.282 +\tdx{True_or_False} (P=True) | (P=False)
1.283 +\end{ttbox}
1.284 +\caption{The \texttt{HOL} rules} \label{hol-rules}
1.285 +\end{figure}
1.286 +
1.287 +Figure~\ref{hol-rules} shows the primitive inference rules of~\HOL{},
1.288 +with their~{\ML} names. Some of the rules deserve additional
1.289 +comments:
1.290 +\begin{ttdescription}
1.291 +\item[\tdx{ext}] expresses extensionality of functions.
1.292 +\item[\tdx{iff}] asserts that logically equivalent formulae are
1.293 + equal.
1.294 +\item[\tdx{selectI}] gives the defining property of the Hilbert
1.295 + $\varepsilon$-operator. It is a form of the Axiom of Choice. The derived rule
1.296 + \tdx{select_equality} (see below) is often easier to use.
1.297 +\item[\tdx{True_or_False}] makes the logic classical.\footnote{In
1.298 + fact, the $\varepsilon$-operator already makes the logic classical, as
1.299 + shown by Diaconescu; see Paulson~\cite{paulson-COLOG} for details.}
1.300 +\end{ttdescription}
1.301 +
1.302 +
1.303 +\begin{figure}\hfuzz=4pt%suppress "Overfull \hbox" message
1.304 +\begin{ttbox}\makeatother
1.305 +\tdx{True_def} True == ((\%x::bool. x)=(\%x. x))
1.306 +\tdx{All_def} All == (\%P. P = (\%x. True))
1.307 +\tdx{Ex_def} Ex == (\%P. P(@x. P x))
1.308 +\tdx{False_def} False == (!P. P)
1.309 +\tdx{not_def} not == (\%P. P-->False)
1.310 +\tdx{and_def} op & == (\%P Q. !R. (P-->Q-->R) --> R)
1.311 +\tdx{or_def} op | == (\%P Q. !R. (P-->R) --> (Q-->R) --> R)
1.312 +\tdx{Ex1_def} Ex1 == (\%P. ? x. P x & (! y. P y --> y=x))
1.313 +
1.314 +\tdx{o_def} op o == (\%(f::'b=>'c) g x::'a. f(g x))
1.315 +\tdx{if_def} If P x y ==
1.316 + (\%P x y. @z::'a.(P=True --> z=x) & (P=False --> z=y))
1.317 +\tdx{Let_def} Let s f == f s
1.318 +\tdx{Least_def} Least P == @x. P(x) & (ALL y. P(y) --> x <= y)"
1.319 +\end{ttbox}
1.320 +\caption{The \texttt{HOL} definitions} \label{hol-defs}
1.321 +\end{figure}
1.322 +
1.323 +
1.324 +\HOL{} follows standard practice in higher-order logic: only a few
1.325 +connectives are taken as primitive, with the remainder defined obscurely
1.326 +(Fig.\ts\ref{hol-defs}). Gordon's {\sc hol} system expresses the
1.327 +corresponding definitions \cite[page~270]{mgordon-hol} using
1.328 +object-equality~({\tt=}), which is possible because equality in
1.329 +higher-order logic may equate formulae and even functions over formulae.
1.330 +But theory~\HOL{}, like all other Isabelle theories, uses
1.331 +meta-equality~({\tt==}) for definitions.
1.332 +\begin{warn}
1.333 +The definitions above should never be expanded and are shown for completeness
1.334 +only. Instead users should reason in terms of the derived rules shown below
1.335 +or, better still, using high-level tactics
1.336 +(see~\S\ref{sec:HOL:generic-packages}).
1.337 +\end{warn}
1.338 +
1.339 +Some of the rules mention type variables; for example, \texttt{refl}
1.340 +mentions the type variable~{\tt'a}. This allows you to instantiate
1.341 +type variables explicitly by calling \texttt{res_inst_tac}.
1.342 +
1.343 +
1.344 +\begin{figure}
1.345 +\begin{ttbox}
1.346 +\tdx{sym} s=t ==> t=s
1.347 +\tdx{trans} [| r=s; s=t |] ==> r=t
1.348 +\tdx{ssubst} [| t=s; P s |] ==> P t
1.349 +\tdx{box_equals} [| a=b; a=c; b=d |] ==> c=d
1.350 +\tdx{arg_cong} x = y ==> f x = f y
1.351 +\tdx{fun_cong} f = g ==> f x = g x
1.352 +\tdx{cong} [| f = g; x = y |] ==> f x = g y
1.353 +\tdx{not_sym} t ~= s ==> s ~= t
1.354 +\subcaption{Equality}
1.355 +
1.356 +\tdx{TrueI} True
1.357 +\tdx{FalseE} False ==> P
1.358 +
1.359 +\tdx{conjI} [| P; Q |] ==> P&Q
1.360 +\tdx{conjunct1} [| P&Q |] ==> P
1.361 +\tdx{conjunct2} [| P&Q |] ==> Q
1.362 +\tdx{conjE} [| P&Q; [| P; Q |] ==> R |] ==> R
1.363 +
1.364 +\tdx{disjI1} P ==> P|Q
1.365 +\tdx{disjI2} Q ==> P|Q
1.366 +\tdx{disjE} [| P | Q; P ==> R; Q ==> R |] ==> R
1.367 +
1.368 +\tdx{notI} (P ==> False) ==> ~ P
1.369 +\tdx{notE} [| ~ P; P |] ==> R
1.370 +\tdx{impE} [| P-->Q; P; Q ==> R |] ==> R
1.371 +\subcaption{Propositional logic}
1.372 +
1.373 +\tdx{iffI} [| P ==> Q; Q ==> P |] ==> P=Q
1.374 +\tdx{iffD1} [| P=Q; P |] ==> Q
1.375 +\tdx{iffD2} [| P=Q; Q |] ==> P
1.376 +\tdx{iffE} [| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R
1.377 +%
1.378 +%\tdx{eqTrueI} P ==> P=True
1.379 +%\tdx{eqTrueE} P=True ==> P
1.380 +\subcaption{Logical equivalence}
1.381 +
1.382 +\end{ttbox}
1.383 +\caption{Derived rules for \HOL} \label{hol-lemmas1}
1.384 +\end{figure}
1.385 +
1.386 +
1.387 +\begin{figure}
1.388 +\begin{ttbox}\makeatother
1.389 +\tdx{allI} (!!x. P x) ==> !x. P x
1.390 +\tdx{spec} !x. P x ==> P x
1.391 +\tdx{allE} [| !x. P x; P x ==> R |] ==> R
1.392 +\tdx{all_dupE} [| !x. P x; [| P x; !x. P x |] ==> R |] ==> R
1.393 +
1.394 +\tdx{exI} P x ==> ? x. P x
1.395 +\tdx{exE} [| ? x. P x; !!x. P x ==> Q |] ==> Q
1.396 +
1.397 +\tdx{ex1I} [| P a; !!x. P x ==> x=a |] ==> ?! x. P x
1.398 +\tdx{ex1E} [| ?! x. P x; !!x. [| P x; ! y. P y --> y=x |] ==> R
1.399 + |] ==> R
1.400 +
1.401 +\tdx{select_equality} [| P a; !!x. P x ==> x=a |] ==> (@x. P x) = a
1.402 +\subcaption{Quantifiers and descriptions}
1.403 +
1.404 +\tdx{ccontr} (~P ==> False) ==> P
1.405 +\tdx{classical} (~P ==> P) ==> P
1.406 +\tdx{excluded_middle} ~P | P
1.407 +
1.408 +\tdx{disjCI} (~Q ==> P) ==> P|Q
1.409 +\tdx{exCI} (! x. ~ P x ==> P a) ==> ? x. P x
1.410 +\tdx{impCE} [| P-->Q; ~ P ==> R; Q ==> R |] ==> R
1.411 +\tdx{iffCE} [| P=Q; [| P;Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R
1.412 +\tdx{notnotD} ~~P ==> P
1.413 +\tdx{swap} ~P ==> (~Q ==> P) ==> Q
1.414 +\subcaption{Classical logic}
1.415 +
1.416 +%\tdx{if_True} (if True then x else y) = x
1.417 +%\tdx{if_False} (if False then x else y) = y
1.418 +\tdx{if_P} P ==> (if P then x else y) = x
1.419 +\tdx{if_not_P} ~ P ==> (if P then x else y) = y
1.420 +\tdx{split_if} P(if Q then x else y) = ((Q --> P x) & (~Q --> P y))
1.421 +\subcaption{Conditionals}
1.422 +\end{ttbox}
1.423 +\caption{More derived rules} \label{hol-lemmas2}
1.424 +\end{figure}
1.425 +
1.426 +Some derived rules are shown in Figures~\ref{hol-lemmas1}
1.427 +and~\ref{hol-lemmas2}, with their {\ML} names. These include natural rules
1.428 +for the logical connectives, as well as sequent-style elimination rules for
1.429 +conjunctions, implications, and universal quantifiers.
1.430 +
1.431 +Note the equality rules: \tdx{ssubst} performs substitution in
1.432 +backward proofs, while \tdx{box_equals} supports reasoning by
1.433 +simplifying both sides of an equation.
1.434 +
1.435 +The following simple tactics are occasionally useful:
1.436 +\begin{ttdescription}
1.437 +\item[\ttindexbold{strip_tac} $i$] applies \texttt{allI} and \texttt{impI}
1.438 + repeatedly to remove all outermost universal quantifiers and implications
1.439 + from subgoal $i$.
1.440 +\item[\ttindexbold{case_tac} {\tt"}$P${\tt"} $i$] performs case distinction
1.441 + on $P$ for subgoal $i$: the latter is replaced by two identical subgoals
1.442 + with the added assumptions $P$ and $\neg P$, respectively.
1.443 +\end{ttdescription}
1.444 +
1.445 +
1.446 +\begin{figure}
1.447 +\begin{center}
1.448 +\begin{tabular}{rrr}
1.449 + \it name &\it meta-type & \it description \\
1.450 +\index{{}@\verb'{}' symbol}
1.451 + \verb|{}| & $\alpha\,set$ & the empty set \\
1.452 + \cdx{insert} & $[\alpha,\alpha\,set]\To \alpha\,set$
1.453 + & insertion of element \\
1.454 + \cdx{Collect} & $(\alpha\To bool)\To\alpha\,set$
1.455 + & comprehension \\
1.456 + \cdx{Compl} & $\alpha\,set\To\alpha\,set$
1.457 + & complement \\
1.458 + \cdx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
1.459 + & intersection over a set\\
1.460 + \cdx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
1.461 + & union over a set\\
1.462 + \cdx{Inter} & $(\alpha\,set)set\To\alpha\,set$
1.463 + &set of sets intersection \\
1.464 + \cdx{Union} & $(\alpha\,set)set\To\alpha\,set$
1.465 + &set of sets union \\
1.466 + \cdx{Pow} & $\alpha\,set \To (\alpha\,set)set$
1.467 + & powerset \\[1ex]
1.468 + \cdx{range} & $(\alpha\To\beta )\To\beta\,set$
1.469 + & range of a function \\[1ex]
1.470 + \cdx{Ball}~~\cdx{Bex} & $[\alpha\,set,\alpha\To bool]\To bool$
1.471 + & bounded quantifiers
1.472 +\end{tabular}
1.473 +\end{center}
1.474 +\subcaption{Constants}
1.475 +
1.476 +\begin{center}
1.477 +\begin{tabular}{llrrr}
1.478 + \it symbol &\it name &\it meta-type & \it priority & \it description \\
1.479 + \sdx{INT} & \cdx{INTER1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 &
1.480 + intersection over a type\\
1.481 + \sdx{UN} & \cdx{UNION1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 &
1.482 + union over a type
1.483 +\end{tabular}
1.484 +\end{center}
1.485 +\subcaption{Binders}
1.486 +
1.487 +\begin{center}
1.488 +\index{*"`"` symbol}
1.489 +\index{*": symbol}
1.490 +\index{*"<"= symbol}
1.491 +\begin{tabular}{rrrr}
1.492 + \it symbol & \it meta-type & \it priority & \it description \\
1.493 + \tt `` & $[\alpha\To\beta ,\alpha\,set]\To \beta\,set$
1.494 + & Left 90 & image \\
1.495 + \sdx{Int} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$
1.496 + & Left 70 & intersection ($\int$) \\
1.497 + \sdx{Un} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$
1.498 + & Left 65 & union ($\un$) \\
1.499 + \tt: & $[\alpha ,\alpha\,set]\To bool$
1.500 + & Left 50 & membership ($\in$) \\
1.501 + \tt <= & $[\alpha\,set,\alpha\,set]\To bool$
1.502 + & Left 50 & subset ($\subseteq$)
1.503 +\end{tabular}
1.504 +\end{center}
1.505 +\subcaption{Infixes}
1.506 +\caption{Syntax of the theory \texttt{Set}} \label{hol-set-syntax}
1.507 +\end{figure}
1.508 +
1.509 +
1.510 +\begin{figure}
1.511 +\begin{center} \tt\frenchspacing
1.512 +\index{*"! symbol}
1.513 +\begin{tabular}{rrr}
1.514 + \it external & \it internal & \it description \\
1.515 + $a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm non-membership\\
1.516 + {\ttlbrace}$a@1$, $\ldots${\ttrbrace} & insert $a@1$ $\ldots$ {\ttlbrace}{\ttrbrace} & \rm finite set \\
1.517 + {\ttlbrace}$x$. $P[x]${\ttrbrace} & Collect($\lambda x. P[x]$) &
1.518 + \rm comprehension \\
1.519 + \sdx{INT} $x$:$A$. $B[x]$ & INTER $A$ $\lambda x. B[x]$ &
1.520 + \rm intersection \\
1.521 + \sdx{UN}{\tt\ } $x$:$A$. $B[x]$ & UNION $A$ $\lambda x. B[x]$ &
1.522 + \rm union \\
1.523 + \tt ! $x$:$A$. $P[x]$ or \sdx{ALL} $x$:$A$. $P[x]$ &
1.524 + Ball $A$ $\lambda x. P[x]$ &
1.525 + \rm bounded $\forall$ \\
1.526 + \sdx{?} $x$:$A$. $P[x]$ or \sdx{EX}{\tt\ } $x$:$A$. $P[x]$ &
1.527 + Bex $A$ $\lambda x. P[x]$ & \rm bounded $\exists$
1.528 +\end{tabular}
1.529 +\end{center}
1.530 +\subcaption{Translations}
1.531 +
1.532 +\dquotes
1.533 +\[\begin{array}{rclcl}
1.534 + term & = & \hbox{other terms\ldots} \\
1.535 + & | & "{\ttlbrace}{\ttrbrace}" \\
1.536 + & | & "{\ttlbrace} " term\; ("," term)^* " {\ttrbrace}" \\
1.537 + & | & "{\ttlbrace} " id " . " formula " {\ttrbrace}" \\
1.538 + & | & term " `` " term \\
1.539 + & | & term " Int " term \\
1.540 + & | & term " Un " term \\
1.541 + & | & "INT~~" id ":" term " . " term \\
1.542 + & | & "UN~~~" id ":" term " . " term \\
1.543 + & | & "INT~~" id~id^* " . " term \\
1.544 + & | & "UN~~~" id~id^* " . " term \\[2ex]
1.545 + formula & = & \hbox{other formulae\ldots} \\
1.546 + & | & term " : " term \\
1.547 + & | & term " \ttilde: " term \\
1.548 + & | & term " <= " term \\
1.549 + & | & "!~" id ":" term " . " formula
1.550 + & | & "ALL " id ":" term " . " formula \\
1.551 + & | & "?~" id ":" term " . " formula
1.552 + & | & "EX~~" id ":" term " . " formula
1.553 + \end{array}
1.554 +\]
1.555 +\subcaption{Full Grammar}
1.556 +\caption{Syntax of the theory \texttt{Set} (continued)} \label{hol-set-syntax2}
1.557 +\end{figure}
1.558 +
1.559 +
1.560 +\section{A formulation of set theory}
1.561 +Historically, higher-order logic gives a foundation for Russell and
1.562 +Whitehead's theory of classes. Let us use modern terminology and call them
1.563 +{\bf sets}, but note that these sets are distinct from those of {\ZF} set
1.564 +theory, and behave more like {\ZF} classes.
1.565 +\begin{itemize}
1.566 +\item
1.567 +Sets are given by predicates over some type~$\sigma$. Types serve to
1.568 +define universes for sets, but type-checking is still significant.
1.569 +\item
1.570 +There is a universal set (for each type). Thus, sets have complements, and
1.571 +may be defined by absolute comprehension.
1.572 +\item
1.573 +Although sets may contain other sets as elements, the containing set must
1.574 +have a more complex type.
1.575 +\end{itemize}
1.576 +Finite unions and intersections have the same behaviour in \HOL\ as they
1.577 +do in~{\ZF}. In \HOL\ the intersection of the empty set is well-defined,
1.578 +denoting the universal set for the given type.
1.579 +
1.580 +\subsection{Syntax of set theory}\index{*set type}
1.581 +\HOL's set theory is called \thydx{Set}. The type $\alpha\,set$ is
1.582 +essentially the same as $\alpha\To bool$. The new type is defined for
1.583 +clarity and to avoid complications involving function types in unification.
1.584 +The isomorphisms between the two types are declared explicitly. They are
1.585 +very natural: \texttt{Collect} maps $\alpha\To bool$ to $\alpha\,set$, while
1.586 +\hbox{\tt op :} maps in the other direction (ignoring argument order).
1.587 +
1.588 +Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax
1.589 +translations. Figure~\ref{hol-set-syntax2} presents the grammar of the new
1.590 +constructs. Infix operators include union and intersection ($A\un B$
1.591 +and $A\int B$), the subset and membership relations, and the image
1.592 +operator~{\tt``}\@. Note that $a$\verb|~:|$b$ is translated to
1.593 +$\neg(a\in b)$.
1.594 +
1.595 +The $\{a@1,\ldots\}$ notation abbreviates finite sets constructed in
1.596 +the obvious manner using~\texttt{insert} and~$\{\}$:
1.597 +\begin{eqnarray*}
1.598 + \{a, b, c\} & \equiv &
1.599 + \texttt{insert} \, a \, ({\tt insert} \, b \, ({\tt insert} \, c \, \{\}))
1.600 +\end{eqnarray*}
1.601 +
1.602 +The set \hbox{\tt{\ttlbrace}$x$.\ $P[x]${\ttrbrace}} consists of all $x$ (of suitable type)
1.603 +that satisfy~$P[x]$, where $P[x]$ is a formula that may contain free
1.604 +occurrences of~$x$. This syntax expands to \cdx{Collect}$(\lambda
1.605 +x. P[x])$. It defines sets by absolute comprehension, which is impossible
1.606 +in~{\ZF}; the type of~$x$ implicitly restricts the comprehension.
1.607 +
1.608 +The set theory defines two {\bf bounded quantifiers}:
1.609 +\begin{eqnarray*}
1.610 + \forall x\in A. P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\
1.611 + \exists x\in A. P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x]
1.612 +\end{eqnarray*}
1.613 +The constants~\cdx{Ball} and~\cdx{Bex} are defined
1.614 +accordingly. Instead of \texttt{Ball $A$ $P$} and \texttt{Bex $A$ $P$} we may
1.615 +write\index{*"! symbol}\index{*"? symbol}
1.616 +\index{*ALL symbol}\index{*EX symbol}
1.617 +%
1.618 +\hbox{\tt !~$x$:$A$.\ $P[x]$} and \hbox{\tt ?~$x$:$A$.\ $P[x]$}. Isabelle's
1.619 +usual quantifier symbols, \sdx{ALL} and \sdx{EX}, are also accepted
1.620 +for input. As with the primitive quantifiers, the {\ML} reference
1.621 +\ttindex{HOL_quantifiers} specifies which notation to use for output.
1.622 +
1.623 +Unions and intersections over sets, namely $\bigcup@{x\in A}B[x]$ and
1.624 +$\bigcap@{x\in A}B[x]$, are written
1.625 +\sdx{UN}~\hbox{\tt$x$:$A$.\ $B[x]$} and
1.626 +\sdx{INT}~\hbox{\tt$x$:$A$.\ $B[x]$}.
1.627 +
1.628 +Unions and intersections over types, namely $\bigcup@x B[x]$ and $\bigcap@x
1.629 +B[x]$, are written \sdx{UN}~\hbox{\tt$x$.\ $B[x]$} and
1.630 +\sdx{INT}~\hbox{\tt$x$.\ $B[x]$}. They are equivalent to the previous
1.631 +union and intersection operators when $A$ is the universal set.
1.632 +
1.633 +The operators $\bigcup A$ and $\bigcap A$ act upon sets of sets. They are
1.634 +not binders, but are equal to $\bigcup@{x\in A}x$ and $\bigcap@{x\in A}x$,
1.635 +respectively.
1.636 +
1.637 +
1.638 +
1.639 +\begin{figure} \underscoreon
1.640 +\begin{ttbox}
1.641 +\tdx{mem_Collect_eq} (a : {\ttlbrace}x. P x{\ttrbrace}) = P a
1.642 +\tdx{Collect_mem_eq} {\ttlbrace}x. x:A{\ttrbrace} = A
1.643 +
1.644 +\tdx{empty_def} {\ttlbrace}{\ttrbrace} == {\ttlbrace}x. False{\ttrbrace}
1.645 +\tdx{insert_def} insert a B == {\ttlbrace}x. x=a{\ttrbrace} Un B
1.646 +\tdx{Ball_def} Ball A P == ! x. x:A --> P x
1.647 +\tdx{Bex_def} Bex A P == ? x. x:A & P x
1.648 +\tdx{subset_def} A <= B == ! x:A. x:B
1.649 +\tdx{Un_def} A Un B == {\ttlbrace}x. x:A | x:B{\ttrbrace}
1.650 +\tdx{Int_def} A Int B == {\ttlbrace}x. x:A & x:B{\ttrbrace}
1.651 +\tdx{set_diff_def} A - B == {\ttlbrace}x. x:A & x~:B{\ttrbrace}
1.652 +\tdx{Compl_def} Compl A == {\ttlbrace}x. ~ x:A{\ttrbrace}
1.653 +\tdx{INTER_def} INTER A B == {\ttlbrace}y. ! x:A. y: B x{\ttrbrace}
1.654 +\tdx{UNION_def} UNION A B == {\ttlbrace}y. ? x:A. y: B x{\ttrbrace}
1.655 +\tdx{INTER1_def} INTER1 B == INTER {\ttlbrace}x. True{\ttrbrace} B
1.656 +\tdx{UNION1_def} UNION1 B == UNION {\ttlbrace}x. True{\ttrbrace} B
1.657 +\tdx{Inter_def} Inter S == (INT x:S. x)
1.658 +\tdx{Union_def} Union S == (UN x:S. x)
1.659 +\tdx{Pow_def} Pow A == {\ttlbrace}B. B <= A{\ttrbrace}
1.660 +\tdx{image_def} f``A == {\ttlbrace}y. ? x:A. y=f x{\ttrbrace}
1.661 +\tdx{range_def} range f == {\ttlbrace}y. ? x. y=f x{\ttrbrace}
1.662 +\end{ttbox}
1.663 +\caption{Rules of the theory \texttt{Set}} \label{hol-set-rules}
1.664 +\end{figure}
1.665 +
1.666 +
1.667 +\begin{figure} \underscoreon
1.668 +\begin{ttbox}
1.669 +\tdx{CollectI} [| P a |] ==> a : {\ttlbrace}x. P x{\ttrbrace}
1.670 +\tdx{CollectD} [| a : {\ttlbrace}x. P x{\ttrbrace} |] ==> P a
1.671 +\tdx{CollectE} [| a : {\ttlbrace}x. P x{\ttrbrace}; P a ==> W |] ==> W
1.672 +
1.673 +\tdx{ballI} [| !!x. x:A ==> P x |] ==> ! x:A. P x
1.674 +\tdx{bspec} [| ! x:A. P x; x:A |] ==> P x
1.675 +\tdx{ballE} [| ! x:A. P x; P x ==> Q; ~ x:A ==> Q |] ==> Q
1.676 +
1.677 +\tdx{bexI} [| P x; x:A |] ==> ? x:A. P x
1.678 +\tdx{bexCI} [| ! x:A. ~ P x ==> P a; a:A |] ==> ? x:A. P x
1.679 +\tdx{bexE} [| ? x:A. P x; !!x. [| x:A; P x |] ==> Q |] ==> Q
1.680 +\subcaption{Comprehension and Bounded quantifiers}
1.681 +
1.682 +\tdx{subsetI} (!!x. x:A ==> x:B) ==> A <= B
1.683 +\tdx{subsetD} [| A <= B; c:A |] ==> c:B
1.684 +\tdx{subsetCE} [| A <= B; ~ (c:A) ==> P; c:B ==> P |] ==> P
1.685 +
1.686 +\tdx{subset_refl} A <= A
1.687 +\tdx{subset_trans} [| A<=B; B<=C |] ==> A<=C
1.688 +
1.689 +\tdx{equalityI} [| A <= B; B <= A |] ==> A = B
1.690 +\tdx{equalityD1} A = B ==> A<=B
1.691 +\tdx{equalityD2} A = B ==> B<=A
1.692 +\tdx{equalityE} [| A = B; [| A<=B; B<=A |] ==> P |] ==> P
1.693 +
1.694 +\tdx{equalityCE} [| A = B; [| c:A; c:B |] ==> P;
1.695 + [| ~ c:A; ~ c:B |] ==> P
1.696 + |] ==> P
1.697 +\subcaption{The subset and equality relations}
1.698 +\end{ttbox}
1.699 +\caption{Derived rules for set theory} \label{hol-set1}
1.700 +\end{figure}
1.701 +
1.702 +
1.703 +\begin{figure} \underscoreon
1.704 +\begin{ttbox}
1.705 +\tdx{emptyE} a : {\ttlbrace}{\ttrbrace} ==> P
1.706 +
1.707 +\tdx{insertI1} a : insert a B
1.708 +\tdx{insertI2} a : B ==> a : insert b B
1.709 +\tdx{insertE} [| a : insert b A; a=b ==> P; a:A ==> P |] ==> P
1.710 +
1.711 +\tdx{ComplI} [| c:A ==> False |] ==> c : Compl A
1.712 +\tdx{ComplD} [| c : Compl A |] ==> ~ c:A
1.713 +
1.714 +\tdx{UnI1} c:A ==> c : A Un B
1.715 +\tdx{UnI2} c:B ==> c : A Un B
1.716 +\tdx{UnCI} (~c:B ==> c:A) ==> c : A Un B
1.717 +\tdx{UnE} [| c : A Un B; c:A ==> P; c:B ==> P |] ==> P
1.718 +
1.719 +\tdx{IntI} [| c:A; c:B |] ==> c : A Int B
1.720 +\tdx{IntD1} c : A Int B ==> c:A
1.721 +\tdx{IntD2} c : A Int B ==> c:B
1.722 +\tdx{IntE} [| c : A Int B; [| c:A; c:B |] ==> P |] ==> P
1.723 +
1.724 +\tdx{UN_I} [| a:A; b: B a |] ==> b: (UN x:A. B x)
1.725 +\tdx{UN_E} [| b: (UN x:A. B x); !!x.[| x:A; b:B x |] ==> R |] ==> R
1.726 +
1.727 +\tdx{INT_I} (!!x. x:A ==> b: B x) ==> b : (INT x:A. B x)
1.728 +\tdx{INT_D} [| b: (INT x:A. B x); a:A |] ==> b: B a
1.729 +\tdx{INT_E} [| b: (INT x:A. B x); b: B a ==> R; ~ a:A ==> R |] ==> R
1.730 +
1.731 +\tdx{UnionI} [| X:C; A:X |] ==> A : Union C
1.732 +\tdx{UnionE} [| A : Union C; !!X.[| A:X; X:C |] ==> R |] ==> R
1.733 +
1.734 +\tdx{InterI} [| !!X. X:C ==> A:X |] ==> A : Inter C
1.735 +\tdx{InterD} [| A : Inter C; X:C |] ==> A:X
1.736 +\tdx{InterE} [| A : Inter C; A:X ==> R; ~ X:C ==> R |] ==> R
1.737 +
1.738 +\tdx{PowI} A<=B ==> A: Pow B
1.739 +\tdx{PowD} A: Pow B ==> A<=B
1.740 +
1.741 +\tdx{imageI} [| x:A |] ==> f x : f``A
1.742 +\tdx{imageE} [| b : f``A; !!x.[| b=f x; x:A |] ==> P |] ==> P
1.743 +
1.744 +\tdx{rangeI} f x : range f
1.745 +\tdx{rangeE} [| b : range f; !!x.[| b=f x |] ==> P |] ==> P
1.746 +\end{ttbox}
1.747 +\caption{Further derived rules for set theory} \label{hol-set2}
1.748 +\end{figure}
1.749 +
1.750 +
1.751 +\subsection{Axioms and rules of set theory}
1.752 +Figure~\ref{hol-set-rules} presents the rules of theory \thydx{Set}. The
1.753 +axioms \tdx{mem_Collect_eq} and \tdx{Collect_mem_eq} assert
1.754 +that the functions \texttt{Collect} and \hbox{\tt op :} are isomorphisms. Of
1.755 +course, \hbox{\tt op :} also serves as the membership relation.
1.756 +
1.757 +All the other axioms are definitions. They include the empty set, bounded
1.758 +quantifiers, unions, intersections, complements and the subset relation.
1.759 +They also include straightforward constructions on functions: image~({\tt``})
1.760 +and \texttt{range}.
1.761 +
1.762 +%The predicate \cdx{inj_on} is used for simulating type definitions.
1.763 +%The statement ${\tt inj_on}~f~A$ asserts that $f$ is injective on the
1.764 +%set~$A$, which specifies a subset of its domain type. In a type
1.765 +%definition, $f$ is the abstraction function and $A$ is the set of valid
1.766 +%representations; we should not expect $f$ to be injective outside of~$A$.
1.767 +
1.768 +%\begin{figure} \underscoreon
1.769 +%\begin{ttbox}
1.770 +%\tdx{Inv_f_f} inj f ==> Inv f (f x) = x
1.771 +%\tdx{f_Inv_f} y : range f ==> f(Inv f y) = y
1.772 +%
1.773 +%\tdx{Inv_injective}
1.774 +% [| Inv f x=Inv f y; x: range f; y: range f |] ==> x=y
1.775 +%
1.776 +%
1.777 +%\tdx{monoI} [| !!A B. A <= B ==> f A <= f B |] ==> mono f
1.778 +%\tdx{monoD} [| mono f; A <= B |] ==> f A <= f B
1.779 +%
1.780 +%\tdx{injI} [| !! x y. f x = f y ==> x=y |] ==> inj f
1.781 +%\tdx{inj_inverseI} (!!x. g(f x) = x) ==> inj f
1.782 +%\tdx{injD} [| inj f; f x = f y |] ==> x=y
1.783 +%
1.784 +%\tdx{inj_onI} (!!x y. [| f x=f y; x:A; y:A |] ==> x=y) ==> inj_on f A
1.785 +%\tdx{inj_onD} [| inj_on f A; f x=f y; x:A; y:A |] ==> x=y
1.786 +%
1.787 +%\tdx{inj_on_inverseI}
1.788 +% (!!x. x:A ==> g(f x) = x) ==> inj_on f A
1.789 +%\tdx{inj_on_contraD}
1.790 +% [| inj_on f A; x~=y; x:A; y:A |] ==> ~ f x=f y
1.791 +%\end{ttbox}
1.792 +%\caption{Derived rules involving functions} \label{hol-fun}
1.793 +%\end{figure}
1.794 +
1.795 +
1.796 +\begin{figure} \underscoreon
1.797 +\begin{ttbox}
1.798 +\tdx{Union_upper} B:A ==> B <= Union A
1.799 +\tdx{Union_least} [| !!X. X:A ==> X<=C |] ==> Union A <= C
1.800 +
1.801 +\tdx{Inter_lower} B:A ==> Inter A <= B
1.802 +\tdx{Inter_greatest} [| !!X. X:A ==> C<=X |] ==> C <= Inter A
1.803 +
1.804 +\tdx{Un_upper1} A <= A Un B
1.805 +\tdx{Un_upper2} B <= A Un B
1.806 +\tdx{Un_least} [| A<=C; B<=C |] ==> A Un B <= C
1.807 +
1.808 +\tdx{Int_lower1} A Int B <= A
1.809 +\tdx{Int_lower2} A Int B <= B
1.810 +\tdx{Int_greatest} [| C<=A; C<=B |] ==> C <= A Int B
1.811 +\end{ttbox}
1.812 +\caption{Derived rules involving subsets} \label{hol-subset}
1.813 +\end{figure}
1.814 +
1.815 +
1.816 +\begin{figure} \underscoreon \hfuzz=4pt%suppress "Overfull \hbox" message
1.817 +\begin{ttbox}
1.818 +\tdx{Int_absorb} A Int A = A
1.819 +\tdx{Int_commute} A Int B = B Int A
1.820 +\tdx{Int_assoc} (A Int B) Int C = A Int (B Int C)
1.821 +\tdx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C)
1.822 +
1.823 +\tdx{Un_absorb} A Un A = A
1.824 +\tdx{Un_commute} A Un B = B Un A
1.825 +\tdx{Un_assoc} (A Un B) Un C = A Un (B Un C)
1.826 +\tdx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C)
1.827 +
1.828 +\tdx{Compl_disjoint} A Int (Compl A) = {\ttlbrace}x. False{\ttrbrace}
1.829 +\tdx{Compl_partition} A Un (Compl A) = {\ttlbrace}x. True{\ttrbrace}
1.830 +\tdx{double_complement} Compl(Compl A) = A
1.831 +\tdx{Compl_Un} Compl(A Un B) = (Compl A) Int (Compl B)
1.832 +\tdx{Compl_Int} Compl(A Int B) = (Compl A) Un (Compl B)
1.833 +
1.834 +\tdx{Union_Un_distrib} Union(A Un B) = (Union A) Un (Union B)
1.835 +\tdx{Int_Union} A Int (Union B) = (UN C:B. A Int C)
1.836 +\tdx{Un_Union_image} (UN x:C.(A x) Un (B x)) = Union(A``C) Un Union(B``C)
1.837 +
1.838 +\tdx{Inter_Un_distrib} Inter(A Un B) = (Inter A) Int (Inter B)
1.839 +\tdx{Un_Inter} A Un (Inter B) = (INT C:B. A Un C)
1.840 +\tdx{Int_Inter_image} (INT x:C.(A x) Int (B x)) = Inter(A``C) Int Inter(B``C)
1.841 +\end{ttbox}
1.842 +\caption{Set equalities} \label{hol-equalities}
1.843 +\end{figure}
1.844 +
1.845 +
1.846 +Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules. Most are
1.847 +obvious and resemble rules of Isabelle's {\ZF} set theory. Certain rules,
1.848 +such as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI},
1.849 +are designed for classical reasoning; the rules \tdx{subsetD},
1.850 +\tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are not
1.851 +strictly necessary but yield more natural proofs. Similarly,
1.852 +\tdx{equalityCE} supports classical reasoning about extensionality,
1.853 +after the fashion of \tdx{iffCE}. See the file \texttt{HOL/Set.ML} for
1.854 +proofs pertaining to set theory.
1.855 +
1.856 +Figure~\ref{hol-subset} presents lattice properties of the subset relation.
1.857 +Unions form least upper bounds; non-empty intersections form greatest lower
1.858 +bounds. Reasoning directly about subsets often yields clearer proofs than
1.859 +reasoning about the membership relation. See the file \texttt{HOL/subset.ML}.
1.860 +
1.861 +Figure~\ref{hol-equalities} presents many common set equalities. They
1.862 +include commutative, associative and distributive laws involving unions,
1.863 +intersections and complements. For a complete listing see the file {\tt
1.864 +HOL/equalities.ML}.
1.865 +
1.866 +\begin{warn}
1.867 +\texttt{Blast_tac} proves many set-theoretic theorems automatically.
1.868 +Hence you seldom need to refer to the theorems above.
1.869 +\end{warn}
1.870 +
1.871 +\begin{figure}
1.872 +\begin{center}
1.873 +\begin{tabular}{rrr}
1.874 + \it name &\it meta-type & \it description \\
1.875 + \cdx{inj}~~\cdx{surj}& $(\alpha\To\beta )\To bool$
1.876 + & injective/surjective \\
1.877 + \cdx{inj_on} & $[\alpha\To\beta ,\alpha\,set]\To bool$
1.878 + & injective over subset\\
1.879 + \cdx{inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & inverse function
1.880 +\end{tabular}
1.881 +\end{center}
1.882 +
1.883 +\underscoreon
1.884 +\begin{ttbox}
1.885 +\tdx{inj_def} inj f == ! x y. f x=f y --> x=y
1.886 +\tdx{surj_def} surj f == ! y. ? x. y=f x
1.887 +\tdx{inj_on_def} inj_on f A == !x:A. !y:A. f x=f y --> x=y
1.888 +\tdx{inv_def} inv f == (\%y. @x. f(x)=y)
1.889 +\end{ttbox}
1.890 +\caption{Theory \thydx{Fun}} \label{fig:HOL:Fun}
1.891 +\end{figure}
1.892 +
1.893 +\subsection{Properties of functions}\nopagebreak
1.894 +Figure~\ref{fig:HOL:Fun} presents a theory of simple properties of functions.
1.895 +Note that ${\tt inv}~f$ uses Hilbert's $\varepsilon$ to yield an inverse
1.896 +of~$f$. See the file \texttt{HOL/Fun.ML} for a complete listing of the derived
1.897 +rules. Reasoning about function composition (the operator~\sdx{o}) and the
1.898 +predicate~\cdx{surj} is done simply by expanding the definitions.
1.899 +
1.900 +There is also a large collection of monotonicity theorems for constructions
1.901 +on sets in the file \texttt{HOL/mono.ML}.
1.902 +
1.903 +\section{Generic packages}
1.904 +\label{sec:HOL:generic-packages}
1.905 +
1.906 +\HOL\ instantiates most of Isabelle's generic packages, making available the
1.907 +simplifier and the classical reasoner.
1.908 +
1.909 +\subsection{Simplification and substitution}
1.910 +
1.911 +Simplification tactics tactics such as \texttt{Asm_simp_tac} and \texttt{Full_simp_tac} use the default simpset
1.912 +(\texttt{simpset()}), which works for most purposes. A quite minimal
1.913 +simplification set for higher-order logic is~\ttindexbold{HOL_ss};
1.914 +even more frugal is \ttindexbold{HOL_basic_ss}. Equality~($=$), which
1.915 +also expresses logical equivalence, may be used for rewriting. See
1.916 +the file \texttt{HOL/simpdata.ML} for a complete listing of the basic
1.917 +simplification rules.
1.918 +
1.919 +See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
1.920 +{Chaps.\ts\ref{substitution} and~\ref{simp-chap}} for details of substitution
1.921 +and simplification.
1.922 +
1.923 +\begin{warn}\index{simplification!of conjunctions}%
1.924 + Reducing $a=b\conj P(a)$ to $a=b\conj P(b)$ is sometimes advantageous. The
1.925 + left part of a conjunction helps in simplifying the right part. This effect
1.926 + is not available by default: it can be slow. It can be obtained by
1.927 + including \ttindex{conj_cong} in a simpset, \verb$addcongs [conj_cong]$.
1.928 +\end{warn}
1.929 +
1.930 +If the simplifier cannot use a certain rewrite rule --- either because
1.931 +of nontermination or because its left-hand side is too flexible ---
1.932 +then you might try \texttt{stac}:
1.933 +\begin{ttdescription}
1.934 +\item[\ttindexbold{stac} $thm$ $i,$] where $thm$ is of the form $lhs = rhs$,
1.935 + replaces in subgoal $i$ instances of $lhs$ by corresponding instances of
1.936 + $rhs$. In case of multiple instances of $lhs$ in subgoal $i$, backtracking
1.937 + may be necessary to select the desired ones.
1.938 +
1.939 +If $thm$ is a conditional equality, the instantiated condition becomes an
1.940 +additional (first) subgoal.
1.941 +\end{ttdescription}
1.942 +
1.943 + \HOL{} provides the tactic \ttindex{hyp_subst_tac}, which substitutes
1.944 + for an equality throughout a subgoal and its hypotheses. This tactic uses
1.945 + \HOL's general substitution rule.
1.946 +
1.947 +\subsubsection{Case splitting}
1.948 +\label{subsec:HOL:case:splitting}
1.949 +
1.950 +\HOL{} also provides convenient means for case splitting during
1.951 +rewriting. Goals containing a subterm of the form \texttt{if}~$b$~{\tt
1.952 +then\dots else\dots} often require a case distinction on $b$. This is
1.953 +expressed by the theorem \tdx{split_if}:
1.954 +$$
1.955 +\Var{P}(\mbox{\tt if}~\Var{b}~{\tt then}~\Var{x}~\mbox{\tt else}~\Var{y})~=~
1.956 +((\Var{b} \to \Var{P}(\Var{x})) \land (\neg \Var{b} \to \Var{P}(\Var{y})))
1.957 +\eqno{(*)}
1.958 +$$
1.959 +For example, a simple instance of $(*)$ is
1.960 +\[
1.961 +x \in (\mbox{\tt if}~x \in A~{\tt then}~A~\mbox{\tt else}~\{x\})~=~
1.962 +((x \in A \to x \in A) \land (x \notin A \to x \in \{x\}))
1.963 +\]
1.964 +Because $(*)$ is too general as a rewrite rule for the simplifier (the
1.965 +left-hand side is not a higher-order pattern in the sense of
1.966 +\iflabelundefined{chap:simplification}{the {\em Reference Manual\/}}%
1.967 +{Chap.\ts\ref{chap:simplification}}), there is a special infix function
1.968 +\ttindexbold{addsplits} of type \texttt{simpset * thm list -> simpset}
1.969 +(analogous to \texttt{addsimps}) that adds rules such as $(*)$ to a
1.970 +simpset, as in
1.971 +\begin{ttbox}
1.972 +by(simp_tac (simpset() addsplits [split_if]) 1);
1.973 +\end{ttbox}
1.974 +The effect is that after each round of simplification, one occurrence of
1.975 +\texttt{if} is split acording to \texttt{split_if}, until all occurences of
1.976 +\texttt{if} have been eliminated.
1.977 +
1.978 +It turns out that using \texttt{split_if} is almost always the right thing to
1.979 +do. Hence \texttt{split_if} is already included in the default simpset. If
1.980 +you want to delete it from a simpset, use \ttindexbold{delsplits}, which is
1.981 +the inverse of \texttt{addsplits}:
1.982 +\begin{ttbox}
1.983 +by(simp_tac (simpset() delsplits [split_if]) 1);
1.984 +\end{ttbox}
1.985 +
1.986 +In general, \texttt{addsplits} accepts rules of the form
1.987 +\[
1.988 +\Var{P}(c~\Var{x@1}~\dots~\Var{x@n})~=~ rhs
1.989 +\]
1.990 +where $c$ is a constant and $rhs$ is arbitrary. Note that $(*)$ is of the
1.991 +right form because internally the left-hand side is
1.992 +$\Var{P}(\mathtt{If}~\Var{b}~\Var{x}~~\Var{y})$. Important further examples
1.993 +are splitting rules for \texttt{case} expressions (see~\S\ref{subsec:list}
1.994 +and~\S\ref{subsec:datatype:basics}).
1.995 +
1.996 +Analogous to \texttt{Addsimps} and \texttt{Delsimps}, there are also
1.997 +imperative versions of \texttt{addsplits} and \texttt{delsplits}
1.998 +\begin{ttbox}
1.999 +\ttindexbold{Addsplits}: thm list -> unit
1.1000 +\ttindexbold{Delsplits}: thm list -> unit
1.1001 +\end{ttbox}
1.1002 +for adding splitting rules to, and deleting them from the current simpset.
1.1003 +
1.1004 +\subsection{Classical reasoning}
1.1005 +
1.1006 +\HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as
1.1007 +well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
1.1008 +rule; recall Fig.\ts\ref{hol-lemmas2} above.
1.1009 +
1.1010 +The classical reasoner is installed. Tactics such as \texttt{Blast_tac} and {\tt
1.1011 +Best_tac} refer to the default claset (\texttt{claset()}), which works for most
1.1012 +purposes. Named clasets include \ttindexbold{prop_cs}, which includes the
1.1013 +propositional rules, and \ttindexbold{HOL_cs}, which also includes quantifier
1.1014 +rules. See the file \texttt{HOL/cladata.ML} for lists of the classical rules,
1.1015 +and \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
1.1016 +{Chap.\ts\ref{chap:classical}} for more discussion of classical proof methods.
1.1017 +
1.1018 +
1.1019 +\section{Types}\label{sec:HOL:Types}
1.1020 +This section describes \HOL's basic predefined types ($\alpha \times
1.1021 +\beta$, $\alpha + \beta$, $nat$ and $\alpha \; list$) and ways for
1.1022 +introducing new types in general. The most important type
1.1023 +construction, the \texttt{datatype}, is treated separately in
1.1024 +\S\ref{sec:HOL:datatype}.
1.1025 +
1.1026 +
1.1027 +\subsection{Product and sum types}\index{*"* type}\index{*"+ type}
1.1028 +\label{subsec:prod-sum}
1.1029 +
1.1030 +\begin{figure}[htbp]
1.1031 +\begin{constants}
1.1032 + \it symbol & \it meta-type & & \it description \\
1.1033 + \cdx{Pair} & $[\alpha,\beta]\To \alpha\times\beta$
1.1034 + & & ordered pairs $(a,b)$ \\
1.1035 + \cdx{fst} & $\alpha\times\beta \To \alpha$ & & first projection\\
1.1036 + \cdx{snd} & $\alpha\times\beta \To \beta$ & & second projection\\
1.1037 + \cdx{split} & $[[\alpha,\beta]\To\gamma, \alpha\times\beta] \To \gamma$
1.1038 + & & generalized projection\\
1.1039 + \cdx{Sigma} &
1.1040 + $[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ &
1.1041 + & general sum of sets
1.1042 +\end{constants}
1.1043 +\begin{ttbox}\makeatletter
1.1044 +%\tdx{fst_def} fst p == @a. ? b. p = (a,b)
1.1045 +%\tdx{snd_def} snd p == @b. ? a. p = (a,b)
1.1046 +%\tdx{split_def} split c p == c (fst p) (snd p)
1.1047 +\tdx{Sigma_def} Sigma A B == UN x:A. UN y:B x. {\ttlbrace}(x,y){\ttrbrace}
1.1048 +
1.1049 +\tdx{Pair_eq} ((a,b) = (a',b')) = (a=a' & b=b')
1.1050 +\tdx{Pair_inject} [| (a, b) = (a',b'); [| a=a'; b=b' |] ==> R |] ==> R
1.1051 +\tdx{PairE} [| !!x y. p = (x,y) ==> Q |] ==> Q
1.1052 +
1.1053 +\tdx{fst_conv} fst (a,b) = a
1.1054 +\tdx{snd_conv} snd (a,b) = b
1.1055 +\tdx{surjective_pairing} p = (fst p,snd p)
1.1056 +
1.1057 +\tdx{split} split c (a,b) = c a b
1.1058 +\tdx{split_split} R(split c p) = (! x y. p = (x,y) --> R(c x y))
1.1059 +
1.1060 +\tdx{SigmaI} [| a:A; b:B a |] ==> (a,b) : Sigma A B
1.1061 +\tdx{SigmaE} [| c:Sigma A B; !!x y.[| x:A; y:B x; c=(x,y) |] ==> P |] ==> P
1.1062 +\end{ttbox}
1.1063 +\caption{Type $\alpha\times\beta$}\label{hol-prod}
1.1064 +\end{figure}
1.1065 +
1.1066 +Theory \thydx{Prod} (Fig.\ts\ref{hol-prod}) defines the product type
1.1067 +$\alpha\times\beta$, with the ordered pair syntax $(a, b)$. General
1.1068 +tuples are simulated by pairs nested to the right:
1.1069 +\begin{center}
1.1070 +\begin{tabular}{c|c}
1.1071 +external & internal \\
1.1072 +\hline
1.1073 +$\tau@1 \times \dots \times \tau@n$ & $\tau@1 \times (\dots (\tau@{n-1} \times \tau@n)\dots)$ \\
1.1074 +\hline
1.1075 +$(t@1,\dots,t@n)$ & $(t@1,(\dots,(t@{n-1},t@n)\dots)$ \\
1.1076 +\end{tabular}
1.1077 +\end{center}
1.1078 +In addition, it is possible to use tuples
1.1079 +as patterns in abstractions:
1.1080 +\begin{center}
1.1081 +{\tt\%($x$,$y$). $t$} \quad stands for\quad \texttt{split(\%$x$\thinspace$y$.\ $t$)}
1.1082 +\end{center}
1.1083 +Nested patterns are also supported. They are translated stepwise:
1.1084 +{\tt\%($x$,$y$,$z$). $t$} $\leadsto$ {\tt\%($x$,($y$,$z$)). $t$} $\leadsto$
1.1085 +{\tt split(\%$x$.\%($y$,$z$). $t$)} $\leadsto$ \texttt{split(\%$x$. split(\%$y$
1.1086 + $z$.\ $t$))}. The reverse translation is performed upon printing.
1.1087 +\begin{warn}
1.1088 + The translation between patterns and \texttt{split} is performed automatically
1.1089 + by the parser and printer. Thus the internal and external form of a term
1.1090 + may differ, which can affects proofs. For example the term {\tt
1.1091 + (\%(x,y).(y,x))(a,b)} requires the theorem \texttt{split} (which is in the
1.1092 + default simpset) to rewrite to {\tt(b,a)}.
1.1093 +\end{warn}
1.1094 +In addition to explicit $\lambda$-abstractions, patterns can be used in any
1.1095 +variable binding construct which is internally described by a
1.1096 +$\lambda$-abstraction. Some important examples are
1.1097 +\begin{description}
1.1098 +\item[Let:] \texttt{let {\it pattern} = $t$ in $u$}
1.1099 +\item[Quantifiers:] \texttt{!~{\it pattern}:$A$.~$P$}
1.1100 +\item[Choice:] {\underscoreon \tt @~{\it pattern}~.~$P$}
1.1101 +\item[Set operations:] \texttt{UN~{\it pattern}:$A$.~$B$}
1.1102 +\item[Sets:] \texttt{{\ttlbrace}~{\it pattern}~.~$P$~{\ttrbrace}}
1.1103 +\end{description}
1.1104 +
1.1105 +There is a simple tactic which supports reasoning about patterns:
1.1106 +\begin{ttdescription}
1.1107 +\item[\ttindexbold{split_all_tac} $i$] replaces in subgoal $i$ all
1.1108 + {\tt!!}-quantified variables of product type by individual variables for
1.1109 + each component. A simple example:
1.1110 +\begin{ttbox}
1.1111 +{\out 1. !!p. (\%(x,y,z). (x, y, z)) p = p}
1.1112 +by(split_all_tac 1);
1.1113 +{\out 1. !!x xa ya. (\%(x,y,z). (x, y, z)) (x, xa, ya) = (x, xa, ya)}
1.1114 +\end{ttbox}
1.1115 +\end{ttdescription}
1.1116 +
1.1117 +Theory \texttt{Prod} also introduces the degenerate product type \texttt{unit}
1.1118 +which contains only a single element named {\tt()} with the property
1.1119 +\begin{ttbox}
1.1120 +\tdx{unit_eq} u = ()
1.1121 +\end{ttbox}
1.1122 +\bigskip
1.1123 +
1.1124 +Theory \thydx{Sum} (Fig.~\ref{hol-sum}) defines the sum type $\alpha+\beta$
1.1125 +which associates to the right and has a lower priority than $*$: $\tau@1 +
1.1126 +\tau@2 + \tau@3*\tau@4$ means $\tau@1 + (\tau@2 + (\tau@3*\tau@4))$.
1.1127 +
1.1128 +The definition of products and sums in terms of existing types is not
1.1129 +shown. The constructions are fairly standard and can be found in the
1.1130 +respective theory files.
1.1131 +
1.1132 +\begin{figure}
1.1133 +\begin{constants}
1.1134 + \it symbol & \it meta-type & & \it description \\
1.1135 + \cdx{Inl} & $\alpha \To \alpha+\beta$ & & first injection\\
1.1136 + \cdx{Inr} & $\beta \To \alpha+\beta$ & & second injection\\
1.1137 + \cdx{sum_case} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$
1.1138 + & & conditional
1.1139 +\end{constants}
1.1140 +\begin{ttbox}\makeatletter
1.1141 +%\tdx{sum_case_def} sum_case == (\%f g p. @z. (!x. p=Inl x --> z=f x) &
1.1142 +% (!y. p=Inr y --> z=g y))
1.1143 +%
1.1144 +\tdx{Inl_not_Inr} Inl a ~= Inr b
1.1145 +
1.1146 +\tdx{inj_Inl} inj Inl
1.1147 +\tdx{inj_Inr} inj Inr
1.1148 +
1.1149 +\tdx{sumE} [| !!x. P(Inl x); !!y. P(Inr y) |] ==> P s
1.1150 +
1.1151 +\tdx{sum_case_Inl} sum_case f g (Inl x) = f x
1.1152 +\tdx{sum_case_Inr} sum_case f g (Inr x) = g x
1.1153 +
1.1154 +\tdx{surjective_sum} sum_case (\%x. f(Inl x)) (\%y. f(Inr y)) s = f s
1.1155 +\tdx{split_sum_case} R(sum_case f g s) = ((! x. s = Inl(x) --> R(f(x))) &
1.1156 + (! y. s = Inr(y) --> R(g(y))))
1.1157 +\end{ttbox}
1.1158 +\caption{Type $\alpha+\beta$}\label{hol-sum}
1.1159 +\end{figure}
1.1160 +
1.1161 +\begin{figure}
1.1162 +\index{*"< symbol}
1.1163 +\index{*"* symbol}
1.1164 +\index{*div symbol}
1.1165 +\index{*mod symbol}
1.1166 +\index{*"+ symbol}
1.1167 +\index{*"- symbol}
1.1168 +\begin{constants}
1.1169 + \it symbol & \it meta-type & \it priority & \it description \\
1.1170 + \cdx{0} & $nat$ & & zero \\
1.1171 + \cdx{Suc} & $nat \To nat$ & & successor function\\
1.1172 +% \cdx{nat_case} & $[\alpha, nat\To\alpha, nat] \To\alpha$ & & conditional\\
1.1173 +% \cdx{nat_rec} & $[nat, \alpha, [nat, \alpha]\To\alpha] \To \alpha$
1.1174 +% & & primitive recursor\\
1.1175 + \tt * & $[nat,nat]\To nat$ & Left 70 & multiplication \\
1.1176 + \tt div & $[nat,nat]\To nat$ & Left 70 & division\\
1.1177 + \tt mod & $[nat,nat]\To nat$ & Left 70 & modulus\\
1.1178 + \tt + & $[nat,nat]\To nat$ & Left 65 & addition\\
1.1179 + \tt - & $[nat,nat]\To nat$ & Left 65 & subtraction
1.1180 +\end{constants}
1.1181 +\subcaption{Constants and infixes}
1.1182 +
1.1183 +\begin{ttbox}\makeatother
1.1184 +\tdx{nat_induct} [| P 0; !!n. P n ==> P(Suc n) |] ==> P n
1.1185 +
1.1186 +\tdx{Suc_not_Zero} Suc m ~= 0
1.1187 +\tdx{inj_Suc} inj Suc
1.1188 +\tdx{n_not_Suc_n} n~=Suc n
1.1189 +\subcaption{Basic properties}
1.1190 +\end{ttbox}
1.1191 +\caption{The type of natural numbers, \tydx{nat}} \label{hol-nat1}
1.1192 +\end{figure}
1.1193 +
1.1194 +
1.1195 +\begin{figure}
1.1196 +\begin{ttbox}\makeatother
1.1197 + 0+n = n
1.1198 + (Suc m)+n = Suc(m+n)
1.1199 +
1.1200 + m-0 = m
1.1201 + 0-n = n
1.1202 + Suc(m)-Suc(n) = m-n
1.1203 +
1.1204 + 0*n = 0
1.1205 + Suc(m)*n = n + m*n
1.1206 +
1.1207 +\tdx{mod_less} m<n ==> m mod n = m
1.1208 +\tdx{mod_geq} [| 0<n; ~m<n |] ==> m mod n = (m-n) mod n
1.1209 +
1.1210 +\tdx{div_less} m<n ==> m div n = 0
1.1211 +\tdx{div_geq} [| 0<n; ~m<n |] ==> m div n = Suc((m-n) div n)
1.1212 +\end{ttbox}
1.1213 +\caption{Recursion equations for the arithmetic operators} \label{hol-nat2}
1.1214 +\end{figure}
1.1215 +
1.1216 +\subsection{The type of natural numbers, \textit{nat}}
1.1217 +\index{nat@{\textit{nat}} type|(}
1.1218 +
1.1219 +The theory \thydx{NatDef} defines the natural numbers in a roundabout but
1.1220 +traditional way. The axiom of infinity postulates a type~\tydx{ind} of
1.1221 +individuals, which is non-empty and closed under an injective operation. The
1.1222 +natural numbers are inductively generated by choosing an arbitrary individual
1.1223 +for~0 and using the injective operation to take successors. This is a least
1.1224 +fixedpoint construction. For details see the file \texttt{NatDef.thy}.
1.1225 +
1.1226 +Type~\tydx{nat} is an instance of class~\cldx{ord}, which makes the
1.1227 +overloaded functions of this class (esp.\ \cdx{<} and \cdx{<=}, but also
1.1228 +\cdx{min}, \cdx{max} and \cdx{LEAST}) available on \tydx{nat}. Theory
1.1229 +\thydx{Nat} builds on \texttt{NatDef} and shows that {\tt<=} is a partial order,
1.1230 +so \tydx{nat} is also an instance of class \cldx{order}.
1.1231 +
1.1232 +Theory \thydx{Arith} develops arithmetic on the natural numbers. It defines
1.1233 +addition, multiplication and subtraction. Theory \thydx{Divides} defines
1.1234 +division, remainder and the ``divides'' relation. The numerous theorems
1.1235 +proved include commutative, associative, distributive, identity and
1.1236 +cancellation laws. See Figs.\ts\ref{hol-nat1} and~\ref{hol-nat2}. The
1.1237 +recursion equations for the operators \texttt{+}, \texttt{-} and \texttt{*} on
1.1238 +\texttt{nat} are part of the default simpset.
1.1239 +
1.1240 +Functions on \tydx{nat} can be defined by primitive or well-founded recursion;
1.1241 +see \S\ref{sec:HOL:recursive}. A simple example is addition.
1.1242 +Here, \texttt{op +} is the name of the infix operator~\texttt{+}, following
1.1243 +the standard convention.
1.1244 +\begin{ttbox}
1.1245 +\sdx{primrec}
1.1246 + "0 + n = n"
1.1247 + "Suc m + n = Suc (m + n)"
1.1248 +\end{ttbox}
1.1249 +There is also a \sdx{case}-construct
1.1250 +of the form
1.1251 +\begin{ttbox}
1.1252 +case \(e\) of 0 => \(a\) | Suc \(m\) => \(b\)
1.1253 +\end{ttbox}
1.1254 +Note that Isabelle insists on precisely this format; you may not even change
1.1255 +the order of the two cases.
1.1256 +Both \texttt{primrec} and \texttt{case} are realized by a recursion operator
1.1257 +\cdx{nat_rec}, the details of which can be found in theory \texttt{NatDef}.
1.1258 +
1.1259 +%The predecessor relation, \cdx{pred_nat}, is shown to be well-founded.
1.1260 +%Recursion along this relation resembles primitive recursion, but is
1.1261 +%stronger because we are in higher-order logic; using primitive recursion to
1.1262 +%define a higher-order function, we can easily Ackermann's function, which
1.1263 +%is not primitive recursive \cite[page~104]{thompson91}.
1.1264 +%The transitive closure of \cdx{pred_nat} is~$<$. Many functions on the
1.1265 +%natural numbers are most easily expressed using recursion along~$<$.
1.1266 +
1.1267 +Tactic {\tt\ttindex{induct_tac} "$n$" $i$} performs induction on variable~$n$
1.1268 +in subgoal~$i$ using theorem \texttt{nat_induct}. There is also the derived
1.1269 +theorem \tdx{less_induct}:
1.1270 +\begin{ttbox}
1.1271 +[| !!n. [| ! m. m<n --> P m |] ==> P n |] ==> P n
1.1272 +\end{ttbox}
1.1273 +
1.1274 +
1.1275 +Reasoning about arithmetic inequalities can be tedious. Fortunately HOL
1.1276 +provides a decision procedure for quantifier-free linear arithmetic (i.e.\
1.1277 +only addition and subtraction). The simplifier invokes a weak version of this
1.1278 +decision procedure automatically. If this is not sufficent, you can invoke
1.1279 +the full procedure \ttindex{arith_tac} explicitly. It copes with arbitrary
1.1280 +formulae involving {\tt=}, {\tt<}, {\tt<=}, {\tt+}, {\tt-}, {\tt Suc}, {\tt
1.1281 + min}, {\tt max} and numerical constants; other subterms are treated as
1.1282 +atomic; subformulae not involving type $nat$ are ignored; quantified
1.1283 +subformulae are ignored unless they are positive universal or negative
1.1284 +existential. Note that the running time is exponential in the number of
1.1285 +occurrences of {\tt min}, {\tt max}, and {\tt-} because they require case
1.1286 +distinctions. Note also that \texttt{arith_tac} is not complete: if
1.1287 +divisibility plays a role, it may fail to prove a valid formula, for example
1.1288 +$m+m \neq n+n+1$. Fortunately such examples are rare in practice.
1.1289 +
1.1290 +If \texttt{arith_tac} fails you, try to find relevant arithmetic results in
1.1291 +the library. The theory \texttt{NatDef} contains theorems about {\tt<} and
1.1292 +{\tt<=}, the theory \texttt{Arith} contains theorems about \texttt{+},
1.1293 +\texttt{-} and \texttt{*}, and theory \texttt{Divides} contains theorems about
1.1294 +\texttt{div} and \texttt{mod}. Use the \texttt{find}-functions to locate them
1.1295 +(see the {\em Reference Manual\/}).
1.1296 +
1.1297 +\begin{figure}
1.1298 +\index{#@{\tt[]} symbol}
1.1299 +\index{#@{\tt\#} symbol}
1.1300 +\index{"@@{\tt\at} symbol}
1.1301 +\index{*"! symbol}
1.1302 +\begin{constants}
1.1303 + \it symbol & \it meta-type & \it priority & \it description \\
1.1304 + \tt[] & $\alpha\,list$ & & empty list\\
1.1305 + \tt \# & $[\alpha,\alpha\,list]\To \alpha\,list$ & Right 65 &
1.1306 + list constructor \\
1.1307 + \cdx{null} & $\alpha\,list \To bool$ & & emptiness test\\
1.1308 + \cdx{hd} & $\alpha\,list \To \alpha$ & & head \\
1.1309 + \cdx{tl} & $\alpha\,list \To \alpha\,list$ & & tail \\
1.1310 + \cdx{last} & $\alpha\,list \To \alpha$ & & last element \\
1.1311 + \cdx{butlast} & $\alpha\,list \To \alpha\,list$ & & drop last element \\
1.1312 + \tt\at & $[\alpha\,list,\alpha\,list]\To \alpha\,list$ & Left 65 & append \\
1.1313 + \cdx{map} & $(\alpha\To\beta) \To (\alpha\,list \To \beta\,list)$
1.1314 + & & apply to all\\
1.1315 + \cdx{filter} & $(\alpha \To bool) \To (\alpha\,list \To \alpha\,list)$
1.1316 + & & filter functional\\
1.1317 + \cdx{set}& $\alpha\,list \To \alpha\,set$ & & elements\\
1.1318 + \sdx{mem} & $\alpha \To \alpha\,list \To bool$ & Left 55 & membership\\
1.1319 + \cdx{foldl} & $(\beta\To\alpha\To\beta) \To \beta \To \alpha\,list \To \beta$ &
1.1320 + & iteration \\
1.1321 + \cdx{concat} & $(\alpha\,list)list\To \alpha\,list$ & & concatenation \\
1.1322 + \cdx{rev} & $\alpha\,list \To \alpha\,list$ & & reverse \\
1.1323 + \cdx{length} & $\alpha\,list \To nat$ & & length \\
1.1324 + \tt! & $\alpha\,list \To nat \To \alpha$ & Left 100 & indexing \\
1.1325 + \cdx{take}, \cdx{drop} & $nat \To \alpha\,list \To \alpha\,list$ &&
1.1326 + take or drop a prefix \\
1.1327 + \cdx{takeWhile},\\
1.1328 + \cdx{dropWhile} &
1.1329 + $(\alpha \To bool) \To \alpha\,list \To \alpha\,list$ &&
1.1330 + take or drop a prefix
1.1331 +\end{constants}
1.1332 +\subcaption{Constants and infixes}
1.1333 +
1.1334 +\begin{center} \tt\frenchspacing
1.1335 +\begin{tabular}{rrr}
1.1336 + \it external & \it internal & \it description \\{}
1.1337 + [$x@1$, $\dots$, $x@n$] & $x@1$ \# $\cdots$ \# $x@n$ \# [] &
1.1338 + \rm finite list \\{}
1.1339 + [$x$:$l$. $P$] & filter ($\lambda x{.}P$) $l$ &
1.1340 + \rm list comprehension
1.1341 +\end{tabular}
1.1342 +\end{center}
1.1343 +\subcaption{Translations}
1.1344 +\caption{The theory \thydx{List}} \label{hol-list}
1.1345 +\end{figure}
1.1346 +
1.1347 +
1.1348 +\begin{figure}
1.1349 +\begin{ttbox}\makeatother
1.1350 +null [] = True
1.1351 +null (x#xs) = False
1.1352 +
1.1353 +hd (x#xs) = x
1.1354 +tl (x#xs) = xs
1.1355 +tl [] = []
1.1356 +
1.1357 +[] @ ys = ys
1.1358 +(x#xs) @ ys = x # xs @ ys
1.1359 +
1.1360 +map f [] = []
1.1361 +map f (x#xs) = f x # map f xs
1.1362 +
1.1363 +filter P [] = []
1.1364 +filter P (x#xs) = (if P x then x#filter P xs else filter P xs)
1.1365 +
1.1366 +set [] = \ttlbrace\ttrbrace
1.1367 +set (x#xs) = insert x (set xs)
1.1368 +
1.1369 +x mem [] = False
1.1370 +x mem (y#ys) = (if y=x then True else x mem ys)
1.1371 +
1.1372 +foldl f a [] = a
1.1373 +foldl f a (x#xs) = foldl f (f a x) xs
1.1374 +
1.1375 +concat([]) = []
1.1376 +concat(x#xs) = x @ concat(xs)
1.1377 +
1.1378 +rev([]) = []
1.1379 +rev(x#xs) = rev(xs) @ [x]
1.1380 +
1.1381 +length([]) = 0
1.1382 +length(x#xs) = Suc(length(xs))
1.1383 +
1.1384 +xs!0 = hd xs
1.1385 +xs!(Suc n) = (tl xs)!n
1.1386 +
1.1387 +take n [] = []
1.1388 +take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)
1.1389 +
1.1390 +drop n [] = []
1.1391 +drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)
1.1392 +
1.1393 +takeWhile P [] = []
1.1394 +takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])
1.1395 +
1.1396 +dropWhile P [] = []
1.1397 +dropWhile P (x#xs) = (if P x then dropWhile P xs else xs)
1.1398 +\end{ttbox}
1.1399 +\caption{Recursions equations for list processing functions}
1.1400 +\label{fig:HOL:list-simps}
1.1401 +\end{figure}
1.1402 +\index{nat@{\textit{nat}} type|)}
1.1403 +
1.1404 +
1.1405 +\subsection{The type constructor for lists, \textit{list}}
1.1406 +\label{subsec:list}
1.1407 +\index{list@{\textit{list}} type|(}
1.1408 +
1.1409 +Figure~\ref{hol-list} presents the theory \thydx{List}: the basic list
1.1410 +operations with their types and syntax. Type $\alpha \; list$ is
1.1411 +defined as a \texttt{datatype} with the constructors {\tt[]} and {\tt\#}.
1.1412 +As a result the generic structural induction and case analysis tactics
1.1413 +\texttt{induct\_tac} and \texttt{exhaust\_tac} also become available for
1.1414 +lists. A \sdx{case} construct of the form
1.1415 +\begin{center}\tt
1.1416 +case $e$ of [] => $a$ | \(x\)\#\(xs\) => b
1.1417 +\end{center}
1.1418 +is defined by translation. For details see~\S\ref{sec:HOL:datatype}. There
1.1419 +is also a case splitting rule \tdx{split_list_case}
1.1420 +\[
1.1421 +\begin{array}{l}
1.1422 +P(\mathtt{case}~e~\mathtt{of}~\texttt{[] =>}~a ~\texttt{|}~
1.1423 + x\texttt{\#}xs~\texttt{=>}~f~x~xs) ~= \\
1.1424 +((e = \texttt{[]} \to P(a)) \land
1.1425 + (\forall x~ xs. e = x\texttt{\#}xs \to P(f~x~xs)))
1.1426 +\end{array}
1.1427 +\]
1.1428 +which can be fed to \ttindex{addsplits} just like
1.1429 +\texttt{split_if} (see~\S\ref{subsec:HOL:case:splitting}).
1.1430 +
1.1431 +\texttt{List} provides a basic library of list processing functions defined by
1.1432 +primitive recursion (see~\S\ref{sec:HOL:primrec}). The recursion equations
1.1433 +are shown in Fig.\ts\ref{fig:HOL:list-simps}.
1.1434 +
1.1435 +\index{list@{\textit{list}} type|)}
1.1436 +
1.1437 +
1.1438 +\subsection{Introducing new types} \label{sec:typedef}
1.1439 +
1.1440 +The \HOL-methodology dictates that all extensions to a theory should
1.1441 +be \textbf{definitional}. The type definition mechanism that
1.1442 +meets this criterion is \ttindex{typedef}. Note that \emph{type synonyms},
1.1443 +which are inherited from {\Pure} and described elsewhere, are just
1.1444 +syntactic abbreviations that have no logical meaning.
1.1445 +
1.1446 +\begin{warn}
1.1447 + Types in \HOL\ must be non-empty; otherwise the quantifier rules would be
1.1448 + unsound, because $\exists x. x=x$ is a theorem \cite[\S7]{paulson-COLOG}.
1.1449 +\end{warn}
1.1450 +A \bfindex{type definition} identifies the new type with a subset of
1.1451 +an existing type. More precisely, the new type is defined by
1.1452 +exhibiting an existing type~$\tau$, a set~$A::\tau\,set$, and a
1.1453 +theorem of the form $x:A$. Thus~$A$ is a non-empty subset of~$\tau$,
1.1454 +and the new type denotes this subset. New functions are defined that
1.1455 +establish an isomorphism between the new type and the subset. If
1.1456 +type~$\tau$ involves type variables $\alpha@1$, \ldots, $\alpha@n$,
1.1457 +then the type definition creates a type constructor
1.1458 +$(\alpha@1,\ldots,\alpha@n)ty$ rather than a particular type.
1.1459 +
1.1460 +\begin{figure}[htbp]
1.1461 +\begin{rail}
1.1462 +typedef : 'typedef' ( () | '(' name ')') type '=' set witness;
1.1463 +
1.1464 +type : typevarlist name ( () | '(' infix ')' );
1.1465 +set : string;
1.1466 +witness : () | '(' id ')';
1.1467 +\end{rail}
1.1468 +\caption{Syntax of type definitions}
1.1469 +\label{fig:HOL:typedef}
1.1470 +\end{figure}
1.1471 +
1.1472 +The syntax for type definitions is shown in Fig.~\ref{fig:HOL:typedef}. For
1.1473 +the definition of `typevarlist' and `infix' see
1.1474 +\iflabelundefined{chap:classical}
1.1475 +{the appendix of the {\em Reference Manual\/}}%
1.1476 +{Appendix~\ref{app:TheorySyntax}}. The remaining nonterminals have the
1.1477 +following meaning:
1.1478 +\begin{description}
1.1479 +\item[\it type:] the new type constructor $(\alpha@1,\dots,\alpha@n)ty$ with
1.1480 + optional infix annotation.
1.1481 +\item[\it name:] an alphanumeric name $T$ for the type constructor
1.1482 + $ty$, in case $ty$ is a symbolic name. Defaults to $ty$.
1.1483 +\item[\it set:] the representing subset $A$.
1.1484 +\item[\it witness:] name of a theorem of the form $a:A$ proving
1.1485 + non-emptiness. It can be omitted in case Isabelle manages to prove
1.1486 + non-emptiness automatically.
1.1487 +\end{description}
1.1488 +If all context conditions are met (no duplicate type variables in
1.1489 +`typevarlist', no extra type variables in `set', and no free term variables
1.1490 +in `set'), the following components are added to the theory:
1.1491 +\begin{itemize}
1.1492 +\item a type $ty :: (term,\dots,term)term$
1.1493 +\item constants
1.1494 +\begin{eqnarray*}
1.1495 +T &::& \tau\;set \\
1.1496 +Rep_T &::& (\alpha@1,\dots,\alpha@n)ty \To \tau \\
1.1497 +Abs_T &::& \tau \To (\alpha@1,\dots,\alpha@n)ty
1.1498 +\end{eqnarray*}
1.1499 +\item a definition and three axioms
1.1500 +\[
1.1501 +\begin{array}{ll}
1.1502 +T{\tt_def} & T \equiv A \\
1.1503 +{\tt Rep_}T & Rep_T\,x \in T \\
1.1504 +{\tt Rep_}T{\tt_inverse} & Abs_T\,(Rep_T\,x) = x \\
1.1505 +{\tt Abs_}T{\tt_inverse} & y \in T \Imp Rep_T\,(Abs_T\,y) = y
1.1506 +\end{array}
1.1507 +\]
1.1508 +stating that $(\alpha@1,\dots,\alpha@n)ty$ is isomorphic to $A$ by $Rep_T$
1.1509 +and its inverse $Abs_T$.
1.1510 +\end{itemize}
1.1511 +Below are two simple examples of \HOL\ type definitions. Non-emptiness
1.1512 +is proved automatically here.
1.1513 +\begin{ttbox}
1.1514 +typedef unit = "{\ttlbrace}True{\ttrbrace}"
1.1515 +
1.1516 +typedef (prod)
1.1517 + ('a, 'b) "*" (infixr 20)
1.1518 + = "{\ttlbrace}f . EX (a::'a) (b::'b). f = (\%x y. x = a & y = b){\ttrbrace}"
1.1519 +\end{ttbox}
1.1520 +
1.1521 +Type definitions permit the introduction of abstract data types in a safe
1.1522 +way, namely by providing models based on already existing types. Given some
1.1523 +abstract axiomatic description $P$ of a type, this involves two steps:
1.1524 +\begin{enumerate}
1.1525 +\item Find an appropriate type $\tau$ and subset $A$ which has the desired
1.1526 + properties $P$, and make a type definition based on this representation.
1.1527 +\item Prove that $P$ holds for $ty$ by lifting $P$ from the representation.
1.1528 +\end{enumerate}
1.1529 +You can now forget about the representation and work solely in terms of the
1.1530 +abstract properties $P$.
1.1531 +
1.1532 +\begin{warn}
1.1533 +If you introduce a new type (constructor) $ty$ axiomatically, i.e.\ by
1.1534 +declaring the type and its operations and by stating the desired axioms, you
1.1535 +should make sure the type has a non-empty model. You must also have a clause
1.1536 +\par
1.1537 +\begin{ttbox}
1.1538 +arities \(ty\) :: (term,\thinspace\(\dots\),{\thinspace}term){\thinspace}term
1.1539 +\end{ttbox}
1.1540 +in your theory file to tell Isabelle that $ty$ is in class \texttt{term}, the
1.1541 +class of all \HOL\ types.
1.1542 +\end{warn}
1.1543 +
1.1544 +
1.1545 +\section{Records}
1.1546 +
1.1547 +At a first approximation, records are just a minor generalisation of tuples,
1.1548 +where components may be addressed by labels instead of just position (think of
1.1549 +{\ML}, for example). The version of records offered by Isabelle/HOL is
1.1550 +slightly more advanced, though, supporting \emph{extensible record schemes}.
1.1551 +This admits operations that are polymorphic with respect to record extension,
1.1552 +yielding ``object-oriented'' effects like (single) inheritance. See also
1.1553 +\cite{Naraschewski-Wenzel:1998:TPHOL} for more details on object-oriented
1.1554 +verification and record subtyping in HOL.
1.1555 +
1.1556 +
1.1557 +\subsection{Basics}
1.1558 +
1.1559 +Isabelle/HOL supports fixed and schematic records both at the level of terms
1.1560 +and types. The concrete syntax is as follows:
1.1561 +
1.1562 +\begin{center}
1.1563 +\begin{tabular}{l|l|l}
1.1564 + & record terms & record types \\ \hline
1.1565 + fixed & $\record{x = a\fs y = b}$ & $\record{x \ty A\fs y \ty B}$ \\
1.1566 + schematic & $\record{x = a\fs y = b\fs \more = m}$ &
1.1567 + $\record{x \ty A\fs y \ty B\fs \more \ty M}$ \\
1.1568 +\end{tabular}
1.1569 +\end{center}
1.1570 +
1.1571 +\noindent The \textsc{ascii} representation of $\record{x = a}$ is \texttt{(| x = a |)}.
1.1572 +
1.1573 +A fixed record $\record{x = a\fs y = b}$ has field $x$ of value $a$ and field
1.1574 +$y$ of value $b$. The corresponding type is $\record{x \ty A\fs y \ty B}$,
1.1575 +assuming that $a \ty A$ and $b \ty B$.
1.1576 +
1.1577 +A record scheme like $\record{x = a\fs y = b\fs \more = m}$ contains fields
1.1578 +$x$ and $y$ as before, but also possibly further fields as indicated by the
1.1579 +``$\more$'' notation (which is actually part of the syntax). The improper
1.1580 +field ``$\more$'' of a record scheme is called the \emph{more part}.
1.1581 +Logically it is just a free variable, which is occasionally referred to as
1.1582 +\emph{row variable} in the literature. The more part of a record scheme may
1.1583 +be instantiated by zero or more further components. For example, above scheme
1.1584 +might get instantiated to $\record{x = a\fs y = b\fs z = c\fs \more = m'}$,
1.1585 +where $m'$ refers to a different more part. Fixed records are special
1.1586 +instances of record schemes, where ``$\more$'' is properly terminated by the
1.1587 +$() :: unit$ element. Actually, $\record{x = a\fs y = b}$ is just an
1.1588 +abbreviation for $\record{x = a\fs y = b\fs \more = ()}$.
1.1589 +
1.1590 +\medskip
1.1591 +
1.1592 +There are two key features that make extensible records in a simply typed
1.1593 +language like HOL feasible:
1.1594 +\begin{enumerate}
1.1595 +\item the more part is internalised, as a free term or type variable,
1.1596 +\item field names are externalised, they cannot be accessed within the logic
1.1597 + as first-class values.
1.1598 +\end{enumerate}
1.1599 +
1.1600 +\medskip
1.1601 +
1.1602 +In Isabelle/HOL record types have to be defined explicitly, fixing their field
1.1603 +names and types, and their (optional) parent record (see
1.1604 +\S\ref{sec:HOL:record-def}). Afterwards, records may be formed using above
1.1605 +syntax, while obeying the canonical order of fields as given by their
1.1606 +declaration. The record package also provides several operations like
1.1607 +selectors and updates (see \S\ref{sec:HOL:record-ops}), together with
1.1608 +characteristic properties (see \S\ref{sec:HOL:record-thms}).
1.1609 +
1.1610 +There is an example theory demonstrating most basic aspects of extensible
1.1611 +records (see theory \texttt{HOL/ex/Points} in the Isabelle sources).
1.1612 +
1.1613 +
1.1614 +\subsection{Defining records}\label{sec:HOL:record-def}
1.1615 +
1.1616 +The theory syntax for record type definitions is shown in
1.1617 +Fig.~\ref{fig:HOL:record}. For the definition of `typevarlist' and `type' see
1.1618 +\iflabelundefined{chap:classical}
1.1619 +{the appendix of the {\em Reference Manual\/}}%
1.1620 +{Appendix~\ref{app:TheorySyntax}}.
1.1621 +
1.1622 +\begin{figure}[htbp]
1.1623 +\begin{rail}
1.1624 +record : 'record' typevarlist name '=' parent (field +);
1.1625 +
1.1626 +parent : ( () | type '+');
1.1627 +field : name '::' type;
1.1628 +\end{rail}
1.1629 +\caption{Syntax of record type definitions}
1.1630 +\label{fig:HOL:record}
1.1631 +\end{figure}
1.1632 +
1.1633 +A general \ttindex{record} specification is of the following form:
1.1634 +\[
1.1635 +\mathtt{record}~(\alpha@1, \dots, \alpha@n) \, t ~=~
1.1636 + (\tau@1, \dots, \tau@m) \, s ~+~ c@1 :: \sigma@1 ~ \dots ~ c@l :: \sigma@l
1.1637 +\]
1.1638 +where $\vec\alpha@n$ are distinct type variables, and $\vec\tau@m$,
1.1639 +$\vec\sigma@l$ are types containing at most variables from $\vec\alpha@n$.
1.1640 +Type constructor $t$ has to be new, while $s$ has to specify an existing
1.1641 +record type. Furthermore, the $\vec c@l$ have to be distinct field names.
1.1642 +There has to be at least one field.
1.1643 +
1.1644 +In principle, field names may never be shared with other records. This is no
1.1645 +actual restriction in practice, since $\vec c@l$ are internally declared
1.1646 +within a separate name space qualified by the name $t$ of the record.
1.1647 +
1.1648 +\medskip
1.1649 +
1.1650 +Above definition introduces a new record type $(\vec\alpha@n) \, t$ by
1.1651 +extending an existing one $(\vec\tau@m) \, s$ by new fields $\vec c@l \ty
1.1652 +\vec\sigma@l$. The parent record specification is optional, by omitting it
1.1653 +$t$ becomes a \emph{root record}. The hierarchy of all records declared
1.1654 +within a theory forms a forest structure, i.e.\ a set of trees, where any of
1.1655 +these is rooted by some root record.
1.1656 +
1.1657 +For convenience, $(\vec\alpha@n) \, t$ is made a type abbreviation for the
1.1658 +fixed record type $\record{\vec c@l \ty \vec\sigma@l}$, and $(\vec\alpha@n,
1.1659 +\zeta) \, t_scheme$ is made an abbreviation for $\record{\vec c@l \ty
1.1660 + \vec\sigma@l\fs \more \ty \zeta}$.
1.1661 +
1.1662 +\medskip
1.1663 +
1.1664 +The following simple example defines a root record type $point$ with fields $x
1.1665 +\ty nat$ and $y \ty nat$, and record type $cpoint$ by extending $point$ with
1.1666 +an additional $colour$ component.
1.1667 +
1.1668 +\begin{ttbox}
1.1669 + record point =
1.1670 + x :: nat
1.1671 + y :: nat
1.1672 +
1.1673 + record cpoint = point +
1.1674 + colour :: string
1.1675 +\end{ttbox}
1.1676 +
1.1677 +
1.1678 +\subsection{Record operations}\label{sec:HOL:record-ops}
1.1679 +
1.1680 +Any record definition of the form presented above produces certain standard
1.1681 +operations. Selectors and updates are provided for any field, including the
1.1682 +improper one ``$more$''. There are also cumulative record constructor
1.1683 +functions.
1.1684 +
1.1685 +To simplify the presentation below, we first assume that $(\vec\alpha@n) \, t$
1.1686 +is a root record with fields $\vec c@l \ty \vec\sigma@l$.
1.1687 +
1.1688 +\medskip
1.1689 +
1.1690 +\textbf{Selectors} and \textbf{updates} are available for any field (including
1.1691 +``$more$'') as follows:
1.1692 +\begin{matharray}{lll}
1.1693 + c@i & \ty & \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta} \To \sigma@i \\
1.1694 + c@i_update & \ty & \sigma@i \To \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta} \To
1.1695 + \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta}
1.1696 +\end{matharray}
1.1697 +
1.1698 +There is some special syntax for updates: $r \, \record{x \asn a}$ abbreviates
1.1699 +term $x_update \, a \, r$. Repeated updates are also supported: $r \,
1.1700 +\record{x \asn a} \, \record{y \asn b} \, \record{z \asn c}$ may be written as
1.1701 +$r \, \record{x \asn a\fs y \asn b\fs z \asn c}$. Note that because of
1.1702 +postfix notation the order of fields shown here is reverse than in the actual
1.1703 +term. This might lead to confusion in conjunction with proof tools like
1.1704 +ordered rewriting.
1.1705 +
1.1706 +Since repeated updates are just function applications, fields may be freely
1.1707 +permuted in $\record{x \asn a\fs y \asn b\fs z \asn c}$, as far as the logic
1.1708 +is concerned. Thus commutativity of updates can be proven within the logic
1.1709 +for any two fields, but not as a general theorem: fields are not first-class
1.1710 +values.
1.1711 +
1.1712 +\medskip
1.1713 +
1.1714 +\textbf{Make} operations provide cumulative record constructor functions:
1.1715 +\begin{matharray}{lll}
1.1716 + make & \ty & \vec\sigma@l \To \record{\vec c@l \ty \vec \sigma@l} \\
1.1717 + make_scheme & \ty & \vec\sigma@l \To
1.1718 + \zeta \To \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta} \\
1.1719 +\end{matharray}
1.1720 +\noindent
1.1721 +These functions are curried. The corresponding definitions in terms of actual
1.1722 +record terms are part of the standard simpset. Thus $point\dtt make\,a\,b$
1.1723 +rewrites to $\record{x = a\fs y = b}$.
1.1724 +
1.1725 +\medskip
1.1726 +
1.1727 +Any of above selector, update and make operations are declared within a local
1.1728 +name space prefixed by the name $t$ of the record. In case that different
1.1729 +records share base names of fields, one has to qualify names explicitly (e.g.\
1.1730 +$t\dtt c@i_update$). This is recommended especially for operations like
1.1731 +$make$ or $update_more$ that always have the same base name. Just use $t\dtt
1.1732 +make$ etc.\ to avoid confusion.
1.1733 +
1.1734 +\bigskip
1.1735 +
1.1736 +We reconsider the case of non-root records, which are derived of some parent
1.1737 +record. In general, the latter may depend on another parent as well,
1.1738 +resulting in a list of \emph{ancestor records}. Appending the lists of fields
1.1739 +of all ancestors results in a certain field prefix. The record package
1.1740 +automatically takes care of this by lifting operations over this context of
1.1741 +ancestor fields. Assuming that $(\vec\alpha@n) \, t$ has ancestor fields
1.1742 +$\vec d@k \ty \vec\rho@k$, selectors will get the following types:
1.1743 +\begin{matharray}{lll}
1.1744 + c@i & \ty & \record{\vec d@k \ty \vec\rho@k, \vec c@l \ty \vec \sigma@l, \more \ty \zeta}
1.1745 + \To \sigma@i
1.1746 +\end{matharray}
1.1747 +\noindent
1.1748 +Update and make operations are analogous.
1.1749 +
1.1750 +
1.1751 +\subsection{Proof tools}\label{sec:HOL:record-thms}
1.1752 +
1.1753 +The record package provides the following proof rules for any record type $t$.
1.1754 +\begin{enumerate}
1.1755 +
1.1756 +\item Standard conversions (selectors or updates applied to record constructor
1.1757 + terms, make function definitions) are part of the standard simpset (via
1.1758 + \texttt{addsimps}).
1.1759 +
1.1760 +\item Inject equations of a form analogous to $((x, y) = (x', y')) \equiv x=x'
1.1761 + \conj y=y'$ are made part of the standard simpset and claset (via
1.1762 + \texttt{addIffs}).
1.1763 +
1.1764 +\item A tactic for record field splitting (\ttindex{record_split_tac}) is made
1.1765 + part of the standard claset (via \texttt{addSWrapper}). This tactic is
1.1766 + based on rules analogous to $(\All x PROP~P~x) \equiv (\All{a~b} PROP~P(a,
1.1767 + b))$ for any field.
1.1768 +\end{enumerate}
1.1769 +
1.1770 +The first two kinds of rules are stored within the theory as $t\dtt simps$ and
1.1771 +$t\dtt iffs$, respectively. In some situations it might be appropriate to
1.1772 +expand the definitions of updates: $t\dtt updates$. Following a new trend in
1.1773 +Isabelle system architecture, these names are \emph{not} bound at the {\ML}
1.1774 +level, though.
1.1775 +
1.1776 +\medskip
1.1777 +
1.1778 +The example theory \texttt{HOL/ex/Points} demonstrates typical proofs
1.1779 +concerning records. The basic idea is to make \ttindex{record_split_tac}
1.1780 +expand quantified record variables and then simplify by the conversion rules.
1.1781 +By using a combination of the simplifier and classical prover together with
1.1782 +the default simpset and claset, record problems should be solved with a single
1.1783 +stroke of \texttt{Auto_tac} or \texttt{Force_tac}.
1.1784 +
1.1785 +
1.1786 +\section{Datatype definitions}
1.1787 +\label{sec:HOL:datatype}
1.1788 +\index{*datatype|(}
1.1789 +
1.1790 +Inductive datatypes, similar to those of \ML, frequently appear in
1.1791 +applications of Isabelle/HOL. In principle, such types could be defined by
1.1792 +hand via \texttt{typedef} (see \S\ref{sec:typedef}), but this would be far too
1.1793 +tedious. The \ttindex{datatype} definition package of \HOL\ automates such
1.1794 +chores. It generates an appropriate \texttt{typedef} based on a least
1.1795 +fixed-point construction, and proves freeness theorems and induction rules, as
1.1796 +well as theorems for recursion and case combinators. The user just has to
1.1797 +give a simple specification of new inductive types using a notation similar to
1.1798 +{\ML} or Haskell.
1.1799 +
1.1800 +The current datatype package can handle both mutual and indirect recursion.
1.1801 +It also offers to represent existing types as datatypes giving the advantage
1.1802 +of a more uniform view on standard theories.
1.1803 +
1.1804 +
1.1805 +\subsection{Basics}
1.1806 +\label{subsec:datatype:basics}
1.1807 +
1.1808 +A general \texttt{datatype} definition is of the following form:
1.1809 +\[
1.1810 +\begin{array}{llcl}
1.1811 +\mathtt{datatype} & (\alpha@1,\ldots,\alpha@h)t@1 & = &
1.1812 + C^1@1~\tau^1@{1,1}~\ldots~\tau^1@{1,m^1@1} ~\mid~ \ldots ~\mid~
1.1813 + C^1@{k@1}~\tau^1@{k@1,1}~\ldots~\tau^1@{k@1,m^1@{k@1}} \\
1.1814 + & & \vdots \\
1.1815 +\mathtt{and} & (\alpha@1,\ldots,\alpha@h)t@n & = &
1.1816 + C^n@1~\tau^n@{1,1}~\ldots~\tau^n@{1,m^n@1} ~\mid~ \ldots ~\mid~
1.1817 + C^n@{k@n}~\tau^n@{k@n,1}~\ldots~\tau^n@{k@n,m^n@{k@n}}
1.1818 +\end{array}
1.1819 +\]
1.1820 +where $\alpha@i$ are type variables, $C^j@i$ are distinct constructor
1.1821 +names and $\tau^j@{i,i'}$ are {\em admissible} types containing at
1.1822 +most the type variables $\alpha@1, \ldots, \alpha@h$. A type $\tau$
1.1823 +occurring in a \texttt{datatype} definition is {\em admissible} iff
1.1824 +\begin{itemize}
1.1825 +\item $\tau$ is non-recursive, i.e.\ $\tau$ does not contain any of the
1.1826 +newly defined type constructors $t@1,\ldots,t@n$, or
1.1827 +\item $\tau = (\alpha@1,\ldots,\alpha@h)t@{j'}$ where $1 \leq j' \leq n$, or
1.1828 +\item $\tau = (\tau'@1,\ldots,\tau'@{h'})t'$, where $t'$ is
1.1829 +the type constructor of an already existing datatype and $\tau'@1,\ldots,\tau'@{h'}$
1.1830 +are admissible types.
1.1831 +\end{itemize}
1.1832 +If some $(\alpha@1,\ldots,\alpha@h)t@{j'}$ occurs in a type $\tau^j@{i,i'}$
1.1833 +of the form
1.1834 +\[
1.1835 +(\ldots,\ldots ~ (\alpha@1,\ldots,\alpha@h)t@{j'} ~ \ldots,\ldots)t'
1.1836 +\]
1.1837 +this is called a {\em nested} (or \emph{indirect}) occurrence. A very simple
1.1838 +example of a datatype is the type \texttt{list}, which can be defined by
1.1839 +\begin{ttbox}
1.1840 +datatype 'a list = Nil
1.1841 + | Cons 'a ('a list)
1.1842 +\end{ttbox}
1.1843 +Arithmetic expressions \texttt{aexp} and boolean expressions \texttt{bexp} can be modelled
1.1844 +by the mutually recursive datatype definition
1.1845 +\begin{ttbox}
1.1846 +datatype 'a aexp = If_then_else ('a bexp) ('a aexp) ('a aexp)
1.1847 + | Sum ('a aexp) ('a aexp)
1.1848 + | Diff ('a aexp) ('a aexp)
1.1849 + | Var 'a
1.1850 + | Num nat
1.1851 +and 'a bexp = Less ('a aexp) ('a aexp)
1.1852 + | And ('a bexp) ('a bexp)
1.1853 + | Or ('a bexp) ('a bexp)
1.1854 +\end{ttbox}
1.1855 +The datatype \texttt{term}, which is defined by
1.1856 +\begin{ttbox}
1.1857 +datatype ('a, 'b) term = Var 'a
1.1858 + | App 'b ((('a, 'b) term) list)
1.1859 +\end{ttbox}
1.1860 +is an example for a datatype with nested recursion.
1.1861 +
1.1862 +\medskip
1.1863 +
1.1864 +Types in HOL must be non-empty. Each of the new datatypes
1.1865 +$(\alpha@1,\ldots,\alpha@h)t@j$ with $1 \le j \le n$ is non-empty iff it has a
1.1866 +constructor $C^j@i$ with the following property: for all argument types
1.1867 +$\tau^j@{i,i'}$ of the form $(\alpha@1,\ldots,\alpha@h)t@{j'}$ the datatype
1.1868 +$(\alpha@1,\ldots,\alpha@h)t@{j'}$ is non-empty.
1.1869 +
1.1870 +If there are no nested occurrences of the newly defined datatypes, obviously
1.1871 +at least one of the newly defined datatypes $(\alpha@1,\ldots,\alpha@h)t@j$
1.1872 +must have a constructor $C^j@i$ without recursive arguments, a \emph{base
1.1873 + case}, to ensure that the new types are non-empty. If there are nested
1.1874 +occurrences, a datatype can even be non-empty without having a base case
1.1875 +itself. Since \texttt{list} is a non-empty datatype, \texttt{datatype t = C (t
1.1876 + list)} is non-empty as well.
1.1877 +
1.1878 +
1.1879 +\subsubsection{Freeness of the constructors}
1.1880 +
1.1881 +The datatype constructors are automatically defined as functions of their
1.1882 +respective type:
1.1883 +\[ C^j@i :: [\tau^j@{i,1},\dots,\tau^j@{i,m^j@i}] \To (\alpha@1,\dots,\alpha@h)t@j \]
1.1884 +These functions have certain {\em freeness} properties. They construct
1.1885 +distinct values:
1.1886 +\[
1.1887 +C^j@i~x@1~\dots~x@{m^j@i} \neq C^j@{i'}~y@1~\dots~y@{m^j@{i'}} \qquad
1.1888 +\mbox{for all}~ i \neq i'.
1.1889 +\]
1.1890 +The constructor functions are injective:
1.1891 +\[
1.1892 +(C^j@i~x@1~\dots~x@{m^j@i} = C^j@i~y@1~\dots~y@{m^j@i}) =
1.1893 +(x@1 = y@1 \land \dots \land x@{m^j@i} = y@{m^j@i})
1.1894 +\]
1.1895 +Because the number of distinctness inequalities is quadratic in the number of
1.1896 +constructors, a different representation is used if there are $7$ or more of
1.1897 +them. In that case every constructor term is mapped to a natural number:
1.1898 +\[
1.1899 +t@j_ord \, (C^j@i \, x@1 \, \dots \, x@{m^j@i}) = i - 1
1.1900 +\]
1.1901 +Then distinctness of constructor terms is expressed by:
1.1902 +\[
1.1903 +t@j_ord \, x \neq t@j_ord \, y \Imp x \neq y.
1.1904 +\]
1.1905 +
1.1906 +\subsubsection{Structural induction}
1.1907 +
1.1908 +The datatype package also provides structural induction rules. For
1.1909 +datatypes without nested recursion, this is of the following form:
1.1910 +\[
1.1911 +\infer{P@1~x@1 \wedge \dots \wedge P@n~x@n}
1.1912 + {\begin{array}{lcl}
1.1913 + \Forall x@1 \dots x@{m^1@1}.
1.1914 + \List{P@{s^1@{1,1}}~x@{r^1@{1,1}}; \dots;
1.1915 + P@{s^1@{1,l^1@1}}~x@{r^1@{1,l^1@1}}} & \Imp &
1.1916 + P@1~\left(C^1@1~x@1~\dots~x@{m^1@1}\right) \\
1.1917 + & \vdots \\
1.1918 + \Forall x@1 \dots x@{m^1@{k@1}}.
1.1919 + \List{P@{s^1@{k@1,1}}~x@{r^1@{k@1,1}}; \dots;
1.1920 + P@{s^1@{k@1,l^1@{k@1}}}~x@{r^1@{k@1,l^1@{k@1}}}} & \Imp &
1.1921 + P@1~\left(C^1@{k@1}~x@1~\ldots~x@{m^1@{k@1}}\right) \\
1.1922 + & \vdots \\
1.1923 + \Forall x@1 \dots x@{m^n@1}.
1.1924 + \List{P@{s^n@{1,1}}~x@{r^n@{1,1}}; \dots;
1.1925 + P@{s^n@{1,l^n@1}}~x@{r^n@{1,l^n@1}}} & \Imp &
1.1926 + P@n~\left(C^n@1~x@1~\ldots~x@{m^n@1}\right) \\
1.1927 + & \vdots \\
1.1928 + \Forall x@1 \dots x@{m^n@{k@n}}.
1.1929 + \List{P@{s^n@{k@n,1}}~x@{r^n@{k@n,1}}; \dots
1.1930 + P@{s^n@{k@n,l^n@{k@n}}}~x@{r^n@{k@n,l^n@{k@n}}}} & \Imp &
1.1931 + P@n~\left(C^n@{k@n}~x@1~\ldots~x@{m^n@{k@n}}\right)
1.1932 + \end{array}}
1.1933 +\]
1.1934 +where
1.1935 +\[
1.1936 +\begin{array}{rcl}
1.1937 +Rec^j@i & := &
1.1938 + \left\{\left(r^j@{i,1},s^j@{i,1}\right),\ldots,
1.1939 + \left(r^j@{i,l^j@i},s^j@{i,l^j@i}\right)\right\} = \\[2ex]
1.1940 +&& \left\{(i',i'')~\left|~
1.1941 + 1\leq i' \leq m^j@i \wedge 1 \leq i'' \leq n \wedge
1.1942 + \tau^j@{i,i'} = (\alpha@1,\ldots,\alpha@h)t@{i''}\right.\right\}
1.1943 +\end{array}
1.1944 +\]
1.1945 +i.e.\ the properties $P@j$ can be assumed for all recursive arguments.
1.1946 +
1.1947 +For datatypes with nested recursion, such as the \texttt{term} example from
1.1948 +above, things are a bit more complicated. Conceptually, Isabelle/HOL unfolds
1.1949 +a definition like
1.1950 +\begin{ttbox}
1.1951 +datatype ('a, 'b) term = Var 'a
1.1952 + | App 'b ((('a, 'b) term) list)
1.1953 +\end{ttbox}
1.1954 +to an equivalent definition without nesting:
1.1955 +\begin{ttbox}
1.1956 +datatype ('a, 'b) term = Var
1.1957 + | App 'b (('a, 'b) term_list)
1.1958 +and ('a, 'b) term_list = Nil'
1.1959 + | Cons' (('a,'b) term) (('a,'b) term_list)
1.1960 +\end{ttbox}
1.1961 +Note however, that the type \texttt{('a,'b) term_list} and the constructors {\tt
1.1962 + Nil'} and \texttt{Cons'} are not really introduced. One can directly work with
1.1963 +the original (isomorphic) type \texttt{(('a, 'b) term) list} and its existing
1.1964 +constructors \texttt{Nil} and \texttt{Cons}. Thus, the structural induction rule for
1.1965 +\texttt{term} gets the form
1.1966 +\[
1.1967 +\infer{P@1~x@1 \wedge P@2~x@2}
1.1968 + {\begin{array}{l}
1.1969 + \Forall x.~P@1~(\mathtt{Var}~x) \\
1.1970 + \Forall x@1~x@2.~P@2~x@2 \Imp P@1~(\mathtt{App}~x@1~x@2) \\
1.1971 + P@2~\mathtt{Nil} \\
1.1972 + \Forall x@1~x@2. \List{P@1~x@1; P@2~x@2} \Imp P@2~(\mathtt{Cons}~x@1~x@2)
1.1973 + \end{array}}
1.1974 +\]
1.1975 +Note that there are two predicates $P@1$ and $P@2$, one for the type \texttt{('a,'b) term}
1.1976 +and one for the type \texttt{(('a, 'b) term) list}.
1.1977 +
1.1978 +\medskip In principle, inductive types are already fully determined by
1.1979 +freeness and structural induction. For convenience in applications,
1.1980 +the following derived constructions are automatically provided for any
1.1981 +datatype.
1.1982 +
1.1983 +\subsubsection{The \sdx{case} construct}
1.1984 +
1.1985 +The type comes with an \ML-like \texttt{case}-construct:
1.1986 +\[
1.1987 +\begin{array}{rrcl}
1.1988 +\mbox{\tt case}~e~\mbox{\tt of} & C^j@1~x@{1,1}~\dots~x@{1,m^j@1} & \To & e@1 \\
1.1989 + \vdots \\
1.1990 + \mid & C^j@{k@j}~x@{k@j,1}~\dots~x@{k@j,m^j@{k@j}} & \To & e@{k@j}
1.1991 +\end{array}
1.1992 +\]
1.1993 +where the $x@{i,j}$ are either identifiers or nested tuple patterns as in
1.1994 +\S\ref{subsec:prod-sum}.
1.1995 +\begin{warn}
1.1996 + All constructors must be present, their order is fixed, and nested patterns
1.1997 + are not supported (with the exception of tuples). Violating this
1.1998 + restriction results in strange error messages.
1.1999 +\end{warn}
1.2000 +
1.2001 +To perform case distinction on a goal containing a \texttt{case}-construct,
1.2002 +the theorem $t@j.$\texttt{split} is provided:
1.2003 +\[
1.2004 +\begin{array}{@{}rcl@{}}
1.2005 +P(t@j_\mathtt{case}~f@1~\dots~f@{k@j}~e) &\!\!\!=&
1.2006 +\!\!\! ((\forall x@1 \dots x@{m^j@1}. e = C^j@1~x@1\dots x@{m^j@1} \to
1.2007 + P(f@1~x@1\dots x@{m^j@1})) \\
1.2008 +&&\!\!\! ~\land~ \dots ~\land \\
1.2009 +&&~\!\!\! (\forall x@1 \dots x@{m^j@{k@j}}. e = C^j@{k@j}~x@1\dots x@{m^j@{k@j}} \to
1.2010 + P(f@{k@j}~x@1\dots x@{m^j@{k@j}})))
1.2011 +\end{array}
1.2012 +\]
1.2013 +where $t@j$\texttt{_case} is the internal name of the \texttt{case}-construct.
1.2014 +This theorem can be added to a simpset via \ttindex{addsplits}
1.2015 +(see~\S\ref{subsec:HOL:case:splitting}).
1.2016 +
1.2017 +\subsubsection{The function \cdx{size}}\label{sec:HOL:size}
1.2018 +
1.2019 +Theory \texttt{Arith} declares a generic function \texttt{size} of type
1.2020 +$\alpha\To nat$. Each datatype defines a particular instance of \texttt{size}
1.2021 +by overloading according to the following scheme:
1.2022 +%%% FIXME: This formula is too big and is completely unreadable
1.2023 +\[
1.2024 +size(C^j@i~x@1~\dots~x@{m^j@i}) = \!
1.2025 +\left\{
1.2026 +\begin{array}{ll}
1.2027 +0 & \!\mbox{if $Rec^j@i = \emptyset$} \\
1.2028 +\!\!\begin{array}{l}
1.2029 +size~x@{r^j@{i,1}} + \cdots \\
1.2030 +\cdots + size~x@{r^j@{i,l^j@i}} + 1
1.2031 +\end{array} &
1.2032 + \!\mbox{if $Rec^j@i = \left\{\left(r^j@{i,1},s^j@{i,1}\right),\ldots,
1.2033 + \left(r^j@{i,l^j@i},s^j@{i,l^j@i}\right)\right\}$}
1.2034 +\end{array}
1.2035 +\right.
1.2036 +\]
1.2037 +where $Rec^j@i$ is defined above. Viewing datatypes as generalised trees, the
1.2038 +size of a leaf is 0 and the size of a node is the sum of the sizes of its
1.2039 +subtrees ${}+1$.
1.2040 +
1.2041 +\subsection{Defining datatypes}
1.2042 +
1.2043 +The theory syntax for datatype definitions is shown in
1.2044 +Fig.~\ref{datatype-grammar}. In order to be well-formed, a datatype
1.2045 +definition has to obey the rules stated in the previous section. As a result
1.2046 +the theory is extended with the new types, the constructors, and the theorems
1.2047 +listed in the previous section.
1.2048 +
1.2049 +\begin{figure}
1.2050 +\begin{rail}
1.2051 +datatype : 'datatype' typedecls;
1.2052 +
1.2053 +typedecls: ( newtype '=' (cons + '|') ) + 'and'
1.2054 + ;
1.2055 +newtype : typevarlist id ( () | '(' infix ')' )
1.2056 + ;
1.2057 +cons : name (argtype *) ( () | ( '(' mixfix ')' ) )
1.2058 + ;
1.2059 +argtype : id | tid | ('(' typevarlist id ')')
1.2060 + ;
1.2061 +\end{rail}
1.2062 +\caption{Syntax of datatype declarations}
1.2063 +\label{datatype-grammar}
1.2064 +\end{figure}
1.2065 +
1.2066 +Most of the theorems about datatypes become part of the default simpset and
1.2067 +you never need to see them again because the simplifier applies them
1.2068 +automatically. Only induction or exhaustion are usually invoked by hand.
1.2069 +\begin{ttdescription}
1.2070 +\item[\ttindexbold{induct_tac} {\tt"}$x${\tt"} $i$]
1.2071 + applies structural induction on variable $x$ to subgoal $i$, provided the
1.2072 + type of $x$ is a datatype.
1.2073 +\item[\ttindexbold{mutual_induct_tac}
1.2074 + {\tt["}$x@1${\tt",}$\ldots${\tt,"}$x@n${\tt"]} $i$] applies simultaneous
1.2075 + structural induction on the variables $x@1,\ldots,x@n$ to subgoal $i$. This
1.2076 + is the canonical way to prove properties of mutually recursive datatypes
1.2077 + such as \texttt{aexp} and \texttt{bexp}, or datatypes with nested recursion such as
1.2078 + \texttt{term}.
1.2079 +\end{ttdescription}
1.2080 +In some cases, induction is overkill and a case distinction over all
1.2081 +constructors of the datatype suffices.
1.2082 +\begin{ttdescription}
1.2083 +\item[\ttindexbold{exhaust_tac} {\tt"}$u${\tt"} $i$]
1.2084 + performs an exhaustive case analysis for the term $u$ whose type
1.2085 + must be a datatype. If the datatype has $k@j$ constructors
1.2086 + $C^j@1$, \dots $C^j@{k@j}$, subgoal $i$ is replaced by $k@j$ new subgoals which
1.2087 + contain the additional assumption $u = C^j@{i'}~x@1~\dots~x@{m^j@{i'}}$ for
1.2088 + $i'=1$, $\dots$,~$k@j$.
1.2089 +\end{ttdescription}
1.2090 +
1.2091 +Note that induction is only allowed on free variables that should not occur
1.2092 +among the premises of the subgoal. Exhaustion applies to arbitrary terms.
1.2093 +
1.2094 +\bigskip
1.2095 +
1.2096 +
1.2097 +For the technically minded, we exhibit some more details. Processing the
1.2098 +theory file produces an \ML\ structure which, in addition to the usual
1.2099 +components, contains a structure named $t$ for each datatype $t$ defined in
1.2100 +the file. Each structure $t$ contains the following elements:
1.2101 +\begin{ttbox}
1.2102 +val distinct : thm list
1.2103 +val inject : thm list
1.2104 +val induct : thm
1.2105 +val exhaust : thm
1.2106 +val cases : thm list
1.2107 +val split : thm
1.2108 +val split_asm : thm
1.2109 +val recs : thm list
1.2110 +val size : thm list
1.2111 +val simps : thm list
1.2112 +\end{ttbox}
1.2113 +\texttt{distinct}, \texttt{inject}, \texttt{induct}, \texttt{size}
1.2114 +and \texttt{split} contain the theorems
1.2115 +described above. For user convenience, \texttt{distinct} contains
1.2116 +inequalities in both directions. The reduction rules of the {\tt
1.2117 + case}-construct are in \texttt{cases}. All theorems from {\tt
1.2118 + distinct}, \texttt{inject} and \texttt{cases} are combined in \texttt{simps}.
1.2119 +In case of mutually recursive datatypes, \texttt{recs}, \texttt{size}, \texttt{induct}
1.2120 +and \texttt{simps} are contained in a separate structure named $t@1_\ldots_t@n$.
1.2121 +
1.2122 +
1.2123 +\subsection{Representing existing types as datatypes}
1.2124 +
1.2125 +For foundational reasons, some basic types such as \texttt{nat}, \texttt{*}, {\tt
1.2126 + +}, \texttt{bool} and \texttt{unit} are not defined in a \texttt{datatype} section,
1.2127 +but by more primitive means using \texttt{typedef}. To be able to use the
1.2128 +tactics \texttt{induct_tac} and \texttt{exhaust_tac} and to define functions by
1.2129 +primitive recursion on these types, such types may be represented as actual
1.2130 +datatypes. This is done by specifying an induction rule, as well as theorems
1.2131 +stating the distinctness and injectivity of constructors in a {\tt
1.2132 + rep_datatype} section. For type \texttt{nat} this works as follows:
1.2133 +\begin{ttbox}
1.2134 +rep_datatype nat
1.2135 + distinct Suc_not_Zero, Zero_not_Suc
1.2136 + inject Suc_Suc_eq
1.2137 + induct nat_induct
1.2138 +\end{ttbox}
1.2139 +The datatype package automatically derives additional theorems for recursion
1.2140 +and case combinators from these rules. Any of the basic HOL types mentioned
1.2141 +above are represented as datatypes. Try an induction on \texttt{bool}
1.2142 +today.
1.2143 +
1.2144 +
1.2145 +\subsection{Examples}
1.2146 +
1.2147 +\subsubsection{The datatype $\alpha~mylist$}
1.2148 +
1.2149 +We want to define a type $\alpha~mylist$. To do this we have to build a new
1.2150 +theory that contains the type definition. We start from the theory
1.2151 +\texttt{Datatype} instead of \texttt{Main} in order to avoid clashes with the
1.2152 +\texttt{List} theory of Isabelle/HOL.
1.2153 +\begin{ttbox}
1.2154 +MyList = Datatype +
1.2155 + datatype 'a mylist = Nil | Cons 'a ('a mylist)
1.2156 +end
1.2157 +\end{ttbox}
1.2158 +After loading the theory, we can prove $Cons~x~xs\neq xs$, for example. To
1.2159 +ease the induction applied below, we state the goal with $x$ quantified at the
1.2160 +object-level. This will be stripped later using \ttindex{qed_spec_mp}.
1.2161 +\begin{ttbox}
1.2162 +Goal "!x. Cons x xs ~= xs";
1.2163 +{\out Level 0}
1.2164 +{\out ! x. Cons x xs ~= xs}
1.2165 +{\out 1. ! x. Cons x xs ~= xs}
1.2166 +\end{ttbox}
1.2167 +This can be proved by the structural induction tactic:
1.2168 +\begin{ttbox}
1.2169 +by (induct_tac "xs" 1);
1.2170 +{\out Level 1}
1.2171 +{\out ! x. Cons x xs ~= xs}
1.2172 +{\out 1. ! x. Cons x Nil ~= Nil}
1.2173 +{\out 2. !!a mylist.}
1.2174 +{\out ! x. Cons x mylist ~= mylist ==>}
1.2175 +{\out ! x. Cons x (Cons a mylist) ~= Cons a mylist}
1.2176 +\end{ttbox}
1.2177 +The first subgoal can be proved using the simplifier. Isabelle/HOL has
1.2178 +already added the freeness properties of lists to the default simplification
1.2179 +set.
1.2180 +\begin{ttbox}
1.2181 +by (Simp_tac 1);
1.2182 +{\out Level 2}
1.2183 +{\out ! x. Cons x xs ~= xs}
1.2184 +{\out 1. !!a mylist.}
1.2185 +{\out ! x. Cons x mylist ~= mylist ==>}
1.2186 +{\out ! x. Cons x (Cons a mylist) ~= Cons a mylist}
1.2187 +\end{ttbox}
1.2188 +Similarly, we prove the remaining goal.
1.2189 +\begin{ttbox}
1.2190 +by (Asm_simp_tac 1);
1.2191 +{\out Level 3}
1.2192 +{\out ! x. Cons x xs ~= xs}
1.2193 +{\out No subgoals!}
1.2194 +\ttbreak
1.2195 +qed_spec_mp "not_Cons_self";
1.2196 +{\out val not_Cons_self = "Cons x xs ~= xs" : thm}
1.2197 +\end{ttbox}
1.2198 +Because both subgoals could have been proved by \texttt{Asm_simp_tac}
1.2199 +we could have done that in one step:
1.2200 +\begin{ttbox}
1.2201 +by (ALLGOALS Asm_simp_tac);
1.2202 +\end{ttbox}
1.2203 +
1.2204 +
1.2205 +\subsubsection{The datatype $\alpha~mylist$ with mixfix syntax}
1.2206 +
1.2207 +In this example we define the type $\alpha~mylist$ again but this time
1.2208 +we want to write \texttt{[]} for \texttt{Nil} and we want to use infix
1.2209 +notation \verb|#| for \texttt{Cons}. To do this we simply add mixfix
1.2210 +annotations after the constructor declarations as follows:
1.2211 +\begin{ttbox}
1.2212 +MyList = Datatype +
1.2213 + datatype 'a mylist =
1.2214 + Nil ("[]") |
1.2215 + Cons 'a ('a mylist) (infixr "#" 70)
1.2216 +end
1.2217 +\end{ttbox}
1.2218 +Now the theorem in the previous example can be written \verb|x#xs ~= xs|.
1.2219 +
1.2220 +
1.2221 +\subsubsection{A datatype for weekdays}
1.2222 +
1.2223 +This example shows a datatype that consists of 7 constructors:
1.2224 +\begin{ttbox}
1.2225 +Days = Main +
1.2226 + datatype days = Mon | Tue | Wed | Thu | Fri | Sat | Sun
1.2227 +end
1.2228 +\end{ttbox}
1.2229 +Because there are more than 6 constructors, inequality is expressed via a function
1.2230 +\verb|days_ord|. The theorem \verb|Mon ~= Tue| is not directly
1.2231 +contained among the distinctness theorems, but the simplifier can
1.2232 +prove it thanks to rewrite rules inherited from theory \texttt{Arith}:
1.2233 +\begin{ttbox}
1.2234 +Goal "Mon ~= Tue";
1.2235 +by (Simp_tac 1);
1.2236 +\end{ttbox}
1.2237 +You need not derive such inequalities explicitly: the simplifier will dispose
1.2238 +of them automatically.
1.2239 +\index{*datatype|)}
1.2240 +
1.2241 +
1.2242 +\section{Recursive function definitions}\label{sec:HOL:recursive}
1.2243 +\index{recursive functions|see{recursion}}
1.2244 +
1.2245 +Isabelle/HOL provides two main mechanisms of defining recursive functions.
1.2246 +\begin{enumerate}
1.2247 +\item \textbf{Primitive recursion} is available only for datatypes, and it is
1.2248 + somewhat restrictive. Recursive calls are only allowed on the argument's
1.2249 + immediate constituents. On the other hand, it is the form of recursion most
1.2250 + often wanted, and it is easy to use.
1.2251 +
1.2252 +\item \textbf{Well-founded recursion} requires that you supply a well-founded
1.2253 + relation that governs the recursion. Recursive calls are only allowed if
1.2254 + they make the argument decrease under the relation. Complicated recursion
1.2255 + forms, such as nested recursion, can be dealt with. Termination can even be
1.2256 + proved at a later time, though having unsolved termination conditions around
1.2257 + can make work difficult.%
1.2258 + \footnote{This facility is based on Konrad Slind's TFL
1.2259 + package~\cite{slind-tfl}. Thanks are due to Konrad for implementing TFL
1.2260 + and assisting with its installation.}
1.2261 +\end{enumerate}
1.2262 +
1.2263 +Following good HOL tradition, these declarations do not assert arbitrary
1.2264 +axioms. Instead, they define the function using a recursion operator. Both
1.2265 +HOL and ZF derive the theory of well-founded recursion from first
1.2266 +principles~\cite{paulson-set-II}. Primitive recursion over some datatype
1.2267 +relies on the recursion operator provided by the datatype package. With
1.2268 +either form of function definition, Isabelle proves the desired recursion
1.2269 +equations as theorems.
1.2270 +
1.2271 +
1.2272 +\subsection{Primitive recursive functions}
1.2273 +\label{sec:HOL:primrec}
1.2274 +\index{recursion!primitive|(}
1.2275 +\index{*primrec|(}
1.2276 +
1.2277 +Datatypes come with a uniform way of defining functions, {\bf primitive
1.2278 + recursion}. In principle, one could introduce primitive recursive functions
1.2279 +by asserting their reduction rules as new axioms, but this is not recommended:
1.2280 +\begin{ttbox}\slshape
1.2281 +Append = Main +
1.2282 +consts app :: ['a list, 'a list] => 'a list
1.2283 +rules
1.2284 + app_Nil "app [] ys = ys"
1.2285 + app_Cons "app (x#xs) ys = x#app xs ys"
1.2286 +end
1.2287 +\end{ttbox}
1.2288 +Asserting axioms brings the danger of accidentally asserting nonsense, as
1.2289 +in \verb$app [] ys = us$.
1.2290 +
1.2291 +The \ttindex{primrec} declaration is a safe means of defining primitive
1.2292 +recursive functions on datatypes:
1.2293 +\begin{ttbox}
1.2294 +Append = Main +
1.2295 +consts app :: ['a list, 'a list] => 'a list
1.2296 +primrec
1.2297 + "app [] ys = ys"
1.2298 + "app (x#xs) ys = x#app xs ys"
1.2299 +end
1.2300 +\end{ttbox}
1.2301 +Isabelle will now check that the two rules do indeed form a primitive
1.2302 +recursive definition. For example
1.2303 +\begin{ttbox}
1.2304 +primrec
1.2305 + "app [] ys = us"
1.2306 +\end{ttbox}
1.2307 +is rejected with an error message ``\texttt{Extra variables on rhs}''.
1.2308 +
1.2309 +\bigskip
1.2310 +
1.2311 +The general form of a primitive recursive definition is
1.2312 +\begin{ttbox}
1.2313 +primrec
1.2314 + {\it reduction rules}
1.2315 +\end{ttbox}
1.2316 +where \textit{reduction rules} specify one or more equations of the form
1.2317 +\[ f \, x@1 \, \dots \, x@m \, (C \, y@1 \, \dots \, y@k) \, z@1 \,
1.2318 +\dots \, z@n = r \] such that $C$ is a constructor of the datatype, $r$
1.2319 +contains only the free variables on the left-hand side, and all recursive
1.2320 +calls in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$. There
1.2321 +must be at most one reduction rule for each constructor. The order is
1.2322 +immaterial. For missing constructors, the function is defined to return a
1.2323 +default value.
1.2324 +
1.2325 +If you would like to refer to some rule by name, then you must prefix
1.2326 +the rule with an identifier. These identifiers, like those in the
1.2327 +\texttt{rules} section of a theory, will be visible at the \ML\ level.
1.2328 +
1.2329 +The primitive recursive function can have infix or mixfix syntax:
1.2330 +\begin{ttbox}\underscoreon
1.2331 +consts "@" :: ['a list, 'a list] => 'a list (infixr 60)
1.2332 +primrec
1.2333 + "[] @ ys = ys"
1.2334 + "(x#xs) @ ys = x#(xs @ ys)"
1.2335 +\end{ttbox}
1.2336 +
1.2337 +The reduction rules become part of the default simpset, which
1.2338 +leads to short proof scripts:
1.2339 +\begin{ttbox}\underscoreon
1.2340 +Goal "(xs @ ys) @ zs = xs @ (ys @ zs)";
1.2341 +by (induct\_tac "xs" 1);
1.2342 +by (ALLGOALS Asm\_simp\_tac);
1.2343 +\end{ttbox}
1.2344 +
1.2345 +\subsubsection{Example: Evaluation of expressions}
1.2346 +Using mutual primitive recursion, we can define evaluation functions \texttt{eval_aexp}
1.2347 +and \texttt{eval_bexp} for the datatypes of arithmetic and boolean expressions mentioned in
1.2348 +\S\ref{subsec:datatype:basics}:
1.2349 +\begin{ttbox}
1.2350 +consts
1.2351 + eval_aexp :: "['a => nat, 'a aexp] => nat"
1.2352 + eval_bexp :: "['a => nat, 'a bexp] => bool"
1.2353 +
1.2354 +primrec
1.2355 + "eval_aexp env (If_then_else b a1 a2) =
1.2356 + (if eval_bexp env b then eval_aexp env a1 else eval_aexp env a2)"
1.2357 + "eval_aexp env (Sum a1 a2) = eval_aexp env a1 + eval_aexp env a2"
1.2358 + "eval_aexp env (Diff a1 a2) = eval_aexp env a1 - eval_aexp env a2"
1.2359 + "eval_aexp env (Var v) = env v"
1.2360 + "eval_aexp env (Num n) = n"
1.2361 +
1.2362 + "eval_bexp env (Less a1 a2) = (eval_aexp env a1 < eval_aexp env a2)"
1.2363 + "eval_bexp env (And b1 b2) = (eval_bexp env b1 & eval_bexp env b2)"
1.2364 + "eval_bexp env (Or b1 b2) = (eval_bexp env b1 & eval_bexp env b2)"
1.2365 +\end{ttbox}
1.2366 +Since the value of an expression depends on the value of its variables,
1.2367 +the functions \texttt{eval_aexp} and \texttt{eval_bexp} take an additional
1.2368 +parameter, an {\em environment} of type \texttt{'a => nat}, which maps
1.2369 +variables to their values.
1.2370 +
1.2371 +Similarly, we may define substitution functions \texttt{subst_aexp}
1.2372 +and \texttt{subst_bexp} for expressions: The mapping \texttt{f} of type
1.2373 +\texttt{'a => 'a aexp} given as a parameter is lifted canonically
1.2374 +on the types {'a aexp} and {'a bexp}:
1.2375 +\begin{ttbox}
1.2376 +consts
1.2377 + subst_aexp :: "['a => 'b aexp, 'a aexp] => 'b aexp"
1.2378 + subst_bexp :: "['a => 'b aexp, 'a bexp] => 'b bexp"
1.2379 +
1.2380 +primrec
1.2381 + "subst_aexp f (If_then_else b a1 a2) =
1.2382 + If_then_else (subst_bexp f b) (subst_aexp f a1) (subst_aexp f a2)"
1.2383 + "subst_aexp f (Sum a1 a2) = Sum (subst_aexp f a1) (subst_aexp f a2)"
1.2384 + "subst_aexp f (Diff a1 a2) = Diff (subst_aexp f a1) (subst_aexp f a2)"
1.2385 + "subst_aexp f (Var v) = f v"
1.2386 + "subst_aexp f (Num n) = Num n"
1.2387 +
1.2388 + "subst_bexp f (Less a1 a2) = Less (subst_aexp f a1) (subst_aexp f a2)"
1.2389 + "subst_bexp f (And b1 b2) = And (subst_bexp f b1) (subst_bexp f b2)"
1.2390 + "subst_bexp f (Or b1 b2) = Or (subst_bexp f b1) (subst_bexp f b2)"
1.2391 +\end{ttbox}
1.2392 +In textbooks about semantics one often finds {\em substitution theorems},
1.2393 +which express the relationship between substitution and evaluation. For
1.2394 +\texttt{'a aexp} and \texttt{'a bexp}, we can prove such a theorem by mutual
1.2395 +induction, followed by simplification:
1.2396 +\begin{ttbox}
1.2397 +Goal
1.2398 + "eval_aexp env (subst_aexp (Var(v := a')) a) =
1.2399 + eval_aexp (env(v := eval_aexp env a')) a &
1.2400 + eval_bexp env (subst_bexp (Var(v := a')) b) =
1.2401 + eval_bexp (env(v := eval_aexp env a')) b";
1.2402 +by (mutual_induct_tac ["a","b"] 1);
1.2403 +by (ALLGOALS Asm_full_simp_tac);
1.2404 +\end{ttbox}
1.2405 +
1.2406 +\subsubsection{Example: A substitution function for terms}
1.2407 +Functions on datatypes with nested recursion, such as the type
1.2408 +\texttt{term} mentioned in \S\ref{subsec:datatype:basics}, are
1.2409 +also defined by mutual primitive recursion. A substitution
1.2410 +function \texttt{subst_term} on type \texttt{term}, similar to the functions
1.2411 +\texttt{subst_aexp} and \texttt{subst_bexp} described above, can
1.2412 +be defined as follows:
1.2413 +\begin{ttbox}
1.2414 +consts
1.2415 + subst_term :: "['a => ('a, 'b) term, ('a, 'b) term] => ('a, 'b) term"
1.2416 + subst_term_list ::
1.2417 + "['a => ('a, 'b) term, ('a, 'b) term list] => ('a, 'b) term list"
1.2418 +
1.2419 +primrec
1.2420 + "subst_term f (Var a) = f a"
1.2421 + "subst_term f (App b ts) = App b (subst_term_list f ts)"
1.2422 +
1.2423 + "subst_term_list f [] = []"
1.2424 + "subst_term_list f (t # ts) =
1.2425 + subst_term f t # subst_term_list f ts"
1.2426 +\end{ttbox}
1.2427 +The recursion scheme follows the structure of the unfolded definition of type
1.2428 +\texttt{term} shown in \S\ref{subsec:datatype:basics}. To prove properties of
1.2429 +this substitution function, mutual induction is needed:
1.2430 +\begin{ttbox}
1.2431 +Goal
1.2432 + "(subst_term ((subst_term f1) o f2) t) =
1.2433 + (subst_term f1 (subst_term f2 t)) &
1.2434 + (subst_term_list ((subst_term f1) o f2) ts) =
1.2435 + (subst_term_list f1 (subst_term_list f2 ts))";
1.2436 +by (mutual_induct_tac ["t", "ts"] 1);
1.2437 +by (ALLGOALS Asm_full_simp_tac);
1.2438 +\end{ttbox}
1.2439 +
1.2440 +\index{recursion!primitive|)}
1.2441 +\index{*primrec|)}
1.2442 +
1.2443 +
1.2444 +\subsection{General recursive functions}
1.2445 +\label{sec:HOL:recdef}
1.2446 +\index{recursion!general|(}
1.2447 +\index{*recdef|(}
1.2448 +
1.2449 +Using \texttt{recdef}, you can declare functions involving nested recursion
1.2450 +and pattern-matching. Recursion need not involve datatypes and there are few
1.2451 +syntactic restrictions. Termination is proved by showing that each recursive
1.2452 +call makes the argument smaller in a suitable sense, which you specify by
1.2453 +supplying a well-founded relation.
1.2454 +
1.2455 +Here is a simple example, the Fibonacci function. The first line declares
1.2456 +\texttt{fib} to be a constant. The well-founded relation is simply~$<$ (on
1.2457 +the natural numbers). Pattern-matching is used here: \texttt{1} is a
1.2458 +macro for \texttt{Suc~0}.
1.2459 +\begin{ttbox}
1.2460 +consts fib :: "nat => nat"
1.2461 +recdef fib "less_than"
1.2462 + "fib 0 = 0"
1.2463 + "fib 1 = 1"
1.2464 + "fib (Suc(Suc x)) = (fib x + fib (Suc x))"
1.2465 +\end{ttbox}
1.2466 +
1.2467 +With \texttt{recdef}, function definitions may be incomplete, and patterns may
1.2468 +overlap, as in functional programming. The \texttt{recdef} package
1.2469 +disambiguates overlapping patterns by taking the order of rules into account.
1.2470 +For missing patterns, the function is defined to return a default value.
1.2471 +
1.2472 +%For example, here is a declaration of the list function \cdx{hd}:
1.2473 +%\begin{ttbox}
1.2474 +%consts hd :: 'a list => 'a
1.2475 +%recdef hd "\{\}"
1.2476 +% "hd (x#l) = x"
1.2477 +%\end{ttbox}
1.2478 +%Because this function is not recursive, we may supply the empty well-founded
1.2479 +%relation, $\{\}$.
1.2480 +
1.2481 +The well-founded relation defines a notion of ``smaller'' for the function's
1.2482 +argument type. The relation $\prec$ is \textbf{well-founded} provided it
1.2483 +admits no infinitely decreasing chains
1.2484 +\[ \cdots\prec x@n\prec\cdots\prec x@1. \]
1.2485 +If the function's argument has type~$\tau$, then $\prec$ has to be a relation
1.2486 +over~$\tau$: it must have type $(\tau\times\tau)set$.
1.2487 +
1.2488 +Proving well-foundedness can be tricky, so Isabelle/HOL provides a collection
1.2489 +of operators for building well-founded relations. The package recognises
1.2490 +these operators and automatically proves that the constructed relation is
1.2491 +well-founded. Here are those operators, in order of importance:
1.2492 +\begin{itemize}
1.2493 +\item \texttt{less_than} is ``less than'' on the natural numbers.
1.2494 + (It has type $(nat\times nat)set$, while $<$ has type $[nat,nat]\To bool$.
1.2495 +
1.2496 +\item $\mathop{\mathtt{measure}} f$, where $f$ has type $\tau\To nat$, is the
1.2497 + relation~$\prec$ on type~$\tau$ such that $x\prec y$ iff $f(x)<f(y)$.
1.2498 + Typically, $f$ takes the recursive function's arguments (as a tuple) and
1.2499 + returns a result expressed in terms of the function \texttt{size}. It is
1.2500 + called a \textbf{measure function}. Recall that \texttt{size} is overloaded
1.2501 + and is defined on all datatypes (see \S\ref{sec:HOL:size}).
1.2502 +
1.2503 +\item $\mathop{\mathtt{inv_image}} f\;R$ is a generalisation of
1.2504 + \texttt{measure}. It specifies a relation such that $x\prec y$ iff $f(x)$
1.2505 + is less than $f(y)$ according to~$R$, which must itself be a well-founded
1.2506 + relation.
1.2507 +
1.2508 +\item $R@1\texttt{**}R@2$ is the lexicographic product of two relations. It
1.2509 + is a relation on pairs and satisfies $(x@1,x@2)\prec(y@1,y@2)$ iff $x@1$
1.2510 + is less than $y@1$ according to~$R@1$ or $x@1=y@1$ and $x@2$
1.2511 + is less than $y@2$ according to~$R@2$.
1.2512 +
1.2513 +\item \texttt{finite_psubset} is the proper subset relation on finite sets.
1.2514 +\end{itemize}
1.2515 +
1.2516 +We can use \texttt{measure} to declare Euclid's algorithm for the greatest
1.2517 +common divisor. The measure function, $\lambda(m,n). n$, specifies that the
1.2518 +recursion terminates because argument~$n$ decreases.
1.2519 +\begin{ttbox}
1.2520 +recdef gcd "measure ((\%(m,n). n) ::nat*nat=>nat)"
1.2521 + "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
1.2522 +\end{ttbox}
1.2523 +
1.2524 +The general form of a well-founded recursive definition is
1.2525 +\begin{ttbox}
1.2526 +recdef {\it function} {\it rel}
1.2527 + congs {\it congruence rules} {\bf(optional)}
1.2528 + simpset {\it simplification set} {\bf(optional)}
1.2529 + {\it reduction rules}
1.2530 +\end{ttbox}
1.2531 +where
1.2532 +\begin{itemize}
1.2533 +\item \textit{function} is the name of the function, either as an \textit{id}
1.2534 + or a \textit{string}.
1.2535 +
1.2536 +\item \textit{rel} is a {\HOL} expression for the well-founded termination
1.2537 + relation.
1.2538 +
1.2539 +\item \textit{congruence rules} are required only in highly exceptional
1.2540 + circumstances.
1.2541 +
1.2542 +\item The \textit{simplification set} is used to prove that the supplied
1.2543 + relation is well-founded. It is also used to prove the \textbf{termination
1.2544 + conditions}: assertions that arguments of recursive calls decrease under
1.2545 + \textit{rel}. By default, simplification uses \texttt{simpset()}, which
1.2546 + is sufficient to prove well-foundedness for the built-in relations listed
1.2547 + above.
1.2548 +
1.2549 +\item \textit{reduction rules} specify one or more recursion equations. Each
1.2550 + left-hand side must have the form $f\,t$, where $f$ is the function and $t$
1.2551 + is a tuple of distinct variables. If more than one equation is present then
1.2552 + $f$ is defined by pattern-matching on components of its argument whose type
1.2553 + is a \texttt{datatype}.
1.2554 +
1.2555 + Unlike with \texttt{primrec}, the reduction rules are not added to the
1.2556 + default simpset, and individual rules may not be labelled with identifiers.
1.2557 + However, the identifier $f$\texttt{.rules} is visible at the \ML\ level
1.2558 + as a list of theorems.
1.2559 +\end{itemize}
1.2560 +
1.2561 +With the definition of \texttt{gcd} shown above, Isabelle/HOL is unable to
1.2562 +prove one termination condition. It remains as a precondition of the
1.2563 +recursion theorems.
1.2564 +\begin{ttbox}
1.2565 +gcd.rules;
1.2566 +{\out ["! m n. n ~= 0 --> m mod n < n}
1.2567 +{\out ==> gcd (?m, ?n) = (if ?n = 0 then ?m else gcd (?n, ?m mod ?n))"] }
1.2568 +{\out : thm list}
1.2569 +\end{ttbox}
1.2570 +The theory \texttt{HOL/ex/Primes} illustrates how to prove termination
1.2571 +conditions afterwards. The function \texttt{Tfl.tgoalw} is like the standard
1.2572 +function \texttt{goalw}, which sets up a goal to prove, but its argument
1.2573 +should be the identifier $f$\texttt{.rules} and its effect is to set up a
1.2574 +proof of the termination conditions:
1.2575 +\begin{ttbox}
1.2576 +Tfl.tgoalw thy [] gcd.rules;
1.2577 +{\out Level 0}
1.2578 +{\out ! m n. n ~= 0 --> m mod n < n}
1.2579 +{\out 1. ! m n. n ~= 0 --> m mod n < n}
1.2580 +\end{ttbox}
1.2581 +This subgoal has a one-step proof using \texttt{simp_tac}. Once the theorem
1.2582 +is proved, it can be used to eliminate the termination conditions from
1.2583 +elements of \texttt{gcd.rules}. Theory \texttt{HOL/Subst/Unify} is a much
1.2584 +more complicated example of this process, where the termination conditions can
1.2585 +only be proved by complicated reasoning involving the recursive function
1.2586 +itself.
1.2587 +
1.2588 +Isabelle/HOL can prove the \texttt{gcd} function's termination condition
1.2589 +automatically if supplied with the right simpset.
1.2590 +\begin{ttbox}
1.2591 +recdef gcd "measure ((\%(m,n). n) ::nat*nat=>nat)"
1.2592 + simpset "simpset() addsimps [mod_less_divisor, zero_less_eq]"
1.2593 + "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
1.2594 +\end{ttbox}
1.2595 +
1.2596 +A \texttt{recdef} definition also returns an induction rule specialised for
1.2597 +the recursive function. For the \texttt{gcd} function above, the induction
1.2598 +rule is
1.2599 +\begin{ttbox}
1.2600 +gcd.induct;
1.2601 +{\out "(!!m n. n ~= 0 --> ?P n (m mod n) ==> ?P m n) ==> ?P ?u ?v" : thm}
1.2602 +\end{ttbox}
1.2603 +This rule should be used to reason inductively about the \texttt{gcd}
1.2604 +function. It usually makes the induction hypothesis available at all
1.2605 +recursive calls, leading to very direct proofs. If any termination conditions
1.2606 +remain unproved, they will become additional premises of this rule.
1.2607 +
1.2608 +\index{recursion!general|)}
1.2609 +\index{*recdef|)}
1.2610 +
1.2611 +
1.2612 +\section{Inductive and coinductive definitions}
1.2613 +\index{*inductive|(}
1.2614 +\index{*coinductive|(}
1.2615 +
1.2616 +An {\bf inductive definition} specifies the least set~$R$ closed under given
1.2617 +rules. (Applying a rule to elements of~$R$ yields a result within~$R$.) For
1.2618 +example, a structural operational semantics is an inductive definition of an
1.2619 +evaluation relation. Dually, a {\bf coinductive definition} specifies the
1.2620 +greatest set~$R$ consistent with given rules. (Every element of~$R$ can be
1.2621 +seen as arising by applying a rule to elements of~$R$.) An important example
1.2622 +is using bisimulation relations to formalise equivalence of processes and
1.2623 +infinite data structures.
1.2624 +
1.2625 +A theory file may contain any number of inductive and coinductive
1.2626 +definitions. They may be intermixed with other declarations; in
1.2627 +particular, the (co)inductive sets {\bf must} be declared separately as
1.2628 +constants, and may have mixfix syntax or be subject to syntax translations.
1.2629 +
1.2630 +Each (co)inductive definition adds definitions to the theory and also
1.2631 +proves some theorems. Each definition creates an \ML\ structure, which is a
1.2632 +substructure of the main theory structure.
1.2633 +
1.2634 +This package is related to the \ZF\ one, described in a separate
1.2635 +paper,%
1.2636 +\footnote{It appeared in CADE~\cite{paulson-CADE}; a longer version is
1.2637 + distributed with Isabelle.} %
1.2638 +which you should refer to in case of difficulties. The package is simpler
1.2639 +than \ZF's thanks to \HOL's extra-logical automatic type-checking. The types
1.2640 +of the (co)inductive sets determine the domain of the fixedpoint definition,
1.2641 +and the package does not have to use inference rules for type-checking.
1.2642 +
1.2643 +
1.2644 +\subsection{The result structure}
1.2645 +Many of the result structure's components have been discussed in the paper;
1.2646 +others are self-explanatory.
1.2647 +\begin{description}
1.2648 +\item[\tt defs] is the list of definitions of the recursive sets.
1.2649 +
1.2650 +\item[\tt mono] is a monotonicity theorem for the fixedpoint operator.
1.2651 +
1.2652 +\item[\tt unfold] is a fixedpoint equation for the recursive set (the union of
1.2653 +the recursive sets, in the case of mutual recursion).
1.2654 +
1.2655 +\item[\tt intrs] is the list of introduction rules, now proved as theorems, for
1.2656 +the recursive sets. The rules are also available individually, using the
1.2657 +names given them in the theory file.
1.2658 +
1.2659 +\item[\tt elims] is the list of elimination rule.
1.2660 +
1.2661 +\item[\tt elim] is the head of the list \texttt{elims}.
1.2662 +
1.2663 +\item[\tt mk_cases] is a function to create simplified instances of {\tt
1.2664 +elim} using freeness reasoning on underlying datatypes.
1.2665 +\end{description}
1.2666 +
1.2667 +For an inductive definition, the result structure contains the
1.2668 +rule \texttt{induct}. For a
1.2669 +coinductive definition, it contains the rule \verb|coinduct|.
1.2670 +
1.2671 +Figure~\ref{def-result-fig} summarises the two result signatures,
1.2672 +specifying the types of all these components.
1.2673 +
1.2674 +\begin{figure}
1.2675 +\begin{ttbox}
1.2676 +sig
1.2677 +val defs : thm list
1.2678 +val mono : thm
1.2679 +val unfold : thm
1.2680 +val intrs : thm list
1.2681 +val elims : thm list
1.2682 +val elim : thm
1.2683 +val mk_cases : string -> thm
1.2684 +{\it(Inductive definitions only)}
1.2685 +val induct : thm
1.2686 +{\it(coinductive definitions only)}
1.2687 +val coinduct : thm
1.2688 +end
1.2689 +\end{ttbox}
1.2690 +\hrule
1.2691 +\caption{The {\ML} result of a (co)inductive definition} \label{def-result-fig}
1.2692 +\end{figure}
1.2693 +
1.2694 +\subsection{The syntax of a (co)inductive definition}
1.2695 +An inductive definition has the form
1.2696 +\begin{ttbox}
1.2697 +inductive {\it inductive sets}
1.2698 + intrs {\it introduction rules}
1.2699 + monos {\it monotonicity theorems}
1.2700 + con_defs {\it constructor definitions}
1.2701 +\end{ttbox}
1.2702 +A coinductive definition is identical, except that it starts with the keyword
1.2703 +\texttt{coinductive}.
1.2704 +
1.2705 +The \texttt{monos} and \texttt{con_defs} sections are optional. If present,
1.2706 +each is specified by a list of identifiers.
1.2707 +
1.2708 +\begin{itemize}
1.2709 +\item The \textit{inductive sets} are specified by one or more strings.
1.2710 +
1.2711 +\item The \textit{introduction rules} specify one or more introduction rules in
1.2712 + the form \textit{ident\/}~\textit{string}, where the identifier gives the name of
1.2713 + the rule in the result structure.
1.2714 +
1.2715 +\item The \textit{monotonicity theorems} are required for each operator
1.2716 + applied to a recursive set in the introduction rules. There {\bf must}
1.2717 + be a theorem of the form $A\subseteq B\Imp M(A)\subseteq M(B)$, for each
1.2718 + premise $t\in M(R@i)$ in an introduction rule!
1.2719 +
1.2720 +\item The \textit{constructor definitions} contain definitions of constants
1.2721 + appearing in the introduction rules. In most cases it can be omitted.
1.2722 +\end{itemize}
1.2723 +
1.2724 +
1.2725 +\subsection{Example of an inductive definition}
1.2726 +Two declarations, included in a theory file, define the finite powerset
1.2727 +operator. First we declare the constant~\texttt{Fin}. Then we declare it
1.2728 +inductively, with two introduction rules:
1.2729 +\begin{ttbox}
1.2730 +consts Fin :: 'a set => 'a set set
1.2731 +inductive "Fin A"
1.2732 + intrs
1.2733 + emptyI "{\ttlbrace}{\ttrbrace} : Fin A"
1.2734 + insertI "[| a: A; b: Fin A |] ==> insert a b : Fin A"
1.2735 +\end{ttbox}
1.2736 +The resulting theory structure contains a substructure, called~\texttt{Fin}.
1.2737 +It contains the \texttt{Fin}$~A$ introduction rules as the list \texttt{Fin.intrs},
1.2738 +and also individually as \texttt{Fin.emptyI} and \texttt{Fin.consI}. The induction
1.2739 +rule is \texttt{Fin.induct}.
1.2740 +
1.2741 +For another example, here is a theory file defining the accessible
1.2742 +part of a relation. The main thing to note is the use of~\texttt{Pow} in
1.2743 +the sole introduction rule, and the corresponding mention of the rule
1.2744 +\verb|Pow_mono| in the \texttt{monos} list. The paper
1.2745 +\cite{paulson-CADE} discusses a \ZF\ version of this example in more
1.2746 +detail.
1.2747 +\begin{ttbox}
1.2748 +Acc = WF +
1.2749 +consts pred :: "['b, ('a * 'b)set] => 'a set" (*Set of predecessors*)
1.2750 + acc :: "('a * 'a)set => 'a set" (*Accessible part*)
1.2751 +defs pred_def "pred x r == {y. (y,x):r}"
1.2752 +inductive "acc r"
1.2753 + intrs
1.2754 + pred "pred a r: Pow(acc r) ==> a: acc r"
1.2755 + monos Pow_mono
1.2756 +end
1.2757 +\end{ttbox}
1.2758 +The Isabelle distribution contains many other inductive definitions. Simple
1.2759 +examples are collected on subdirectory \texttt{HOL/Induct}. The theory
1.2760 +\texttt{HOL/Induct/LList} contains coinductive definitions. Larger examples
1.2761 +may be found on other subdirectories of \texttt{HOL}, such as \texttt{IMP},
1.2762 +\texttt{Lambda} and \texttt{Auth}.
1.2763 +
1.2764 +\index{*coinductive|)} \index{*inductive|)}
1.2765 +
1.2766 +
1.2767 +\section{The examples directories}
1.2768 +
1.2769 +Directory \texttt{HOL/Auth} contains theories for proving the correctness of
1.2770 +cryptographic protocols. The approach is based upon operational
1.2771 +semantics~\cite{paulson-security} rather than the more usual belief logics.
1.2772 +On the same directory are proofs for some standard examples, such as the
1.2773 +Needham-Schroeder public-key authentication protocol~\cite{paulson-ns}
1.2774 +and the Otway-Rees protocol.
1.2775 +
1.2776 +Directory \texttt{HOL/IMP} contains a formalization of various denotational,
1.2777 +operational and axiomatic semantics of a simple while-language, the necessary
1.2778 +equivalence proofs, soundness and completeness of the Hoare rules with respect
1.2779 +to the
1.2780 +denotational semantics, and soundness and completeness of a verification
1.2781 +condition generator. Much of development is taken from
1.2782 +Winskel~\cite{winskel93}. For details see~\cite{nipkow-IMP}.
1.2783 +
1.2784 +Directory \texttt{HOL/Hoare} contains a user friendly surface syntax for Hoare
1.2785 +logic, including a tactic for generating verification-conditions.
1.2786 +
1.2787 +Directory \texttt{HOL/MiniML} contains a formalization of the type system of the
1.2788 +core functional language Mini-ML and a correctness proof for its type
1.2789 +inference algorithm $\cal W$~\cite{milner78,nazareth-nipkow}.
1.2790 +
1.2791 +Directory \texttt{HOL/Lambda} contains a formalization of untyped
1.2792 +$\lambda$-calculus in de~Bruijn notation and Church-Rosser proofs for $\beta$
1.2793 +and $\eta$ reduction~\cite{Nipkow-CR}.
1.2794 +
1.2795 +Directory \texttt{HOL/Subst} contains Martin Coen's mechanization of a theory of
1.2796 +substitutions and unifiers. It is based on Paulson's previous
1.2797 +mechanisation in {\LCF}~\cite{paulson85} of Manna and Waldinger's
1.2798 +theory~\cite{mw81}. It demonstrates a complicated use of \texttt{recdef},
1.2799 +with nested recursion.
1.2800 +
1.2801 +Directory \texttt{HOL/Induct} presents simple examples of (co)inductive
1.2802 +definitions and datatypes.
1.2803 +\begin{itemize}
1.2804 +\item Theory \texttt{PropLog} proves the soundness and completeness of
1.2805 + classical propositional logic, given a truth table semantics. The only
1.2806 + connective is $\imp$. A Hilbert-style axiom system is specified, and its
1.2807 + set of theorems defined inductively. A similar proof in \ZF{} is
1.2808 + described elsewhere~\cite{paulson-set-II}.
1.2809 +
1.2810 +\item Theory \texttt{Term} defines the datatype \texttt{term}.
1.2811 +
1.2812 +\item Theory \texttt{ABexp} defines arithmetic and boolean expressions
1.2813 + as mutually recursive datatypes.
1.2814 +
1.2815 +\item The definition of lazy lists demonstrates methods for handling
1.2816 + infinite data structures and coinduction in higher-order
1.2817 + logic~\cite{paulson-coind}.%
1.2818 +\footnote{To be precise, these lists are \emph{potentially infinite} rather
1.2819 + than lazy. Lazy implies a particular operational semantics.}
1.2820 + Theory \thydx{LList} defines an operator for
1.2821 + corecursion on lazy lists, which is used to define a few simple functions
1.2822 + such as map and append. A coinduction principle is defined
1.2823 + for proving equations on lazy lists.
1.2824 +
1.2825 +\item Theory \thydx{LFilter} defines the filter functional for lazy lists.
1.2826 + This functional is notoriously difficult to define because finding the next
1.2827 + element meeting the predicate requires possibly unlimited search. It is not
1.2828 + computable, but can be expressed using a combination of induction and
1.2829 + corecursion.
1.2830 +
1.2831 +\item Theory \thydx{Exp} illustrates the use of iterated inductive definitions
1.2832 + to express a programming language semantics that appears to require mutual
1.2833 + induction. Iterated induction allows greater modularity.
1.2834 +\end{itemize}
1.2835 +
1.2836 +Directory \texttt{HOL/ex} contains other examples and experimental proofs in
1.2837 +{\HOL}.
1.2838 +\begin{itemize}
1.2839 +\item Theory \texttt{Recdef} presents many examples of using \texttt{recdef}
1.2840 + to define recursive functions. Another example is \texttt{Fib}, which
1.2841 + defines the Fibonacci function.
1.2842 +
1.2843 +\item Theory \texttt{Primes} defines the Greatest Common Divisor of two
1.2844 + natural numbers and proves a key lemma of the Fundamental Theorem of
1.2845 + Arithmetic: if $p$ is prime and $p$ divides $m\times n$ then $p$ divides~$m$
1.2846 + or $p$ divides~$n$.
1.2847 +
1.2848 +\item Theory \texttt{Primrec} develops some computation theory. It
1.2849 + inductively defines the set of primitive recursive functions and presents a
1.2850 + proof that Ackermann's function is not primitive recursive.
1.2851 +
1.2852 +\item File \texttt{cla.ML} demonstrates the classical reasoner on over sixty
1.2853 + predicate calculus theorems, ranging from simple tautologies to
1.2854 + moderately difficult problems involving equality and quantifiers.
1.2855 +
1.2856 +\item File \texttt{meson.ML} contains an experimental implementation of the {\sc
1.2857 + meson} proof procedure, inspired by Plaisted~\cite{plaisted90}. It is
1.2858 + much more powerful than Isabelle's classical reasoner. But it is less
1.2859 + useful in practice because it works only for pure logic; it does not
1.2860 + accept derived rules for the set theory primitives, for example.
1.2861 +
1.2862 +\item File \texttt{mesontest.ML} contains test data for the {\sc meson} proof
1.2863 + procedure. These are mostly taken from Pelletier \cite{pelletier86}.
1.2864 +
1.2865 +\item File \texttt{set.ML} proves Cantor's Theorem, which is presented in
1.2866 + \S\ref{sec:hol-cantor} below, and the Schr\"oder-Bernstein Theorem.
1.2867 +
1.2868 +\item Theory \texttt{MT} contains Jacob Frost's formalization~\cite{frost93} of
1.2869 + Milner and Tofte's coinduction example~\cite{milner-coind}. This
1.2870 + substantial proof concerns the soundness of a type system for a simple
1.2871 + functional language. The semantics of recursion is given by a cyclic
1.2872 + environment, which makes a coinductive argument appropriate.
1.2873 +\end{itemize}
1.2874 +
1.2875 +
1.2876 +\goodbreak
1.2877 +\section{Example: Cantor's Theorem}\label{sec:hol-cantor}
1.2878 +Cantor's Theorem states that every set has more subsets than it has
1.2879 +elements. It has become a favourite example in higher-order logic since
1.2880 +it is so easily expressed:
1.2881 +\[ \forall f::\alpha \To \alpha \To bool. \exists S::\alpha\To bool.
1.2882 + \forall x::\alpha. f~x \not= S
1.2883 +\]
1.2884 +%
1.2885 +Viewing types as sets, $\alpha\To bool$ represents the powerset
1.2886 +of~$\alpha$. This version states that for every function from $\alpha$ to
1.2887 +its powerset, some subset is outside its range.
1.2888 +
1.2889 +The Isabelle proof uses \HOL's set theory, with the type $\alpha\,set$ and
1.2890 +the operator \cdx{range}.
1.2891 +\begin{ttbox}
1.2892 +context Set.thy;
1.2893 +\end{ttbox}
1.2894 +The set~$S$ is given as an unknown instead of a
1.2895 +quantified variable so that we may inspect the subset found by the proof.
1.2896 +\begin{ttbox}
1.2897 +Goal "?S ~: range\thinspace(f :: 'a=>'a set)";
1.2898 +{\out Level 0}
1.2899 +{\out ?S ~: range f}
1.2900 +{\out 1. ?S ~: range f}
1.2901 +\end{ttbox}
1.2902 +The first two steps are routine. The rule \tdx{rangeE} replaces
1.2903 +$\Var{S}\in \texttt{range} \, f$ by $\Var{S}=f~x$ for some~$x$.
1.2904 +\begin{ttbox}
1.2905 +by (resolve_tac [notI] 1);
1.2906 +{\out Level 1}
1.2907 +{\out ?S ~: range f}
1.2908 +{\out 1. ?S : range f ==> False}
1.2909 +\ttbreak
1.2910 +by (eresolve_tac [rangeE] 1);
1.2911 +{\out Level 2}
1.2912 +{\out ?S ~: range f}
1.2913 +{\out 1. !!x. ?S = f x ==> False}
1.2914 +\end{ttbox}
1.2915 +Next, we apply \tdx{equalityCE}, reasoning that since $\Var{S}=f~x$,
1.2916 +we have $\Var{c}\in \Var{S}$ if and only if $\Var{c}\in f~x$ for
1.2917 +any~$\Var{c}$.
1.2918 +\begin{ttbox}
1.2919 +by (eresolve_tac [equalityCE] 1);
1.2920 +{\out Level 3}
1.2921 +{\out ?S ~: range f}
1.2922 +{\out 1. !!x. [| ?c3 x : ?S; ?c3 x : f x |] ==> False}
1.2923 +{\out 2. !!x. [| ?c3 x ~: ?S; ?c3 x ~: f x |] ==> False}
1.2924 +\end{ttbox}
1.2925 +Now we use a bit of creativity. Suppose that~$\Var{S}$ has the form of a
1.2926 +comprehension. Then $\Var{c}\in\{x.\Var{P}~x\}$ implies
1.2927 +$\Var{P}~\Var{c}$. Destruct-resolution using \tdx{CollectD}
1.2928 +instantiates~$\Var{S}$ and creates the new assumption.
1.2929 +\begin{ttbox}
1.2930 +by (dresolve_tac [CollectD] 1);
1.2931 +{\out Level 4}
1.2932 +{\out {\ttlbrace}x. ?P7 x{\ttrbrace} ~: range f}
1.2933 +{\out 1. !!x. [| ?c3 x : f x; ?P7(?c3 x) |] ==> False}
1.2934 +{\out 2. !!x. [| ?c3 x ~: {\ttlbrace}x. ?P7 x{\ttrbrace}; ?c3 x ~: f x |] ==> False}
1.2935 +\end{ttbox}
1.2936 +Forcing a contradiction between the two assumptions of subgoal~1
1.2937 +completes the instantiation of~$S$. It is now the set $\{x. x\not\in
1.2938 +f~x\}$, which is the standard diagonal construction.
1.2939 +\begin{ttbox}
1.2940 +by (contr_tac 1);
1.2941 +{\out Level 5}
1.2942 +{\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f}
1.2943 +{\out 1. !!x. [| x ~: {\ttlbrace}x. x ~: f x{\ttrbrace}; x ~: f x |] ==> False}
1.2944 +\end{ttbox}
1.2945 +The rest should be easy. To apply \tdx{CollectI} to the negated
1.2946 +assumption, we employ \ttindex{swap_res_tac}:
1.2947 +\begin{ttbox}
1.2948 +by (swap_res_tac [CollectI] 1);
1.2949 +{\out Level 6}
1.2950 +{\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f}
1.2951 +{\out 1. !!x. [| x ~: f x; ~ False |] ==> x ~: f x}
1.2952 +\ttbreak
1.2953 +by (assume_tac 1);
1.2954 +{\out Level 7}
1.2955 +{\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f}
1.2956 +{\out No subgoals!}
1.2957 +\end{ttbox}
1.2958 +How much creativity is required? As it happens, Isabelle can prove this
1.2959 +theorem automatically. The default classical set \texttt{claset()} contains rules
1.2960 +for most of the constructs of \HOL's set theory. We must augment it with
1.2961 +\tdx{equalityCE} to break up set equalities, and then apply best-first
1.2962 +search. Depth-first search would diverge, but best-first search
1.2963 +successfully navigates through the large search space.
1.2964 +\index{search!best-first}
1.2965 +\begin{ttbox}
1.2966 +choplev 0;
1.2967 +{\out Level 0}
1.2968 +{\out ?S ~: range f}
1.2969 +{\out 1. ?S ~: range f}
1.2970 +\ttbreak
1.2971 +by (best_tac (claset() addSEs [equalityCE]) 1);
1.2972 +{\out Level 1}
1.2973 +{\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f}
1.2974 +{\out No subgoals!}
1.2975 +\end{ttbox}
1.2976 +If you run this example interactively, make sure your current theory contains
1.2977 +theory \texttt{Set}, for example by executing \ttindex{context}~{\tt Set.thy}.
1.2978 +Otherwise the default claset may not contain the rules for set theory.
1.2979 +\index{higher-order logic|)}
1.2980 +
1.2981 +%%% Local Variables:
1.2982 +%%% mode: latex
1.2983 +%%% TeX-master: "logics"
1.2984 +%%% End: