1\chapter{Higher-Order Logic} 2\index{higher-order logic|(} 3\index{HOL system@{\sc hol} system} 4 5This chapter describes Isabelle's formalization of Higher-Order Logic, a 6polymorphic version of Church's Simple Theory of Types. HOL can be best 7understood as a simply-typed version of classical set theory. The monograph 8\emph{Isabelle/HOL --- A Proof Assistant for Higher-Order Logic} provides a 9gentle introduction on using Isabelle/HOL in practice. 10All of this material is mainly of historical interest! 11 12\begin{figure} 13\begin{constants} 14 \it name &\it meta-type & \it description \\ 15 \cdx{Trueprop}& $bool\To prop$ & coercion to $prop$\\ 16 \cdx{Not} & $bool\To bool$ & negation ($\lnot$) \\ 17 \cdx{True} & $bool$ & tautology ($\top$) \\ 18 \cdx{False} & $bool$ & absurdity ($\bot$) \\ 19 \cdx{If} & $[bool,\alpha,\alpha]\To\alpha$ & conditional \\ 20 \cdx{Let} & $[\alpha,\alpha\To\beta]\To\beta$ & let binder 21\end{constants} 22\subcaption{Constants} 23 24\begin{constants} 25\index{"@@{\tt\at} symbol} 26\index{*"! symbol}\index{*"? symbol} 27\index{*"?"! symbol}\index{*"E"X"! symbol} 28 \it symbol &\it name &\it meta-type & \it description \\ 29 \sdx{SOME} or \tt\at & \cdx{Eps} & $(\alpha\To bool)\To\alpha$ & 30 Hilbert description ($\varepsilon$) \\ 31 \sdx{ALL} or {\tt!~} & \cdx{All} & $(\alpha\To bool)\To bool$ & 32 universal quantifier ($\forall$) \\ 33 \sdx{EX} or {\tt?~} & \cdx{Ex} & $(\alpha\To bool)\To bool$ & 34 existential quantifier ($\exists$) \\ 35 \texttt{EX!} or {\tt?!} & \cdx{Ex1} & $(\alpha\To bool)\To bool$ & 36 unique existence ($\exists!$)\\ 37 \texttt{LEAST} & \cdx{Least} & $(\alpha::ord \To bool)\To\alpha$ & 38 least element 39\end{constants} 40\subcaption{Binders} 41 42\begin{constants} 43\index{*"= symbol} 44\index{&@{\tt\&} symbol} 45\index{"!@{\tt\char124} symbol} %\char124 is vertical bar. We use ! because | stopped working 46\index{*"-"-"> symbol} 47 \it symbol & \it meta-type & \it priority & \it description \\ 48 \sdx{o} & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ & 49 Left 55 & composition ($\circ$) \\ 50 \tt = & $[\alpha,\alpha]\To bool$ & Left 50 & equality ($=$) \\ 51 \tt < & $[\alpha::ord,\alpha]\To bool$ & Left 50 & less than ($<$) \\ 52 \tt <= & $[\alpha::ord,\alpha]\To bool$ & Left 50 & 53 less than or equals ($\leq$)\\ 54 \tt \& & $[bool,bool]\To bool$ & Right 35 & conjunction ($\conj$) \\ 55 \tt | & $[bool,bool]\To bool$ & Right 30 & disjunction ($\disj$) \\ 56 \tt --> & $[bool,bool]\To bool$ & Right 25 & implication ($\imp$) 57\end{constants} 58\subcaption{Infixes} 59\caption{Syntax of \texttt{HOL}} \label{hol-constants} 60\end{figure} 61 62 63\begin{figure} 64\index{*let symbol} 65\index{*in symbol} 66\dquotes 67\[\begin{array}{rclcl} 68 term & = & \hbox{expression of class~$term$} \\ 69 & | & "SOME~" id " . " formula 70 & | & "\at~" id " . " formula \\ 71 & | & 72 \multicolumn{3}{l}{"let"~id~"="~term";"\dots";"~id~"="~term~"in"~term} \\ 73 & | & 74 \multicolumn{3}{l}{"if"~formula~"then"~term~"else"~term} \\ 75 & | & "LEAST"~ id " . " formula \\[2ex] 76 formula & = & \hbox{expression of type~$bool$} \\ 77 & | & term " = " term \\ 78 & | & term " \ttilde= " term \\ 79 & | & term " < " term \\ 80 & | & term " <= " term \\ 81 & | & "\ttilde\ " formula \\ 82 & | & formula " \& " formula \\ 83 & | & formula " | " formula \\ 84 & | & formula " --> " formula \\ 85 & | & "ALL~" id~id^* " . " formula 86 & | & "!~~~" id~id^* " . " formula \\ 87 & | & "EX~~" id~id^* " . " formula 88 & | & "?~~~" id~id^* " . " formula \\ 89 & | & "EX!~" id~id^* " . " formula 90 & | & "?!~~" id~id^* " . " formula \\ 91 \end{array} 92\] 93\caption{Full grammar for HOL} \label{hol-grammar} 94\end{figure} 95 96 97\section{Syntax} 98 99Figure~\ref{hol-constants} lists the constants (including infixes and 100binders), while Fig.\ts\ref{hol-grammar} presents the grammar of 101higher-order logic. Note that $a$\verb|~=|$b$ is translated to 102$\lnot(a=b)$. 103 104\begin{warn} 105 HOL has no if-and-only-if connective; logical equivalence is expressed using 106 equality. But equality has a high priority, as befitting a relation, while 107 if-and-only-if typically has the lowest priority. Thus, $\lnot\lnot P=P$ 108 abbreviates $\lnot\lnot (P=P)$ and not $(\lnot\lnot P)=P$. When using $=$ 109 to mean logical equivalence, enclose both operands in parentheses. 110\end{warn} 111 112\subsection{Types and overloading} 113The universal type class of higher-order terms is called~\cldx{term}. 114By default, explicit type variables have class \cldx{term}. In 115particular the equality symbol and quantifiers are polymorphic over 116class \texttt{term}. 117 118The type of formulae, \tydx{bool}, belongs to class \cldx{term}; thus, 119formulae are terms. The built-in type~\tydx{fun}, which constructs 120function types, is overloaded with arity {\tt(term,\thinspace 121 term)\thinspace term}. Thus, $\sigma\To\tau$ belongs to class~{\tt 122 term} if $\sigma$ and~$\tau$ do, allowing quantification over 123functions. 124 125HOL allows new types to be declared as subsets of existing types, 126either using the primitive \texttt{typedef} or the more convenient 127\texttt{datatype} (see~{\S}\ref{sec:HOL:datatype}). 128 129Several syntactic type classes --- \cldx{plus}, \cldx{minus}, 130\cldx{times} and 131\cldx{power} --- permit overloading of the operators {\tt+},\index{*"+ 132 symbol} {\tt-}\index{*"- symbol}, {\tt*}.\index{*"* symbol} 133and \verb|^|.\index{^@\verb.^. symbol} 134% 135They are overloaded to denote the obvious arithmetic operations on types 136\tdx{nat}, \tdx{int} and~\tdx{real}. (With the \verb|^| operator, the 137exponent always has type~\tdx{nat}.) Non-arithmetic overloadings are also 138done: the operator {\tt-} can denote set difference, while \verb|^| can 139denote exponentiation of relations (iterated composition). Unary minus is 140also written as~{\tt-} and is overloaded like its 2-place counterpart; it even 141can stand for set complement. 142 143The constant \cdx{0} is also overloaded. It serves as the zero element of 144several types, of which the most important is \tdx{nat} (the natural 145numbers). The type class \cldx{plus_ac0} comprises all types for which 0 146and~+ satisfy the laws $x+y=y+x$, $(x+y)+z = x+(y+z)$ and $0+x = x$. These 147types include the numeric ones \tdx{nat}, \tdx{int} and~\tdx{real} and also 148multisets. The summation operator \cdx{sum} is available for all types in 149this class. 150 151Theory \thydx{Ord} defines the syntactic class \cldx{ord} of order 152signatures. The relations $<$ and $\leq$ are polymorphic over this 153class, as are the functions \cdx{mono}, \cdx{min} and \cdx{max}, and 154the \cdx{LEAST} operator. \thydx{Ord} also defines a subclass 155\cldx{order} of \cldx{ord} which axiomatizes the types that are partially 156ordered with respect to~$\leq$. A further subclass \cldx{linorder} of 157\cldx{order} axiomatizes linear orderings. 158For details, see the file \texttt{Ord.thy}. 159 160If you state a goal containing overloaded functions, you may need to include 161type constraints. Type inference may otherwise make the goal more 162polymorphic than you intended, with confusing results. For example, the 163variables $i$, $j$ and $k$ in the goal $i \leq j \Imp i \leq j+k$ have type 164$\alpha::\{ord,plus\}$, although you may have expected them to have some 165numeric type, e.g. $nat$. Instead you should have stated the goal as 166$(i::nat) \leq j \Imp i \leq j+k$, which causes all three variables to have 167type $nat$. 168 169\begin{warn} 170 If resolution fails for no obvious reason, try setting 171 \ttindex{show_types} to \texttt{true}, causing Isabelle to display 172 types of terms. Possibly set \ttindex{show_sorts} to \texttt{true} as 173 well, causing Isabelle to display type classes and sorts. 174 175 \index{unification!incompleteness of} 176 Where function types are involved, Isabelle's unification code does not 177 guarantee to find instantiations for type variables automatically. Be 178 prepared to use \ttindex{res_inst_tac} instead of \texttt{resolve_tac}, 179 possibly instantiating type variables. Setting 180 \ttindex{Unify.trace_types} to \texttt{true} causes Isabelle to report 181 omitted search paths during unification.\index{tracing!of unification} 182\end{warn} 183 184 185\subsection{Binders} 186 187Hilbert's {\bf description} operator~$\varepsilon x. P[x]$ stands for some~$x$ 188satisfying~$P$, if such exists. Since all terms in HOL denote something, a 189description is always meaningful, but we do not know its value unless $P$ 190defines it uniquely. We may write descriptions as \cdx{Eps}($\lambda x. 191P[x]$) or use the syntax \hbox{\tt SOME~$x$.~$P[x]$}. 192 193Existential quantification is defined by 194\[ \exists x. P~x \;\equiv\; P(\varepsilon x. P~x). \] 195The unique existence quantifier, $\exists!x. P$, is defined in terms 196of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested 197quantifications. For instance, $\exists!x\,y. P\,x\,y$ abbreviates 198$\exists!x. \exists!y. P\,x\,y$; note that this does not mean that there 199exists a unique pair $(x,y)$ satisfying~$P\,x\,y$. 200 201\medskip 202 203\index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system} The 204basic Isabelle/HOL binders have two notations. Apart from the usual 205\texttt{ALL} and \texttt{EX} for $\forall$ and $\exists$, Isabelle/HOL also 206supports the original notation of Gordon's {\sc hol} system: \texttt{!}\ 207and~\texttt{?}. In the latter case, the existential quantifier \emph{must} be 208followed by a space; thus {\tt?x} is an unknown, while \verb'? x. f x=y' is a 209quantification. Both notations are accepted for input. The print mode 210``\ttindexbold{HOL}'' governs the output notation. If enabled (e.g.\ by 211passing option \texttt{-m HOL} to the \texttt{isabelle} executable), 212then~{\tt!}\ and~{\tt?}\ are displayed. 213 214\medskip 215 216If $\tau$ is a type of class \cldx{ord}, $P$ a formula and $x$ a 217variable of type $\tau$, then the term \cdx{LEAST}~$x. P[x]$ is defined 218to be the least (w.r.t.\ $\leq$) $x$ such that $P~x$ holds (see 219Fig.~\ref{hol-defs}). The definition uses Hilbert's $\varepsilon$ 220choice operator, so \texttt{Least} is always meaningful, but may yield 221nothing useful in case there is not a unique least element satisfying 222$P$.\footnote{Class $ord$ does not require much of its instances, so 223 $\leq$ need not be a well-ordering, not even an order at all!} 224 225\medskip All these binders have priority 10. 226 227\begin{warn} 228The low priority of binders means that they need to be enclosed in 229parenthesis when they occur in the context of other operations. For example, 230instead of $P \land \forall x. Q$ you need to write $P \land (\forall x. Q)$. 231\end{warn} 232 233 234\subsection{The let and case constructions} 235Local abbreviations can be introduced by a \texttt{let} construct whose 236syntax appears in Fig.\ts\ref{hol-grammar}. Internally it is translated into 237the constant~\cdx{Let}. It can be expanded by rewriting with its 238definition, \tdx{Let_def}. 239 240HOL also defines the basic syntax 241\[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n\] 242as a uniform means of expressing \texttt{case} constructs. Therefore \texttt{case} 243and \sdx{of} are reserved words. Initially, this is mere syntax and has no 244logical meaning. By declaring translations, you can cause instances of the 245\texttt{case} construct to denote applications of particular case operators. 246This is what happens automatically for each \texttt{datatype} definition 247(see~{\S}\ref{sec:HOL:datatype}). 248 249\begin{warn} 250Both \texttt{if} and \texttt{case} constructs have as low a priority as 251quantifiers, which requires additional enclosing parentheses in the context 252of most other operations. For example, instead of $f~x = {\tt if\dots 253then\dots else}\dots$ you need to write $f~x = ({\tt if\dots then\dots 254else\dots})$. 255\end{warn} 256 257\section{Rules of inference} 258 259\begin{figure} 260\begin{ttbox}\makeatother 261\tdx{refl} t = (t::'a) 262\tdx{subst} [| s = t; P s |] ==> P (t::'a) 263\tdx{ext} (!!x::'a. (f x :: 'b) = g x) ==> (\%x. f x) = (\%x. g x) 264\tdx{impI} (P ==> Q) ==> P-->Q 265\tdx{mp} [| P-->Q; P |] ==> Q 266\tdx{iff} (P-->Q) --> (Q-->P) --> (P=Q) 267\tdx{someI} P(x::'a) ==> P(@x. P x) 268\tdx{True_or_False} (P=True) | (P=False) 269\end{ttbox} 270\caption{The \texttt{HOL} rules} \label{hol-rules} 271\end{figure} 272 273Figure~\ref{hol-rules} shows the primitive inference rules of~HOL, with 274their~{\ML} names. Some of the rules deserve additional comments: 275\begin{ttdescription} 276\item[\tdx{ext}] expresses extensionality of functions. 277\item[\tdx{iff}] asserts that logically equivalent formulae are 278 equal. 279\item[\tdx{someI}] gives the defining property of the Hilbert 280 $\varepsilon$-operator. It is a form of the Axiom of Choice. The derived rule 281 \tdx{some_equality} (see below) is often easier to use. 282\item[\tdx{True_or_False}] makes the logic classical.\footnote{In 283 fact, the $\varepsilon$-operator already makes the logic classical, as 284 shown by Diaconescu; see Paulson~\cite{paulson-COLOG} for details.} 285\end{ttdescription} 286 287 288\begin{figure}\hfuzz=4pt%suppress "Overfull \hbox" message 289\begin{ttbox}\makeatother 290\tdx{True_def} True == ((\%x::bool. x)=(\%x. x)) 291\tdx{All_def} All == (\%P. P = (\%x. True)) 292\tdx{Ex_def} Ex == (\%P. P(@x. P x)) 293\tdx{False_def} False == (!P. P) 294\tdx{not_def} not == (\%P. P-->False) 295\tdx{and_def} op & == (\%P Q. !R. (P-->Q-->R) --> R) 296\tdx{or_def} op | == (\%P Q. !R. (P-->R) --> (Q-->R) --> R) 297\tdx{Ex1_def} Ex1 == (\%P. ? x. P x & (! y. P y --> y=x)) 298 299\tdx{o_def} op o == (\%(f::'b=>'c) g x::'a. f(g x)) 300\tdx{if_def} If P x y == 301 (\%P x y. @z::'a.(P=True --> z=x) & (P=False --> z=y)) 302\tdx{Let_def} Let s f == f s 303\tdx{Least_def} Least P == @x. P(x) & (ALL y. P(y) --> x <= y)" 304\end{ttbox} 305\caption{The \texttt{HOL} definitions} \label{hol-defs} 306\end{figure} 307 308 309HOL follows standard practice in higher-order logic: only a few connectives 310are taken as primitive, with the remainder defined obscurely 311(Fig.\ts\ref{hol-defs}). Gordon's {\sc hol} system expresses the 312corresponding definitions \cite[page~270]{mgordon-hol} using 313object-equality~({\tt=}), which is possible because equality in higher-order 314logic may equate formulae and even functions over formulae. But theory~HOL, 315like all other Isabelle theories, uses meta-equality~({\tt==}) for 316definitions. 317\begin{warn} 318The definitions above should never be expanded and are shown for completeness 319only. Instead users should reason in terms of the derived rules shown below 320or, better still, using high-level tactics. 321\end{warn} 322 323Some of the rules mention type variables; for example, \texttt{refl} 324mentions the type variable~{\tt'a}. This allows you to instantiate 325type variables explicitly by calling \texttt{res_inst_tac}. 326 327 328\begin{figure} 329\begin{ttbox} 330\tdx{sym} s=t ==> t=s 331\tdx{trans} [| r=s; s=t |] ==> r=t 332\tdx{ssubst} [| t=s; P s |] ==> P t 333\tdx{box_equals} [| a=b; a=c; b=d |] ==> c=d 334\tdx{arg_cong} x = y ==> f x = f y 335\tdx{fun_cong} f = g ==> f x = g x 336\tdx{cong} [| f = g; x = y |] ==> f x = g y 337\tdx{not_sym} t ~= s ==> s ~= t 338\subcaption{Equality} 339 340\tdx{TrueI} True 341\tdx{FalseE} False ==> P 342 343\tdx{conjI} [| P; Q |] ==> P&Q 344\tdx{conjunct1} [| P&Q |] ==> P 345\tdx{conjunct2} [| P&Q |] ==> Q 346\tdx{conjE} [| P&Q; [| P; Q |] ==> R |] ==> R 347 348\tdx{disjI1} P ==> P|Q 349\tdx{disjI2} Q ==> P|Q 350\tdx{disjE} [| P | Q; P ==> R; Q ==> R |] ==> R 351 352\tdx{notI} (P ==> False) ==> ~ P 353\tdx{notE} [| ~ P; P |] ==> R 354\tdx{impE} [| P-->Q; P; Q ==> R |] ==> R 355\subcaption{Propositional logic} 356 357\tdx{iffI} [| P ==> Q; Q ==> P |] ==> P=Q 358\tdx{iffD1} [| P=Q; P |] ==> Q 359\tdx{iffD2} [| P=Q; Q |] ==> P 360\tdx{iffE} [| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R 361\subcaption{Logical equivalence} 362 363\end{ttbox} 364\caption{Derived rules for HOL} \label{hol-lemmas1} 365\end{figure} 366% 367%\tdx{eqTrueI} P ==> P=True 368%\tdx{eqTrueE} P=True ==> P 369 370 371\begin{figure} 372\begin{ttbox}\makeatother 373\tdx{allI} (!!x. P x) ==> !x. P x 374\tdx{spec} !x. P x ==> P x 375\tdx{allE} [| !x. P x; P x ==> R |] ==> R 376\tdx{all_dupE} [| !x. P x; [| P x; !x. P x |] ==> R |] ==> R 377 378\tdx{exI} P x ==> ? x. P x 379\tdx{exE} [| ? x. P x; !!x. P x ==> Q |] ==> Q 380 381\tdx{ex1I} [| P a; !!x. P x ==> x=a |] ==> ?! x. P x 382\tdx{ex1E} [| ?! x. P x; !!x. [| P x; ! y. P y --> y=x |] ==> R 383 |] ==> R 384 385\tdx{some_equality} [| P a; !!x. P x ==> x=a |] ==> (@x. P x) = a 386\subcaption{Quantifiers and descriptions} 387 388\tdx{ccontr} (~P ==> False) ==> P 389\tdx{classical} (~P ==> P) ==> P 390\tdx{excluded_middle} ~P | P 391 392\tdx{disjCI} (~Q ==> P) ==> P|Q 393\tdx{exCI} (! x. ~ P x ==> P a) ==> ? x. P x 394\tdx{impCE} [| P-->Q; ~ P ==> R; Q ==> R |] ==> R 395\tdx{iffCE} [| P=Q; [| P;Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R 396\tdx{notnotD} ~~P ==> P 397\tdx{swap} ~P ==> (~Q ==> P) ==> Q 398\subcaption{Classical logic} 399 400\tdx{if_P} P ==> (if P then x else y) = x 401\tdx{if_not_P} ~ P ==> (if P then x else y) = y 402\tdx{split_if} P(if Q then x else y) = ((Q --> P x) & (~Q --> P y)) 403\subcaption{Conditionals} 404\end{ttbox} 405\caption{More derived rules} \label{hol-lemmas2} 406\end{figure} 407 408Some derived rules are shown in Figures~\ref{hol-lemmas1} 409and~\ref{hol-lemmas2}, with their {\ML} names. These include natural rules 410for the logical connectives, as well as sequent-style elimination rules for 411conjunctions, implications, and universal quantifiers. 412 413Note the equality rules: \tdx{ssubst} performs substitution in 414backward proofs, while \tdx{box_equals} supports reasoning by 415simplifying both sides of an equation. 416 417The following simple tactics are occasionally useful: 418\begin{ttdescription} 419\item[\ttindexbold{strip_tac} $i$] applies \texttt{allI} and \texttt{impI} 420 repeatedly to remove all outermost universal quantifiers and implications 421 from subgoal $i$. 422\item[\ttindexbold{case_tac} {\tt"}$P${\tt"} $i$] performs case distinction on 423 $P$ for subgoal $i$: the latter is replaced by two identical subgoals with 424 the added assumptions $P$ and $\lnot P$, respectively. 425\item[\ttindexbold{smp_tac} $j$ $i$] applies $j$ times \texttt{spec} and then 426 \texttt{mp} in subgoal $i$, which is typically useful when forward-chaining 427 from an induction hypothesis. As a generalization of \texttt{mp_tac}, 428 if there are assumptions $\forall \vec{x}. P \vec{x} \imp Q \vec{x}$ and 429 $P \vec{a}$, ($\vec{x}$ being a vector of $j$ variables) 430 then it replaces the universally quantified implication by $Q \vec{a}$. 431 It may instantiate unknowns. It fails if it can do nothing. 432\end{ttdescription} 433 434 435\begin{figure} 436\begin{center} 437\begin{tabular}{rrr} 438 \it name &\it meta-type & \it description \\ 439\index{{}@\verb'{}' symbol} 440 \verb|{}| & $\alpha\,set$ & the empty set \\ 441 \cdx{insert} & $[\alpha,\alpha\,set]\To \alpha\,set$ 442 & insertion of element \\ 443 \cdx{Collect} & $(\alpha\To bool)\To\alpha\,set$ 444 & comprehension \\ 445 \cdx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$ 446 & intersection over a set\\ 447 \cdx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$ 448 & union over a set\\ 449 \cdx{Inter} & $(\alpha\,set)set\To\alpha\,set$ 450 &set of sets intersection \\ 451 \cdx{Union} & $(\alpha\,set)set\To\alpha\,set$ 452 &set of sets union \\ 453 \cdx{Pow} & $\alpha\,set \To (\alpha\,set)set$ 454 & powerset \\[1ex] 455 \cdx{range} & $(\alpha\To\beta )\To\beta\,set$ 456 & range of a function \\[1ex] 457 \cdx{Ball}~~\cdx{Bex} & $[\alpha\,set,\alpha\To bool]\To bool$ 458 & bounded quantifiers 459\end{tabular} 460\end{center} 461\subcaption{Constants} 462 463\begin{center} 464\begin{tabular}{llrrr} 465 \it symbol &\it name &\it meta-type & \it priority & \it description \\ 466 \sdx{INT} & \cdx{INTER1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 & 467 intersection\\ 468 \sdx{UN} & \cdx{UNION1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 & 469 union 470\end{tabular} 471\end{center} 472\subcaption{Binders} 473 474\begin{center} 475\index{*"`"` symbol} 476\index{*": symbol} 477\index{*"<"= symbol} 478\begin{tabular}{rrrr} 479 \it symbol & \it meta-type & \it priority & \it description \\ 480 \tt `` & $[\alpha\To\beta ,\alpha\,set]\To \beta\,set$ 481 & Left 90 & image \\ 482 \sdx{Int} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$ 483 & Left 70 & intersection ($\int$) \\ 484 \sdx{Un} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$ 485 & Left 65 & union ($\un$) \\ 486 \tt: & $[\alpha ,\alpha\,set]\To bool$ 487 & Left 50 & membership ($\in$) \\ 488 \tt <= & $[\alpha\,set,\alpha\,set]\To bool$ 489 & Left 50 & subset ($\subseteq$) 490\end{tabular} 491\end{center} 492\subcaption{Infixes} 493\caption{Syntax of the theory \texttt{Set}} \label{hol-set-syntax} 494\end{figure} 495 496 497\begin{figure} 498\begin{center} \tt\frenchspacing 499\index{*"! symbol} 500\begin{tabular}{rrr} 501 \it external & \it internal & \it description \\ 502 $a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm not in\\ 503 {\ttlbrace}$a@1$, $\ldots${\ttrbrace} & insert $a@1$ $\ldots$ {\ttlbrace}{\ttrbrace} & \rm finite set \\ 504 {\ttlbrace}$x$. $P[x]${\ttrbrace} & Collect($\lambda x. P[x]$) & 505 \rm comprehension \\ 506 \sdx{INT} $x$:$A$. $B[x]$ & INTER $A$ $\lambda x. B[x]$ & 507 \rm intersection \\ 508 \sdx{UN}{\tt\ } $x$:$A$. $B[x]$ & UNION $A$ $\lambda x. B[x]$ & 509 \rm union \\ 510 \sdx{ALL} $x$:$A$.\ $P[x]$ or \texttt{!} $x$:$A$.\ $P[x]$ & 511 Ball $A$ $\lambda x.\ P[x]$ & 512 \rm bounded $\forall$ \\ 513 \sdx{EX}{\tt\ } $x$:$A$.\ $P[x]$ or \texttt{?} $x$:$A$.\ $P[x]$ & 514 Bex $A$ $\lambda x.\ P[x]$ & \rm bounded $\exists$ 515\end{tabular} 516\end{center} 517\subcaption{Translations} 518 519\dquotes 520\[\begin{array}{rclcl} 521 term & = & \hbox{other terms\ldots} \\ 522 & | & "{\ttlbrace}{\ttrbrace}" \\ 523 & | & "{\ttlbrace} " term\; ("," term)^* " {\ttrbrace}" \\ 524 & | & "{\ttlbrace} " id " . " formula " {\ttrbrace}" \\ 525 & | & term " `` " term \\ 526 & | & term " Int " term \\ 527 & | & term " Un " term \\ 528 & | & "INT~~" id ":" term " . " term \\ 529 & | & "UN~~~" id ":" term " . " term \\ 530 & | & "INT~~" id~id^* " . " term \\ 531 & | & "UN~~~" id~id^* " . " term \\[2ex] 532 formula & = & \hbox{other formulae\ldots} \\ 533 & | & term " : " term \\ 534 & | & term " \ttilde: " term \\ 535 & | & term " <= " term \\ 536 & | & "ALL " id ":" term " . " formula 537 & | & "!~" id ":" term " . " formula \\ 538 & | & "EX~~" id ":" term " . " formula 539 & | & "?~" id ":" term " . " formula \\ 540 \end{array} 541\] 542\subcaption{Full Grammar} 543\caption{Syntax of the theory \texttt{Set} (continued)} \label{hol-set-syntax2} 544\end{figure} 545 546 547\section{A formulation of set theory} 548Historically, higher-order logic gives a foundation for Russell and 549Whitehead's theory of classes. Let us use modern terminology and call them 550{\bf sets}, but note that these sets are distinct from those of ZF set theory, 551and behave more like ZF classes. 552\begin{itemize} 553\item 554Sets are given by predicates over some type~$\sigma$. Types serve to 555define universes for sets, but type-checking is still significant. 556\item 557There is a universal set (for each type). Thus, sets have complements, and 558may be defined by absolute comprehension. 559\item 560Although sets may contain other sets as elements, the containing set must 561have a more complex type. 562\end{itemize} 563Finite unions and intersections have the same behaviour in HOL as they do 564in~ZF. In HOL the intersection of the empty set is well-defined, denoting the 565universal set for the given type. 566 567\subsection{Syntax of set theory}\index{*set type} 568HOL's set theory is called \thydx{Set}. The type $\alpha\,set$ is essentially 569the same as $\alpha\To bool$. The new type is defined for clarity and to 570avoid complications involving function types in unification. The isomorphisms 571between the two types are declared explicitly. They are very natural: 572\texttt{Collect} maps $\alpha\To bool$ to $\alpha\,set$, while \hbox{\tt op :} 573maps in the other direction (ignoring argument order). 574 575Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax 576translations. Figure~\ref{hol-set-syntax2} presents the grammar of the new 577constructs. Infix operators include union and intersection ($A\un B$ 578and $A\int B$), the subset and membership relations, and the image 579operator~{\tt``}\@. Note that $a$\verb|~:|$b$ is translated to 580$\lnot(a\in b)$. 581 582The $\{a@1,\ldots\}$ notation abbreviates finite sets constructed in 583the obvious manner using~\texttt{insert} and~$\{\}$: 584\begin{eqnarray*} 585 \{a, b, c\} & \equiv & 586 \texttt{insert} \, a \, ({\tt insert} \, b \, ({\tt insert} \, c \, \{\})) 587\end{eqnarray*} 588 589The set \hbox{\tt{\ttlbrace}$x$.\ $P[x]${\ttrbrace}} consists of all $x$ (of 590suitable type) that satisfy~$P[x]$, where $P[x]$ is a formula that may contain 591free occurrences of~$x$. This syntax expands to \cdx{Collect}$(\lambda x. 592P[x])$. It defines sets by absolute comprehension, which is impossible in~ZF; 593the type of~$x$ implicitly restricts the comprehension. 594 595The set theory defines two {\bf bounded quantifiers}: 596\begin{eqnarray*} 597 \forall x\in A. P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\ 598 \exists x\in A. P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x] 599\end{eqnarray*} 600The constants~\cdx{Ball} and~\cdx{Bex} are defined 601accordingly. Instead of \texttt{Ball $A$ $P$} and \texttt{Bex $A$ $P$} we may 602write\index{*"! symbol}\index{*"? symbol} 603\index{*ALL symbol}\index{*EX symbol} 604% 605\hbox{\tt ALL~$x$:$A$.\ $P[x]$} and \hbox{\tt EX~$x$:$A$.\ $P[x]$}. The 606original notation of Gordon's {\sc hol} system is supported as well: 607\texttt{!}\ and \texttt{?}. 608 609Unions and intersections over sets, namely $\bigcup@{x\in A}B[x]$ and 610$\bigcap@{x\in A}B[x]$, are written 611\sdx{UN}~\hbox{\tt$x$:$A$.\ $B[x]$} and 612\sdx{INT}~\hbox{\tt$x$:$A$.\ $B[x]$}. 613 614Unions and intersections over types, namely $\bigcup@x B[x]$ and $\bigcap@x 615B[x]$, are written \sdx{UN}~\hbox{\tt$x$.\ $B[x]$} and 616\sdx{INT}~\hbox{\tt$x$.\ $B[x]$}. They are equivalent to the previous 617union and intersection operators when $A$ is the universal set. 618 619The operators $\bigcup A$ and $\bigcap A$ act upon sets of sets. They are 620not binders, but are equal to $\bigcup@{x\in A}x$ and $\bigcap@{x\in A}x$, 621respectively. 622 623 624 625\begin{figure} \underscoreon 626\begin{ttbox} 627\tdx{mem_Collect_eq} (a : {\ttlbrace}x. P x{\ttrbrace}) = P a 628\tdx{Collect_mem_eq} {\ttlbrace}x. x:A{\ttrbrace} = A 629 630\tdx{empty_def} {\ttlbrace}{\ttrbrace} == {\ttlbrace}x. False{\ttrbrace} 631\tdx{insert_def} insert a B == {\ttlbrace}x. x=a{\ttrbrace} Un B 632\tdx{Ball_def} Ball A P == ! x. x:A --> P x 633\tdx{Bex_def} Bex A P == ? x. x:A & P x 634\tdx{subset_def} A <= B == ! x:A. x:B 635\tdx{Un_def} A Un B == {\ttlbrace}x. x:A | x:B{\ttrbrace} 636\tdx{Int_def} A Int B == {\ttlbrace}x. x:A & x:B{\ttrbrace} 637\tdx{set_diff_def} A - B == {\ttlbrace}x. x:A & x~:B{\ttrbrace} 638\tdx{Compl_def} -A == {\ttlbrace}x. ~ x:A{\ttrbrace} 639\tdx{INTER_def} INTER A B == {\ttlbrace}y. ! x:A. y: B x{\ttrbrace} 640\tdx{UNION_def} UNION A B == {\ttlbrace}y. ? x:A. y: B x{\ttrbrace} 641\tdx{INTER1_def} INTER1 B == INTER {\ttlbrace}x. True{\ttrbrace} B 642\tdx{UNION1_def} UNION1 B == UNION {\ttlbrace}x. True{\ttrbrace} B 643\tdx{Inter_def} Inter S == (INT x:S. x) 644\tdx{Union_def} Union S == (UN x:S. x) 645\tdx{Pow_def} Pow A == {\ttlbrace}B. B <= A{\ttrbrace} 646\tdx{image_def} f``A == {\ttlbrace}y. ? x:A. y=f x{\ttrbrace} 647\tdx{range_def} range f == {\ttlbrace}y. ? x. y=f x{\ttrbrace} 648\end{ttbox} 649\caption{Rules of the theory \texttt{Set}} \label{hol-set-rules} 650\end{figure} 651 652 653\begin{figure} \underscoreon 654\begin{ttbox} 655\tdx{CollectI} [| P a |] ==> a : {\ttlbrace}x. P x{\ttrbrace} 656\tdx{CollectD} [| a : {\ttlbrace}x. P x{\ttrbrace} |] ==> P a 657\tdx{CollectE} [| a : {\ttlbrace}x. P x{\ttrbrace}; P a ==> W |] ==> W 658 659\tdx{ballI} [| !!x. x:A ==> P x |] ==> ! x:A. P x 660\tdx{bspec} [| ! x:A. P x; x:A |] ==> P x 661\tdx{ballE} [| ! x:A. P x; P x ==> Q; ~ x:A ==> Q |] ==> Q 662 663\tdx{bexI} [| P x; x:A |] ==> ? x:A. P x 664\tdx{bexCI} [| ! x:A. ~ P x ==> P a; a:A |] ==> ? x:A. P x 665\tdx{bexE} [| ? x:A. P x; !!x. [| x:A; P x |] ==> Q |] ==> Q 666\subcaption{Comprehension and Bounded quantifiers} 667 668\tdx{subsetI} (!!x. x:A ==> x:B) ==> A <= B 669\tdx{subsetD} [| A <= B; c:A |] ==> c:B 670\tdx{subsetCE} [| A <= B; ~ (c:A) ==> P; c:B ==> P |] ==> P 671 672\tdx{subset_refl} A <= A 673\tdx{subset_trans} [| A<=B; B<=C |] ==> A<=C 674 675\tdx{equalityI} [| A <= B; B <= A |] ==> A = B 676\tdx{equalityD1} A = B ==> A<=B 677\tdx{equalityD2} A = B ==> B<=A 678\tdx{equalityE} [| A = B; [| A<=B; B<=A |] ==> P |] ==> P 679 680\tdx{equalityCE} [| A = B; [| c:A; c:B |] ==> P; 681 [| ~ c:A; ~ c:B |] ==> P 682 |] ==> P 683\subcaption{The subset and equality relations} 684\end{ttbox} 685\caption{Derived rules for set theory} \label{hol-set1} 686\end{figure} 687 688 689\begin{figure} \underscoreon 690\begin{ttbox} 691\tdx{emptyE} a : {\ttlbrace}{\ttrbrace} ==> P 692 693\tdx{insertI1} a : insert a B 694\tdx{insertI2} a : B ==> a : insert b B 695\tdx{insertE} [| a : insert b A; a=b ==> P; a:A ==> P |] ==> P 696 697\tdx{ComplI} [| c:A ==> False |] ==> c : -A 698\tdx{ComplD} [| c : -A |] ==> ~ c:A 699 700\tdx{UnI1} c:A ==> c : A Un B 701\tdx{UnI2} c:B ==> c : A Un B 702\tdx{UnCI} (~c:B ==> c:A) ==> c : A Un B 703\tdx{UnE} [| c : A Un B; c:A ==> P; c:B ==> P |] ==> P 704 705\tdx{IntI} [| c:A; c:B |] ==> c : A Int B 706\tdx{IntD1} c : A Int B ==> c:A 707\tdx{IntD2} c : A Int B ==> c:B 708\tdx{IntE} [| c : A Int B; [| c:A; c:B |] ==> P |] ==> P 709 710\tdx{UN_I} [| a:A; b: B a |] ==> b: (UN x:A. B x) 711\tdx{UN_E} [| b: (UN x:A. B x); !!x.[| x:A; b:B x |] ==> R |] ==> R 712 713\tdx{INT_I} (!!x. x:A ==> b: B x) ==> b : (INT x:A. B x) 714\tdx{INT_D} [| b: (INT x:A. B x); a:A |] ==> b: B a 715\tdx{INT_E} [| b: (INT x:A. B x); b: B a ==> R; ~ a:A ==> R |] ==> R 716 717\tdx{UnionI} [| X:C; A:X |] ==> A : Union C 718\tdx{UnionE} [| A : Union C; !!X.[| A:X; X:C |] ==> R |] ==> R 719 720\tdx{InterI} [| !!X. X:C ==> A:X |] ==> A : Inter C 721\tdx{InterD} [| A : Inter C; X:C |] ==> A:X 722\tdx{InterE} [| A : Inter C; A:X ==> R; ~ X:C ==> R |] ==> R 723 724\tdx{PowI} A<=B ==> A: Pow B 725\tdx{PowD} A: Pow B ==> A<=B 726 727\tdx{imageI} [| x:A |] ==> f x : f``A 728\tdx{imageE} [| b : f``A; !!x.[| b=f x; x:A |] ==> P |] ==> P 729 730\tdx{rangeI} f x : range f 731\tdx{rangeE} [| b : range f; !!x.[| b=f x |] ==> P |] ==> P 732\end{ttbox} 733\caption{Further derived rules for set theory} \label{hol-set2} 734\end{figure} 735 736 737\subsection{Axioms and rules of set theory} 738Figure~\ref{hol-set-rules} presents the rules of theory \thydx{Set}. The 739axioms \tdx{mem_Collect_eq} and \tdx{Collect_mem_eq} assert 740that the functions \texttt{Collect} and \hbox{\tt op :} are isomorphisms. Of 741course, \hbox{\tt op :} also serves as the membership relation. 742 743All the other axioms are definitions. They include the empty set, bounded 744quantifiers, unions, intersections, complements and the subset relation. 745They also include straightforward constructions on functions: image~({\tt``}) 746and \texttt{range}. 747 748%The predicate \cdx{inj_on} is used for simulating type definitions. 749%The statement ${\tt inj_on}~f~A$ asserts that $f$ is injective on the 750%set~$A$, which specifies a subset of its domain type. In a type 751%definition, $f$ is the abstraction function and $A$ is the set of valid 752%representations; we should not expect $f$ to be injective outside of~$A$. 753 754%\begin{figure} \underscoreon 755%\begin{ttbox} 756%\tdx{Inv_f_f} inj f ==> Inv f (f x) = x 757%\tdx{f_Inv_f} y : range f ==> f(Inv f y) = y 758% 759%\tdx{Inv_injective} 760% [| Inv f x=Inv f y; x: range f; y: range f |] ==> x=y 761% 762% 763%\tdx{monoI} [| !!A B. A <= B ==> f A <= f B |] ==> mono f 764%\tdx{monoD} [| mono f; A <= B |] ==> f A <= f B 765% 766%\tdx{injI} [| !! x y. f x = f y ==> x=y |] ==> inj f 767%\tdx{inj_inverseI} (!!x. g(f x) = x) ==> inj f 768%\tdx{injD} [| inj f; f x = f y |] ==> x=y 769% 770%\tdx{inj_onI} (!!x y. [| f x=f y; x:A; y:A |] ==> x=y) ==> inj_on f A 771%\tdx{inj_onD} [| inj_on f A; f x=f y; x:A; y:A |] ==> x=y 772% 773%\tdx{inj_on_inverseI} 774% (!!x. x:A ==> g(f x) = x) ==> inj_on f A 775%\tdx{inj_on_contraD} 776% [| inj_on f A; x~=y; x:A; y:A |] ==> ~ f x=f y 777%\end{ttbox} 778%\caption{Derived rules involving functions} \label{hol-fun} 779%\end{figure} 780 781 782\begin{figure} \underscoreon 783\begin{ttbox} 784\tdx{Union_upper} B:A ==> B <= Union A 785\tdx{Union_least} [| !!X. X:A ==> X<=C |] ==> Union A <= C 786 787\tdx{Inter_lower} B:A ==> Inter A <= B 788\tdx{Inter_greatest} [| !!X. X:A ==> C<=X |] ==> C <= Inter A 789 790\tdx{Un_upper1} A <= A Un B 791\tdx{Un_upper2} B <= A Un B 792\tdx{Un_least} [| A<=C; B<=C |] ==> A Un B <= C 793 794\tdx{Int_lower1} A Int B <= A 795\tdx{Int_lower2} A Int B <= B 796\tdx{Int_greatest} [| C<=A; C<=B |] ==> C <= A Int B 797\end{ttbox} 798\caption{Derived rules involving subsets} \label{hol-subset} 799\end{figure} 800 801 802\begin{figure} \underscoreon \hfuzz=4pt%suppress "Overfull \hbox" message 803\begin{ttbox} 804\tdx{Int_absorb} A Int A = A 805\tdx{Int_commute} A Int B = B Int A 806\tdx{Int_assoc} (A Int B) Int C = A Int (B Int C) 807\tdx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C) 808 809\tdx{Un_absorb} A Un A = A 810\tdx{Un_commute} A Un B = B Un A 811\tdx{Un_assoc} (A Un B) Un C = A Un (B Un C) 812\tdx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C) 813 814\tdx{Compl_disjoint} A Int (-A) = {\ttlbrace}x. False{\ttrbrace} 815\tdx{Compl_partition} A Un (-A) = {\ttlbrace}x. True{\ttrbrace} 816\tdx{double_complement} -(-A) = A 817\tdx{Compl_Un} -(A Un B) = (-A) Int (-B) 818\tdx{Compl_Int} -(A Int B) = (-A) Un (-B) 819 820\tdx{Union_Un_distrib} Union(A Un B) = (Union A) Un (Union B) 821\tdx{Int_Union} A Int (Union B) = (UN C:B. A Int C) 822 823\tdx{Inter_Un_distrib} Inter(A Un B) = (Inter A) Int (Inter B) 824\tdx{Un_Inter} A Un (Inter B) = (INT C:B. A Un C) 825 826\end{ttbox} 827\caption{Set equalities} \label{hol-equalities} 828\end{figure} 829%\tdx{Un_Union_image} (UN x:C.(A x) Un (B x)) = Union(A``C) Un Union(B``C) 830%\tdx{Int_Inter_image} (INT x:C.(A x) Int (B x)) = Inter(A``C) Int Inter(B``C) 831 832Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules. Most are 833obvious and resemble rules of Isabelle's ZF set theory. Certain rules, such 834as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI}, are designed for classical 835reasoning; the rules \tdx{subsetD}, \tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are 836not strictly necessary but yield more natural proofs. Similarly, 837\tdx{equalityCE} supports classical reasoning about extensionality, after the 838fashion of \tdx{iffCE}. See the file \texttt{HOL/Set.ML} for proofs 839pertaining to set theory. 840 841Figure~\ref{hol-subset} presents lattice properties of the subset relation. 842Unions form least upper bounds; non-empty intersections form greatest lower 843bounds. Reasoning directly about subsets often yields clearer proofs than 844reasoning about the membership relation. See the file \texttt{HOL/subset.ML}. 845 846Figure~\ref{hol-equalities} presents many common set equalities. They 847include commutative, associative and distributive laws involving unions, 848intersections and complements. For a complete listing see the file {\tt 849HOL/equalities.ML}. 850 851\begin{warn} 852\texttt{Blast_tac} proves many set-theoretic theorems automatically. 853Hence you seldom need to refer to the theorems above. 854\end{warn} 855 856\begin{figure} 857\begin{center} 858\begin{tabular}{rrr} 859 \it name &\it meta-type & \it description \\ 860 \cdx{inj}~~\cdx{surj}& $(\alpha\To\beta )\To bool$ 861 & injective/surjective \\ 862 \cdx{inj_on} & $[\alpha\To\beta ,\alpha\,set]\To bool$ 863 & injective over subset\\ 864 \cdx{inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & inverse function 865\end{tabular} 866\end{center} 867 868\underscoreon 869\begin{ttbox} 870\tdx{inj_def} inj f == ! x y. f x=f y --> x=y 871\tdx{surj_def} surj f == ! y. ? x. y=f x 872\tdx{inj_on_def} inj_on f A == !x:A. !y:A. f x=f y --> x=y 873\tdx{inv_def} inv f == (\%y. @x. f(x)=y) 874\end{ttbox} 875\caption{Theory \thydx{Fun}} \label{fig:HOL:Fun} 876\end{figure} 877 878\subsection{Properties of functions}\nopagebreak 879Figure~\ref{fig:HOL:Fun} presents a theory of simple properties of functions. 880Note that ${\tt inv}~f$ uses Hilbert's $\varepsilon$ to yield an inverse 881of~$f$. See the file \texttt{HOL/Fun.ML} for a complete listing of the derived 882rules. Reasoning about function composition (the operator~\sdx{o}) and the 883predicate~\cdx{surj} is done simply by expanding the definitions. 884 885There is also a large collection of monotonicity theorems for constructions 886on sets in the file \texttt{HOL/mono.ML}. 887 888 889\section{Simplification and substitution} 890 891Simplification tactics tactics such as \texttt{Asm_simp_tac} and \texttt{Full_simp_tac} use the default simpset 892(\texttt{simpset()}), which works for most purposes. A quite minimal 893simplification set for higher-order logic is~\ttindexbold{HOL_ss}; 894even more frugal is \ttindexbold{HOL_basic_ss}. Equality~($=$), which 895also expresses logical equivalence, may be used for rewriting. See 896the file \texttt{HOL/simpdata.ML} for a complete listing of the basic 897simplification rules. 898 899See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% 900{Chaps.\ts\ref{substitution} and~\ref{simp-chap}} for details of substitution 901and simplification. 902 903\begin{warn}\index{simplification!of conjunctions}% 904 Reducing $a=b\conj P(a)$ to $a=b\conj P(b)$ is sometimes advantageous. The 905 left part of a conjunction helps in simplifying the right part. This effect 906 is not available by default: it can be slow. It can be obtained by 907 including \ttindex{conj_cong} in a simpset, \verb$addcongs [conj_cong]$. 908\end{warn} 909 910\begin{warn}\index{simplification!of \texttt{if}}\label{if-simp}% 911 By default only the condition of an \ttindex{if} is simplified but not the 912 \texttt{then} and \texttt{else} parts. Of course the latter are simplified 913 once the condition simplifies to \texttt{True} or \texttt{False}. To ensure 914 full simplification of all parts of a conditional you must remove 915 \ttindex{if_weak_cong} from the simpset, \verb$delcongs [if_weak_cong]$. 916\end{warn} 917 918If the simplifier cannot use a certain rewrite rule --- either because 919of nontermination or because its left-hand side is too flexible --- 920then you might try \texttt{stac}: 921\begin{ttdescription} 922\item[\ttindexbold{stac} $thm$ $i,$] where $thm$ is of the form $lhs = rhs$, 923 replaces in subgoal $i$ instances of $lhs$ by corresponding instances of 924 $rhs$. In case of multiple instances of $lhs$ in subgoal $i$, backtracking 925 may be necessary to select the desired ones. 926 927If $thm$ is a conditional equality, the instantiated condition becomes an 928additional (first) subgoal. 929\end{ttdescription} 930 931HOL provides the tactic \ttindex{hyp_subst_tac}, which substitutes for an 932equality throughout a subgoal and its hypotheses. This tactic uses HOL's 933general substitution rule. 934 935\subsection{Case splitting} 936\label{subsec:HOL:case:splitting} 937 938HOL also provides convenient means for case splitting during rewriting. Goals 939containing a subterm of the form \texttt{if}~$b$~{\tt then\dots else\dots} 940often require a case distinction on $b$. This is expressed by the theorem 941\tdx{split_if}: 942$$ 943\Var{P}(\mbox{\tt if}~\Var{b}~{\tt then}~\Var{x}~\mbox{\tt else}~\Var{y})~=~ 944((\Var{b} \to \Var{P}(\Var{x})) \land (\lnot \Var{b} \to \Var{P}(\Var{y}))) 945\eqno{(*)} 946$$ 947For example, a simple instance of $(*)$ is 948\[ 949x \in (\mbox{\tt if}~x \in A~{\tt then}~A~\mbox{\tt else}~\{x\})~=~ 950((x \in A \to x \in A) \land (x \notin A \to x \in \{x\})) 951\] 952Because $(*)$ is too general as a rewrite rule for the simplifier (the 953left-hand side is not a higher-order pattern in the sense of 954\iflabelundefined{chap:simplification}{the {\em Reference Manual\/}}% 955{Chap.\ts\ref{chap:simplification}}), there is a special infix function 956\ttindexbold{addsplits} of type \texttt{simpset * thm list -> simpset} 957(analogous to \texttt{addsimps}) that adds rules such as $(*)$ to a 958simpset, as in 959\begin{ttbox} 960by(simp_tac (simpset() addsplits [split_if]) 1); 961\end{ttbox} 962The effect is that after each round of simplification, one occurrence of 963\texttt{if} is split acording to \texttt{split_if}, until all occurrences of 964\texttt{if} have been eliminated. 965 966It turns out that using \texttt{split_if} is almost always the right thing to 967do. Hence \texttt{split_if} is already included in the default simpset. If 968you want to delete it from a simpset, use \ttindexbold{delsplits}, which is 969the inverse of \texttt{addsplits}: 970\begin{ttbox} 971by(simp_tac (simpset() delsplits [split_if]) 1); 972\end{ttbox} 973 974In general, \texttt{addsplits} accepts rules of the form 975\[ 976\Var{P}(c~\Var{x@1}~\dots~\Var{x@n})~=~ rhs 977\] 978where $c$ is a constant and $rhs$ is arbitrary. Note that $(*)$ is of the 979right form because internally the left-hand side is 980$\Var{P}(\mathtt{If}~\Var{b}~\Var{x}~~\Var{y})$. Important further examples 981are splitting rules for \texttt{case} expressions (see~{\S}\ref{subsec:list} 982and~{\S}\ref{subsec:datatype:basics}). 983 984Analogous to \texttt{Addsimps} and \texttt{Delsimps}, there are also 985imperative versions of \texttt{addsplits} and \texttt{delsplits} 986\begin{ttbox} 987\ttindexbold{Addsplits}: thm list -> unit 988\ttindexbold{Delsplits}: thm list -> unit 989\end{ttbox} 990for adding splitting rules to, and deleting them from the current simpset. 991 992 993\section{Types}\label{sec:HOL:Types} 994This section describes HOL's basic predefined types ($\alpha \times \beta$, 995$\alpha + \beta$, $nat$ and $\alpha \; list$) and ways for introducing new 996types in general. The most important type construction, the 997\texttt{datatype}, is treated separately in {\S}\ref{sec:HOL:datatype}. 998 999 1000\subsection{Product and sum types}\index{*"* type}\index{*"+ type} 1001\label{subsec:prod-sum} 1002 1003\begin{figure}[htbp] 1004\begin{constants} 1005 \it symbol & \it meta-type & & \it description \\ 1006 \cdx{Pair} & $[\alpha,\beta]\To \alpha\times\beta$ 1007 & & ordered pairs $(a,b)$ \\ 1008 \cdx{fst} & $\alpha\times\beta \To \alpha$ & & first projection\\ 1009 \cdx{snd} & $\alpha\times\beta \To \beta$ & & second projection\\ 1010 \cdx{split} & $[[\alpha,\beta]\To\gamma, \alpha\times\beta] \To \gamma$ 1011 & & generalized projection\\ 1012 \cdx{Sigma} & 1013 $[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ & 1014 & general sum of sets 1015\end{constants} 1016%\tdx{fst_def} fst p == @a. ? b. p = (a,b) 1017%\tdx{snd_def} snd p == @b. ? a. p = (a,b) 1018%\tdx{split_def} case_prod c p == c (fst p) (snd p) 1019\begin{ttbox}\makeatletter 1020\tdx{Sigma_def} Sigma A B == UN x:A. UN y:B x. {\ttlbrace}(x,y){\ttrbrace} 1021 1022\tdx{prod.inject} ((a,b) = (a',b')) = (a=a' & b=b') 1023\tdx{Pair_inject} [| (a, b) = (a',b'); [| a=a'; b=b' |] ==> R |] ==> R 1024\tdx{prod.exhaust} [| !!x y. p = (x,y) ==> Q |] ==> Q 1025 1026\tdx{fst_conv} fst (a,b) = a 1027\tdx{snd_conv} snd (a,b) = b 1028\tdx{surjective_pairing} p = (fst p,snd p) 1029 1030\tdx{split} case_prod c (a,b) = c a b 1031\tdx{prod.split} R(case_prod c p) = (! x y. p = (x,y) --> R(c x y)) 1032 1033\tdx{SigmaI} [| a:A; b:B a |] ==> (a,b) : Sigma A B 1034 1035\tdx{SigmaE} [| c:Sigma A B; !!x y.[| x:A; y:B x; c=(x,y) |] ==> P 1036 |] ==> P 1037\end{ttbox} 1038\caption{Type $\alpha\times\beta$}\label{hol-prod} 1039\end{figure} 1040 1041Theory \thydx{Prod} (Fig.\ts\ref{hol-prod}) defines the product type 1042$\alpha\times\beta$, with the ordered pair syntax $(a, b)$. General 1043tuples are simulated by pairs nested to the right: 1044\begin{center} 1045\begin{tabular}{c|c} 1046external & internal \\ 1047\hline 1048$\tau@1 \times \dots \times \tau@n$ & $\tau@1 \times (\dots (\tau@{n-1} \times \tau@n)\dots)$ \\ 1049\hline 1050$(t@1,\dots,t@n)$ & $(t@1,(\dots,(t@{n-1},t@n)\dots)$ \\ 1051\end{tabular} 1052\end{center} 1053In addition, it is possible to use tuples 1054as patterns in abstractions: 1055\begin{center} 1056{\tt\%($x$,$y$). $t$} \quad stands for\quad \texttt{split(\%$x$\thinspace$y$.\ $t$)} 1057\end{center} 1058Nested patterns are also supported. They are translated stepwise: 1059\begin{eqnarray*} 1060\hbox{\tt\%($x$,$y$,$z$).\ $t$} 1061 & \leadsto & \hbox{\tt\%($x$,($y$,$z$)).\ $t$} \\ 1062 & \leadsto & \hbox{\tt case_prod(\%$x$.\%($y$,$z$).\ $t$)}\\ 1063 & \leadsto & \hbox{\tt case_prod(\%$x$.\ case_prod(\%$y$ $z$.\ $t$))} 1064\end{eqnarray*} 1065The reverse translation is performed upon printing. 1066\begin{warn} 1067 The translation between patterns and \texttt{split} is performed automatically 1068 by the parser and printer. Thus the internal and external form of a term 1069 may differ, which can affects proofs. For example the term {\tt 1070 (\%(x,y).(y,x))(a,b)} requires the theorem \texttt{split} (which is in the 1071 default simpset) to rewrite to {\tt(b,a)}. 1072\end{warn} 1073In addition to explicit $\lambda$-abstractions, patterns can be used in any 1074variable binding construct which is internally described by a 1075$\lambda$-abstraction. Some important examples are 1076\begin{description} 1077\item[Let:] \texttt{let {\it pattern} = $t$ in $u$} 1078\item[Quantifiers:] \texttt{ALL~{\it pattern}:$A$.~$P$} 1079\item[Choice:] {\underscoreon \tt SOME~{\it pattern}.~$P$} 1080\item[Set operations:] \texttt{UN~{\it pattern}:$A$.~$B$} 1081\item[Sets:] \texttt{{\ttlbrace}{\it pattern}.~$P${\ttrbrace}} 1082\end{description} 1083 1084There is a simple tactic which supports reasoning about patterns: 1085\begin{ttdescription} 1086\item[\ttindexbold{split_all_tac} $i$] replaces in subgoal $i$ all 1087 {\tt!!}-quantified variables of product type by individual variables for 1088 each component. A simple example: 1089\begin{ttbox} 1090{\out 1. !!p. (\%(x,y,z). (x, y, z)) p = p} 1091by(split_all_tac 1); 1092{\out 1. !!x xa ya. (\%(x,y,z). (x, y, z)) (x, xa, ya) = (x, xa, ya)} 1093\end{ttbox} 1094\end{ttdescription} 1095 1096Theory \texttt{Prod} also introduces the degenerate product type \texttt{unit} 1097which contains only a single element named {\tt()} with the property 1098\begin{ttbox} 1099\tdx{unit_eq} u = () 1100\end{ttbox} 1101\bigskip 1102 1103Theory \thydx{Sum} (Fig.~\ref{hol-sum}) defines the sum type $\alpha+\beta$ 1104which associates to the right and has a lower priority than $*$: $\tau@1 + 1105\tau@2 + \tau@3*\tau@4$ means $\tau@1 + (\tau@2 + (\tau@3*\tau@4))$. 1106 1107The definition of products and sums in terms of existing types is not 1108shown. The constructions are fairly standard and can be found in the 1109respective theory files. Although the sum and product types are 1110constructed manually for foundational reasons, they are represented as 1111actual datatypes later. 1112 1113\begin{figure} 1114\begin{constants} 1115 \it symbol & \it meta-type & & \it description \\ 1116 \cdx{Inl} & $\alpha \To \alpha+\beta$ & & first injection\\ 1117 \cdx{Inr} & $\beta \To \alpha+\beta$ & & second injection\\ 1118 \cdx{case_sum} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$ 1119 & & conditional 1120\end{constants} 1121\begin{ttbox}\makeatletter 1122\tdx{Inl_not_Inr} Inl a ~= Inr b 1123 1124\tdx{inj_Inl} inj Inl 1125\tdx{inj_Inr} inj Inr 1126 1127\tdx{sumE} [| !!x. P(Inl x); !!y. P(Inr y) |] ==> P s 1128 1129\tdx{case_sum_Inl} case_sum f g (Inl x) = f x 1130\tdx{case_sum_Inr} case_sum f g (Inr x) = g x 1131 1132\tdx{surjective_sum} case_sum (\%x. f(Inl x)) (\%y. f(Inr y)) s = f s 1133\tdx{sum.split_case} R(case_sum f g s) = ((! x. s = Inl(x) --> R(f(x))) & 1134 (! y. s = Inr(y) --> R(g(y)))) 1135\end{ttbox} 1136\caption{Type $\alpha+\beta$}\label{hol-sum} 1137\end{figure} 1138 1139\begin{figure} 1140\index{*"< symbol} 1141\index{*"* symbol} 1142\index{*div symbol} 1143\index{*mod symbol} 1144\index{*dvd symbol} 1145\index{*"+ symbol} 1146\index{*"- symbol} 1147\begin{constants} 1148 \it symbol & \it meta-type & \it priority & \it description \\ 1149 \cdx{0} & $\alpha$ & & zero \\ 1150 \cdx{Suc} & $nat \To nat$ & & successor function\\ 1151 \tt * & $[\alpha,\alpha]\To \alpha$ & Left 70 & multiplication \\ 1152 \tt div & $[\alpha,\alpha]\To \alpha$ & Left 70 & division\\ 1153 \tt mod & $[\alpha,\alpha]\To \alpha$ & Left 70 & modulus\\ 1154 \tt dvd & $[\alpha,\alpha]\To bool$ & Left 70 & ``divides'' relation\\ 1155 \tt + & $[\alpha,\alpha]\To \alpha$ & Left 65 & addition\\ 1156 \tt - & $[\alpha,\alpha]\To \alpha$ & Left 65 & subtraction 1157\end{constants} 1158\subcaption{Constants and infixes} 1159 1160\begin{ttbox}\makeatother 1161\tdx{nat_induct} [| P 0; !!n. P n ==> P(Suc n) |] ==> P n 1162 1163\tdx{Suc_not_Zero} Suc m ~= 0 1164\tdx{inj_Suc} inj Suc 1165\tdx{n_not_Suc_n} n~=Suc n 1166\subcaption{Basic properties} 1167\end{ttbox} 1168\caption{The type of natural numbers, \tydx{nat}} \label{hol-nat1} 1169\end{figure} 1170 1171 1172\begin{figure} 1173\begin{ttbox}\makeatother 1174 0+n = n 1175 (Suc m)+n = Suc(m+n) 1176 1177 m-0 = m 1178 0-n = n 1179 Suc(m)-Suc(n) = m-n 1180 1181 0*n = 0 1182 Suc(m)*n = n + m*n 1183 1184\tdx{mod_less} m<n ==> m mod n = m 1185\tdx{mod_geq} [| 0<n; ~m<n |] ==> m mod n = (m-n) mod n 1186 1187\tdx{div_less} m<n ==> m div n = 0 1188\tdx{div_geq} [| 0<n; ~m<n |] ==> m div n = Suc((m-n) div n) 1189\end{ttbox} 1190\caption{Recursion equations for the arithmetic operators} \label{hol-nat2} 1191\end{figure} 1192 1193\subsection{The type of natural numbers, \textit{nat}} 1194\index{nat@{\textit{nat}} type|(} 1195 1196The theory \thydx{Nat} defines the natural numbers in a roundabout but 1197traditional way. The axiom of infinity postulates a type~\tydx{ind} of 1198individuals, which is non-empty and closed under an injective operation. The 1199natural numbers are inductively generated by choosing an arbitrary individual 1200for~0 and using the injective operation to take successors. This is a least 1201fixedpoint construction. 1202 1203Type~\tydx{nat} is an instance of class~\cldx{ord}, which makes the overloaded 1204functions of this class (especially \cdx{<} and \cdx{<=}, but also \cdx{min}, 1205\cdx{max} and \cdx{LEAST}) available on \tydx{nat}. Theory \thydx{Nat} 1206also shows that {\tt<=} is a linear order, so \tydx{nat} is 1207also an instance of class \cldx{linorder}. 1208 1209Theory \thydx{NatArith} develops arithmetic on the natural numbers. It defines 1210addition, multiplication and subtraction. Theory \thydx{Divides} defines 1211division, remainder and the ``divides'' relation. The numerous theorems 1212proved include commutative, associative, distributive, identity and 1213cancellation laws. See Figs.\ts\ref{hol-nat1} and~\ref{hol-nat2}. The 1214recursion equations for the operators \texttt{+}, \texttt{-} and \texttt{*} on 1215\texttt{nat} are part of the default simpset. 1216 1217Functions on \tydx{nat} can be defined by primitive or well-founded recursion; 1218see {\S}\ref{sec:HOL:recursive}. A simple example is addition. 1219Here, \texttt{op +} is the name of the infix operator~\texttt{+}, following 1220the standard convention. 1221\begin{ttbox} 1222\sdx{primrec} 1223 "0 + n = n" 1224 "Suc m + n = Suc (m + n)" 1225\end{ttbox} 1226There is also a \sdx{case}-construct 1227of the form 1228\begin{ttbox} 1229case \(e\) of 0 => \(a\) | Suc \(m\) => \(b\) 1230\end{ttbox} 1231Note that Isabelle insists on precisely this format; you may not even change 1232the order of the two cases. 1233Both \texttt{primrec} and \texttt{case} are realized by a recursion operator 1234\cdx{rec_nat}, which is available because \textit{nat} is represented as 1235a datatype. 1236 1237%The predecessor relation, \cdx{pred_nat}, is shown to be well-founded. 1238%Recursion along this relation resembles primitive recursion, but is 1239%stronger because we are in higher-order logic; using primitive recursion to 1240%define a higher-order function, we can easily Ackermann's function, which 1241%is not primitive recursive \cite[page~104]{thompson91}. 1242%The transitive closure of \cdx{pred_nat} is~$<$. Many functions on the 1243%natural numbers are most easily expressed using recursion along~$<$. 1244 1245Tactic {\tt\ttindex{induct_tac} "$n$" $i$} performs induction on variable~$n$ 1246in subgoal~$i$ using theorem \texttt{nat_induct}. There is also the derived 1247theorem \tdx{less_induct}: 1248\begin{ttbox} 1249[| !!n. [| ! m. m<n --> P m |] ==> P n |] ==> P n 1250\end{ttbox} 1251 1252 1253\subsection{Numerical types and numerical reasoning} 1254 1255The integers (type \tdx{int}) are also available in HOL, and the reals (type 1256\tdx{real}) are available in the logic image \texttt{HOL-Complex}. They support 1257the expected operations of addition (\texttt{+}), subtraction (\texttt{-}) and 1258multiplication (\texttt{*}), and much else. Type \tdx{int} provides the 1259\texttt{div} and \texttt{mod} operators, while type \tdx{real} provides real 1260division and other operations. Both types belong to class \cldx{linorder}, so 1261they inherit the relational operators and all the usual properties of linear 1262orderings. For full details, please survey the theories in subdirectories 1263\texttt{Integ}, \texttt{Real}, and \texttt{Complex}. 1264 1265All three numeric types admit numerals of the form \texttt{$sd\ldots d$}, 1266where $s$ is an optional minus sign and $d\ldots d$ is a string of digits. 1267Numerals are represented internally by a datatype for binary notation, which 1268allows numerical calculations to be performed by rewriting. For example, the 1269integer division of \texttt{54342339} by \texttt{3452} takes about five 1270seconds. By default, the simplifier cancels like terms on the opposite sites 1271of relational operators (reducing \texttt{z+x<x+y} to \texttt{z<y}, for 1272instance. The simplifier also collects like terms, replacing \texttt{x+y+x*3} 1273by \texttt{4*x+y}. 1274 1275Sometimes numerals are not wanted, because for example \texttt{n+3} does not 1276match a pattern of the form \texttt{Suc $k$}. You can re-arrange the form of 1277an arithmetic expression by proving (via \texttt{subgoal_tac}) a lemma such as 1278\texttt{n+3 = Suc (Suc (Suc n))}. As an alternative, you can disable the 1279fancier simplifications by using a basic simpset such as \texttt{HOL_ss} 1280rather than the default one, \texttt{simpset()}. 1281 1282Reasoning about arithmetic inequalities can be tedious. Fortunately, HOL 1283provides a decision procedure for \emph{linear arithmetic}: formulae involving 1284addition and subtraction. The simplifier invokes a weak version of this 1285decision procedure automatically. If this is not sufficent, you can invoke the 1286full procedure \ttindex{Lin_Arith.tac} explicitly. It copes with arbitrary 1287formulae involving {\tt=}, {\tt<}, {\tt<=}, {\tt+}, {\tt-}, {\tt Suc}, {\tt 1288 min}, {\tt max} and numerical constants. Other subterms are treated as 1289atomic, while subformulae not involving numerical types are ignored. Quantified 1290subformulae are ignored unless they are positive universal or negative 1291existential. The running time is exponential in the number of 1292occurrences of {\tt min}, {\tt max}, and {\tt-} because they require case 1293distinctions. 1294If {\tt k} is a numeral, then {\tt div k}, {\tt mod k} and 1295{\tt k dvd} are also supported. The former two are eliminated 1296by case distinctions, again blowing up the running time. 1297If the formula involves explicit quantifiers, \texttt{Lin_Arith.tac} may take 1298super-exponential time and space. 1299 1300If \texttt{Lin_Arith.tac} fails, try to find relevant arithmetic results in 1301the library. The theories \texttt{Nat} and \texttt{NatArith} contain 1302theorems about {\tt<}, {\tt<=}, \texttt{+}, \texttt{-} and \texttt{*}. 1303Theory \texttt{Divides} contains theorems about \texttt{div} and 1304\texttt{mod}. Use Proof General's \emph{find} button (or other search 1305facilities) to locate them. 1306 1307\index{nat@{\textit{nat}} type|)} 1308 1309 1310\begin{figure} 1311\index{#@{\tt[]} symbol} 1312\index{#@{\tt\#} symbol} 1313\index{"@@{\tt\at} symbol} 1314\index{*"! symbol} 1315\begin{constants} 1316 \it symbol & \it meta-type & \it priority & \it description \\ 1317 \tt[] & $\alpha\,list$ & & empty list\\ 1318 \tt \# & $[\alpha,\alpha\,list]\To \alpha\,list$ & Right 65 & 1319 list constructor \\ 1320 \cdx{null} & $\alpha\,list \To bool$ & & emptiness test\\ 1321 \cdx{hd} & $\alpha\,list \To \alpha$ & & head \\ 1322 \cdx{tl} & $\alpha\,list \To \alpha\,list$ & & tail \\ 1323 \cdx{last} & $\alpha\,list \To \alpha$ & & last element \\ 1324 \cdx{butlast} & $\alpha\,list \To \alpha\,list$ & & drop last element \\ 1325 \tt\at & $[\alpha\,list,\alpha\,list]\To \alpha\,list$ & Left 65 & append \\ 1326 \cdx{map} & $(\alpha\To\beta) \To (\alpha\,list \To \beta\,list)$ 1327 & & apply to all\\ 1328 \cdx{filter} & $(\alpha \To bool) \To (\alpha\,list \To \alpha\,list)$ 1329 & & filter functional\\ 1330 \cdx{set}& $\alpha\,list \To \alpha\,set$ & & elements\\ 1331 \sdx{mem} & $\alpha \To \alpha\,list \To bool$ & Left 55 & membership\\ 1332 \cdx{foldl} & $(\beta\To\alpha\To\beta) \To \beta \To \alpha\,list \To \beta$ & 1333 & iteration \\ 1334 \cdx{concat} & $(\alpha\,list)list\To \alpha\,list$ & & concatenation \\ 1335 \cdx{rev} & $\alpha\,list \To \alpha\,list$ & & reverse \\ 1336 \cdx{length} & $\alpha\,list \To nat$ & & length \\ 1337 \tt! & $\alpha\,list \To nat \To \alpha$ & Left 100 & indexing \\ 1338 \cdx{take}, \cdx{drop} & $nat \To \alpha\,list \To \alpha\,list$ && 1339 take/drop a prefix \\ 1340 \cdx{takeWhile},\\ 1341 \cdx{dropWhile} & 1342 $(\alpha \To bool) \To \alpha\,list \To \alpha\,list$ && 1343 take/drop a prefix 1344\end{constants} 1345\subcaption{Constants and infixes} 1346 1347\begin{center} \tt\frenchspacing 1348\begin{tabular}{rrr} 1349 \it external & \it internal & \it description \\{} 1350 [$x@1$, $\dots$, $x@n$] & $x@1$ \# $\cdots$ \# $x@n$ \# [] & 1351 \rm finite list \\{} 1352 [$x$:$l$. $P$] & filter ($\lambda x{.}P$) $l$ & 1353 \rm list comprehension 1354\end{tabular} 1355\end{center} 1356\subcaption{Translations} 1357\caption{The theory \thydx{List}} \label{hol-list} 1358\end{figure} 1359 1360 1361\begin{figure} 1362\begin{ttbox}\makeatother 1363null [] = True 1364null (x#xs) = False 1365 1366hd (x#xs) = x 1367 1368tl (x#xs) = xs 1369tl [] = [] 1370 1371[] @ ys = ys 1372(x#xs) @ ys = x # xs @ ys 1373 1374set [] = \ttlbrace\ttrbrace 1375set (x#xs) = insert x (set xs) 1376 1377x mem [] = False 1378x mem (y#ys) = (if y=x then True else x mem ys) 1379 1380concat([]) = [] 1381concat(x#xs) = x @ concat(xs) 1382 1383rev([]) = [] 1384rev(x#xs) = rev(xs) @ [x] 1385 1386length([]) = 0 1387length(x#xs) = Suc(length(xs)) 1388 1389xs!0 = hd xs 1390xs!(Suc n) = (tl xs)!n 1391\end{ttbox} 1392\caption{Simple list processing functions} 1393\label{fig:HOL:list-simps} 1394\end{figure} 1395 1396\begin{figure} 1397\begin{ttbox}\makeatother 1398map f [] = [] 1399map f (x#xs) = f x # map f xs 1400 1401filter P [] = [] 1402filter P (x#xs) = (if P x then x#filter P xs else filter P xs) 1403 1404foldl f a [] = a 1405foldl f a (x#xs) = foldl f (f a x) xs 1406 1407take n [] = [] 1408take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs) 1409 1410drop n [] = [] 1411drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs) 1412 1413takeWhile P [] = [] 1414takeWhile P (x#xs) = (if P x then x#takeWhile P xs else []) 1415 1416dropWhile P [] = [] 1417dropWhile P (x#xs) = (if P x then dropWhile P xs else xs) 1418\end{ttbox} 1419\caption{Further list processing functions} 1420\label{fig:HOL:list-simps2} 1421\end{figure} 1422 1423 1424\subsection{The type constructor for lists, \textit{list}} 1425\label{subsec:list} 1426\index{list@{\textit{list}} type|(} 1427 1428Figure~\ref{hol-list} presents the theory \thydx{List}: the basic list 1429operations with their types and syntax. Type $\alpha \; list$ is 1430defined as a \texttt{datatype} with the constructors {\tt[]} and {\tt\#}. 1431As a result the generic structural induction and case analysis tactics 1432\texttt{induct\_tac} and \texttt{cases\_tac} also become available for 1433lists. A \sdx{case} construct of the form 1434\begin{center}\tt 1435case $e$ of [] => $a$ | \(x\)\#\(xs\) => b 1436\end{center} 1437is defined by translation. For details see~{\S}\ref{sec:HOL:datatype}. There 1438is also a case splitting rule \tdx{list.split} 1439\[ 1440\begin{array}{l} 1441P(\mathtt{case}~e~\mathtt{of}~\texttt{[] =>}~a ~\texttt{|}~ 1442 x\texttt{\#}xs~\texttt{=>}~f~x~xs) ~= \\ 1443((e = \texttt{[]} \to P(a)) \land 1444 (\forall x~ xs. e = x\texttt{\#}xs \to P(f~x~xs))) 1445\end{array} 1446\] 1447which can be fed to \ttindex{addsplits} just like 1448\texttt{split_if} (see~{\S}\ref{subsec:HOL:case:splitting}). 1449 1450\texttt{List} provides a basic library of list processing functions defined by 1451primitive recursion. The recursion equations 1452are shown in Figs.\ts\ref{fig:HOL:list-simps} and~\ref{fig:HOL:list-simps2}. 1453 1454\index{list@{\textit{list}} type|)} 1455 1456 1457\section{Datatype definitions} 1458\label{sec:HOL:datatype} 1459\index{*datatype|(} 1460 1461Inductive datatypes, similar to those of \ML, frequently appear in 1462applications of Isabelle/HOL. In principle, such types could be defined by 1463hand via \texttt{typedef}, but this would be far too 1464tedious. The \ttindex{datatype} definition package of Isabelle/HOL (cf.\ 1465\cite{Berghofer-Wenzel:1999:TPHOL}) automates such chores. It generates an 1466appropriate \texttt{typedef} based on a least fixed-point construction, and 1467proves freeness theorems and induction rules, as well as theorems for 1468recursion and case combinators. The user just has to give a simple 1469specification of new inductive types using a notation similar to {\ML} or 1470Haskell. 1471 1472The current datatype package can handle both mutual and indirect recursion. 1473It also offers to represent existing types as datatypes giving the advantage 1474of a more uniform view on standard theories. 1475 1476 1477\subsection{Basics} 1478\label{subsec:datatype:basics} 1479 1480A general \texttt{datatype} definition is of the following form: 1481\[ 1482\begin{array}{llcl} 1483\mathtt{datatype} & (\vec{\alpha})t@1 & = & 1484 C^1@1~\tau^1@{1,1}~\ldots~\tau^1@{1,m^1@1} ~\mid~ \ldots ~\mid~ 1485 C^1@{k@1}~\tau^1@{k@1,1}~\ldots~\tau^1@{k@1,m^1@{k@1}} \\ 1486 & & \vdots \\ 1487\mathtt{and} & (\vec{\alpha})t@n & = & 1488 C^n@1~\tau^n@{1,1}~\ldots~\tau^n@{1,m^n@1} ~\mid~ \ldots ~\mid~ 1489 C^n@{k@n}~\tau^n@{k@n,1}~\ldots~\tau^n@{k@n,m^n@{k@n}} 1490\end{array} 1491\] 1492where $\vec{\alpha} = (\alpha@1,\ldots,\alpha@h)$ is a list of type variables, 1493$C^j@i$ are distinct constructor names and $\tau^j@{i,i'}$ are {\em 1494 admissible} types containing at most the type variables $\alpha@1, \ldots, 1495\alpha@h$. A type $\tau$ occurring in a \texttt{datatype} definition is {\em 1496 admissible} if and only if 1497\begin{itemize} 1498\item $\tau$ is non-recursive, i.e.\ $\tau$ does not contain any of the 1499newly defined type constructors $t@1,\ldots,t@n$, or 1500\item $\tau = (\vec{\alpha})t@{j'}$ where $1 \leq j' \leq n$, or 1501\item $\tau = (\tau'@1,\ldots,\tau'@{h'})t'$, where $t'$ is 1502the type constructor of an already existing datatype and $\tau'@1,\ldots,\tau'@{h'}$ 1503are admissible types. 1504\item $\tau = \sigma \to \tau'$, where $\tau'$ is an admissible 1505type and $\sigma$ is non-recursive (i.e. the occurrences of the newly defined 1506types are {\em strictly positive}) 1507\end{itemize} 1508If some $(\vec{\alpha})t@{j'}$ occurs in a type $\tau^j@{i,i'}$ 1509of the form 1510\[ 1511(\ldots,\ldots ~ (\vec{\alpha})t@{j'} ~ \ldots,\ldots)t' 1512\] 1513this is called a {\em nested} (or \emph{indirect}) occurrence. A very simple 1514example of a datatype is the type \texttt{list}, which can be defined by 1515\begin{ttbox} 1516datatype 'a list = Nil 1517 | Cons 'a ('a list) 1518\end{ttbox} 1519Arithmetic expressions \texttt{aexp} and boolean expressions \texttt{bexp} can be modelled 1520by the mutually recursive datatype definition 1521\begin{ttbox} 1522datatype 'a aexp = If_then_else ('a bexp) ('a aexp) ('a aexp) 1523 | Sum ('a aexp) ('a aexp) 1524 | Diff ('a aexp) ('a aexp) 1525 | Var 'a 1526 | Num nat 1527and 'a bexp = Less ('a aexp) ('a aexp) 1528 | And ('a bexp) ('a bexp) 1529 | Or ('a bexp) ('a bexp) 1530\end{ttbox} 1531The datatype \texttt{term}, which is defined by 1532\begin{ttbox} 1533datatype ('a, 'b) term = Var 'a 1534 | App 'b ((('a, 'b) term) list) 1535\end{ttbox} 1536is an example for a datatype with nested recursion. Using nested recursion 1537involving function spaces, we may also define infinitely branching datatypes, e.g. 1538\begin{ttbox} 1539datatype 'a tree = Atom 'a | Branch "nat => 'a tree" 1540\end{ttbox} 1541 1542\medskip 1543 1544Types in HOL must be non-empty. Each of the new datatypes 1545$(\vec{\alpha})t@j$ with $1 \leq j \leq n$ is non-empty if and only if it has a 1546constructor $C^j@i$ with the following property: for all argument types 1547$\tau^j@{i,i'}$ of the form $(\vec{\alpha})t@{j'}$ the datatype 1548$(\vec{\alpha})t@{j'}$ is non-empty. 1549 1550If there are no nested occurrences of the newly defined datatypes, obviously 1551at least one of the newly defined datatypes $(\vec{\alpha})t@j$ 1552must have a constructor $C^j@i$ without recursive arguments, a \emph{base 1553 case}, to ensure that the new types are non-empty. If there are nested 1554occurrences, a datatype can even be non-empty without having a base case 1555itself. Since \texttt{list} is a non-empty datatype, \texttt{datatype t = C (t 1556 list)} is non-empty as well. 1557 1558 1559\subsubsection{Freeness of the constructors} 1560 1561The datatype constructors are automatically defined as functions of their 1562respective type: 1563\[ C^j@i :: [\tau^j@{i,1},\dots,\tau^j@{i,m^j@i}] \To (\alpha@1,\dots,\alpha@h)t@j \] 1564These functions have certain {\em freeness} properties. They construct 1565distinct values: 1566\[ 1567C^j@i~x@1~\dots~x@{m^j@i} \neq C^j@{i'}~y@1~\dots~y@{m^j@{i'}} \qquad 1568\mbox{for all}~ i \neq i'. 1569\] 1570The constructor functions are injective: 1571\[ 1572(C^j@i~x@1~\dots~x@{m^j@i} = C^j@i~y@1~\dots~y@{m^j@i}) = 1573(x@1 = y@1 \land \dots \land x@{m^j@i} = y@{m^j@i}) 1574\] 1575Since the number of distinctness inequalities is quadratic in the number of 1576constructors, the datatype package avoids proving them separately if there are 1577too many constructors. Instead, specific inequalities are proved by a suitable 1578simplification procedure on demand.\footnote{This procedure, which is already part 1579of the default simpset, may be referred to by the ML identifier 1580\texttt{DatatypePackage.distinct_simproc}.} 1581 1582\subsubsection{Structural induction} 1583 1584The datatype package also provides structural induction rules. For 1585datatypes without nested recursion, this is of the following form: 1586\[ 1587\infer{P@1~x@1 \land \dots \land P@n~x@n} 1588 {\begin{array}{lcl} 1589 \Forall x@1 \dots x@{m^1@1}. 1590 \List{P@{s^1@{1,1}}~x@{r^1@{1,1}}; \dots; 1591 P@{s^1@{1,l^1@1}}~x@{r^1@{1,l^1@1}}} & \Imp & 1592 P@1~\left(C^1@1~x@1~\dots~x@{m^1@1}\right) \\ 1593 & \vdots \\ 1594 \Forall x@1 \dots x@{m^1@{k@1}}. 1595 \List{P@{s^1@{k@1,1}}~x@{r^1@{k@1,1}}; \dots; 1596 P@{s^1@{k@1,l^1@{k@1}}}~x@{r^1@{k@1,l^1@{k@1}}}} & \Imp & 1597 P@1~\left(C^1@{k@1}~x@1~\ldots~x@{m^1@{k@1}}\right) \\ 1598 & \vdots \\ 1599 \Forall x@1 \dots x@{m^n@1}. 1600 \List{P@{s^n@{1,1}}~x@{r^n@{1,1}}; \dots; 1601 P@{s^n@{1,l^n@1}}~x@{r^n@{1,l^n@1}}} & \Imp & 1602 P@n~\left(C^n@1~x@1~\ldots~x@{m^n@1}\right) \\ 1603 & \vdots \\ 1604 \Forall x@1 \dots x@{m^n@{k@n}}. 1605 \List{P@{s^n@{k@n,1}}~x@{r^n@{k@n,1}}; \dots 1606 P@{s^n@{k@n,l^n@{k@n}}}~x@{r^n@{k@n,l^n@{k@n}}}} & \Imp & 1607 P@n~\left(C^n@{k@n}~x@1~\ldots~x@{m^n@{k@n}}\right) 1608 \end{array}} 1609\] 1610where 1611\[ 1612\begin{array}{rcl} 1613Rec^j@i & := & 1614 \left\{\left(r^j@{i,1},s^j@{i,1}\right),\ldots, 1615 \left(r^j@{i,l^j@i},s^j@{i,l^j@i}\right)\right\} = \\[2ex] 1616&& \left\{(i',i'')~\left|~ 1617 1\leq i' \leq m^j@i \land 1 \leq i'' \leq n \land 1618 \tau^j@{i,i'} = (\alpha@1,\ldots,\alpha@h)t@{i''}\right.\right\} 1619\end{array} 1620\] 1621i.e.\ the properties $P@j$ can be assumed for all recursive arguments. 1622 1623For datatypes with nested recursion, such as the \texttt{term} example from 1624above, things are a bit more complicated. Conceptually, Isabelle/HOL unfolds 1625a definition like 1626\begin{ttbox} 1627datatype ('a,'b) term = Var 'a 1628 | App 'b ((('a, 'b) term) list) 1629\end{ttbox} 1630to an equivalent definition without nesting: 1631\begin{ttbox} 1632datatype ('a,'b) term = Var 1633 | App 'b (('a, 'b) term_list) 1634and ('a,'b) term_list = Nil' 1635 | Cons' (('a,'b) term) (('a,'b) term_list) 1636\end{ttbox} 1637Note however, that the type \texttt{('a,'b) term_list} and the constructors {\tt 1638 Nil'} and \texttt{Cons'} are not really introduced. One can directly work with 1639the original (isomorphic) type \texttt{(('a, 'b) term) list} and its existing 1640constructors \texttt{Nil} and \texttt{Cons}. Thus, the structural induction rule for 1641\texttt{term} gets the form 1642\[ 1643\infer{P@1~x@1 \land P@2~x@2} 1644 {\begin{array}{l} 1645 \Forall x.~P@1~(\mathtt{Var}~x) \\ 1646 \Forall x@1~x@2.~P@2~x@2 \Imp P@1~(\mathtt{App}~x@1~x@2) \\ 1647 P@2~\mathtt{Nil} \\ 1648 \Forall x@1~x@2. \List{P@1~x@1; P@2~x@2} \Imp P@2~(\mathtt{Cons}~x@1~x@2) 1649 \end{array}} 1650\] 1651Note that there are two predicates $P@1$ and $P@2$, one for the type \texttt{('a,'b) term} 1652and one for the type \texttt{(('a, 'b) term) list}. 1653 1654For a datatype with function types such as \texttt{'a tree}, the induction rule 1655is of the form 1656\[ 1657\infer{P~t} 1658 {\Forall a.~P~(\mathtt{Atom}~a) & 1659 \Forall ts.~(\forall x.~P~(ts~x)) \Imp P~(\mathtt{Branch}~ts)} 1660\] 1661 1662\medskip In principle, inductive types are already fully determined by 1663freeness and structural induction. For convenience in applications, 1664the following derived constructions are automatically provided for any 1665datatype. 1666 1667\subsubsection{The \sdx{case} construct} 1668 1669The type comes with an \ML-like \texttt{case}-construct: 1670\[ 1671\begin{array}{rrcl} 1672\mbox{\tt case}~e~\mbox{\tt of} & C^j@1~x@{1,1}~\dots~x@{1,m^j@1} & \To & e@1 \\ 1673 \vdots \\ 1674 \mid & C^j@{k@j}~x@{k@j,1}~\dots~x@{k@j,m^j@{k@j}} & \To & e@{k@j} 1675\end{array} 1676\] 1677where the $x@{i,j}$ are either identifiers or nested tuple patterns as in 1678{\S}\ref{subsec:prod-sum}. 1679\begin{warn} 1680 All constructors must be present, their order is fixed, and nested patterns 1681 are not supported (with the exception of tuples). Violating this 1682 restriction results in strange error messages. 1683\end{warn} 1684 1685To perform case distinction on a goal containing a \texttt{case}-construct, 1686the theorem $t@j.$\texttt{split} is provided: 1687\[ 1688\begin{array}{@{}rcl@{}} 1689P(t@j_\mathtt{case}~f@1~\dots~f@{k@j}~e) &\!\!\!=& 1690\!\!\! ((\forall x@1 \dots x@{m^j@1}. e = C^j@1~x@1\dots x@{m^j@1} \to 1691 P(f@1~x@1\dots x@{m^j@1})) \\ 1692&&\!\!\! ~\land~ \dots ~\land \\ 1693&&~\!\!\! (\forall x@1 \dots x@{m^j@{k@j}}. e = C^j@{k@j}~x@1\dots x@{m^j@{k@j}} \to 1694 P(f@{k@j}~x@1\dots x@{m^j@{k@j}}))) 1695\end{array} 1696\] 1697where $t@j$\texttt{_case} is the internal name of the \texttt{case}-construct. 1698This theorem can be added to a simpset via \ttindex{addsplits} 1699(see~{\S}\ref{subsec:HOL:case:splitting}). 1700 1701Case splitting on assumption works as well, by using the rule 1702$t@j.$\texttt{split_asm} in the same manner. Both rules are available under 1703$t@j.$\texttt{splits} (this name is \emph{not} bound in ML, though). 1704 1705\begin{warn}\index{simplification!of \texttt{case}}% 1706 By default only the selector expression ($e$ above) in a 1707 \texttt{case}-construct is simplified, in analogy with \texttt{if} (see 1708 page~\pageref{if-simp}). Only if that reduces to a constructor is one of 1709 the arms of the \texttt{case}-construct exposed and simplified. To ensure 1710 full simplification of all parts of a \texttt{case}-construct for datatype 1711 $t$, remove $t$\texttt{.}\ttindexbold{case_weak_cong} from the simpset, for 1712 example by \texttt{delcongs [thm "$t$.case_cong_weak"]}. 1713\end{warn} 1714 1715\subsubsection{The function \cdx{size}}\label{sec:HOL:size} 1716 1717Theory \texttt{NatArith} declares a generic function \texttt{size} of type 1718$\alpha\To nat$. Each datatype defines a particular instance of \texttt{size} 1719by overloading according to the following scheme: 1720%%% FIXME: This formula is too big and is completely unreadable 1721\[ 1722size(C^j@i~x@1~\dots~x@{m^j@i}) = \! 1723\left\{ 1724\begin{array}{ll} 17250 & \!\mbox{if $Rec^j@i = \emptyset$} \\ 17261+\sum\limits@{h=1}^{l^j@i}size~x@{r^j@{i,h}} & 1727 \!\mbox{if $Rec^j@i = \left\{\left(r^j@{i,1},s^j@{i,1}\right),\ldots, 1728 \left(r^j@{i,l^j@i},s^j@{i,l^j@i}\right)\right\}$} 1729\end{array} 1730\right. 1731\] 1732where $Rec^j@i$ is defined above. Viewing datatypes as generalised trees, the 1733size of a leaf is 0 and the size of a node is the sum of the sizes of its 1734subtrees ${}+1$. 1735 1736\subsection{Defining datatypes} 1737 1738The theory syntax for datatype definitions is given in the 1739Isabelle/Isar reference manual. In order to be well-formed, a 1740datatype definition has to obey the rules stated in the previous 1741section. As a result the theory is extended with the new types, the 1742constructors, and the theorems listed in the previous section. 1743 1744Most of the theorems about datatypes become part of the default simpset and 1745you never need to see them again because the simplifier applies them 1746automatically. Only induction or case distinction are usually invoked by hand. 1747\begin{ttdescription} 1748\item[\ttindexbold{induct_tac} {\tt"}$x${\tt"} $i$] 1749 applies structural induction on variable $x$ to subgoal $i$, provided the 1750 type of $x$ is a datatype. 1751\item[\texttt{induct_tac} 1752 {\tt"}$x@1$ $\ldots$ $x@n${\tt"} $i$] applies simultaneous 1753 structural induction on the variables $x@1,\ldots,x@n$ to subgoal $i$. This 1754 is the canonical way to prove properties of mutually recursive datatypes 1755 such as \texttt{aexp} and \texttt{bexp}, or datatypes with nested recursion such as 1756 \texttt{term}. 1757\end{ttdescription} 1758In some cases, induction is overkill and a case distinction over all 1759constructors of the datatype suffices. 1760\begin{ttdescription} 1761\item[\ttindexbold{case_tac} {\tt"}$u${\tt"} $i$] 1762 performs a case analysis for the term $u$ whose type must be a datatype. 1763 If the datatype has $k@j$ constructors $C^j@1$, \dots $C^j@{k@j}$, subgoal 1764 $i$ is replaced by $k@j$ new subgoals which contain the additional 1765 assumption $u = C^j@{i'}~x@1~\dots~x@{m^j@{i'}}$ for $i'=1$, $\dots$,~$k@j$. 1766\end{ttdescription} 1767 1768Note that induction is only allowed on free variables that should not occur 1769among the premises of the subgoal. Case distinction applies to arbitrary terms. 1770 1771\bigskip 1772 1773 1774For the technically minded, we exhibit some more details. Processing the 1775theory file produces an \ML\ structure which, in addition to the usual 1776components, contains a structure named $t$ for each datatype $t$ defined in 1777the file. Each structure $t$ contains the following elements: 1778\begin{ttbox} 1779val distinct : thm list 1780val inject : thm list 1781val induct : thm 1782val exhaust : thm 1783val cases : thm list 1784val split : thm 1785val split_asm : thm 1786val recs : thm list 1787val size : thm list 1788val simps : thm list 1789\end{ttbox} 1790\texttt{distinct}, \texttt{inject}, \texttt{induct}, \texttt{size} 1791and \texttt{split} contain the theorems 1792described above. For user convenience, \texttt{distinct} contains 1793inequalities in both directions. The reduction rules of the {\tt 1794 case}-construct are in \texttt{cases}. All theorems from {\tt 1795 distinct}, \texttt{inject} and \texttt{cases} are combined in \texttt{simps}. 1796In case of mutually recursive datatypes, \texttt{recs}, \texttt{size}, \texttt{induct} 1797and \texttt{simps} are contained in a separate structure named $t@1_\ldots_t@n$. 1798 1799 1800\section{Old-style recursive function definitions}\label{sec:HOL:recursive} 1801\index{recursion!general|(} 1802\index{*recdef|(} 1803 1804Old-style recursive definitions via \texttt{recdef} requires that you 1805supply a well-founded relation that governs the recursion. Recursive 1806calls are only allowed if they make the argument decrease under the 1807relation. Complicated recursion forms, such as nested recursion, can 1808be dealt with. Termination can even be proved at a later time, though 1809having unsolved termination conditions around can make work 1810difficult.% 1811\footnote{This facility is based on Konrad Slind's TFL 1812 package~\cite{slind-tfl}. Thanks are due to Konrad for implementing 1813 TFL and assisting with its installation.} 1814 1815Using \texttt{recdef}, you can declare functions involving nested recursion 1816and pattern-matching. Recursion need not involve datatypes and there are few 1817syntactic restrictions. Termination is proved by showing that each recursive 1818call makes the argument smaller in a suitable sense, which you specify by 1819supplying a well-founded relation. 1820 1821Here is a simple example, the Fibonacci function. The first line declares 1822\texttt{fib} to be a constant. The well-founded relation is simply~$<$ (on 1823the natural numbers). Pattern-matching is used here: \texttt{1} is a 1824macro for \texttt{Suc~0}. 1825\begin{ttbox} 1826consts fib :: "nat => nat" 1827recdef fib "less_than" 1828 "fib 0 = 0" 1829 "fib 1 = 1" 1830 "fib (Suc(Suc x)) = (fib x + fib (Suc x))" 1831\end{ttbox} 1832 1833With \texttt{recdef}, function definitions may be incomplete, and patterns may 1834overlap, as in functional programming. The \texttt{recdef} package 1835disambiguates overlapping patterns by taking the order of rules into account. 1836For missing patterns, the function is defined to return a default value. 1837 1838%For example, here is a declaration of the list function \cdx{hd}: 1839%\begin{ttbox} 1840%consts hd :: 'a list => 'a 1841%recdef hd "\{\}" 1842% "hd (x#l) = x" 1843%\end{ttbox} 1844%Because this function is not recursive, we may supply the empty well-founded 1845%relation, $\{\}$. 1846 1847The well-founded relation defines a notion of ``smaller'' for the function's 1848argument type. The relation $\prec$ is \textbf{well-founded} provided it 1849admits no infinitely decreasing chains 1850\[ \cdots\prec x@n\prec\cdots\prec x@1. \] 1851If the function's argument has type~$\tau$, then $\prec$ has to be a relation 1852over~$\tau$: it must have type $(\tau\times\tau)set$. 1853 1854Proving well-foundedness can be tricky, so Isabelle/HOL provides a collection 1855of operators for building well-founded relations. The package recognises 1856these operators and automatically proves that the constructed relation is 1857well-founded. Here are those operators, in order of importance: 1858\begin{itemize} 1859\item \texttt{less_than} is ``less than'' on the natural numbers. 1860 (It has type $(nat\times nat)set$, while $<$ has type $[nat,nat]\To bool$. 1861 1862\item $\mathop{\mathtt{measure}} f$, where $f$ has type $\tau\To nat$, is the 1863 relation~$\prec$ on type~$\tau$ such that $x\prec y$ if and only if 1864 $f(x)<f(y)$. 1865 Typically, $f$ takes the recursive function's arguments (as a tuple) and 1866 returns a result expressed in terms of the function \texttt{size}. It is 1867 called a \textbf{measure function}. Recall that \texttt{size} is overloaded 1868 and is defined on all datatypes (see {\S}\ref{sec:HOL:size}). 1869 1870\item $\mathop{\mathtt{inv_image}} R\;f$ is a generalisation of 1871 \texttt{measure}. It specifies a relation such that $x\prec y$ if and only 1872 if $f(x)$ 1873 is less than $f(y)$ according to~$R$, which must itself be a well-founded 1874 relation. 1875 1876\item $R@1\texttt{<*lex*>}R@2$ is the lexicographic product of two relations. 1877 It 1878 is a relation on pairs and satisfies $(x@1,x@2)\prec(y@1,y@2)$ if and only 1879 if $x@1$ 1880 is less than $y@1$ according to~$R@1$ or $x@1=y@1$ and $x@2$ 1881 is less than $y@2$ according to~$R@2$. 1882 1883\item \texttt{finite_psubset} is the proper subset relation on finite sets. 1884\end{itemize} 1885 1886We can use \texttt{measure} to declare Euclid's algorithm for the greatest 1887common divisor. The measure function, $\lambda(m,n). n$, specifies that the 1888recursion terminates because argument~$n$ decreases. 1889\begin{ttbox} 1890recdef gcd "measure ((\%(m,n). n) ::nat*nat=>nat)" 1891 "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))" 1892\end{ttbox} 1893 1894The general form of a well-founded recursive definition is 1895\begin{ttbox} 1896recdef {\it function} {\it rel} 1897 congs {\it congruence rules} {\bf(optional)} 1898 simpset {\it simplification set} {\bf(optional)} 1899 {\it reduction rules} 1900\end{ttbox} 1901where 1902\begin{itemize} 1903\item \textit{function} is the name of the function, either as an \textit{id} 1904 or a \textit{string}. 1905 1906\item \textit{rel} is a HOL expression for the well-founded termination 1907 relation. 1908 1909\item \textit{congruence rules} are required only in highly exceptional 1910 circumstances. 1911 1912\item The \textit{simplification set} is used to prove that the supplied 1913 relation is well-founded. It is also used to prove the \textbf{termination 1914 conditions}: assertions that arguments of recursive calls decrease under 1915 \textit{rel}. By default, simplification uses \texttt{simpset()}, which 1916 is sufficient to prove well-foundedness for the built-in relations listed 1917 above. 1918 1919\item \textit{reduction rules} specify one or more recursion equations. Each 1920 left-hand side must have the form $f\,t$, where $f$ is the function and $t$ 1921 is a tuple of distinct variables. If more than one equation is present then 1922 $f$ is defined by pattern-matching on components of its argument whose type 1923 is a \texttt{datatype}. 1924 1925 The \ML\ identifier $f$\texttt{.simps} contains the reduction rules as 1926 a list of theorems. 1927\end{itemize} 1928 1929With the definition of \texttt{gcd} shown above, Isabelle/HOL is unable to 1930prove one termination condition. It remains as a precondition of the 1931recursion theorems: 1932\begin{ttbox} 1933gcd.simps; 1934{\out ["! m n. n ~= 0 --> m mod n < n} 1935{\out ==> gcd (?m,?n) = (if ?n=0 then ?m else gcd (?n, ?m mod ?n))"] } 1936{\out : thm list} 1937\end{ttbox} 1938The theory \texttt{HOL/ex/Primes} illustrates how to prove termination 1939conditions afterwards. The function \texttt{Tfl.tgoalw} is like the standard 1940function \texttt{goalw}, which sets up a goal to prove, but its argument 1941should be the identifier $f$\texttt{.simps} and its effect is to set up a 1942proof of the termination conditions: 1943\begin{ttbox} 1944Tfl.tgoalw thy [] gcd.simps; 1945{\out Level 0} 1946{\out ! m n. n ~= 0 --> m mod n < n} 1947{\out 1. ! m n. n ~= 0 --> m mod n < n} 1948\end{ttbox} 1949This subgoal has a one-step proof using \texttt{simp_tac}. Once the theorem 1950is proved, it can be used to eliminate the termination conditions from 1951elements of \texttt{gcd.simps}. Theory \texttt{HOL/Subst/Unify} is a much 1952more complicated example of this process, where the termination conditions can 1953only be proved by complicated reasoning involving the recursive function 1954itself. 1955 1956Isabelle/HOL can prove the \texttt{gcd} function's termination condition 1957automatically if supplied with the right simpset. 1958\begin{ttbox} 1959recdef gcd "measure ((\%(m,n). n) ::nat*nat=>nat)" 1960 simpset "simpset() addsimps [mod_less_divisor, zero_less_eq]" 1961 "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))" 1962\end{ttbox} 1963 1964If all termination conditions were proved automatically, $f$\texttt{.simps} 1965is added to the simpset automatically, just as in \texttt{primrec}. 1966The simplification rules corresponding to clause $i$ (where counting starts 1967at 0) are called $f$\texttt{.}$i$ and can be accessed as \texttt{thms 1968 "$f$.$i$"}, 1969which returns a list of theorems. Thus you can, for example, remove specific 1970clauses from the simpset. Note that a single clause may give rise to a set of 1971simplification rules in order to capture the fact that if clauses overlap, 1972their order disambiguates them. 1973 1974A \texttt{recdef} definition also returns an induction rule specialised for 1975the recursive function. For the \texttt{gcd} function above, the induction 1976rule is 1977\begin{ttbox} 1978gcd.induct; 1979{\out "(!!m n. n ~= 0 --> ?P n (m mod n) ==> ?P m n) ==> ?P ?u ?v" : thm} 1980\end{ttbox} 1981This rule should be used to reason inductively about the \texttt{gcd} 1982function. It usually makes the induction hypothesis available at all 1983recursive calls, leading to very direct proofs. If any termination conditions 1984remain unproved, they will become additional premises of this rule. 1985 1986\index{recursion!general|)} 1987\index{*recdef|)} 1988 1989 1990\section{Example: Cantor's Theorem}\label{sec:hol-cantor} 1991Cantor's Theorem states that every set has more subsets than it has 1992elements. It has become a favourite example in higher-order logic since 1993it is so easily expressed: 1994\[ \forall f::\alpha \To \alpha \To bool. \exists S::\alpha\To bool. 1995 \forall x::\alpha. f~x \not= S 1996\] 1997% 1998Viewing types as sets, $\alpha\To bool$ represents the powerset 1999of~$\alpha$. This version states that for every function from $\alpha$ to 2000its powerset, some subset is outside its range. 2001 2002The Isabelle proof uses HOL's set theory, with the type $\alpha\,set$ and 2003the operator \cdx{range}. 2004\begin{ttbox} 2005context Set.thy; 2006\end{ttbox} 2007The set~$S$ is given as an unknown instead of a 2008quantified variable so that we may inspect the subset found by the proof. 2009\begin{ttbox} 2010Goal "?S ~: range\thinspace(f :: 'a=>'a set)"; 2011{\out Level 0} 2012{\out ?S ~: range f} 2013{\out 1. ?S ~: range f} 2014\end{ttbox} 2015The first two steps are routine. The rule \tdx{rangeE} replaces 2016$\Var{S}\in \texttt{range} \, f$ by $\Var{S}=f~x$ for some~$x$. 2017\begin{ttbox} 2018by (resolve_tac [notI] 1); 2019{\out Level 1} 2020{\out ?S ~: range f} 2021{\out 1. ?S : range f ==> False} 2022\ttbreak 2023by (eresolve_tac [rangeE] 1); 2024{\out Level 2} 2025{\out ?S ~: range f} 2026{\out 1. !!x. ?S = f x ==> False} 2027\end{ttbox} 2028Next, we apply \tdx{equalityCE}, reasoning that since $\Var{S}=f~x$, 2029we have $\Var{c}\in \Var{S}$ if and only if $\Var{c}\in f~x$ for 2030any~$\Var{c}$. 2031\begin{ttbox} 2032by (eresolve_tac [equalityCE] 1); 2033{\out Level 3} 2034{\out ?S ~: range f} 2035{\out 1. !!x. [| ?c3 x : ?S; ?c3 x : f x |] ==> False} 2036{\out 2. !!x. [| ?c3 x ~: ?S; ?c3 x ~: f x |] ==> False} 2037\end{ttbox} 2038Now we use a bit of creativity. Suppose that~$\Var{S}$ has the form of a 2039comprehension. Then $\Var{c}\in\{x.\Var{P}~x\}$ implies 2040$\Var{P}~\Var{c}$. Destruct-resolution using \tdx{CollectD} 2041instantiates~$\Var{S}$ and creates the new assumption. 2042\begin{ttbox} 2043by (dresolve_tac [CollectD] 1); 2044{\out Level 4} 2045{\out {\ttlbrace}x. ?P7 x{\ttrbrace} ~: range f} 2046{\out 1. !!x. [| ?c3 x : f x; ?P7(?c3 x) |] ==> False} 2047{\out 2. !!x. [| ?c3 x ~: {\ttlbrace}x. ?P7 x{\ttrbrace}; ?c3 x ~: f x |] ==> False} 2048\end{ttbox} 2049Forcing a contradiction between the two assumptions of subgoal~1 2050completes the instantiation of~$S$. It is now the set $\{x. x\not\in 2051f~x\}$, which is the standard diagonal construction. 2052\begin{ttbox} 2053by (contr_tac 1); 2054{\out Level 5} 2055{\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f} 2056{\out 1. !!x. [| x ~: {\ttlbrace}x. x ~: f x{\ttrbrace}; x ~: f x |] ==> False} 2057\end{ttbox} 2058The rest should be easy. To apply \tdx{CollectI} to the negated 2059assumption, we employ \ttindex{swap_res_tac}: 2060\begin{ttbox} 2061by (swap_res_tac [CollectI] 1); 2062{\out Level 6} 2063{\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f} 2064{\out 1. !!x. [| x ~: f x; ~ False |] ==> x ~: f x} 2065\ttbreak 2066by (assume_tac 1); 2067{\out Level 7} 2068{\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f} 2069{\out No subgoals!} 2070\end{ttbox} 2071How much creativity is required? As it happens, Isabelle can prove this 2072theorem automatically. The default classical set \texttt{claset()} contains 2073rules for most of the constructs of HOL's set theory. We must augment it with 2074\tdx{equalityCE} to break up set equalities, and then apply best-first search. 2075Depth-first search would diverge, but best-first search successfully navigates 2076through the large search space. \index{search!best-first} 2077\begin{ttbox} 2078choplev 0; 2079{\out Level 0} 2080{\out ?S ~: range f} 2081{\out 1. ?S ~: range f} 2082\ttbreak 2083by (best_tac (claset() addSEs [equalityCE]) 1); 2084{\out Level 1} 2085{\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f} 2086{\out No subgoals!} 2087\end{ttbox} 2088If you run this example interactively, make sure your current theory contains 2089theory \texttt{Set}, for example by executing \ttindex{context}~{\tt Set.thy}. 2090Otherwise the default claset may not contain the rules for set theory. 2091\index{higher-order logic|)} 2092 2093%%% Local Variables: 2094%%% mode: latex 2095%%% TeX-master: "logics-HOL" 2096%%% End: 2097