summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/HOL/HOL.tex

author | immler@in.tum.de |

Thu, 26 Feb 2009 10:13:43 +0100 | |

changeset 30151 | 629f3a92863e |

parent 27452 | 5c1fb7d262bf |

child 30686 | 47a32dd1b86e |

permissions | -rw-r--r-- |

removed global ref dfg_format

%% $Id$ \chapter{Higher-Order Logic} \index{higher-order logic|(} \index{HOL system@{\sc hol} system} The theory~\thydx{HOL} implements higher-order logic. It is based on Gordon's~{\sc hol} system~\cite{mgordon-hol}, which itself is based on Church's original paper~\cite{church40}. Andrews's book~\cite{andrews86} is a full description of the original Church-style higher-order logic. Experience with the {\sc hol} system has demonstrated that higher-order logic is widely applicable in many areas of mathematics and computer science, not just hardware verification, {\sc hol}'s original \textit{raison d'{\^e}tre\/}. It is weaker than ZF set theory but for most applications this does not matter. If you prefer {\ML} to Lisp, you will probably prefer HOL to~ZF. The syntax of HOL\footnote{Earlier versions of Isabelle's HOL used a different syntax. Ancient releases of Isabelle included still another version of~HOL, with explicit type inference rules~\cite{paulson-COLOG}. This version no longer exists, but \thydx{ZF} supports a similar style of reasoning.} follows $\lambda$-calculus and functional programming. Function application is curried. To apply the function~$f$ of type $\tau@1\To\tau@2\To\tau@3$ to the arguments~$a$ and~$b$ in HOL, you simply write $f\,a\,b$. There is no `apply' operator as in \thydx{ZF}. Note that $f(a,b)$ means ``$f$ applied to the pair $(a,b)$'' in HOL. We write ordered pairs as $(a,b)$, not $\langle a,b\rangle$ as in ZF. HOL has a distinct feel, compared with ZF and CTT. It identifies object-level types with meta-level types, taking advantage of Isabelle's built-in type-checker. It identifies object-level functions with meta-level functions, so it uses Isabelle's operations for abstraction and application. These identifications allow Isabelle to support HOL particularly nicely, but they also mean that HOL requires more sophistication from the user --- in particular, an understanding of Isabelle's type system. Beginners should work with \texttt{show_types} (or even \texttt{show_sorts}) set to \texttt{true}. \begin{figure} \begin{constants} \it name &\it meta-type & \it description \\ \cdx{Trueprop}& $bool\To prop$ & coercion to $prop$\\ \cdx{Not} & $bool\To bool$ & negation ($\lnot$) \\ \cdx{True} & $bool$ & tautology ($\top$) \\ \cdx{False} & $bool$ & absurdity ($\bot$) \\ \cdx{If} & $[bool,\alpha,\alpha]\To\alpha$ & conditional \\ \cdx{Let} & $[\alpha,\alpha\To\beta]\To\beta$ & let binder \end{constants} \subcaption{Constants} \begin{constants} \index{"@@{\tt\at} symbol} \index{*"! symbol}\index{*"? symbol} \index{*"?"! symbol}\index{*"E"X"! symbol} \it symbol &\it name &\it meta-type & \it description \\ \sdx{SOME} or \tt\at & \cdx{Eps} & $(\alpha\To bool)\To\alpha$ & Hilbert description ($\varepsilon$) \\ \sdx{ALL} or {\tt!~} & \cdx{All} & $(\alpha\To bool)\To bool$ & universal quantifier ($\forall$) \\ \sdx{EX} or {\tt?~} & \cdx{Ex} & $(\alpha\To bool)\To bool$ & existential quantifier ($\exists$) \\ \texttt{EX!} or {\tt?!} & \cdx{Ex1} & $(\alpha\To bool)\To bool$ & unique existence ($\exists!$)\\ \texttt{LEAST} & \cdx{Least} & $(\alpha::ord \To bool)\To\alpha$ & least element \end{constants} \subcaption{Binders} \begin{constants} \index{*"= symbol} \index{&@{\tt\&} symbol} \index{*"| symbol} \index{*"-"-"> symbol} \it symbol & \it meta-type & \it priority & \it description \\ \sdx{o} & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ & Left 55 & composition ($\circ$) \\ \tt = & $[\alpha,\alpha]\To bool$ & Left 50 & equality ($=$) \\ \tt < & $[\alpha::ord,\alpha]\To bool$ & Left 50 & less than ($<$) \\ \tt <= & $[\alpha::ord,\alpha]\To bool$ & Left 50 & less than or equals ($\leq$)\\ \tt \& & $[bool,bool]\To bool$ & Right 35 & conjunction ($\conj$) \\ \tt | & $[bool,bool]\To bool$ & Right 30 & disjunction ($\disj$) \\ \tt --> & $[bool,bool]\To bool$ & Right 25 & implication ($\imp$) \end{constants} \subcaption{Infixes} \caption{Syntax of \texttt{HOL}} \label{hol-constants} \end{figure} \begin{figure} \index{*let symbol} \index{*in symbol} \dquotes \[\begin{array}{rclcl} term & = & \hbox{expression of class~$term$} \\ & | & "SOME~" id " . " formula & | & "\at~" id " . " formula \\ & | & \multicolumn{3}{l}{"let"~id~"="~term";"\dots";"~id~"="~term~"in"~term} \\ & | & \multicolumn{3}{l}{"if"~formula~"then"~term~"else"~term} \\ & | & "LEAST"~ id " . " formula \\[2ex] formula & = & \hbox{expression of type~$bool$} \\ & | & term " = " term \\ & | & term " \ttilde= " term \\ & | & term " < " term \\ & | & term " <= " term \\ & | & "\ttilde\ " formula \\ & | & formula " \& " formula \\ & | & formula " | " formula \\ & | & formula " --> " formula \\ & | & "ALL~" id~id^* " . " formula & | & "!~~~" id~id^* " . " formula \\ & | & "EX~~" id~id^* " . " formula & | & "?~~~" id~id^* " . " formula \\ & | & "EX!~" id~id^* " . " formula & | & "?!~~" id~id^* " . " formula \\ \end{array} \] \caption{Full grammar for HOL} \label{hol-grammar} \end{figure} \section{Syntax} Figure~\ref{hol-constants} lists the constants (including infixes and binders), while Fig.\ts\ref{hol-grammar} presents the grammar of higher-order logic. Note that $a$\verb|~=|$b$ is translated to $\lnot(a=b)$. \begin{warn} HOL has no if-and-only-if connective; logical equivalence is expressed using equality. But equality has a high priority, as befitting a relation, while if-and-only-if typically has the lowest priority. Thus, $\lnot\lnot P=P$ abbreviates $\lnot\lnot (P=P)$ and not $(\lnot\lnot P)=P$. When using $=$ to mean logical equivalence, enclose both operands in parentheses. \end{warn} \subsection{Types and overloading} The universal type class of higher-order terms is called~\cldx{term}. By default, explicit type variables have class \cldx{term}. In particular the equality symbol and quantifiers are polymorphic over class \texttt{term}. The type of formulae, \tydx{bool}, belongs to class \cldx{term}; thus, formulae are terms. The built-in type~\tydx{fun}, which constructs function types, is overloaded with arity {\tt(term,\thinspace term)\thinspace term}. Thus, $\sigma\To\tau$ belongs to class~{\tt term} if $\sigma$ and~$\tau$ do, allowing quantification over functions. HOL allows new types to be declared as subsets of existing types; see~{\S}\ref{sec:HOL:Types}. ML-like datatypes can also be declared; see ~{\S}\ref{sec:HOL:datatype}. Several syntactic type classes --- \cldx{plus}, \cldx{minus}, \cldx{times} and \cldx{power} --- permit overloading of the operators {\tt+},\index{*"+ symbol} {\tt-}\index{*"- symbol}, {\tt*}.\index{*"* symbol} and \verb|^|.\index{^@\verb.^. symbol} % They are overloaded to denote the obvious arithmetic operations on types \tdx{nat}, \tdx{int} and~\tdx{real}. (With the \verb|^| operator, the exponent always has type~\tdx{nat}.) Non-arithmetic overloadings are also done: the operator {\tt-} can denote set difference, while \verb|^| can denote exponentiation of relations (iterated composition). Unary minus is also written as~{\tt-} and is overloaded like its 2-place counterpart; it even can stand for set complement. The constant \cdx{0} is also overloaded. It serves as the zero element of several types, of which the most important is \tdx{nat} (the natural numbers). The type class \cldx{plus_ac0} comprises all types for which 0 and~+ satisfy the laws $x+y=y+x$, $(x+y)+z = x+(y+z)$ and $0+x = x$. These types include the numeric ones \tdx{nat}, \tdx{int} and~\tdx{real} and also multisets. The summation operator \cdx{setsum} is available for all types in this class. Theory \thydx{Ord} defines the syntactic class \cldx{ord} of order signatures. The relations $<$ and $\leq$ are polymorphic over this class, as are the functions \cdx{mono}, \cdx{min} and \cdx{max}, and the \cdx{LEAST} operator. \thydx{Ord} also defines a subclass \cldx{order} of \cldx{ord} which axiomatizes the types that are partially ordered with respect to~$\leq$. A further subclass \cldx{linorder} of \cldx{order} axiomatizes linear orderings. For details, see the file \texttt{Ord.thy}. If you state a goal containing overloaded functions, you may need to include type constraints. Type inference may otherwise make the goal more polymorphic than you intended, with confusing results. For example, the variables $i$, $j$ and $k$ in the goal $i \leq j \Imp i \leq j+k$ have type $\alpha::\{ord,plus\}$, although you may have expected them to have some numeric type, e.g. $nat$. Instead you should have stated the goal as $(i::nat) \leq j \Imp i \leq j+k$, which causes all three variables to have type $nat$. \begin{warn} If resolution fails for no obvious reason, try setting \ttindex{show_types} to \texttt{true}, causing Isabelle to display types of terms. Possibly set \ttindex{show_sorts} to \texttt{true} as well, causing Isabelle to display type classes and sorts. \index{unification!incompleteness of} Where function types are involved, Isabelle's unification code does not guarantee to find instantiations for type variables automatically. Be prepared to use \ttindex{res_inst_tac} instead of \texttt{resolve_tac}, possibly instantiating type variables. Setting \ttindex{Unify.trace_types} to \texttt{true} causes Isabelle to report omitted search paths during unification.\index{tracing!of unification} \end{warn} \subsection{Binders} Hilbert's {\bf description} operator~$\varepsilon x. P[x]$ stands for some~$x$ satisfying~$P$, if such exists. Since all terms in HOL denote something, a description is always meaningful, but we do not know its value unless $P$ defines it uniquely. We may write descriptions as \cdx{Eps}($\lambda x. P[x]$) or use the syntax \hbox{\tt SOME~$x$.~$P[x]$}. Existential quantification is defined by \[ \exists x. P~x \;\equiv\; P(\varepsilon x. P~x). \] The unique existence quantifier, $\exists!x. P$, is defined in terms of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested quantifications. For instance, $\exists!x\,y. P\,x\,y$ abbreviates $\exists!x. \exists!y. P\,x\,y$; note that this does not mean that there exists a unique pair $(x,y)$ satisfying~$P\,x\,y$. \medskip \index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system} The basic Isabelle/HOL binders have two notations. Apart from the usual \texttt{ALL} and \texttt{EX} for $\forall$ and $\exists$, Isabelle/HOL also supports the original notation of Gordon's {\sc hol} system: \texttt{!}\ and~\texttt{?}. In the latter case, the existential quantifier \emph{must} be followed by a space; thus {\tt?x} is an unknown, while \verb'? x. f x=y' is a quantification. Both notations are accepted for input. The print mode ``\ttindexbold{HOL}'' governs the output notation. If enabled (e.g.\ by passing option \texttt{-m HOL} to the \texttt{isabelle} executable), then~{\tt!}\ and~{\tt?}\ are displayed. \medskip If $\tau$ is a type of class \cldx{ord}, $P$ a formula and $x$ a variable of type $\tau$, then the term \cdx{LEAST}~$x. P[x]$ is defined to be the least (w.r.t.\ $\leq$) $x$ such that $P~x$ holds (see Fig.~\ref{hol-defs}). The definition uses Hilbert's $\varepsilon$ choice operator, so \texttt{Least} is always meaningful, but may yield nothing useful in case there is not a unique least element satisfying $P$.\footnote{Class $ord$ does not require much of its instances, so $\leq$ need not be a well-ordering, not even an order at all!} \medskip All these binders have priority 10. \begin{warn} The low priority of binders means that they need to be enclosed in parenthesis when they occur in the context of other operations. For example, instead of $P \land \forall x. Q$ you need to write $P \land (\forall x. Q)$. \end{warn} \subsection{The let and case constructions} Local abbreviations can be introduced by a \texttt{let} construct whose syntax appears in Fig.\ts\ref{hol-grammar}. Internally it is translated into the constant~\cdx{Let}. It can be expanded by rewriting with its definition, \tdx{Let_def}. HOL also defines the basic syntax \[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n\] as a uniform means of expressing \texttt{case} constructs. Therefore \texttt{case} and \sdx{of} are reserved words. Initially, this is mere syntax and has no logical meaning. By declaring translations, you can cause instances of the \texttt{case} construct to denote applications of particular case operators. This is what happens automatically for each \texttt{datatype} definition (see~{\S}\ref{sec:HOL:datatype}). \begin{warn} Both \texttt{if} and \texttt{case} constructs have as low a priority as quantifiers, which requires additional enclosing parentheses in the context of most other operations. For example, instead of $f~x = {\tt if\dots then\dots else}\dots$ you need to write $f~x = ({\tt if\dots then\dots else\dots})$. \end{warn} \section{Rules of inference} \begin{figure} \begin{ttbox}\makeatother \tdx{refl} t = (t::'a) \tdx{subst} [| s = t; P s |] ==> P (t::'a) \tdx{ext} (!!x::'a. (f x :: 'b) = g x) ==> (\%x. f x) = (\%x. g x) \tdx{impI} (P ==> Q) ==> P-->Q \tdx{mp} [| P-->Q; P |] ==> Q \tdx{iff} (P-->Q) --> (Q-->P) --> (P=Q) \tdx{someI} P(x::'a) ==> P(@x. P x) \tdx{True_or_False} (P=True) | (P=False) \end{ttbox} \caption{The \texttt{HOL} rules} \label{hol-rules} \end{figure} Figure~\ref{hol-rules} shows the primitive inference rules of~HOL, with their~{\ML} names. Some of the rules deserve additional comments: \begin{ttdescription} \item[\tdx{ext}] expresses extensionality of functions. \item[\tdx{iff}] asserts that logically equivalent formulae are equal. \item[\tdx{someI}] gives the defining property of the Hilbert $\varepsilon$-operator. It is a form of the Axiom of Choice. The derived rule \tdx{some_equality} (see below) is often easier to use. \item[\tdx{True_or_False}] makes the logic classical.\footnote{In fact, the $\varepsilon$-operator already makes the logic classical, as shown by Diaconescu; see Paulson~\cite{paulson-COLOG} for details.} \end{ttdescription} \begin{figure}\hfuzz=4pt%suppress "Overfull \hbox" message \begin{ttbox}\makeatother \tdx{True_def} True == ((\%x::bool. x)=(\%x. x)) \tdx{All_def} All == (\%P. P = (\%x. True)) \tdx{Ex_def} Ex == (\%P. P(@x. P x)) \tdx{False_def} False == (!P. P) \tdx{not_def} not == (\%P. P-->False) \tdx{and_def} op & == (\%P Q. !R. (P-->Q-->R) --> R) \tdx{or_def} op | == (\%P Q. !R. (P-->R) --> (Q-->R) --> R) \tdx{Ex1_def} Ex1 == (\%P. ? x. P x & (! y. P y --> y=x)) \tdx{o_def} op o == (\%(f::'b=>'c) g x::'a. f(g x)) \tdx{if_def} If P x y == (\%P x y. @z::'a.(P=True --> z=x) & (P=False --> z=y)) \tdx{Let_def} Let s f == f s \tdx{Least_def} Least P == @x. P(x) & (ALL y. P(y) --> x <= y)" \end{ttbox} \caption{The \texttt{HOL} definitions} \label{hol-defs} \end{figure} HOL follows standard practice in higher-order logic: only a few connectives are taken as primitive, with the remainder defined obscurely (Fig.\ts\ref{hol-defs}). Gordon's {\sc hol} system expresses the corresponding definitions \cite[page~270]{mgordon-hol} using object-equality~({\tt=}), which is possible because equality in higher-order logic may equate formulae and even functions over formulae. But theory~HOL, like all other Isabelle theories, uses meta-equality~({\tt==}) for definitions. \begin{warn} The definitions above should never be expanded and are shown for completeness only. Instead users should reason in terms of the derived rules shown below or, better still, using high-level tactics (see~{\S}\ref{sec:HOL:generic-packages}). \end{warn} Some of the rules mention type variables; for example, \texttt{refl} mentions the type variable~{\tt'a}. This allows you to instantiate type variables explicitly by calling \texttt{res_inst_tac}. \begin{figure} \begin{ttbox} \tdx{sym} s=t ==> t=s \tdx{trans} [| r=s; s=t |] ==> r=t \tdx{ssubst} [| t=s; P s |] ==> P t \tdx{box_equals} [| a=b; a=c; b=d |] ==> c=d \tdx{arg_cong} x = y ==> f x = f y \tdx{fun_cong} f = g ==> f x = g x \tdx{cong} [| f = g; x = y |] ==> f x = g y \tdx{not_sym} t ~= s ==> s ~= t \subcaption{Equality} \tdx{TrueI} True \tdx{FalseE} False ==> P \tdx{conjI} [| P; Q |] ==> P&Q \tdx{conjunct1} [| P&Q |] ==> P \tdx{conjunct2} [| P&Q |] ==> Q \tdx{conjE} [| P&Q; [| P; Q |] ==> R |] ==> R \tdx{disjI1} P ==> P|Q \tdx{disjI2} Q ==> P|Q \tdx{disjE} [| P | Q; P ==> R; Q ==> R |] ==> R \tdx{notI} (P ==> False) ==> ~ P \tdx{notE} [| ~ P; P |] ==> R \tdx{impE} [| P-->Q; P; Q ==> R |] ==> R \subcaption{Propositional logic} \tdx{iffI} [| P ==> Q; Q ==> P |] ==> P=Q \tdx{iffD1} [| P=Q; P |] ==> Q \tdx{iffD2} [| P=Q; Q |] ==> P \tdx{iffE} [| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R \subcaption{Logical equivalence} \end{ttbox} \caption{Derived rules for HOL} \label{hol-lemmas1} \end{figure} % %\tdx{eqTrueI} P ==> P=True %\tdx{eqTrueE} P=True ==> P \begin{figure} \begin{ttbox}\makeatother \tdx{allI} (!!x. P x) ==> !x. P x \tdx{spec} !x. P x ==> P x \tdx{allE} [| !x. P x; P x ==> R |] ==> R \tdx{all_dupE} [| !x. P x; [| P x; !x. P x |] ==> R |] ==> R \tdx{exI} P x ==> ? x. P x \tdx{exE} [| ? x. P x; !!x. P x ==> Q |] ==> Q \tdx{ex1I} [| P a; !!x. P x ==> x=a |] ==> ?! x. P x \tdx{ex1E} [| ?! x. P x; !!x. [| P x; ! y. P y --> y=x |] ==> R |] ==> R \tdx{some_equality} [| P a; !!x. P x ==> x=a |] ==> (@x. P x) = a \subcaption{Quantifiers and descriptions} \tdx{ccontr} (~P ==> False) ==> P \tdx{classical} (~P ==> P) ==> P \tdx{excluded_middle} ~P | P \tdx{disjCI} (~Q ==> P) ==> P|Q \tdx{exCI} (! x. ~ P x ==> P a) ==> ? x. P x \tdx{impCE} [| P-->Q; ~ P ==> R; Q ==> R |] ==> R \tdx{iffCE} [| P=Q; [| P;Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R \tdx{notnotD} ~~P ==> P \tdx{swap} ~P ==> (~Q ==> P) ==> Q \subcaption{Classical logic} \tdx{if_P} P ==> (if P then x else y) = x \tdx{if_not_P} ~ P ==> (if P then x else y) = y \tdx{split_if} P(if Q then x else y) = ((Q --> P x) & (~Q --> P y)) \subcaption{Conditionals} \end{ttbox} \caption{More derived rules} \label{hol-lemmas2} \end{figure} Some derived rules are shown in Figures~\ref{hol-lemmas1} and~\ref{hol-lemmas2}, with their {\ML} names. These include natural rules for the logical connectives, as well as sequent-style elimination rules for conjunctions, implications, and universal quantifiers. Note the equality rules: \tdx{ssubst} performs substitution in backward proofs, while \tdx{box_equals} supports reasoning by simplifying both sides of an equation. The following simple tactics are occasionally useful: \begin{ttdescription} \item[\ttindexbold{strip_tac} $i$] applies \texttt{allI} and \texttt{impI} repeatedly to remove all outermost universal quantifiers and implications from subgoal $i$. \item[\ttindexbold{case_tac} {\tt"}$P${\tt"} $i$] performs case distinction on $P$ for subgoal $i$: the latter is replaced by two identical subgoals with the added assumptions $P$ and $\lnot P$, respectively. \item[\ttindexbold{smp_tac} $j$ $i$] applies $j$ times \texttt{spec} and then \texttt{mp} in subgoal $i$, which is typically useful when forward-chaining from an induction hypothesis. As a generalization of \texttt{mp_tac}, if there are assumptions $\forall \vec{x}. P \vec{x} \imp Q \vec{x}$ and $P \vec{a}$, ($\vec{x}$ being a vector of $j$ variables) then it replaces the universally quantified implication by $Q \vec{a}$. It may instantiate unknowns. It fails if it can do nothing. \end{ttdescription} \begin{figure} \begin{center} \begin{tabular}{rrr} \it name &\it meta-type & \it description \\ \index{{}@\verb'{}' symbol} \verb|{}| & $\alpha\,set$ & the empty set \\ \cdx{insert} & $[\alpha,\alpha\,set]\To \alpha\,set$ & insertion of element \\ \cdx{Collect} & $(\alpha\To bool)\To\alpha\,set$ & comprehension \\ \cdx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$ & intersection over a set\\ \cdx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$ & union over a set\\ \cdx{Inter} & $(\alpha\,set)set\To\alpha\,set$ &set of sets intersection \\ \cdx{Union} & $(\alpha\,set)set\To\alpha\,set$ &set of sets union \\ \cdx{Pow} & $\alpha\,set \To (\alpha\,set)set$ & powerset \\[1ex] \cdx{range} & $(\alpha\To\beta )\To\beta\,set$ & range of a function \\[1ex] \cdx{Ball}~~\cdx{Bex} & $[\alpha\,set,\alpha\To bool]\To bool$ & bounded quantifiers \end{tabular} \end{center} \subcaption{Constants} \begin{center} \begin{tabular}{llrrr} \it symbol &\it name &\it meta-type & \it priority & \it description \\ \sdx{INT} & \cdx{INTER1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 & intersection\\ \sdx{UN} & \cdx{UNION1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 & union \end{tabular} \end{center} \subcaption{Binders} \begin{center} \index{*"`"` symbol} \index{*": symbol} \index{*"<"= symbol} \begin{tabular}{rrrr} \it symbol & \it meta-type & \it priority & \it description \\ \tt `` & $[\alpha\To\beta ,\alpha\,set]\To \beta\,set$ & Left 90 & image \\ \sdx{Int} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$ & Left 70 & intersection ($\int$) \\ \sdx{Un} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$ & Left 65 & union ($\un$) \\ \tt: & $[\alpha ,\alpha\,set]\To bool$ & Left 50 & membership ($\in$) \\ \tt <= & $[\alpha\,set,\alpha\,set]\To bool$ & Left 50 & subset ($\subseteq$) \end{tabular} \end{center} \subcaption{Infixes} \caption{Syntax of the theory \texttt{Set}} \label{hol-set-syntax} \end{figure} \begin{figure} \begin{center} \tt\frenchspacing \index{*"! symbol} \begin{tabular}{rrr} \it external & \it internal & \it description \\ $a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm not in\\ {\ttlbrace}$a@1$, $\ldots${\ttrbrace} & insert $a@1$ $\ldots$ {\ttlbrace}{\ttrbrace} & \rm finite set \\ {\ttlbrace}$x$. $P[x]${\ttrbrace} & Collect($\lambda x. P[x]$) & \rm comprehension \\ \sdx{INT} $x$:$A$. $B[x]$ & INTER $A$ $\lambda x. B[x]$ & \rm intersection \\ \sdx{UN}{\tt\ } $x$:$A$. $B[x]$ & UNION $A$ $\lambda x. B[x]$ & \rm union \\ \sdx{ALL} $x$:$A$.\ $P[x]$ or \texttt{!} $x$:$A$.\ $P[x]$ & Ball $A$ $\lambda x.\ P[x]$ & \rm bounded $\forall$ \\ \sdx{EX}{\tt\ } $x$:$A$.\ $P[x]$ or \texttt{?} $x$:$A$.\ $P[x]$ & Bex $A$ $\lambda x.\ P[x]$ & \rm bounded $\exists$ \end{tabular} \end{center} \subcaption{Translations} \dquotes \[\begin{array}{rclcl} term & = & \hbox{other terms\ldots} \\ & | & "{\ttlbrace}{\ttrbrace}" \\ & | & "{\ttlbrace} " term\; ("," term)^* " {\ttrbrace}" \\ & | & "{\ttlbrace} " id " . " formula " {\ttrbrace}" \\ & | & term " `` " term \\ & | & term " Int " term \\ & | & term " Un " term \\ & | & "INT~~" id ":" term " . " term \\ & | & "UN~~~" id ":" term " . " term \\ & | & "INT~~" id~id^* " . " term \\ & | & "UN~~~" id~id^* " . " term \\[2ex] formula & = & \hbox{other formulae\ldots} \\ & | & term " : " term \\ & | & term " \ttilde: " term \\ & | & term " <= " term \\ & | & "ALL " id ":" term " . " formula & | & "!~" id ":" term " . " formula \\ & | & "EX~~" id ":" term " . " formula & | & "?~" id ":" term " . " formula \\ \end{array} \] \subcaption{Full Grammar} \caption{Syntax of the theory \texttt{Set} (continued)} \label{hol-set-syntax2} \end{figure} \section{A formulation of set theory} Historically, higher-order logic gives a foundation for Russell and Whitehead's theory of classes. Let us use modern terminology and call them {\bf sets}, but note that these sets are distinct from those of ZF set theory, and behave more like ZF classes. \begin{itemize} \item Sets are given by predicates over some type~$\sigma$. Types serve to define universes for sets, but type-checking is still significant. \item There is a universal set (for each type). Thus, sets have complements, and may be defined by absolute comprehension. \item Although sets may contain other sets as elements, the containing set must have a more complex type. \end{itemize} Finite unions and intersections have the same behaviour in HOL as they do in~ZF. In HOL the intersection of the empty set is well-defined, denoting the universal set for the given type. \subsection{Syntax of set theory}\index{*set type} HOL's set theory is called \thydx{Set}. The type $\alpha\,set$ is essentially the same as $\alpha\To bool$. The new type is defined for clarity and to avoid complications involving function types in unification. The isomorphisms between the two types are declared explicitly. They are very natural: \texttt{Collect} maps $\alpha\To bool$ to $\alpha\,set$, while \hbox{\tt op :} maps in the other direction (ignoring argument order). Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax translations. Figure~\ref{hol-set-syntax2} presents the grammar of the new constructs. Infix operators include union and intersection ($A\un B$ and $A\int B$), the subset and membership relations, and the image operator~{\tt``}\@. Note that $a$\verb|~:|$b$ is translated to $\lnot(a\in b)$. The $\{a@1,\ldots\}$ notation abbreviates finite sets constructed in the obvious manner using~\texttt{insert} and~$\{\}$: \begin{eqnarray*} \{a, b, c\} & \equiv & \texttt{insert} \, a \, ({\tt insert} \, b \, ({\tt insert} \, c \, \{\})) \end{eqnarray*} The set \hbox{\tt{\ttlbrace}$x$.\ $P[x]${\ttrbrace}} consists of all $x$ (of suitable type) that satisfy~$P[x]$, where $P[x]$ is a formula that may contain free occurrences of~$x$. This syntax expands to \cdx{Collect}$(\lambda x. P[x])$. It defines sets by absolute comprehension, which is impossible in~ZF; the type of~$x$ implicitly restricts the comprehension. The set theory defines two {\bf bounded quantifiers}: \begin{eqnarray*} \forall x\in A. P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\ \exists x\in A. P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x] \end{eqnarray*} The constants~\cdx{Ball} and~\cdx{Bex} are defined accordingly. Instead of \texttt{Ball $A$ $P$} and \texttt{Bex $A$ $P$} we may write\index{*"! symbol}\index{*"? symbol} \index{*ALL symbol}\index{*EX symbol} % \hbox{\tt ALL~$x$:$A$.\ $P[x]$} and \hbox{\tt EX~$x$:$A$.\ $P[x]$}. The original notation of Gordon's {\sc hol} system is supported as well: \texttt{!}\ and \texttt{?}. Unions and intersections over sets, namely $\bigcup@{x\in A}B[x]$ and $\bigcap@{x\in A}B[x]$, are written \sdx{UN}~\hbox{\tt$x$:$A$.\ $B[x]$} and \sdx{INT}~\hbox{\tt$x$:$A$.\ $B[x]$}. Unions and intersections over types, namely $\bigcup@x B[x]$ and $\bigcap@x B[x]$, are written \sdx{UN}~\hbox{\tt$x$.\ $B[x]$} and \sdx{INT}~\hbox{\tt$x$.\ $B[x]$}. They are equivalent to the previous union and intersection operators when $A$ is the universal set. The operators $\bigcup A$ and $\bigcap A$ act upon sets of sets. They are not binders, but are equal to $\bigcup@{x\in A}x$ and $\bigcap@{x\in A}x$, respectively. \begin{figure} \underscoreon \begin{ttbox} \tdx{mem_Collect_eq} (a : {\ttlbrace}x. P x{\ttrbrace}) = P a \tdx{Collect_mem_eq} {\ttlbrace}x. x:A{\ttrbrace} = A \tdx{empty_def} {\ttlbrace}{\ttrbrace} == {\ttlbrace}x. False{\ttrbrace} \tdx{insert_def} insert a B == {\ttlbrace}x. x=a{\ttrbrace} Un B \tdx{Ball_def} Ball A P == ! x. x:A --> P x \tdx{Bex_def} Bex A P == ? x. x:A & P x \tdx{subset_def} A <= B == ! x:A. x:B \tdx{Un_def} A Un B == {\ttlbrace}x. x:A | x:B{\ttrbrace} \tdx{Int_def} A Int B == {\ttlbrace}x. x:A & x:B{\ttrbrace} \tdx{set_diff_def} A - B == {\ttlbrace}x. x:A & x~:B{\ttrbrace} \tdx{Compl_def} -A == {\ttlbrace}x. ~ x:A{\ttrbrace} \tdx{INTER_def} INTER A B == {\ttlbrace}y. ! x:A. y: B x{\ttrbrace} \tdx{UNION_def} UNION A B == {\ttlbrace}y. ? x:A. y: B x{\ttrbrace} \tdx{INTER1_def} INTER1 B == INTER {\ttlbrace}x. True{\ttrbrace} B \tdx{UNION1_def} UNION1 B == UNION {\ttlbrace}x. True{\ttrbrace} B \tdx{Inter_def} Inter S == (INT x:S. x) \tdx{Union_def} Union S == (UN x:S. x) \tdx{Pow_def} Pow A == {\ttlbrace}B. B <= A{\ttrbrace} \tdx{image_def} f``A == {\ttlbrace}y. ? x:A. y=f x{\ttrbrace} \tdx{range_def} range f == {\ttlbrace}y. ? x. y=f x{\ttrbrace} \end{ttbox} \caption{Rules of the theory \texttt{Set}} \label{hol-set-rules} \end{figure} \begin{figure} \underscoreon \begin{ttbox} \tdx{CollectI} [| P a |] ==> a : {\ttlbrace}x. P x{\ttrbrace} \tdx{CollectD} [| a : {\ttlbrace}x. P x{\ttrbrace} |] ==> P a \tdx{CollectE} [| a : {\ttlbrace}x. P x{\ttrbrace}; P a ==> W |] ==> W \tdx{ballI} [| !!x. x:A ==> P x |] ==> ! x:A. P x \tdx{bspec} [| ! x:A. P x; x:A |] ==> P x \tdx{ballE} [| ! x:A. P x; P x ==> Q; ~ x:A ==> Q |] ==> Q \tdx{bexI} [| P x; x:A |] ==> ? x:A. P x \tdx{bexCI} [| ! x:A. ~ P x ==> P a; a:A |] ==> ? x:A. P x \tdx{bexE} [| ? x:A. P x; !!x. [| x:A; P x |] ==> Q |] ==> Q \subcaption{Comprehension and Bounded quantifiers} \tdx{subsetI} (!!x. x:A ==> x:B) ==> A <= B \tdx{subsetD} [| A <= B; c:A |] ==> c:B \tdx{subsetCE} [| A <= B; ~ (c:A) ==> P; c:B ==> P |] ==> P \tdx{subset_refl} A <= A \tdx{subset_trans} [| A<=B; B<=C |] ==> A<=C \tdx{equalityI} [| A <= B; B <= A |] ==> A = B \tdx{equalityD1} A = B ==> A<=B \tdx{equalityD2} A = B ==> B<=A \tdx{equalityE} [| A = B; [| A<=B; B<=A |] ==> P |] ==> P \tdx{equalityCE} [| A = B; [| c:A; c:B |] ==> P; [| ~ c:A; ~ c:B |] ==> P |] ==> P \subcaption{The subset and equality relations} \end{ttbox} \caption{Derived rules for set theory} \label{hol-set1} \end{figure} \begin{figure} \underscoreon \begin{ttbox} \tdx{emptyE} a : {\ttlbrace}{\ttrbrace} ==> P \tdx{insertI1} a : insert a B \tdx{insertI2} a : B ==> a : insert b B \tdx{insertE} [| a : insert b A; a=b ==> P; a:A ==> P |] ==> P \tdx{ComplI} [| c:A ==> False |] ==> c : -A \tdx{ComplD} [| c : -A |] ==> ~ c:A \tdx{UnI1} c:A ==> c : A Un B \tdx{UnI2} c:B ==> c : A Un B \tdx{UnCI} (~c:B ==> c:A) ==> c : A Un B \tdx{UnE} [| c : A Un B; c:A ==> P; c:B ==> P |] ==> P \tdx{IntI} [| c:A; c:B |] ==> c : A Int B \tdx{IntD1} c : A Int B ==> c:A \tdx{IntD2} c : A Int B ==> c:B \tdx{IntE} [| c : A Int B; [| c:A; c:B |] ==> P |] ==> P \tdx{UN_I} [| a:A; b: B a |] ==> b: (UN x:A. B x) \tdx{UN_E} [| b: (UN x:A. B x); !!x.[| x:A; b:B x |] ==> R |] ==> R \tdx{INT_I} (!!x. x:A ==> b: B x) ==> b : (INT x:A. B x) \tdx{INT_D} [| b: (INT x:A. B x); a:A |] ==> b: B a \tdx{INT_E} [| b: (INT x:A. B x); b: B a ==> R; ~ a:A ==> R |] ==> R \tdx{UnionI} [| X:C; A:X |] ==> A : Union C \tdx{UnionE} [| A : Union C; !!X.[| A:X; X:C |] ==> R |] ==> R \tdx{InterI} [| !!X. X:C ==> A:X |] ==> A : Inter C \tdx{InterD} [| A : Inter C; X:C |] ==> A:X \tdx{InterE} [| A : Inter C; A:X ==> R; ~ X:C ==> R |] ==> R \tdx{PowI} A<=B ==> A: Pow B \tdx{PowD} A: Pow B ==> A<=B \tdx{imageI} [| x:A |] ==> f x : f``A \tdx{imageE} [| b : f``A; !!x.[| b=f x; x:A |] ==> P |] ==> P \tdx{rangeI} f x : range f \tdx{rangeE} [| b : range f; !!x.[| b=f x |] ==> P |] ==> P \end{ttbox} \caption{Further derived rules for set theory} \label{hol-set2} \end{figure} \subsection{Axioms and rules of set theory} Figure~\ref{hol-set-rules} presents the rules of theory \thydx{Set}. The axioms \tdx{mem_Collect_eq} and \tdx{Collect_mem_eq} assert that the functions \texttt{Collect} and \hbox{\tt op :} are isomorphisms. Of course, \hbox{\tt op :} also serves as the membership relation. All the other axioms are definitions. They include the empty set, bounded quantifiers, unions, intersections, complements and the subset relation. They also include straightforward constructions on functions: image~({\tt``}) and \texttt{range}. %The predicate \cdx{inj_on} is used for simulating type definitions. %The statement ${\tt inj_on}~f~A$ asserts that $f$ is injective on the %set~$A$, which specifies a subset of its domain type. In a type %definition, $f$ is the abstraction function and $A$ is the set of valid %representations; we should not expect $f$ to be injective outside of~$A$. %\begin{figure} \underscoreon %\begin{ttbox} %\tdx{Inv_f_f} inj f ==> Inv f (f x) = x %\tdx{f_Inv_f} y : range f ==> f(Inv f y) = y % %\tdx{Inv_injective} % [| Inv f x=Inv f y; x: range f; y: range f |] ==> x=y % % %\tdx{monoI} [| !!A B. A <= B ==> f A <= f B |] ==> mono f %\tdx{monoD} [| mono f; A <= B |] ==> f A <= f B % %\tdx{injI} [| !! x y. f x = f y ==> x=y |] ==> inj f %\tdx{inj_inverseI} (!!x. g(f x) = x) ==> inj f %\tdx{injD} [| inj f; f x = f y |] ==> x=y % %\tdx{inj_onI} (!!x y. [| f x=f y; x:A; y:A |] ==> x=y) ==> inj_on f A %\tdx{inj_onD} [| inj_on f A; f x=f y; x:A; y:A |] ==> x=y % %\tdx{inj_on_inverseI} % (!!x. x:A ==> g(f x) = x) ==> inj_on f A %\tdx{inj_on_contraD} % [| inj_on f A; x~=y; x:A; y:A |] ==> ~ f x=f y %\end{ttbox} %\caption{Derived rules involving functions} \label{hol-fun} %\end{figure} \begin{figure} \underscoreon \begin{ttbox} \tdx{Union_upper} B:A ==> B <= Union A \tdx{Union_least} [| !!X. X:A ==> X<=C |] ==> Union A <= C \tdx{Inter_lower} B:A ==> Inter A <= B \tdx{Inter_greatest} [| !!X. X:A ==> C<=X |] ==> C <= Inter A \tdx{Un_upper1} A <= A Un B \tdx{Un_upper2} B <= A Un B \tdx{Un_least} [| A<=C; B<=C |] ==> A Un B <= C \tdx{Int_lower1} A Int B <= A \tdx{Int_lower2} A Int B <= B \tdx{Int_greatest} [| C<=A; C<=B |] ==> C <= A Int B \end{ttbox} \caption{Derived rules involving subsets} \label{hol-subset} \end{figure} \begin{figure} \underscoreon \hfuzz=4pt%suppress "Overfull \hbox" message \begin{ttbox} \tdx{Int_absorb} A Int A = A \tdx{Int_commute} A Int B = B Int A \tdx{Int_assoc} (A Int B) Int C = A Int (B Int C) \tdx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C) \tdx{Un_absorb} A Un A = A \tdx{Un_commute} A Un B = B Un A \tdx{Un_assoc} (A Un B) Un C = A Un (B Un C) \tdx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C) \tdx{Compl_disjoint} A Int (-A) = {\ttlbrace}x. False{\ttrbrace} \tdx{Compl_partition} A Un (-A) = {\ttlbrace}x. True{\ttrbrace} \tdx{double_complement} -(-A) = A \tdx{Compl_Un} -(A Un B) = (-A) Int (-B) \tdx{Compl_Int} -(A Int B) = (-A) Un (-B) \tdx{Union_Un_distrib} Union(A Un B) = (Union A) Un (Union B) \tdx{Int_Union} A Int (Union B) = (UN C:B. A Int C) \tdx{Inter_Un_distrib} Inter(A Un B) = (Inter A) Int (Inter B) \tdx{Un_Inter} A Un (Inter B) = (INT C:B. A Un C) \end{ttbox} \caption{Set equalities} \label{hol-equalities} \end{figure} %\tdx{Un_Union_image} (UN x:C.(A x) Un (B x)) = Union(A``C) Un Union(B``C) %\tdx{Int_Inter_image} (INT x:C.(A x) Int (B x)) = Inter(A``C) Int Inter(B``C) Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules. Most are obvious and resemble rules of Isabelle's ZF set theory. Certain rules, such as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI}, are designed for classical reasoning; the rules \tdx{subsetD}, \tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are not strictly necessary but yield more natural proofs. Similarly, \tdx{equalityCE} supports classical reasoning about extensionality, after the fashion of \tdx{iffCE}. See the file \texttt{HOL/Set.ML} for proofs pertaining to set theory. Figure~\ref{hol-subset} presents lattice properties of the subset relation. Unions form least upper bounds; non-empty intersections form greatest lower bounds. Reasoning directly about subsets often yields clearer proofs than reasoning about the membership relation. See the file \texttt{HOL/subset.ML}. Figure~\ref{hol-equalities} presents many common set equalities. They include commutative, associative and distributive laws involving unions, intersections and complements. For a complete listing see the file {\tt HOL/equalities.ML}. \begin{warn} \texttt{Blast_tac} proves many set-theoretic theorems automatically. Hence you seldom need to refer to the theorems above. \end{warn} \begin{figure} \begin{center} \begin{tabular}{rrr} \it name &\it meta-type & \it description \\ \cdx{inj}~~\cdx{surj}& $(\alpha\To\beta )\To bool$ & injective/surjective \\ \cdx{inj_on} & $[\alpha\To\beta ,\alpha\,set]\To bool$ & injective over subset\\ \cdx{inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & inverse function \end{tabular} \end{center} \underscoreon \begin{ttbox} \tdx{inj_def} inj f == ! x y. f x=f y --> x=y \tdx{surj_def} surj f == ! y. ? x. y=f x \tdx{inj_on_def} inj_on f A == !x:A. !y:A. f x=f y --> x=y \tdx{inv_def} inv f == (\%y. @x. f(x)=y) \end{ttbox} \caption{Theory \thydx{Fun}} \label{fig:HOL:Fun} \end{figure} \subsection{Properties of functions}\nopagebreak Figure~\ref{fig:HOL:Fun} presents a theory of simple properties of functions. Note that ${\tt inv}~f$ uses Hilbert's $\varepsilon$ to yield an inverse of~$f$. See the file \texttt{HOL/Fun.ML} for a complete listing of the derived rules. Reasoning about function composition (the operator~\sdx{o}) and the predicate~\cdx{surj} is done simply by expanding the definitions. There is also a large collection of monotonicity theorems for constructions on sets in the file \texttt{HOL/mono.ML}. \section{Generic packages} \label{sec:HOL:generic-packages} HOL instantiates most of Isabelle's generic packages, making available the simplifier and the classical reasoner. \subsection{Simplification and substitution} Simplification tactics tactics such as \texttt{Asm_simp_tac} and \texttt{Full_simp_tac} use the default simpset (\texttt{simpset()}), which works for most purposes. A quite minimal simplification set for higher-order logic is~\ttindexbold{HOL_ss}; even more frugal is \ttindexbold{HOL_basic_ss}. Equality~($=$), which also expresses logical equivalence, may be used for rewriting. See the file \texttt{HOL/simpdata.ML} for a complete listing of the basic simplification rules. See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% {Chaps.\ts\ref{substitution} and~\ref{simp-chap}} for details of substitution and simplification. \begin{warn}\index{simplification!of conjunctions}% Reducing $a=b\conj P(a)$ to $a=b\conj P(b)$ is sometimes advantageous. The left part of a conjunction helps in simplifying the right part. This effect is not available by default: it can be slow. It can be obtained by including \ttindex{conj_cong} in a simpset, \verb$addcongs [conj_cong]$. \end{warn} \begin{warn}\index{simplification!of \texttt{if}}\label{if-simp}% By default only the condition of an \ttindex{if} is simplified but not the \texttt{then} and \texttt{else} parts. Of course the latter are simplified once the condition simplifies to \texttt{True} or \texttt{False}. To ensure full simplification of all parts of a conditional you must remove \ttindex{if_weak_cong} from the simpset, \verb$delcongs [if_weak_cong]$. \end{warn} If the simplifier cannot use a certain rewrite rule --- either because of nontermination or because its left-hand side is too flexible --- then you might try \texttt{stac}: \begin{ttdescription} \item[\ttindexbold{stac} $thm$ $i,$] where $thm$ is of the form $lhs = rhs$, replaces in subgoal $i$ instances of $lhs$ by corresponding instances of $rhs$. In case of multiple instances of $lhs$ in subgoal $i$, backtracking may be necessary to select the desired ones. If $thm$ is a conditional equality, the instantiated condition becomes an additional (first) subgoal. \end{ttdescription} HOL provides the tactic \ttindex{hyp_subst_tac}, which substitutes for an equality throughout a subgoal and its hypotheses. This tactic uses HOL's general substitution rule. \subsubsection{Case splitting} \label{subsec:HOL:case:splitting} HOL also provides convenient means for case splitting during rewriting. Goals containing a subterm of the form \texttt{if}~$b$~{\tt then\dots else\dots} often require a case distinction on $b$. This is expressed by the theorem \tdx{split_if}: $$ \Var{P}(\mbox{\tt if}~\Var{b}~{\tt then}~\Var{x}~\mbox{\tt else}~\Var{y})~=~ ((\Var{b} \to \Var{P}(\Var{x})) \land (\lnot \Var{b} \to \Var{P}(\Var{y}))) \eqno{(*)} $$ For example, a simple instance of $(*)$ is \[ x \in (\mbox{\tt if}~x \in A~{\tt then}~A~\mbox{\tt else}~\{x\})~=~ ((x \in A \to x \in A) \land (x \notin A \to x \in \{x\})) \] Because $(*)$ is too general as a rewrite rule for the simplifier (the left-hand side is not a higher-order pattern in the sense of \iflabelundefined{chap:simplification}{the {\em Reference Manual\/}}% {Chap.\ts\ref{chap:simplification}}), there is a special infix function \ttindexbold{addsplits} of type \texttt{simpset * thm list -> simpset} (analogous to \texttt{addsimps}) that adds rules such as $(*)$ to a simpset, as in \begin{ttbox} by(simp_tac (simpset() addsplits [split_if]) 1); \end{ttbox} The effect is that after each round of simplification, one occurrence of \texttt{if} is split acording to \texttt{split_if}, until all occurences of \texttt{if} have been eliminated. It turns out that using \texttt{split_if} is almost always the right thing to do. Hence \texttt{split_if} is already included in the default simpset. If you want to delete it from a simpset, use \ttindexbold{delsplits}, which is the inverse of \texttt{addsplits}: \begin{ttbox} by(simp_tac (simpset() delsplits [split_if]) 1); \end{ttbox} In general, \texttt{addsplits} accepts rules of the form \[ \Var{P}(c~\Var{x@1}~\dots~\Var{x@n})~=~ rhs \] where $c$ is a constant and $rhs$ is arbitrary. Note that $(*)$ is of the right form because internally the left-hand side is $\Var{P}(\mathtt{If}~\Var{b}~\Var{x}~~\Var{y})$. Important further examples are splitting rules for \texttt{case} expressions (see~{\S}\ref{subsec:list} and~{\S}\ref{subsec:datatype:basics}). Analogous to \texttt{Addsimps} and \texttt{Delsimps}, there are also imperative versions of \texttt{addsplits} and \texttt{delsplits} \begin{ttbox} \ttindexbold{Addsplits}: thm list -> unit \ttindexbold{Delsplits}: thm list -> unit \end{ttbox} for adding splitting rules to, and deleting them from the current simpset. \subsection{Classical reasoning} HOL derives classical introduction rules for $\disj$ and~$\exists$, as well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule; recall Fig.\ts\ref{hol-lemmas2} above. The classical reasoner is installed. Tactics such as \texttt{Blast_tac} and {\tt Best_tac} refer to the default claset (\texttt{claset()}), which works for most purposes. Named clasets include \ttindexbold{prop_cs}, which includes the propositional rules, and \ttindexbold{HOL_cs}, which also includes quantifier rules. See the file \texttt{HOL/cladata.ML} for lists of the classical rules, and \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% {Chap.\ts\ref{chap:classical}} for more discussion of classical proof methods. %FIXME outdated, both from the Isabelle and SVC perspective % \section{Calling the decision procedure SVC}\label{sec:HOL:SVC} % \index{SVC decision procedure|(} % The Stanford Validity Checker (SVC) is a tool that can check the validity of % certain types of formulae. If it is installed on your machine, then % Isabelle/HOL can be configured to call it through the tactic % \ttindex{svc_tac}. It is ideal for large tautologies and complex problems in % linear arithmetic. Subexpressions that SVC cannot handle are automatically % replaced by variables, so you can call the tactic on any subgoal. See the % file \texttt{HOL/ex/svc_test.ML} for examples. % \begin{ttbox} % svc_tac : int -> tactic % Svc.trace : bool ref \hfill{\bf initially false} % \end{ttbox} % \begin{ttdescription} % \item[\ttindexbold{svc_tac} $i$] attempts to prove subgoal~$i$ by translating % it into a formula recognized by~SVC\@. If it succeeds then the subgoal is % removed. It fails if SVC is unable to prove the subgoal. It crashes with % an error message if SVC appears not to be installed. Numeric variables may % have types \texttt{nat}, \texttt{int} or \texttt{real}. % \item[\ttindexbold{Svc.trace}] is a flag that, if set, causes \texttt{svc_tac} % to trace its operations: abstraction of the subgoal, translation to SVC % syntax, SVC's response. % \end{ttdescription} % Here is an example, with tracing turned on: % \begin{ttbox} % set Svc.trace; % {\out val it : bool = true} % Goal "(#3::nat)*a <= #2 + #4*b + #6*c & #11 <= #2*a + b + #2*c & \ttback % \ttback a + #3*b <= #5 + #2*c --> #2 + #3*b <= #2*a + #6*c"; % by (svc_tac 1); % {\out Subgoal abstracted to} % {\out #3 * a <= #2 + #4 * b + #6 * c &} % {\out #11 <= #2 * a + b + #2 * c & a + #3 * b <= #5 + #2 * c -->} % {\out #2 + #3 * b <= #2 * a + #6 * c} % {\out Calling SVC:} % {\out (=> (<= 0 (F_c) ) (=> (<= 0 (F_b) ) (=> (<= 0 (F_a) )} % {\out (=> (AND (<= {* 3 (F_a) } {+ {+ 2 {* 4 (F_b) } } } % {\out {* 6 (F_c) } } ) (AND (<= 11 {+ {+ {* 2 (F_a) } (F_b) }} % {\out {* 2 (F_c) } } ) (<= {+ (F_a) {* 3 (F_b) } } {+ 5 } % {\out {* 2 (F_c) } } ) ) ) (< {+ 2 {* 3 (F_b) } } {+ 1 {+ } % {\out {* 2 (F_a) } {* 6 (F_c) } } } ) ) ) ) ) } % {\out SVC Returns:} % {\out VALID} % {\out Level 1} % {\out #3 * a <= #2 + #4 * b + #6 * c &} % {\out #11 <= #2 * a + b + #2 * c & a + #3 * b <= #5 + #2 * c -->} % {\out #2 + #3 * b <= #2 * a + #6 * c} % {\out No subgoals!} % \end{ttbox} % \begin{warn} % Calling \ttindex{svc_tac} entails an above-average risk of % unsoundness. Isabelle does not check SVC's result independently. Moreover, % the tactic translates the submitted formula using code that lies outside % Isabelle's inference core. Theorems that depend upon results proved using SVC % (and other oracles) are displayed with the annotation \texttt{[!]} attached. % You can also use \texttt{\#der (rep_thm $th$)} to examine the proof object of % theorem~$th$, as described in the \emph{Reference Manual}. % \end{warn} % To start, first download SVC from the Internet at URL % \begin{ttbox} % http://agamemnon.stanford.edu/~levitt/vc/index.html % \end{ttbox} % and install it using the instructions supplied. SVC requires two environment % variables: % \begin{ttdescription} % \item[\ttindexbold{SVC_HOME}] is an absolute pathname to the SVC % distribution directory. % \item[\ttindexbold{SVC_MACHINE}] identifies the type of computer and % operating system. % \end{ttdescription} % You can set these environment variables either using the Unix shell or through % an Isabelle \texttt{settings} file. Isabelle assumes SVC to be installed if % \texttt{SVC_HOME} is defined. % \paragraph*{Acknowledgement.} This interface uses code supplied by S{\o}ren % Heilmann. % \index{SVC decision procedure|)} \section{Types}\label{sec:HOL:Types} This section describes HOL's basic predefined types ($\alpha \times \beta$, $\alpha + \beta$, $nat$ and $\alpha \; list$) and ways for introducing new types in general. The most important type construction, the \texttt{datatype}, is treated separately in {\S}\ref{sec:HOL:datatype}. \subsection{Product and sum types}\index{*"* type}\index{*"+ type} \label{subsec:prod-sum} \begin{figure}[htbp] \begin{constants} \it symbol & \it meta-type & & \it description \\ \cdx{Pair} & $[\alpha,\beta]\To \alpha\times\beta$ & & ordered pairs $(a,b)$ \\ \cdx{fst} & $\alpha\times\beta \To \alpha$ & & first projection\\ \cdx{snd} & $\alpha\times\beta \To \beta$ & & second projection\\ \cdx{split} & $[[\alpha,\beta]\To\gamma, \alpha\times\beta] \To \gamma$ & & generalized projection\\ \cdx{Sigma} & $[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ & & general sum of sets \end{constants} %\tdx{fst_def} fst p == @a. ? b. p = (a,b) %\tdx{snd_def} snd p == @b. ? a. p = (a,b) %\tdx{split_def} split c p == c (fst p) (snd p) \begin{ttbox}\makeatletter \tdx{Sigma_def} Sigma A B == UN x:A. UN y:B x. {\ttlbrace}(x,y){\ttrbrace} \tdx{Pair_eq} ((a,b) = (a',b')) = (a=a' & b=b') \tdx{Pair_inject} [| (a, b) = (a',b'); [| a=a'; b=b' |] ==> R |] ==> R \tdx{PairE} [| !!x y. p = (x,y) ==> Q |] ==> Q \tdx{fst_conv} fst (a,b) = a \tdx{snd_conv} snd (a,b) = b \tdx{surjective_pairing} p = (fst p,snd p) \tdx{split} split c (a,b) = c a b \tdx{split_split} R(split c p) = (! x y. p = (x,y) --> R(c x y)) \tdx{SigmaI} [| a:A; b:B a |] ==> (a,b) : Sigma A B \tdx{SigmaE} [| c:Sigma A B; !!x y.[| x:A; y:B x; c=(x,y) |] ==> P |] ==> P \end{ttbox} \caption{Type $\alpha\times\beta$}\label{hol-prod} \end{figure} Theory \thydx{Prod} (Fig.\ts\ref{hol-prod}) defines the product type $\alpha\times\beta$, with the ordered pair syntax $(a, b)$. General tuples are simulated by pairs nested to the right: \begin{center} \begin{tabular}{c|c} external & internal \\ \hline $\tau@1 \times \dots \times \tau@n$ & $\tau@1 \times (\dots (\tau@{n-1} \times \tau@n)\dots)$ \\ \hline $(t@1,\dots,t@n)$ & $(t@1,(\dots,(t@{n-1},t@n)\dots)$ \\ \end{tabular} \end{center} In addition, it is possible to use tuples as patterns in abstractions: \begin{center} {\tt\%($x$,$y$). $t$} \quad stands for\quad \texttt{split(\%$x$\thinspace$y$.\ $t$)} \end{center} Nested patterns are also supported. They are translated stepwise: \begin{eqnarray*} \hbox{\tt\%($x$,$y$,$z$).\ $t$} & \leadsto & \hbox{\tt\%($x$,($y$,$z$)).\ $t$} \\ & \leadsto & \hbox{\tt split(\%$x$.\%($y$,$z$).\ $t$)}\\ & \leadsto & \hbox{\tt split(\%$x$.\ split(\%$y$ $z$.\ $t$))} \end{eqnarray*} The reverse translation is performed upon printing. \begin{warn} The translation between patterns and \texttt{split} is performed automatically by the parser and printer. Thus the internal and external form of a term may differ, which can affects proofs. For example the term {\tt (\%(x,y).(y,x))(a,b)} requires the theorem \texttt{split} (which is in the default simpset) to rewrite to {\tt(b,a)}. \end{warn} In addition to explicit $\lambda$-abstractions, patterns can be used in any variable binding construct which is internally described by a $\lambda$-abstraction. Some important examples are \begin{description} \item[Let:] \texttt{let {\it pattern} = $t$ in $u$} \item[Quantifiers:] \texttt{ALL~{\it pattern}:$A$.~$P$} \item[Choice:] {\underscoreon \tt SOME~{\it pattern}.~$P$} \item[Set operations:] \texttt{UN~{\it pattern}:$A$.~$B$} \item[Sets:] \texttt{{\ttlbrace}{\it pattern}.~$P${\ttrbrace}} \end{description} There is a simple tactic which supports reasoning about patterns: \begin{ttdescription} \item[\ttindexbold{split_all_tac} $i$] replaces in subgoal $i$ all {\tt!!}-quantified variables of product type by individual variables for each component. A simple example: \begin{ttbox} {\out 1. !!p. (\%(x,y,z). (x, y, z)) p = p} by(split_all_tac 1); {\out 1. !!x xa ya. (\%(x,y,z). (x, y, z)) (x, xa, ya) = (x, xa, ya)} \end{ttbox} \end{ttdescription} Theory \texttt{Prod} also introduces the degenerate product type \texttt{unit} which contains only a single element named {\tt()} with the property \begin{ttbox} \tdx{unit_eq} u = () \end{ttbox} \bigskip Theory \thydx{Sum} (Fig.~\ref{hol-sum}) defines the sum type $\alpha+\beta$ which associates to the right and has a lower priority than $*$: $\tau@1 + \tau@2 + \tau@3*\tau@4$ means $\tau@1 + (\tau@2 + (\tau@3*\tau@4))$. The definition of products and sums in terms of existing types is not shown. The constructions are fairly standard and can be found in the respective theory files. Although the sum and product types are constructed manually for foundational reasons, they are represented as actual datatypes later (see {\S}\ref{subsec:datatype:rep_datatype}). Therefore, the theory \texttt{Datatype} should be used instead of \texttt{Sum} or \texttt{Prod}. \begin{figure} \begin{constants} \it symbol & \it meta-type & & \it description \\ \cdx{Inl} & $\alpha \To \alpha+\beta$ & & first injection\\ \cdx{Inr} & $\beta \To \alpha+\beta$ & & second injection\\ \cdx{sum_case} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$ & & conditional \end{constants} \begin{ttbox}\makeatletter \tdx{Inl_not_Inr} Inl a ~= Inr b \tdx{inj_Inl} inj Inl \tdx{inj_Inr} inj Inr \tdx{sumE} [| !!x. P(Inl x); !!y. P(Inr y) |] ==> P s \tdx{sum_case_Inl} sum_case f g (Inl x) = f x \tdx{sum_case_Inr} sum_case f g (Inr x) = g x \tdx{surjective_sum} sum_case (\%x. f(Inl x)) (\%y. f(Inr y)) s = f s \tdx{sum.split_case} R(sum_case f g s) = ((! x. s = Inl(x) --> R(f(x))) & (! y. s = Inr(y) --> R(g(y)))) \end{ttbox} \caption{Type $\alpha+\beta$}\label{hol-sum} \end{figure} \begin{figure} \index{*"< symbol} \index{*"* symbol} \index{*div symbol} \index{*mod symbol} \index{*dvd symbol} \index{*"+ symbol} \index{*"- symbol} \begin{constants} \it symbol & \it meta-type & \it priority & \it description \\ \cdx{0} & $\alpha$ & & zero \\ \cdx{Suc} & $nat \To nat$ & & successor function\\ \tt * & $[\alpha,\alpha]\To \alpha$ & Left 70 & multiplication \\ \tt div & $[\alpha,\alpha]\To \alpha$ & Left 70 & division\\ \tt mod & $[\alpha,\alpha]\To \alpha$ & Left 70 & modulus\\ \tt dvd & $[\alpha,\alpha]\To bool$ & Left 70 & ``divides'' relation\\ \tt + & $[\alpha,\alpha]\To \alpha$ & Left 65 & addition\\ \tt - & $[\alpha,\alpha]\To \alpha$ & Left 65 & subtraction \end{constants} \subcaption{Constants and infixes} \begin{ttbox}\makeatother \tdx{nat_induct} [| P 0; !!n. P n ==> P(Suc n) |] ==> P n \tdx{Suc_not_Zero} Suc m ~= 0 \tdx{inj_Suc} inj Suc \tdx{n_not_Suc_n} n~=Suc n \subcaption{Basic properties} \end{ttbox} \caption{The type of natural numbers, \tydx{nat}} \label{hol-nat1} \end{figure} \begin{figure} \begin{ttbox}\makeatother 0+n = n (Suc m)+n = Suc(m+n) m-0 = m 0-n = n Suc(m)-Suc(n) = m-n 0*n = 0 Suc(m)*n = n + m*n \tdx{mod_less} m<n ==> m mod n = m \tdx{mod_geq} [| 0<n; ~m<n |] ==> m mod n = (m-n) mod n \tdx{div_less} m<n ==> m div n = 0 \tdx{div_geq} [| 0<n; ~m<n |] ==> m div n = Suc((m-n) div n) \end{ttbox} \caption{Recursion equations for the arithmetic operators} \label{hol-nat2} \end{figure} \subsection{The type of natural numbers, \textit{nat}} \index{nat@{\textit{nat}} type|(} The theory \thydx{Nat} defines the natural numbers in a roundabout but traditional way. The axiom of infinity postulates a type~\tydx{ind} of individuals, which is non-empty and closed under an injective operation. The natural numbers are inductively generated by choosing an arbitrary individual for~0 and using the injective operation to take successors. This is a least fixedpoint construction. Type~\tydx{nat} is an instance of class~\cldx{ord}, which makes the overloaded functions of this class (especially \cdx{<} and \cdx{<=}, but also \cdx{min}, \cdx{max} and \cdx{LEAST}) available on \tydx{nat}. Theory \thydx{Nat} also shows that {\tt<=} is a linear order, so \tydx{nat} is also an instance of class \cldx{linorder}. Theory \thydx{NatArith} develops arithmetic on the natural numbers. It defines addition, multiplication and subtraction. Theory \thydx{Divides} defines division, remainder and the ``divides'' relation. The numerous theorems proved include commutative, associative, distributive, identity and cancellation laws. See Figs.\ts\ref{hol-nat1} and~\ref{hol-nat2}. The recursion equations for the operators \texttt{+}, \texttt{-} and \texttt{*} on \texttt{nat} are part of the default simpset. Functions on \tydx{nat} can be defined by primitive or well-founded recursion; see {\S}\ref{sec:HOL:recursive}. A simple example is addition. Here, \texttt{op +} is the name of the infix operator~\texttt{+}, following the standard convention. \begin{ttbox} \sdx{primrec} "0 + n = n" "Suc m + n = Suc (m + n)" \end{ttbox} There is also a \sdx{case}-construct of the form \begin{ttbox} case \(e\) of 0 => \(a\) | Suc \(m\) => \(b\) \end{ttbox} Note that Isabelle insists on precisely this format; you may not even change the order of the two cases. Both \texttt{primrec} and \texttt{case} are realized by a recursion operator \cdx{nat_rec}, which is available because \textit{nat} is represented as a datatype (see {\S}\ref{subsec:datatype:rep_datatype}). %The predecessor relation, \cdx{pred_nat}, is shown to be well-founded. %Recursion along this relation resembles primitive recursion, but is %stronger because we are in higher-order logic; using primitive recursion to %define a higher-order function, we can easily Ackermann's function, which %is not primitive recursive \cite[page~104]{thompson91}. %The transitive closure of \cdx{pred_nat} is~$<$. Many functions on the %natural numbers are most easily expressed using recursion along~$<$. Tactic {\tt\ttindex{induct_tac} "$n$" $i$} performs induction on variable~$n$ in subgoal~$i$ using theorem \texttt{nat_induct}. There is also the derived theorem \tdx{less_induct}: \begin{ttbox} [| !!n. [| ! m. m<n --> P m |] ==> P n |] ==> P n \end{ttbox} \subsection{Numerical types and numerical reasoning} The integers (type \tdx{int}) are also available in HOL, and the reals (type \tdx{real}) are available in the logic image \texttt{HOL-Complex}. They support the expected operations of addition (\texttt{+}), subtraction (\texttt{-}) and multiplication (\texttt{*}), and much else. Type \tdx{int} provides the \texttt{div} and \texttt{mod} operators, while type \tdx{real} provides real division and other operations. Both types belong to class \cldx{linorder}, so they inherit the relational operators and all the usual properties of linear orderings. For full details, please survey the theories in subdirectories \texttt{Integ}, \texttt{Real}, and \texttt{Complex}. All three numeric types admit numerals of the form \texttt{$sd\ldots d$}, where $s$ is an optional minus sign and $d\ldots d$ is a string of digits. Numerals are represented internally by a datatype for binary notation, which allows numerical calculations to be performed by rewriting. For example, the integer division of \texttt{54342339} by \texttt{3452} takes about five seconds. By default, the simplifier cancels like terms on the opposite sites of relational operators (reducing \texttt{z+x<x+y} to \texttt{z<y}, for instance. The simplifier also collects like terms, replacing \texttt{x+y+x*3} by \texttt{4*x+y}. Sometimes numerals are not wanted, because for example \texttt{n+3} does not match a pattern of the form \texttt{Suc $k$}. You can re-arrange the form of an arithmetic expression by proving (via \texttt{subgoal_tac}) a lemma such as \texttt{n+3 = Suc (Suc (Suc n))}. As an alternative, you can disable the fancier simplifications by using a basic simpset such as \texttt{HOL_ss} rather than the default one, \texttt{simpset()}. Reasoning about arithmetic inequalities can be tedious. Fortunately, HOL provides a decision procedure for \emph{linear arithmetic}: formulae involving addition and subtraction. The simplifier invokes a weak version of this decision procedure automatically. If this is not sufficent, you can invoke the full procedure \ttindex{arith_tac} explicitly. It copes with arbitrary formulae involving {\tt=}, {\tt<}, {\tt<=}, {\tt+}, {\tt-}, {\tt Suc}, {\tt min}, {\tt max} and numerical constants. Other subterms are treated as atomic, while subformulae not involving numerical types are ignored. Quantified subformulae are ignored unless they are positive universal or negative existential. The running time is exponential in the number of occurrences of {\tt min}, {\tt max}, and {\tt-} because they require case distinctions. If {\tt k} is a numeral, then {\tt div k}, {\tt mod k} and {\tt k dvd} are also supported. The former two are eliminated by case distinctions, again blowing up the running time. If the formula involves explicit quantifiers, \texttt{arith_tac} may take super-exponential time and space. If \texttt{arith_tac} fails, try to find relevant arithmetic results in the library. The theories \texttt{Nat} and \texttt{NatArith} contain theorems about {\tt<}, {\tt<=}, \texttt{+}, \texttt{-} and \texttt{*}. Theory \texttt{Divides} contains theorems about \texttt{div} and \texttt{mod}. Use Proof General's \emph{find} button (or other search facilities) to locate them. \index{nat@{\textit{nat}} type|)} \begin{figure} \index{#@{\tt[]} symbol} \index{#@{\tt\#} symbol} \index{"@@{\tt\at} symbol} \index{*"! symbol} \begin{constants} \it symbol & \it meta-type & \it priority & \it description \\ \tt[] & $\alpha\,list$ & & empty list\\ \tt \# & $[\alpha,\alpha\,list]\To \alpha\,list$ & Right 65 & list constructor \\ \cdx{null} & $\alpha\,list \To bool$ & & emptiness test\\ \cdx{hd} & $\alpha\,list \To \alpha$ & & head \\ \cdx{tl} & $\alpha\,list \To \alpha\,list$ & & tail \\ \cdx{last} & $\alpha\,list \To \alpha$ & & last element \\ \cdx{butlast} & $\alpha\,list \To \alpha\,list$ & & drop last element \\ \tt\at & $[\alpha\,list,\alpha\,list]\To \alpha\,list$ & Left 65 & append \\ \cdx{map} & $(\alpha\To\beta) \To (\alpha\,list \To \beta\,list)$ & & apply to all\\ \cdx{filter} & $(\alpha \To bool) \To (\alpha\,list \To \alpha\,list)$ & & filter functional\\ \cdx{set}& $\alpha\,list \To \alpha\,set$ & & elements\\ \sdx{mem} & $\alpha \To \alpha\,list \To bool$ & Left 55 & membership\\ \cdx{foldl} & $(\beta\To\alpha\To\beta) \To \beta \To \alpha\,list \To \beta$ & & iteration \\ \cdx{concat} & $(\alpha\,list)list\To \alpha\,list$ & & concatenation \\ \cdx{rev} & $\alpha\,list \To \alpha\,list$ & & reverse \\ \cdx{length} & $\alpha\,list \To nat$ & & length \\ \tt! & $\alpha\,list \To nat \To \alpha$ & Left 100 & indexing \\ \cdx{take}, \cdx{drop} & $nat \To \alpha\,list \To \alpha\,list$ && take/drop a prefix \\ \cdx{takeWhile},\\ \cdx{dropWhile} & $(\alpha \To bool) \To \alpha\,list \To \alpha\,list$ && take/drop a prefix \end{constants} \subcaption{Constants and infixes} \begin{center} \tt\frenchspacing \begin{tabular}{rrr} \it external & \it internal & \it description \\{} [$x@1$, $\dots$, $x@n$] & $x@1$ \# $\cdots$ \# $x@n$ \# [] & \rm finite list \\{} [$x$:$l$. $P$] & filter ($\lambda x{.}P$) $l$ & \rm list comprehension \end{tabular} \end{center} \subcaption{Translations} \caption{The theory \thydx{List}} \label{hol-list} \end{figure} \begin{figure} \begin{ttbox}\makeatother null [] = True null (x#xs) = False hd (x#xs) = x tl (x#xs) = xs tl [] = [] [] @ ys = ys (x#xs) @ ys = x # xs @ ys set [] = \ttlbrace\ttrbrace set (x#xs) = insert x (set xs) x mem [] = False x mem (y#ys) = (if y=x then True else x mem ys) concat([]) = [] concat(x#xs) = x @ concat(xs) rev([]) = [] rev(x#xs) = rev(xs) @ [x] length([]) = 0 length(x#xs) = Suc(length(xs)) xs!0 = hd xs xs!(Suc n) = (tl xs)!n \end{ttbox} \caption{Simple list processing functions} \label{fig:HOL:list-simps} \end{figure} \begin{figure} \begin{ttbox}\makeatother map f [] = [] map f (x#xs) = f x # map f xs filter P [] = [] filter P (x#xs) = (if P x then x#filter P xs else filter P xs) foldl f a [] = a foldl f a (x#xs) = foldl f (f a x) xs take n [] = [] take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs) drop n [] = [] drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs) takeWhile P [] = [] takeWhile P (x#xs) = (if P x then x#takeWhile P xs else []) dropWhile P [] = [] dropWhile P (x#xs) = (if P x then dropWhile P xs else xs) \end{ttbox} \caption{Further list processing functions} \label{fig:HOL:list-simps2} \end{figure} \subsection{The type constructor for lists, \textit{list}} \label{subsec:list} \index{list@{\textit{list}} type|(} Figure~\ref{hol-list} presents the theory \thydx{List}: the basic list operations with their types and syntax. Type $\alpha \; list$ is defined as a \texttt{datatype} with the constructors {\tt[]} and {\tt\#}. As a result the generic structural induction and case analysis tactics \texttt{induct\_tac} and \texttt{cases\_tac} also become available for lists. A \sdx{case} construct of the form \begin{center}\tt case $e$ of [] => $a$ | \(x\)\#\(xs\) => b \end{center} is defined by translation. For details see~{\S}\ref{sec:HOL:datatype}. There is also a case splitting rule \tdx{split_list_case} \[ \begin{array}{l} P(\mathtt{case}~e~\mathtt{of}~\texttt{[] =>}~a ~\texttt{|}~ x\texttt{\#}xs~\texttt{=>}~f~x~xs) ~= \\ ((e = \texttt{[]} \to P(a)) \land (\forall x~ xs. e = x\texttt{\#}xs \to P(f~x~xs))) \end{array} \] which can be fed to \ttindex{addsplits} just like \texttt{split_if} (see~{\S}\ref{subsec:HOL:case:splitting}). \texttt{List} provides a basic library of list processing functions defined by primitive recursion (see~{\S}\ref{sec:HOL:primrec}). The recursion equations are shown in Figs.\ts\ref{fig:HOL:list-simps} and~\ref{fig:HOL:list-simps2}. \index{list@{\textit{list}} type|)} \subsection{Introducing new types} \label{sec:typedef} The HOL-methodology dictates that all extensions to a theory should be \textbf{definitional}. The type definition mechanism that meets this criterion is \ttindex{typedef}. Note that \emph{type synonyms}, which are inherited from Pure and described elsewhere, are just syntactic abbreviations that have no logical meaning. \begin{warn} Types in HOL must be non-empty; otherwise the quantifier rules would be unsound, because $\exists x. x=x$ is a theorem \cite[{\S}7]{paulson-COLOG}. \end{warn} A \bfindex{type definition} identifies the new type with a subset of an existing type. More precisely, the new type is defined by exhibiting an existing type~$\tau$, a set~$A::\tau\,set$, and a theorem of the form $x:A$. Thus~$A$ is a non-empty subset of~$\tau$, and the new type denotes this subset. New functions are defined that establish an isomorphism between the new type and the subset. If type~$\tau$ involves type variables $\alpha@1$, \ldots, $\alpha@n$, then the type definition creates a type constructor $(\alpha@1,\ldots,\alpha@n)ty$ rather than a particular type. \begin{figure}[htbp] \begin{rail} typedef : 'typedef' ( () | '(' name ')') type '=' set witness; type : typevarlist name ( () | '(' infix ')' ); set : string; witness : () | '(' id ')'; \end{rail} \caption{Syntax of type definitions} \label{fig:HOL:typedef} \end{figure} The syntax for type definitions is shown in Fig.~\ref{fig:HOL:typedef}. For the definition of `typevarlist' and `infix' see \iflabelundefined{chap:classical} {the appendix of the {\em Reference Manual\/}}% {Appendix~\ref{app:TheorySyntax}}. The remaining nonterminals have the following meaning: \begin{description} \item[\it type:] the new type constructor $(\alpha@1,\dots,\alpha@n)ty$ with optional infix annotation. \item[\it name:] an alphanumeric name $T$ for the type constructor $ty$, in case $ty$ is a symbolic name. Defaults to $ty$. \item[\it set:] the representing subset $A$. \item[\it witness:] name of a theorem of the form $a:A$ proving non-emptiness. It can be omitted in case Isabelle manages to prove non-emptiness automatically. \end{description} If all context conditions are met (no duplicate type variables in `typevarlist', no extra type variables in `set', and no free term variables in `set'), the following components are added to the theory: \begin{itemize} \item a type $ty :: (term,\dots,term)term$ \item constants \begin{eqnarray*} T &::& \tau\;set \\ Rep_T &::& (\alpha@1,\dots,\alpha@n)ty \To \tau \\ Abs_T &::& \tau \To (\alpha@1,\dots,\alpha@n)ty \end{eqnarray*} \item a definition and three axioms \[ \begin{array}{ll} T{\tt_def} & T \equiv A \\ {\tt Rep_}T & Rep_T\,x \in T \\ {\tt Rep_}T{\tt_inverse} & Abs_T\,(Rep_T\,x) = x \\ {\tt Abs_}T{\tt_inverse} & y \in T \Imp Rep_T\,(Abs_T\,y) = y \end{array} \] stating that $(\alpha@1,\dots,\alpha@n)ty$ is isomorphic to $A$ by $Rep_T$ and its inverse $Abs_T$. \end{itemize} Below are two simple examples of HOL type definitions. Non-emptiness is proved automatically here. \begin{ttbox} typedef unit = "{\ttlbrace}True{\ttrbrace}" typedef (prod) ('a, 'b) "*" (infixr 20) = "{\ttlbrace}f . EX (a::'a) (b::'b). f = (\%x y. x = a & y = b){\ttrbrace}" \end{ttbox} Type definitions permit the introduction of abstract data types in a safe way, namely by providing models based on already existing types. Given some abstract axiomatic description $P$ of a type, this involves two steps: \begin{enumerate} \item Find an appropriate type $\tau$ and subset $A$ which has the desired properties $P$, and make a type definition based on this representation. \item Prove that $P$ holds for $ty$ by lifting $P$ from the representation. \end{enumerate} You can now forget about the representation and work solely in terms of the abstract properties $P$. \begin{warn} If you introduce a new type (constructor) $ty$ axiomatically, i.e.\ by declaring the type and its operations and by stating the desired axioms, you should make sure the type has a non-empty model. You must also have a clause \par \begin{ttbox} arities \(ty\) :: (term,\thinspace\(\dots\),{\thinspace}term){\thinspace}term \end{ttbox} in your theory file to tell Isabelle that $ty$ is in class \texttt{term}, the class of all HOL types. \end{warn} \section{Datatype definitions} \label{sec:HOL:datatype} \index{*datatype|(} Inductive datatypes, similar to those of \ML, frequently appear in applications of Isabelle/HOL. In principle, such types could be defined by hand via \texttt{typedef} (see {\S}\ref{sec:typedef}), but this would be far too tedious. The \ttindex{datatype} definition package of Isabelle/HOL (cf.\ \cite{Berghofer-Wenzel:1999:TPHOL}) automates such chores. It generates an appropriate \texttt{typedef} based on a least fixed-point construction, and proves freeness theorems and induction rules, as well as theorems for recursion and case combinators. The user just has to give a simple specification of new inductive types using a notation similar to {\ML} or Haskell. The current datatype package can handle both mutual and indirect recursion. It also offers to represent existing types as datatypes giving the advantage of a more uniform view on standard theories. \subsection{Basics} \label{subsec:datatype:basics} A general \texttt{datatype} definition is of the following form: \[ \begin{array}{llcl} \mathtt{datatype} & (\vec{\alpha})t@1 & = & C^1@1~\tau^1@{1,1}~\ldots~\tau^1@{1,m^1@1} ~\mid~ \ldots ~\mid~ C^1@{k@1}~\tau^1@{k@1,1}~\ldots~\tau^1@{k@1,m^1@{k@1}} \\ & & \vdots \\ \mathtt{and} & (\vec{\alpha})t@n & = & C^n@1~\tau^n@{1,1}~\ldots~\tau^n@{1,m^n@1} ~\mid~ \ldots ~\mid~ C^n@{k@n}~\tau^n@{k@n,1}~\ldots~\tau^n@{k@n,m^n@{k@n}} \end{array} \] where $\vec{\alpha} = (\alpha@1,\ldots,\alpha@h)$ is a list of type variables, $C^j@i$ are distinct constructor names and $\tau^j@{i,i'}$ are {\em admissible} types containing at most the type variables $\alpha@1, \ldots, \alpha@h$. A type $\tau$ occurring in a \texttt{datatype} definition is {\em admissible} if and only if \begin{itemize} \item $\tau$ is non-recursive, i.e.\ $\tau$ does not contain any of the newly defined type constructors $t@1,\ldots,t@n$, or \item $\tau = (\vec{\alpha})t@{j'}$ where $1 \leq j' \leq n$, or \item $\tau = (\tau'@1,\ldots,\tau'@{h'})t'$, where $t'$ is the type constructor of an already existing datatype and $\tau'@1,\ldots,\tau'@{h'}$ are admissible types. \item $\tau = \sigma \to \tau'$, where $\tau'$ is an admissible type and $\sigma$ is non-recursive (i.e. the occurrences of the newly defined types are {\em strictly positive}) \end{itemize} If some $(\vec{\alpha})t@{j'}$ occurs in a type $\tau^j@{i,i'}$ of the form \[ (\ldots,\ldots ~ (\vec{\alpha})t@{j'} ~ \ldots,\ldots)t' \] this is called a {\em nested} (or \emph{indirect}) occurrence. A very simple example of a datatype is the type \texttt{list}, which can be defined by \begin{ttbox} datatype 'a list = Nil | Cons 'a ('a list) \end{ttbox} Arithmetic expressions \texttt{aexp} and boolean expressions \texttt{bexp} can be modelled by the mutually recursive datatype definition \begin{ttbox} datatype 'a aexp = If_then_else ('a bexp) ('a aexp) ('a aexp) | Sum ('a aexp) ('a aexp) | Diff ('a aexp) ('a aexp) | Var 'a | Num nat and 'a bexp = Less ('a aexp) ('a aexp) | And ('a bexp) ('a bexp) | Or ('a bexp) ('a bexp) \end{ttbox} The datatype \texttt{term}, which is defined by \begin{ttbox} datatype ('a, 'b) term = Var 'a | App 'b ((('a, 'b) term) list) \end{ttbox} is an example for a datatype with nested recursion. Using nested recursion involving function spaces, we may also define infinitely branching datatypes, e.g. \begin{ttbox} datatype 'a tree = Atom 'a | Branch "nat => 'a tree" \end{ttbox} \medskip Types in HOL must be non-empty. Each of the new datatypes $(\vec{\alpha})t@j$ with $1 \leq j \leq n$ is non-empty if and only if it has a constructor $C^j@i$ with the following property: for all argument types $\tau^j@{i,i'}$ of the form $(\vec{\alpha})t@{j'}$ the datatype $(\vec{\alpha})t@{j'}$ is non-empty. If there are no nested occurrences of the newly defined datatypes, obviously at least one of the newly defined datatypes $(\vec{\alpha})t@j$ must have a constructor $C^j@i$ without recursive arguments, a \emph{base case}, to ensure that the new types are non-empty. If there are nested occurrences, a datatype can even be non-empty without having a base case itself. Since \texttt{list} is a non-empty datatype, \texttt{datatype t = C (t list)} is non-empty as well. \subsubsection{Freeness of the constructors} The datatype constructors are automatically defined as functions of their respective type: \[ C^j@i :: [\tau^j@{i,1},\dots,\tau^j@{i,m^j@i}] \To (\alpha@1,\dots,\alpha@h)t@j \] These functions have certain {\em freeness} properties. They construct distinct values: \[ C^j@i~x@1~\dots~x@{m^j@i} \neq C^j@{i'}~y@1~\dots~y@{m^j@{i'}} \qquad \mbox{for all}~ i \neq i'. \] The constructor functions are injective: \[ (C^j@i~x@1~\dots~x@{m^j@i} = C^j@i~y@1~\dots~y@{m^j@i}) = (x@1 = y@1 \land \dots \land x@{m^j@i} = y@{m^j@i}) \] Since the number of distinctness inequalities is quadratic in the number of constructors, the datatype package avoids proving them separately if there are too many constructors. Instead, specific inequalities are proved by a suitable simplification procedure on demand.\footnote{This procedure, which is already part of the default simpset, may be referred to by the ML identifier \texttt{DatatypePackage.distinct_simproc}.} \subsubsection{Structural induction} The datatype package also provides structural induction rules. For datatypes without nested recursion, this is of the following form: \[ \infer{P@1~x@1 \land \dots \land P@n~x@n} {\begin{array}{lcl} \Forall x@1 \dots x@{m^1@1}. \List{P@{s^1@{1,1}}~x@{r^1@{1,1}}; \dots; P@{s^1@{1,l^1@1}}~x@{r^1@{1,l^1@1}}} & \Imp & P@1~\left(C^1@1~x@1~\dots~x@{m^1@1}\right) \\ & \vdots \\ \Forall x@1 \dots x@{m^1@{k@1}}. \List{P@{s^1@{k@1,1}}~x@{r^1@{k@1,1}}; \dots; P@{s^1@{k@1,l^1@{k@1}}}~x@{r^1@{k@1,l^1@{k@1}}}} & \Imp & P@1~\left(C^1@{k@1}~x@1~\ldots~x@{m^1@{k@1}}\right) \\ & \vdots \\ \Forall x@1 \dots x@{m^n@1}. \List{P@{s^n@{1,1}}~x@{r^n@{1,1}}; \dots; P@{s^n@{1,l^n@1}}~x@{r^n@{1,l^n@1}}} & \Imp & P@n~\left(C^n@1~x@1~\ldots~x@{m^n@1}\right) \\ & \vdots \\ \Forall x@1 \dots x@{m^n@{k@n}}. \List{P@{s^n@{k@n,1}}~x@{r^n@{k@n,1}}; \dots P@{s^n@{k@n,l^n@{k@n}}}~x@{r^n@{k@n,l^n@{k@n}}}} & \Imp & P@n~\left(C^n@{k@n}~x@1~\ldots~x@{m^n@{k@n}}\right) \end{array}} \] where \[ \begin{array}{rcl} Rec^j@i & := & \left\{\left(r^j@{i,1},s^j@{i,1}\right),\ldots, \left(r^j@{i,l^j@i},s^j@{i,l^j@i}\right)\right\} = \\[2ex] && \left\{(i',i'')~\left|~ 1\leq i' \leq m^j@i \land 1 \leq i'' \leq n \land \tau^j@{i,i'} = (\alpha@1,\ldots,\alpha@h)t@{i''}\right.\right\} \end{array} \] i.e.\ the properties $P@j$ can be assumed for all recursive arguments. For datatypes with nested recursion, such as the \texttt{term} example from above, things are a bit more complicated. Conceptually, Isabelle/HOL unfolds a definition like \begin{ttbox} datatype ('a,'b) term = Var 'a | App 'b ((('a, 'b) term) list) \end{ttbox} to an equivalent definition without nesting: \begin{ttbox} datatype ('a,'b) term = Var | App 'b (('a, 'b) term_list) and ('a,'b) term_list = Nil' | Cons' (('a,'b) term) (('a,'b) term_list) \end{ttbox} Note however, that the type \texttt{('a,'b) term_list} and the constructors {\tt Nil'} and \texttt{Cons'} are not really introduced. One can directly work with the original (isomorphic) type \texttt{(('a, 'b) term) list} and its existing constructors \texttt{Nil} and \texttt{Cons}. Thus, the structural induction rule for \texttt{term} gets the form \[ \infer{P@1~x@1 \land P@2~x@2} {\begin{array}{l} \Forall x.~P@1~(\mathtt{Var}~x) \\ \Forall x@1~x@2.~P@2~x@2 \Imp P@1~(\mathtt{App}~x@1~x@2) \\ P@2~\mathtt{Nil} \\ \Forall x@1~x@2. \List{P@1~x@1; P@2~x@2} \Imp P@2~(\mathtt{Cons}~x@1~x@2) \end{array}} \] Note that there are two predicates $P@1$ and $P@2$, one for the type \texttt{('a,'b) term} and one for the type \texttt{(('a, 'b) term) list}. For a datatype with function types such as \texttt{'a tree}, the induction rule is of the form \[ \infer{P~t} {\Forall a.~P~(\mathtt{Atom}~a) & \Forall ts.~(\forall x.~P~(ts~x)) \Imp P~(\mathtt{Branch}~ts)} \] \medskip In principle, inductive types are already fully determined by freeness and structural induction. For convenience in applications, the following derived constructions are automatically provided for any datatype. \subsubsection{The \sdx{case} construct} The type comes with an \ML-like \texttt{case}-construct: \[ \begin{array}{rrcl} \mbox{\tt case}~e~\mbox{\tt of} & C^j@1~x@{1,1}~\dots~x@{1,m^j@1} & \To & e@1 \\ \vdots \\ \mid & C^j@{k@j}~x@{k@j,1}~\dots~x@{k@j,m^j@{k@j}} & \To & e@{k@j} \end{array} \] where the $x@{i,j}$ are either identifiers or nested tuple patterns as in {\S}\ref{subsec:prod-sum}. \begin{warn} All constructors must be present, their order is fixed, and nested patterns are not supported (with the exception of tuples). Violating this restriction results in strange error messages. \end{warn} To perform case distinction on a goal containing a \texttt{case}-construct, the theorem $t@j.$\texttt{split} is provided: \[ \begin{array}{@{}rcl@{}} P(t@j_\mathtt{case}~f@1~\dots~f@{k@j}~e) &\!\!\!=& \!\!\! ((\forall x@1 \dots x@{m^j@1}. e = C^j@1~x@1\dots x@{m^j@1} \to P(f@1~x@1\dots x@{m^j@1})) \\ &&\!\!\! ~\land~ \dots ~\land \\ &&~\!\!\! (\forall x@1 \dots x@{m^j@{k@j}}. e = C^j@{k@j}~x@1\dots x@{m^j@{k@j}} \to P(f@{k@j}~x@1\dots x@{m^j@{k@j}}))) \end{array} \] where $t@j$\texttt{_case} is the internal name of the \texttt{case}-construct. This theorem can be added to a simpset via \ttindex{addsplits} (see~{\S}\ref{subsec:HOL:case:splitting}). Case splitting on assumption works as well, by using the rule $t@j.$\texttt{split_asm} in the same manner. Both rules are available under $t@j.$\texttt{splits} (this name is \emph{not} bound in ML, though). \begin{warn}\index{simplification!of \texttt{case}}% By default only the selector expression ($e$ above) in a \texttt{case}-construct is simplified, in analogy with \texttt{if} (see page~\pageref{if-simp}). Only if that reduces to a constructor is one of the arms of the \texttt{case}-construct exposed and simplified. To ensure full simplification of all parts of a \texttt{case}-construct for datatype $t$, remove $t$\texttt{.}\ttindexbold{case_weak_cong} from the simpset, for example by \texttt{delcongs [thm "$t$.weak_case_cong"]}. \end{warn} \subsubsection{The function \cdx{size}}\label{sec:HOL:size} Theory \texttt{NatArith} declares a generic function \texttt{size} of type $\alpha\To nat$. Each datatype defines a particular instance of \texttt{size} by overloading according to the following scheme: %%% FIXME: This formula is too big and is completely unreadable \[ size(C^j@i~x@1~\dots~x@{m^j@i}) = \! \left\{ \begin{array}{ll} 0 & \!\mbox{if $Rec^j@i = \emptyset$} \\ 1+\sum\limits@{h=1}^{l^j@i}size~x@{r^j@{i,h}} & \!\mbox{if $Rec^j@i = \left\{\left(r^j@{i,1},s^j@{i,1}\right),\ldots, \left(r^j@{i,l^j@i},s^j@{i,l^j@i}\right)\right\}$} \end{array} \right. \] where $Rec^j@i$ is defined above. Viewing datatypes as generalised trees, the size of a leaf is 0 and the size of a node is the sum of the sizes of its subtrees ${}+1$. \subsection{Defining datatypes} The theory syntax for datatype definitions is shown in Fig.~\ref{datatype-grammar}. In order to be well-formed, a datatype definition has to obey the rules stated in the previous section. As a result the theory is extended with the new types, the constructors, and the theorems listed in the previous section. \begin{figure} \begin{rail} datatype : 'datatype' typedecls; typedecls: ( newtype '=' (cons + '|') ) + 'and' ; newtype : typevarlist id ( () | '(' infix ')' ) ; cons : name (argtype *) ( () | ( '(' mixfix ')' ) ) ; argtype : id | tid | ('(' typevarlist id ')') ; \end{rail} \caption{Syntax of datatype declarations} \label{datatype-grammar} \end{figure} Most of the theorems about datatypes become part of the default simpset and you never need to see them again because the simplifier applies them automatically. Only induction or case distinction are usually invoked by hand. \begin{ttdescription} \item[\ttindexbold{induct_tac} {\tt"}$x${\tt"} $i$] applies structural induction on variable $x$ to subgoal $i$, provided the type of $x$ is a datatype. \item[\texttt{induct_tac} {\tt"}$x@1$ $\ldots$ $x@n${\tt"} $i$] applies simultaneous structural induction on the variables $x@1,\ldots,x@n$ to subgoal $i$. This is the canonical way to prove properties of mutually recursive datatypes such as \texttt{aexp} and \texttt{bexp}, or datatypes with nested recursion such as \texttt{term}. \end{ttdescription} In some cases, induction is overkill and a case distinction over all constructors of the datatype suffices. \begin{ttdescription} \item[\ttindexbold{case_tac} {\tt"}$u${\tt"} $i$] performs a case analysis for the term $u$ whose type must be a datatype. If the datatype has $k@j$ constructors $C^j@1$, \dots $C^j@{k@j}$, subgoal $i$ is replaced by $k@j$ new subgoals which contain the additional assumption $u = C^j@{i'}~x@1~\dots~x@{m^j@{i'}}$ for $i'=1$, $\dots$,~$k@j$. \end{ttdescription} Note that induction is only allowed on free variables that should not occur among the premises of the subgoal. Case distinction applies to arbitrary terms. \bigskip For the technically minded, we exhibit some more details. Processing the theory file produces an \ML\ structure which, in addition to the usual components, contains a structure named $t$ for each datatype $t$ defined in the file. Each structure $t$ contains the following elements: \begin{ttbox} val distinct : thm list val inject : thm list val induct : thm val exhaust : thm val cases : thm list val split : thm val split_asm : thm val recs : thm list val size : thm list val simps : thm list \end{ttbox} \texttt{distinct}, \texttt{inject}, \texttt{induct}, \texttt{size} and \texttt{split} contain the theorems described above. For user convenience, \texttt{distinct} contains inequalities in both directions. The reduction rules of the {\tt case}-construct are in \texttt{cases}. All theorems from {\tt distinct}, \texttt{inject} and \texttt{cases} are combined in \texttt{simps}. In case of mutually recursive datatypes, \texttt{recs}, \texttt{size}, \texttt{induct} and \texttt{simps} are contained in a separate structure named $t@1_\ldots_t@n$. \subsection{Representing existing types as datatypes}\label{subsec:datatype:rep_datatype} For foundational reasons, some basic types such as \texttt{nat}, \texttt{*}, {\tt +}, \texttt{bool} and \texttt{unit} are not defined in a \texttt{datatype} section, but by more primitive means using \texttt{typedef}. To be able to use the tactics \texttt{induct_tac} and \texttt{case_tac} and to define functions by primitive recursion on these types, such types may be represented as actual datatypes. This is done by specifying the constructors of the desired type, plus a proof of the induction rule, as well as theorems stating the distinctness and injectivity of constructors in a {\tt rep_datatype} section. For the sum type this works as follows: \begin{ttbox} rep_datatype (sum) Inl Inr proof - fix P fix s :: "'a + 'b" assume x: "!!x::'a. P (Inl x)" and y: "!!y::'b. P (Inr y)" then show "P s" by (auto intro: sumE [of s]) qed simp_all \end{ttbox} The datatype package automatically derives additional theorems for recursion and case combinators from these rules. Any of the basic HOL types mentioned above are represented as datatypes. Try an induction on \texttt{bool} today. \subsection{Examples} \subsubsection{The datatype $\alpha~mylist$} We want to define a type $\alpha~mylist$. To do this we have to build a new theory that contains the type definition. We start from the theory \texttt{Datatype} instead of \texttt{Main} in order to avoid clashes with the \texttt{List} theory of Isabelle/HOL. \begin{ttbox} MyList = Datatype + datatype 'a mylist = Nil | Cons 'a ('a mylist) end \end{ttbox} After loading the theory, we can prove $Cons~x~xs\neq xs$, for example. To ease the induction applied below, we state the goal with $x$ quantified at the object-level. This will be stripped later using \ttindex{qed_spec_mp}. \begin{ttbox} Goal "!x. Cons x xs ~= xs"; {\out Level 0} {\out ! x. Cons x xs ~= xs} {\out 1. ! x. Cons x xs ~= xs} \end{ttbox} This can be proved by the structural induction tactic: \begin{ttbox} by (induct_tac "xs" 1); {\out Level 1} {\out ! x. Cons x xs ~= xs} {\out 1. ! x. Cons x Nil ~= Nil} {\out 2. !!a mylist.} {\out ! x. Cons x mylist ~= mylist ==>} {\out ! x. Cons x (Cons a mylist) ~= Cons a mylist} \end{ttbox} The first subgoal can be proved using the simplifier. Isabelle/HOL has already added the freeness properties of lists to the default simplification set. \begin{ttbox} by (Simp_tac 1); {\out Level 2} {\out ! x. Cons x xs ~= xs} {\out 1. !!a mylist.} {\out ! x. Cons x mylist ~= mylist ==>} {\out ! x. Cons x (Cons a mylist) ~= Cons a mylist} \end{ttbox} Similarly, we prove the remaining goal. \begin{ttbox} by (Asm_simp_tac 1); {\out Level 3} {\out ! x. Cons x xs ~= xs} {\out No subgoals!} \ttbreak qed_spec_mp "not_Cons_self"; {\out val not_Cons_self = "Cons x xs ~= xs" : thm} \end{ttbox} Because both subgoals could have been proved by \texttt{Asm_simp_tac} we could have done that in one step: \begin{ttbox} by (ALLGOALS Asm_simp_tac); \end{ttbox} \subsubsection{The datatype $\alpha~mylist$ with mixfix syntax} In this example we define the type $\alpha~mylist$ again but this time we want to write \texttt{[]} for \texttt{Nil} and we want to use infix notation \verb|#| for \texttt{Cons}. To do this we simply add mixfix annotations after the constructor declarations as follows: \begin{ttbox} MyList = Datatype + datatype 'a mylist = Nil ("[]") | Cons 'a ('a mylist) (infixr "#" 70) end \end{ttbox} Now the theorem in the previous example can be written \verb|x#xs ~= xs|. \subsubsection{A datatype for weekdays} This example shows a datatype that consists of 7 constructors: \begin{ttbox} Days = Main + datatype days = Mon | Tue | Wed | Thu | Fri | Sat | Sun end \end{ttbox} Because there are more than 6 constructors, inequality is expressed via a function \verb|days_ord|. The theorem \verb|Mon ~= Tue| is not directly contained among the distinctness theorems, but the simplifier can prove it thanks to rewrite rules inherited from theory \texttt{NatArith}: \begin{ttbox} Goal "Mon ~= Tue"; by (Simp_tac 1); \end{ttbox} You need not derive such inequalities explicitly: the simplifier will dispose of them automatically. \index{*datatype|)} \section{Recursive function definitions}\label{sec:HOL:recursive} \index{recursive functions|see{recursion}} Isabelle/HOL provides two main mechanisms of defining recursive functions. \begin{enumerate} \item \textbf{Primitive recursion} is available only for datatypes, and it is somewhat restrictive. Recursive calls are only allowed on the argument's immediate constituents. On the other hand, it is the form of recursion most often wanted, and it is easy to use. \item \textbf{Well-founded recursion} requires that you supply a well-founded relation that governs the recursion. Recursive calls are only allowed if they make the argument decrease under the relation. Complicated recursion forms, such as nested recursion, can be dealt with. Termination can even be proved at a later time, though having unsolved termination conditions around can make work difficult.% \footnote{This facility is based on Konrad Slind's TFL package~\cite{slind-tfl}. Thanks are due to Konrad for implementing TFL and assisting with its installation.} \end{enumerate} Following good HOL tradition, these declarations do not assert arbitrary axioms. Instead, they define the function using a recursion operator. Both HOL and ZF derive the theory of well-founded recursion from first principles~\cite{paulson-set-II}. Primitive recursion over some datatype relies on the recursion operator provided by the datatype package. With either form of function definition, Isabelle proves the desired recursion equations as theorems. \subsection{Primitive recursive functions} \label{sec:HOL:primrec} \index{recursion!primitive|(} \index{*primrec|(} Datatypes come with a uniform way of defining functions, {\bf primitive recursion}. In principle, one could introduce primitive recursive functions by asserting their reduction rules as new axioms, but this is not recommended: \begin{ttbox}\slshape Append = Main + consts app :: ['a list, 'a list] => 'a list rules app_Nil "app [] ys = ys" app_Cons "app (x#xs) ys = x#app xs ys" end \end{ttbox} Asserting axioms brings the danger of accidentally asserting nonsense, as in \verb$app [] ys = us$. The \ttindex{primrec} declaration is a safe means of defining primitive recursive functions on datatypes: \begin{ttbox} Append = Main + consts app :: ['a list, 'a list] => 'a list primrec "app [] ys = ys" "app (x#xs) ys = x#app xs ys" end \end{ttbox} Isabelle will now check that the two rules do indeed form a primitive recursive definition. For example \begin{ttbox} primrec "app [] ys = us" \end{ttbox} is rejected with an error message ``\texttt{Extra variables on rhs}''. \bigskip The general form of a primitive recursive definition is \begin{ttbox} primrec {\it reduction rules} \end{ttbox} where \textit{reduction rules} specify one or more equations of the form \[ f \, x@1 \, \dots \, x@m \, (C \, y@1 \, \dots \, y@k) \, z@1 \, \dots \, z@n = r \] such that $C$ is a constructor of the datatype, $r$ contains only the free variables on the left-hand side, and all recursive calls in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$. There must be at most one reduction rule for each constructor. The order is immaterial. For missing constructors, the function is defined to return a default value. If you would like to refer to some rule by name, then you must prefix the rule with an identifier. These identifiers, like those in the \texttt{rules} section of a theory, will be visible at the \ML\ level. The primitive recursive function can have infix or mixfix syntax: \begin{ttbox}\underscoreon consts "@" :: ['a list, 'a list] => 'a list (infixr 60) primrec "[] @ ys = ys" "(x#xs) @ ys = x#(xs @ ys)" \end{ttbox} The reduction rules become part of the default simpset, which leads to short proof scripts: \begin{ttbox}\underscoreon Goal "(xs @ ys) @ zs = xs @ (ys @ zs)"; by (induct\_tac "xs" 1); by (ALLGOALS Asm\_simp\_tac); \end{ttbox} \subsubsection{Example: Evaluation of expressions} Using mutual primitive recursion, we can define evaluation functions \texttt{evala} and \texttt{eval_bexp} for the datatypes of arithmetic and boolean expressions mentioned in {\S}\ref{subsec:datatype:basics}: \begin{ttbox} consts evala :: "['a => nat, 'a aexp] => nat" evalb :: "['a => nat, 'a bexp] => bool" primrec "evala env (If_then_else b a1 a2) = (if evalb env b then evala env a1 else evala env a2)" "evala env (Sum a1 a2) = evala env a1 + evala env a2" "evala env (Diff a1 a2) = evala env a1 - evala env a2" "evala env (Var v) = env v" "evala env (Num n) = n" "evalb env (Less a1 a2) = (evala env a1 < evala env a2)" "evalb env (And b1 b2) = (evalb env b1 & evalb env b2)" "evalb env (Or b1 b2) = (evalb env b1 & evalb env b2)" \end{ttbox} Since the value of an expression depends on the value of its variables, the functions \texttt{evala} and \texttt{evalb} take an additional parameter, an {\em environment} of type \texttt{'a => nat}, which maps variables to their values. Similarly, we may define substitution functions \texttt{substa} and \texttt{substb} for expressions: The mapping \texttt{f} of type \texttt{'a => 'a aexp} given as a parameter is lifted canonically on the types \texttt{'a aexp} and \texttt{'a bexp}: \begin{ttbox} consts substa :: "['a => 'b aexp, 'a aexp] => 'b aexp" substb :: "['a => 'b aexp, 'a bexp] => 'b bexp" primrec "substa f (If_then_else b a1 a2) = If_then_else (substb f b) (substa f a1) (substa f a2)" "substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)" "substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)" "substa f (Var v) = f v" "substa f (Num n) = Num n" "substb f (Less a1 a2) = Less (substa f a1) (substa f a2)" "substb f (And b1 b2) = And (substb f b1) (substb f b2)" "substb f (Or b1 b2) = Or (substb f b1) (substb f b2)" \end{ttbox} In textbooks about semantics one often finds {\em substitution theorems}, which express the relationship between substitution and evaluation. For \texttt{'a aexp} and \texttt{'a bexp}, we can prove such a theorem by mutual induction, followed by simplification: \begin{ttbox} Goal "evala env (substa (Var(v := a')) a) = evala (env(v := evala env a')) a & evalb env (substb (Var(v := a')) b) = evalb (env(v := evala env a')) b"; by (induct_tac "a b" 1); by (ALLGOALS Asm_full_simp_tac); \end{ttbox} \subsubsection{Example: A substitution function for terms} Functions on datatypes with nested recursion, such as the type \texttt{term} mentioned in {\S}\ref{subsec:datatype:basics}, are also defined by mutual primitive recursion. A substitution function \texttt{subst_term} on type \texttt{term}, similar to the functions \texttt{substa} and \texttt{substb} described above, can be defined as follows: \begin{ttbox} consts subst_term :: "['a => ('a,'b) term, ('a,'b) term] => ('a,'b) term" subst_term_list :: "['a => ('a,'b) term, ('a,'b) term list] => ('a,'b) term list" primrec "subst_term f (Var a) = f a" "subst_term f (App b ts) = App b (subst_term_list f ts)" "subst_term_list f [] = []" "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts" \end{ttbox} The recursion scheme follows the structure of the unfolded definition of type \texttt{term} shown in {\S}\ref{subsec:datatype:basics}. To prove properties of this substitution function, mutual induction is needed: \begin{ttbox} Goal "(subst_term ((subst_term f1) o f2) t) = (subst_term f1 (subst_term f2 t)) & (subst_term_list ((subst_term f1) o f2) ts) = (subst_term_list f1 (subst_term_list f2 ts))"; by (induct_tac "t ts" 1); by (ALLGOALS Asm_full_simp_tac); \end{ttbox} \subsubsection{Example: A map function for infinitely branching trees} Defining functions on infinitely branching datatypes by primitive recursion is just as easy. For example, we can define a function \texttt{map_tree} on \texttt{'a tree} as follows: \begin{ttbox} consts map_tree :: "('a => 'b) => 'a tree => 'b tree" primrec "map_tree f (Atom a) = Atom (f a)" "map_tree f (Branch ts) = Branch (\%x. map_tree f (ts x))" \end{ttbox} Note that all occurrences of functions such as \texttt{ts} in the \texttt{primrec} clauses must be applied to an argument. In particular, \texttt{map_tree f o ts} is not allowed. \index{recursion!primitive|)} \index{*primrec|)} \subsection{General recursive functions} \label{sec:HOL:recdef} \index{recursion!general|(} \index{*recdef|(} Using \texttt{recdef}, you can declare functions involving nested recursion and pattern-matching. Recursion need not involve datatypes and there are few syntactic restrictions. Termination is proved by showing that each recursive call makes the argument smaller in a suitable sense, which you specify by supplying a well-founded relation. Here is a simple example, the Fibonacci function. The first line declares \texttt{fib} to be a constant. The well-founded relation is simply~$<$ (on the natural numbers). Pattern-matching is used here: \texttt{1} is a macro for \texttt{Suc~0}. \begin{ttbox} consts fib :: "nat => nat" recdef fib "less_than" "fib 0 = 0" "fib 1 = 1" "fib (Suc(Suc x)) = (fib x + fib (Suc x))" \end{ttbox} With \texttt{recdef}, function definitions may be incomplete, and patterns may overlap, as in functional programming. The \texttt{recdef} package disambiguates overlapping patterns by taking the order of rules into account. For missing patterns, the function is defined to return a default value. %For example, here is a declaration of the list function \cdx{hd}: %\begin{ttbox} %consts hd :: 'a list => 'a %recdef hd "\{\}" % "hd (x#l) = x" %\end{ttbox} %Because this function is not recursive, we may supply the empty well-founded %relation, $\{\}$. The well-founded relation defines a notion of ``smaller'' for the function's argument type. The relation $\prec$ is \textbf{well-founded} provided it admits no infinitely decreasing chains \[ \cdots\prec x@n\prec\cdots\prec x@1. \] If the function's argument has type~$\tau$, then $\prec$ has to be a relation over~$\tau$: it must have type $(\tau\times\tau)set$. Proving well-foundedness can be tricky, so Isabelle/HOL provides a collection of operators for building well-founded relations. The package recognises these operators and automatically proves that the constructed relation is well-founded. Here are those operators, in order of importance: \begin{itemize} \item \texttt{less_than} is ``less than'' on the natural numbers. (It has type $(nat\times nat)set$, while $<$ has type $[nat,nat]\To bool$. \item $\mathop{\mathtt{measure}} f$, where $f$ has type $\tau\To nat$, is the relation~$\prec$ on type~$\tau$ such that $x\prec y$ if and only if $f(x)<f(y)$. Typically, $f$ takes the recursive function's arguments (as a tuple) and returns a result expressed in terms of the function \texttt{size}. It is called a \textbf{measure function}. Recall that \texttt{size} is overloaded and is defined on all datatypes (see {\S}\ref{sec:HOL:size}). \item $\mathop{\mathtt{inv_image}} R\;f$ is a generalisation of \texttt{measure}. It specifies a relation such that $x\prec y$ if and only if $f(x)$ is less than $f(y)$ according to~$R$, which must itself be a well-founded relation. \item $R@1\texttt{<*lex*>}R@2$ is the lexicographic product of two relations. It is a relation on pairs and satisfies $(x@1,x@2)\prec(y@1,y@2)$ if and only if $x@1$ is less than $y@1$ according to~$R@1$ or $x@1=y@1$ and $x@2$ is less than $y@2$ according to~$R@2$. \item \texttt{finite_psubset} is the proper subset relation on finite sets. \end{itemize} We can use \texttt{measure} to declare Euclid's algorithm for the greatest common divisor. The measure function, $\lambda(m,n). n$, specifies that the recursion terminates because argument~$n$ decreases. \begin{ttbox} recdef gcd "measure ((\%(m,n). n) ::nat*nat=>nat)" "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))" \end{ttbox} The general form of a well-founded recursive definition is \begin{ttbox} recdef {\it function} {\it rel} congs {\it congruence rules} {\bf(optional)} simpset {\it simplification set} {\bf(optional)} {\it reduction rules} \end{ttbox} where \begin{itemize} \item \textit{function} is the name of the function, either as an \textit{id} or a \textit{string}. \item \textit{rel} is a HOL expression for the well-founded termination relation. \item \textit{congruence rules} are required only in highly exceptional circumstances. \item The \textit{simplification set} is used to prove that the supplied relation is well-founded. It is also used to prove the \textbf{termination conditions}: assertions that arguments of recursive calls decrease under \textit{rel}. By default, simplification uses \texttt{simpset()}, which is sufficient to prove well-foundedness for the built-in relations listed above. \item \textit{reduction rules} specify one or more recursion equations. Each left-hand side must have the form $f\,t$, where $f$ is the function and $t$ is a tuple of distinct variables. If more than one equation is present then $f$ is defined by pattern-matching on components of its argument whose type is a \texttt{datatype}. The \ML\ identifier $f$\texttt{.simps} contains the reduction rules as a list of theorems. \end{itemize} With the definition of \texttt{gcd} shown above, Isabelle/HOL is unable to prove one termination condition. It remains as a precondition of the recursion theorems: \begin{ttbox} gcd.simps; {\out ["! m n. n ~= 0 --> m mod n < n} {\out ==> gcd (?m,?n) = (if ?n=0 then ?m else gcd (?n, ?m mod ?n))"] } {\out : thm list} \end{ttbox} The theory \texttt{HOL/ex/Primes} illustrates how to prove termination conditions afterwards. The function \texttt{Tfl.tgoalw} is like the standard function \texttt{goalw}, which sets up a goal to prove, but its argument should be the identifier $f$\texttt{.simps} and its effect is to set up a proof of the termination conditions: \begin{ttbox} Tfl.tgoalw thy [] gcd.simps; {\out Level 0} {\out ! m n. n ~= 0 --> m mod n < n} {\out 1. ! m n. n ~= 0 --> m mod n < n} \end{ttbox} This subgoal has a one-step proof using \texttt{simp_tac}. Once the theorem is proved, it can be used to eliminate the termination conditions from elements of \texttt{gcd.simps}. Theory \texttt{HOL/Subst/Unify} is a much more complicated example of this process, where the termination conditions can only be proved by complicated reasoning involving the recursive function itself. Isabelle/HOL can prove the \texttt{gcd} function's termination condition automatically if supplied with the right simpset. \begin{ttbox} recdef gcd "measure ((\%(m,n). n) ::nat*nat=>nat)" simpset "simpset() addsimps [mod_less_divisor, zero_less_eq]" "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))" \end{ttbox} If all termination conditions were proved automatically, $f$\texttt{.simps} is added to the simpset automatically, just as in \texttt{primrec}. The simplification rules corresponding to clause $i$ (where counting starts at 0) are called $f$\texttt{.}$i$ and can be accessed as \texttt{thms "$f$.$i$"}, which returns a list of theorems. Thus you can, for example, remove specific clauses from the simpset. Note that a single clause may give rise to a set of simplification rules in order to capture the fact that if clauses overlap, their order disambiguates them. A \texttt{recdef} definition also returns an induction rule specialised for the recursive function. For the \texttt{gcd} function above, the induction rule is \begin{ttbox} gcd.induct; {\out "(!!m n. n ~= 0 --> ?P n (m mod n) ==> ?P m n) ==> ?P ?u ?v" : thm} \end{ttbox} This rule should be used to reason inductively about the \texttt{gcd} function. It usually makes the induction hypothesis available at all recursive calls, leading to very direct proofs. If any termination conditions remain unproved, they will become additional premises of this rule. \index{recursion!general|)} \index{*recdef|)} \section{Inductive and coinductive definitions} \index{*inductive|(} \index{*coinductive|(} An {\bf inductive definition} specifies the least set~$R$ closed under given rules. (Applying a rule to elements of~$R$ yields a result within~$R$.) For example, a structural operational semantics is an inductive definition of an evaluation relation. Dually, a {\bf coinductive definition} specifies the greatest set~$R$ consistent with given rules. (Every element of~$R$ can be seen as arising by applying a rule to elements of~$R$.) An important example is using bisimulation relations to formalise equivalence of processes and infinite data structures. A theory file may contain any number of inductive and coinductive definitions. They may be intermixed with other declarations; in particular, the (co)inductive sets {\bf must} be declared separately as constants, and may have mixfix syntax or be subject to syntax translations. Each (co)inductive definition adds definitions to the theory and also proves some theorems. Each definition creates an \ML\ structure, which is a substructure of the main theory structure. This package is related to the ZF one, described in a separate paper,% \footnote{It appeared in CADE~\cite{paulson-CADE}; a longer version is distributed with Isabelle.} % which you should refer to in case of difficulties. The package is simpler than ZF's thanks to HOL's extra-logical automatic type-checking. The types of the (co)inductive sets determine the domain of the fixedpoint definition, and the package does not have to use inference rules for type-checking. \subsection{The result structure} Many of the result structure's components have been discussed in the paper; others are self-explanatory. \begin{description} \item[\tt defs] is the list of definitions of the recursive sets. \item[\tt mono] is a monotonicity theorem for the fixedpoint operator. \item[\tt unfold] is a fixedpoint equation for the recursive set (the union of the recursive sets, in the case of mutual recursion). \item[\tt intrs] is the list of introduction rules, now proved as theorems, for the recursive sets. The rules are also available individually, using the names given them in the theory file. \item[\tt elims] is the list of elimination rule. This is for compatibility with ML scripts; within the theory the name is \texttt{cases}. \item[\tt elim] is the head of the list \texttt{elims}. This is for compatibility only. \item[\tt mk_cases] is a function to create simplified instances of {\tt elim} using freeness reasoning on underlying datatypes. \end{description} For an inductive definition, the result structure contains the rule \texttt{induct}. For a coinductive definition, it contains the rule \verb|coinduct|. Figure~\ref{def-result-fig} summarises the two result signatures, specifying the types of all these components. \begin{figure} \begin{ttbox} sig val defs : thm list val mono : thm val unfold : thm val intrs : thm list val elims : thm list val elim : thm val mk_cases : string -> thm {\it(Inductive definitions only)} val induct : thm {\it(coinductive definitions only)} val coinduct : thm end \end{ttbox} \hrule \caption{The {\ML} result of a (co)inductive definition} \label{def-result-fig} \end{figure} \subsection{The syntax of a (co)inductive definition} An inductive definition has the form \begin{ttbox} inductive {\it inductive sets} intrs {\it introduction rules} monos {\it monotonicity theorems} \end{ttbox} A coinductive definition is identical, except that it starts with the keyword \texttt{coinductive}. The \texttt{monos} section is optional; if present it is specified by a list of identifiers. \begin{itemize} \item The \textit{inductive sets} are specified by one or more strings. \item The \textit{introduction rules} specify one or more introduction rules in the form \textit{ident\/}~\textit{string}, where the identifier gives the name of the rule in the result structure. \item The \textit{monotonicity theorems} are required for each operator applied to a recursive set in the introduction rules. There {\bf must} be a theorem of the form $A\subseteq B\Imp M(A)\subseteq M(B)$, for each premise $t\in M(R@i)$ in an introduction rule! \item The \textit{constructor definitions} contain definitions of constants appearing in the introduction rules. In most cases it can be omitted. \end{itemize} \subsection{*Monotonicity theorems} Each theory contains a default set of theorems that are used in monotonicity proofs. New rules can be added to this set via the \texttt{mono} attribute. Theory \texttt{Inductive} shows how this is done. In general, the following monotonicity theorems may be added: \begin{itemize} \item Theorems of the form $A\subseteq B\Imp M(A)\subseteq M(B)$, for proving monotonicity of inductive definitions whose introduction rules have premises involving terms such as $t\in M(R@i)$. \item Monotonicity theorems for logical operators, which are of the general form $\List{\cdots \to \cdots;~\ldots;~\cdots \to \cdots} \Imp \cdots \to \cdots$. For example, in the case of the operator $\lor$, the corresponding theorem is \[ \infer{P@1 \lor P@2 \to Q@1 \lor Q@2} {P@1 \to Q@1 & P@2 \to Q@2} \] \item De Morgan style equations for reasoning about the ``polarity'' of expressions, e.g. \[ (\lnot \lnot P) ~=~ P \qquad\qquad (\lnot (P \land Q)) ~=~ (\lnot P \lor \lnot Q) \] \item Equations for reducing complex operators to more primitive ones whose monotonicity can easily be proved, e.g. \[ (P \to Q) ~=~ (\lnot P \lor Q) \qquad\qquad \mathtt{Ball}~A~P ~\equiv~ \forall x.~x \in A \to P~x \] \end{itemize} \subsection{Example of an inductive definition} Two declarations, included in a theory file, define the finite powerset operator. First we declare the constant~\texttt{Fin}. Then we declare it inductively, with two introduction rules: \begin{ttbox} consts Fin :: 'a set => 'a set set inductive "Fin A" intrs emptyI "{\ttlbrace}{\ttrbrace} : Fin A" insertI "[| a: A; b: Fin A |] ==> insert a b : Fin A" \end{ttbox} The resulting theory structure contains a substructure, called~\texttt{Fin}. It contains the \texttt{Fin}$~A$ introduction rules as the list \texttt{Fin.intrs}, and also individually as \texttt{Fin.emptyI} and \texttt{Fin.consI}. The induction rule is \texttt{Fin.induct}. For another example, here is a theory file defining the accessible part of a relation. The paper \cite{paulson-CADE} discusses a ZF version of this example in more detail. \begin{ttbox} Acc = WF + Inductive + consts acc :: "('a * 'a)set => 'a set" (* accessible part *) inductive "acc r" intrs accI "ALL y. (y, x) : r --> y : acc r ==> x : acc r" end \end{ttbox} The Isabelle distribution contains many other inductive definitions. Simple examples are collected on subdirectory \texttt{HOL/Induct}. The theory \texttt{HOL/Induct/LList} contains coinductive definitions. Larger examples may be found on other subdirectories of \texttt{HOL}, such as \texttt{IMP}, \texttt{Lambda} and \texttt{Auth}. \index{*coinductive|)} \index{*inductive|)} \section{Executable specifications} \index{code generator} For validation purposes, it is often useful to {\em execute} specifications. In principle, specifications could be ``executed'' using Isabelle's inference kernel, i.e. by a combination of resolution and simplification. Unfortunately, this approach is rather inefficient. A more efficient way of executing specifications is to translate them into a functional programming language such as ML. Isabelle's built-in code generator supports this. \railalias{verblbrace}{\texttt{\ttlbrace*}} \railalias{verbrbrace}{\texttt{*\ttrbrace}} \railterm{verblbrace} \railterm{verbrbrace} \begin{figure} \begin{rail} codegen : ( 'code_module' | 'code_library' ) modespec ? name ? \\ ( 'file' name ) ? ( 'imports' ( name + ) ) ? \\ 'contains' ( ( name '=' term ) + | term + ); modespec : '(' ( name * ) ')'; \end{rail} \caption{Code generator invocation syntax} \label{fig:HOL:codegen-invocation} \end{figure} \begin{figure} \begin{rail} constscode : 'consts_code' (codespec +); codespec : const template attachment ?; typescode : 'types_code' (tycodespec +); tycodespec : name template attachment ?; const : term; template: '(' string ')'; attachment: 'attach' modespec ? verblbrace text verbrbrace; \end{rail} \caption{Code generator configuration syntax} \label{fig:HOL:codegen-configuration} \end{figure} \subsection{Invoking the code generator} The code generator is invoked via the \ttindex{code_module} and \ttindex{code_library} commands (see Fig.~\ref{fig:HOL:codegen-invocation}), which correspond to {\em incremental} and {\em modular} code generation, respectively. \begin{description} \item[Modular] For each theory, an ML structure is generated, containing the code generated from the constants defined in this theory. \item[Incremental] All the generated code is emitted into the same structure. This structure may import code from previously generated structures, which can be specified via \texttt{imports}. Moreover, the generated structure may also be referred to in later invocations of the code generator. \end{description} After the \texttt{code_module} and \texttt{code_library} keywords, the user may specify an optional list of ``modes'' in parentheses. These can be used to instruct the code generator to emit additional code for special purposes, e.g.\ functions for converting elements of generated datatypes to Isabelle terms, or test data generators. The list of modes is followed by a module name. The module name is optional for modular code generation, but must be specified for incremental code generation. The code can either be written to a file, in which case a file name has to be specified after the \texttt{file} keyword, or be loaded directly into Isabelle's ML environment. In the latter case, the \texttt{ML} theory command can be used to inspect the results interactively. The terms from which to generate code can be specified after the \texttt{contains} keyword, either as a list of bindings, or just as a list of terms. In the latter case, the code generator just produces code for all constants and types occuring in the term, but does not bind the compiled terms to ML identifiers. For example, \begin{ttbox} code_module Test contains test = "foldl op + (0::int) [1,2,3,4,5]" \end{ttbox} binds the result of compiling the term \texttt{foldl op + (0::int) [1,2,3,4,5]} (i.e.~\texttt{15}) to the ML identifier \texttt{Test.test}. \subsection{Configuring the code generator} When generating code for a complex term, the code generator recursively calls itself for all subterms. When it arrives at a constant, the default strategy of the code generator is to look up its definition and try to generate code for it. Constants which have no definitions that are immediately executable, may be associated with a piece of ML code manually using the \ttindex{consts_code} command (see Fig.~\ref{fig:HOL:codegen-configuration}). It takes a list whose elements consist of a constant (given in usual term syntax -- an explicit type constraint accounts for overloading), and a mixfix template describing the ML code. The latter is very much the same as the mixfix templates used when declaring new constants. The most notable difference is that terms may be included in the ML template using antiquotation brackets \verb|{*|~$\ldots$~\verb|*}|. A similar mechanism is available for types: \ttindex{types_code} associates type constructors with specific ML code. For example, the declaration \begin{ttbox} types_code "*" ("(_ */ _)") consts_code "Pair" ("(_,/ _)") \end{ttbox} in theory \texttt{Product_Type} describes how the product type of Isabelle/HOL should be compiled to ML. Sometimes, the code associated with a constant or type may need to refer to auxiliary functions, which have to be emitted when the constant is used. Code for such auxiliary functions can be declared using \texttt{attach}. For example, the \texttt{wfrec} function from theory \texttt{Wellfounded_Recursion} is implemented as follows: \begin{ttbox} consts_code "wfrec" ("\bs<module>wfrec?") attach \{* fun wfrec f x = f (wfrec f) x; *\} \end{ttbox} If the code containing a call to \texttt{wfrec} resides in an ML structure different from the one containing the function definition attached to \texttt{wfrec}, the name of the ML structure (followed by a ``\texttt{.}'') is inserted in place of ``\texttt{\bs<module>}'' in the above template. The ``\texttt{?}'' means that the code generator should ignore the first argument of \texttt{wfrec}, i.e.\ the termination relation, which is usually not executable. Another possibility of configuring the code generator is to register theorems to be used for code generation. Theorems can be registered via the \ttindex{code} attribute. It takes an optional name as an argument, which indicates the format of the theorem. Currently supported formats are equations (this is the default when no name is specified) and horn clauses (this is indicated by the name \texttt{ind}). The left-hand sides of equations may only contain constructors and distinct variables, whereas horn clauses must have the same format as introduction rules of inductive definitions. For example, the declaration \begin{ttbox} lemma Suc_less_eq [iff, code]: "(Suc m < Suc n) = (m < n)" \(\langle\ldots\rangle\) lemma [code]: "((n::nat) < 0) = False" by simp lemma [code]: "(0 < Suc n) = True" by simp \end{ttbox} in theory \texttt{Nat} specifies three equations from which to generate code for \texttt{<} on natural numbers. \subsection{Specific HOL code generators} The basic code generator framework offered by Isabelle/Pure has already been extended with additional code generators for specific HOL constructs. These include datatypes, recursive functions and inductive relations. The code generator for inductive relations can handle expressions of the form $(t@1,\ldots,t@n) \in r$, where $r$ is an inductively defined relation. If at least one of the $t@i$ is a dummy pattern ``$_$'', the above expression evaluates to a sequence of possible answers. If all of the $t@i$ are proper terms, the expression evaluates to a boolean value. \begin{small} \begin{alltt} theory Test = Lambda: code_module Test contains test1 = "Abs (Var 0) \(\circ\) Var 0 -> Var 0" test2 = "Abs (Abs (Var 0 \(\circ\) Var 0) \(\circ\) (Abs (Var 0) \(\circ\) Var 0)) -> _" \end{alltt} \end{small} In the above example, \texttt{Test.test1} evaluates to the boolean value \texttt{true}, whereas \texttt{Test.test2} is a sequence whose elements can be inspected using \texttt{Seq.pull} or similar functions. \begin{ttbox} ML \{* Seq.pull Test.test2 *\} -- \{* This is the first answer *\} ML \{* Seq.pull (snd (the it)) *\} -- \{* This is the second answer *\} \end{ttbox} The theory underlying the HOL code generator is described more detailed in \cite{Berghofer-Nipkow:2002}. More examples that illustrate the usage of the code generator can be found e.g.~in theories \texttt{MicroJava/J/JListExample} and \texttt{MicroJava/JVM/JVMListExample}. \section{The examples directories} Directory \texttt{HOL/Auth} contains theories for proving the correctness of cryptographic protocols~\cite{paulson-jcs}. The approach is based upon operational semantics rather than the more usual belief logics. On the same directory are proofs for some standard examples, such as the Needham-Schroeder public-key authentication protocol and the Otway-Rees protocol. Directory \texttt{HOL/IMP} contains a formalization of various denotational, operational and axiomatic semantics of a simple while-language, the necessary equivalence proofs, soundness and completeness of the Hoare rules with respect to the denotational semantics, and soundness and completeness of a verification condition generator. Much of development is taken from Winskel~\cite{winskel93}. For details see~\cite{nipkow-IMP}. Directory \texttt{HOL/Hoare} contains a user friendly surface syntax for Hoare logic, including a tactic for generating verification-conditions. Directory \texttt{HOL/MiniML} contains a formalization of the type system of the core functional language Mini-ML and a correctness proof for its type inference algorithm $\cal W$~\cite{milner78,nipkow-W}. Directory \texttt{HOL/Lambda} contains a formalization of untyped $\lambda$-calculus in de~Bruijn notation and Church-Rosser proofs for $\beta$ and $\eta$ reduction~\cite{Nipkow-CR}. Directory \texttt{HOL/Subst} contains Martin Coen's mechanization of a theory of substitutions and unifiers. It is based on Paulson's previous mechanisation in LCF~\cite{paulson85} of Manna and Waldinger's theory~\cite{mw81}. It demonstrates a complicated use of \texttt{recdef}, with nested recursion. Directory \texttt{HOL/Induct} presents simple examples of (co)inductive definitions and datatypes. \begin{itemize} \item Theory \texttt{PropLog} proves the soundness and completeness of classical propositional logic, given a truth table semantics. The only connective is $\imp$. A Hilbert-style axiom system is specified, and its set of theorems defined inductively. A similar proof in ZF is described elsewhere~\cite{paulson-set-II}. \item Theory \texttt{Term} defines the datatype \texttt{term}. \item Theory \texttt{ABexp} defines arithmetic and boolean expressions as mutually recursive datatypes. \item The definition of lazy lists demonstrates methods for handling infinite data structures and coinduction in higher-order logic~\cite{paulson-coind}.% \footnote{To be precise, these lists are \emph{potentially infinite} rather than lazy. Lazy implies a particular operational semantics.} Theory \thydx{LList} defines an operator for corecursion on lazy lists, which is used to define a few simple functions such as map and append. A coinduction principle is defined for proving equations on lazy lists. \item Theory \thydx{LFilter} defines the filter functional for lazy lists. This functional is notoriously difficult to define because finding the next element meeting the predicate requires possibly unlimited search. It is not computable, but can be expressed using a combination of induction and corecursion. \item Theory \thydx{Exp} illustrates the use of iterated inductive definitions to express a programming language semantics that appears to require mutual induction. Iterated induction allows greater modularity. \end{itemize} Directory \texttt{HOL/ex} contains other examples and experimental proofs in HOL. \begin{itemize} \item Theory \texttt{Recdef} presents many examples of using \texttt{recdef} to define recursive functions. Another example is \texttt{Fib}, which defines the Fibonacci function. \item Theory \texttt{Primes} defines the Greatest Common Divisor of two natural numbers and proves a key lemma of the Fundamental Theorem of Arithmetic: if $p$ is prime and $p$ divides $m\times n$ then $p$ divides~$m$ or $p$ divides~$n$. \item Theory \texttt{Primrec} develops some computation theory. It inductively defines the set of primitive recursive functions and presents a proof that Ackermann's function is not primitive recursive. \item File \texttt{cla.ML} demonstrates the classical reasoner on over sixty predicate calculus theorems, ranging from simple tautologies to moderately difficult problems involving equality and quantifiers. \item File \texttt{meson.ML} contains an experimental implementation of the {\sc meson} proof procedure, inspired by Plaisted~\cite{plaisted90}. It is much more powerful than Isabelle's classical reasoner. But it is less useful in practice because it works only for pure logic; it does not accept derived rules for the set theory primitives, for example. \item File \texttt{mesontest.ML} contains test data for the {\sc meson} proof procedure. These are mostly taken from Pelletier \cite{pelletier86}. \item File \texttt{set.ML} proves Cantor's Theorem, which is presented in {\S}\ref{sec:hol-cantor} below, and the Schr{\"o}der-Bernstein Theorem. \item Theory \texttt{MT} contains Jacob Frost's formalization~\cite{frost93} of Milner and Tofte's coinduction example~\cite{milner-coind}. This substantial proof concerns the soundness of a type system for a simple functional language. The semantics of recursion is given by a cyclic environment, which makes a coinductive argument appropriate. \end{itemize} \goodbreak \section{Example: Cantor's Theorem}\label{sec:hol-cantor} Cantor's Theorem states that every set has more subsets than it has elements. It has become a favourite example in higher-order logic since it is so easily expressed: \[ \forall f::\alpha \To \alpha \To bool. \exists S::\alpha\To bool. \forall x::\alpha. f~x \not= S \] % Viewing types as sets, $\alpha\To bool$ represents the powerset of~$\alpha$. This version states that for every function from $\alpha$ to its powerset, some subset is outside its range. The Isabelle proof uses HOL's set theory, with the type $\alpha\,set$ and the operator \cdx{range}. \begin{ttbox} context Set.thy; \end{ttbox} The set~$S$ is given as an unknown instead of a quantified variable so that we may inspect the subset found by the proof. \begin{ttbox} Goal "?S ~: range\thinspace(f :: 'a=>'a set)"; {\out Level 0} {\out ?S ~: range f} {\out 1. ?S ~: range f} \end{ttbox} The first two steps are routine. The rule \tdx{rangeE} replaces $\Var{S}\in \texttt{range} \, f$ by $\Var{S}=f~x$ for some~$x$. \begin{ttbox} by (resolve_tac [notI] 1); {\out Level 1} {\out ?S ~: range f} {\out 1. ?S : range f ==> False} \ttbreak by (eresolve_tac [rangeE] 1); {\out Level 2} {\out ?S ~: range f} {\out 1. !!x. ?S = f x ==> False} \end{ttbox} Next, we apply \tdx{equalityCE}, reasoning that since $\Var{S}=f~x$, we have $\Var{c}\in \Var{S}$ if and only if $\Var{c}\in f~x$ for any~$\Var{c}$. \begin{ttbox} by (eresolve_tac [equalityCE] 1); {\out Level 3} {\out ?S ~: range f} {\out 1. !!x. [| ?c3 x : ?S; ?c3 x : f x |] ==> False} {\out 2. !!x. [| ?c3 x ~: ?S; ?c3 x ~: f x |] ==> False} \end{ttbox} Now we use a bit of creativity. Suppose that~$\Var{S}$ has the form of a comprehension. Then $\Var{c}\in\{x.\Var{P}~x\}$ implies $\Var{P}~\Var{c}$. Destruct-resolution using \tdx{CollectD} instantiates~$\Var{S}$ and creates the new assumption. \begin{ttbox} by (dresolve_tac [CollectD] 1); {\out Level 4} {\out {\ttlbrace}x. ?P7 x{\ttrbrace} ~: range f} {\out 1. !!x. [| ?c3 x : f x; ?P7(?c3 x) |] ==> False} {\out 2. !!x. [| ?c3 x ~: {\ttlbrace}x. ?P7 x{\ttrbrace}; ?c3 x ~: f x |] ==> False} \end{ttbox} Forcing a contradiction between the two assumptions of subgoal~1 completes the instantiation of~$S$. It is now the set $\{x. x\not\in f~x\}$, which is the standard diagonal construction. \begin{ttbox} by (contr_tac 1); {\out Level 5} {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f} {\out 1. !!x. [| x ~: {\ttlbrace}x. x ~: f x{\ttrbrace}; x ~: f x |] ==> False} \end{ttbox} The rest should be easy. To apply \tdx{CollectI} to the negated assumption, we employ \ttindex{swap_res_tac}: \begin{ttbox} by (swap_res_tac [CollectI] 1); {\out Level 6} {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f} {\out 1. !!x. [| x ~: f x; ~ False |] ==> x ~: f x} \ttbreak by (assume_tac 1); {\out Level 7} {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f} {\out No subgoals!} \end{ttbox} How much creativity is required? As it happens, Isabelle can prove this theorem automatically. The default classical set \texttt{claset()} contains rules for most of the constructs of HOL's set theory. We must augment it with \tdx{equalityCE} to break up set equalities, and then apply best-first search. Depth-first search would diverge, but best-first search successfully navigates through the large search space. \index{search!best-first} \begin{ttbox} choplev 0; {\out Level 0} {\out ?S ~: range f} {\out 1. ?S ~: range f} \ttbreak by (best_tac (claset() addSEs [equalityCE]) 1); {\out Level 1} {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f} {\out No subgoals!} \end{ttbox} If you run this example interactively, make sure your current theory contains theory \texttt{Set}, for example by executing \ttindex{context}~{\tt Set.thy}. Otherwise the default claset may not contain the rules for set theory. \index{higher-order logic|)} %%% Local Variables: %%% mode: latex %%% TeX-master: "logics-HOL" %%% End: