doc-src/HOL/HOL.tex
 author wenzelm Sat Apr 30 20:48:29 2011 +0200 (2011-04-30) changeset 42506 876887b07e8d parent 31101 26c7bb764a38 child 42627 8749742785b8 permissions -rw-r--r--
more robust error handling (NB: Source.source requires total scanner or recover);
tuned;
 wenzelm@6580  1 %% $Id$  wenzelm@6580  2 \chapter{Higher-Order Logic}  wenzelm@6580  3 \index{higher-order logic|(}  wenzelm@6580  4 \index{HOL system@{\sc hol} system}  wenzelm@6580  5 wenzelm@6580  6 The theory~\thydx{HOL} implements higher-order logic. It is based on  wenzelm@6580  7 Gordon's~{\sc hol} system~\cite{mgordon-hol}, which itself is based on  wenzelm@9695  8 Church's original paper~\cite{church40}. Andrews's book~\cite{andrews86} is a  wenzelm@9695  9 full description of the original Church-style higher-order logic. Experience  wenzelm@9695  10 with the {\sc hol} system has demonstrated that higher-order logic is widely  wenzelm@9695  11 applicable in many areas of mathematics and computer science, not just  wenzelm@9695  12 hardware verification, {\sc hol}'s original \textit{raison d'{\^e}tre\/}. It  wenzelm@9695  13 is weaker than ZF set theory but for most applications this does not matter.  wenzelm@9695  14 If you prefer {\ML} to Lisp, you will probably prefer HOL to~ZF.  wenzelm@9695  15 wenzelm@9695  16 The syntax of HOL\footnote{Earlier versions of Isabelle's HOL used a different  wenzelm@9695  17  syntax. Ancient releases of Isabelle included still another version of~HOL,  wenzelm@9695  18  with explicit type inference rules~\cite{paulson-COLOG}. This version no  wenzelm@9695  19  longer exists, but \thydx{ZF} supports a similar style of reasoning.}  wenzelm@9695  20 follows $\lambda$-calculus and functional programming. Function application  wenzelm@9695  21 is curried. To apply the function~$f$ of type $\tau@1\To\tau@2\To\tau@3$ to  wenzelm@9695  22 the arguments~$a$ and~$b$ in HOL, you simply write $f\,a\,b$. There is no  wenzelm@9695  23 apply' operator as in \thydx{ZF}. Note that $f(a,b)$ means $f$ applied to  wenzelm@9695  24 the pair $(a,b)$'' in HOL. We write ordered pairs as $(a,b)$, not $\langle  wenzelm@9695  25 a,b\rangle$ as in ZF.  wenzelm@9695  26 wenzelm@9695  27 HOL has a distinct feel, compared with ZF and CTT. It identifies object-level  wenzelm@9695  28 types with meta-level types, taking advantage of Isabelle's built-in  wenzelm@9695  29 type-checker. It identifies object-level functions with meta-level functions,  wenzelm@9695  30 so it uses Isabelle's operations for abstraction and application.  wenzelm@9695  31 wenzelm@9695  32 These identifications allow Isabelle to support HOL particularly nicely, but  wenzelm@9695  33 they also mean that HOL requires more sophistication from the user --- in  wenzelm@9695  34 particular, an understanding of Isabelle's type system. Beginners should work  wenzelm@9695  35 with \texttt{show_types} (or even \texttt{show_sorts}) set to \texttt{true}.  wenzelm@6580  36 wenzelm@6580  37 wenzelm@6580  38 \begin{figure}  wenzelm@6580  39 \begin{constants}  wenzelm@6580  40  \it name &\it meta-type & \it description \\  wenzelm@6580  41  \cdx{Trueprop}& $bool\To prop$ & coercion to $prop$\\  oheimb@7490  42  \cdx{Not} & $bool\To bool$ & negation ($\lnot$) \\  wenzelm@6580  43  \cdx{True} & $bool$ & tautology ($\top$) \\  wenzelm@6580  44  \cdx{False} & $bool$ & absurdity ($\bot$) \\  wenzelm@6580  45  \cdx{If} & $[bool,\alpha,\alpha]\To\alpha$ & conditional \\  wenzelm@6580  46  \cdx{Let} & $[\alpha,\alpha\To\beta]\To\beta$ & let binder  wenzelm@6580  47 \end{constants}  wenzelm@6580  48 \subcaption{Constants}  wenzelm@6580  49 wenzelm@6580  50 \begin{constants}  wenzelm@6580  51 \index{"@@{\tt\at} symbol}  wenzelm@6580  52 \index{*"! symbol}\index{*"? symbol}  wenzelm@6580  53 \index{*"?"! symbol}\index{*"E"X"! symbol}  wenzelm@6580  54  \it symbol &\it name &\it meta-type & \it description \\  wenzelm@7245  55  \sdx{SOME} or \tt\at & \cdx{Eps} & $(\alpha\To bool)\To\alpha$ &  wenzelm@6580  56  Hilbert description ($\varepsilon$) \\  wenzelm@7245  57  \sdx{ALL} or {\tt!~} & \cdx{All} & $(\alpha\To bool)\To bool$ &  wenzelm@6580  58  universal quantifier ($\forall$) \\  wenzelm@7245  59  \sdx{EX} or {\tt?~} & \cdx{Ex} & $(\alpha\To bool)\To bool$ &  wenzelm@6580  60  existential quantifier ($\exists$) \\  wenzelm@7245  61  \texttt{EX!} or {\tt?!} & \cdx{Ex1} & $(\alpha\To bool)\To bool$ &  wenzelm@6580  62  unique existence ($\exists!$)\\  wenzelm@6580  63  \texttt{LEAST} & \cdx{Least} & $(\alpha::ord \To bool)\To\alpha$ &  wenzelm@6580  64  least element  wenzelm@6580  65 \end{constants}  wenzelm@6580  66 \subcaption{Binders}  wenzelm@6580  67 wenzelm@6580  68 \begin{constants}  wenzelm@6580  69 \index{*"= symbol}  wenzelm@6580  70 \index{&@{\tt\&} symbol}  wenzelm@6580  71 \index{*"| symbol}  wenzelm@6580  72 \index{*"-"-"> symbol}  wenzelm@6580  73  \it symbol & \it meta-type & \it priority & \it description \\  wenzelm@6580  74  \sdx{o} & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ &  wenzelm@6580  75  Left 55 & composition ($\circ$) \\  wenzelm@6580  76  \tt = & $[\alpha,\alpha]\To bool$ & Left 50 & equality ($=$) \\  wenzelm@6580  77  \tt < & $[\alpha::ord,\alpha]\To bool$ & Left 50 & less than ($<$) \\  wenzelm@6580  78  \tt <= & $[\alpha::ord,\alpha]\To bool$ & Left 50 &  wenzelm@6580  79  less than or equals ($\leq$)\\  wenzelm@6580  80  \tt \& & $[bool,bool]\To bool$ & Right 35 & conjunction ($\conj$) \\  wenzelm@6580  81  \tt | & $[bool,bool]\To bool$ & Right 30 & disjunction ($\disj$) \\  wenzelm@6580  82  \tt --> & $[bool,bool]\To bool$ & Right 25 & implication ($\imp$)  wenzelm@6580  83 \end{constants}  wenzelm@6580  84 \subcaption{Infixes}  wenzelm@6580  85 \caption{Syntax of \texttt{HOL}} \label{hol-constants}  wenzelm@6580  86 \end{figure}  wenzelm@6580  87 wenzelm@6580  88 wenzelm@6580  89 \begin{figure}  wenzelm@6580  90 \index{*let symbol}  wenzelm@6580  91 \index{*in symbol}  wenzelm@6580  92 \dquotes  wenzelm@6580  93 $\begin{array}{rclcl}  wenzelm@6580  94  term & = & \hbox{expression of class~term} \\  wenzelm@7245  95  & | & "SOME~" id " . " formula  wenzelm@6580  96  & | & "\at~" id " . " formula \\  wenzelm@6580  97  & | &  wenzelm@6580  98  \multicolumn{3}{l}{"let"~id~"="~term";"\dots";"~id~"="~term~"in"~term} \\  wenzelm@6580  99  & | &  wenzelm@6580  100  \multicolumn{3}{l}{"if"~formula~"then"~term~"else"~term} \\  wenzelm@6580  101  & | & "LEAST"~ id " . " formula \\[2ex]  wenzelm@6580  102  formula & = & \hbox{expression of type~bool} \\  wenzelm@6580  103  & | & term " = " term \\  wenzelm@6580  104  & | & term " \ttilde= " term \\  wenzelm@6580  105  & | & term " < " term \\  wenzelm@6580  106  & | & term " <= " term \\  wenzelm@6580  107  & | & "\ttilde\ " formula \\  wenzelm@6580  108  & | & formula " \& " formula \\  wenzelm@6580  109  & | & formula " | " formula \\  wenzelm@6580  110  & | & formula " --> " formula \\  wenzelm@7245  111  & | & "ALL~" id~id^* " . " formula  wenzelm@7245  112  & | & "!~~~" id~id^* " . " formula \\  wenzelm@7245  113  & | & "EX~~" id~id^* " . " formula  wenzelm@7245  114  & | & "?~~~" id~id^* " . " formula \\  wenzelm@6580  115  & | & "EX!~" id~id^* " . " formula  wenzelm@7245  116  & | & "?!~~" id~id^* " . " formula \\  wenzelm@6580  117  \end{array}  wenzelm@6580  118 $  wenzelm@9695  119 \caption{Full grammar for HOL} \label{hol-grammar}  wenzelm@6580  120 \end{figure}  wenzelm@6580  121 wenzelm@6580  122 wenzelm@6580  123 \section{Syntax}  wenzelm@6580  124 wenzelm@6580  125 Figure~\ref{hol-constants} lists the constants (including infixes and  wenzelm@6580  126 binders), while Fig.\ts\ref{hol-grammar} presents the grammar of  wenzelm@6580  127 higher-order logic. Note that $a$\verb|~=|$b$ is translated to  oheimb@7490  128 $\lnot(a=b)$.  wenzelm@6580  129 wenzelm@6580  130 \begin{warn}  wenzelm@9695  131  HOL has no if-and-only-if connective; logical equivalence is expressed using  wenzelm@9695  132  equality. But equality has a high priority, as befitting a relation, while  wenzelm@9695  133  if-and-only-if typically has the lowest priority. Thus, $\lnot\lnot P=P$  wenzelm@9695  134  abbreviates $\lnot\lnot (P=P)$ and not $(\lnot\lnot P)=P$. When using $=$  wenzelm@9695  135  to mean logical equivalence, enclose both operands in parentheses.  wenzelm@6580  136 \end{warn}  wenzelm@6580  137 paulson@9212  138 \subsection{Types and overloading}  wenzelm@6580  139 The universal type class of higher-order terms is called~\cldx{term}.  wenzelm@6580  140 By default, explicit type variables have class \cldx{term}. In  wenzelm@6580  141 particular the equality symbol and quantifiers are polymorphic over  wenzelm@6580  142 class \texttt{term}.  wenzelm@6580  143 wenzelm@6580  144 The type of formulae, \tydx{bool}, belongs to class \cldx{term}; thus,  wenzelm@6580  145 formulae are terms. The built-in type~\tydx{fun}, which constructs  wenzelm@6580  146 function types, is overloaded with arity {\tt(term,\thinspace  wenzelm@6580  147  term)\thinspace term}. Thus, $\sigma\To\tau$ belongs to class~{\tt  wenzelm@6580  148  term} if $\sigma$ and~$\tau$ do, allowing quantification over  wenzelm@6580  149 functions.  wenzelm@6580  150 wenzelm@9695  151 HOL allows new types to be declared as subsets of existing types;  paulson@9212  152 see~{\S}\ref{sec:HOL:Types}. ML-like datatypes can also be declared; see  paulson@9212  153 ~{\S}\ref{sec:HOL:datatype}.  paulson@9212  154 paulson@9212  155 Several syntactic type classes --- \cldx{plus}, \cldx{minus},  paulson@9212  156 \cldx{times} and  paulson@9212  157 \cldx{power} --- permit overloading of the operators {\tt+},\index{*"+  paulson@9212  158  symbol} {\tt-}\index{*"- symbol}, {\tt*}.\index{*"* symbol}  paulson@9212  159 and \verb|^|.\index{^@\verb.^. symbol}  paulson@9212  160 %  paulson@9212  161 They are overloaded to denote the obvious arithmetic operations on types  paulson@9212  162 \tdx{nat}, \tdx{int} and~\tdx{real}. (With the \verb|^| operator, the  paulson@9212  163 exponent always has type~\tdx{nat}.) Non-arithmetic overloadings are also  paulson@9212  164 done: the operator {\tt-} can denote set difference, while \verb|^| can  paulson@9212  165 denote exponentiation of relations (iterated composition). Unary minus is  paulson@9212  166 also written as~{\tt-} and is overloaded like its 2-place counterpart; it even  paulson@9212  167 can stand for set complement.  paulson@9212  168 paulson@9212  169 The constant \cdx{0} is also overloaded. It serves as the zero element of  paulson@9212  170 several types, of which the most important is \tdx{nat} (the natural  paulson@9212  171 numbers). The type class \cldx{plus_ac0} comprises all types for which 0  paulson@9212  172 and~+ satisfy the laws $x+y=y+x$, $(x+y)+z = x+(y+z)$ and $0+x = x$. These  paulson@9212  173 types include the numeric ones \tdx{nat}, \tdx{int} and~\tdx{real} and also  paulson@9212  174 multisets. The summation operator \cdx{setsum} is available for all types in  paulson@9212  175 this class.  wenzelm@6580  176 wenzelm@6580  177 Theory \thydx{Ord} defines the syntactic class \cldx{ord} of order  paulson@9212  178 signatures. The relations $<$ and $\leq$ are polymorphic over this  wenzelm@6580  179 class, as are the functions \cdx{mono}, \cdx{min} and \cdx{max}, and  wenzelm@6580  180 the \cdx{LEAST} operator. \thydx{Ord} also defines a subclass  paulson@9212  181 \cldx{order} of \cldx{ord} which axiomatizes the types that are partially  paulson@9212  182 ordered with respect to~$\leq$. A further subclass \cldx{linorder} of  paulson@9212  183 \cldx{order} axiomatizes linear orderings.  paulson@9212  184 For details, see the file \texttt{Ord.thy}.  paulson@9212  185   wenzelm@6580  186 If you state a goal containing overloaded functions, you may need to include  wenzelm@6580  187 type constraints. Type inference may otherwise make the goal more  wenzelm@6580  188 polymorphic than you intended, with confusing results. For example, the  oheimb@7490  189 variables $i$, $j$ and $k$ in the goal $i \leq j \Imp i \leq j+k$ have type  wenzelm@6580  190 $\alpha::\{ord,plus\}$, although you may have expected them to have some  wenzelm@6580  191 numeric type, e.g. $nat$. Instead you should have stated the goal as  oheimb@7490  192 $(i::nat) \leq j \Imp i \leq j+k$, which causes all three variables to have  wenzelm@6580  193 type $nat$.  wenzelm@6580  194 wenzelm@6580  195 \begin{warn}  wenzelm@6580  196  If resolution fails for no obvious reason, try setting  wenzelm@6580  197  \ttindex{show_types} to \texttt{true}, causing Isabelle to display  wenzelm@6580  198  types of terms. Possibly set \ttindex{show_sorts} to \texttt{true} as  wenzelm@6580  199  well, causing Isabelle to display type classes and sorts.  wenzelm@6580  200 wenzelm@6580  201  \index{unification!incompleteness of}  wenzelm@6580  202  Where function types are involved, Isabelle's unification code does not  wenzelm@6580  203  guarantee to find instantiations for type variables automatically. Be  wenzelm@6580  204  prepared to use \ttindex{res_inst_tac} instead of \texttt{resolve_tac},  wenzelm@6580  205  possibly instantiating type variables. Setting  wenzelm@6580  206  \ttindex{Unify.trace_types} to \texttt{true} causes Isabelle to report  wenzelm@6580  207  omitted search paths during unification.\index{tracing!of unification}  wenzelm@6580  208 \end{warn}  wenzelm@6580  209 wenzelm@6580  210 wenzelm@6580  211 \subsection{Binders}  wenzelm@6580  212 wenzelm@9695  213 Hilbert's {\bf description} operator~$\varepsilon x. P[x]$ stands for some~$x$  wenzelm@9695  214 satisfying~$P$, if such exists. Since all terms in HOL denote something, a  wenzelm@9695  215 description is always meaningful, but we do not know its value unless $P$  wenzelm@9695  216 defines it uniquely. We may write descriptions as \cdx{Eps}($\lambda x.  wenzelm@9695  217 P[x]$) or use the syntax \hbox{\tt SOME~$x$.~$P[x]$}.  wenzelm@6580  218 wenzelm@6580  219 Existential quantification is defined by  wenzelm@6580  220 $\exists x. P~x \;\equiv\; P(\varepsilon x. P~x).$  wenzelm@6580  221 The unique existence quantifier, $\exists!x. P$, is defined in terms  wenzelm@6580  222 of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested  wenzelm@6580  223 quantifications. For instance, $\exists!x\,y. P\,x\,y$ abbreviates  wenzelm@6580  224 $\exists!x. \exists!y. P\,x\,y$; note that this does not mean that there  wenzelm@6580  225 exists a unique pair $(x,y)$ satisfying~$P\,x\,y$.  wenzelm@6580  226 wenzelm@7245  227 \medskip  wenzelm@7245  228 wenzelm@7245  229 \index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system} The  wenzelm@7245  230 basic Isabelle/HOL binders have two notations. Apart from the usual  wenzelm@7245  231 \texttt{ALL} and \texttt{EX} for $\forall$ and $\exists$, Isabelle/HOL also  wenzelm@7245  232 supports the original notation of Gordon's {\sc hol} system: \texttt{!}\  wenzelm@7245  233 and~\texttt{?}. In the latter case, the existential quantifier \emph{must} be  wenzelm@7245  234 followed by a space; thus {\tt?x} is an unknown, while \verb'? x. f x=y' is a  wenzelm@7245  235 quantification. Both notations are accepted for input. The print mode  wenzelm@7245  236 \ttindexbold{HOL}'' governs the output notation. If enabled (e.g.\ by  wenzelm@7245  237 passing option \texttt{-m HOL} to the \texttt{isabelle} executable),  wenzelm@7245  238 then~{\tt!}\ and~{\tt?}\ are displayed.  wenzelm@7245  239 wenzelm@7245  240 \medskip  wenzelm@6580  241 wenzelm@6580  242 If $\tau$ is a type of class \cldx{ord}, $P$ a formula and $x$ a  wenzelm@6580  243 variable of type $\tau$, then the term \cdx{LEAST}~$x. P[x]$ is defined  oheimb@7490  244 to be the least (w.r.t.\ $\leq$) $x$ such that $P~x$ holds (see  wenzelm@6580  245 Fig.~\ref{hol-defs}). The definition uses Hilbert's $\varepsilon$  wenzelm@6580  246 choice operator, so \texttt{Least} is always meaningful, but may yield  wenzelm@6580  247 nothing useful in case there is not a unique least element satisfying  wenzelm@6580  248 $P$.\footnote{Class $ord$ does not require much of its instances, so  oheimb@7490  249  $\leq$ need not be a well-ordering, not even an order at all!}  wenzelm@6580  250 wenzelm@6580  251 \medskip All these binders have priority 10.  wenzelm@6580  252 wenzelm@6580  253 \begin{warn}  wenzelm@6580  254 The low priority of binders means that they need to be enclosed in  wenzelm@6580  255 parenthesis when they occur in the context of other operations. For example,  wenzelm@6580  256 instead of $P \land \forall x. Q$ you need to write $P \land (\forall x. Q)$.  wenzelm@6580  257 \end{warn}  wenzelm@6580  258 wenzelm@6580  259 wenzelm@6620  260 \subsection{The let and case constructions}  wenzelm@6580  261 Local abbreviations can be introduced by a \texttt{let} construct whose  wenzelm@6580  262 syntax appears in Fig.\ts\ref{hol-grammar}. Internally it is translated into  wenzelm@6580  263 the constant~\cdx{Let}. It can be expanded by rewriting with its  wenzelm@6580  264 definition, \tdx{Let_def}.  wenzelm@6580  265 wenzelm@9695  266 HOL also defines the basic syntax  wenzelm@6580  267 $\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n$  wenzelm@6580  268 as a uniform means of expressing \texttt{case} constructs. Therefore \texttt{case}  wenzelm@6580  269 and \sdx{of} are reserved words. Initially, this is mere syntax and has no  wenzelm@6580  270 logical meaning. By declaring translations, you can cause instances of the  wenzelm@6580  271 \texttt{case} construct to denote applications of particular case operators.  wenzelm@6580  272 This is what happens automatically for each \texttt{datatype} definition  oheimb@7490  273 (see~{\S}\ref{sec:HOL:datatype}).  wenzelm@6580  274 wenzelm@6580  275 \begin{warn}  wenzelm@6580  276 Both \texttt{if} and \texttt{case} constructs have as low a priority as  wenzelm@6580  277 quantifiers, which requires additional enclosing parentheses in the context  wenzelm@6580  278 of most other operations. For example, instead of $f~x = {\tt if\dots  wenzelm@6580  279 then\dots else}\dots$ you need to write $f~x = ({\tt if\dots then\dots  wenzelm@6580  280 else\dots})$.  wenzelm@6580  281 \end{warn}  wenzelm@6580  282 wenzelm@6580  283 \section{Rules of inference}  wenzelm@6580  284 wenzelm@6580  285 \begin{figure}  wenzelm@6580  286 \begin{ttbox}\makeatother  paulson@9212  287 \tdx{refl} t = (t::'a)  paulson@9212  288 \tdx{subst} [| s = t; P s |] ==> P (t::'a)  paulson@9212  289 \tdx{ext} (!!x::'a. (f x :: 'b) = g x) ==> (\%x. f x) = (\%x. g x)  paulson@9212  290 \tdx{impI} (P ==> Q) ==> P-->Q  paulson@9212  291 \tdx{mp} [| P-->Q; P |] ==> Q  paulson@9212  292 \tdx{iff} (P-->Q) --> (Q-->P) --> (P=Q)  paulson@9969  293 \tdx{someI} P(x::'a) ==> P(@x. P x)  paulson@9212  294 \tdx{True_or_False} (P=True) | (P=False)  wenzelm@6580  295 \end{ttbox}  wenzelm@6580  296 \caption{The \texttt{HOL} rules} \label{hol-rules}  wenzelm@6580  297 \end{figure}  wenzelm@6580  298 wenzelm@9695  299 Figure~\ref{hol-rules} shows the primitive inference rules of~HOL, with  wenzelm@9695  300 their~{\ML} names. Some of the rules deserve additional comments:  wenzelm@6580  301 \begin{ttdescription}  wenzelm@6580  302 \item[\tdx{ext}] expresses extensionality of functions.  wenzelm@6580  303 \item[\tdx{iff}] asserts that logically equivalent formulae are  wenzelm@6580  304  equal.  paulson@9969  305 \item[\tdx{someI}] gives the defining property of the Hilbert  wenzelm@6580  306  $\varepsilon$-operator. It is a form of the Axiom of Choice. The derived rule  paulson@9969  307  \tdx{some_equality} (see below) is often easier to use.  wenzelm@6580  308 \item[\tdx{True_or_False}] makes the logic classical.\footnote{In  wenzelm@6580  309  fact, the $\varepsilon$-operator already makes the logic classical, as  wenzelm@6580  310  shown by Diaconescu; see Paulson~\cite{paulson-COLOG} for details.}  wenzelm@6580  311 \end{ttdescription}  wenzelm@6580  312 wenzelm@6580  313 wenzelm@6580  314 \begin{figure}\hfuzz=4pt%suppress "Overfull \hbox" message  wenzelm@6580  315 \begin{ttbox}\makeatother  wenzelm@6580  316 \tdx{True_def} True == ((\%x::bool. x)=(\%x. x))  wenzelm@6580  317 \tdx{All_def} All == (\%P. P = (\%x. True))  wenzelm@6580  318 \tdx{Ex_def} Ex == (\%P. P(@x. P x))  wenzelm@6580  319 \tdx{False_def} False == (!P. P)  wenzelm@6580  320 \tdx{not_def} not == (\%P. P-->False)  wenzelm@6580  321 \tdx{and_def} op & == (\%P Q. !R. (P-->Q-->R) --> R)  wenzelm@6580  322 \tdx{or_def} op | == (\%P Q. !R. (P-->R) --> (Q-->R) --> R)  wenzelm@6580  323 \tdx{Ex1_def} Ex1 == (\%P. ? x. P x & (! y. P y --> y=x))  wenzelm@6580  324 wenzelm@6580  325 \tdx{o_def} op o == (\%(f::'b=>'c) g x::'a. f(g x))  wenzelm@6580  326 \tdx{if_def} If P x y ==  wenzelm@6580  327  (\%P x y. @z::'a.(P=True --> z=x) & (P=False --> z=y))  wenzelm@6580  328 \tdx{Let_def} Let s f == f s  wenzelm@6580  329 \tdx{Least_def} Least P == @x. P(x) & (ALL y. P(y) --> x <= y)"  wenzelm@6580  330 \end{ttbox}  wenzelm@6580  331 \caption{The \texttt{HOL} definitions} \label{hol-defs}  wenzelm@6580  332 \end{figure}  wenzelm@6580  333 wenzelm@6580  334 wenzelm@9695  335 HOL follows standard practice in higher-order logic: only a few connectives  wenzelm@9695  336 are taken as primitive, with the remainder defined obscurely  wenzelm@6580  337 (Fig.\ts\ref{hol-defs}). Gordon's {\sc hol} system expresses the  wenzelm@6580  338 corresponding definitions \cite[page~270]{mgordon-hol} using  wenzelm@9695  339 object-equality~({\tt=}), which is possible because equality in higher-order  wenzelm@9695  340 logic may equate formulae and even functions over formulae. But theory~HOL,  wenzelm@9695  341 like all other Isabelle theories, uses meta-equality~({\tt==}) for  wenzelm@9695  342 definitions.  wenzelm@6580  343 \begin{warn}  wenzelm@6580  344 The definitions above should never be expanded and are shown for completeness  wenzelm@6580  345 only. Instead users should reason in terms of the derived rules shown below  wenzelm@6580  346 or, better still, using high-level tactics  oheimb@7490  347 (see~{\S}\ref{sec:HOL:generic-packages}).  wenzelm@6580  348 \end{warn}  wenzelm@6580  349 wenzelm@6580  350 Some of the rules mention type variables; for example, \texttt{refl}  wenzelm@6580  351 mentions the type variable~{\tt'a}. This allows you to instantiate  wenzelm@6580  352 type variables explicitly by calling \texttt{res_inst_tac}.  wenzelm@6580  353 wenzelm@6580  354 wenzelm@6580  355 \begin{figure}  wenzelm@6580  356 \begin{ttbox}  wenzelm@6580  357 \tdx{sym} s=t ==> t=s  wenzelm@6580  358 \tdx{trans} [| r=s; s=t |] ==> r=t  wenzelm@6580  359 \tdx{ssubst} [| t=s; P s |] ==> P t  wenzelm@6580  360 \tdx{box_equals} [| a=b; a=c; b=d |] ==> c=d  wenzelm@6580  361 \tdx{arg_cong} x = y ==> f x = f y  wenzelm@6580  362 \tdx{fun_cong} f = g ==> f x = g x  wenzelm@6580  363 \tdx{cong} [| f = g; x = y |] ==> f x = g y  wenzelm@6580  364 \tdx{not_sym} t ~= s ==> s ~= t  wenzelm@6580  365 \subcaption{Equality}  wenzelm@6580  366 wenzelm@6580  367 \tdx{TrueI} True  wenzelm@6580  368 \tdx{FalseE} False ==> P  wenzelm@6580  369 wenzelm@6580  370 \tdx{conjI} [| P; Q |] ==> P&Q  wenzelm@6580  371 \tdx{conjunct1} [| P&Q |] ==> P  wenzelm@6580  372 \tdx{conjunct2} [| P&Q |] ==> Q  wenzelm@6580  373 \tdx{conjE} [| P&Q; [| P; Q |] ==> R |] ==> R  wenzelm@6580  374 wenzelm@6580  375 \tdx{disjI1} P ==> P|Q  wenzelm@6580  376 \tdx{disjI2} Q ==> P|Q  wenzelm@6580  377 \tdx{disjE} [| P | Q; P ==> R; Q ==> R |] ==> R  wenzelm@6580  378 wenzelm@6580  379 \tdx{notI} (P ==> False) ==> ~ P  wenzelm@6580  380 \tdx{notE} [| ~ P; P |] ==> R  wenzelm@6580  381 \tdx{impE} [| P-->Q; P; Q ==> R |] ==> R  wenzelm@6580  382 \subcaption{Propositional logic}  wenzelm@6580  383 wenzelm@6580  384 \tdx{iffI} [| P ==> Q; Q ==> P |] ==> P=Q  wenzelm@6580  385 \tdx{iffD1} [| P=Q; P |] ==> Q  wenzelm@6580  386 \tdx{iffD2} [| P=Q; Q |] ==> P  wenzelm@6580  387 \tdx{iffE} [| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R  wenzelm@6580  388 \subcaption{Logical equivalence}  wenzelm@6580  389 wenzelm@6580  390 \end{ttbox}  wenzelm@9695  391 \caption{Derived rules for HOL} \label{hol-lemmas1}  wenzelm@6580  392 \end{figure}  kleing@14013  393 %  kleing@14013  394 %\tdx{eqTrueI} P ==> P=True  kleing@14013  395 %\tdx{eqTrueE} P=True ==> P  wenzelm@6580  396 wenzelm@6580  397 wenzelm@6580  398 \begin{figure}  wenzelm@6580  399 \begin{ttbox}\makeatother  wenzelm@6580  400 \tdx{allI} (!!x. P x) ==> !x. P x  wenzelm@6580  401 \tdx{spec} !x. P x ==> P x  wenzelm@6580  402 \tdx{allE} [| !x. P x; P x ==> R |] ==> R  wenzelm@6580  403 \tdx{all_dupE} [| !x. P x; [| P x; !x. P x |] ==> R |] ==> R  wenzelm@6580  404 wenzelm@6580  405 \tdx{exI} P x ==> ? x. P x  wenzelm@6580  406 \tdx{exE} [| ? x. P x; !!x. P x ==> Q |] ==> Q  wenzelm@6580  407 wenzelm@6580  408 \tdx{ex1I} [| P a; !!x. P x ==> x=a |] ==> ?! x. P x  wenzelm@6580  409 \tdx{ex1E} [| ?! x. P x; !!x. [| P x; ! y. P y --> y=x |] ==> R  wenzelm@6580  410  |] ==> R  wenzelm@6580  411 paulson@9969  412 \tdx{some_equality} [| P a; !!x. P x ==> x=a |] ==> (@x. P x) = a  wenzelm@6580  413 \subcaption{Quantifiers and descriptions}  wenzelm@6580  414 wenzelm@6580  415 \tdx{ccontr} (~P ==> False) ==> P  wenzelm@6580  416 \tdx{classical} (~P ==> P) ==> P  wenzelm@6580  417 \tdx{excluded_middle} ~P | P  wenzelm@6580  418 paulson@9212  419 \tdx{disjCI} (~Q ==> P) ==> P|Q  paulson@9212  420 \tdx{exCI} (! x. ~ P x ==> P a) ==> ? x. P x  paulson@9212  421 \tdx{impCE} [| P-->Q; ~ P ==> R; Q ==> R |] ==> R  paulson@9212  422 \tdx{iffCE} [| P=Q; [| P;Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R  paulson@9212  423 \tdx{notnotD} ~~P ==> P  paulson@9212  424 \tdx{swap} ~P ==> (~Q ==> P) ==> Q  wenzelm@6580  425 \subcaption{Classical logic}  wenzelm@6580  426 paulson@9212  427 \tdx{if_P} P ==> (if P then x else y) = x  paulson@9212  428 \tdx{if_not_P} ~ P ==> (if P then x else y) = y  paulson@9212  429 \tdx{split_if} P(if Q then x else y) = ((Q --> P x) & (~Q --> P y))  wenzelm@6580  430 \subcaption{Conditionals}  wenzelm@6580  431 \end{ttbox}  wenzelm@6580  432 \caption{More derived rules} \label{hol-lemmas2}  wenzelm@6580  433 \end{figure}  wenzelm@6580  434 wenzelm@6580  435 Some derived rules are shown in Figures~\ref{hol-lemmas1}  wenzelm@6580  436 and~\ref{hol-lemmas2}, with their {\ML} names. These include natural rules  wenzelm@6580  437 for the logical connectives, as well as sequent-style elimination rules for  wenzelm@6580  438 conjunctions, implications, and universal quantifiers.  wenzelm@6580  439 wenzelm@6580  440 Note the equality rules: \tdx{ssubst} performs substitution in  wenzelm@6580  441 backward proofs, while \tdx{box_equals} supports reasoning by  wenzelm@6580  442 simplifying both sides of an equation.  wenzelm@6580  443 wenzelm@6580  444 The following simple tactics are occasionally useful:  wenzelm@6580  445 \begin{ttdescription}  wenzelm@6580  446 \item[\ttindexbold{strip_tac} $i$] applies \texttt{allI} and \texttt{impI}  wenzelm@6580  447  repeatedly to remove all outermost universal quantifiers and implications  wenzelm@6580  448  from subgoal $i$.  wenzelm@8443  449 \item[\ttindexbold{case_tac} {\tt"}$P${\tt"} $i$] performs case distinction on  wenzelm@8443  450  $P$ for subgoal $i$: the latter is replaced by two identical subgoals with  wenzelm@8443  451  the added assumptions $P$ and $\lnot P$, respectively.  oheimb@7490  452 \item[\ttindexbold{smp_tac} $j$ $i$] applies $j$ times \texttt{spec} and then  oheimb@7490  453  \texttt{mp} in subgoal $i$, which is typically useful when forward-chaining  oheimb@7490  454  from an induction hypothesis. As a generalization of \texttt{mp_tac},  oheimb@7490  455  if there are assumptions $\forall \vec{x}. P \vec{x} \imp Q \vec{x}$ and  oheimb@7490  456  $P \vec{a}$, ($\vec{x}$ being a vector of $j$ variables)  oheimb@7490  457  then it replaces the universally quantified implication by $Q \vec{a}$.  oheimb@7490  458  It may instantiate unknowns. It fails if it can do nothing.  wenzelm@6580  459 \end{ttdescription}  wenzelm@6580  460 wenzelm@6580  461 wenzelm@6580  462 \begin{figure}  wenzelm@6580  463 \begin{center}  wenzelm@6580  464 \begin{tabular}{rrr}  wenzelm@6580  465  \it name &\it meta-type & \it description \\  wenzelm@6580  466 \index{{}@\verb'{}' symbol}  wenzelm@6580  467  \verb|{}| & $\alpha\,set$ & the empty set \\  wenzelm@6580  468  \cdx{insert} & $[\alpha,\alpha\,set]\To \alpha\,set$  wenzelm@6580  469  & insertion of element \\  wenzelm@6580  470  \cdx{Collect} & $(\alpha\To bool)\To\alpha\,set$  wenzelm@6580  471  & comprehension \\  wenzelm@6580  472  \cdx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$  wenzelm@6580  473  & intersection over a set\\  wenzelm@6580  474  \cdx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$  wenzelm@6580  475  & union over a set\\  wenzelm@6580  476  \cdx{Inter} & $(\alpha\,set)set\To\alpha\,set$  wenzelm@6580  477  &set of sets intersection \\  wenzelm@6580  478  \cdx{Union} & $(\alpha\,set)set\To\alpha\,set$  wenzelm@6580  479  &set of sets union \\  wenzelm@6580  480  \cdx{Pow} & $\alpha\,set \To (\alpha\,set)set$  wenzelm@6580  481  & powerset \$1ex]  wenzelm@6580  482  \cdx{range} & (\alpha\To\beta )\To\beta\,set  wenzelm@6580  483  & range of a function \\[1ex]  wenzelm@6580  484  \cdx{Ball}~~\cdx{Bex} & [\alpha\,set,\alpha\To bool]\To bool  wenzelm@6580  485  & bounded quantifiers  wenzelm@6580  486 \end{tabular}  wenzelm@6580  487 \end{center}  wenzelm@6580  488 \subcaption{Constants}  wenzelm@6580  489 wenzelm@6580  490 \begin{center}  wenzelm@6580  491 \begin{tabular}{llrrr}  wenzelm@6580  492  \it symbol &\it name &\it meta-type & \it priority & \it description \\  wenzelm@6580  493  \sdx{INT} & \cdx{INTER1} & (\alpha\To\beta\,set)\To\beta\,set & 10 &  paulson@9212  494  intersection\\  wenzelm@6580  495  \sdx{UN} & \cdx{UNION1} & (\alpha\To\beta\,set)\To\beta\,set & 10 &  paulson@9212  496  union  wenzelm@6580  497 \end{tabular}  wenzelm@6580  498 \end{center}  wenzelm@6580  499 \subcaption{Binders}  wenzelm@6580  500 wenzelm@6580  501 \begin{center}  wenzelm@6580  502 \index{*"" symbol}  wenzelm@6580  503 \index{*": symbol}  wenzelm@6580  504 \index{*"<"= symbol}  wenzelm@6580  505 \begin{tabular}{rrrr}  wenzelm@6580  506  \it symbol & \it meta-type & \it priority & \it description \\  wenzelm@6580  507  \tt  & [\alpha\To\beta ,\alpha\,set]\To \beta\,set  wenzelm@6580  508  & Left 90 & image \\  wenzelm@6580  509  \sdx{Int} & [\alpha\,set,\alpha\,set]\To\alpha\,set  wenzelm@6580  510  & Left 70 & intersection (\int) \\  wenzelm@6580  511  \sdx{Un} & [\alpha\,set,\alpha\,set]\To\alpha\,set  wenzelm@6580  512  & Left 65 & union (\un) \\  wenzelm@6580  513  \tt: & [\alpha ,\alpha\,set]\To bool  wenzelm@6580  514  & Left 50 & membership (\in) \\  wenzelm@6580  515  \tt <= & [\alpha\,set,\alpha\,set]\To bool  wenzelm@6580  516  & Left 50 & subset (\subseteq)  wenzelm@6580  517 \end{tabular}  wenzelm@6580  518 \end{center}  wenzelm@6580  519 \subcaption{Infixes}  wenzelm@6580  520 \caption{Syntax of the theory \texttt{Set}} \label{hol-set-syntax}  wenzelm@6580  521 \end{figure}  wenzelm@6580  522 wenzelm@6580  523 wenzelm@6580  524 \begin{figure}  wenzelm@6580  525 \begin{center} \tt\frenchspacing  wenzelm@6580  526 \index{*"! symbol}  wenzelm@6580  527 \begin{tabular}{rrr}  wenzelm@6580  528  \it external & \it internal & \it description \\  paulson@9212  529  a \ttilde: b & \ttilde(a : b) & \rm not in\\  wenzelm@6580  530  {\ttlbrace}a@1, \ldots{\ttrbrace} & insert a@1 \ldots {\ttlbrace}{\ttrbrace} & \rm finite set \\  wenzelm@6580  531  {\ttlbrace}x. P[x]{\ttrbrace} & Collect(\lambda x. P[x]) &  wenzelm@6580  532  \rm comprehension \\  wenzelm@6580  533  \sdx{INT} x:A. B[x] & INTER A \lambda x. B[x] &  wenzelm@6580  534  \rm intersection \\  wenzelm@6580  535  \sdx{UN}{\tt\ } x:A. B[x] & UNION A \lambda x. B[x] &  wenzelm@6580  536  \rm union \\  paulson@9212  537  \sdx{ALL} x:A.\ P[x] or \texttt{!} x:A.\ P[x] &  paulson@9212  538  Ball A \lambda x.\ P[x] &  wenzelm@6580  539  \rm bounded \forall \\  paulson@9212  540  \sdx{EX}{\tt\ } x:A.\ P[x] or \texttt{?} x:A.\ P[x] &  paulson@9212  541  Bex A \lambda x.\ P[x] & \rm bounded \exists  wenzelm@6580  542 \end{tabular}  wenzelm@6580  543 \end{center}  wenzelm@6580  544 \subcaption{Translations}  wenzelm@6580  545 wenzelm@6580  546 \dquotes  wenzelm@6580  547 \[\begin{array}{rclcl}  wenzelm@6580  548  term & = & \hbox{other terms\ldots} \\  wenzelm@6580  549  & | & "{\ttlbrace}{\ttrbrace}" \\  wenzelm@6580  550  & | & "{\ttlbrace} " term\; ("," term)^* " {\ttrbrace}" \\  wenzelm@6580  551  & | & "{\ttlbrace} " id " . " formula " {\ttrbrace}" \\  wenzelm@6580  552  & | & term "  " term \\  wenzelm@6580  553  & | & term " Int " term \\  wenzelm@6580  554  & | & term " Un " term \\  wenzelm@6580  555  & | & "INT~~" id ":" term " . " term \\  wenzelm@6580  556  & | & "UN~~~" id ":" term " . " term \\  wenzelm@6580  557  & | & "INT~~" id~id^* " . " term \\  wenzelm@6580  558  & | & "UN~~~" id~id^* " . " term \\[2ex]  wenzelm@6580  559  formula & = & \hbox{other formulae\ldots} \\  wenzelm@6580  560  & | & term " : " term \\  wenzelm@6580  561  & | & term " \ttilde: " term \\  wenzelm@6580  562  & | & term " <= " term \\  wenzelm@7245  563  & | & "ALL " id ":" term " . " formula  wenzelm@7245  564  & | & "!~" id ":" term " . " formula \\  wenzelm@6580  565  & | & "EX~~" id ":" term " . " formula  wenzelm@7245  566  & | & "?~" id ":" term " . " formula \\  wenzelm@6580  567  \end{array}  wenzelm@6580  568 $  wenzelm@6580  569 \subcaption{Full Grammar}  wenzelm@6580  570 \caption{Syntax of the theory \texttt{Set} (continued)} \label{hol-set-syntax2}  wenzelm@6580  571 \end{figure}  wenzelm@6580  572 wenzelm@6580  573 wenzelm@6580  574 \section{A formulation of set theory}  wenzelm@6580  575 Historically, higher-order logic gives a foundation for Russell and  wenzelm@6580  576 Whitehead's theory of classes. Let us use modern terminology and call them  wenzelm@9695  577 {\bf sets}, but note that these sets are distinct from those of ZF set theory,  wenzelm@9695  578 and behave more like ZF classes.  wenzelm@6580  579 \begin{itemize}  wenzelm@6580  580 \item  wenzelm@6580  581 Sets are given by predicates over some type~$\sigma$. Types serve to  wenzelm@6580  582 define universes for sets, but type-checking is still significant.  wenzelm@6580  583 \item  wenzelm@6580  584 There is a universal set (for each type). Thus, sets have complements, and  wenzelm@6580  585 may be defined by absolute comprehension.  wenzelm@6580  586 \item  wenzelm@6580  587 Although sets may contain other sets as elements, the containing set must  wenzelm@6580  588 have a more complex type.  wenzelm@6580  589 \end{itemize}  wenzelm@9695  590 Finite unions and intersections have the same behaviour in HOL as they do  wenzelm@9695  591 in~ZF. In HOL the intersection of the empty set is well-defined, denoting the  wenzelm@9695  592 universal set for the given type.  wenzelm@6580  593 wenzelm@6580  594 \subsection{Syntax of set theory}\index{*set type}  wenzelm@9695  595 HOL's set theory is called \thydx{Set}. The type $\alpha\,set$ is essentially  wenzelm@9695  596 the same as $\alpha\To bool$. The new type is defined for clarity and to  wenzelm@9695  597 avoid complications involving function types in unification. The isomorphisms  wenzelm@9695  598 between the two types are declared explicitly. They are very natural:  wenzelm@9695  599 \texttt{Collect} maps $\alpha\To bool$ to $\alpha\,set$, while \hbox{\tt op :}  wenzelm@9695  600 maps in the other direction (ignoring argument order).  wenzelm@6580  601 wenzelm@6580  602 Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax  wenzelm@6580  603 translations. Figure~\ref{hol-set-syntax2} presents the grammar of the new  wenzelm@6580  604 constructs. Infix operators include union and intersection ($A\un B$  wenzelm@6580  605 and $A\int B$), the subset and membership relations, and the image  wenzelm@6580  606 operator~{\tt}\@. Note that $a$\verb|~:|$b$ is translated to  oheimb@7490  607 $\lnot(a\in b)$.  wenzelm@6580  608 wenzelm@6580  609 The $\{a@1,\ldots\}$ notation abbreviates finite sets constructed in  wenzelm@6580  610 the obvious manner using~\texttt{insert} and~$\{\}$:  wenzelm@6580  611 \begin{eqnarray*}  wenzelm@6580  612  \{a, b, c\} & \equiv &  wenzelm@6580  613  \texttt{insert} \, a \, ({\tt insert} \, b \, ({\tt insert} \, c \, \{\}))  wenzelm@6580  614 \end{eqnarray*}  wenzelm@6580  615 wenzelm@9695  616 The set \hbox{\tt{\ttlbrace}$x$.\ $P[x]${\ttrbrace}} consists of all $x$ (of  wenzelm@9695  617 suitable type) that satisfy~$P[x]$, where $P[x]$ is a formula that may contain  wenzelm@9695  618 free occurrences of~$x$. This syntax expands to \cdx{Collect}$(\lambda x.  wenzelm@9695  619 P[x])$. It defines sets by absolute comprehension, which is impossible in~ZF;  wenzelm@9695  620 the type of~$x$ implicitly restricts the comprehension.  wenzelm@6580  621 wenzelm@6580  622 The set theory defines two {\bf bounded quantifiers}:  wenzelm@6580  623 \begin{eqnarray*}  wenzelm@6580  624  \forall x\in A. P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\  wenzelm@6580  625  \exists x\in A. P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x]  wenzelm@6580  626 \end{eqnarray*}  wenzelm@6580  627 The constants~\cdx{Ball} and~\cdx{Bex} are defined  wenzelm@6580  628 accordingly. Instead of \texttt{Ball $A$ $P$} and \texttt{Bex $A$ $P$} we may  wenzelm@6580  629 write\index{*"! symbol}\index{*"? symbol}  wenzelm@6580  630 \index{*ALL symbol}\index{*EX symbol}  wenzelm@6580  631 %  wenzelm@7245  632 \hbox{\tt ALL~$x$:$A$.\ $P[x]$} and \hbox{\tt EX~$x$:$A$.\ $P[x]$}. The  paulson@9212  633 original notation of Gordon's {\sc hol} system is supported as well:  paulson@9212  634 \texttt{!}\ and \texttt{?}.  wenzelm@6580  635 wenzelm@6580  636 Unions and intersections over sets, namely $\bigcup@{x\in A}B[x]$ and  wenzelm@6580  637 $\bigcap@{x\in A}B[x]$, are written  wenzelm@6580  638 \sdx{UN}~\hbox{\tt$x$:$A$.\ $B[x]$} and  wenzelm@6580  639 \sdx{INT}~\hbox{\tt$x$:$A$.\ $B[x]$}.  wenzelm@6580  640 wenzelm@6580  641 Unions and intersections over types, namely $\bigcup@x B[x]$ and $\bigcap@x  wenzelm@6580  642 B[x]$, are written \sdx{UN}~\hbox{\tt$x$.\ $B[x]$} and  wenzelm@6580  643 \sdx{INT}~\hbox{\tt$x$.\ $B[x]$}. They are equivalent to the previous  wenzelm@6580  644 union and intersection operators when $A$ is the universal set.  wenzelm@6580  645 wenzelm@6580  646 The operators $\bigcup A$ and $\bigcap A$ act upon sets of sets. They are  wenzelm@6580  647 not binders, but are equal to $\bigcup@{x\in A}x$ and $\bigcap@{x\in A}x$,  wenzelm@6580  648 respectively.  wenzelm@6580  649 wenzelm@6580  650 wenzelm@6580  651 wenzelm@6580  652 \begin{figure} \underscoreon  wenzelm@6580  653 \begin{ttbox}  wenzelm@6580  654 \tdx{mem_Collect_eq} (a : {\ttlbrace}x. P x{\ttrbrace}) = P a  wenzelm@6580  655 \tdx{Collect_mem_eq} {\ttlbrace}x. x:A{\ttrbrace} = A  wenzelm@6580  656 wenzelm@6580  657 \tdx{empty_def} {\ttlbrace}{\ttrbrace} == {\ttlbrace}x. False{\ttrbrace}  wenzelm@6580  658 \tdx{insert_def} insert a B == {\ttlbrace}x. x=a{\ttrbrace} Un B  wenzelm@6580  659 \tdx{Ball_def} Ball A P == ! x. x:A --> P x  wenzelm@6580  660 \tdx{Bex_def} Bex A P == ? x. x:A & P x  wenzelm@6580  661 \tdx{subset_def} A <= B == ! x:A. x:B  wenzelm@6580  662 \tdx{Un_def} A Un B == {\ttlbrace}x. x:A | x:B{\ttrbrace}  wenzelm@6580  663 \tdx{Int_def} A Int B == {\ttlbrace}x. x:A & x:B{\ttrbrace}  wenzelm@6580  664 \tdx{set_diff_def} A - B == {\ttlbrace}x. x:A & x~:B{\ttrbrace}  paulson@9212  665 \tdx{Compl_def} -A == {\ttlbrace}x. ~ x:A{\ttrbrace}  wenzelm@6580  666 \tdx{INTER_def} INTER A B == {\ttlbrace}y. ! x:A. y: B x{\ttrbrace}  wenzelm@6580  667 \tdx{UNION_def} UNION A B == {\ttlbrace}y. ? x:A. y: B x{\ttrbrace}  wenzelm@6580  668 \tdx{INTER1_def} INTER1 B == INTER {\ttlbrace}x. True{\ttrbrace} B  wenzelm@6580  669 \tdx{UNION1_def} UNION1 B == UNION {\ttlbrace}x. True{\ttrbrace} B  wenzelm@6580  670 \tdx{Inter_def} Inter S == (INT x:S. x)  wenzelm@6580  671 \tdx{Union_def} Union S == (UN x:S. x)  wenzelm@6580  672 \tdx{Pow_def} Pow A == {\ttlbrace}B. B <= A{\ttrbrace}  wenzelm@6580  673 \tdx{image_def} fA == {\ttlbrace}y. ? x:A. y=f x{\ttrbrace}  wenzelm@6580  674 \tdx{range_def} range f == {\ttlbrace}y. ? x. y=f x{\ttrbrace}  wenzelm@6580  675 \end{ttbox}  wenzelm@6580  676 \caption{Rules of the theory \texttt{Set}} \label{hol-set-rules}  wenzelm@6580  677 \end{figure}  wenzelm@6580  678 wenzelm@6580  679 wenzelm@6580  680 \begin{figure} \underscoreon  wenzelm@6580  681 \begin{ttbox}  wenzelm@6580  682 \tdx{CollectI} [| P a |] ==> a : {\ttlbrace}x. P x{\ttrbrace}  wenzelm@6580  683 \tdx{CollectD} [| a : {\ttlbrace}x. P x{\ttrbrace} |] ==> P a  wenzelm@6580  684 \tdx{CollectE} [| a : {\ttlbrace}x. P x{\ttrbrace}; P a ==> W |] ==> W  wenzelm@6580  685 wenzelm@6580  686 \tdx{ballI} [| !!x. x:A ==> P x |] ==> ! x:A. P x  wenzelm@6580  687 \tdx{bspec} [| ! x:A. P x; x:A |] ==> P x  wenzelm@6580  688 \tdx{ballE} [| ! x:A. P x; P x ==> Q; ~ x:A ==> Q |] ==> Q  wenzelm@6580  689 wenzelm@6580  690 \tdx{bexI} [| P x; x:A |] ==> ? x:A. P x  wenzelm@6580  691 \tdx{bexCI} [| ! x:A. ~ P x ==> P a; a:A |] ==> ? x:A. P x  wenzelm@6580  692 \tdx{bexE} [| ? x:A. P x; !!x. [| x:A; P x |] ==> Q |] ==> Q  wenzelm@6580  693 \subcaption{Comprehension and Bounded quantifiers}  wenzelm@6580  694 wenzelm@6580  695 \tdx{subsetI} (!!x. x:A ==> x:B) ==> A <= B  wenzelm@6580  696 \tdx{subsetD} [| A <= B; c:A |] ==> c:B  wenzelm@6580  697 \tdx{subsetCE} [| A <= B; ~ (c:A) ==> P; c:B ==> P |] ==> P  wenzelm@6580  698 wenzelm@6580  699 \tdx{subset_refl} A <= A  wenzelm@6580  700 \tdx{subset_trans} [| A<=B; B<=C |] ==> A<=C  wenzelm@6580  701 wenzelm@6580  702 \tdx{equalityI} [| A <= B; B <= A |] ==> A = B  wenzelm@6580  703 \tdx{equalityD1} A = B ==> A<=B  wenzelm@6580  704 \tdx{equalityD2} A = B ==> B<=A  wenzelm@6580  705 \tdx{equalityE} [| A = B; [| A<=B; B<=A |] ==> P |] ==> P  wenzelm@6580  706 wenzelm@6580  707 \tdx{equalityCE} [| A = B; [| c:A; c:B |] ==> P;  wenzelm@6580  708  [| ~ c:A; ~ c:B |] ==> P  wenzelm@6580  709  |] ==> P  wenzelm@6580  710 \subcaption{The subset and equality relations}  wenzelm@6580  711 \end{ttbox}  wenzelm@6580  712 \caption{Derived rules for set theory} \label{hol-set1}  wenzelm@6580  713 \end{figure}  wenzelm@6580  714 wenzelm@6580  715 wenzelm@6580  716 \begin{figure} \underscoreon  wenzelm@6580  717 \begin{ttbox}  wenzelm@6580  718 \tdx{emptyE} a : {\ttlbrace}{\ttrbrace} ==> P  wenzelm@6580  719 wenzelm@6580  720 \tdx{insertI1} a : insert a B  wenzelm@6580  721 \tdx{insertI2} a : B ==> a : insert b B  wenzelm@6580  722 \tdx{insertE} [| a : insert b A; a=b ==> P; a:A ==> P |] ==> P  wenzelm@6580  723 paulson@9212  724 \tdx{ComplI} [| c:A ==> False |] ==> c : -A  paulson@9212  725 \tdx{ComplD} [| c : -A |] ==> ~ c:A  wenzelm@6580  726 wenzelm@6580  727 \tdx{UnI1} c:A ==> c : A Un B  wenzelm@6580  728 \tdx{UnI2} c:B ==> c : A Un B  wenzelm@6580  729 \tdx{UnCI} (~c:B ==> c:A) ==> c : A Un B  wenzelm@6580  730 \tdx{UnE} [| c : A Un B; c:A ==> P; c:B ==> P |] ==> P  wenzelm@6580  731 wenzelm@6580  732 \tdx{IntI} [| c:A; c:B |] ==> c : A Int B  wenzelm@6580  733 \tdx{IntD1} c : A Int B ==> c:A  wenzelm@6580  734 \tdx{IntD2} c : A Int B ==> c:B  wenzelm@6580  735 \tdx{IntE} [| c : A Int B; [| c:A; c:B |] ==> P |] ==> P  wenzelm@6580  736 wenzelm@6580  737 \tdx{UN_I} [| a:A; b: B a |] ==> b: (UN x:A. B x)  wenzelm@6580  738 \tdx{UN_E} [| b: (UN x:A. B x); !!x.[| x:A; b:B x |] ==> R |] ==> R  wenzelm@6580  739 wenzelm@6580  740 \tdx{INT_I} (!!x. x:A ==> b: B x) ==> b : (INT x:A. B x)  wenzelm@6580  741 \tdx{INT_D} [| b: (INT x:A. B x); a:A |] ==> b: B a  wenzelm@6580  742 \tdx{INT_E} [| b: (INT x:A. B x); b: B a ==> R; ~ a:A ==> R |] ==> R  wenzelm@6580  743 wenzelm@6580  744 \tdx{UnionI} [| X:C; A:X |] ==> A : Union C  wenzelm@6580  745 \tdx{UnionE} [| A : Union C; !!X.[| A:X; X:C |] ==> R |] ==> R  wenzelm@6580  746 wenzelm@6580  747 \tdx{InterI} [| !!X. X:C ==> A:X |] ==> A : Inter C  wenzelm@6580  748 \tdx{InterD} [| A : Inter C; X:C |] ==> A:X  wenzelm@6580  749 \tdx{InterE} [| A : Inter C; A:X ==> R; ~ X:C ==> R |] ==> R  wenzelm@6580  750 wenzelm@6580  751 \tdx{PowI} A<=B ==> A: Pow B  wenzelm@6580  752 \tdx{PowD} A: Pow B ==> A<=B  wenzelm@6580  753 wenzelm@6580  754 \tdx{imageI} [| x:A |] ==> f x : fA  wenzelm@6580  755 \tdx{imageE} [| b : fA; !!x.[| b=f x; x:A |] ==> P |] ==> P  wenzelm@6580  756 wenzelm@6580  757 \tdx{rangeI} f x : range f  wenzelm@6580  758 \tdx{rangeE} [| b : range f; !!x.[| b=f x |] ==> P |] ==> P  wenzelm@6580  759 \end{ttbox}  wenzelm@6580  760 \caption{Further derived rules for set theory} \label{hol-set2}  wenzelm@6580  761 \end{figure}  wenzelm@6580  762 wenzelm@6580  763 wenzelm@6580  764 \subsection{Axioms and rules of set theory}  wenzelm@6580  765 Figure~\ref{hol-set-rules} presents the rules of theory \thydx{Set}. The  wenzelm@6580  766 axioms \tdx{mem_Collect_eq} and \tdx{Collect_mem_eq} assert  wenzelm@6580  767 that the functions \texttt{Collect} and \hbox{\tt op :} are isomorphisms. Of  wenzelm@6580  768 course, \hbox{\tt op :} also serves as the membership relation.  wenzelm@6580  769 wenzelm@6580  770 All the other axioms are definitions. They include the empty set, bounded  wenzelm@6580  771 quantifiers, unions, intersections, complements and the subset relation.  wenzelm@6580  772 They also include straightforward constructions on functions: image~({\tt})  wenzelm@6580  773 and \texttt{range}.  wenzelm@6580  774 wenzelm@6580  775 %The predicate \cdx{inj_on} is used for simulating type definitions.  wenzelm@6580  776 %The statement ${\tt inj_on}~f~A$ asserts that $f$ is injective on the  wenzelm@6580  777 %set~$A$, which specifies a subset of its domain type. In a type  wenzelm@6580  778 %definition, $f$ is the abstraction function and $A$ is the set of valid  wenzelm@6580  779 %representations; we should not expect $f$ to be injective outside of~$A$.  wenzelm@6580  780 wenzelm@6580  781 %\begin{figure} \underscoreon  wenzelm@6580  782 %\begin{ttbox}  wenzelm@6580  783 %\tdx{Inv_f_f} inj f ==> Inv f (f x) = x  wenzelm@6580  784 %\tdx{f_Inv_f} y : range f ==> f(Inv f y) = y  wenzelm@6580  785 %  wenzelm@6580  786 %\tdx{Inv_injective}  wenzelm@6580  787 % [| Inv f x=Inv f y; x: range f; y: range f |] ==> x=y  wenzelm@6580  788 %  wenzelm@6580  789 %  wenzelm@6580  790 %\tdx{monoI} [| !!A B. A <= B ==> f A <= f B |] ==> mono f  wenzelm@6580  791 %\tdx{monoD} [| mono f; A <= B |] ==> f A <= f B  wenzelm@6580  792 %  wenzelm@6580  793 %\tdx{injI} [| !! x y. f x = f y ==> x=y |] ==> inj f  wenzelm@6580  794 %\tdx{inj_inverseI} (!!x. g(f x) = x) ==> inj f  wenzelm@6580  795 %\tdx{injD} [| inj f; f x = f y |] ==> x=y  wenzelm@6580  796 %  wenzelm@6580  797 %\tdx{inj_onI} (!!x y. [| f x=f y; x:A; y:A |] ==> x=y) ==> inj_on f A  wenzelm@6580  798 %\tdx{inj_onD} [| inj_on f A; f x=f y; x:A; y:A |] ==> x=y  wenzelm@6580  799 %  wenzelm@6580  800 %\tdx{inj_on_inverseI}  wenzelm@6580  801 % (!!x. x:A ==> g(f x) = x) ==> inj_on f A  wenzelm@6580  802 %\tdx{inj_on_contraD}  wenzelm@6580  803 % [| inj_on f A; x~=y; x:A; y:A |] ==> ~ f x=f y  wenzelm@6580  804 %\end{ttbox}  wenzelm@6580  805 %\caption{Derived rules involving functions} \label{hol-fun}  wenzelm@6580  806 %\end{figure}  wenzelm@6580  807 wenzelm@6580  808 wenzelm@6580  809 \begin{figure} \underscoreon  wenzelm@6580  810 \begin{ttbox}  wenzelm@6580  811 \tdx{Union_upper} B:A ==> B <= Union A  wenzelm@6580  812 \tdx{Union_least} [| !!X. X:A ==> X<=C |] ==> Union A <= C  wenzelm@6580  813 wenzelm@6580  814 \tdx{Inter_lower} B:A ==> Inter A <= B  wenzelm@6580  815 \tdx{Inter_greatest} [| !!X. X:A ==> C<=X |] ==> C <= Inter A  wenzelm@6580  816 wenzelm@6580  817 \tdx{Un_upper1} A <= A Un B  wenzelm@6580  818 \tdx{Un_upper2} B <= A Un B  wenzelm@6580  819 \tdx{Un_least} [| A<=C; B<=C |] ==> A Un B <= C  wenzelm@6580  820 wenzelm@6580  821 \tdx{Int_lower1} A Int B <= A  wenzelm@6580  822 \tdx{Int_lower2} A Int B <= B  wenzelm@6580  823 \tdx{Int_greatest} [| C<=A; C<=B |] ==> C <= A Int B  wenzelm@6580  824 \end{ttbox}  wenzelm@6580  825 \caption{Derived rules involving subsets} \label{hol-subset}  wenzelm@6580  826 \end{figure}  wenzelm@6580  827 wenzelm@6580  828 wenzelm@6580  829 \begin{figure} \underscoreon \hfuzz=4pt%suppress "Overfull \hbox" message  wenzelm@6580  830 \begin{ttbox}  wenzelm@6580  831 \tdx{Int_absorb} A Int A = A  wenzelm@6580  832 \tdx{Int_commute} A Int B = B Int A  wenzelm@6580  833 \tdx{Int_assoc} (A Int B) Int C = A Int (B Int C)  wenzelm@6580  834 \tdx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C)  wenzelm@6580  835 wenzelm@6580  836 \tdx{Un_absorb} A Un A = A  wenzelm@6580  837 \tdx{Un_commute} A Un B = B Un A  wenzelm@6580  838 \tdx{Un_assoc} (A Un B) Un C = A Un (B Un C)  wenzelm@6580  839 \tdx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C)  wenzelm@6580  840 paulson@9212  841 \tdx{Compl_disjoint} A Int (-A) = {\ttlbrace}x. False{\ttrbrace}  paulson@9212  842 \tdx{Compl_partition} A Un (-A) = {\ttlbrace}x. True{\ttrbrace}  paulson@9212  843 \tdx{double_complement} -(-A) = A  paulson@9212  844 \tdx{Compl_Un} -(A Un B) = (-A) Int (-B)  paulson@9212  845 \tdx{Compl_Int} -(A Int B) = (-A) Un (-B)  wenzelm@6580  846 wenzelm@6580  847 \tdx{Union_Un_distrib} Union(A Un B) = (Union A) Un (Union B)  wenzelm@6580  848 \tdx{Int_Union} A Int (Union B) = (UN C:B. A Int C)  wenzelm@6580  849 wenzelm@6580  850 \tdx{Inter_Un_distrib} Inter(A Un B) = (Inter A) Int (Inter B)  wenzelm@6580  851 \tdx{Un_Inter} A Un (Inter B) = (INT C:B. A Un C)  kleing@14013  852 wenzelm@6580  853 \end{ttbox}  wenzelm@6580  854 \caption{Set equalities} \label{hol-equalities}  wenzelm@6580  855 \end{figure}  kleing@14013  856 %\tdx{Un_Union_image} (UN x:C.(A x) Un (B x)) = Union(AC) Un Union(BC)  kleing@14013  857 %\tdx{Int_Inter_image} (INT x:C.(A x) Int (B x)) = Inter(AC) Int Inter(BC)  wenzelm@6580  858 wenzelm@6580  859 Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules. Most are  wenzelm@9695  860 obvious and resemble rules of Isabelle's ZF set theory. Certain rules, such  wenzelm@9695  861 as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI}, are designed for classical  wenzelm@9695  862 reasoning; the rules \tdx{subsetD}, \tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are  wenzelm@9695  863 not strictly necessary but yield more natural proofs. Similarly,  wenzelm@9695  864 \tdx{equalityCE} supports classical reasoning about extensionality, after the  wenzelm@9695  865 fashion of \tdx{iffCE}. See the file \texttt{HOL/Set.ML} for proofs  wenzelm@9695  866 pertaining to set theory.  wenzelm@6580  867 wenzelm@6580  868 Figure~\ref{hol-subset} presents lattice properties of the subset relation.  wenzelm@6580  869 Unions form least upper bounds; non-empty intersections form greatest lower  wenzelm@6580  870 bounds. Reasoning directly about subsets often yields clearer proofs than  wenzelm@6580  871 reasoning about the membership relation. See the file \texttt{HOL/subset.ML}.  wenzelm@6580  872 wenzelm@6580  873 Figure~\ref{hol-equalities} presents many common set equalities. They  wenzelm@6580  874 include commutative, associative and distributive laws involving unions,  wenzelm@6580  875 intersections and complements. For a complete listing see the file {\tt  wenzelm@6580  876 HOL/equalities.ML}.  wenzelm@6580  877 wenzelm@6580  878 \begin{warn}  wenzelm@6580  879 \texttt{Blast_tac} proves many set-theoretic theorems automatically.  wenzelm@6580  880 Hence you seldom need to refer to the theorems above.  wenzelm@6580  881 \end{warn}  wenzelm@6580  882 wenzelm@6580  883 \begin{figure}  wenzelm@6580  884 \begin{center}  wenzelm@6580  885 \begin{tabular}{rrr}  wenzelm@6580  886  \it name &\it meta-type & \it description \\  wenzelm@6580  887  \cdx{inj}~~\cdx{surj}& $(\alpha\To\beta )\To bool$  wenzelm@6580  888  & injective/surjective \\  wenzelm@6580  889  \cdx{inj_on} & $[\alpha\To\beta ,\alpha\,set]\To bool$  wenzelm@6580  890  & injective over subset\\  wenzelm@6580  891  \cdx{inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & inverse function  wenzelm@6580  892 \end{tabular}  wenzelm@6580  893 \end{center}  wenzelm@6580  894 wenzelm@6580  895 \underscoreon  wenzelm@6580  896 \begin{ttbox}  wenzelm@6580  897 \tdx{inj_def} inj f == ! x y. f x=f y --> x=y  wenzelm@6580  898 \tdx{surj_def} surj f == ! y. ? x. y=f x  wenzelm@6580  899 \tdx{inj_on_def} inj_on f A == !x:A. !y:A. f x=f y --> x=y  wenzelm@6580  900 \tdx{inv_def} inv f == (\%y. @x. f(x)=y)  wenzelm@6580  901 \end{ttbox}  wenzelm@6580  902 \caption{Theory \thydx{Fun}} \label{fig:HOL:Fun}  wenzelm@6580  903 \end{figure}  wenzelm@6580  904 wenzelm@6580  905 \subsection{Properties of functions}\nopagebreak  wenzelm@6580  906 Figure~\ref{fig:HOL:Fun} presents a theory of simple properties of functions.  wenzelm@6580  907 Note that ${\tt inv}~f$ uses Hilbert's $\varepsilon$ to yield an inverse  wenzelm@6580  908 of~$f$. See the file \texttt{HOL/Fun.ML} for a complete listing of the derived  wenzelm@6580  909 rules. Reasoning about function composition (the operator~\sdx{o}) and the  wenzelm@6580  910 predicate~\cdx{surj} is done simply by expanding the definitions.  wenzelm@6580  911 wenzelm@6580  912 There is also a large collection of monotonicity theorems for constructions  wenzelm@6580  913 on sets in the file \texttt{HOL/mono.ML}.  wenzelm@6580  914 paulson@7283  915 wenzelm@6580  916 \section{Generic packages}  wenzelm@6580  917 \label{sec:HOL:generic-packages}  wenzelm@6580  918 wenzelm@9695  919 HOL instantiates most of Isabelle's generic packages, making available the  wenzelm@6580  920 simplifier and the classical reasoner.  wenzelm@6580  921 wenzelm@6580  922 \subsection{Simplification and substitution}  wenzelm@6580  923 wenzelm@6580  924 Simplification tactics tactics such as \texttt{Asm_simp_tac} and \texttt{Full_simp_tac} use the default simpset  wenzelm@6580  925 (\texttt{simpset()}), which works for most purposes. A quite minimal  wenzelm@6580  926 simplification set for higher-order logic is~\ttindexbold{HOL_ss};  wenzelm@6580  927 even more frugal is \ttindexbold{HOL_basic_ss}. Equality~($=$), which  wenzelm@6580  928 also expresses logical equivalence, may be used for rewriting. See  wenzelm@6580  929 the file \texttt{HOL/simpdata.ML} for a complete listing of the basic  wenzelm@6580  930 simplification rules.  wenzelm@6580  931 wenzelm@6580  932 See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%  wenzelm@6580  933 {Chaps.\ts\ref{substitution} and~\ref{simp-chap}} for details of substitution  wenzelm@6580  934 and simplification.  wenzelm@6580  935 wenzelm@6580  936 \begin{warn}\index{simplification!of conjunctions}%  wenzelm@6580  937  Reducing $a=b\conj P(a)$ to $a=b\conj P(b)$ is sometimes advantageous. The  wenzelm@6580  938  left part of a conjunction helps in simplifying the right part. This effect  wenzelm@6580  939  is not available by default: it can be slow. It can be obtained by  wenzelm@6580  940  including \ttindex{conj_cong} in a simpset, \verb$addcongs [conj_cong]$.  wenzelm@6580  941 \end{warn}  wenzelm@6580  942 nipkow@8604  943 \begin{warn}\index{simplification!of \texttt{if}}\label{if-simp}%  nipkow@8604  944  By default only the condition of an \ttindex{if} is simplified but not the  nipkow@8604  945  \texttt{then} and \texttt{else} parts. Of course the latter are simplified  nipkow@8604  946  once the condition simplifies to \texttt{True} or \texttt{False}. To ensure  nipkow@8604  947  full simplification of all parts of a conditional you must remove  nipkow@8604  948  \ttindex{if_weak_cong} from the simpset, \verb$delcongs [if_weak_cong]$.  nipkow@8604  949 \end{warn}  nipkow@8604  950 wenzelm@6580  951 If the simplifier cannot use a certain rewrite rule --- either because  wenzelm@6580  952 of nontermination or because its left-hand side is too flexible ---  wenzelm@6580  953 then you might try \texttt{stac}:  wenzelm@6580  954 \begin{ttdescription}  wenzelm@6580  955 \item[\ttindexbold{stac} $thm$ $i,$] where $thm$ is of the form $lhs = rhs$,  wenzelm@6580  956  replaces in subgoal $i$ instances of $lhs$ by corresponding instances of  wenzelm@6580  957  $rhs$. In case of multiple instances of $lhs$ in subgoal $i$, backtracking  wenzelm@6580  958  may be necessary to select the desired ones.  wenzelm@6580  959 wenzelm@6580  960 If $thm$ is a conditional equality, the instantiated condition becomes an  wenzelm@6580  961 additional (first) subgoal.  wenzelm@6580  962 \end{ttdescription}  wenzelm@6580  963 wenzelm@9695  964 HOL provides the tactic \ttindex{hyp_subst_tac}, which substitutes for an  wenzelm@9695  965 equality throughout a subgoal and its hypotheses. This tactic uses HOL's  wenzelm@9695  966 general substitution rule.  wenzelm@6580  967 wenzelm@6580  968 \subsubsection{Case splitting}  wenzelm@6580  969 \label{subsec:HOL:case:splitting}  wenzelm@6580  970 wenzelm@9695  971 HOL also provides convenient means for case splitting during rewriting. Goals  wenzelm@9695  972 containing a subterm of the form \texttt{if}~$b$~{\tt then\dots else\dots}  wenzelm@9695  973 often require a case distinction on $b$. This is expressed by the theorem  wenzelm@9695  974 \tdx{split_if}:  wenzelm@6580  975 $$ wenzelm@6580  976 \Var{P}(\mbox{\tt if}~\Var{b}~{\tt then}~\Var{x}~\mbox{\tt else}~\Var{y})~=~  oheimb@7490  977 ((\Var{b} \to \Var{P}(\Var{x})) \land (\lnot \Var{b} \to \Var{P}(\Var{y})))  wenzelm@6580  978 \eqno{(*)}  wenzelm@6580  979 $$  wenzelm@6580  980 For example, a simple instance of $(*)$ is  wenzelm@6580  981 $ wenzelm@6580  982 x \in (\mbox{\tt if}~x \in A~{\tt then}~A~\mbox{\tt else}~\{x\})~=~  wenzelm@6580  983 ((x \in A \to x \in A) \land (x \notin A \to x \in \{x\}))  wenzelm@6580  984 $  wenzelm@6580  985 Because $(*)$ is too general as a rewrite rule for the simplifier (the  wenzelm@6580  986 left-hand side is not a higher-order pattern in the sense of  wenzelm@6580  987 \iflabelundefined{chap:simplification}{the {\em Reference Manual\/}}%  wenzelm@6580  988 {Chap.\ts\ref{chap:simplification}}), there is a special infix function  wenzelm@6580  989 \ttindexbold{addsplits} of type \texttt{simpset * thm list -> simpset}  wenzelm@6580  990 (analogous to \texttt{addsimps}) that adds rules such as $(*)$ to a  wenzelm@6580  991 simpset, as in  wenzelm@6580  992 \begin{ttbox}  wenzelm@6580  993 by(simp_tac (simpset() addsplits [split_if]) 1);  wenzelm@6580  994 \end{ttbox}  wenzelm@6580  995 The effect is that after each round of simplification, one occurrence of  wenzelm@6580  996 \texttt{if} is split acording to \texttt{split_if}, until all occurences of  wenzelm@6580  997 \texttt{if} have been eliminated.  wenzelm@6580  998 wenzelm@6580  999 It turns out that using \texttt{split_if} is almost always the right thing to  wenzelm@6580  1000 do. Hence \texttt{split_if} is already included in the default simpset. If  wenzelm@6580  1001 you want to delete it from a simpset, use \ttindexbold{delsplits}, which is  wenzelm@6580  1002 the inverse of \texttt{addsplits}:  wenzelm@6580  1003 \begin{ttbox}  wenzelm@6580  1004 by(simp_tac (simpset() delsplits [split_if]) 1);  wenzelm@6580  1005 \end{ttbox}  wenzelm@6580  1006 wenzelm@6580  1007 In general, \texttt{addsplits} accepts rules of the form  wenzelm@6580  1008 $ wenzelm@6580  1009 \Var{P}(c~\Var{x@1}~\dots~\Var{x@n})~=~ rhs  wenzelm@6580  1010 $  wenzelm@6580  1011 where $c$ is a constant and $rhs$ is arbitrary. Note that $(*)$ is of the  wenzelm@6580  1012 right form because internally the left-hand side is  wenzelm@6580  1013 $\Var{P}(\mathtt{If}~\Var{b}~\Var{x}~~\Var{y})$. Important further examples  oheimb@7490  1014 are splitting rules for \texttt{case} expressions (see~{\S}\ref{subsec:list}  oheimb@7490  1015 and~{\S}\ref{subsec:datatype:basics}).  wenzelm@6580  1016 wenzelm@6580  1017 Analogous to \texttt{Addsimps} and \texttt{Delsimps}, there are also  wenzelm@6580  1018 imperative versions of \texttt{addsplits} and \texttt{delsplits}  wenzelm@6580  1019 \begin{ttbox}  wenzelm@6580  1020 \ttindexbold{Addsplits}: thm list -> unit  wenzelm@6580  1021 \ttindexbold{Delsplits}: thm list -> unit  wenzelm@6580  1022 \end{ttbox}  wenzelm@6580  1023 for adding splitting rules to, and deleting them from the current simpset.  wenzelm@6580  1024 wenzelm@6580  1025 \subsection{Classical reasoning}  wenzelm@6580  1026 wenzelm@9695  1027 HOL derives classical introduction rules for $\disj$ and~$\exists$, as well as  wenzelm@9695  1028 classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule; recall  wenzelm@9695  1029 Fig.\ts\ref{hol-lemmas2} above.  wenzelm@6580  1030 paulson@7283  1031 The classical reasoner is installed. Tactics such as \texttt{Blast_tac} and  paulson@7283  1032 {\tt Best_tac} refer to the default claset (\texttt{claset()}), which works  paulson@7283  1033 for most purposes. Named clasets include \ttindexbold{prop_cs}, which  paulson@7283  1034 includes the propositional rules, and \ttindexbold{HOL_cs}, which also  paulson@7283  1035 includes quantifier rules. See the file \texttt{HOL/cladata.ML} for lists of  paulson@7283  1036 the classical rules,  wenzelm@6580  1037 and \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%  wenzelm@6580  1038 {Chap.\ts\ref{chap:classical}} for more discussion of classical proof methods.  wenzelm@6580  1039 wenzelm@6580  1040 wenzelm@13012  1041 %FIXME outdated, both from the Isabelle and SVC perspective  wenzelm@13012  1042 % \section{Calling the decision procedure SVC}\label{sec:HOL:SVC}  wenzelm@13012  1043 wenzelm@13012  1044 % \index{SVC decision procedure|(}  wenzelm@13012  1045 wenzelm@13012  1046 % The Stanford Validity Checker (SVC) is a tool that can check the validity of  wenzelm@13012  1047 % certain types of formulae. If it is installed on your machine, then  wenzelm@13012  1048 % Isabelle/HOL can be configured to call it through the tactic  wenzelm@13012  1049 % \ttindex{svc_tac}. It is ideal for large tautologies and complex problems in  wenzelm@13012  1050 % linear arithmetic. Subexpressions that SVC cannot handle are automatically  wenzelm@13012  1051 % replaced by variables, so you can call the tactic on any subgoal. See the  wenzelm@13012  1052 % file \texttt{HOL/ex/svc_test.ML} for examples.  wenzelm@13012  1053 % \begin{ttbox}  wenzelm@13012  1054 % svc_tac : int -> tactic  wenzelm@13012  1055 % Svc.trace : bool ref \hfill{\bf initially false}  wenzelm@13012  1056 % \end{ttbox}  wenzelm@13012  1057 wenzelm@13012  1058 % \begin{ttdescription}  wenzelm@13012  1059 % \item[\ttindexbold{svc_tac} $i$] attempts to prove subgoal~$i$ by translating  wenzelm@13012  1060 % it into a formula recognized by~SVC\@. If it succeeds then the subgoal is  wenzelm@13012  1061 % removed. It fails if SVC is unable to prove the subgoal. It crashes with  wenzelm@13012  1062 % an error message if SVC appears not to be installed. Numeric variables may  wenzelm@13012  1063 % have types \texttt{nat}, \texttt{int} or \texttt{real}.  wenzelm@13012  1064 wenzelm@13012  1065 % \item[\ttindexbold{Svc.trace}] is a flag that, if set, causes \texttt{svc_tac}  wenzelm@13012  1066 % to trace its operations: abstraction of the subgoal, translation to SVC  wenzelm@13012  1067 % syntax, SVC's response.  wenzelm@13012  1068 % \end{ttdescription}  wenzelm@13012  1069 wenzelm@13012  1070 % Here is an example, with tracing turned on:  wenzelm@13012  1071 % \begin{ttbox}  wenzelm@13012  1072 % set Svc.trace;  wenzelm@13012  1073 % {\out val it : bool = true}  wenzelm@13012  1074 % Goal "(#3::nat)*a <= #2 + #4*b + #6*c & #11 <= #2*a + b + #2*c & \ttback  wenzelm@13012  1075 % \ttback a + #3*b <= #5 + #2*c --> #2 + #3*b <= #2*a + #6*c";  wenzelm@13012  1076 wenzelm@13012  1077 % by (svc_tac 1);  wenzelm@13012  1078 % {\out Subgoal abstracted to}  wenzelm@13012  1079 % {\out #3 * a <= #2 + #4 * b + #6 * c &}  wenzelm@13012  1080 % {\out #11 <= #2 * a + b + #2 * c & a + #3 * b <= #5 + #2 * c -->}  wenzelm@13012  1081 % {\out #2 + #3 * b <= #2 * a + #6 * c}  wenzelm@13012  1082 % {\out Calling SVC:}  wenzelm@13012  1083 % {\out (=> (<= 0 (F_c) ) (=> (<= 0 (F_b) ) (=> (<= 0 (F_a) )}  wenzelm@13012  1084 % {\out (=> (AND (<= {* 3 (F_a) } {+ {+ 2 {* 4 (F_b) } } }  wenzelm@13012  1085 % {\out {* 6 (F_c) } } ) (AND (<= 11 {+ {+ {* 2 (F_a) } (F_b) }}  wenzelm@13012  1086 % {\out {* 2 (F_c) } } ) (<= {+ (F_a) {* 3 (F_b) } } {+ 5 }  wenzelm@13012  1087 % {\out {* 2 (F_c) } } ) ) ) (< {+ 2 {* 3 (F_b) } } {+ 1 {+ }  wenzelm@13012  1088 % {\out {* 2 (F_a) } {* 6 (F_c) } } } ) ) ) ) ) }  wenzelm@13012  1089 % {\out SVC Returns:}  wenzelm@13012  1090 % {\out VALID}  wenzelm@13012  1091 % {\out Level 1}  wenzelm@13012  1092 % {\out #3 * a <= #2 + #4 * b + #6 * c &}  wenzelm@13012  1093 % {\out #11 <= #2 * a + b + #2 * c & a + #3 * b <= #5 + #2 * c -->}  wenzelm@13012  1094 % {\out #2 + #3 * b <= #2 * a + #6 * c}  wenzelm@13012  1095 % {\out No subgoals!}  wenzelm@13012  1096 % \end{ttbox}  wenzelm@13012  1097 wenzelm@13012  1098 wenzelm@13012  1099 % \begin{warn}  wenzelm@13012  1100 % Calling \ttindex{svc_tac} entails an above-average risk of  wenzelm@13012  1101 % unsoundness. Isabelle does not check SVC's result independently. Moreover,  wenzelm@13012  1102 % the tactic translates the submitted formula using code that lies outside  wenzelm@13012  1103 % Isabelle's inference core. Theorems that depend upon results proved using SVC  wenzelm@13012  1104 % (and other oracles) are displayed with the annotation \texttt{[!]} attached.  wenzelm@13012  1105 % You can also use \texttt{\#der (rep_thm $th$)} to examine the proof object of  wenzelm@13012  1106 % theorem~$th$, as described in the \emph{Reference Manual}.  wenzelm@13012  1107 % \end{warn}  wenzelm@13012  1108 wenzelm@13012  1109 % To start, first download SVC from the Internet at URL  wenzelm@13012  1110 % \begin{ttbox}  wenzelm@13012  1111 % http://agamemnon.stanford.edu/~levitt/vc/index.html  wenzelm@13012  1112 % \end{ttbox}  wenzelm@13012  1113 % and install it using the instructions supplied. SVC requires two environment  wenzelm@13012  1114 % variables:  wenzelm@13012  1115 % \begin{ttdescription}  wenzelm@13012  1116 % \item[\ttindexbold{SVC_HOME}] is an absolute pathname to the SVC  wenzelm@13012  1117 % distribution directory.  paulson@7283  1118   wenzelm@13012  1119 % \item[\ttindexbold{SVC_MACHINE}] identifies the type of computer and  wenzelm@13012  1120 % operating system.  wenzelm@13012  1121 % \end{ttdescription}  wenzelm@13012  1122 % You can set these environment variables either using the Unix shell or through  wenzelm@13012  1123 % an Isabelle \texttt{settings} file. Isabelle assumes SVC to be installed if  wenzelm@13012  1124 % \texttt{SVC_HOME} is defined.  wenzelm@13012  1125 wenzelm@13012  1126 % \paragraph*{Acknowledgement.} This interface uses code supplied by S{\o}ren  wenzelm@13012  1127 % Heilmann.  wenzelm@13012  1128 wenzelm@13012  1129 wenzelm@13012  1130 % \index{SVC decision procedure|)}  paulson@7283  1131 paulson@7283  1132 paulson@7283  1133 paulson@7283  1134 wenzelm@6580  1135 \section{Types}\label{sec:HOL:Types}  wenzelm@9695  1136 This section describes HOL's basic predefined types ($\alpha \times \beta$,  wenzelm@9695  1137 $\alpha + \beta$, $nat$ and $\alpha \; list$) and ways for introducing new  wenzelm@9695  1138 types in general. The most important type construction, the  wenzelm@9695  1139 \texttt{datatype}, is treated separately in {\S}\ref{sec:HOL:datatype}.  wenzelm@6580  1140 wenzelm@6580  1141 wenzelm@6580  1142 \subsection{Product and sum types}\index{*"* type}\index{*"+ type}  wenzelm@6580  1143 \label{subsec:prod-sum}  wenzelm@6580  1144 wenzelm@6580  1145 \begin{figure}[htbp]  wenzelm@6580  1146 \begin{constants}  wenzelm@6580  1147  \it symbol & \it meta-type & & \it description \\  wenzelm@6580  1148  \cdx{Pair} & $[\alpha,\beta]\To \alpha\times\beta$  wenzelm@6580  1149  & & ordered pairs $(a,b)$ \\  wenzelm@6580  1150  \cdx{fst} & $\alpha\times\beta \To \alpha$ & & first projection\\  wenzelm@6580  1151  \cdx{snd} & $\alpha\times\beta \To \beta$ & & second projection\\  wenzelm@6580  1152  \cdx{split} & $[[\alpha,\beta]\To\gamma, \alpha\times\beta] \To \gamma$  wenzelm@6580  1153  & & generalized projection\\  wenzelm@6580  1154  \cdx{Sigma} &  wenzelm@6580  1155  $[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ &  wenzelm@6580  1156  & general sum of sets  wenzelm@6580  1157 \end{constants}  wenzelm@6580  1158 %\tdx{fst_def} fst p == @a. ? b. p = (a,b)  wenzelm@6580  1159 %\tdx{snd_def} snd p == @b. ? a. p = (a,b)  wenzelm@6580  1160 %\tdx{split_def} split c p == c (fst p) (snd p)  kleing@14013  1161 \begin{ttbox}\makeatletter  wenzelm@6580  1162 \tdx{Sigma_def} Sigma A B == UN x:A. UN y:B x. {\ttlbrace}(x,y){\ttrbrace}  wenzelm@6580  1163 wenzelm@6580  1164 \tdx{Pair_eq} ((a,b) = (a',b')) = (a=a' & b=b')  wenzelm@6580  1165 \tdx{Pair_inject} [| (a, b) = (a',b'); [| a=a'; b=b' |] ==> R |] ==> R  wenzelm@6580  1166 \tdx{PairE} [| !!x y. p = (x,y) ==> Q |] ==> Q  wenzelm@6580  1167 wenzelm@6580  1168 \tdx{fst_conv} fst (a,b) = a  wenzelm@6580  1169 \tdx{snd_conv} snd (a,b) = b  wenzelm@6580  1170 \tdx{surjective_pairing} p = (fst p,snd p)  wenzelm@6580  1171 wenzelm@6580  1172 \tdx{split} split c (a,b) = c a b  wenzelm@6580  1173 \tdx{split_split} R(split c p) = (! x y. p = (x,y) --> R(c x y))  wenzelm@6580  1174 wenzelm@6580  1175 \tdx{SigmaI} [| a:A; b:B a |] ==> (a,b) : Sigma A B  paulson@9212  1176 paulson@9212  1177 \tdx{SigmaE} [| c:Sigma A B; !!x y.[| x:A; y:B x; c=(x,y) |] ==> P  paulson@9212  1178  |] ==> P  wenzelm@6580  1179 \end{ttbox}  wenzelm@6580  1180 \caption{Type $\alpha\times\beta$}\label{hol-prod}  wenzelm@6580  1181 \end{figure}  wenzelm@6580  1182 wenzelm@6580  1183 Theory \thydx{Prod} (Fig.\ts\ref{hol-prod}) defines the product type  wenzelm@6580  1184 $\alpha\times\beta$, with the ordered pair syntax $(a, b)$. General  wenzelm@6580  1185 tuples are simulated by pairs nested to the right:  wenzelm@6580  1186 \begin{center}  wenzelm@6580  1187 \begin{tabular}{c|c}  wenzelm@6580  1188 external & internal \\  wenzelm@6580  1189 \hline  wenzelm@6580  1190 $\tau@1 \times \dots \times \tau@n$ & $\tau@1 \times (\dots (\tau@{n-1} \times \tau@n)\dots)$ \\  wenzelm@6580  1191 \hline  wenzelm@6580  1192 $(t@1,\dots,t@n)$ & $(t@1,(\dots,(t@{n-1},t@n)\dots)$ \\  wenzelm@6580  1193 \end{tabular}  wenzelm@6580  1194 \end{center}  wenzelm@6580  1195 In addition, it is possible to use tuples  wenzelm@6580  1196 as patterns in abstractions:  wenzelm@6580  1197 \begin{center}  wenzelm@6580  1198 {\tt\%($x$,$y$). $t$} \quad stands for\quad \texttt{split(\%$x$\thinspace$y$.\ $t$)}  wenzelm@6580  1199 \end{center}  wenzelm@6580  1200 Nested patterns are also supported. They are translated stepwise:  paulson@9212  1201 \begin{eqnarray*}  paulson@9212  1202 \hbox{\tt\%($x$,$y$,$z$).\ $t$}  paulson@9212  1203  & \leadsto & \hbox{\tt\%($x$,($y$,$z$)).\ $t$} \\  paulson@9212  1204  & \leadsto & \hbox{\tt split(\%$x$.\%($y$,$z$).\ $t$)}\\  paulson@9212  1205  & \leadsto & \hbox{\tt split(\%$x$.\ split(\%$y$ $z$.\ $t$))}  paulson@9212  1206 \end{eqnarray*}  paulson@9212  1207 The reverse translation is performed upon printing.  wenzelm@6580  1208 \begin{warn}  wenzelm@6580  1209  The translation between patterns and \texttt{split} is performed automatically  wenzelm@6580  1210  by the parser and printer. Thus the internal and external form of a term  wenzelm@6580  1211  may differ, which can affects proofs. For example the term {\tt  wenzelm@6580  1212  (\%(x,y).(y,x))(a,b)} requires the theorem \texttt{split} (which is in the  wenzelm@6580  1213  default simpset) to rewrite to {\tt(b,a)}.  wenzelm@6580  1214 \end{warn}  wenzelm@6580  1215 In addition to explicit $\lambda$-abstractions, patterns can be used in any  wenzelm@6580  1216 variable binding construct which is internally described by a  wenzelm@6580  1217 $\lambda$-abstraction. Some important examples are  wenzelm@6580  1218 \begin{description}  wenzelm@6580  1219 \item[Let:] \texttt{let {\it pattern} = $t$ in $u$}  wenzelm@10109  1220 \item[Quantifiers:] \texttt{ALL~{\it pattern}:$A$.~$P$}  wenzelm@10109  1221 \item[Choice:] {\underscoreon \tt SOME~{\it pattern}.~$P$}  wenzelm@6580  1222 \item[Set operations:] \texttt{UN~{\it pattern}:$A$.~$B$}  wenzelm@10109  1223 \item[Sets:] \texttt{{\ttlbrace}{\it pattern}.~$P${\ttrbrace}}  wenzelm@6580  1224 \end{description}  wenzelm@6580  1225 wenzelm@6580  1226 There is a simple tactic which supports reasoning about patterns:  wenzelm@6580  1227 \begin{ttdescription}  wenzelm@6580  1228 \item[\ttindexbold{split_all_tac} $i$] replaces in subgoal $i$ all  wenzelm@6580  1229  {\tt!!}-quantified variables of product type by individual variables for  wenzelm@6580  1230  each component. A simple example:  wenzelm@6580  1231 \begin{ttbox}  wenzelm@6580  1232 {\out 1. !!p. (\%(x,y,z). (x, y, z)) p = p}  wenzelm@6580  1233 by(split_all_tac 1);  wenzelm@6580  1234 {\out 1. !!x xa ya. (\%(x,y,z). (x, y, z)) (x, xa, ya) = (x, xa, ya)}  wenzelm@6580  1235 \end{ttbox}  wenzelm@6580  1236 \end{ttdescription}  wenzelm@6580  1237 wenzelm@6580  1238 Theory \texttt{Prod} also introduces the degenerate product type \texttt{unit}  wenzelm@6580  1239 which contains only a single element named {\tt()} with the property  wenzelm@6580  1240 \begin{ttbox}  wenzelm@6580  1241 \tdx{unit_eq} u = ()  wenzelm@6580  1242 \end{ttbox}  wenzelm@6580  1243 \bigskip  wenzelm@6580  1244 wenzelm@6580  1245 Theory \thydx{Sum} (Fig.~\ref{hol-sum}) defines the sum type $\alpha+\beta$  wenzelm@6580  1246 which associates to the right and has a lower priority than $*$: $\tau@1 +  wenzelm@6580  1247 \tau@2 + \tau@3*\tau@4$ means $\tau@1 + (\tau@2 + (\tau@3*\tau@4))$.  wenzelm@6580  1248 wenzelm@6580  1249 The definition of products and sums in terms of existing types is not  wenzelm@6580  1250 shown. The constructions are fairly standard and can be found in the  berghofe@7325  1251 respective theory files. Although the sum and product types are  berghofe@7325  1252 constructed manually for foundational reasons, they are represented as  oheimb@7490  1253 actual datatypes later (see {\S}\ref{subsec:datatype:rep_datatype}).  berghofe@7325  1254 Therefore, the theory \texttt{Datatype} should be used instead of  berghofe@7325  1255 \texttt{Sum} or \texttt{Prod}.  wenzelm@6580  1256 wenzelm@6580  1257 \begin{figure}  wenzelm@6580  1258 \begin{constants}  wenzelm@6580  1259  \it symbol & \it meta-type & & \it description \\  wenzelm@6580  1260  \cdx{Inl} & $\alpha \To \alpha+\beta$ & & first injection\\  wenzelm@6580  1261  \cdx{Inr} & $\beta \To \alpha+\beta$ & & second injection\\  wenzelm@6580  1262  \cdx{sum_case} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$  wenzelm@6580  1263  & & conditional  wenzelm@6580  1264 \end{constants}  wenzelm@6580  1265 \begin{ttbox}\makeatletter  wenzelm@6580  1266 \tdx{Inl_not_Inr} Inl a ~= Inr b  wenzelm@6580  1267 wenzelm@6580  1268 \tdx{inj_Inl} inj Inl  wenzelm@6580  1269 \tdx{inj_Inr} inj Inr  wenzelm@6580  1270 wenzelm@6580  1271 \tdx{sumE} [| !!x. P(Inl x); !!y. P(Inr y) |] ==> P s  wenzelm@6580  1272 wenzelm@6580  1273 \tdx{sum_case_Inl} sum_case f g (Inl x) = f x  wenzelm@6580  1274 \tdx{sum_case_Inr} sum_case f g (Inr x) = g x  wenzelm@6580  1275 wenzelm@6580  1276 \tdx{surjective_sum} sum_case (\%x. f(Inl x)) (\%y. f(Inr y)) s = f s  berghofe@7325  1277 \tdx{sum.split_case} R(sum_case f g s) = ((! x. s = Inl(x) --> R(f(x))) &  wenzelm@6580  1278  (! y. s = Inr(y) --> R(g(y))))  wenzelm@6580  1279 \end{ttbox}  wenzelm@6580  1280 \caption{Type $\alpha+\beta$}\label{hol-sum}  wenzelm@6580  1281 \end{figure}  wenzelm@6580  1282 wenzelm@6580  1283 \begin{figure}  wenzelm@6580  1284 \index{*"< symbol}  wenzelm@6580  1285 \index{*"* symbol}  wenzelm@6580  1286 \index{*div symbol}  wenzelm@6580  1287 \index{*mod symbol}  paulson@9212  1288 \index{*dvd symbol}  wenzelm@6580  1289 \index{*"+ symbol}  wenzelm@6580  1290 \index{*"- symbol}  wenzelm@6580  1291 \begin{constants}  wenzelm@6580  1292  \it symbol & \it meta-type & \it priority & \it description \\  paulson@9212  1293  \cdx{0} & $\alpha$ & & zero \\  wenzelm@6580  1294  \cdx{Suc} & $nat \To nat$ & & successor function\\  paulson@9212  1295  \tt * & $[\alpha,\alpha]\To \alpha$ & Left 70 & multiplication \\  paulson@9212  1296  \tt div & $[\alpha,\alpha]\To \alpha$ & Left 70 & division\\  paulson@9212  1297  \tt mod & $[\alpha,\alpha]\To \alpha$ & Left 70 & modulus\\  paulson@9212  1298  \tt dvd & $[\alpha,\alpha]\To bool$ & Left 70 & divides'' relation\\  paulson@9212  1299  \tt + & $[\alpha,\alpha]\To \alpha$ & Left 65 & addition\\  paulson@9212  1300  \tt - & $[\alpha,\alpha]\To \alpha$ & Left 65 & subtraction  wenzelm@6580  1301 \end{constants}  wenzelm@6580  1302 \subcaption{Constants and infixes}  wenzelm@6580  1303 wenzelm@6580  1304 \begin{ttbox}\makeatother  wenzelm@6580  1305 \tdx{nat_induct} [| P 0; !!n. P n ==> P(Suc n) |] ==> P n  wenzelm@6580  1306 wenzelm@6580  1307 \tdx{Suc_not_Zero} Suc m ~= 0  wenzelm@6580  1308 \tdx{inj_Suc} inj Suc  wenzelm@6580  1309 \tdx{n_not_Suc_n} n~=Suc n  wenzelm@6580  1310 \subcaption{Basic properties}  wenzelm@6580  1311 \end{ttbox}  wenzelm@6580  1312 \caption{The type of natural numbers, \tydx{nat}} \label{hol-nat1}  wenzelm@6580  1313 \end{figure}  wenzelm@6580  1314 wenzelm@6580  1315 wenzelm@6580  1316 \begin{figure}  wenzelm@6580  1317 \begin{ttbox}\makeatother  wenzelm@6580  1318  0+n = n  wenzelm@6580  1319  (Suc m)+n = Suc(m+n)  wenzelm@6580  1320 wenzelm@6580  1321  m-0 = m  wenzelm@6580  1322  0-n = n  wenzelm@6580  1323  Suc(m)-Suc(n) = m-n  wenzelm@6580  1324 wenzelm@6580  1325  0*n = 0  wenzelm@6580  1326  Suc(m)*n = n + m*n  wenzelm@6580  1327 wenzelm@6580  1328 \tdx{mod_less} m m mod n = m  wenzelm@6580  1329 \tdx{mod_geq} [| 0 m mod n = (m-n) mod n  wenzelm@6580  1330 wenzelm@6580  1331 \tdx{div_less} m m div n = 0  wenzelm@6580  1332 \tdx{div_geq} [| 0 m div n = Suc((m-n) div n)  wenzelm@6580  1333 \end{ttbox}  wenzelm@6580  1334 \caption{Recursion equations for the arithmetic operators} \label{hol-nat2}  wenzelm@6580  1335 \end{figure}  wenzelm@6580  1336 wenzelm@6580  1337 \subsection{The type of natural numbers, \textit{nat}}  wenzelm@6580  1338 \index{nat@{\textit{nat}} type|(}  wenzelm@6580  1339 paulson@15455  1340 The theory \thydx{Nat} defines the natural numbers in a roundabout but  wenzelm@6580  1341 traditional way. The axiom of infinity postulates a type~\tydx{ind} of  wenzelm@6580  1342 individuals, which is non-empty and closed under an injective operation. The  wenzelm@6580  1343 natural numbers are inductively generated by choosing an arbitrary individual  wenzelm@6580  1344 for~0 and using the injective operation to take successors. This is a least  paulson@15455  1345 fixedpoint construction.  wenzelm@6580  1346 paulson@9212  1347 Type~\tydx{nat} is an instance of class~\cldx{ord}, which makes the overloaded  paulson@9212  1348 functions of this class (especially \cdx{<} and \cdx{<=}, but also \cdx{min},  paulson@15455  1349 \cdx{max} and \cdx{LEAST}) available on \tydx{nat}. Theory \thydx{Nat}  paulson@15455  1350 also shows that {\tt<=} is a linear order, so \tydx{nat} is  paulson@9212  1351 also an instance of class \cldx{linorder}.  wenzelm@6580  1352 paulson@15455  1353 Theory \thydx{NatArith} develops arithmetic on the natural numbers. It defines  wenzelm@6580  1354 addition, multiplication and subtraction. Theory \thydx{Divides} defines  wenzelm@6580  1355 division, remainder and the divides'' relation. The numerous theorems  wenzelm@6580  1356 proved include commutative, associative, distributive, identity and  wenzelm@6580  1357 cancellation laws. See Figs.\ts\ref{hol-nat1} and~\ref{hol-nat2}. The  wenzelm@6580  1358 recursion equations for the operators \texttt{+}, \texttt{-} and \texttt{*} on  wenzelm@6580  1359 \texttt{nat} are part of the default simpset.  wenzelm@6580  1360 wenzelm@6580  1361 Functions on \tydx{nat} can be defined by primitive or well-founded recursion;  oheimb@7490  1362 see {\S}\ref{sec:HOL:recursive}. A simple example is addition.  wenzelm@6580  1363 Here, \texttt{op +} is the name of the infix operator~\texttt{+}, following  wenzelm@6580  1364 the standard convention.  wenzelm@6580  1365 \begin{ttbox}  wenzelm@6580  1366 \sdx{primrec}  wenzelm@6580  1367  "0 + n = n"  wenzelm@6580  1368  "Suc m + n = Suc (m + n)"  wenzelm@6580  1369 \end{ttbox}  wenzelm@6580  1370 There is also a \sdx{case}-construct  wenzelm@6580  1371 of the form  wenzelm@6580  1372 \begin{ttbox}  wenzelm@6580  1373 case $$e$$ of 0 => $$a$$ | Suc $$m$$ => $$b$$  wenzelm@6580  1374 \end{ttbox}  wenzelm@6580  1375 Note that Isabelle insists on precisely this format; you may not even change  wenzelm@6580  1376 the order of the two cases.  wenzelm@6580  1377 Both \texttt{primrec} and \texttt{case} are realized by a recursion operator  berghofe@7325  1378 \cdx{nat_rec}, which is available because \textit{nat} is represented as  oheimb@7490  1379 a datatype (see {\S}\ref{subsec:datatype:rep_datatype}).  wenzelm@6580  1380 wenzelm@6580  1381 %The predecessor relation, \cdx{pred_nat}, is shown to be well-founded.  wenzelm@6580  1382 %Recursion along this relation resembles primitive recursion, but is  wenzelm@6580  1383 %stronger because we are in higher-order logic; using primitive recursion to  wenzelm@6580  1384 %define a higher-order function, we can easily Ackermann's function, which  wenzelm@6580  1385 %is not primitive recursive \cite[page~104]{thompson91}.  wenzelm@6580  1386 %The transitive closure of \cdx{pred_nat} is~$<$. Many functions on the  wenzelm@6580  1387 %natural numbers are most easily expressed using recursion along~$<$.  wenzelm@6580  1388 wenzelm@6580  1389 Tactic {\tt\ttindex{induct_tac} "$n$" $i$} performs induction on variable~$n$  wenzelm@6580  1390 in subgoal~$i$ using theorem \texttt{nat_induct}. There is also the derived  wenzelm@6580  1391 theorem \tdx{less_induct}:  wenzelm@6580  1392 \begin{ttbox}  wenzelm@6580  1393 [| !!n. [| ! m. m P m |] ==> P n |] ==> P n  wenzelm@6580  1394 \end{ttbox}  wenzelm@6580  1395 wenzelm@6580  1396 paulson@9212  1397 \subsection{Numerical types and numerical reasoning}  paulson@9212  1398 wenzelm@9695  1399 The integers (type \tdx{int}) are also available in HOL, and the reals (type  kleing@14024  1400 \tdx{real}) are available in the logic image \texttt{HOL-Complex}. They support  paulson@9212  1401 the expected operations of addition (\texttt{+}), subtraction (\texttt{-}) and  paulson@9212  1402 multiplication (\texttt{*}), and much else. Type \tdx{int} provides the  paulson@9212  1403 \texttt{div} and \texttt{mod} operators, while type \tdx{real} provides real  paulson@9212  1404 division and other operations. Both types belong to class \cldx{linorder}, so  paulson@9212  1405 they inherit the relational operators and all the usual properties of linear  paulson@9212  1406 orderings. For full details, please survey the theories in subdirectories  kleing@14024  1407 \texttt{Integ}, \texttt{Real}, and \texttt{Complex}.  paulson@9212  1408 wenzelm@13012  1409 All three numeric types admit numerals of the form \texttt{$sd\ldots d$},  paulson@9212  1410 where $s$ is an optional minus sign and $d\ldots d$ is a string of digits.  paulson@9212  1411 Numerals are represented internally by a datatype for binary notation, which  paulson@9212  1412 allows numerical calculations to be performed by rewriting. For example, the  wenzelm@13012  1413 integer division of \texttt{54342339} by \texttt{3452} takes about five  paulson@9212  1414 seconds. By default, the simplifier cancels like terms on the opposite sites  paulson@9212  1415 of relational operators (reducing \texttt{z+x [] | Suc(m) => x # take m xs)  wenzelm@6580  1553 wenzelm@6580  1554 drop n [] = []  wenzelm@6580  1555 drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)  wenzelm@6580  1556 wenzelm@6580  1557 takeWhile P [] = []  wenzelm@6580  1558 takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])  wenzelm@6580  1559 wenzelm@6580  1560 dropWhile P [] = []  wenzelm@6580  1561 dropWhile P (x#xs) = (if P x then dropWhile P xs else xs)  wenzelm@6580  1562 \end{ttbox}  paulson@9212  1563 \caption{Further list processing functions}  paulson@9212  1564 \label{fig:HOL:list-simps2}  wenzelm@6580  1565 \end{figure}  wenzelm@6580  1566 wenzelm@6580  1567 wenzelm@6580  1568 \subsection{The type constructor for lists, \textit{list}}  wenzelm@6580  1569 \label{subsec:list}  wenzelm@6580  1570 \index{list@{\textit{list}} type|(}  wenzelm@6580  1571 wenzelm@6580  1572 Figure~\ref{hol-list} presents the theory \thydx{List}: the basic list  wenzelm@6580  1573 operations with their types and syntax. Type $\alpha \; list$ is  wenzelm@6580  1574 defined as a \texttt{datatype} with the constructors {\tt[]} and {\tt\#}.  wenzelm@6580  1575 As a result the generic structural induction and case analysis tactics  nipkow@8424  1576 \texttt{induct\_tac} and \texttt{cases\_tac} also become available for  wenzelm@6580  1577 lists. A \sdx{case} construct of the form  wenzelm@6580  1578 \begin{center}\tt  wenzelm@6580  1579 case $e$ of [] => $a$ | $$x$$\#$$xs$$ => b  wenzelm@6580  1580 \end{center}  oheimb@7490  1581 is defined by translation. For details see~{\S}\ref{sec:HOL:datatype}. There  wenzelm@6580  1582 is also a case splitting rule \tdx{split_list_case}  wenzelm@6580  1583 $ wenzelm@6580  1584 \begin{array}{l}  wenzelm@6580  1585 P(\mathtt{case}~e~\mathtt{of}~\texttt{[] =>}~a ~\texttt{|}~  wenzelm@6580  1586  x\texttt{\#}xs~\texttt{=>}~f~x~xs) ~= \\  wenzelm@6580  1587 ((e = \texttt{[]} \to P(a)) \land  wenzelm@6580  1588  (\forall x~ xs. e = x\texttt{\#}xs \to P(f~x~xs)))  wenzelm@6580  1589 \end{array}  wenzelm@6580  1590 $  wenzelm@6580  1591 which can be fed to \ttindex{addsplits} just like  oheimb@7490  1592 \texttt{split_if} (see~{\S}\ref{subsec:HOL:case:splitting}).  wenzelm@6580  1593 wenzelm@6580  1594 \texttt{List} provides a basic library of list processing functions defined by  oheimb@7490  1595 primitive recursion (see~{\S}\ref{sec:HOL:primrec}). The recursion equations  paulson@9212  1596 are shown in Figs.\ts\ref{fig:HOL:list-simps} and~\ref{fig:HOL:list-simps2}.  wenzelm@6580  1597 wenzelm@6580  1598 \index{list@{\textit{list}} type|)}  wenzelm@6580  1599 wenzelm@6580  1600 wenzelm@6580  1601 \subsection{Introducing new types} \label{sec:typedef}  wenzelm@6580  1602 wenzelm@9695  1603 The HOL-methodology dictates that all extensions to a theory should be  wenzelm@9695  1604 \textbf{definitional}. The type definition mechanism that meets this  wenzelm@9695  1605 criterion is \ttindex{typedef}. Note that \emph{type synonyms}, which are  wenzelm@9695  1606 inherited from Pure and described elsewhere, are just syntactic abbreviations  wenzelm@9695  1607 that have no logical meaning.  wenzelm@6580  1608 wenzelm@6580  1609 \begin{warn}  wenzelm@9695  1610  Types in HOL must be non-empty; otherwise the quantifier rules would be  oheimb@7490  1611  unsound, because $\exists x. x=x$ is a theorem \cite[{\S}7]{paulson-COLOG}.  wenzelm@6580  1612 \end{warn}  wenzelm@6580  1613 A \bfindex{type definition} identifies the new type with a subset of  wenzelm@6580  1614 an existing type. More precisely, the new type is defined by  wenzelm@6580  1615 exhibiting an existing type~$\tau$, a set~$A::\tau\,set$, and a  wenzelm@6580  1616 theorem of the form $x:A$. Thus~$A$ is a non-empty subset of~$\tau$,  wenzelm@6580  1617 and the new type denotes this subset. New functions are defined that  wenzelm@6580  1618 establish an isomorphism between the new type and the subset. If  wenzelm@6580  1619 type~$\tau$ involves type variables $\alpha@1$, \ldots, $\alpha@n$,  wenzelm@6580  1620 then the type definition creates a type constructor  wenzelm@6580  1621 $(\alpha@1,\ldots,\alpha@n)ty$ rather than a particular type.  wenzelm@6580  1622 wenzelm@6580  1623 \begin{figure}[htbp]  wenzelm@6580  1624 \begin{rail}  wenzelm@6580  1625 typedef : 'typedef' ( () | '(' name ')') type '=' set witness;  wenzelm@6580  1626 wenzelm@6580  1627 type : typevarlist name ( () | '(' infix ')' );  wenzelm@6580  1628 set : string;  wenzelm@6580  1629 witness : () | '(' id ')';  wenzelm@6580  1630 \end{rail}  wenzelm@6580  1631 \caption{Syntax of type definitions}  wenzelm@6580  1632 \label{fig:HOL:typedef}  wenzelm@6580  1633 \end{figure}  wenzelm@6580  1634 wenzelm@6580  1635 The syntax for type definitions is shown in Fig.~\ref{fig:HOL:typedef}. For  wenzelm@6580  1636 the definition of typevarlist' and infix' see  wenzelm@6580  1637 \iflabelundefined{chap:classical}  wenzelm@6580  1638 {the appendix of the {\em Reference Manual\/}}%  wenzelm@6580  1639 {Appendix~\ref{app:TheorySyntax}}. The remaining nonterminals have the  wenzelm@6580  1640 following meaning:  wenzelm@6580  1641 \begin{description}  wenzelm@6580  1642 \item[\it type:] the new type constructor $(\alpha@1,\dots,\alpha@n)ty$ with  wenzelm@6580  1643  optional infix annotation.  wenzelm@6580  1644 \item[\it name:] an alphanumeric name $T$ for the type constructor  wenzelm@6580  1645  $ty$, in case $ty$ is a symbolic name. Defaults to $ty$.  wenzelm@6580  1646 \item[\it set:] the representing subset $A$.  wenzelm@6580  1647 \item[\it witness:] name of a theorem of the form $a:A$ proving  wenzelm@6580  1648  non-emptiness. It can be omitted in case Isabelle manages to prove  wenzelm@6580  1649  non-emptiness automatically.  wenzelm@6580  1650 \end{description}  wenzelm@6580  1651 If all context conditions are met (no duplicate type variables in  wenzelm@6580  1652 typevarlist', no extra type variables in set', and no free term variables  wenzelm@6580  1653 in set'), the following components are added to the theory:  wenzelm@6580  1654 \begin{itemize}  wenzelm@6580  1655 \item a type $ty :: (term,\dots,term)term$  wenzelm@6580  1656 \item constants  wenzelm@6580  1657 \begin{eqnarray*}  wenzelm@6580  1658 T &::& \tau\;set \\  wenzelm@6580  1659 Rep_T &::& (\alpha@1,\dots,\alpha@n)ty \To \tau \\  wenzelm@6580  1660 Abs_T &::& \tau \To (\alpha@1,\dots,\alpha@n)ty  wenzelm@6580  1661 \end{eqnarray*}  wenzelm@6580  1662 \item a definition and three axioms  wenzelm@6580  1663 $ wenzelm@6580  1664 \begin{array}{ll}  wenzelm@6580  1665 T{\tt_def} & T \equiv A \\  wenzelm@6580  1666 {\tt Rep_}T & Rep_T\,x \in T \\  wenzelm@6580  1667 {\tt Rep_}T{\tt_inverse} & Abs_T\,(Rep_T\,x) = x \\  wenzelm@6580  1668 {\tt Abs_}T{\tt_inverse} & y \in T \Imp Rep_T\,(Abs_T\,y) = y  wenzelm@6580  1669 \end{array}  wenzelm@6580  1670 $  wenzelm@6580  1671 stating that $(\alpha@1,\dots,\alpha@n)ty$ is isomorphic to $A$ by $Rep_T$  wenzelm@6580  1672 and its inverse $Abs_T$.  wenzelm@6580  1673 \end{itemize}  wenzelm@9695  1674 Below are two simple examples of HOL type definitions. Non-emptiness is  wenzelm@9695  1675 proved automatically here.  wenzelm@6580  1676 \begin{ttbox}  wenzelm@6580  1677 typedef unit = "{\ttlbrace}True{\ttrbrace}"  wenzelm@6580  1678 wenzelm@6580  1679 typedef (prod)  wenzelm@6580  1680  ('a, 'b) "*" (infixr 20)  wenzelm@6580  1681  = "{\ttlbrace}f . EX (a::'a) (b::'b). f = (\%x y. x = a & y = b){\ttrbrace}"  wenzelm@6580  1682 \end{ttbox}  wenzelm@6580  1683 wenzelm@6580  1684 Type definitions permit the introduction of abstract data types in a safe  wenzelm@6580  1685 way, namely by providing models based on already existing types. Given some  wenzelm@6580  1686 abstract axiomatic description $P$ of a type, this involves two steps:  wenzelm@6580  1687 \begin{enumerate}  wenzelm@6580  1688 \item Find an appropriate type $\tau$ and subset $A$ which has the desired  wenzelm@6580  1689  properties $P$, and make a type definition based on this representation.  wenzelm@6580  1690 \item Prove that $P$ holds for $ty$ by lifting $P$ from the representation.  wenzelm@6580  1691 \end{enumerate}  wenzelm@6580  1692 You can now forget about the representation and work solely in terms of the  wenzelm@6580  1693 abstract properties $P$.  wenzelm@6580  1694 wenzelm@6580  1695 \begin{warn}  wenzelm@6580  1696 If you introduce a new type (constructor) $ty$ axiomatically, i.e.\ by  wenzelm@6580  1697 declaring the type and its operations and by stating the desired axioms, you  wenzelm@6580  1698 should make sure the type has a non-empty model. You must also have a clause  wenzelm@6580  1699 \par  wenzelm@6580  1700 \begin{ttbox}  wenzelm@6580  1701 arities $$ty$$ :: (term,\thinspace$$\dots$$,{\thinspace}term){\thinspace}term  wenzelm@6580  1702 \end{ttbox}  wenzelm@6580  1703 in your theory file to tell Isabelle that $ty$ is in class \texttt{term}, the  wenzelm@9695  1704 class of all HOL types.  wenzelm@6580  1705 \end{warn}  wenzelm@6580  1706 wenzelm@6580  1707 wenzelm@6580  1708 \section{Datatype definitions}  wenzelm@6580  1709 \label{sec:HOL:datatype}  wenzelm@6580  1710 \index{*datatype|(}  wenzelm@6580  1711 wenzelm@6626  1712 Inductive datatypes, similar to those of \ML, frequently appear in  wenzelm@6580  1713 applications of Isabelle/HOL. In principle, such types could be defined by  oheimb@7490  1714 hand via \texttt{typedef} (see {\S}\ref{sec:typedef}), but this would be far too  wenzelm@6626  1715 tedious. The \ttindex{datatype} definition package of Isabelle/HOL (cf.\  wenzelm@6626  1716 \cite{Berghofer-Wenzel:1999:TPHOL}) automates such chores. It generates an  wenzelm@6626  1717 appropriate \texttt{typedef} based on a least fixed-point construction, and  wenzelm@6626  1718 proves freeness theorems and induction rules, as well as theorems for  wenzelm@6626  1719 recursion and case combinators. The user just has to give a simple  wenzelm@6626  1720 specification of new inductive types using a notation similar to {\ML} or  wenzelm@6626  1721 Haskell.  wenzelm@6580  1722 wenzelm@6580  1723 The current datatype package can handle both mutual and indirect recursion.  wenzelm@6580  1724 It also offers to represent existing types as datatypes giving the advantage  wenzelm@6580  1725 of a more uniform view on standard theories.  wenzelm@6580  1726 wenzelm@6580  1727 wenzelm@6580  1728 \subsection{Basics}  wenzelm@6580  1729 \label{subsec:datatype:basics}  wenzelm@6580  1730 wenzelm@6580  1731 A general \texttt{datatype} definition is of the following form:  wenzelm@6580  1732 $ wenzelm@6580  1733 \begin{array}{llcl}  paulson@9212  1734 \mathtt{datatype} & (\vec{\alpha})t@1 & = &  wenzelm@6580  1735  C^1@1~\tau^1@{1,1}~\ldots~\tau^1@{1,m^1@1} ~\mid~ \ldots ~\mid~  wenzelm@6580  1736  C^1@{k@1}~\tau^1@{k@1,1}~\ldots~\tau^1@{k@1,m^1@{k@1}} \\  wenzelm@6580  1737  & & \vdots \\  paulson@9212  1738 \mathtt{and} & (\vec{\alpha})t@n & = &  wenzelm@6580  1739  C^n@1~\tau^n@{1,1}~\ldots~\tau^n@{1,m^n@1} ~\mid~ \ldots ~\mid~  wenzelm@6580  1740  C^n@{k@n}~\tau^n@{k@n,1}~\ldots~\tau^n@{k@n,m^n@{k@n}}  wenzelm@6580  1741 \end{array}  wenzelm@6580  1742 $  paulson@9212  1743 where $\vec{\alpha} = (\alpha@1,\ldots,\alpha@h)$ is a list of type variables,  paulson@9212  1744 $C^j@i$ are distinct constructor names and $\tau^j@{i,i'}$ are {\em  paulson@9212  1745  admissible} types containing at most the type variables $\alpha@1, \ldots,  paulson@9212  1746 \alpha@h$. A type $\tau$ occurring in a \texttt{datatype} definition is {\em  paulson@9258  1747  admissible} if and only if  wenzelm@6580  1748 \begin{itemize}  wenzelm@6580  1749 \item $\tau$ is non-recursive, i.e.\ $\tau$ does not contain any of the  wenzelm@6580  1750 newly defined type constructors $t@1,\ldots,t@n$, or  paulson@9212  1751 \item $\tau = (\vec{\alpha})t@{j'}$ where $1 \leq j' \leq n$, or  wenzelm@6580  1752 \item $\tau = (\tau'@1,\ldots,\tau'@{h'})t'$, where $t'$ is  wenzelm@6580  1753 the type constructor of an already existing datatype and $\tau'@1,\ldots,\tau'@{h'}$  wenzelm@6580  1754 are admissible types.  oheimb@7490  1755 \item $\tau = \sigma \to \tau'$, where $\tau'$ is an admissible  berghofe@7044  1756 type and $\sigma$ is non-recursive (i.e. the occurrences of the newly defined  berghofe@7044  1757 types are {\em strictly positive})  wenzelm@6580  1758 \end{itemize}  paulson@9212  1759 If some $(\vec{\alpha})t@{j'}$ occurs in a type $\tau^j@{i,i'}$  wenzelm@6580  1760 of the form  wenzelm@6580  1761 $ paulson@9212  1762 (\ldots,\ldots ~ (\vec{\alpha})t@{j'} ~ \ldots,\ldots)t'  wenzelm@6580  1763 $  wenzelm@6580  1764 this is called a {\em nested} (or \emph{indirect}) occurrence. A very simple  wenzelm@6580  1765 example of a datatype is the type \texttt{list}, which can be defined by  wenzelm@6580  1766 \begin{ttbox}  wenzelm@6580  1767 datatype 'a list = Nil  wenzelm@6580  1768  | Cons 'a ('a list)  wenzelm@6580  1769 \end{ttbox}  wenzelm@6580  1770 Arithmetic expressions \texttt{aexp} and boolean expressions \texttt{bexp} can be modelled  wenzelm@6580  1771 by the mutually recursive datatype definition  wenzelm@6580  1772 \begin{ttbox}  wenzelm@6580  1773 datatype 'a aexp = If_then_else ('a bexp) ('a aexp) ('a aexp)  wenzelm@6580  1774  | Sum ('a aexp) ('a aexp)  wenzelm@6580  1775  | Diff ('a aexp) ('a aexp)  wenzelm@6580  1776  | Var 'a  wenzelm@6580  1777  | Num nat  wenzelm@6580  1778 and 'a bexp = Less ('a aexp) ('a aexp)  wenzelm@6580  1779  | And ('a bexp) ('a bexp)  wenzelm@6580  1780  | Or ('a bexp) ('a bexp)  wenzelm@6580  1781 \end{ttbox}  wenzelm@6580  1782 The datatype \texttt{term}, which is defined by  wenzelm@6580  1783 \begin{ttbox}  wenzelm@6580  1784 datatype ('a, 'b) term = Var 'a  wenzelm@6580  1785  | App 'b ((('a, 'b) term) list)  wenzelm@6580  1786 \end{ttbox}  berghofe@7044  1787 is an example for a datatype with nested recursion. Using nested recursion  berghofe@7044  1788 involving function spaces, we may also define infinitely branching datatypes, e.g.  berghofe@7044  1789 \begin{ttbox}  berghofe@7044  1790 datatype 'a tree = Atom 'a | Branch "nat => 'a tree"  berghofe@7044  1791 \end{ttbox}  wenzelm@6580  1792 wenzelm@6580  1793 \medskip  wenzelm@6580  1794 wenzelm@6580  1795 Types in HOL must be non-empty. Each of the new datatypes  paulson@9258  1796 $(\vec{\alpha})t@j$ with $1 \leq j \leq n$ is non-empty if and only if it has a  wenzelm@6580  1797 constructor $C^j@i$ with the following property: for all argument types  paulson@9212  1798 $\tau^j@{i,i'}$ of the form $(\vec{\alpha})t@{j'}$ the datatype  paulson@9212  1799 $(\vec{\alpha})t@{j'}$ is non-empty.  wenzelm@6580  1800 wenzelm@6580  1801 If there are no nested occurrences of the newly defined datatypes, obviously  paulson@9212  1802 at least one of the newly defined datatypes $(\vec{\alpha})t@j$  wenzelm@6580  1803 must have a constructor $C^j@i$ without recursive arguments, a \emph{base  wenzelm@6580  1804  case}, to ensure that the new types are non-empty. If there are nested  wenzelm@6580  1805 occurrences, a datatype can even be non-empty without having a base case  wenzelm@6580  1806 itself. Since \texttt{list} is a non-empty datatype, \texttt{datatype t = C (t  wenzelm@6580  1807  list)} is non-empty as well.  wenzelm@6580  1808 wenzelm@6580  1809 wenzelm@6580  1810 \subsubsection{Freeness of the constructors}  wenzelm@6580  1811 wenzelm@6580  1812 The datatype constructors are automatically defined as functions of their  wenzelm@6580  1813 respective type:  wenzelm@6580  1814 $C^j@i :: [\tau^j@{i,1},\dots,\tau^j@{i,m^j@i}] \To (\alpha@1,\dots,\alpha@h)t@j$  wenzelm@6580  1815 These functions have certain {\em freeness} properties. They construct  wenzelm@6580  1816 distinct values:  wenzelm@6580  1817 $ wenzelm@6580  1818 C^j@i~x@1~\dots~x@{m^j@i} \neq C^j@{i'}~y@1~\dots~y@{m^j@{i'}} \qquad  wenzelm@6580  1819 \mbox{for all}~ i \neq i'.  wenzelm@6580  1820 $  wenzelm@6580  1821 The constructor functions are injective:  wenzelm@6580  1822 $ wenzelm@6580  1823 (C^j@i~x@1~\dots~x@{m^j@i} = C^j@i~y@1~\dots~y@{m^j@i}) =  wenzelm@6580  1824 (x@1 = y@1 \land \dots \land x@{m^j@i} = y@{m^j@i})  wenzelm@6580  1825 $  berghofe@7044  1826 Since the number of distinctness inequalities is quadratic in the number of  berghofe@7044  1827 constructors, the datatype package avoids proving them separately if there are  berghofe@7044  1828 too many constructors. Instead, specific inequalities are proved by a suitable  berghofe@7044  1829 simplification procedure on demand.\footnote{This procedure, which is already part  berghofe@7044  1830 of the default simpset, may be referred to by the ML identifier  berghofe@7044  1831 \texttt{DatatypePackage.distinct_simproc}.}  wenzelm@6580  1832 wenzelm@6580  1833 \subsubsection{Structural induction}  wenzelm@6580  1834 wenzelm@6580  1835 The datatype package also provides structural induction rules. For  wenzelm@6580  1836 datatypes without nested recursion, this is of the following form:  wenzelm@6580  1837 $ oheimb@7490  1838 \infer{P@1~x@1 \land \dots \land P@n~x@n}  wenzelm@6580  1839  {\begin{array}{lcl}  wenzelm@6580  1840  \Forall x@1 \dots x@{m^1@1}.  wenzelm@6580  1841  \List{P@{s^1@{1,1}}~x@{r^1@{1,1}}; \dots;  wenzelm@6580  1842  P@{s^1@{1,l^1@1}}~x@{r^1@{1,l^1@1}}} & \Imp &  wenzelm@6580  1843  P@1~\left(C^1@1~x@1~\dots~x@{m^1@1}\right) \\  wenzelm@6580  1844  & \vdots \\  wenzelm@6580  1845  \Forall x@1 \dots x@{m^1@{k@1}}.  wenzelm@6580  1846  \List{P@{s^1@{k@1,1}}~x@{r^1@{k@1,1}}; \dots;  wenzelm@6580  1847  P@{s^1@{k@1,l^1@{k@1}}}~x@{r^1@{k@1,l^1@{k@1}}}} & \Imp &  wenzelm@6580  1848  P@1~\left(C^1@{k@1}~x@1~\ldots~x@{m^1@{k@1}}\right) \\  wenzelm@6580  1849  & \vdots \\  wenzelm@6580  1850  \Forall x@1 \dots x@{m^n@1}.  wenzelm@6580  1851  \List{P@{s^n@{1,1}}~x@{r^n@{1,1}}; \dots;  wenzelm@6580  1852  P@{s^n@{1,l^n@1}}~x@{r^n@{1,l^n@1}}} & \Imp &  wenzelm@6580  1853  P@n~\left(C^n@1~x@1~\ldots~x@{m^n@1}\right) \\  wenzelm@6580  1854  & \vdots \\  wenzelm@6580  1855  \Forall x@1 \dots x@{m^n@{k@n}}.  wenzelm@6580  1856  \List{P@{s^n@{k@n,1}}~x@{r^n@{k@n,1}}; \dots  wenzelm@6580  1857  P@{s^n@{k@n,l^n@{k@n}}}~x@{r^n@{k@n,l^n@{k@n}}}} & \Imp &  wenzelm@6580  1858  P@n~\left(C^n@{k@n}~x@1~\ldots~x@{m^n@{k@n}}\right)  wenzelm@6580  1859  \end{array}}  wenzelm@6580  1860 $  wenzelm@6580  1861 where  wenzelm@6580  1862 $ wenzelm@6580  1863 \begin{array}{rcl}  wenzelm@6580  1864 Rec^j@i & := &  wenzelm@6580  1865  \left\{\left(r^j@{i,1},s^j@{i,1}\right),\ldots,  wenzelm@6580  1866  \left(r^j@{i,l^j@i},s^j@{i,l^j@i}\right)\right\} = \\[2ex]  wenzelm@6580  1867 && \left\{(i',i'')~\left|~  oheimb@7490  1868  1\leq i' \leq m^j@i \land 1 \leq i'' \leq n \land  wenzelm@6580  1869  \tau^j@{i,i'} = (\alpha@1,\ldots,\alpha@h)t@{i''}\right.\right\}  wenzelm@6580  1870 \end{array}  wenzelm@6580  1871 $  wenzelm@6580  1872 i.e.\ the properties $P@j$ can be assumed for all recursive arguments.  wenzelm@6580  1873 wenzelm@6580  1874 For datatypes with nested recursion, such as the \texttt{term} example from  wenzelm@6580  1875 above, things are a bit more complicated. Conceptually, Isabelle/HOL unfolds  wenzelm@6580  1876 a definition like  wenzelm@6580  1877 \begin{ttbox}  paulson@9212  1878 datatype ('a,'b) term = Var 'a  paulson@9212  1879  | App 'b ((('a, 'b) term) list)  wenzelm@6580  1880 \end{ttbox}  wenzelm@6580  1881 to an equivalent definition without nesting:  wenzelm@6580  1882 \begin{ttbox}  paulson@9212  1883 datatype ('a,'b) term = Var  paulson@9212  1884  | App 'b (('a, 'b) term_list)  paulson@9212  1885 and ('a,'b) term_list = Nil'  paulson@9212  1886  | Cons' (('a,'b) term) (('a,'b) term_list)  wenzelm@6580  1887 \end{ttbox}  wenzelm@6580  1888 Note however, that the type \texttt{('a,'b) term_list} and the constructors {\tt  wenzelm@6580  1889  Nil'} and \texttt{Cons'} are not really introduced. One can directly work with  wenzelm@6580  1890 the original (isomorphic) type \texttt{(('a, 'b) term) list} and its existing  wenzelm@6580  1891 constructors \texttt{Nil} and \texttt{Cons}. Thus, the structural induction rule for  wenzelm@6580  1892 \texttt{term} gets the form  wenzelm@6580  1893 $ oheimb@7490  1894 \infer{P@1~x@1 \land P@2~x@2}  wenzelm@6580  1895  {\begin{array}{l}  wenzelm@6580  1896  \Forall x.~P@1~(\mathtt{Var}~x) \\  wenzelm@6580  1897  \Forall x@1~x@2.~P@2~x@2 \Imp P@1~(\mathtt{App}~x@1~x@2) \\  wenzelm@6580  1898  P@2~\mathtt{Nil} \\  wenzelm@6580  1899  \Forall x@1~x@2. \List{P@1~x@1; P@2~x@2} \Imp P@2~(\mathtt{Cons}~x@1~x@2)  wenzelm@6580  1900  \end{array}}  wenzelm@6580  1901 $  wenzelm@6580  1902 Note that there are two predicates $P@1$ and $P@2$, one for the type \texttt{('a,'b) term}  wenzelm@6580  1903 and one for the type \texttt{(('a, 'b) term) list}.  wenzelm@6580  1904 berghofe@7044  1905 For a datatype with function types such as \texttt{'a tree}, the induction rule  berghofe@7044  1906 is of the form  berghofe@7044  1907 $ berghofe@7044  1908 \infer{P~t}  berghofe@7044  1909  {\Forall a.~P~(\mathtt{Atom}~a) &  berghofe@7044  1910  \Forall ts.~(\forall x.~P~(ts~x)) \Imp P~(\mathtt{Branch}~ts)}  berghofe@7044  1911 $  berghofe@7044  1912 wenzelm@6580  1913 \medskip In principle, inductive types are already fully determined by  wenzelm@6580  1914 freeness and structural induction. For convenience in applications,  wenzelm@6580  1915 the following derived constructions are automatically provided for any  wenzelm@6580  1916 datatype.  wenzelm@6580  1917 wenzelm@6580  1918 \subsubsection{The \sdx{case} construct}  wenzelm@6580  1919 wenzelm@6580  1920 The type comes with an \ML-like \texttt{case}-construct:  wenzelm@6580  1921 $ wenzelm@6580  1922 \begin{array}{rrcl}  wenzelm@6580  1923 \mbox{\tt case}~e~\mbox{\tt of} & C^j@1~x@{1,1}~\dots~x@{1,m^j@1} & \To & e@1 \\  wenzelm@6580  1924  \vdots \\  wenzelm@6580  1925  \mid & C^j@{k@j}~x@{k@j,1}~\dots~x@{k@j,m^j@{k@j}} & \To & e@{k@j}  wenzelm@6580  1926 \end{array}  wenzelm@6580  1927 $  wenzelm@6580  1928 where the $x@{i,j}$ are either identifiers or nested tuple patterns as in  oheimb@7490  1929 {\S}\ref{subsec:prod-sum}.  wenzelm@6580  1930 \begin{warn}  wenzelm@6580  1931  All constructors must be present, their order is fixed, and nested patterns  wenzelm@6580  1932  are not supported (with the exception of tuples). Violating this  wenzelm@6580  1933  restriction results in strange error messages.  wenzelm@6580  1934 \end{warn}  wenzelm@6580  1935 wenzelm@6580  1936 To perform case distinction on a goal containing a \texttt{case}-construct,  wenzelm@6580  1937 the theorem $t@j.$\texttt{split} is provided:  wenzelm@6580  1938 $ wenzelm@6580  1939 \begin{array}{@{}rcl@{}}  wenzelm@6580  1940 P(t@j_\mathtt{case}~f@1~\dots~f@{k@j}~e) &\!\!\!=&  wenzelm@6580  1941 \!\!\! ((\forall x@1 \dots x@{m^j@1}. e = C^j@1~x@1\dots x@{m^j@1} \to  wenzelm@6580  1942  P(f@1~x@1\dots x@{m^j@1})) \\  wenzelm@6580  1943 &&\!\!\! ~\land~ \dots ~\land \\  wenzelm@6580  1944 &&~\!\!\! (\forall x@1 \dots x@{m^j@{k@j}}. e = C^j@{k@j}~x@1\dots x@{m^j@{k@j}} \to  wenzelm@6580  1945  P(f@{k@j}~x@1\dots x@{m^j@{k@j}})))  wenzelm@6580  1946 \end{array}  wenzelm@6580  1947 $  wenzelm@6580  1948 where $t@j$\texttt{_case} is the internal name of the \texttt{case}-construct.  wenzelm@6580  1949 This theorem can be added to a simpset via \ttindex{addsplits}  oheimb@7490  1950 (see~{\S}\ref{subsec:HOL:case:splitting}).  wenzelm@6580  1951 wenzelm@10109  1952 Case splitting on assumption works as well, by using the rule  wenzelm@10109  1953 $t@j.$\texttt{split_asm} in the same manner. Both rules are available under  wenzelm@10109  1954 $t@j.$\texttt{splits} (this name is \emph{not} bound in ML, though).  wenzelm@10109  1955 nipkow@8604  1956 \begin{warn}\index{simplification!of \texttt{case}}%  nipkow@8604  1957  By default only the selector expression ($e$ above) in a  nipkow@8604  1958  \texttt{case}-construct is simplified, in analogy with \texttt{if} (see  nipkow@8604  1959  page~\pageref{if-simp}). Only if that reduces to a constructor is one of  nipkow@8604  1960  the arms of the \texttt{case}-construct exposed and simplified. To ensure  nipkow@8604  1961  full simplification of all parts of a \texttt{case}-construct for datatype  nipkow@8604  1962  $t$, remove $t$\texttt{.}\ttindexbold{case_weak_cong} from the simpset, for  nipkow@8604  1963  example by \texttt{delcongs [thm "$t$.weak_case_cong"]}.  nipkow@8604  1964 \end{warn}  nipkow@8604  1965 wenzelm@6580  1966 \subsubsection{The function \cdx{size}}\label{sec:HOL:size}  wenzelm@6580  1967 paulson@15455  1968 Theory \texttt{NatArith} declares a generic function \texttt{size} of type  wenzelm@6580  1969 $\alpha\To nat$. Each datatype defines a particular instance of \texttt{size}  wenzelm@6580  1970 by overloading according to the following scheme:  wenzelm@6580  1971 %%% FIXME: This formula is too big and is completely unreadable  wenzelm@6580  1972 $ wenzelm@6580  1973 size(C^j@i~x@1~\dots~x@{m^j@i}) = \!  wenzelm@6580  1974 \left\{  wenzelm@6580  1975 \begin{array}{ll}  wenzelm@6580  1976 0 & \!\mbox{if Rec^j@i = \emptyset} \\  berghofe@7044  1977 1+\sum\limits@{h=1}^{l^j@i}size~x@{r^j@{i,h}} &  wenzelm@6580  1978  \!\mbox{if Rec^j@i = \left\{\left(r^j@{i,1},s^j@{i,1}\right),\ldots,  wenzelm@6580  1979  \left(r^j@{i,l^j@i},s^j@{i,l^j@i}\right)\right\}}  wenzelm@6580  1980 \end{array}  wenzelm@6580  1981 \right.  wenzelm@6580  1982 $  wenzelm@6580  1983 where $Rec^j@i$ is defined above. Viewing datatypes as generalised trees, the  wenzelm@6580  1984 size of a leaf is 0 and the size of a node is the sum of the sizes of its  wenzelm@6580  1985 subtrees ${}+1$.  wenzelm@6580  1986 wenzelm@6580  1987 \subsection{Defining datatypes}  wenzelm@6580  1988 wenzelm@6580  1989 The theory syntax for datatype definitions is shown in  wenzelm@6580  1990 Fig.~\ref{datatype-grammar}. In order to be well-formed, a datatype  wenzelm@6580  1991 definition has to obey the rules stated in the previous section. As a result  wenzelm@6580  1992 the theory is extended with the new types, the constructors, and the theorems  wenzelm@6580  1993 listed in the previous section.  wenzelm@6580  1994 wenzelm@6580  1995 \begin{figure}  wenzelm@6580  1996 \begin{rail}  wenzelm@6580  1997 datatype : 'datatype' typedecls;  wenzelm@6580  1998 wenzelm@6580  1999 typedecls: ( newtype '=' (cons + '|') ) + 'and'  wenzelm@6580  2000  ;  wenzelm@6580  2001 newtype : typevarlist id ( () | '(' infix ')' )  wenzelm@6580  2002  ;  wenzelm@6580  2003 cons : name (argtype *) ( () | ( '(' mixfix ')' ) )  wenzelm@6580  2004  ;  wenzelm@6580  2005 argtype : id | tid | ('(' typevarlist id ')')  wenzelm@6580  2006  ;  wenzelm@6580  2007 \end{rail}  wenzelm@6580  2008 \caption{Syntax of datatype declarations}  wenzelm@6580  2009 \label{datatype-grammar}  wenzelm@6580  2010 \end{figure}  wenzelm@6580  2011 wenzelm@6580  2012 Most of the theorems about datatypes become part of the default simpset and  wenzelm@6580  2013 you never need to see them again because the simplifier applies them  nipkow@8424  2014 automatically. Only induction or case distinction are usually invoked by hand.  wenzelm@6580  2015 \begin{ttdescription}  wenzelm@6580  2016 \item[\ttindexbold{induct_tac} {\tt"}$x${\tt"} $i$]  wenzelm@6580  2017  applies structural induction on variable $x$ to subgoal $i$, provided the  wenzelm@6580  2018  type of $x$ is a datatype.  berghofe@7846  2019 \item[\texttt{induct_tac}  berghofe@7846  2020  {\tt"}$x@1$ $\ldots$ $x@n${\tt"} $i$] applies simultaneous  wenzelm@6580  2021  structural induction on the variables $x@1,\ldots,x@n$ to subgoal $i$. This  wenzelm@6580  2022  is the canonical way to prove properties of mutually recursive datatypes  wenzelm@6580  2023  such as \texttt{aexp} and \texttt{bexp}, or datatypes with nested recursion such as  wenzelm@6580  2024  \texttt{term}.  wenzelm@6580  2025 \end{ttdescription}  wenzelm@6580  2026 In some cases, induction is overkill and a case distinction over all  wenzelm@6580  2027 constructors of the datatype suffices.  wenzelm@6580  2028 \begin{ttdescription}  wenzelm@8443  2029 \item[\ttindexbold{case_tac} {\tt"}$u${\tt"} $i$]  nipkow@8424  2030  performs a case analysis for the term $u$ whose type must be a datatype.  nipkow@8424  2031  If the datatype has $k@j$ constructors $C^j@1$, \dots $C^j@{k@j}$, subgoal  nipkow@8424  2032  $i$ is replaced by $k@j$ new subgoals which contain the additional  nipkow@8424  2033  assumption $u = C^j@{i'}~x@1~\dots~x@{m^j@{i'}}$ for $i'=1$, $\dots$,~$k@j$.  wenzelm@6580  2034 \end{ttdescription}  wenzelm@6580  2035 wenzelm@6580  2036 Note that induction is only allowed on free variables that should not occur  nipkow@8424  2037 among the premises of the subgoal. Case distinction applies to arbitrary terms.  wenzelm@6580  2038 wenzelm@6580  2039 \bigskip  wenzelm@6580  2040 wenzelm@6580  2041 wenzelm@6580  2042 For the technically minded, we exhibit some more details. Processing the  wenzelm@6580  2043 theory file produces an \ML\ structure which, in addition to the usual  wenzelm@6580  2044 components, contains a structure named $t$ for each datatype $t$ defined in  wenzelm@6580  2045 the file. Each structure $t$ contains the following elements:  wenzelm@6580  2046 \begin{ttbox}  wenzelm@6580  2047 val distinct : thm list  wenzelm@6580  2048 val inject : thm list  wenzelm@6580  2049 val induct : thm  wenzelm@6580  2050 val exhaust : thm  wenzelm@6580  2051 val cases : thm list  wenzelm@6580  2052 val split : thm  wenzelm@6580  2053 val split_asm : thm  wenzelm@6580  2054 val recs : thm list  wenzelm@6580  2055 val size : thm list  wenzelm@6580  2056 val simps : thm list  wenzelm@6580  2057 \end{ttbox}  wenzelm@6580  2058 \texttt{distinct}, \texttt{inject}, \texttt{induct}, \texttt{size}  wenzelm@6580  2059 and \texttt{split} contain the theorems  wenzelm@6580  2060 described above. For user convenience, \texttt{distinct} contains  wenzelm@6580  2061 inequalities in both directions. The reduction rules of the {\tt  wenzelm@6580  2062  case}-construct are in \texttt{cases}. All theorems from {\tt  wenzelm@6580  2063  distinct}, \texttt{inject} and \texttt{cases} are combined in \texttt{simps}.  wenzelm@6580  2064 In case of mutually recursive datatypes, \texttt{recs}, \texttt{size}, \texttt{induct}  wenzelm@6580  2065 and \texttt{simps} are contained in a separate structure named $t@1_\ldots_t@n$.  wenzelm@6580  2066 wenzelm@6580  2067 berghofe@7325  2068 \subsection{Representing existing types as datatypes}\label{subsec:datatype:rep_datatype}  wenzelm@6580  2069 wenzelm@6580  2070 For foundational reasons, some basic types such as \texttt{nat}, \texttt{*}, {\tt  wenzelm@6580  2071  +}, \texttt{bool} and \texttt{unit} are not defined in a \texttt{datatype} section,  wenzelm@6580  2072 but by more primitive means using \texttt{typedef}. To be able to use the  wenzelm@8443  2073 tactics \texttt{induct_tac} and \texttt{case_tac} and to define functions by  wenzelm@6580  2074 primitive recursion on these types, such types may be represented as actual  haftmann@27452  2075 datatypes. This is done by specifying the constructors of the desired type,  haftmann@27452  2076 plus a proof of the induction rule, as well as theorems  wenzelm@6580  2077 stating the distinctness and injectivity of constructors in a {\tt  haftmann@27452  2078 rep_datatype} section. For the sum type this works as follows:  wenzelm@6580  2079 \begin{ttbox}  haftmann@27452  2080 rep_datatype (sum) Inl Inr  haftmann@27452  2081 proof -  haftmann@27452  2082  fix P  haftmann@27452  2083  fix s :: "'a + 'b"  haftmann@27452  2084  assume x: "!!x::'a. P (Inl x)" and y: "!!y::'b. P (Inr y)"  haftmann@27452  2085  then show "P s" by (auto intro: sumE [of s])  haftmann@27452  2086 qed simp_all  wenzelm@6580  2087 \end{ttbox}  wenzelm@6580  2088 The datatype package automatically derives additional theorems for recursion  wenzelm@6580  2089 and case combinators from these rules. Any of the basic HOL types mentioned  wenzelm@6580  2090 above are represented as datatypes. Try an induction on \texttt{bool}  wenzelm@6580  2091 today.  wenzelm@6580  2092 wenzelm@6580  2093 wenzelm@6580  2094 \subsection{Examples}  wenzelm@6580  2095 wenzelm@6580  2096 \subsubsection{The datatype $\alpha~mylist$}  wenzelm@6580  2097 wenzelm@6580  2098 We want to define a type $\alpha~mylist$. To do this we have to build a new  wenzelm@6580  2099 theory that contains the type definition. We start from the theory  wenzelm@6580  2100 \texttt{Datatype} instead of \texttt{Main} in order to avoid clashes with the  wenzelm@6580  2101 \texttt{List} theory of Isabelle/HOL.  wenzelm@6580  2102 \begin{ttbox}  wenzelm@6580  2103 MyList = Datatype +  wenzelm@6580  2104  datatype 'a mylist = Nil | Cons 'a ('a mylist)  wenzelm@6580  2105 end  wenzelm@6580  2106 \end{ttbox}  wenzelm@6580  2107 After loading the theory, we can prove $Cons~x~xs\neq xs$, for example. To  wenzelm@6580  2108 ease the induction applied below, we state the goal with $x$ quantified at the  wenzelm@6580  2109 object-level. This will be stripped later using \ttindex{qed_spec_mp}.  wenzelm@6580  2110 \begin{ttbox}  wenzelm@6580  2111 Goal "!x. Cons x xs ~= xs";  wenzelm@6580  2112 {\out Level 0}  wenzelm@6580  2113 {\out ! x. Cons x xs ~= xs}  wenzelm@6580  2114 {\out 1. ! x. Cons x xs ~= xs}  wenzelm@6580  2115 \end{ttbox}  wenzelm@6580  2116 This can be proved by the structural induction tactic:  wenzelm@6580  2117 \begin{ttbox}  wenzelm@6580  2118 by (induct_tac "xs" 1);  wenzelm@6580  2119 {\out Level 1}  wenzelm@6580  2120 {\out ! x. Cons x xs ~= xs}  wenzelm@6580  2121 {\out 1. ! x. Cons x Nil ~= Nil}  wenzelm@6580  2122 {\out 2. !!a mylist.}  wenzelm@6580  2123 {\out ! x. Cons x mylist ~= mylist ==>}  wenzelm@6580  2124 {\out ! x. Cons x (Cons a mylist) ~= Cons a mylist}  wenzelm@6580  2125 \end{ttbox}  wenzelm@6580  2126 The first subgoal can be proved using the simplifier. Isabelle/HOL has  wenzelm@6580  2127 already added the freeness properties of lists to the default simplification  wenzelm@6580  2128 set.  wenzelm@6580  2129 \begin{ttbox}  wenzelm@6580  2130 by (Simp_tac 1);  wenzelm@6580  2131 {\out Level 2}  wenzelm@6580  2132 {\out ! x. Cons x xs ~= xs}  wenzelm@6580  2133 {\out 1. !!a mylist.}  wenzelm@6580  2134 {\out ! x. Cons x mylist ~= mylist ==>}  wenzelm@6580  2135 {\out ! x. Cons x (Cons a mylist) ~= Cons a mylist}  wenzelm@6580  2136 \end{ttbox}  wenzelm@6580  2137 Similarly, we prove the remaining goal.  wenzelm@6580  2138 \begin{ttbox}  wenzelm@6580  2139 by (Asm_simp_tac 1);  wenzelm@6580  2140 {\out Level 3}  wenzelm@6580  2141 {\out ! x. Cons x xs ~= xs}  wenzelm@6580  2142 {\out No subgoals!}  wenzelm@6580  2143 \ttbreak  wenzelm@6580  2144 qed_spec_mp "not_Cons_self";  wenzelm@6580  2145 {\out val not_Cons_self = "Cons x xs ~= xs" : thm}  wenzelm@6580  2146 \end{ttbox}  wenzelm@6580  2147 Because both subgoals could have been proved by \texttt{Asm_simp_tac}  wenzelm@6580  2148 we could have done that in one step:  wenzelm@6580  2149 \begin{ttbox}  wenzelm@6580  2150 by (ALLGOALS Asm_simp_tac);  wenzelm@6580  2151 \end{ttbox}  wenzelm@6580  2152 wenzelm@6580  2153 wenzelm@6580  2154 \subsubsection{The datatype $\alpha~mylist$ with mixfix syntax}  wenzelm@6580  2155 wenzelm@6580  2156 In this example we define the type $\alpha~mylist$ again but this time  wenzelm@6580  2157 we want to write \texttt{[]} for \texttt{Nil} and we want to use infix  wenzelm@6580  2158 notation \verb|#| for \texttt{Cons}. To do this we simply add mixfix  wenzelm@6580  2159 annotations after the constructor declarations as follows:  wenzelm@6580  2160 \begin{ttbox}  wenzelm@6580  2161 MyList = Datatype +  wenzelm@6580  2162  datatype 'a mylist =  wenzelm@6580  2163  Nil ("[]") |  wenzelm@6580  2164  Cons 'a ('a mylist) (infixr "#" 70)  wenzelm@6580  2165 end  wenzelm@6580  2166 \end{ttbox}  wenzelm@6580  2167 Now the theorem in the previous example can be written \verb|x#xs ~= xs|.  wenzelm@6580  2168 wenzelm@6580  2169 wenzelm@6580  2170 \subsubsection{A datatype for weekdays}  wenzelm@6580  2171 wenzelm@6580  2172 This example shows a datatype that consists of 7 constructors:  wenzelm@6580  2173 \begin{ttbox}  wenzelm@6580  2174 Days = Main +  wenzelm@6580  2175  datatype days = Mon | Tue | Wed | Thu | Fri | Sat | Sun  wenzelm@6580  2176 end  wenzelm@6580  2177 \end{ttbox}  wenzelm@6580  2178 Because there are more than 6 constructors, inequality is expressed via a function  wenzelm@6580  2179 \verb|days_ord|. The theorem \verb|Mon ~= Tue| is not directly  wenzelm@6580  2180 contained among the distinctness theorems, but the simplifier can  paulson@15455  2181 prove it thanks to rewrite rules inherited from theory \texttt{NatArith}:  wenzelm@6580  2182 \begin{ttbox}  wenzelm@6580  2183 Goal "Mon ~= Tue";  wenzelm@6580  2184 by (Simp_tac 1);  wenzelm@6580  2185 \end{ttbox}  wenzelm@6580  2186 You need not derive such inequalities explicitly: the simplifier will dispose  wenzelm@6580  2187 of them automatically.  wenzelm@6580  2188 \index{*datatype|)}  wenzelm@6580  2189 wenzelm@6580  2190 wenzelm@6580  2191 \section{Recursive function definitions}\label{sec:HOL:recursive}  wenzelm@6580  2192 \index{recursive functions|see{recursion}}  wenzelm@6580  2193 wenzelm@6580  2194 Isabelle/HOL provides two main mechanisms of defining recursive functions.  wenzelm@6580  2195 \begin{enumerate}  wenzelm@6580  2196 \item \textbf{Primitive recursion} is available only for datatypes, and it is  wenzelm@6580  2197  somewhat restrictive. Recursive calls are only allowed on the argument's  wenzelm@6580  2198  immediate constituents. On the other hand, it is the form of recursion most  wenzelm@6580  2199  often wanted, and it is easy to use.  wenzelm@6580  2200   wenzelm@6580  2201 \item \textbf{Well-founded recursion} requires that you supply a well-founded  wenzelm@6580  2202  relation that governs the recursion. Recursive calls are only allowed if  wenzelm@6580  2203  they make the argument decrease under the relation. Complicated recursion  wenzelm@6580  2204  forms, such as nested recursion, can be dealt with. Termination can even be  wenzelm@6580  2205  proved at a later time, though having unsolved termination conditions around  wenzelm@6580  2206  can make work difficult.%  wenzelm@6580  2207  \footnote{This facility is based on Konrad Slind's TFL  wenzelm@6580  2208  package~\cite{slind-tfl}. Thanks are due to Konrad for implementing TFL  wenzelm@6580  2209  and assisting with its installation.}  wenzelm@6580  2210 \end{enumerate}  wenzelm@6580  2211 wenzelm@6580  2212 Following good HOL tradition, these declarations do not assert arbitrary  wenzelm@6580  2213 axioms. Instead, they define the function using a recursion operator. Both  wenzelm@6580  2214 HOL and ZF derive the theory of well-founded recursion from first  wenzelm@6580  2215 principles~\cite{paulson-set-II}. Primitive recursion over some datatype  wenzelm@6580  2216 relies on the recursion operator provided by the datatype package. With  wenzelm@6580  2217 either form of function definition, Isabelle proves the desired recursion  wenzelm@6580  2218 equations as theorems.  wenzelm@6580  2219 wenzelm@6580  2220 wenzelm@6580  2221 \subsection{Primitive recursive functions}  wenzelm@6580  2222 \label{sec:HOL:primrec}  wenzelm@6580  2223 \index{recursion!primitive|(}  wenzelm@6580  2224 \index{*primrec|(}  wenzelm@6580  2225 wenzelm@6580  2226 Datatypes come with a uniform way of defining functions, {\bf primitive  wenzelm@6580  2227  recursion}. In principle, one could introduce primitive recursive functions  wenzelm@6580  2228 by asserting their reduction rules as new axioms, but this is not recommended:  wenzelm@6580  2229 \begin{ttbox}\slshape  wenzelm@6580  2230 Append = Main +  wenzelm@6580  2231 consts app :: ['a list, 'a list] => 'a list  wenzelm@6580  2232 rules  wenzelm@6580  2233  app_Nil "app [] ys = ys"  wenzelm@6580  2234  app_Cons "app (x#xs) ys = x#app xs ys"  wenzelm@6580  2235 end  wenzelm@6580  2236 \end{ttbox}  wenzelm@6580  2237 Asserting axioms brings the danger of accidentally asserting nonsense, as  wenzelm@6580  2238 in \verb$app [] ys = us$.  wenzelm@6580  2239 wenzelm@6580  2240 The \ttindex{primrec} declaration is a safe means of defining primitive  wenzelm@6580  2241 recursive functions on datatypes:  wenzelm@6580  2242 \begin{ttbox}  wenzelm@6580  2243 Append = Main +  wenzelm@6580  2244 consts app :: ['a list, 'a list] => 'a list  wenzelm@6580  2245 primrec  wenzelm@6580  2246  "app [] ys = ys"  wenzelm@6580  2247  "app (x#xs) ys = x#app xs ys"  wenzelm@6580  2248 end  wenzelm@6580  2249 \end{ttbox}  wenzelm@6580  2250 Isabelle will now check that the two rules do indeed form a primitive  wenzelm@6580  2251 recursive definition. For example  wenzelm@6580  2252 \begin{ttbox}  wenzelm@6580  2253 primrec  wenzelm@6580  2254  "app [] ys = us"  wenzelm@6580  2255 \end{ttbox}  wenzelm@6580  2256 is rejected with an error message \texttt{Extra variables on rhs}''.  wenzelm@6580  2257 wenzelm@6580  2258 \bigskip  wenzelm@6580  2259 wenzelm@6580  2260 The general form of a primitive recursive definition is  wenzelm@6580  2261 \begin{ttbox}  wenzelm@6580  2262 primrec  wenzelm@6580  2263  {\it reduction rules}  wenzelm@6580  2264 \end{ttbox}  wenzelm@6580  2265 where \textit{reduction rules} specify one or more equations of the form  wenzelm@6580  2266 $f \, x@1 \, \dots \, x@m \, (C \, y@1 \, \dots \, y@k) \, z@1 \,  wenzelm@6580  2267 \dots \, z@n = r$ such that $C$ is a constructor of the datatype, $r$  wenzelm@6580  2268 contains only the free variables on the left-hand side, and all recursive  wenzelm@6580  2269 calls in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$. There  wenzelm@6580  2270 must be at most one reduction rule for each constructor. The order is  wenzelm@6580  2271 immaterial. For missing constructors, the function is defined to return a  wenzelm@6580  2272 default value.  wenzelm@6580  2273 wenzelm@6580  2274 If you would like to refer to some rule by name, then you must prefix  wenzelm@6580  2275 the rule with an identifier. These identifiers, like those in the  wenzelm@6580  2276 \texttt{rules} section of a theory, will be visible at the \ML\ level.  wenzelm@6580  2277 wenzelm@6580  2278 The primitive recursive function can have infix or mixfix syntax:  wenzelm@6580  2279 \begin{ttbox}\underscoreon  wenzelm@6580  2280 consts "@" :: ['a list, 'a list] => 'a list (infixr 60)  wenzelm@6580  2281 primrec  wenzelm@6580  2282  "[] @ ys = ys"  wenzelm@6580  2283  "(x#xs) @ ys = x#(xs @ ys)"  wenzelm@6580  2284 \end{ttbox}  wenzelm@6580  2285 wenzelm@6580  2286 The reduction rules become part of the default simpset, which  wenzelm@6580  2287 leads to short proof scripts:  wenzelm@6580  2288 \begin{ttbox}\underscoreon  wenzelm@6580  2289 Goal "(xs @ ys) @ zs = xs @ (ys @ zs)";  wenzelm@6580  2290 by (induct\_tac "xs" 1);  wenzelm@6580  2291 by (ALLGOALS Asm\_simp\_tac);  wenzelm@6580  2292 \end{ttbox}  wenzelm@6580  2293 wenzelm@6580  2294 \subsubsection{Example: Evaluation of expressions}  berghofe@7044  2295 Using mutual primitive recursion, we can define evaluation functions \texttt{evala}  wenzelm@6580  2296 and \texttt{eval_bexp} for the datatypes of arithmetic and boolean expressions mentioned in  oheimb@7490  2297 {\S}\ref{subsec:datatype:basics}:  wenzelm@6580  2298 \begin{ttbox}  wenzelm@6580  2299 consts  berghofe@7044  2300  evala :: "['a => nat, 'a aexp] => nat"  berghofe@7044  2301  evalb :: "['a => nat, 'a bexp] => bool"  wenzelm@6580  2302 wenzelm@6580  2303 primrec  berghofe@7044  2304  "evala env (If_then_else b a1 a2) =  berghofe@7044  2305  (if evalb env b then evala env a1 else evala env a2)"  berghofe@7044  2306  "evala env (Sum a1 a2) = evala env a1 + evala env a2"  berghofe@7044  2307  "evala env (Diff a1 a2) = evala env a1 - evala env a2"  berghofe@7044  2308  "evala env (Var v) = env v"  berghofe@7044  2309  "evala env (Num n) = n"  berghofe@7044  2310 berghofe@7044  2311  "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"  berghofe@7044  2312  "evalb env (And b1 b2) = (evalb env b1 & evalb env b2)"  berghofe@7044  2313  "evalb env (Or b1 b2) = (evalb env b1 & evalb env b2)"  wenzelm@6580  2314 \end{ttbox}  wenzelm@6580  2315 Since the value of an expression depends on the value of its variables,  berghofe@7044  2316 the functions \texttt{evala} and \texttt{evalb} take an additional  wenzelm@6580  2317 parameter, an {\em environment} of type \texttt{'a => nat}, which maps  wenzelm@6580  2318 variables to their values.  wenzelm@6580  2319 berghofe@7044  2320 Similarly, we may define substitution functions \texttt{substa}  berghofe@7044  2321 and \texttt{substb} for expressions: The mapping \texttt{f} of type  wenzelm@6580  2322 \texttt{'a => 'a aexp} given as a parameter is lifted canonically  berghofe@7044  2323 on the types \texttt{'a aexp} and \texttt{'a bexp}:  wenzelm@6580  2324 \begin{ttbox}  wenzelm@6580  2325 consts  berghofe@7044  2326  substa :: "['a => 'b aexp, 'a aexp] => 'b aexp"  berghofe@7044  2327  substb :: "['a => 'b aexp, 'a bexp] => 'b bexp"  wenzelm@6580  2328 wenzelm@6580  2329 primrec  berghofe@7044  2330  "substa f (If_then_else b a1 a2) =  berghofe@7044  2331  If_then_else (substb f b) (substa f a1) (substa f a2)"  berghofe@7044  2332  "substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)"  berghofe@7044  2333  "substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)"  berghofe@7044  2334  "substa f (Var v) = f v"  berghofe@7044  2335  "substa f (Num n) = Num n"  berghofe@7044  2336 berghofe@7044  2337  "substb f (Less a1 a2) = Less (substa f a1) (substa f a2)"  berghofe@7044  2338  "substb f (And b1 b2) = And (substb f b1) (substb f b2)"  berghofe@7044  2339  "substb f (Or b1 b2) = Or (substb f b1) (substb f b2)"  wenzelm@6580  2340 \end{ttbox}  wenzelm@6580  2341 In textbooks about semantics one often finds {\em substitution theorems},  wenzelm@6580  2342 which express the relationship between substitution and evaluation. For  wenzelm@6580  2343 \texttt{'a aexp} and \texttt{'a bexp}, we can prove such a theorem by mutual  wenzelm@6580  2344 induction, followed by simplification:  wenzelm@6580  2345 \begin{ttbox}  wenzelm@6580  2346 Goal  berghofe@7044  2347  "evala env (substa (Var(v := a')) a) =  berghofe@7044  2348  evala (env(v := evala env a')) a &  berghofe@7044  2349  evalb env (substb (Var(v := a')) b) =  berghofe@7044  2350  evalb (env(v := evala env a')) b";  berghofe@7846  2351 by (induct_tac "a b" 1);  wenzelm@6580  2352 by (ALLGOALS Asm_full_simp_tac);  wenzelm@6580  2353 \end{ttbox}  wenzelm@6580  2354 wenzelm@6580  2355 \subsubsection{Example: A substitution function for terms}  wenzelm@6580  2356 Functions on datatypes with nested recursion, such as the type  oheimb@7490  2357 \texttt{term} mentioned in {\S}\ref{subsec:datatype:basics}, are  wenzelm@6580  2358 also defined by mutual primitive recursion. A substitution  wenzelm@6580  2359 function \texttt{subst_term} on type \texttt{term}, similar to the functions  berghofe@7044  2360 \texttt{substa} and \texttt{substb} described above, can  wenzelm@6580  2361 be defined as follows:  wenzelm@6580  2362 \begin{ttbox}  wenzelm@6580  2363 consts  paulson@9212  2364  subst_term :: "['a => ('a,'b) term, ('a,'b) term] => ('a,'b) term"  wenzelm@6580  2365  subst_term_list ::  paulson@9212  2366  "['a => ('a,'b) term, ('a,'b) term list] => ('a,'b) term list"  wenzelm@6580  2367 wenzelm@6580  2368 primrec  wenzelm@6580  2369  "subst_term f (Var a) = f a"  wenzelm@6580  2370  "subst_term f (App b ts) = App b (subst_term_list f ts)"  wenzelm@6580  2371 wenzelm@6580  2372  "subst_term_list f [] = []"  wenzelm@6580  2373  "subst_term_list f (t # ts) =  wenzelm@6580  2374  subst_term f t # subst_term_list f ts"  wenzelm@6580  2375 \end{ttbox}  wenzelm@6580  2376 The recursion scheme follows the structure of the unfolded definition of type  oheimb@7490  2377 \texttt{term} shown in {\S}\ref{subsec:datatype:basics}. To prove properties of  wenzelm@6580  2378 this substitution function, mutual induction is needed:  wenzelm@6580  2379 \begin{ttbox}  wenzelm@6580  2380 Goal  wenzelm@6580  2381  "(subst_term ((subst_term f1) o f2) t) =  wenzelm@6580  2382  (subst_term f1 (subst_term f2 t)) &  wenzelm@6580  2383  (subst_term_list ((subst_term f1) o f2) ts) =  wenzelm@6580  2384  (subst_term_list f1 (subst_term_list f2 ts))";  berghofe@7846  2385 by (induct_tac "t ts" 1);  wenzelm@6580  2386 by (ALLGOALS Asm_full_simp_tac);  wenzelm@6580  2387 \end{ttbox}  wenzelm@6580  2388 berghofe@7044  2389 \subsubsection{Example: A map function for infinitely branching trees}  berghofe@7044  2390 Defining functions on infinitely branching datatypes by primitive  berghofe@7044  2391 recursion is just as easy. For example, we can define a function  berghofe@7044  2392 \texttt{map_tree} on \texttt{'a tree} as follows:  berghofe@7044  2393 \begin{ttbox}  berghofe@7044  2394 consts  berghofe@7044  2395  map_tree :: "('a => 'b) => 'a tree => 'b tree"  berghofe@7044  2396 berghofe@7044  2397 primrec  berghofe@7044  2398  "map_tree f (Atom a) = Atom (f a)"  berghofe@7044  2399  "map_tree f (Branch ts) = Branch (\%x. map_tree f (ts x))"  berghofe@7044  2400 \end{ttbox}  berghofe@7044  2401 Note that all occurrences of functions such as \texttt{ts} in the  berghofe@7044  2402 \texttt{primrec} clauses must be applied to an argument. In particular,  berghofe@7044  2403 \texttt{map_tree f o ts} is not allowed.  berghofe@7044  2404 wenzelm@6580  2405 \index{recursion!primitive|)}  wenzelm@6580  2406 \index{*primrec|)}  wenzelm@6580  2407 wenzelm@6580  2408 wenzelm@6580  2409 \subsection{General recursive functions}  wenzelm@6580  2410 \label{sec:HOL:recdef}  wenzelm@6580  2411 \index{recursion!general|(}  wenzelm@6580  2412 \index{*recdef|(}  wenzelm@6580  2413 wenzelm@6580  2414 Using \texttt{recdef}, you can declare functions involving nested recursion  wenzelm@6580  2415 and pattern-matching. Recursion need not involve datatypes and there are few  wenzelm@6580  2416 syntactic restrictions. Termination is proved by showing that each recursive  wenzelm@6580  2417 call makes the argument smaller in a suitable sense, which you specify by  wenzelm@6580  2418 supplying a well-founded relation.  wenzelm@6580  2419 wenzelm@6580  2420 Here is a simple example, the Fibonacci function. The first line declares  wenzelm@6580  2421 \texttt{fib} to be a constant. The well-founded relation is simply~$<$ (on  wenzelm@6580  2422 the natural numbers). Pattern-matching is used here: \texttt{1} is a  wenzelm@6580  2423 macro for \texttt{Suc~0}.  wenzelm@6580  2424 \begin{ttbox}  wenzelm@6580  2425 consts fib :: "nat => nat"  wenzelm@6580  2426 recdef fib "less_than"  wenzelm@6580  2427  "fib 0 = 0"  wenzelm@6580  2428  "fib 1 = 1"  wenzelm@6580  2429  "fib (Suc(Suc x)) = (fib x + fib (Suc x))"  wenzelm@6580  2430 \end{ttbox}  wenzelm@6580  2431 wenzelm@6580  2432 With \texttt{recdef}, function definitions may be incomplete, and patterns may  wenzelm@6580  2433 overlap, as in functional programming. The \texttt{recdef} package  wenzelm@6580  2434 disambiguates overlapping patterns by taking the order of rules into account.  wenzelm@6580  2435 For missing patterns, the function is defined to return a default value.  wenzelm@6580  2436 wenzelm@6580  2437 %For example, here is a declaration of the list function \cdx{hd}:  wenzelm@6580  2438 %\begin{ttbox}  wenzelm@6580  2439 %consts hd :: 'a list => 'a  wenzelm@6580  2440 %recdef hd "\{\}"  wenzelm@6580  2441 % "hd (x#l) = x"  wenzelm@6580  2442 %\end{ttbox}  wenzelm@6580  2443 %Because this function is not recursive, we may supply the empty well-founded  wenzelm@6580  2444 %relation, $\{\}$.  wenzelm@6580  2445 wenzelm@6580  2446 The well-founded relation defines a notion of smaller'' for the function's  wenzelm@6580  2447 argument type. The relation $\prec$ is \textbf{well-founded} provided it  wenzelm@6580  2448 admits no infinitely decreasing chains  wenzelm@6580  2449 $\cdots\prec x@n\prec\cdots\prec x@1.$  wenzelm@6580  2450 If the function's argument has type~$\tau$, then $\prec$ has to be a relation  wenzelm@6580  2451 over~$\tau$: it must have type $(\tau\times\tau)set$.  wenzelm@6580  2452 wenzelm@6580  2453 Proving well-foundedness can be tricky, so Isabelle/HOL provides a collection  wenzelm@6580  2454 of operators for building well-founded relations. The package recognises  wenzelm@6580  2455 these operators and automatically proves that the constructed relation is  wenzelm@6580  2456 well-founded. Here are those operators, in order of importance:  wenzelm@6580  2457 \begin{itemize}  wenzelm@6580  2458 \item \texttt{less_than} is less than'' on the natural numbers.  wenzelm@6580  2459  (It has type $(nat\times nat)set$, while $<$ has type $[nat,nat]\To bool$.  wenzelm@6580  2460   wenzelm@6580  2461 \item $\mathop{\mathtt{measure}} f$, where $f$ has type $\tau\To nat$, is the  paulson@9258  2462  relation~$\prec$ on type~$\tau$ such that $x\prec y$ if and only if  paulson@9258  2463  $f(x)}R@2$ is the lexicographic product of two relations.  paulson@11242  2476  It  paulson@9258  2477  is a relation on pairs and satisfies $(x@1,x@2)\prec(y@1,y@2)$ if and only  paulson@9258  2478  if $x@1$  wenzelm@6580  2479  is less than $y@1$ according to~$R@1$ or $x@1=y@1$ and $x@2$  wenzelm@6580  2480  is less than $y@2$ according to~$R@2$.  wenzelm@6580  2481 wenzelm@6580  2482 \item \texttt{finite_psubset} is the proper subset relation on finite sets.  wenzelm@6580  2483 \end{itemize}  wenzelm@6580  2484 wenzelm@6580  2485 We can use \texttt{measure} to declare Euclid's algorithm for the greatest  wenzelm@6580  2486 common divisor. The measure function, $\lambda(m,n). n$, specifies that the  wenzelm@6580  2487 recursion terminates because argument~$n$ decreases.  wenzelm@6580  2488 \begin{ttbox}  wenzelm@6580  2489 recdef gcd "measure ((\%(m,n). n) ::nat*nat=>nat)"  wenzelm@6580  2490  "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"  wenzelm@6580  2491 \end{ttbox}  wenzelm@6580  2492 wenzelm@6580  2493 The general form of a well-founded recursive definition is  wenzelm@6580  2494 \begin{ttbox}  wenzelm@6580  2495 recdef {\it function} {\it rel}  wenzelm@6580  2496  congs {\it congruence rules} {\bf(optional)}  wenzelm@6580  2497  simpset {\it simplification set} {\bf(optional)}  wenzelm@6580  2498  {\it reduction rules}  wenzelm@6580  2499 \end{ttbox}  wenzelm@6580  2500 where  wenzelm@6580  2501 \begin{itemize}  wenzelm@6580  2502 \item \textit{function} is the name of the function, either as an \textit{id}  wenzelm@6580  2503  or a \textit{string}.  wenzelm@6580  2504   wenzelm@9695  2505 \item \textit{rel} is a HOL expression for the well-founded termination  wenzelm@6580  2506  relation.  wenzelm@6580  2507   wenzelm@6580  2508 \item \textit{congruence rules} are required only in highly exceptional  wenzelm@6580  2509  circumstances.  wenzelm@6580  2510   wenzelm@6580  2511 \item The \textit{simplification set} is used to prove that the supplied  wenzelm@6580  2512  relation is well-founded. It is also used to prove the \textbf{termination  wenzelm@6580  2513  conditions}: assertions that arguments of recursive calls decrease under  wenzelm@6580  2514  \textit{rel}. By default, simplification uses \texttt{simpset()}, which  wenzelm@6580  2515  is sufficient to prove well-foundedness for the built-in relations listed  wenzelm@6580  2516  above.  wenzelm@6580  2517   wenzelm@6580  2518 \item \textit{reduction rules} specify one or more recursion equations. Each  wenzelm@6580  2519  left-hand side must have the form $f\,t$, where $f$ is the function and $t$  wenzelm@6580  2520  is a tuple of distinct variables. If more than one equation is present then  wenzelm@6580  2521  $f$ is defined by pattern-matching on components of its argument whose type  wenzelm@6580  2522  is a \texttt{datatype}.  wenzelm@6580  2523 nipkow@8628  2524  The \ML\ identifier $f$\texttt{.simps} contains the reduction rules as  nipkow@8628  2525  a list of theorems.  wenzelm@6580  2526 \end{itemize}  wenzelm@6580  2527 wenzelm@6580  2528 With the definition of \texttt{gcd} shown above, Isabelle/HOL is unable to  wenzelm@6580  2529 prove one termination condition. It remains as a precondition of the  nipkow@8628  2530 recursion theorems:  wenzelm@6580  2531 \begin{ttbox}  nipkow@8628  2532 gcd.simps;  wenzelm@6580  2533 {\out ["! m n. n ~= 0 --> m mod n < n}  paulson@9212  2534 {\out ==> gcd (?m,?n) = (if ?n=0 then ?m else gcd (?n, ?m mod ?n))"] }  wenzelm@6580  2535 {\out : thm list}  wenzelm@6580  2536 \end{ttbox}  wenzelm@6580  2537 The theory \texttt{HOL/ex/Primes} illustrates how to prove termination  wenzelm@6580  2538 conditions afterwards. The function \texttt{Tfl.tgoalw} is like the standard  wenzelm@6580  2539 function \texttt{goalw}, which sets up a goal to prove, but its argument  nipkow@8628  2540 should be the identifier $f$\texttt{.simps} and its effect is to set up a  wenzelm@6580  2541 proof of the termination conditions:  wenzelm@6580  2542 \begin{ttbox}  nipkow@8628  2543 Tfl.tgoalw thy [] gcd.simps;  wenzelm@6580  2544 {\out Level 0}  wenzelm@6580  2545 {\out ! m n. n ~= 0 --> m mod n < n}  wenzelm@6580  2546 {\out 1. ! m n. n ~= 0 --> m mod n < n}  wenzelm@6580  2547 \end{ttbox}  wenzelm@6580  2548 This subgoal has a one-step proof using \texttt{simp_tac}. Once the theorem  wenzelm@6580  2549 is proved, it can be used to eliminate the termination conditions from  nipkow@8628  2550 elements of \texttt{gcd.simps}. Theory \texttt{HOL/Subst/Unify} is a much  wenzelm@6580  2551 more complicated example of this process, where the termination conditions can  wenzelm@6580  2552 only be proved by complicated reasoning involving the recursive function  wenzelm@6580  2553 itself.  wenzelm@6580  2554 wenzelm@6580  2555 Isabelle/HOL can prove the \texttt{gcd} function's termination condition  wenzelm@6580  2556 automatically if supplied with the right simpset.  wenzelm@6580  2557 \begin{ttbox}  wenzelm@6580  2558 recdef gcd "measure ((\%(m,n). n) ::nat*nat=>nat)"  wenzelm@6580  2559  simpset "simpset() addsimps [mod_less_divisor, zero_less_eq]"  wenzelm@6580  2560  "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"  wenzelm@6580  2561 \end{ttbox}  wenzelm@6580  2562 nipkow@8628  2563 If all termination conditions were proved automatically, $f$\texttt{.simps}  nipkow@8628  2564 is added to the simpset automatically, just as in \texttt{primrec}.  nipkow@8628  2565 The simplification rules corresponding to clause $i$ (where counting starts  nipkow@8628  2566 at 0) are called $f$\texttt{.}$i$ and can be accessed as \texttt{thms  nipkow@8628  2567  "$f$.$i$"},  nipkow@8628  2568 which returns a list of theorems. Thus you can, for example, remove specific  nipkow@8628  2569 clauses from the simpset. Note that a single clause may give rise to a set of  nipkow@8628  2570 simplification rules in order to capture the fact that if clauses overlap,  nipkow@8628  2571 their order disambiguates them.  nipkow@8628  2572 wenzelm@6580  2573 A \texttt{recdef} definition also returns an induction rule specialised for  wenzelm@6580  2574 the recursive function. For the \texttt{gcd} function above, the induction  wenzelm@6580  2575 rule is  wenzelm@6580  2576 \begin{ttbox}  wenzelm@6580  2577 gcd.induct;  wenzelm@6580  2578 {\out "(!!m n. n ~= 0 --> ?P n (m mod n) ==> ?P m n) ==> ?P ?u ?v" : thm}  wenzelm@6580  2579 \end{ttbox}  wenzelm@6580  2580 This rule should be used to reason inductively about the \texttt{gcd}  wenzelm@6580  2581 function. It usually makes the induction hypothesis available at all  wenzelm@6580  2582 recursive calls, leading to very direct proofs. If any termination conditions  wenzelm@6580  2583 remain unproved, they will become additional premises of this rule.  wenzelm@6580  2584 wenzelm@6580  2585 \index{recursion!general|)}  wenzelm@6580  2586 \index{*recdef|)}  wenzelm@6580  2587 wenzelm@6580  2588 wenzelm@6580  2589 \section{Inductive and coinductive definitions}  wenzelm@6580  2590 \index{*inductive|(}  wenzelm@6580  2591 \index{*coinductive|(}  wenzelm@6580  2592 wenzelm@6580  2593 An {\bf inductive definition} specifies the least set~$R$ closed under given  wenzelm@6580  2594 rules. (Applying a rule to elements of~$R$ yields a result within~$R$.) For  wenzelm@6580  2595 example, a structural operational semantics is an inductive definition of an  wenzelm@6580  2596 evaluation relation. Dually, a {\bf coinductive definition} specifies the  wenzelm@6580  2597 greatest set~$R$ consistent with given rules. (Every element of~$R$ can be  wenzelm@6580  2598 seen as arising by applying a rule to elements of~$R$.) An important example  wenzelm@6580  2599 is using bisimulation relations to formalise equivalence of processes and  wenzelm@6580  2600 infinite data structures.  wenzelm@6580  2601 wenzelm@6580  2602 A theory file may contain any number of inductive and coinductive  wenzelm@6580  2603 definitions. They may be intermixed with other declarations; in  wenzelm@6580  2604 particular, the (co)inductive sets {\bf must} be declared separately as  wenzelm@6580  2605 constants, and may have mixfix syntax or be subject to syntax translations.  wenzelm@6580  2606 wenzelm@6580  2607 Each (co)inductive definition adds definitions to the theory and also  wenzelm@6580  2608 proves some theorems. Each definition creates an \ML\ structure, which is a  wenzelm@6580  2609 substructure of the main theory structure.  wenzelm@6580  2610 wenzelm@9695  2611 This package is related to the ZF one, described in a separate  wenzelm@6580  2612 paper,%  wenzelm@6580  2613 \footnote{It appeared in CADE~\cite{paulson-CADE}; a longer version is  wenzelm@6580  2614  distributed with Isabelle.} %  wenzelm@6580  2615 which you should refer to in case of difficulties. The package is simpler  wenzelm@9695  2616 than ZF's thanks to HOL's extra-logical automatic type-checking. The types of  wenzelm@9695  2617 the (co)inductive sets determine the domain of the fixedpoint definition, and  wenzelm@9695  2618 the package does not have to use inference rules for type-checking.  wenzelm@6580  2619 wenzelm@6580  2620 wenzelm@6580  2621 \subsection{The result structure}  wenzelm@6580  2622 Many of the result structure's components have been discussed in the paper;  wenzelm@6580  2623 others are self-explanatory.  wenzelm@6580  2624 \begin{description}  wenzelm@6580  2625 \item[\tt defs] is the list of definitions of the recursive sets.