diff -r f4fe75218cec -r 0260bdba4dd7 src/Doc/HOL/document/HOL.tex --- a/src/Doc/HOL/document/HOL.tex Sun Jul 07 18:50:16 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,2089 +0,0 @@ -\chapter{Higher-Order Logic} -\index{higher-order logic|(} -\index{HOL system@{\sc hol} system} - -\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{"!@{\tt\char124} symbol} %\char124 is vertical bar. We use ! because | stopped working -\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, -either using the primitive \texttt{typedef} or the more convenient -\texttt{datatype} (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. -\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{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. - -\subsection{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. - - -\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. - -\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 m mod n = m -\tdx{mod_geq} [| 0 m mod n = (m-n) mod n - -\tdx{div_less} m m div n = 0 -\tdx{div_geq} [| 0 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. - -%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 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 [] | 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. The recursion equations -are shown in Figs.\ts\ref{fig:HOL:list-simps} and~\ref{fig:HOL:list-simps2}. - -\index{list@{\textit{list}} type|)} - - -\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}, 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 given in the -Isabelle/Isar reference manual. 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. - -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$. - - -\section{Old-style recursive function definitions}\label{sec:HOL:recursive} -\index{recursion!general|(} -\index{*recdef|(} - -Old-style recursive definitions via \texttt{recdef} 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.} - -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)}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{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: