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;
     1 %% $Id$

     2 \chapter{Higher-Order Logic}

     3 \index{higher-order logic|(}

     4 \index{HOL system@{\sc hol} system}

     5

     6 The theory~\thydx{HOL} implements higher-order logic.  It is based on

     7 Gordon's~{\sc hol} system~\cite{mgordon-hol}, which itself is based on

     8 Church's original paper~\cite{church40}.  Andrews's book~\cite{andrews86} is a

     9 full description of the original Church-style higher-order logic.  Experience

    10 with the {\sc hol} system has demonstrated that higher-order logic is widely

    11 applicable in many areas of mathematics and computer science, not just

    12 hardware verification, {\sc hol}'s original \textit{raison d'{\^e}tre\/}.  It

    13 is weaker than ZF set theory but for most applications this does not matter.

    14 If you prefer {\ML} to Lisp, you will probably prefer HOL to~ZF.

    15

    16 The syntax of HOL\footnote{Earlier versions of Isabelle's HOL used a different

    17   syntax.  Ancient releases of Isabelle included still another version of~HOL,

    18   with explicit type inference rules~\cite{paulson-COLOG}.  This version no

    19   longer exists, but \thydx{ZF} supports a similar style of reasoning.}

    20 follows $\lambda$-calculus and functional programming.  Function application

    21 is curried.  To apply the function~$f$ of type $\tau@1\To\tau@2\To\tau@3$ to

    22 the arguments~$a$ and~$b$ in HOL, you simply write $f\,a\,b$.  There is no

    23 apply' operator as in \thydx{ZF}.  Note that $f(a,b)$ means $f$ applied to

    24 the pair $(a,b)$'' in HOL.  We write ordered pairs as $(a,b)$, not $\langle   25 a,b\rangle$ as in ZF.

    26

    27 HOL has a distinct feel, compared with ZF and CTT.  It identifies object-level

    28 types with meta-level types, taking advantage of Isabelle's built-in

    29 type-checker.  It identifies object-level functions with meta-level functions,

    30 so it uses Isabelle's operations for abstraction and application.

    31

    32 These identifications allow Isabelle to support HOL particularly nicely, but

    33 they also mean that HOL requires more sophistication from the user --- in

    34 particular, an understanding of Isabelle's type system.  Beginners should work

    35 with \texttt{show_types} (or even \texttt{show_sorts}) set to \texttt{true}.

    36

    37

    38 \begin{figure}

    39 \begin{constants}

    40   \it name      &\it meta-type  & \it description \\

    41   \cdx{Trueprop}& $bool\To prop$                & coercion to $prop$\\

    42   \cdx{Not}     & $bool\To bool$                & negation ($\lnot$) \\

    43   \cdx{True}    & $bool$                        & tautology ($\top$) \\

    44   \cdx{False}   & $bool$                        & absurdity ($\bot$) \\

    45   \cdx{If}      & $[bool,\alpha,\alpha]\To\alpha$ & conditional \\

    46   \cdx{Let}     & $[\alpha,\alpha\To\beta]\To\beta$ & let binder

    47 \end{constants}

    48 \subcaption{Constants}

    49

    50 \begin{constants}

    51 \index{"@@{\tt\at} symbol}

    52 \index{*"! symbol}\index{*"? symbol}

    53 \index{*"?"! symbol}\index{*"E"X"! symbol}

    54   \it symbol &\it name     &\it meta-type & \it description \\

    55   \sdx{SOME} or \tt\at & \cdx{Eps}  & $(\alpha\To bool)\To\alpha$ &

    56         Hilbert description ($\varepsilon$) \\

    57   \sdx{ALL} or {\tt!~} & \cdx{All}  & $(\alpha\To bool)\To bool$ &

    58         universal quantifier ($\forall$) \\

    59   \sdx{EX} or {\tt?~}  & \cdx{Ex}   & $(\alpha\To bool)\To bool$ &

    60         existential quantifier ($\exists$) \\

    61   \texttt{EX!} or {\tt?!} & \cdx{Ex1}  & $(\alpha\To bool)\To bool$ &

    62         unique existence ($\exists!$)\\

    63   \texttt{LEAST}  & \cdx{Least}  & $(\alpha::ord \To bool)\To\alpha$ &

    64         least element

    65 \end{constants}

    66 \subcaption{Binders}

    67

    68 \begin{constants}

    69 \index{*"= symbol}

    70 \index{&@{\tt\&} symbol}

    71 \index{*"| symbol}

    72 \index{*"-"-"> symbol}

    73   \it symbol    & \it meta-type & \it priority & \it description \\

    74   \sdx{o}       & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ &

    75         Left 55 & composition ($\circ$) \\

    76   \tt =         & $[\alpha,\alpha]\To bool$ & Left 50 & equality ($=$) \\

    77   \tt <         & $[\alpha::ord,\alpha]\To bool$ & Left 50 & less than ($<$) \\

    78   \tt <=        & $[\alpha::ord,\alpha]\To bool$ & Left 50 &

    79                 less than or equals ($\leq$)\\

    80   \tt \&        & $[bool,bool]\To bool$ & Right 35 & conjunction ($\conj$) \\

    81   \tt |         & $[bool,bool]\To bool$ & Right 30 & disjunction ($\disj$) \\

    82   \tt -->       & $[bool,bool]\To bool$ & Right 25 & implication ($\imp$)

    83 \end{constants}

    84 \subcaption{Infixes}

    85 \caption{Syntax of \texttt{HOL}} \label{hol-constants}

    86 \end{figure}

    87

    88

    89 \begin{figure}

    90 \index{*let symbol}

    91 \index{*in symbol}

    92 \dquotes

    93 $\begin{array}{rclcl}   94 term & = & \hbox{expression of class~term} \\   95 & | & "SOME~" id " . " formula   96 & | & "\at~" id " . " formula \\   97 & | &   98 \multicolumn{3}{l}{"let"~id~"="~term";"\dots";"~id~"="~term~"in"~term} \\   99 & | &   100 \multicolumn{3}{l}{"if"~formula~"then"~term~"else"~term} \\   101 & | & "LEAST"~ id " . " formula \\[2ex]   102 formula & = & \hbox{expression of type~bool} \\   103 & | & term " = " term \\   104 & | & term " \ttilde= " term \\   105 & | & term " < " term \\   106 & | & term " <= " term \\   107 & | & "\ttilde\ " formula \\   108 & | & formula " \& " formula \\   109 & | & formula " | " formula \\   110 & | & formula " --> " formula \\   111 & | & "ALL~" id~id^* " . " formula   112 & | & "!~~~" id~id^* " . " formula \\   113 & | & "EX~~" id~id^* " . " formula   114 & | & "?~~~" id~id^* " . " formula \\   115 & | & "EX!~" id~id^* " . " formula   116 & | & "?!~~" id~id^* " . " formula \\   117 \end{array}   118$

   119 \caption{Full grammar for HOL} \label{hol-grammar}

   120 \end{figure}

   121

   122

   123 \section{Syntax}

   124

   125 Figure~\ref{hol-constants} lists the constants (including infixes and

   126 binders), while Fig.\ts\ref{hol-grammar} presents the grammar of

   127 higher-order logic.  Note that $a$\verb|~=|$b$ is translated to

   128 $\lnot(a=b)$.

   129

   130 \begin{warn}

   131   HOL has no if-and-only-if connective; logical equivalence is expressed using

   132   equality.  But equality has a high priority, as befitting a relation, while

   133   if-and-only-if typically has the lowest priority.  Thus, $\lnot\lnot P=P$

   134   abbreviates $\lnot\lnot (P=P)$ and not $(\lnot\lnot P)=P$.  When using $=$

   135   to mean logical equivalence, enclose both operands in parentheses.

   136 \end{warn}

   137

   138 \subsection{Types and overloading}

   139 The universal type class of higher-order terms is called~\cldx{term}.

   140 By default, explicit type variables have class \cldx{term}.  In

   141 particular the equality symbol and quantifiers are polymorphic over

   142 class \texttt{term}.

   143

   144 The type of formulae, \tydx{bool}, belongs to class \cldx{term}; thus,

   145 formulae are terms.  The built-in type~\tydx{fun}, which constructs

   146 function types, is overloaded with arity {\tt(term,\thinspace

   147   term)\thinspace term}.  Thus, $\sigma\To\tau$ belongs to class~{\tt

   148   term} if $\sigma$ and~$\tau$ do, allowing quantification over

   149 functions.

   150

   151 HOL allows new types to be declared as subsets of existing types;

   152 see~{\S}\ref{sec:HOL:Types}.  ML-like datatypes can also be declared; see

   153 ~{\S}\ref{sec:HOL:datatype}.

   154

   155 Several syntactic type classes --- \cldx{plus}, \cldx{minus},

   156 \cldx{times} and

   157 \cldx{power} --- permit overloading of the operators {\tt+},\index{*"+

   158   symbol} {\tt-}\index{*"- symbol}, {\tt*}.\index{*"* symbol}

   159 and \verb|^|.\index{^@\verb.^. symbol}

   160 %

   161 They are overloaded to denote the obvious arithmetic operations on types

   162 \tdx{nat}, \tdx{int} and~\tdx{real}. (With the \verb|^| operator, the

   163 exponent always has type~\tdx{nat}.)  Non-arithmetic overloadings are also

   164 done: the operator {\tt-} can denote set difference, while \verb|^| can

   165 denote exponentiation of relations (iterated composition).  Unary minus is

   166 also written as~{\tt-} and is overloaded like its 2-place counterpart; it even

   167 can stand for set complement.

   168

   169 The constant \cdx{0} is also overloaded.  It serves as the zero element of

   170 several types, of which the most important is \tdx{nat} (the natural

   171 numbers).  The type class \cldx{plus_ac0} comprises all types for which 0

   172 and~+ satisfy the laws $x+y=y+x$, $(x+y)+z = x+(y+z)$ and $0+x = x$.  These

   173 types include the numeric ones \tdx{nat}, \tdx{int} and~\tdx{real} and also

   174 multisets.  The summation operator \cdx{setsum} is available for all types in

   175 this class.

   176

   177 Theory \thydx{Ord} defines the syntactic class \cldx{ord} of order

   178 signatures.  The relations $<$ and $\leq$ are polymorphic over this

   179 class, as are the functions \cdx{mono}, \cdx{min} and \cdx{max}, and

   180 the \cdx{LEAST} operator. \thydx{Ord} also defines a subclass

   181 \cldx{order} of \cldx{ord} which axiomatizes the types that are partially

   182 ordered with respect to~$\leq$.  A further subclass \cldx{linorder} of

   183 \cldx{order} axiomatizes linear orderings.

   184 For details, see the file \texttt{Ord.thy}.

   185

   186 If you state a goal containing overloaded functions, you may need to include

   187 type constraints.  Type inference may otherwise make the goal more

   188 polymorphic than you intended, with confusing results.  For example, the

   189 variables $i$, $j$ and $k$ in the goal $i \leq j \Imp i \leq j+k$ have type

   190 $\alpha::\{ord,plus\}$, although you may have expected them to have some

   191 numeric type, e.g. $nat$.  Instead you should have stated the goal as

   192 $(i::nat) \leq j \Imp i \leq j+k$, which causes all three variables to have

   193 type $nat$.

   194

   195 \begin{warn}

   196   If resolution fails for no obvious reason, try setting

   197   \ttindex{show_types} to \texttt{true}, causing Isabelle to display

   198   types of terms.  Possibly set \ttindex{show_sorts} to \texttt{true} as

   199   well, causing Isabelle to display type classes and sorts.

   200

   201   \index{unification!incompleteness of}

   202   Where function types are involved, Isabelle's unification code does not

   203   guarantee to find instantiations for type variables automatically.  Be

   204   prepared to use \ttindex{res_inst_tac} instead of \texttt{resolve_tac},

   205   possibly instantiating type variables.  Setting

   206   \ttindex{Unify.trace_types} to \texttt{true} causes Isabelle to report

   207   omitted search paths during unification.\index{tracing!of unification}

   208 \end{warn}

   209

   210

   211 \subsection{Binders}

   212

   213 Hilbert's {\bf description} operator~$\varepsilon x. P[x]$ stands for some~$x$

   214 satisfying~$P$, if such exists.  Since all terms in HOL denote something, a

   215 description is always meaningful, but we do not know its value unless $P$

   216 defines it uniquely.  We may write descriptions as \cdx{Eps}($\lambda x.   217 P[x]$) or use the syntax \hbox{\tt SOME~$x$.~$P[x]$}.

   218

   219 Existential quantification is defined by

   220 $\exists x. P~x \;\equiv\; P(\varepsilon x. P~x).$

   221 The unique existence quantifier, $\exists!x. P$, is defined in terms

   222 of~$\exists$ and~$\forall$.  An Isabelle binder, it admits nested

   223 quantifications.  For instance, $\exists!x\,y. P\,x\,y$ abbreviates

   224 $\exists!x. \exists!y. P\,x\,y$; note that this does not mean that there

   225 exists a unique pair $(x,y)$ satisfying~$P\,x\,y$.

   226

   227 \medskip

   228

   229 \index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system} The

   230 basic Isabelle/HOL binders have two notations.  Apart from the usual

   231 \texttt{ALL} and \texttt{EX} for $\forall$ and $\exists$, Isabelle/HOL also

   232 supports the original notation of Gordon's {\sc hol} system: \texttt{!}\

   233 and~\texttt{?}.  In the latter case, the existential quantifier \emph{must} be

   234 followed by a space; thus {\tt?x} is an unknown, while \verb'? x. f x=y' is a

   235 quantification.  Both notations are accepted for input.  The print mode

   236 \ttindexbold{HOL}'' governs the output notation.  If enabled (e.g.\ by

   237 passing option \texttt{-m HOL} to the \texttt{isabelle} executable),

   238 then~{\tt!}\ and~{\tt?}\ are displayed.

   239

   240 \medskip

   241

   242 If $\tau$ is a type of class \cldx{ord}, $P$ a formula and $x$ a

   243 variable of type $\tau$, then the term \cdx{LEAST}~$x. P[x]$ is defined

   244 to be the least (w.r.t.\ $\leq$) $x$ such that $P~x$ holds (see

   245 Fig.~\ref{hol-defs}).  The definition uses Hilbert's $\varepsilon$

   246 choice operator, so \texttt{Least} is always meaningful, but may yield

   247 nothing useful in case there is not a unique least element satisfying

   248 $P$.\footnote{Class $ord$ does not require much of its instances, so

   249   $\leq$ need not be a well-ordering, not even an order at all!}

   250

   251 \medskip All these binders have priority 10.

   252

   253 \begin{warn}

   254 The low priority of binders means that they need to be enclosed in

   255 parenthesis when they occur in the context of other operations.  For example,

   256 instead of $P \land \forall x. Q$ you need to write $P \land (\forall x. Q)$.

   257 \end{warn}

   258

   259

   260 \subsection{The let and case constructions}

   261 Local abbreviations can be introduced by a \texttt{let} construct whose

   262 syntax appears in Fig.\ts\ref{hol-grammar}.  Internally it is translated into

   263 the constant~\cdx{Let}.  It can be expanded by rewriting with its

   264 definition, \tdx{Let_def}.

   265

   266 HOL also defines the basic syntax

   267 $\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n$

   268 as a uniform means of expressing \texttt{case} constructs.  Therefore \texttt{case}

   269 and \sdx{of} are reserved words.  Initially, this is mere syntax and has no

   270 logical meaning.  By declaring translations, you can cause instances of the

   271 \texttt{case} construct to denote applications of particular case operators.

   272 This is what happens automatically for each \texttt{datatype} definition

   273 (see~{\S}\ref{sec:HOL:datatype}).

   274

   275 \begin{warn}

   276 Both \texttt{if} and \texttt{case} constructs have as low a priority as

   277 quantifiers, which requires additional enclosing parentheses in the context

   278 of most other operations.  For example, instead of $f~x = {\tt if\dots   279 then\dots else}\dots$ you need to write $f~x = ({\tt if\dots then\dots   280 else\dots})$.

   281 \end{warn}

   282

   283 \section{Rules of inference}

   284

   285 \begin{figure}

   286 \begin{ttbox}\makeatother

   287 \tdx{refl}          t = (t::'a)

   288 \tdx{subst}         [| s = t; P s |] ==> P (t::'a)

   289 \tdx{ext}           (!!x::'a. (f x :: 'b) = g x) ==> (\%x. f x) = (\%x. g x)

   290 \tdx{impI}          (P ==> Q) ==> P-->Q

   291 \tdx{mp}            [| P-->Q;  P |] ==> Q

   292 \tdx{iff}           (P-->Q) --> (Q-->P) --> (P=Q)

   293 \tdx{someI}         P(x::'a) ==> P(@x. P x)

   294 \tdx{True_or_False} (P=True) | (P=False)

   295 \end{ttbox}

   296 \caption{The \texttt{HOL} rules} \label{hol-rules}

   297 \end{figure}

   298

   299 Figure~\ref{hol-rules} shows the primitive inference rules of~HOL, with

   300 their~{\ML} names.  Some of the rules deserve additional comments:

   301 \begin{ttdescription}

   302 \item[\tdx{ext}] expresses extensionality of functions.

   303 \item[\tdx{iff}] asserts that logically equivalent formulae are

   304   equal.

   305 \item[\tdx{someI}] gives the defining property of the Hilbert

   306   $\varepsilon$-operator.  It is a form of the Axiom of Choice.  The derived rule

   307   \tdx{some_equality} (see below) is often easier to use.

   308 \item[\tdx{True_or_False}] makes the logic classical.\footnote{In

   309     fact, the $\varepsilon$-operator already makes the logic classical, as

   310     shown by Diaconescu; see Paulson~\cite{paulson-COLOG} for details.}

   311 \end{ttdescription}

   312

   313

   314 \begin{figure}\hfuzz=4pt%suppress "Overfull \hbox" message

   315 \begin{ttbox}\makeatother

   316 \tdx{True_def}   True     == ((\%x::bool. x)=(\%x. x))

   317 \tdx{All_def}    All      == (\%P. P = (\%x. True))

   318 \tdx{Ex_def}     Ex       == (\%P. P(@x. P x))

   319 \tdx{False_def}  False    == (!P. P)

   320 \tdx{not_def}    not      == (\%P. P-->False)

   321 \tdx{and_def}    op &     == (\%P Q. !R. (P-->Q-->R) --> R)

   322 \tdx{or_def}     op |     == (\%P Q. !R. (P-->R) --> (Q-->R) --> R)

   323 \tdx{Ex1_def}    Ex1      == (\%P. ? x. P x & (! y. P y --> y=x))

   324

   325 \tdx{o_def}      op o     == (\%(f::'b=>'c) g x::'a. f(g x))

   326 \tdx{if_def}     If P x y ==

   327               (\%P x y. @z::'a.(P=True --> z=x) & (P=False --> z=y))

   328 \tdx{Let_def}    Let s f  == f s

   329 \tdx{Least_def}  Least P  == @x. P(x) & (ALL y. P(y) --> x <= y)"

   330 \end{ttbox}

   331 \caption{The \texttt{HOL} definitions} \label{hol-defs}

   332 \end{figure}

   333

   334

   335 HOL follows standard practice in higher-order logic: only a few connectives

   336 are taken as primitive, with the remainder defined obscurely

   337 (Fig.\ts\ref{hol-defs}).  Gordon's {\sc hol} system expresses the

   338 corresponding definitions \cite[page~270]{mgordon-hol} using

   339 object-equality~({\tt=}), which is possible because equality in higher-order

   340 logic may equate formulae and even functions over formulae.  But theory~HOL,

   341 like all other Isabelle theories, uses meta-equality~({\tt==}) for

   342 definitions.

   343 \begin{warn}

   344 The definitions above should never be expanded and are shown for completeness

   345 only.  Instead users should reason in terms of the derived rules shown below

   346 or, better still, using high-level tactics

   347 (see~{\S}\ref{sec:HOL:generic-packages}).

   348 \end{warn}

   349

   350 Some of the rules mention type variables; for example, \texttt{refl}

   351 mentions the type variable~{\tt'a}.  This allows you to instantiate

   352 type variables explicitly by calling \texttt{res_inst_tac}.

   353

   354

   355 \begin{figure}

   356 \begin{ttbox}

   357 \tdx{sym}         s=t ==> t=s

   358 \tdx{trans}       [| r=s; s=t |] ==> r=t

   359 \tdx{ssubst}      [| t=s; P s |] ==> P t

   360 \tdx{box_equals}  [| a=b;  a=c;  b=d |] ==> c=d

   361 \tdx{arg_cong}    x = y ==> f x = f y

   362 \tdx{fun_cong}    f = g ==> f x = g x

   363 \tdx{cong}        [| f = g; x = y |] ==> f x = g y

   364 \tdx{not_sym}     t ~= s ==> s ~= t

   365 \subcaption{Equality}

   366

   367 \tdx{TrueI}       True

   368 \tdx{FalseE}      False ==> P

   369

   370 \tdx{conjI}       [| P; Q |] ==> P&Q

   371 \tdx{conjunct1}   [| P&Q |] ==> P

   372 \tdx{conjunct2}   [| P&Q |] ==> Q

   373 \tdx{conjE}       [| P&Q;  [| P; Q |] ==> R |] ==> R

   374

   375 \tdx{disjI1}      P ==> P|Q

   376 \tdx{disjI2}      Q ==> P|Q

   377 \tdx{disjE}       [| P | Q; P ==> R; Q ==> R |] ==> R

   378

   379 \tdx{notI}        (P ==> False) ==> ~ P

   380 \tdx{notE}        [| ~ P;  P |] ==> R

   381 \tdx{impE}        [| P-->Q;  P;  Q ==> R |] ==> R

   382 \subcaption{Propositional logic}

   383

   384 \tdx{iffI}        [| P ==> Q;  Q ==> P |] ==> P=Q

   385 \tdx{iffD1}       [| P=Q; P |] ==> Q

   386 \tdx{iffD2}       [| P=Q; Q |] ==> P

   387 \tdx{iffE}        [| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R

   388 \subcaption{Logical equivalence}

   389

   390 \end{ttbox}

   391 \caption{Derived rules for HOL} \label{hol-lemmas1}

   392 \end{figure}

   393 %

   394 %\tdx{eqTrueI}     P ==> P=True

   395 %\tdx{eqTrueE}     P=True ==> P

   396

   397

   398 \begin{figure}

   399 \begin{ttbox}\makeatother

   400 \tdx{allI}      (!!x. P x) ==> !x. P x

   401 \tdx{spec}      !x. P x ==> P x

   402 \tdx{allE}      [| !x. P x;  P x ==> R |] ==> R

   403 \tdx{all_dupE}  [| !x. P x;  [| P x; !x. P x |] ==> R |] ==> R

   404

   405 \tdx{exI}       P x ==> ? x. P x

   406 \tdx{exE}       [| ? x. P x; !!x. P x ==> Q |] ==> Q

   407

   408 \tdx{ex1I}      [| P a;  !!x. P x ==> x=a |] ==> ?! x. P x

   409 \tdx{ex1E}      [| ?! x. P x;  !!x. [| P x;  ! y. P y --> y=x |] ==> R

   410           |] ==> R

   411

   412 \tdx{some_equality}   [| P a;  !!x. P x ==> x=a |] ==> (@x. P x) = a

   413 \subcaption{Quantifiers and descriptions}

   414

   415 \tdx{ccontr}          (~P ==> False) ==> P

   416 \tdx{classical}       (~P ==> P) ==> P

   417 \tdx{excluded_middle} ~P | P

   418

   419 \tdx{disjCI}       (~Q ==> P) ==> P|Q

   420 \tdx{exCI}         (! x. ~ P x ==> P a) ==> ? x. P x

   421 \tdx{impCE}        [| P-->Q; ~ P ==> R; Q ==> R |] ==> R

   422 \tdx{iffCE}        [| P=Q;  [| P;Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R

   423 \tdx{notnotD}      ~~P ==> P

   424 \tdx{swap}         ~P ==> (~Q ==> P) ==> Q

   425 \subcaption{Classical logic}

   426

   427 \tdx{if_P}         P ==> (if P then x else y) = x

   428 \tdx{if_not_P}     ~ P ==> (if P then x else y) = y

   429 \tdx{split_if}     P(if Q then x else y) = ((Q --> P x) & (~Q --> P y))

   430 \subcaption{Conditionals}

   431 \end{ttbox}

   432 \caption{More derived rules} \label{hol-lemmas2}

   433 \end{figure}

   434

   435 Some derived rules are shown in Figures~\ref{hol-lemmas1}

   436 and~\ref{hol-lemmas2}, with their {\ML} names.  These include natural rules

   437 for the logical connectives, as well as sequent-style elimination rules for

   438 conjunctions, implications, and universal quantifiers.

   439

   440 Note the equality rules: \tdx{ssubst} performs substitution in

   441 backward proofs, while \tdx{box_equals} supports reasoning by

   442 simplifying both sides of an equation.

   443

   444 The following simple tactics are occasionally useful:

   445 \begin{ttdescription}

   446 \item[\ttindexbold{strip_tac} $i$] applies \texttt{allI} and \texttt{impI}

   447   repeatedly to remove all outermost universal quantifiers and implications

   448   from subgoal $i$.

   449 \item[\ttindexbold{case_tac} {\tt"}$P${\tt"} $i$] performs case distinction on

   450   $P$ for subgoal $i$: the latter is replaced by two identical subgoals with

   451   the added assumptions $P$ and $\lnot P$, respectively.

   452 \item[\ttindexbold{smp_tac} $j$ $i$] applies $j$ times \texttt{spec} and then

   453   \texttt{mp} in subgoal $i$, which is typically useful when forward-chaining

   454   from an induction hypothesis. As a generalization of \texttt{mp_tac},

   455   if there are assumptions $\forall \vec{x}. P \vec{x} \imp Q \vec{x}$ and

   456   $P \vec{a}$, ($\vec{x}$ being a vector of $j$ variables)

   457   then it replaces the universally quantified implication by $Q \vec{a}$.

   458   It may instantiate unknowns. It fails if it can do nothing.

   459 \end{ttdescription}

   460

   461

   462 \begin{figure}

   463 \begin{center}

   464 \begin{tabular}{rrr}

   465   \it name      &\it meta-type  & \it description \\

   466 \index{{}@\verb'{}' symbol}

   467   \verb|{}|     & $\alpha\,set$         & the empty set \\

   468   \cdx{insert}  & $[\alpha,\alpha\,set]\To \alpha\,set$

   469         & insertion of element \\

   470   \cdx{Collect} & $(\alpha\To bool)\To\alpha\,set$

   471         & comprehension \\

   472   \cdx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$

   473         & intersection over a set\\

   474   \cdx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$

   475         & union over a set\\

   476   \cdx{Inter} & $(\alpha\,set)set\To\alpha\,set$

   477         &set of sets intersection \\

   478   \cdx{Union} & $(\alpha\,set)set\To\alpha\,set$

   479         &set of sets union \\

   480   \cdx{Pow}   & $\alpha\,set \To (\alpha\,set)set$

   481         & powerset \$1ex]   482 \cdx{range} & (\alpha\To\beta )\To\beta\,set   483 & range of a function \\[1ex]   484 \cdx{Ball}~~\cdx{Bex} & [\alpha\,set,\alpha\To bool]\To bool   485 & bounded quantifiers   486 \end{tabular}   487 \end{center}   488 \subcaption{Constants}   489   490 \begin{center}   491 \begin{tabular}{llrrr}   492 \it symbol &\it name &\it meta-type & \it priority & \it description \\   493 \sdx{INT} & \cdx{INTER1} & (\alpha\To\beta\,set)\To\beta\,set & 10 &   494 intersection\\   495 \sdx{UN} & \cdx{UNION1} & (\alpha\To\beta\,set)\To\beta\,set & 10 &   496 union   497 \end{tabular}   498 \end{center}   499 \subcaption{Binders}   500   501 \begin{center}   502 \index{*"" symbol}   503 \index{*": symbol}   504 \index{*"<"= symbol}   505 \begin{tabular}{rrrr}   506 \it symbol & \it meta-type & \it priority & \it description \\   507 \tt  & [\alpha\To\beta ,\alpha\,set]\To \beta\,set   508 & Left 90 & image \\   509 \sdx{Int} & [\alpha\,set,\alpha\,set]\To\alpha\,set   510 & Left 70 & intersection (\int) \\   511 \sdx{Un} & [\alpha\,set,\alpha\,set]\To\alpha\,set   512 & Left 65 & union (\un) \\   513 \tt: & [\alpha ,\alpha\,set]\To bool   514 & Left 50 & membership (\in) \\   515 \tt <= & [\alpha\,set,\alpha\,set]\To bool   516 & Left 50 & subset (\subseteq)   517 \end{tabular}   518 \end{center}   519 \subcaption{Infixes}   520 \caption{Syntax of the theory \texttt{Set}} \label{hol-set-syntax}   521 \end{figure}   522   523   524 \begin{figure}   525 \begin{center} \tt\frenchspacing   526 \index{*"! symbol}   527 \begin{tabular}{rrr}   528 \it external & \it internal & \it description \\   529 a \ttilde: b & \ttilde(a : b) & \rm not in\\   530 {\ttlbrace}a@1, \ldots{\ttrbrace} & insert a@1 \ldots {\ttlbrace}{\ttrbrace} & \rm finite set \\   531 {\ttlbrace}x. P[x]{\ttrbrace} & Collect(\lambda x. P[x]) &   532 \rm comprehension \\   533 \sdx{INT} x:A. B[x] & INTER A \lambda x. B[x] &   534 \rm intersection \\   535 \sdx{UN}{\tt\ } x:A. B[x] & UNION A \lambda x. B[x] &   536 \rm union \\   537 \sdx{ALL} x:A.\ P[x] or \texttt{!} x:A.\ P[x] &   538 Ball A \lambda x.\ P[x] &   539 \rm bounded \forall \\   540 \sdx{EX}{\tt\ } x:A.\ P[x] or \texttt{?} x:A.\ P[x] &   541 Bex A \lambda x.\ P[x] & \rm bounded \exists   542 \end{tabular}   543 \end{center}   544 \subcaption{Translations}   545   546 \dquotes   547 \[\begin{array}{rclcl}   548 term & = & \hbox{other terms\ldots} \\   549 & | & "{\ttlbrace}{\ttrbrace}" \\   550 & | & "{\ttlbrace} " term\; ("," term)^* " {\ttrbrace}" \\   551 & | & "{\ttlbrace} " id " . " formula " {\ttrbrace}" \\   552 & | & term "  " term \\   553 & | & term " Int " term \\   554 & | & term " Un " term \\   555 & | & "INT~~" id ":" term " . " term \\   556 & | & "UN~~~" id ":" term " . " term \\   557 & | & "INT~~" id~id^* " . " term \\   558 & | & "UN~~~" id~id^* " . " term \\[2ex]   559 formula & = & \hbox{other formulae\ldots} \\   560 & | & term " : " term \\   561 & | & term " \ttilde: " term \\   562 & | & term " <= " term \\   563 & | & "ALL " id ":" term " . " formula   564 & | & "!~" id ":" term " . " formula \\   565 & | & "EX~~" id ":" term " . " formula   566 & | & "?~" id ":" term " . " formula \\   567 \end{array}   568$

   569 \subcaption{Full Grammar}

   570 \caption{Syntax of the theory \texttt{Set} (continued)} \label{hol-set-syntax2}

   571 \end{figure}

   572

   573

   574 \section{A formulation of set theory}

   575 Historically, higher-order logic gives a foundation for Russell and

   576 Whitehead's theory of classes.  Let us use modern terminology and call them

   577 {\bf sets}, but note that these sets are distinct from those of ZF set theory,

   578 and behave more like ZF classes.

   579 \begin{itemize}

   580 \item

   581 Sets are given by predicates over some type~$\sigma$.  Types serve to

   582 define universes for sets, but type-checking is still significant.

   583 \item

   584 There is a universal set (for each type).  Thus, sets have complements, and

   585 may be defined by absolute comprehension.

   586 \item

   587 Although sets may contain other sets as elements, the containing set must

   588 have a more complex type.

   589 \end{itemize}

   590 Finite unions and intersections have the same behaviour in HOL as they do

   591 in~ZF.  In HOL the intersection of the empty set is well-defined, denoting the

   592 universal set for the given type.

   593

   594 \subsection{Syntax of set theory}\index{*set type}

   595 HOL's set theory is called \thydx{Set}.  The type $\alpha\,set$ is essentially

   596 the same as $\alpha\To bool$.  The new type is defined for clarity and to

   597 avoid complications involving function types in unification.  The isomorphisms

   598 between the two types are declared explicitly.  They are very natural:

   599 \texttt{Collect} maps $\alpha\To bool$ to $\alpha\,set$, while \hbox{\tt op :}

   600 maps in the other direction (ignoring argument order).

   601

   602 Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax

   603 translations.  Figure~\ref{hol-set-syntax2} presents the grammar of the new

   604 constructs.  Infix operators include union and intersection ($A\un B$

   605 and $A\int B$), the subset and membership relations, and the image

   606 operator~{\tt}\@.  Note that $a$\verb|~:|$b$ is translated to

   607 $\lnot(a\in b)$.

   608

   609 The $\{a@1,\ldots\}$ notation abbreviates finite sets constructed in

   610 the obvious manner using~\texttt{insert} and~$\{\}$:

   611 \begin{eqnarray*}

   612   \{a, b, c\} & \equiv &

   613   \texttt{insert} \, a \, ({\tt insert} \, b \, ({\tt insert} \, c \, \{\}))

   614 \end{eqnarray*}

   615

   616 The set \hbox{\tt{\ttlbrace}$x$.\ $P[x]${\ttrbrace}} consists of all $x$ (of

   617 suitable type) that satisfy~$P[x]$, where $P[x]$ is a formula that may contain

   618 free occurrences of~$x$.  This syntax expands to \cdx{Collect}$(\lambda x.   619 P[x])$.  It defines sets by absolute comprehension, which is impossible in~ZF;

   620 the type of~$x$ implicitly restricts the comprehension.

   621

   622 The set theory defines two {\bf bounded quantifiers}:

   623 \begin{eqnarray*}

   624    \forall x\in A. P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\

   625    \exists x\in A. P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x]

   626 \end{eqnarray*}

   627 The constants~\cdx{Ball} and~\cdx{Bex} are defined

   628 accordingly.  Instead of \texttt{Ball $A$ $P$} and \texttt{Bex $A$ $P$} we may

   629 write\index{*"! symbol}\index{*"? symbol}

   630 \index{*ALL symbol}\index{*EX symbol}

   631 %

   632 \hbox{\tt ALL~$x$:$A$.\ $P[x]$} and \hbox{\tt EX~$x$:$A$.\ $P[x]$}.  The

   633 original notation of Gordon's {\sc hol} system is supported as well:

   634 \texttt{!}\ and \texttt{?}.

   635

   636 Unions and intersections over sets, namely $\bigcup@{x\in A}B[x]$ and

   637 $\bigcap@{x\in A}B[x]$, are written

   638 \sdx{UN}~\hbox{\tt$x$:$A$.\ $B[x]$} and

   639 \sdx{INT}~\hbox{\tt$x$:$A$.\ $B[x]$}.

   640

   641 Unions and intersections over types, namely $\bigcup@x B[x]$ and $\bigcap@x   642 B[x]$, are written \sdx{UN}~\hbox{\tt$x$.\ $B[x]$} and

   643 \sdx{INT}~\hbox{\tt$x$.\ $B[x]$}.  They are equivalent to the previous

   644 union and intersection operators when $A$ is the universal set.

   645

   646 The operators $\bigcup A$ and $\bigcap A$ act upon sets of sets.  They are

   647 not binders, but are equal to $\bigcup@{x\in A}x$ and $\bigcap@{x\in A}x$,

   648 respectively.

   649

   650

   651

   652 \begin{figure} \underscoreon

   653 \begin{ttbox}

   654 \tdx{mem_Collect_eq}    (a : {\ttlbrace}x. P x{\ttrbrace}) = P a

   655 \tdx{Collect_mem_eq}    {\ttlbrace}x. x:A{\ttrbrace} = A

   656

   657 \tdx{empty_def}         {\ttlbrace}{\ttrbrace}          == {\ttlbrace}x. False{\ttrbrace}

   658 \tdx{insert_def}        insert a B  == {\ttlbrace}x. x=a{\ttrbrace} Un B

   659 \tdx{Ball_def}          Ball A P    == ! x. x:A --> P x

   660 \tdx{Bex_def}           Bex A P     == ? x. x:A & P x

   661 \tdx{subset_def}        A <= B      == ! x:A. x:B

   662 \tdx{Un_def}            A Un B      == {\ttlbrace}x. x:A | x:B{\ttrbrace}

   663 \tdx{Int_def}           A Int B     == {\ttlbrace}x. x:A & x:B{\ttrbrace}

   664 \tdx{set_diff_def}      A - B       == {\ttlbrace}x. x:A & x~:B{\ttrbrace}

   665 \tdx{Compl_def}         -A          == {\ttlbrace}x. ~ x:A{\ttrbrace}

   666 \tdx{INTER_def}         INTER A B   == {\ttlbrace}y. ! x:A. y: B x{\ttrbrace}

   667 \tdx{UNION_def}         UNION A B   == {\ttlbrace}y. ? x:A. y: B x{\ttrbrace}

   668 \tdx{INTER1_def}        INTER1 B    == INTER {\ttlbrace}x. True{\ttrbrace} B

   669 \tdx{UNION1_def}        UNION1 B    == UNION {\ttlbrace}x. True{\ttrbrace} B

   670 \tdx{Inter_def}         Inter S     == (INT x:S. x)

   671 \tdx{Union_def}         Union S     == (UN  x:S. x)

   672 \tdx{Pow_def}           Pow A       == {\ttlbrace}B. B <= A{\ttrbrace}

   673 \tdx{image_def}         fA        == {\ttlbrace}y. ? x:A. y=f x{\ttrbrace}

   674 \tdx{range_def}         range f     == {\ttlbrace}y. ? x. y=f x{\ttrbrace}

   675 \end{ttbox}

   676 \caption{Rules of the theory \texttt{Set}} \label{hol-set-rules}

   677 \end{figure}

   678

   679

   680 \begin{figure} \underscoreon

   681 \begin{ttbox}

   682 \tdx{CollectI}        [| P a |] ==> a : {\ttlbrace}x. P x{\ttrbrace}

   683 \tdx{CollectD}        [| a : {\ttlbrace}x. P x{\ttrbrace} |] ==> P a

   684 \tdx{CollectE}        [| a : {\ttlbrace}x. P x{\ttrbrace};  P a ==> W |] ==> W

   685

   686 \tdx{ballI}           [| !!x. x:A ==> P x |] ==> ! x:A. P x

   687 \tdx{bspec}           [| ! x:A. P x;  x:A |] ==> P x

   688 \tdx{ballE}           [| ! x:A. P x;  P x ==> Q;  ~ x:A ==> Q |] ==> Q

   689

   690 \tdx{bexI}            [| P x;  x:A |] ==> ? x:A. P x

   691 \tdx{bexCI}           [| ! x:A. ~ P x ==> P a;  a:A |] ==> ? x:A. P x

   692 \tdx{bexE}            [| ? x:A. P x;  !!x. [| x:A; P x |] ==> Q  |] ==> Q

   693 \subcaption{Comprehension and Bounded quantifiers}

   694

   695 \tdx{subsetI}         (!!x. x:A ==> x:B) ==> A <= B

   696 \tdx{subsetD}         [| A <= B;  c:A |] ==> c:B

   697 \tdx{subsetCE}        [| A <= B;  ~ (c:A) ==> P;  c:B ==> P |] ==> P

   698

   699 \tdx{subset_refl}     A <= A

   700 \tdx{subset_trans}    [| A<=B;  B<=C |] ==> A<=C

   701

   702 \tdx{equalityI}       [| A <= B;  B <= A |] ==> A = B

   703 \tdx{equalityD1}      A = B ==> A<=B

   704 \tdx{equalityD2}      A = B ==> B<=A

   705 \tdx{equalityE}       [| A = B;  [| A<=B; B<=A |] ==> P |]  ==>  P

   706

   707 \tdx{equalityCE}      [| A = B;  [| c:A; c:B |] ==> P;

   708                            [| ~ c:A; ~ c:B |] ==> P

   709                 |]  ==>  P

   710 \subcaption{The subset and equality relations}

   711 \end{ttbox}

   712 \caption{Derived rules for set theory} \label{hol-set1}

   713 \end{figure}

   714

   715

   716 \begin{figure} \underscoreon

   717 \begin{ttbox}

   718 \tdx{emptyE}   a : {\ttlbrace}{\ttrbrace} ==> P

   719

   720 \tdx{insertI1} a : insert a B

   721 \tdx{insertI2} a : B ==> a : insert b B

   722 \tdx{insertE}  [| a : insert b A;  a=b ==> P;  a:A ==> P |] ==> P

   723

   724 \tdx{ComplI}   [| c:A ==> False |] ==> c : -A

   725 \tdx{ComplD}   [| c : -A |] ==> ~ c:A

   726

   727 \tdx{UnI1}     c:A ==> c : A Un B

   728 \tdx{UnI2}     c:B ==> c : A Un B

   729 \tdx{UnCI}     (~c:B ==> c:A) ==> c : A Un B

   730 \tdx{UnE}      [| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P

   731

   732 \tdx{IntI}     [| c:A;  c:B |] ==> c : A Int B

   733 \tdx{IntD1}    c : A Int B ==> c:A

   734 \tdx{IntD2}    c : A Int B ==> c:B

   735 \tdx{IntE}     [| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P

   736

   737 \tdx{UN_I}     [| a:A;  b: B a |] ==> b: (UN x:A. B x)

   738 \tdx{UN_E}     [| b: (UN x:A. B x);  !!x.[| x:A;  b:B x |] ==> R |] ==> R

   739

   740 \tdx{INT_I}    (!!x. x:A ==> b: B x) ==> b : (INT x:A. B x)

   741 \tdx{INT_D}    [| b: (INT x:A. B x);  a:A |] ==> b: B a

   742 \tdx{INT_E}    [| b: (INT x:A. B x);  b: B a ==> R;  ~ a:A ==> R |] ==> R

   743

   744 \tdx{UnionI}   [| X:C;  A:X |] ==> A : Union C

   745 \tdx{UnionE}   [| A : Union C;  !!X.[| A:X;  X:C |] ==> R |] ==> R

   746

   747 \tdx{InterI}   [| !!X. X:C ==> A:X |] ==> A : Inter C

   748 \tdx{InterD}   [| A : Inter C;  X:C |] ==> A:X

   749 \tdx{InterE}   [| A : Inter C;  A:X ==> R;  ~ X:C ==> R |] ==> R

   750

   751 \tdx{PowI}     A<=B ==> A: Pow B

   752 \tdx{PowD}     A: Pow B ==> A<=B

   753

   754 \tdx{imageI}   [| x:A |] ==> f x : fA

   755 \tdx{imageE}   [| b : fA;  !!x.[| b=f x;  x:A |] ==> P |] ==> P

   756

   757 \tdx{rangeI}   f x : range f

   758 \tdx{rangeE}   [| b : range f;  !!x.[| b=f x |] ==> P |] ==> P

   759 \end{ttbox}

   760 \caption{Further derived rules for set theory} \label{hol-set2}

   761 \end{figure}

   762

   763

   764 \subsection{Axioms and rules of set theory}

   765 Figure~\ref{hol-set-rules} presents the rules of theory \thydx{Set}.  The

   766 axioms \tdx{mem_Collect_eq} and \tdx{Collect_mem_eq} assert

   767 that the functions \texttt{Collect} and \hbox{\tt op :} are isomorphisms.  Of

   768 course, \hbox{\tt op :} also serves as the membership relation.

   769

   770 All the other axioms are definitions.  They include the empty set, bounded

   771 quantifiers, unions, intersections, complements and the subset relation.

   772 They also include straightforward constructions on functions: image~({\tt})

   773 and \texttt{range}.

   774

   775 %The predicate \cdx{inj_on} is used for simulating type definitions.

   776 %The statement ${\tt inj_on}~f~A$ asserts that $f$ is injective on the

   777 %set~$A$, which specifies a subset of its domain type.  In a type

   778 %definition, $f$ is the abstraction function and $A$ is the set of valid

   779 %representations; we should not expect $f$ to be injective outside of~$A$.

   780

   781 %\begin{figure} \underscoreon

   782 %\begin{ttbox}

   783 %\tdx{Inv_f_f}    inj f ==> Inv f (f x) = x

   784 %\tdx{f_Inv_f}    y : range f ==> f(Inv f y) = y

   785 %

   786 %\tdx{Inv_injective}

   787 %    [| Inv f x=Inv f y; x: range f;  y: range f |] ==> x=y

   788 %

   789 %

   790 %\tdx{monoI}      [| !!A B. A <= B ==> f A <= f B |] ==> mono f

   791 %\tdx{monoD}      [| mono f;  A <= B |] ==> f A <= f B

   792 %

   793 %\tdx{injI}       [| !! x y. f x = f y ==> x=y |] ==> inj f

   794 %\tdx{inj_inverseI}              (!!x. g(f x) = x) ==> inj f

   795 %\tdx{injD}       [| inj f; f x = f y |] ==> x=y

   796 %

   797 %\tdx{inj_onI}  (!!x y. [| f x=f y; x:A; y:A |] ==> x=y) ==> inj_on f A

   798 %\tdx{inj_onD}  [| inj_on f A;  f x=f y;  x:A;  y:A |] ==> x=y

   799 %

   800 %\tdx{inj_on_inverseI}

   801 %    (!!x. x:A ==> g(f x) = x) ==> inj_on f A

   802 %\tdx{inj_on_contraD}

   803 %    [| inj_on f A;  x~=y;  x:A;  y:A |] ==> ~ f x=f y

   804 %\end{ttbox}

   805 %\caption{Derived rules involving functions} \label{hol-fun}

   806 %\end{figure}

   807

   808

   809 \begin{figure} \underscoreon

   810 \begin{ttbox}

   811 \tdx{Union_upper}     B:A ==> B <= Union A

   812 \tdx{Union_least}     [| !!X. X:A ==> X<=C |] ==> Union A <= C

   813

   814 \tdx{Inter_lower}     B:A ==> Inter A <= B

   815 \tdx{Inter_greatest}  [| !!X. X:A ==> C<=X |] ==> C <= Inter A

   816

   817 \tdx{Un_upper1}       A <= A Un B

   818 \tdx{Un_upper2}       B <= A Un B

   819 \tdx{Un_least}        [| A<=C;  B<=C |] ==> A Un B <= C

   820

   821 \tdx{Int_lower1}      A Int B <= A

   822 \tdx{Int_lower2}      A Int B <= B

   823 \tdx{Int_greatest}    [| C<=A;  C<=B |] ==> C <= A Int B

   824 \end{ttbox}

   825 \caption{Derived rules involving subsets} \label{hol-subset}

   826 \end{figure}

   827

   828

   829 \begin{figure} \underscoreon   \hfuzz=4pt%suppress "Overfull \hbox" message

   830 \begin{ttbox}

   831 \tdx{Int_absorb}        A Int A = A

   832 \tdx{Int_commute}       A Int B = B Int A

   833 \tdx{Int_assoc}         (A Int B) Int C  =  A Int (B Int C)

   834 \tdx{Int_Un_distrib}    (A Un B)  Int C  =  (A Int C) Un (B Int C)

   835

   836 \tdx{Un_absorb}         A Un A = A

   837 \tdx{Un_commute}        A Un B = B Un A

   838 \tdx{Un_assoc}          (A Un B)  Un C  =  A Un (B Un C)

   839 \tdx{Un_Int_distrib}    (A Int B) Un C  =  (A Un C) Int (B Un C)

   840

   841 \tdx{Compl_disjoint}    A Int (-A) = {\ttlbrace}x. False{\ttrbrace}

   842 \tdx{Compl_partition}   A Un  (-A) = {\ttlbrace}x. True{\ttrbrace}

   843 \tdx{double_complement} -(-A) = A

   844 \tdx{Compl_Un}          -(A Un B)  = (-A) Int (-B)

   845 \tdx{Compl_Int}         -(A Int B) = (-A) Un (-B)

   846

   847 \tdx{Union_Un_distrib}  Union(A Un B) = (Union A) Un (Union B)

   848 \tdx{Int_Union}         A Int (Union B) = (UN C:B. A Int C)

   849

   850 \tdx{Inter_Un_distrib}  Inter(A Un B) = (Inter A) Int (Inter B)

   851 \tdx{Un_Inter}          A Un (Inter B) = (INT C:B. A Un C)

   852

   853 \end{ttbox}

   854 \caption{Set equalities} \label{hol-equalities}

   855 \end{figure}

   856 %\tdx{Un_Union_image}    (UN x:C.(A x) Un (B x)) = Union(AC) Un Union(BC)

   857 %\tdx{Int_Inter_image}   (INT x:C.(A x) Int (B x)) = Inter(AC) Int Inter(BC)

   858

   859 Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules.  Most are

   860 obvious and resemble rules of Isabelle's ZF set theory.  Certain rules, such

   861 as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI}, are designed for classical

   862 reasoning; the rules \tdx{subsetD}, \tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are

   863 not strictly necessary but yield more natural proofs.  Similarly,

   864 \tdx{equalityCE} supports classical reasoning about extensionality, after the

   865 fashion of \tdx{iffCE}.  See the file \texttt{HOL/Set.ML} for proofs

   866 pertaining to set theory.

   867

   868 Figure~\ref{hol-subset} presents lattice properties of the subset relation.

   869 Unions form least upper bounds; non-empty intersections form greatest lower

   870 bounds.  Reasoning directly about subsets often yields clearer proofs than

   871 reasoning about the membership relation.  See the file \texttt{HOL/subset.ML}.

   872

   873 Figure~\ref{hol-equalities} presents many common set equalities.  They

   874 include commutative, associative and distributive laws involving unions,

   875 intersections and complements.  For a complete listing see the file {\tt

   876 HOL/equalities.ML}.

   877

   878 \begin{warn}

   879 \texttt{Blast_tac} proves many set-theoretic theorems automatically.

   880 Hence you seldom need to refer to the theorems above.

   881 \end{warn}

   882

   883 \begin{figure}

   884 \begin{center}

   885 \begin{tabular}{rrr}

   886   \it name      &\it meta-type  & \it description \\

   887   \cdx{inj}~~\cdx{surj}& $(\alpha\To\beta )\To bool$

   888         & injective/surjective \\

   889   \cdx{inj_on}        & $[\alpha\To\beta ,\alpha\,set]\To bool$

   890         & injective over subset\\

   891   \cdx{inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & inverse function

   892 \end{tabular}

   893 \end{center}

   894

   895 \underscoreon

   896 \begin{ttbox}

   897 \tdx{inj_def}         inj f      == ! x y. f x=f y --> x=y

   898 \tdx{surj_def}        surj f     == ! y. ? x. y=f x

   899 \tdx{inj_on_def}      inj_on f A == !x:A. !y:A. f x=f y --> x=y

   900 \tdx{inv_def}         inv f      == (\%y. @x. f(x)=y)

   901 \end{ttbox}

   902 \caption{Theory \thydx{Fun}} \label{fig:HOL:Fun}

   903 \end{figure}

   904

   905 \subsection{Properties of functions}\nopagebreak

   906 Figure~\ref{fig:HOL:Fun} presents a theory of simple properties of functions.

   907 Note that ${\tt inv}~f$ uses Hilbert's $\varepsilon$ to yield an inverse

   908 of~$f$.  See the file \texttt{HOL/Fun.ML} for a complete listing of the derived

   909 rules.  Reasoning about function composition (the operator~\sdx{o}) and the

   910 predicate~\cdx{surj} is done simply by expanding the definitions.

   911

   912 There is also a large collection of monotonicity theorems for constructions

   913 on sets in the file \texttt{HOL/mono.ML}.

   914

   915

   916 \section{Generic packages}

   917 \label{sec:HOL:generic-packages}

   918

   919 HOL instantiates most of Isabelle's generic packages, making available the

   920 simplifier and the classical reasoner.

   921

   922 \subsection{Simplification and substitution}

   923

   924 Simplification tactics tactics such as \texttt{Asm_simp_tac} and \texttt{Full_simp_tac} use the default simpset

   925 (\texttt{simpset()}), which works for most purposes.  A quite minimal

   926 simplification set for higher-order logic is~\ttindexbold{HOL_ss};

   927 even more frugal is \ttindexbold{HOL_basic_ss}.  Equality~($=$), which

   928 also expresses logical equivalence, may be used for rewriting.  See

   929 the file \texttt{HOL/simpdata.ML} for a complete listing of the basic

   930 simplification rules.

   931

   932 See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%

   933 {Chaps.\ts\ref{substitution} and~\ref{simp-chap}} for details of substitution

   934 and simplification.

   935

   936 \begin{warn}\index{simplification!of conjunctions}%

   937   Reducing $a=b\conj P(a)$ to $a=b\conj P(b)$ is sometimes advantageous.  The

   938   left part of a conjunction helps in simplifying the right part.  This effect

   939   is not available by default: it can be slow.  It can be obtained by

   940   including \ttindex{conj_cong} in a simpset, \verb$addcongs [conj_cong]$.

   941 \end{warn}

   942

   943 \begin{warn}\index{simplification!of \texttt{if}}\label{if-simp}%

   944   By default only the condition of an \ttindex{if} is simplified but not the

   945   \texttt{then} and \texttt{else} parts. Of course the latter are simplified

   946   once the condition simplifies to \texttt{True} or \texttt{False}. To ensure

   947   full simplification of all parts of a conditional you must remove

   948   \ttindex{if_weak_cong} from the simpset, \verb$delcongs [if_weak_cong]$.

   949 \end{warn}

   950

   951 If the simplifier cannot use a certain rewrite rule --- either because

   952 of nontermination or because its left-hand side is too flexible ---

   953 then you might try \texttt{stac}:

   954 \begin{ttdescription}

   955 \item[\ttindexbold{stac} $thm$ $i,$] where $thm$ is of the form $lhs = rhs$,

   956   replaces in subgoal $i$ instances of $lhs$ by corresponding instances of

   957   $rhs$.  In case of multiple instances of $lhs$ in subgoal $i$, backtracking

   958   may be necessary to select the desired ones.

   959

   960 If $thm$ is a conditional equality, the instantiated condition becomes an

   961 additional (first) subgoal.

   962 \end{ttdescription}

   963

   964 HOL provides the tactic \ttindex{hyp_subst_tac}, which substitutes for an

   965 equality throughout a subgoal and its hypotheses.  This tactic uses HOL's

   966 general substitution rule.

   967

   968 \subsubsection{Case splitting}

   969 \label{subsec:HOL:case:splitting}

   970

   971 HOL also provides convenient means for case splitting during rewriting. Goals

   972 containing a subterm of the form \texttt{if}~$b$~{\tt then\dots else\dots}

   973 often require a case distinction on $b$. This is expressed by the theorem

   974 \tdx{split_if}:

   975 $$  976 \Var{P}(\mbox{\tt if}~\Var{b}~{\tt then}~\Var{x}~\mbox{\tt else}~\Var{y})~=~   977 ((\Var{b} \to \Var{P}(\Var{x})) \land (\lnot \Var{b} \to \Var{P}(\Var{y})))   978 \eqno{(*)}   979$$

   980 For example, a simple instance of $(*)$ is

   981 $  982 x \in (\mbox{\tt if}~x \in A~{\tt then}~A~\mbox{\tt else}~\{x\})~=~   983 ((x \in A \to x \in A) \land (x \notin A \to x \in \{x\}))   984$

   985 Because $(*)$ is too general as a rewrite rule for the simplifier (the

   986 left-hand side is not a higher-order pattern in the sense of

   987 \iflabelundefined{chap:simplification}{the {\em Reference Manual\/}}%

   988 {Chap.\ts\ref{chap:simplification}}), there is a special infix function

   989 \ttindexbold{addsplits} of type \texttt{simpset * thm list -> simpset}

   990 (analogous to \texttt{addsimps}) that adds rules such as $(*)$ to a

   991 simpset, as in

   992 \begin{ttbox}

   993 by(simp_tac (simpset() addsplits [split_if]) 1);

   994 \end{ttbox}

   995 The effect is that after each round of simplification, one occurrence of

   996 \texttt{if} is split acording to \texttt{split_if}, until all occurences of

   997 \texttt{if} have been eliminated.

   998

   999 It turns out that using \texttt{split_if} is almost always the right thing to

  1000 do. Hence \texttt{split_if} is already included in the default simpset. If

  1001 you want to delete it from a simpset, use \ttindexbold{delsplits}, which is

  1002 the inverse of \texttt{addsplits}:

  1003 \begin{ttbox}

  1004 by(simp_tac (simpset() delsplits [split_if]) 1);

  1005 \end{ttbox}

  1006

  1007 In general, \texttt{addsplits} accepts rules of the form

  1008 $  1009 \Var{P}(c~\Var{x@1}~\dots~\Var{x@n})~=~ rhs   1010$

  1011 where $c$ is a constant and $rhs$ is arbitrary. Note that $(*)$ is of the

  1012 right form because internally the left-hand side is

  1013 $\Var{P}(\mathtt{If}~\Var{b}~\Var{x}~~\Var{y})$. Important further examples

  1014 are splitting rules for \texttt{case} expressions (see~{\S}\ref{subsec:list}

  1015 and~{\S}\ref{subsec:datatype:basics}).

  1016

  1017 Analogous to \texttt{Addsimps} and \texttt{Delsimps}, there are also

  1018 imperative versions of \texttt{addsplits} and \texttt{delsplits}

  1019 \begin{ttbox}

  1020 \ttindexbold{Addsplits}: thm list -> unit

  1021 \ttindexbold{Delsplits}: thm list -> unit

  1022 \end{ttbox}

  1023 for adding splitting rules to, and deleting them from the current simpset.

  1024

  1025 \subsection{Classical reasoning}

  1026

  1027 HOL derives classical introduction rules for $\disj$ and~$\exists$, as well as

  1028 classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule; recall

  1029 Fig.\ts\ref{hol-lemmas2} above.

  1030

  1031 The classical reasoner is installed.  Tactics such as \texttt{Blast_tac} and

  1032 {\tt Best_tac} refer to the default claset (\texttt{claset()}), which works

  1033 for most purposes.  Named clasets include \ttindexbold{prop_cs}, which

  1034 includes the propositional rules, and \ttindexbold{HOL_cs}, which also

  1035 includes quantifier rules.  See the file \texttt{HOL/cladata.ML} for lists of

  1036 the classical rules,

  1037 and \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%

  1038 {Chap.\ts\ref{chap:classical}} for more discussion of classical proof methods.

  1039

  1040

  1041 %FIXME outdated, both from the Isabelle and SVC perspective

  1042 % \section{Calling the decision procedure SVC}\label{sec:HOL:SVC}

  1043

  1044 % \index{SVC decision procedure|(}

  1045

  1046 % The Stanford Validity Checker (SVC) is a tool that can check the validity of

  1047 % certain types of formulae.  If it is installed on your machine, then

  1048 % Isabelle/HOL can be configured to call it through the tactic

  1049 % \ttindex{svc_tac}.  It is ideal for large tautologies and complex problems in

  1050 % linear arithmetic.  Subexpressions that SVC cannot handle are automatically

  1051 % replaced by variables, so you can call the tactic on any subgoal.  See the

  1052 % file \texttt{HOL/ex/svc_test.ML} for examples.

  1053 % \begin{ttbox}

  1054 % svc_tac   : int -> tactic

  1055 % Svc.trace : bool ref      \hfill{\bf initially false}

  1056 % \end{ttbox}

  1057

  1058 % \begin{ttdescription}

  1059 % \item[\ttindexbold{svc_tac} $i$] attempts to prove subgoal~$i$ by translating

  1060 %   it into a formula recognized by~SVC\@.  If it succeeds then the subgoal is

  1061 %   removed.  It fails if SVC is unable to prove the subgoal.  It crashes with

  1062 %   an error message if SVC appears not to be installed.  Numeric variables may

  1063 %   have types \texttt{nat}, \texttt{int} or \texttt{real}.

  1064

  1065 % \item[\ttindexbold{Svc.trace}] is a flag that, if set, causes \texttt{svc_tac}

  1066 %   to trace its operations: abstraction of the subgoal, translation to SVC

  1067 %   syntax, SVC's response.

  1068 % \end{ttdescription}

  1069

  1070 % Here is an example, with tracing turned on:

  1071 % \begin{ttbox}

  1072 % set Svc.trace;

  1073 % {\out val it : bool = true}

  1074 % Goal "(#3::nat)*a <= #2 + #4*b + #6*c  & #11 <= #2*a + b + #2*c & \ttback

  1075 % \ttback     a + #3*b <= #5 + #2*c  --> #2 + #3*b <= #2*a + #6*c";

  1076

  1077 % by (svc_tac 1);

  1078 % {\out Subgoal abstracted to}

  1079 % {\out #3 * a <= #2 + #4 * b + #6 * c &}

  1080 % {\out #11 <= #2 * a + b + #2 * c & a + #3 * b <= #5 + #2 * c -->}

  1081 % {\out #2 + #3 * b <= #2 * a + #6 * c}

  1082 % {\out Calling SVC:}

  1083 % {\out (=> (<= 0  (F_c) )  (=> (<= 0  (F_b) )  (=> (<= 0  (F_a) )}

  1084 % {\out   (=> (AND (<= {* 3  (F_a) }  {+ {+ 2  {* 4  (F_b) } }  }

  1085 % {\out {* 6  (F_c) } } )  (AND (<= 11  {+ {+ {* 2  (F_a) }  (F_b) }}

  1086 % {\out   {* 2  (F_c) } } )  (<= {+ (F_a)  {* 3  (F_b) } }  {+ 5  }

  1087 % {\out {* 2  (F_c) } } ) ) )  (< {+ 2  {* 3  (F_b) } }  {+ 1  {+ }

  1088 % {\out {* 2  (F_a) }  {* 6  (F_c) } } } ) ) ) ) ) }

  1089 % {\out SVC Returns:}

  1090 % {\out VALID}

  1091 % {\out Level 1}

  1092 % {\out #3 * a <= #2 + #4 * b + #6 * c &}

  1093 % {\out #11 <= #2 * a + b + #2 * c & a + #3 * b <= #5 + #2 * c -->}

  1094 % {\out #2 + #3 * b <= #2 * a + #6 * c}

  1095 % {\out No subgoals!}

  1096 % \end{ttbox}

  1097

  1098

  1099 % \begin{warn}

  1100 % Calling \ttindex{svc_tac} entails an above-average risk of

  1101 % unsoundness.  Isabelle does not check SVC's result independently.  Moreover,

  1102 % the tactic translates the submitted formula using code that lies outside

  1103 % Isabelle's inference core.  Theorems that depend upon results proved using SVC

  1104 % (and other oracles) are displayed with the annotation \texttt{[!]} attached.

  1105 % You can also use \texttt{\#der (rep_thm $th$)} to examine the proof object of

  1106 % theorem~$th$, as described in the \emph{Reference Manual}.

  1107 % \end{warn}

  1108

  1109 % To start, first download SVC from the Internet at URL

  1110 % \begin{ttbox}

  1111 % http://agamemnon.stanford.edu/~levitt/vc/index.html

  1112 % \end{ttbox}

  1113 % and install it using the instructions supplied.  SVC requires two environment

  1114 % variables:

  1115 % \begin{ttdescription}

  1116 % \item[\ttindexbold{SVC_HOME}] is an absolute pathname to the SVC

  1117 %     distribution directory.

  1118

  1119 %   \item[\ttindexbold{SVC_MACHINE}] identifies the type of computer and

  1120 %     operating system.

  1121 % \end{ttdescription}

  1122 % You can set these environment variables either using the Unix shell or through

  1123 % an Isabelle \texttt{settings} file.  Isabelle assumes SVC to be installed if

  1124 % \texttt{SVC_HOME} is defined.

  1125

  1126 % \paragraph*{Acknowledgement.}  This interface uses code supplied by S{\o}ren

  1127 % Heilmann.

  1128

  1129

  1130 % \index{SVC decision procedure|)}

  1131

  1132

  1133

  1134

  1135 \section{Types}\label{sec:HOL:Types}

  1136 This section describes HOL's basic predefined types ($\alpha \times \beta$,

  1137 $\alpha + \beta$, $nat$ and $\alpha \; list$) and ways for introducing new

  1138 types in general.  The most important type construction, the

  1139 \texttt{datatype}, is treated separately in {\S}\ref{sec:HOL:datatype}.

  1140

  1141

  1142 \subsection{Product and sum types}\index{*"* type}\index{*"+ type}

  1143 \label{subsec:prod-sum}

  1144

  1145 \begin{figure}[htbp]

  1146 \begin{constants}

  1147   \it symbol    & \it meta-type &           & \it description \\

  1148   \cdx{Pair}    & $[\alpha,\beta]\To \alpha\times\beta$

  1149         & & ordered pairs $(a,b)$ \\

  1150   \cdx{fst}     & $\alpha\times\beta \To \alpha$        & & first projection\\

  1151   \cdx{snd}     & $\alpha\times\beta \To \beta$         & & second projection\\

  1152   \cdx{split}   & $[[\alpha,\beta]\To\gamma, \alpha\times\beta] \To \gamma$

  1153         & & generalized projection\\

  1154   \cdx{Sigma}  &

  1155         $[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ &

  1156         & general sum of sets

  1157 \end{constants}

  1158 %\tdx{fst_def}      fst p     == @a. ? b. p = (a,b)

  1159 %\tdx{snd_def}      snd p     == @b. ? a. p = (a,b)

  1160 %\tdx{split_def}    split c p == c (fst p) (snd p)

  1161 \begin{ttbox}\makeatletter

  1162 \tdx{Sigma_def}    Sigma A B == UN x:A. UN y:B x. {\ttlbrace}(x,y){\ttrbrace}

  1163

  1164 \tdx{Pair_eq}      ((a,b) = (a',b')) = (a=a' & b=b')

  1165 \tdx{Pair_inject}  [| (a, b) = (a',b');  [| a=a';  b=b' |] ==> R |] ==> R

  1166 \tdx{PairE}        [| !!x y. p = (x,y) ==> Q |] ==> Q

  1167

  1168 \tdx{fst_conv}     fst (a,b) = a

  1169 \tdx{snd_conv}     snd (a,b) = b

  1170 \tdx{surjective_pairing}  p = (fst p,snd p)

  1171

  1172 \tdx{split}        split c (a,b) = c a b

  1173 \tdx{split_split}  R(split c p) = (! x y. p = (x,y) --> R(c x y))

  1174

  1175 \tdx{SigmaI}    [| a:A;  b:B a |] ==> (a,b) : Sigma A B

  1176

  1177 \tdx{SigmaE}    [| c:Sigma A B; !!x y.[| x:A; y:B x; c=(x,y) |] ==> P

  1178           |] ==> P

  1179 \end{ttbox}

  1180 \caption{Type $\alpha\times\beta$}\label{hol-prod}

  1181 \end{figure}

  1182

  1183 Theory \thydx{Prod} (Fig.\ts\ref{hol-prod}) defines the product type

  1184 $\alpha\times\beta$, with the ordered pair syntax $(a, b)$.  General

  1185 tuples are simulated by pairs nested to the right:

  1186 \begin{center}

  1187 \begin{tabular}{c|c}

  1188 external & internal \\

  1189 \hline

  1190 $\tau@1 \times \dots \times \tau@n$ & $\tau@1 \times (\dots (\tau@{n-1} \times \tau@n)\dots)$ \\

  1191 \hline

  1192 $(t@1,\dots,t@n)$ & $(t@1,(\dots,(t@{n-1},t@n)\dots)$ \\

  1193 \end{tabular}

  1194 \end{center}

  1195 In addition, it is possible to use tuples

  1196 as patterns in abstractions:

  1197 \begin{center}

  1198 {\tt\%($x$,$y$). $t$} \quad stands for\quad \texttt{split(\%$x$\thinspace$y$.\ $t$)}

  1199 \end{center}

  1200 Nested patterns are also supported.  They are translated stepwise:

  1201 \begin{eqnarray*}

  1202 \hbox{\tt\%($x$,$y$,$z$).\ $t$}

  1203    & \leadsto & \hbox{\tt\%($x$,($y$,$z$)).\ $t$} \\

  1204    & \leadsto & \hbox{\tt split(\%$x$.\%($y$,$z$).\ $t$)}\\

  1205    & \leadsto & \hbox{\tt split(\%$x$.\ split(\%$y$ $z$.\ $t$))}

  1206 \end{eqnarray*}

  1207 The reverse translation is performed upon printing.

  1208 \begin{warn}

  1209   The translation between patterns and \texttt{split} is performed automatically

  1210   by the parser and printer.  Thus the internal and external form of a term

  1211   may differ, which can affects proofs.  For example the term {\tt

  1212   (\%(x,y).(y,x))(a,b)} requires the theorem \texttt{split} (which is in the

  1213   default simpset) to rewrite to {\tt(b,a)}.

  1214 \end{warn}

  1215 In addition to explicit $\lambda$-abstractions, patterns can be used in any

  1216 variable binding construct which is internally described by a

  1217 $\lambda$-abstraction.  Some important examples are

  1218 \begin{description}

  1219 \item[Let:] \texttt{let {\it pattern} = $t$ in $u$}

  1220 \item[Quantifiers:] \texttt{ALL~{\it pattern}:$A$.~$P$}

  1221 \item[Choice:] {\underscoreon \tt SOME~{\it pattern}.~$P$}

  1222 \item[Set operations:] \texttt{UN~{\it pattern}:$A$.~$B$}

  1223 \item[Sets:] \texttt{{\ttlbrace}{\it pattern}.~$P${\ttrbrace}}

  1224 \end{description}

  1225

  1226 There is a simple tactic which supports reasoning about patterns:

  1227 \begin{ttdescription}

  1228 \item[\ttindexbold{split_all_tac} $i$] replaces in subgoal $i$ all

  1229   {\tt!!}-quantified variables of product type by individual variables for

  1230   each component.  A simple example:

  1231 \begin{ttbox}

  1232 {\out 1. !!p. (\%(x,y,z). (x, y, z)) p = p}

  1233 by(split_all_tac 1);

  1234 {\out 1. !!x xa ya. (\%(x,y,z). (x, y, z)) (x, xa, ya) = (x, xa, ya)}

  1235 \end{ttbox}

  1236 \end{ttdescription}

  1237

  1238 Theory \texttt{Prod} also introduces the degenerate product type \texttt{unit}

  1239 which contains only a single element named {\tt()} with the property

  1240 \begin{ttbox}

  1241 \tdx{unit_eq}       u = ()

  1242 \end{ttbox}

  1243 \bigskip

  1244

  1245 Theory \thydx{Sum} (Fig.~\ref{hol-sum}) defines the sum type $\alpha+\beta$

  1246 which associates to the right and has a lower priority than $*$: $\tau@1 +   1247 \tau@2 + \tau@3*\tau@4$ means $\tau@1 + (\tau@2 + (\tau@3*\tau@4))$.

  1248

  1249 The definition of products and sums in terms of existing types is not

  1250 shown.  The constructions are fairly standard and can be found in the

  1251 respective theory files. Although the sum and product types are

  1252 constructed manually for foundational reasons, they are represented as

  1253 actual datatypes later (see {\S}\ref{subsec:datatype:rep_datatype}).

  1254 Therefore, the theory \texttt{Datatype} should be used instead of

  1255 \texttt{Sum} or \texttt{Prod}.

  1256

  1257 \begin{figure}

  1258 \begin{constants}

  1259   \it symbol    & \it meta-type &           & \it description \\

  1260   \cdx{Inl}     & $\alpha \To \alpha+\beta$    & & first injection\\

  1261   \cdx{Inr}     & $\beta \To \alpha+\beta$     & & second injection\\

  1262   \cdx{sum_case} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$

  1263         & & conditional

  1264 \end{constants}

  1265 \begin{ttbox}\makeatletter

  1266 \tdx{Inl_not_Inr}    Inl a ~= Inr b

  1267

  1268 \tdx{inj_Inl}        inj Inl

  1269 \tdx{inj_Inr}        inj Inr

  1270

  1271 \tdx{sumE}           [| !!x. P(Inl x);  !!y. P(Inr y) |] ==> P s

  1272

  1273 \tdx{sum_case_Inl}   sum_case f g (Inl x) = f x

  1274 \tdx{sum_case_Inr}   sum_case f g (Inr x) = g x

  1275

  1276 \tdx{surjective_sum} sum_case (\%x. f(Inl x)) (\%y. f(Inr y)) s = f s

  1277 \tdx{sum.split_case} R(sum_case f g s) = ((! x. s = Inl(x) --> R(f(x))) &

  1278                                      (! y. s = Inr(y) --> R(g(y))))

  1279 \end{ttbox}

  1280 \caption{Type $\alpha+\beta$}\label{hol-sum}

  1281 \end{figure}

  1282

  1283 \begin{figure}

  1284 \index{*"< symbol}

  1285 \index{*"* symbol}

  1286 \index{*div symbol}

  1287 \index{*mod symbol}

  1288 \index{*dvd symbol}

  1289 \index{*"+ symbol}

  1290 \index{*"- symbol}

  1291 \begin{constants}

  1292   \it symbol    & \it meta-type & \it priority & \it description \\

  1293   \cdx{0}       & $\alpha$  & & zero \\

  1294   \cdx{Suc}     & $nat \To nat$ & & successor function\\

  1295   \tt *    & $[\alpha,\alpha]\To \alpha$    &  Left 70 & multiplication \\

  1296   \tt div  & $[\alpha,\alpha]\To \alpha$    &  Left 70 & division\\

  1297   \tt mod  & $[\alpha,\alpha]\To \alpha$    &  Left 70 & modulus\\

  1298   \tt dvd  & $[\alpha,\alpha]\To bool$     &  Left 70 & divides'' relation\\

  1299   \tt +    & $[\alpha,\alpha]\To \alpha$    &  Left 65 & addition\\

  1300   \tt -    & $[\alpha,\alpha]\To \alpha$    &  Left 65 & subtraction

  1301 \end{constants}

  1302 \subcaption{Constants and infixes}

  1303

  1304 \begin{ttbox}\makeatother

  1305 \tdx{nat_induct}     [| P 0; !!n. P n ==> P(Suc n) |]  ==> P n

  1306

  1307 \tdx{Suc_not_Zero}   Suc m ~= 0

  1308 \tdx{inj_Suc}        inj Suc

  1309 \tdx{n_not_Suc_n}    n~=Suc n

  1310 \subcaption{Basic properties}

  1311 \end{ttbox}

  1312 \caption{The type of natural numbers, \tydx{nat}} \label{hol-nat1}

  1313 \end{figure}

  1314

  1315

  1316 \begin{figure}

  1317 \begin{ttbox}\makeatother

  1318               0+n           = n

  1319               (Suc m)+n     = Suc(m+n)

  1320

  1321               m-0           = m

  1322               0-n           = n

  1323               Suc(m)-Suc(n) = m-n

  1324

  1325               0*n           = 0

  1326               Suc(m)*n      = n + m*n

  1327

  1328 \tdx{mod_less}      m<n ==> m mod n = m

  1329 \tdx{mod_geq}       [| 0<n;  ~m<n |] ==> m mod n = (m-n) mod n

  1330

  1331 \tdx{div_less}      m<n ==> m div n = 0

  1332 \tdx{div_geq}       [| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)

  1333 \end{ttbox}

  1334 \caption{Recursion equations for the arithmetic operators} \label{hol-nat2}

  1335 \end{figure}

  1336

  1337 \subsection{The type of natural numbers, \textit{nat}}

  1338 \index{nat@{\textit{nat}} type|(}

  1339

  1340 The theory \thydx{Nat} defines the natural numbers in a roundabout but

  1341 traditional way.  The axiom of infinity postulates a type~\tydx{ind} of

  1342 individuals, which is non-empty and closed under an injective operation.  The

  1343 natural numbers are inductively generated by choosing an arbitrary individual

  1344 for~0 and using the injective operation to take successors.  This is a least

  1345 fixedpoint construction.

  1346

  1347 Type~\tydx{nat} is an instance of class~\cldx{ord}, which makes the overloaded

  1348 functions of this class (especially \cdx{<} and \cdx{<=}, but also \cdx{min},

  1349 \cdx{max} and \cdx{LEAST}) available on \tydx{nat}.  Theory \thydx{Nat}

  1350 also shows that {\tt<=} is a linear order, so \tydx{nat} is

  1351 also an instance of class \cldx{linorder}.

  1352

  1353 Theory \thydx{NatArith} develops arithmetic on the natural numbers.  It defines

  1354 addition, multiplication and subtraction.  Theory \thydx{Divides} defines

  1355 division, remainder and the divides'' relation.  The numerous theorems

  1356 proved include commutative, associative, distributive, identity and

  1357 cancellation laws.  See Figs.\ts\ref{hol-nat1} and~\ref{hol-nat2}.  The

  1358 recursion equations for the operators \texttt{+}, \texttt{-} and \texttt{*} on

  1359 \texttt{nat} are part of the default simpset.

  1360

  1361 Functions on \tydx{nat} can be defined by primitive or well-founded recursion;

  1362 see {\S}\ref{sec:HOL:recursive}.  A simple example is addition.

  1363 Here, \texttt{op +} is the name of the infix operator~\texttt{+}, following

  1364 the standard convention.

  1365 \begin{ttbox}

  1366 \sdx{primrec}

  1367       "0 + n = n"

  1368   "Suc m + n = Suc (m + n)"

  1369 \end{ttbox}

  1370 There is also a \sdx{case}-construct

  1371 of the form

  1372 \begin{ttbox}

  1373 case $$e$$ of 0 => $$a$$ | Suc $$m$$ => $$b$$

  1374 \end{ttbox}

  1375 Note that Isabelle insists on precisely this format; you may not even change

  1376 the order of the two cases.

  1377 Both \texttt{primrec} and \texttt{case} are realized by a recursion operator

  1378 \cdx{nat_rec}, which is available because \textit{nat} is represented as

  1379 a datatype (see {\S}\ref{subsec:datatype:rep_datatype}).

  1380

  1381 %The predecessor relation, \cdx{pred_nat}, is shown to be well-founded.

  1382 %Recursion along this relation resembles primitive recursion, but is

  1383 %stronger because we are in higher-order logic; using primitive recursion to

  1384 %define a higher-order function, we can easily Ackermann's function, which

  1385 %is not primitive recursive \cite[page~104]{thompson91}.

  1386 %The transitive closure of \cdx{pred_nat} is~$<$.  Many functions on the

  1387 %natural numbers are most easily expressed using recursion along~$<$.

  1388

  1389 Tactic {\tt\ttindex{induct_tac} "$n$" $i$} performs induction on variable~$n$

  1390 in subgoal~$i$ using theorem \texttt{nat_induct}.  There is also the derived

  1391 theorem \tdx{less_induct}:

  1392 \begin{ttbox}

  1393 [| !!n. [| ! m. m<n --> P m |] ==> P n |]  ==>  P n

  1394 \end{ttbox}

  1395

  1396

  1397 \subsection{Numerical types and numerical reasoning}

  1398

  1399 The integers (type \tdx{int}) are also available in HOL, and the reals (type

  1400 \tdx{real}) are available in the logic image \texttt{HOL-Complex}.  They support

  1401 the expected operations of addition (\texttt{+}), subtraction (\texttt{-}) and

  1402 multiplication (\texttt{*}), and much else.  Type \tdx{int} provides the

  1403 \texttt{div} and \texttt{mod} operators, while type \tdx{real} provides real

  1404 division and other operations.  Both types belong to class \cldx{linorder}, so

  1405 they inherit the relational operators and all the usual properties of linear

  1406 orderings.  For full details, please survey the theories in subdirectories

  1407 \texttt{Integ}, \texttt{Real}, and \texttt{Complex}.

  1408

  1409 All three numeric types admit numerals of the form \texttt{$sd\ldots d$},

  1410 where $s$ is an optional minus sign and $d\ldots d$ is a string of digits.

  1411 Numerals are represented internally by a datatype for binary notation, which

  1412 allows numerical calculations to be performed by rewriting.  For example, the

  1413 integer division of \texttt{54342339} by \texttt{3452} takes about five

  1414 seconds.  By default, the simplifier cancels like terms on the opposite sites

  1415 of relational operators (reducing \texttt{z+x<x+y} to \texttt{z<y}, for

  1416 instance.  The simplifier also collects like terms, replacing \texttt{x+y+x*3}

  1417 by \texttt{4*x+y}.

  1418

  1419 Sometimes numerals are not wanted, because for example \texttt{n+3} does not

  1420 match a pattern of the form \texttt{Suc $k$}.  You can re-arrange the form of

  1421 an arithmetic expression by proving (via \texttt{subgoal_tac}) a lemma such as

  1422 \texttt{n+3 = Suc (Suc (Suc n))}.  As an alternative, you can disable the

  1423 fancier simplifications by using a basic simpset such as \texttt{HOL_ss}

  1424 rather than the default one, \texttt{simpset()}.

  1425

  1426 Reasoning about arithmetic inequalities can be tedious.  Fortunately, HOL

  1427 provides a decision procedure for \emph{linear arithmetic}: formulae involving

  1428 addition and subtraction. The simplifier invokes a weak version of this

  1429 decision procedure automatically. If this is not sufficent, you can invoke the

  1430 full procedure \ttindex{Lin_Arith.tac} explicitly.  It copes with arbitrary

  1431 formulae involving {\tt=}, {\tt<}, {\tt<=}, {\tt+}, {\tt-}, {\tt Suc}, {\tt

  1432   min}, {\tt max} and numerical constants. Other subterms are treated as

  1433 atomic, while subformulae not involving numerical types are ignored. Quantified

  1434 subformulae are ignored unless they are positive universal or negative

  1435 existential. The running time is exponential in the number of

  1436 occurrences of {\tt min}, {\tt max}, and {\tt-} because they require case

  1437 distinctions.

  1438 If {\tt k} is a numeral, then {\tt div k}, {\tt mod k} and

  1439 {\tt k dvd} are also supported. The former two are eliminated

  1440 by case distinctions, again blowing up the running time.

  1441 If the formula involves explicit quantifiers, \texttt{Lin_Arith.tac} may take

  1442 super-exponential time and space.

  1443

  1444 If \texttt{Lin_Arith.tac} fails, try to find relevant arithmetic results in

  1445 the library.  The theories \texttt{Nat} and \texttt{NatArith} contain

  1446 theorems about {\tt<}, {\tt<=}, \texttt{+}, \texttt{-} and \texttt{*}.

  1447 Theory \texttt{Divides} contains theorems about \texttt{div} and

  1448 \texttt{mod}.  Use Proof General's \emph{find} button (or other search

  1449 facilities) to locate them.

  1450

  1451 \index{nat@{\textit{nat}} type|)}

  1452

  1453

  1454 \begin{figure}

  1455 \index{#@{\tt[]} symbol}

  1456 \index{#@{\tt\#} symbol}

  1457 \index{"@@{\tt\at} symbol}

  1458 \index{*"! symbol}

  1459 \begin{constants}

  1460   \it symbol & \it meta-type & \it priority & \it description \\

  1461   \tt[]    & $\alpha\,list$ & & empty list\\

  1462   \tt \#   & $[\alpha,\alpha\,list]\To \alpha\,list$ & Right 65 &

  1463         list constructor \\

  1464   \cdx{null}    & $\alpha\,list \To bool$ & & emptiness test\\

  1465   \cdx{hd}      & $\alpha\,list \To \alpha$ & & head \\

  1466   \cdx{tl}      & $\alpha\,list \To \alpha\,list$ & & tail \\

  1467   \cdx{last}    & $\alpha\,list \To \alpha$ & & last element \\

  1468   \cdx{butlast} & $\alpha\,list \To \alpha\,list$ & & drop last element \\

  1469   \tt\at  & $[\alpha\,list,\alpha\,list]\To \alpha\,list$ & Left 65 & append \\

  1470   \cdx{map}     & $(\alpha\To\beta) \To (\alpha\,list \To \beta\,list)$

  1471         & & apply to all\\

  1472   \cdx{filter}  & $(\alpha \To bool) \To (\alpha\,list \To \alpha\,list)$

  1473         & & filter functional\\

  1474   \cdx{set}& $\alpha\,list \To \alpha\,set$ & & elements\\

  1475   \sdx{mem}  & $\alpha \To \alpha\,list \To bool$  &  Left 55   & membership\\

  1476   \cdx{foldl}   & $(\beta\To\alpha\To\beta) \To \beta \To \alpha\,list \To \beta$ &

  1477   & iteration \\

  1478   \cdx{concat}   & $(\alpha\,list)list\To \alpha\,list$ & & concatenation \\

  1479   \cdx{rev}     & $\alpha\,list \To \alpha\,list$ & & reverse \\

  1480   \cdx{length}  & $\alpha\,list \To nat$ & & length \\

  1481   \tt! & $\alpha\,list \To nat \To \alpha$ & Left 100 & indexing \\

  1482   \cdx{take}, \cdx{drop} & $nat \To \alpha\,list \To \alpha\,list$ &&

  1483     take/drop a prefix \\

  1484   \cdx{takeWhile},\\

  1485   \cdx{dropWhile} &

  1486     $(\alpha \To bool) \To \alpha\,list \To \alpha\,list$ &&

  1487     take/drop a prefix

  1488 \end{constants}

  1489 \subcaption{Constants and infixes}

  1490

  1491 \begin{center} \tt\frenchspacing

  1492 \begin{tabular}{rrr}

  1493   \it external        & \it internal  & \it description \\{}

  1494   [$x@1$, $\dots$, $x@n$]  &  $x@1$ \# $\cdots$ \# $x@n$ \# [] &

  1495         \rm finite list \\{}

  1496   [$x$:$l$. $P$]  & filter ($\lambda x{.}P$) $l$ &

  1497         \rm list comprehension

  1498 \end{tabular}

  1499 \end{center}

  1500 \subcaption{Translations}

  1501 \caption{The theory \thydx{List}} \label{hol-list}

  1502 \end{figure}

  1503

  1504

  1505 \begin{figure}

  1506 \begin{ttbox}\makeatother

  1507 null [] = True

  1508 null (x#xs) = False

  1509

  1510 hd (x#xs) = x

  1511

  1512 tl (x#xs) = xs

  1513 tl [] = []

  1514

  1515 [] @ ys = ys

  1516 (x#xs) @ ys = x # xs @ ys

  1517

  1518 set [] = \ttlbrace\ttrbrace

  1519 set (x#xs) = insert x (set xs)

  1520

  1521 x mem [] = False

  1522 x mem (y#ys) = (if y=x then True else x mem ys)

  1523

  1524 concat([]) = []

  1525 concat(x#xs) = x @ concat(xs)

  1526

  1527 rev([]) = []

  1528 rev(x#xs) = rev(xs) @ [x]

  1529

  1530 length([]) = 0

  1531 length(x#xs) = Suc(length(xs))

  1532

  1533 xs!0 = hd xs

  1534 xs!(Suc n) = (tl xs)!n

  1535 \end{ttbox}

  1536 \caption{Simple list processing functions}

  1537 \label{fig:HOL:list-simps}

  1538 \end{figure}

  1539

  1540 \begin{figure}

  1541 \begin{ttbox}\makeatother

  1542 map f [] = []

  1543 map f (x#xs) = f x # map f xs

  1544

  1545 filter P [] = []

  1546 filter P (x#xs) = (if P x then x#filter P xs else filter P xs)

  1547

  1548 foldl f a [] = a

  1549 foldl f a (x#xs) = foldl f (f a x) xs

  1550

  1551 take n [] = []

  1552 take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)

  1553

  1554 drop n [] = []

  1555 drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)

  1556

  1557 takeWhile P [] = []

  1558 takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])

  1559

  1560 dropWhile P [] = []

  1561 dropWhile P (x#xs) = (if P x then dropWhile P xs else xs)

  1562 \end{ttbox}

  1563 \caption{Further list processing functions}

  1564 \label{fig:HOL:list-simps2}

  1565 \end{figure}

  1566

  1567

  1568 \subsection{The type constructor for lists, \textit{list}}

  1569 \label{subsec:list}

  1570 \index{list@{\textit{list}} type|(}

  1571

  1572 Figure~\ref{hol-list} presents the theory \thydx{List}: the basic list

  1573 operations with their types and syntax.  Type $\alpha \; list$ is

  1574 defined as a \texttt{datatype} with the constructors {\tt[]} and {\tt\#}.

  1575 As a result the generic structural induction and case analysis tactics

  1576 \texttt{induct\_tac} and \texttt{cases\_tac} also become available for

  1577 lists.  A \sdx{case} construct of the form

  1578 \begin{center}\tt

  1579 case $e$ of [] => $a$  |  $$x$$\#$$xs$$ => b

  1580 \end{center}

  1581 is defined by translation.  For details see~{\S}\ref{sec:HOL:datatype}. There

  1582 is also a case splitting rule \tdx{split_list_case}

  1583 $  1584 \begin{array}{l}   1585 P(\mathtt{case}~e~\mathtt{of}~\texttt{[] =>}~a ~\texttt{|}~   1586 x\texttt{\#}xs~\texttt{=>}~f~x~xs) ~= \\   1587 ((e = \texttt{[]} \to P(a)) \land   1588 (\forall x~ xs. e = x\texttt{\#}xs \to P(f~x~xs)))   1589 \end{array}   1590$

  1591 which can be fed to \ttindex{addsplits} just like

  1592 \texttt{split_if} (see~{\S}\ref{subsec:HOL:case:splitting}).

  1593

  1594 \texttt{List} provides a basic library of list processing functions defined by

  1595 primitive recursion (see~{\S}\ref{sec:HOL:primrec}).  The recursion equations

  1596 are shown in Figs.\ts\ref{fig:HOL:list-simps} and~\ref{fig:HOL:list-simps2}.

  1597

  1598 \index{list@{\textit{list}} type|)}

  1599

  1600

  1601 \subsection{Introducing new types} \label{sec:typedef}

  1602

  1603 The HOL-methodology dictates that all extensions to a theory should be

  1604 \textbf{definitional}.  The type definition mechanism that meets this

  1605 criterion is \ttindex{typedef}.  Note that \emph{type synonyms}, which are

  1606 inherited from Pure and described elsewhere, are just syntactic abbreviations

  1607 that have no logical meaning.

  1608

  1609 \begin{warn}

  1610   Types in HOL must be non-empty; otherwise the quantifier rules would be

  1611   unsound, because $\exists x. x=x$ is a theorem \cite[{\S}7]{paulson-COLOG}.

  1612 \end{warn}

  1613 A \bfindex{type definition} identifies the new type with a subset of

  1614 an existing type.  More precisely, the new type is defined by

  1615 exhibiting an existing type~$\tau$, a set~$A::\tau\,set$, and a

  1616 theorem of the form $x:A$.  Thus~$A$ is a non-empty subset of~$\tau$,

  1617 and the new type denotes this subset.  New functions are defined that

  1618 establish an isomorphism between the new type and the subset.  If

  1619 type~$\tau$ involves type variables $\alpha@1$, \ldots, $\alpha@n$,

  1620 then the type definition creates a type constructor

  1621 $(\alpha@1,\ldots,\alpha@n)ty$ rather than a particular type.

  1622

  1623 \begin{figure}[htbp]

  1624 \begin{rail}

  1625 typedef  : 'typedef' ( () | '(' name ')') type '=' set witness;

  1626

  1627 type    : typevarlist name ( () | '(' infix ')' );

  1628 set     : string;

  1629 witness : () | '(' id ')';

  1630 \end{rail}

  1631 \caption{Syntax of type definitions}

  1632 \label{fig:HOL:typedef}

  1633 \end{figure}

  1634

  1635 The syntax for type definitions is shown in Fig.~\ref{fig:HOL:typedef}.  For

  1636 the definition of typevarlist' and infix' see

  1637 \iflabelundefined{chap:classical}

  1638 {the appendix of the {\em Reference Manual\/}}%

  1639 {Appendix~\ref{app:TheorySyntax}}.  The remaining nonterminals have the

  1640 following meaning:

  1641 \begin{description}

  1642 \item[\it type:] the new type constructor $(\alpha@1,\dots,\alpha@n)ty$ with

  1643   optional infix annotation.

  1644 \item[\it name:] an alphanumeric name $T$ for the type constructor

  1645   $ty$, in case $ty$ is a symbolic name.  Defaults to $ty$.

  1646 \item[\it set:] the representing subset $A$.

  1647 \item[\it witness:] name of a theorem of the form $a:A$ proving

  1648   non-emptiness.  It can be omitted in case Isabelle manages to prove

  1649   non-emptiness automatically.

  1650 \end{description}

  1651 If all context conditions are met (no duplicate type variables in

  1652 typevarlist', no extra type variables in set', and no free term variables

  1653 in set'), the following components are added to the theory:

  1654 \begin{itemize}

  1655 \item a type $ty :: (term,\dots,term)term$

  1656 \item constants

  1657 \begin{eqnarray*}

  1658 T &::& \tau\;set \\

  1659 Rep_T &::& (\alpha@1,\dots,\alpha@n)ty \To \tau \\

  1660 Abs_T &::& \tau \To (\alpha@1,\dots,\alpha@n)ty

  1661 \end{eqnarray*}

  1662 \item a definition and three axioms

  1663 $  1664 \begin{array}{ll}   1665 T{\tt_def} & T \equiv A \\   1666 {\tt Rep_}T & Rep_T\,x \in T \\   1667 {\tt Rep_}T{\tt_inverse} & Abs_T\,(Rep_T\,x) = x \\   1668 {\tt Abs_}T{\tt_inverse} & y \in T \Imp Rep_T\,(Abs_T\,y) = y   1669 \end{array}   1670$

  1671 stating that $(\alpha@1,\dots,\alpha@n)ty$ is isomorphic to $A$ by $Rep_T$

  1672 and its inverse $Abs_T$.

  1673 \end{itemize}

  1674 Below are two simple examples of HOL type definitions.  Non-emptiness is

  1675 proved automatically here.

  1676 \begin{ttbox}

  1677 typedef unit = "{\ttlbrace}True{\ttrbrace}"

  1678

  1679 typedef (prod)

  1680   ('a, 'b) "*"    (infixr 20)

  1681       = "{\ttlbrace}f . EX (a::'a) (b::'b). f = (\%x y. x = a & y = b){\ttrbrace}"

  1682 \end{ttbox}

  1683

  1684 Type definitions permit the introduction of abstract data types in a safe

  1685 way, namely by providing models based on already existing types.  Given some

  1686 abstract axiomatic description $P$ of a type, this involves two steps:

  1687 \begin{enumerate}

  1688 \item Find an appropriate type $\tau$ and subset $A$ which has the desired

  1689   properties $P$, and make a type definition based on this representation.

  1690 \item Prove that $P$ holds for $ty$ by lifting $P$ from the representation.

  1691 \end{enumerate}

  1692 You can now forget about the representation and work solely in terms of the

  1693 abstract properties $P$.

  1694

  1695 \begin{warn}

  1696 If you introduce a new type (constructor) $ty$ axiomatically, i.e.\ by

  1697 declaring the type and its operations and by stating the desired axioms, you

  1698 should make sure the type has a non-empty model.  You must also have a clause

  1699 \par

  1700 \begin{ttbox}

  1701 arities $$ty$$ :: (term,\thinspace$$\dots$$,{\thinspace}term){\thinspace}term

  1702 \end{ttbox}

  1703 in your theory file to tell Isabelle that $ty$ is in class \texttt{term}, the

  1704 class of all HOL types.

  1705 \end{warn}

  1706

  1707

  1708 \section{Datatype definitions}

  1709 \label{sec:HOL:datatype}

  1710 \index{*datatype|(}

  1711

  1712 Inductive datatypes, similar to those of \ML, frequently appear in

  1713 applications of Isabelle/HOL.  In principle, such types could be defined by

  1714 hand via \texttt{typedef} (see {\S}\ref{sec:typedef}), but this would be far too

  1715 tedious.  The \ttindex{datatype} definition package of Isabelle/HOL (cf.\

  1716 \cite{Berghofer-Wenzel:1999:TPHOL}) automates such chores.  It generates an

  1717 appropriate \texttt{typedef} based on a least fixed-point construction, and

  1718 proves freeness theorems and induction rules, as well as theorems for

  1719 recursion and case combinators.  The user just has to give a simple

  1720 specification of new inductive types using a notation similar to {\ML} or

  1721 Haskell.

  1722

  1723 The current datatype package can handle both mutual and indirect recursion.

  1724 It also offers to represent existing types as datatypes giving the advantage

  1725 of a more uniform view on standard theories.

  1726

  1727

  1728 \subsection{Basics}

  1729 \label{subsec:datatype:basics}

  1730

  1731 A general \texttt{datatype} definition is of the following form:

  1732 $  1733 \begin{array}{llcl}   1734 \mathtt{datatype} & (\vec{\alpha})t@1 & = &   1735 C^1@1~\tau^1@{1,1}~\ldots~\tau^1@{1,m^1@1} ~\mid~ \ldots ~\mid~   1736 C^1@{k@1}~\tau^1@{k@1,1}~\ldots~\tau^1@{k@1,m^1@{k@1}} \\   1737 & & \vdots \\   1738 \mathtt{and} & (\vec{\alpha})t@n & = &   1739 C^n@1~\tau^n@{1,1}~\ldots~\tau^n@{1,m^n@1} ~\mid~ \ldots ~\mid~   1740 C^n@{k@n}~\tau^n@{k@n,1}~\ldots~\tau^n@{k@n,m^n@{k@n}}   1741 \end{array}   1742$

  1743 where $\vec{\alpha} = (\alpha@1,\ldots,\alpha@h)$ is a list of type variables,

  1744 $C^j@i$ are distinct constructor names and $\tau^j@{i,i'}$ are {\em

  1745   admissible} types containing at most the type variables $\alpha@1, \ldots,   1746 \alpha@h$. A type $\tau$ occurring in a \texttt{datatype} definition is {\em

  1747   admissible} if and only if

  1748 \begin{itemize}

  1749 \item $\tau$ is non-recursive, i.e.\ $\tau$ does not contain any of the

  1750 newly defined type constructors $t@1,\ldots,t@n$, or

  1751 \item $\tau = (\vec{\alpha})t@{j'}$ where $1 \leq j' \leq n$, or

  1752 \item $\tau = (\tau'@1,\ldots,\tau'@{h'})t'$, where $t'$ is

  1753 the type constructor of an already existing datatype and $\tau'@1,\ldots,\tau'@{h'}$

  1754 are admissible types.

  1755 \item $\tau = \sigma \to \tau'$, where $\tau'$ is an admissible

  1756 type and $\sigma$ is non-recursive (i.e. the occurrences of the newly defined

  1757 types are {\em strictly positive})

  1758 \end{itemize}

  1759 If some $(\vec{\alpha})t@{j'}$ occurs in a type $\tau^j@{i,i'}$

  1760 of the form

  1761 $  1762 (\ldots,\ldots ~ (\vec{\alpha})t@{j'} ~ \ldots,\ldots)t'   1763$

  1764 this is called a {\em nested} (or \emph{indirect}) occurrence. A very simple

  1765 example of a datatype is the type \texttt{list}, which can be defined by

  1766 \begin{ttbox}

  1767 datatype 'a list = Nil

  1768                  | Cons 'a ('a list)

  1769 \end{ttbox}

  1770 Arithmetic expressions \texttt{aexp} and boolean expressions \texttt{bexp} can be modelled

  1771 by the mutually recursive datatype definition

  1772 \begin{ttbox}

  1773 datatype 'a aexp = If_then_else ('a bexp) ('a aexp) ('a aexp)

  1774                  | Sum ('a aexp) ('a aexp)

  1775                  | Diff ('a aexp) ('a aexp)

  1776                  | Var 'a

  1777                  | Num nat

  1778 and      'a bexp = Less ('a aexp) ('a aexp)

  1779                  | And ('a bexp) ('a bexp)

  1780                  | Or ('a bexp) ('a bexp)

  1781 \end{ttbox}

  1782 The datatype \texttt{term}, which is defined by

  1783 \begin{ttbox}

  1784 datatype ('a, 'b) term = Var 'a

  1785                        | App 'b ((('a, 'b) term) list)

  1786 \end{ttbox}

  1787 is an example for a datatype with nested recursion. Using nested recursion

  1788 involving function spaces, we may also define infinitely branching datatypes, e.g.

  1789 \begin{ttbox}

  1790 datatype 'a tree = Atom 'a | Branch "nat => 'a tree"

  1791 \end{ttbox}

  1792

  1793 \medskip

  1794

  1795 Types in HOL must be non-empty. Each of the new datatypes

  1796 $(\vec{\alpha})t@j$ with $1 \leq j \leq n$ is non-empty if and only if it has a

  1797 constructor $C^j@i$ with the following property: for all argument types

  1798 $\tau^j@{i,i'}$ of the form $(\vec{\alpha})t@{j'}$ the datatype

  1799 $(\vec{\alpha})t@{j'}$ is non-empty.

  1800

  1801 If there are no nested occurrences of the newly defined datatypes, obviously

  1802 at least one of the newly defined datatypes $(\vec{\alpha})t@j$

  1803 must have a constructor $C^j@i$ without recursive arguments, a \emph{base

  1804   case}, to ensure that the new types are non-empty. If there are nested

  1805 occurrences, a datatype can even be non-empty without having a base case

  1806 itself. Since \texttt{list} is a non-empty datatype, \texttt{datatype t = C (t

  1807   list)} is non-empty as well.

  1808

  1809

  1810 \subsubsection{Freeness of the constructors}

  1811

  1812 The datatype constructors are automatically defined as functions of their

  1813 respective type:

  1814 $C^j@i :: [\tau^j@{i,1},\dots,\tau^j@{i,m^j@i}] \To (\alpha@1,\dots,\alpha@h)t@j$

  1815 These functions have certain {\em freeness} properties.  They construct

  1816 distinct values:

  1817 $  1818 C^j@i~x@1~\dots~x@{m^j@i} \neq C^j@{i'}~y@1~\dots~y@{m^j@{i'}} \qquad   1819 \mbox{for all}~ i \neq i'.   1820$

  1821 The constructor functions are injective:

  1822 $  1823 (C^j@i~x@1~\dots~x@{m^j@i} = C^j@i~y@1~\dots~y@{m^j@i}) =   1824 (x@1 = y@1 \land \dots \land x@{m^j@i} = y@{m^j@i})   1825$

  1826 Since the number of distinctness inequalities is quadratic in the number of

  1827 constructors, the datatype package avoids proving them separately if there are

  1828 too many constructors. Instead, specific inequalities are proved by a suitable

  1829 simplification procedure on demand.\footnote{This procedure, which is already part

  1830 of the default simpset, may be referred to by the ML identifier

  1831 \texttt{DatatypePackage.distinct_simproc}.}

  1832

  1833 \subsubsection{Structural induction}

  1834

  1835 The datatype package also provides structural induction rules.  For

  1836 datatypes without nested recursion, this is of the following form:

  1837 $  1838 \infer{P@1~x@1 \land \dots \land P@n~x@n}   1839 {\begin{array}{lcl}   1840 \Forall x@1 \dots x@{m^1@1}.   1841 \List{P@{s^1@{1,1}}~x@{r^1@{1,1}}; \dots;   1842 P@{s^1@{1,l^1@1}}~x@{r^1@{1,l^1@1}}} & \Imp &   1843 P@1~\left(C^1@1~x@1~\dots~x@{m^1@1}\right) \\   1844 & \vdots \\   1845 \Forall x@1 \dots x@{m^1@{k@1}}.   1846 \List{P@{s^1@{k@1,1}}~x@{r^1@{k@1,1}}; \dots;   1847 P@{s^1@{k@1,l^1@{k@1}}}~x@{r^1@{k@1,l^1@{k@1}}}} & \Imp &   1848 P@1~\left(C^1@{k@1}~x@1~\ldots~x@{m^1@{k@1}}\right) \\   1849 & \vdots \\   1850 \Forall x@1 \dots x@{m^n@1}.   1851 \List{P@{s^n@{1,1}}~x@{r^n@{1,1}}; \dots;   1852 P@{s^n@{1,l^n@1}}~x@{r^n@{1,l^n@1}}} & \Imp &   1853 P@n~\left(C^n@1~x@1~\ldots~x@{m^n@1}\right) \\   1854 & \vdots \\   1855 \Forall x@1 \dots x@{m^n@{k@n}}.   1856 \List{P@{s^n@{k@n,1}}~x@{r^n@{k@n,1}}; \dots   1857 P@{s^n@{k@n,l^n@{k@n}}}~x@{r^n@{k@n,l^n@{k@n}}}} & \Imp &   1858 P@n~\left(C^n@{k@n}~x@1~\ldots~x@{m^n@{k@n}}\right)   1859 \end{array}}   1860$

  1861 where

  1862 $  1863 \begin{array}{rcl}   1864 Rec^j@i & := &   1865 \left\{\left(r^j@{i,1},s^j@{i,1}\right),\ldots,   1866 \left(r^j@{i,l^j@i},s^j@{i,l^j@i}\right)\right\} = \\[2ex]   1867 && \left\{(i',i'')~\left|~   1868 1\leq i' \leq m^j@i \land 1 \leq i'' \leq n \land   1869 \tau^j@{i,i'} = (\alpha@1,\ldots,\alpha@h)t@{i''}\right.\right\}   1870 \end{array}   1871$

  1872 i.e.\ the properties $P@j$ can be assumed for all recursive arguments.

  1873

  1874 For datatypes with nested recursion, such as the \texttt{term} example from

  1875 above, things are a bit more complicated.  Conceptually, Isabelle/HOL unfolds

  1876 a definition like

  1877 \begin{ttbox}

  1878 datatype ('a,'b) term = Var 'a

  1879                       | App 'b ((('a, 'b) term) list)

  1880 \end{ttbox}

  1881 to an equivalent definition without nesting:

  1882 \begin{ttbox}

  1883 datatype ('a,'b) term      = Var

  1884                            | App 'b (('a, 'b) term_list)

  1885 and      ('a,'b) term_list = Nil'

  1886                            | Cons' (('a,'b) term) (('a,'b) term_list)

  1887 \end{ttbox}

  1888 Note however, that the type \texttt{('a,'b) term_list} and the constructors {\tt

  1889   Nil'} and \texttt{Cons'} are not really introduced.  One can directly work with

  1890 the original (isomorphic) type \texttt{(('a, 'b) term) list} and its existing

  1891 constructors \texttt{Nil} and \texttt{Cons}. Thus, the structural induction rule for

  1892 \texttt{term} gets the form

  1893 $  1894 \infer{P@1~x@1 \land P@2~x@2}   1895 {\begin{array}{l}   1896 \Forall x.~P@1~(\mathtt{Var}~x) \\   1897 \Forall x@1~x@2.~P@2~x@2 \Imp P@1~(\mathtt{App}~x@1~x@2) \\   1898 P@2~\mathtt{Nil} \\   1899 \Forall x@1~x@2. \List{P@1~x@1; P@2~x@2} \Imp P@2~(\mathtt{Cons}~x@1~x@2)   1900 \end{array}}   1901$

  1902 Note that there are two predicates $P@1$ and $P@2$, one for the type \texttt{('a,'b) term}

  1903 and one for the type \texttt{(('a, 'b) term) list}.

  1904

  1905 For a datatype with function types such as \texttt{'a tree}, the induction rule

  1906 is of the form

  1907 $  1908 \infer{P~t}   1909 {\Forall a.~P~(\mathtt{Atom}~a) &   1910 \Forall ts.~(\forall x.~P~(ts~x)) \Imp P~(\mathtt{Branch}~ts)}   1911$

  1912

  1913 \medskip In principle, inductive types are already fully determined by

  1914 freeness and structural induction.  For convenience in applications,

  1915 the following derived constructions are automatically provided for any

  1916 datatype.

  1917

  1918 \subsubsection{The \sdx{case} construct}

  1919

  1920 The type comes with an \ML-like \texttt{case}-construct:

  1921 $  1922 \begin{array}{rrcl}   1923 \mbox{\tt case}~e~\mbox{\tt of} & C^j@1~x@{1,1}~\dots~x@{1,m^j@1} & \To & e@1 \\   1924 \vdots \\   1925 \mid & C^j@{k@j}~x@{k@j,1}~\dots~x@{k@j,m^j@{k@j}} & \To & e@{k@j}   1926 \end{array}   1927$

  1928 where the $x@{i,j}$ are either identifiers or nested tuple patterns as in

  1929 {\S}\ref{subsec:prod-sum}.

  1930 \begin{warn}

  1931   All constructors must be present, their order is fixed, and nested patterns

  1932   are not supported (with the exception of tuples).  Violating this

  1933   restriction results in strange error messages.

  1934 \end{warn}

  1935

  1936 To perform case distinction on a goal containing a \texttt{case}-construct,

  1937 the theorem $t@j.$\texttt{split} is provided:

  1938 $  1939 \begin{array}{@{}rcl@{}}   1940 P(t@j_\mathtt{case}~f@1~\dots~f@{k@j}~e) &\!\!\!=&   1941 \!\!\! ((\forall x@1 \dots x@{m^j@1}. e = C^j@1~x@1\dots x@{m^j@1} \to   1942 P(f@1~x@1\dots x@{m^j@1})) \\   1943 &&\!\!\! ~\land~ \dots ~\land \\   1944 &&~\!\!\! (\forall x@1 \dots x@{m^j@{k@j}}. e = C^j@{k@j}~x@1\dots x@{m^j@{k@j}} \to   1945 P(f@{k@j}~x@1\dots x@{m^j@{k@j}})))   1946 \end{array}   1947$

  1948 where $t@j$\texttt{_case} is the internal name of the \texttt{case}-construct.

  1949 This theorem can be added to a simpset via \ttindex{addsplits}

  1950 (see~{\S}\ref{subsec:HOL:case:splitting}).

  1951

  1952 Case splitting on assumption works as well, by using the rule

  1953 $t@j.$\texttt{split_asm} in the same manner.  Both rules are available under

  1954 $t@j.$\texttt{splits} (this name is \emph{not} bound in ML, though).

  1955

  1956 \begin{warn}\index{simplification!of \texttt{case}}%

  1957   By default only the selector expression ($e$ above) in a

  1958   \texttt{case}-construct is simplified, in analogy with \texttt{if} (see

  1959   page~\pageref{if-simp}). Only if that reduces to a constructor is one of

  1960   the arms of the \texttt{case}-construct exposed and simplified. To ensure

  1961   full simplification of all parts of a \texttt{case}-construct for datatype

  1962   $t$, remove $t$\texttt{.}\ttindexbold{case_weak_cong} from the simpset, for

  1963   example by \texttt{delcongs [thm "$t$.weak_case_cong"]}.

  1964 \end{warn}

  1965

  1966 \subsubsection{The function \cdx{size}}\label{sec:HOL:size}

  1967

  1968 Theory \texttt{NatArith} declares a generic function \texttt{size} of type

  1969 $\alpha\To nat$.  Each datatype defines a particular instance of \texttt{size}

  1970 by overloading according to the following scheme:

  1971 %%% FIXME: This formula is too big and is completely unreadable

  1972 $  1973 size(C^j@i~x@1~\dots~x@{m^j@i}) = \!   1974 \left\{   1975 \begin{array}{ll}   1976 0 & \!\mbox{if Rec^j@i = \emptyset} \\   1977 1+\sum\limits@{h=1}^{l^j@i}size~x@{r^j@{i,h}} &   1978 \!\mbox{if Rec^j@i = \left\{\left(r^j@{i,1},s^j@{i,1}\right),\ldots,   1979 \left(r^j@{i,l^j@i},s^j@{i,l^j@i}\right)\right\}}   1980 \end{array}   1981 \right.   1982$

  1983 where $Rec^j@i$ is defined above.  Viewing datatypes as generalised trees, the

  1984 size of a leaf is 0 and the size of a node is the sum of the sizes of its

  1985 subtrees ${}+1$.

  1986

  1987 \subsection{Defining datatypes}

  1988

  1989 The theory syntax for datatype definitions is shown in

  1990 Fig.~\ref{datatype-grammar}.  In order to be well-formed, a datatype

  1991 definition has to obey the rules stated in the previous section.  As a result

  1992 the theory is extended with the new types, the constructors, and the theorems

  1993 listed in the previous section.

  1994

  1995 \begin{figure}

  1996 \begin{rail}

  1997 datatype : 'datatype' typedecls;

  1998

  1999 typedecls: ( newtype '=' (cons + '|') ) + 'and'

  2000          ;

  2001 newtype  : typevarlist id ( () | '(' infix ')' )

  2002          ;

  2003 cons     : name (argtype *) ( () | ( '(' mixfix ')' ) )

  2004          ;

  2005 argtype  : id | tid | ('(' typevarlist id ')')

  2006          ;

  2007 \end{rail}

  2008 \caption{Syntax of datatype declarations}

  2009 \label{datatype-grammar}

  2010 \end{figure}

  2011

  2012 Most of the theorems about datatypes become part of the default simpset and

  2013 you never need to see them again because the simplifier applies them

  2014 automatically.  Only induction or case distinction are usually invoked by hand.

  2015 \begin{ttdescription}

  2016 \item[\ttindexbold{induct_tac} {\tt"}$x${\tt"} $i$]

  2017  applies structural induction on variable $x$ to subgoal $i$, provided the

  2018  type of $x$ is a datatype.

  2019 \item[\texttt{induct_tac}

  2020   {\tt"}$x@1$ $\ldots$ $x@n${\tt"} $i$] applies simultaneous

  2021   structural induction on the variables $x@1,\ldots,x@n$ to subgoal $i$.  This

  2022   is the canonical way to prove properties of mutually recursive datatypes

  2023   such as \texttt{aexp} and \texttt{bexp}, or datatypes with nested recursion such as

  2024   \texttt{term}.

  2025 \end{ttdescription}

  2026 In some cases, induction is overkill and a case distinction over all

  2027 constructors of the datatype suffices.

  2028 \begin{ttdescription}

  2029 \item[\ttindexbold{case_tac} {\tt"}$u${\tt"} $i$]

  2030  performs a case analysis for the term $u$ whose type  must be a datatype.

  2031  If the datatype has $k@j$ constructors  $C^j@1$, \dots $C^j@{k@j}$, subgoal

  2032  $i$ is replaced by $k@j$ new subgoals which  contain the additional

  2033  assumption $u = C^j@{i'}~x@1~\dots~x@{m^j@{i'}}$ for  $i'=1$, $\dots$,~$k@j$.

  2034 \end{ttdescription}

  2035

  2036 Note that induction is only allowed on free variables that should not occur

  2037 among the premises of the subgoal. Case distinction applies to arbitrary terms.

  2038

  2039 \bigskip

  2040

  2041

  2042 For the technically minded, we exhibit some more details.  Processing the

  2043 theory file produces an \ML\ structure which, in addition to the usual

  2044 components, contains a structure named $t$ for each datatype $t$ defined in

  2045 the file.  Each structure $t$ contains the following elements:

  2046 \begin{ttbox}

  2047 val distinct : thm list

  2048 val inject : thm list

  2049 val induct : thm

  2050 val exhaust : thm

  2051 val cases : thm list

  2052 val split : thm

  2053 val split_asm : thm

  2054 val recs : thm list

  2055 val size : thm list

  2056 val simps : thm list

  2057 \end{ttbox}

  2058 \texttt{distinct}, \texttt{inject}, \texttt{induct}, \texttt{size}

  2059 and \texttt{split} contain the theorems

  2060 described above.  For user convenience, \texttt{distinct} contains

  2061 inequalities in both directions.  The reduction rules of the {\tt

  2062   case}-construct are in \texttt{cases}.  All theorems from {\tt

  2063   distinct}, \texttt{inject} and \texttt{cases} are combined in \texttt{simps}.

  2064 In case of mutually recursive datatypes, \texttt{recs}, \texttt{size}, \texttt{induct}

  2065 and \texttt{simps} are contained in a separate structure named $t@1_\ldots_t@n$.

  2066

  2067

  2068 \subsection{Representing existing types as datatypes}\label{subsec:datatype:rep_datatype}

  2069

  2070 For foundational reasons, some basic types such as \texttt{nat}, \texttt{*}, {\tt

  2071   +}, \texttt{bool} and \texttt{unit} are not defined in a \texttt{datatype} section,

  2072 but by more primitive means using \texttt{typedef}. To be able to use the

  2073 tactics \texttt{induct_tac} and \texttt{case_tac} and to define functions by

  2074 primitive recursion on these types, such types may be represented as actual

  2075 datatypes.  This is done by specifying the constructors of the desired type,

  2076 plus a proof of the  induction rule, as well as theorems

  2077 stating the distinctness and injectivity of constructors in a {\tt

  2078 rep_datatype} section.  For the sum type this works as follows:

  2079 \begin{ttbox}

  2080 rep_datatype (sum) Inl Inr

  2081 proof -

  2082   fix P

  2083   fix s :: "'a + 'b"

  2084   assume x: "!!x::'a. P (Inl x)" and y: "!!y::'b. P (Inr y)"

  2085   then show "P s" by (auto intro: sumE [of s])

  2086 qed simp_all

  2087 \end{ttbox}

  2088 The datatype package automatically derives additional theorems for recursion

  2089 and case combinators from these rules.  Any of the basic HOL types mentioned

  2090 above are represented as datatypes.  Try an induction on \texttt{bool}

  2091 today.

  2092

  2093

  2094 \subsection{Examples}

  2095

  2096 \subsubsection{The datatype $\alpha~mylist$}

  2097

  2098 We want to define a type $\alpha~mylist$. To do this we have to build a new

  2099 theory that contains the type definition.  We start from the theory

  2100 \texttt{Datatype} instead of \texttt{Main} in order to avoid clashes with the

  2101 \texttt{List} theory of Isabelle/HOL.

  2102 \begin{ttbox}

  2103 MyList = Datatype +

  2104   datatype 'a mylist = Nil | Cons 'a ('a mylist)

  2105 end

  2106 \end{ttbox}

  2107 After loading the theory, we can prove $Cons~x~xs\neq xs$, for example.  To

  2108 ease the induction applied below, we state the goal with $x$ quantified at the

  2109 object-level.  This will be stripped later using \ttindex{qed_spec_mp}.

  2110 \begin{ttbox}

  2111 Goal "!x. Cons x xs ~= xs";

  2112 {\out Level 0}

  2113 {\out ! x. Cons x xs ~= xs}

  2114 {\out  1. ! x. Cons x xs ~= xs}

  2115 \end{ttbox}

  2116 This can be proved by the structural induction tactic:

  2117 \begin{ttbox}

  2118 by (induct_tac "xs" 1);

  2119 {\out Level 1}

  2120 {\out ! x. Cons x xs ~= xs}

  2121 {\out  1. ! x. Cons x Nil ~= Nil}

  2122 {\out  2. !!a mylist.}

  2123 {\out        ! x. Cons x mylist ~= mylist ==>}

  2124 {\out        ! x. Cons x (Cons a mylist) ~= Cons a mylist}

  2125 \end{ttbox}

  2126 The first subgoal can be proved using the simplifier.  Isabelle/HOL has

  2127 already added the freeness properties of lists to the default simplification

  2128 set.

  2129 \begin{ttbox}

  2130 by (Simp_tac 1);

  2131 {\out Level 2}

  2132 {\out ! x. Cons x xs ~= xs}

  2133 {\out  1. !!a mylist.}

  2134 {\out        ! x. Cons x mylist ~= mylist ==>}

  2135 {\out        ! x. Cons x (Cons a mylist) ~= Cons a mylist}

  2136 \end{ttbox}

  2137 Similarly, we prove the remaining goal.

  2138 \begin{ttbox}

  2139 by (Asm_simp_tac 1);

  2140 {\out Level 3}

  2141 {\out ! x. Cons x xs ~= xs}

  2142 {\out No subgoals!}

  2143 \ttbreak

  2144 qed_spec_mp "not_Cons_self";

  2145 {\out val not_Cons_self = "Cons x xs ~= xs" : thm}

  2146 \end{ttbox}

  2147 Because both subgoals could have been proved by \texttt{Asm_simp_tac}

  2148 we could have done that in one step:

  2149 \begin{ttbox}

  2150 by (ALLGOALS Asm_simp_tac);

  2151 \end{ttbox}

  2152

  2153

  2154 \subsubsection{The datatype $\alpha~mylist$ with mixfix syntax}

  2155

  2156 In this example we define the type $\alpha~mylist$ again but this time

  2157 we want to write \texttt{[]} for \texttt{Nil} and we want to use infix

  2158 notation \verb|#| for \texttt{Cons}.  To do this we simply add mixfix

  2159 annotations after the constructor declarations as follows:

  2160 \begin{ttbox}

  2161 MyList = Datatype +

  2162   datatype 'a mylist =

  2163     Nil ("[]")  |

  2164     Cons 'a ('a mylist)  (infixr "#" 70)

  2165 end

  2166 \end{ttbox}

  2167 Now the theorem in the previous example can be written \verb|x#xs ~= xs|.

  2168

  2169

  2170 \subsubsection{A datatype for weekdays}

  2171

  2172 This example shows a datatype that consists of 7 constructors:

  2173 \begin{ttbox}

  2174 Days = Main +

  2175   datatype days = Mon | Tue | Wed | Thu | Fri | Sat | Sun

  2176 end

  2177 \end{ttbox}

  2178 Because there are more than 6 constructors, inequality is expressed via a function

  2179 \verb|days_ord|.  The theorem \verb|Mon ~= Tue| is not directly

  2180 contained among the distinctness theorems, but the simplifier can

  2181 prove it thanks to rewrite rules inherited from theory \texttt{NatArith}:

  2182 \begin{ttbox}

  2183 Goal "Mon ~= Tue";

  2184 by (Simp_tac 1);

  2185 \end{ttbox}

  2186 You need not derive such inequalities explicitly: the simplifier will dispose

  2187 of them automatically.

  2188 \index{*datatype|)}

  2189

  2190

  2191 \section{Recursive function definitions}\label{sec:HOL:recursive}

  2192 \index{recursive functions|see{recursion}}

  2193

  2194 Isabelle/HOL provides two main mechanisms of defining recursive functions.

  2195 \begin{enumerate}

  2196 \item \textbf{Primitive recursion} is available only for datatypes, and it is

  2197   somewhat restrictive.  Recursive calls are only allowed on the argument's

  2198   immediate constituents.  On the other hand, it is the form of recursion most

  2199   often wanted, and it is easy to use.

  2200

  2201 \item \textbf{Well-founded recursion} requires that you supply a well-founded

  2202   relation that governs the recursion.  Recursive calls are only allowed if

  2203   they make the argument decrease under the relation.  Complicated recursion

  2204   forms, such as nested recursion, can be dealt with.  Termination can even be

  2205   proved at a later time, though having unsolved termination conditions around

  2206   can make work difficult.%

  2207   \footnote{This facility is based on Konrad Slind's TFL

  2208     package~\cite{slind-tfl}.  Thanks are due to Konrad for implementing TFL

  2209     and assisting with its installation.}

  2210 \end{enumerate}

  2211

  2212 Following good HOL tradition, these declarations do not assert arbitrary

  2213 axioms.  Instead, they define the function using a recursion operator.  Both

  2214 HOL and ZF derive the theory of well-founded recursion from first

  2215 principles~\cite{paulson-set-II}.  Primitive recursion over some datatype

  2216 relies on the recursion operator provided by the datatype package.  With

  2217 either form of function definition, Isabelle proves the desired recursion

  2218 equations as theorems.

  2219

  2220

  2221 \subsection{Primitive recursive functions}

  2222 \label{sec:HOL:primrec}

  2223 \index{recursion!primitive|(}

  2224 \index{*primrec|(}

  2225

  2226 Datatypes come with a uniform way of defining functions, {\bf primitive

  2227   recursion}.  In principle, one could introduce primitive recursive functions

  2228 by asserting their reduction rules as new axioms, but this is not recommended:

  2229 \begin{ttbox}\slshape

  2230 Append = Main +

  2231 consts app :: ['a list, 'a list] => 'a list

  2232 rules

  2233    app_Nil   "app [] ys = ys"

  2234    app_Cons  "app (x#xs) ys = x#app xs ys"

  2235 end

  2236 \end{ttbox}

  2237 Asserting axioms brings the danger of accidentally asserting nonsense, as

  2238 in \verb$app [] ys = us$.

  2239

  2240 The \ttindex{primrec} declaration is a safe means of defining primitive

  2241 recursive functions on datatypes:

  2242 \begin{ttbox}

  2243 Append = Main +

  2244 consts app :: ['a list, 'a list] => 'a list

  2245 primrec

  2246    "app [] ys = ys"

  2247    "app (x#xs) ys = x#app xs ys"

  2248 end

  2249 \end{ttbox}

  2250 Isabelle will now check that the two rules do indeed form a primitive

  2251 recursive definition.  For example

  2252 \begin{ttbox}

  2253 primrec

  2254     "app [] ys = us"

  2255 \end{ttbox}

  2256 is rejected with an error message \texttt{Extra variables on rhs}''.

  2257

  2258 \bigskip

  2259

  2260 The general form of a primitive recursive definition is

  2261 \begin{ttbox}

  2262 primrec

  2263     {\it reduction rules}

  2264 \end{ttbox}

  2265 where \textit{reduction rules} specify one or more equations of the form

  2266 $f \, x@1 \, \dots \, x@m \, (C \, y@1 \, \dots \, y@k) \, z@1 \,   2267 \dots \, z@n = r$ such that $C$ is a constructor of the datatype, $r$

  2268 contains only the free variables on the left-hand side, and all recursive

  2269 calls in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$.  There

  2270 must be at most one reduction rule for each constructor.  The order is

  2271 immaterial.  For missing constructors, the function is defined to return a

  2272 default value.

  2273

  2274 If you would like to refer to some rule by name, then you must prefix

  2275 the rule with an identifier.  These identifiers, like those in the

  2276 \texttt{rules} section of a theory, will be visible at the \ML\ level.

  2277

  2278 The primitive recursive function can have infix or mixfix syntax:

  2279 \begin{ttbox}\underscoreon

  2280 consts "@"  :: ['a list, 'a list] => 'a list  (infixr 60)

  2281 primrec

  2282    "[] @ ys = ys"

  2283    "(x#xs) @ ys = x#(xs @ ys)"

  2284 \end{ttbox}

  2285

  2286 The reduction rules become part of the default simpset, which

  2287 leads to short proof scripts:

  2288 \begin{ttbox}\underscoreon

  2289 Goal "(xs @ ys) @ zs = xs @ (ys @ zs)";

  2290 by (induct\_tac "xs" 1);

  2291 by (ALLGOALS Asm\_simp\_tac);

  2292 \end{ttbox}

  2293

  2294 \subsubsection{Example: Evaluation of expressions}

  2295 Using mutual primitive recursion, we can define evaluation functions \texttt{evala}

  2296 and \texttt{eval_bexp} for the datatypes of arithmetic and boolean expressions mentioned in

  2297 {\S}\ref{subsec:datatype:basics}:

  2298 \begin{ttbox}

  2299 consts

  2300   evala :: "['a => nat, 'a aexp] => nat"

  2301   evalb :: "['a => nat, 'a bexp] => bool"

  2302

  2303 primrec

  2304   "evala env (If_then_else b a1 a2) =

  2305      (if evalb env b then evala env a1 else evala env a2)"

  2306   "evala env (Sum a1 a2) = evala env a1 + evala env a2"

  2307   "evala env (Diff a1 a2) = evala env a1 - evala env a2"

  2308   "evala env (Var v) = env v"

  2309   "evala env (Num n) = n"

  2310

  2311   "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"

  2312   "evalb env (And b1 b2) = (evalb env b1 & evalb env b2)"

  2313   "evalb env (Or b1 b2) = (evalb env b1 & evalb env b2)"

  2314 \end{ttbox}

  2315 Since the value of an expression depends on the value of its variables,

  2316 the functions \texttt{evala} and \texttt{evalb} take an additional

  2317 parameter, an {\em environment} of type \texttt{'a => nat}, which maps

  2318 variables to their values.

  2319

  2320 Similarly, we may define substitution functions \texttt{substa}

  2321 and \texttt{substb} for expressions: The mapping \texttt{f} of type

  2322 \texttt{'a => 'a aexp} given as a parameter is lifted canonically

  2323 on the types \texttt{'a aexp} and \texttt{'a bexp}:

  2324 \begin{ttbox}

  2325 consts

  2326   substa :: "['a => 'b aexp, 'a aexp] => 'b aexp"

  2327   substb :: "['a => 'b aexp, 'a bexp] => 'b bexp"

  2328

  2329 primrec

  2330   "substa f (If_then_else b a1 a2) =

  2331      If_then_else (substb f b) (substa f a1) (substa f a2)"

  2332   "substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)"

  2333   "substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)"

  2334   "substa f (Var v) = f v"

  2335   "substa f (Num n) = Num n"

  2336

  2337   "substb f (Less a1 a2) = Less (substa f a1) (substa f a2)"

  2338   "substb f (And b1 b2) = And (substb f b1) (substb f b2)"

  2339   "substb f (Or b1 b2) = Or (substb f b1) (substb f b2)"

  2340 \end{ttbox}

  2341 In textbooks about semantics one often finds {\em substitution theorems},

  2342 which express the relationship between substitution and evaluation. For

  2343 \texttt{'a aexp} and \texttt{'a bexp}, we can prove such a theorem by mutual

  2344 induction, followed by simplification:

  2345 \begin{ttbox}

  2346 Goal

  2347   "evala env (substa (Var(v := a')) a) =

  2348      evala (env(v := evala env a')) a &

  2349    evalb env (substb (Var(v := a')) b) =

  2350      evalb (env(v := evala env a')) b";

  2351 by (induct_tac "a b" 1);

  2352 by (ALLGOALS Asm_full_simp_tac);

  2353 \end{ttbox}

  2354

  2355 \subsubsection{Example: A substitution function for terms}

  2356 Functions on datatypes with nested recursion, such as the type

  2357 \texttt{term} mentioned in {\S}\ref{subsec:datatype:basics}, are

  2358 also defined by mutual primitive recursion. A substitution

  2359 function \texttt{subst_term} on type \texttt{term}, similar to the functions

  2360 \texttt{substa} and \texttt{substb} described above, can

  2361 be defined as follows:

  2362 \begin{ttbox}

  2363 consts

  2364   subst_term :: "['a => ('a,'b) term, ('a,'b) term] => ('a,'b) term"

  2365   subst_term_list ::

  2366     "['a => ('a,'b) term, ('a,'b) term list] => ('a,'b) term list"

  2367

  2368 primrec

  2369   "subst_term f (Var a) = f a"

  2370   "subst_term f (App b ts) = App b (subst_term_list f ts)"

  2371

  2372   "subst_term_list f [] = []"

  2373   "subst_term_list f (t # ts) =

  2374      subst_term f t # subst_term_list f ts"

  2375 \end{ttbox}

  2376 The recursion scheme follows the structure of the unfolded definition of type

  2377 \texttt{term} shown in {\S}\ref{subsec:datatype:basics}. To prove properties of

  2378 this substitution function, mutual induction is needed:

  2379 \begin{ttbox}

  2380 Goal

  2381   "(subst_term ((subst_term f1) o f2) t) =

  2382      (subst_term f1 (subst_term f2 t)) &

  2383    (subst_term_list ((subst_term f1) o f2) ts) =

  2384      (subst_term_list f1 (subst_term_list f2 ts))";

  2385 by (induct_tac "t ts" 1);

  2386 by (ALLGOALS Asm_full_simp_tac);

  2387 \end{ttbox}

  2388

  2389 \subsubsection{Example: A map function for infinitely branching trees}

  2390 Defining functions on infinitely branching datatypes by primitive

  2391 recursion is just as easy. For example, we can define a function

  2392 \texttt{map_tree} on \texttt{'a tree} as follows:

  2393 \begin{ttbox}

  2394 consts

  2395   map_tree :: "('a => 'b) => 'a tree => 'b tree"

  2396

  2397 primrec

  2398   "map_tree f (Atom a) = Atom (f a)"

  2399   "map_tree f (Branch ts) = Branch (\%x. map_tree f (ts x))"

  2400 \end{ttbox}

  2401 Note that all occurrences of functions such as \texttt{ts} in the

  2402 \texttt{primrec} clauses must be applied to an argument. In particular,

  2403 \texttt{map_tree f o ts} is not allowed.

  2404

  2405 \index{recursion!primitive|)}

  2406 \index{*primrec|)}

  2407

  2408

  2409 \subsection{General recursive functions}

  2410 \label{sec:HOL:recdef}

  2411 \index{recursion!general|(}

  2412 \index{*recdef|(}

  2413

  2414 Using \texttt{recdef}, you can declare functions involving nested recursion

  2415 and pattern-matching.  Recursion need not involve datatypes and there are few

  2416 syntactic restrictions.  Termination is proved by showing that each recursive

  2417 call makes the argument smaller in a suitable sense, which you specify by

  2418 supplying a well-founded relation.

  2419

  2420 Here is a simple example, the Fibonacci function.  The first line declares

  2421 \texttt{fib} to be a constant.  The well-founded relation is simply~$<$ (on

  2422 the natural numbers).  Pattern-matching is used here: \texttt{1} is a

  2423 macro for \texttt{Suc~0}.

  2424 \begin{ttbox}

  2425 consts fib  :: "nat => nat"

  2426 recdef fib "less_than"

  2427     "fib 0 = 0"

  2428     "fib 1 = 1"

  2429     "fib (Suc(Suc x)) = (fib x + fib (Suc x))"

  2430 \end{ttbox}

  2431

  2432 With \texttt{recdef}, function definitions may be incomplete, and patterns may

  2433 overlap, as in functional programming.  The \texttt{recdef} package

  2434 disambiguates overlapping patterns by taking the order of rules into account.

  2435 For missing patterns, the function is defined to return a default value.

  2436

  2437 %For example, here is a declaration of the list function \cdx{hd}:

  2438 %\begin{ttbox}

  2439 %consts hd :: 'a list => 'a

  2440 %recdef hd "\{\}"

  2441 %    "hd (x#l) = x"

  2442 %\end{ttbox}

  2443 %Because this function is not recursive, we may supply the empty well-founded

  2444 %relation, $\{\}$.

  2445

  2446 The well-founded relation defines a notion of smaller'' for the function's

  2447 argument type.  The relation $\prec$ is \textbf{well-founded} provided it

  2448 admits no infinitely decreasing chains

  2449 $\cdots\prec x@n\prec\cdots\prec x@1.$

  2450 If the function's argument has type~$\tau$, then $\prec$ has to be a relation

  2451 over~$\tau$: it must have type $(\tau\times\tau)set$.

  2452

  2453 Proving well-foundedness can be tricky, so Isabelle/HOL provides a collection

  2454 of operators for building well-founded relations.  The package recognises

  2455 these operators and automatically proves that the constructed relation is

  2456 well-founded.  Here are those operators, in order of importance:

  2457 \begin{itemize}

  2458 \item \texttt{less_than} is less than'' on the natural numbers.

  2459   (It has type $(nat\times nat)set$, while $<$ has type $[nat,nat]\To bool$.

  2460

  2461 \item $\mathop{\mathtt{measure}} f$, where $f$ has type $\tau\To nat$, is the

  2462   relation~$\prec$ on type~$\tau$ such that $x\prec y$ if and only if

  2463   $f(x)<f(y)$.

  2464   Typically, $f$ takes the recursive function's arguments (as a tuple) and

  2465   returns a result expressed in terms of the function \texttt{size}.  It is

  2466   called a \textbf{measure function}.  Recall that \texttt{size} is overloaded

  2467   and is defined on all datatypes (see {\S}\ref{sec:HOL:size}).

  2468

  2469 \item $\mathop{\mathtt{inv_image}} R\;f$ is a generalisation of

  2470   \texttt{measure}.  It specifies a relation such that $x\prec y$ if and only

  2471   if $f(x)$

  2472   is less than $f(y)$ according to~$R$, which must itself be a well-founded

  2473   relation.

  2474

  2475 \item $R@1\texttt{<*lex*>}R@2$ is the lexicographic product of two relations.

  2476   It

  2477   is a relation on pairs and satisfies $(x@1,x@2)\prec(y@1,y@2)$ if and only

  2478   if $x@1$

  2479   is less than $y@1$ according to~$R@1$ or $x@1=y@1$ and $x@2$

  2480   is less than $y@2$ according to~$R@2$.

  2481

  2482 \item \texttt{finite_psubset} is the proper subset relation on finite sets.

  2483 \end{itemize}

  2484

  2485 We can use \texttt{measure} to declare Euclid's algorithm for the greatest

  2486 common divisor.  The measure function, $\lambda(m,n). n$, specifies that the

  2487 recursion terminates because argument~$n$ decreases.

  2488 \begin{ttbox}

  2489 recdef gcd "measure ((\%(m,n). n) ::nat*nat=>nat)"

  2490     "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"

  2491 \end{ttbox}

  2492

  2493 The general form of a well-founded recursive definition is

  2494 \begin{ttbox}

  2495 recdef {\it function} {\it rel}

  2496     congs   {\it congruence rules}      {\bf(optional)}

  2497     simpset {\it simplification set}      {\bf(optional)}

  2498    {\it reduction rules}

  2499 \end{ttbox}

  2500 where

  2501 \begin{itemize}

  2502 \item \textit{function} is the name of the function, either as an \textit{id}

  2503   or a \textit{string}.

  2504

  2505 \item \textit{rel} is a HOL expression for the well-founded termination

  2506   relation.

  2507

  2508 \item \textit{congruence rules} are required only in highly exceptional

  2509   circumstances.

  2510

  2511 \item The \textit{simplification set} is used to prove that the supplied

  2512   relation is well-founded.  It is also used to prove the \textbf{termination

  2513     conditions}: assertions that arguments of recursive calls decrease under

  2514   \textit{rel}.  By default, simplification uses \texttt{simpset()}, which

  2515   is sufficient to prove well-foundedness for the built-in relations listed

  2516   above.

  2517

  2518 \item \textit{reduction rules} specify one or more recursion equations.  Each

  2519   left-hand side must have the form $f\,t$, where $f$ is the function and $t$

  2520   is a tuple of distinct variables.  If more than one equation is present then

  2521   $f$ is defined by pattern-matching on components of its argument whose type

  2522   is a \texttt{datatype}.

  2523

  2524   The \ML\ identifier $f$\texttt{.simps} contains the reduction rules as

  2525   a list of theorems.

  2526 \end{itemize}

  2527

  2528 With the definition of \texttt{gcd} shown above, Isabelle/HOL is unable to

  2529 prove one termination condition.  It remains as a precondition of the

  2530 recursion theorems:

  2531 \begin{ttbox}

  2532 gcd.simps;

  2533 {\out ["! m n. n ~= 0 --> m mod n < n}

  2534 {\out   ==> gcd (?m,?n) = (if ?n=0 then ?m else gcd (?n, ?m mod ?n))"] }

  2535 {\out : thm list}

  2536 \end{ttbox}

  2537 The theory \texttt{HOL/ex/Primes} illustrates how to prove termination

  2538 conditions afterwards.  The function \texttt{Tfl.tgoalw} is like the standard

  2539 function \texttt{goalw}, which sets up a goal to prove, but its argument

  2540 should be the identifier $f$\texttt{.simps} and its effect is to set up a

  2541 proof of the termination conditions:

  2542 \begin{ttbox}

  2543 Tfl.tgoalw thy [] gcd.simps;

  2544 {\out Level 0}

  2545 {\out ! m n. n ~= 0 --> m mod n < n}

  2546 {\out  1. ! m n. n ~= 0 --> m mod n < n}

  2547 \end{ttbox}

  2548 This subgoal has a one-step proof using \texttt{simp_tac}.  Once the theorem

  2549 is proved, it can be used to eliminate the termination conditions from

  2550 elements of \texttt{gcd.simps}.  Theory \texttt{HOL/Subst/Unify} is a much

  2551 more complicated example of this process, where the termination conditions can

  2552 only be proved by complicated reasoning involving the recursive function

  2553 itself.

  2554

  2555 Isabelle/HOL can prove the \texttt{gcd} function's termination condition

  2556 automatically if supplied with the right simpset.

  2557 \begin{ttbox}

  2558 recdef gcd "measure ((\%(m,n). n) ::nat*nat=>nat)"

  2559   simpset "simpset() addsimps [mod_less_divisor, zero_less_eq]"

  2560     "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"

  2561 \end{ttbox}

  2562

  2563 If all termination conditions were proved automatically, $f$\texttt{.simps}

  2564 is added to the simpset automatically, just as in \texttt{primrec}.

  2565 The simplification rules corresponding to clause $i$ (where counting starts

  2566 at 0) are called $f$\texttt{.}$i$ and can be accessed as \texttt{thms

  2567   "$f$.$i$"},

  2568 which returns a list of theorems. Thus you can, for example, remove specific

  2569 clauses from the simpset. Note that a single clause may give rise to a set of

  2570 simplification rules in order to capture the fact that if clauses overlap,

  2571 their order disambiguates them.

  2572

  2573 A \texttt{recdef} definition also returns an induction rule specialised for

  2574 the recursive function.  For the \texttt{gcd} function above, the induction

  2575 rule is

  2576 \begin{ttbox}

  2577 gcd.induct;

  2578 {\out "(!!m n. n ~= 0 --> ?P n (m mod n) ==> ?P m n) ==> ?P ?u ?v" : thm}

  2579 \end{ttbox}

  2580 This rule should be used to reason inductively about the \texttt{gcd}

  2581 function.  It usually makes the induction hypothesis available at all

  2582 recursive calls, leading to very direct proofs.  If any termination conditions

  2583 remain unproved, they will become additional premises of this rule.

  2584

  2585 \index{recursion!general|)}

  2586 \index{*recdef|)}

  2587

  2588

  2589 \section{Inductive and coinductive definitions}

  2590 \index{*inductive|(}

  2591 \index{*coinductive|(}

  2592

  2593 An {\bf inductive definition} specifies the least set~$R$ closed under given

  2594 rules.  (Applying a rule to elements of~$R$ yields a result within~$R$.)  For

  2595 example, a structural operational semantics is an inductive definition of an

  2596 evaluation relation.  Dually, a {\bf coinductive definition} specifies the

  2597 greatest set~$R$ consistent with given rules.  (Every element of~$R$ can be

  2598 seen as arising by applying a rule to elements of~$R$.)  An important example

  2599 is using bisimulation relations to formalise equivalence of processes and

  2600 infinite data structures.

  2601

  2602 A theory file may contain any number of inductive and coinductive

  2603 definitions.  They may be intermixed with other declarations; in

  2604 particular, the (co)inductive sets {\bf must} be declared separately as

  2605 constants, and may have mixfix syntax or be subject to syntax translations.

  2606

  2607 Each (co)inductive definition adds definitions to the theory and also

  2608 proves some theorems.  Each definition creates an \ML\ structure, which is a

  2609 substructure of the main theory structure.

  2610

  2611 This package is related to the ZF one, described in a separate

  2612 paper,%

  2613 \footnote{It appeared in CADE~\cite{paulson-CADE}; a longer version is

  2614   distributed with Isabelle.}  %

  2615 which you should refer to in case of difficulties.  The package is simpler

  2616 than ZF's thanks to HOL's extra-logical automatic type-checking.  The types of

  2617 the (co)inductive sets determine the domain of the fixedpoint definition, and

  2618 the package does not have to use inference rules for type-checking.

  2619

  2620

  2621 \subsection{The result structure}

  2622 Many of the result structure's components have been discussed in the paper;

  2623 others are self-explanatory.

  2624 \begin{description}

  2625 \item[\tt defs] is the list of definitions of the recursive sets.

  2626

  2627 \item[\tt mono] is a monotonicity theorem for the fixedpoint operator.

  2628

  2629 \item[\tt unfold] is a fixedpoint equation for the recursive set (the union of

  2630 the recursive sets, in the case of mutual recursion).

  2631

  2632 \item[\tt intrs] is the list of introduction rules, now proved as theorems, for

  2633 the recursive sets.  The rules are also available individually, using the

  2634 names given them in the theory file.

  2635

  2636 \item[\tt elims] is the list of elimination rule.  This is for compatibility

  2637   with ML scripts; within the theory the name is \texttt{cases}.

  2638

  2639 \item[\tt elim] is the head of the list \texttt{elims}.  This is for

  2640   compatibility only.

  2641

  2642 \item[\tt mk_cases] is a function to create simplified instances of {\tt

  2643 elim} using freeness reasoning on underlying datatypes.

  2644 \end{description}

  2645

  2646 For an inductive definition, the result structure contains the

  2647 rule \texttt{induct}.  For a

  2648 coinductive definition, it contains the rule \verb|coinduct|.

  2649

  2650 Figure~\ref{def-result-fig} summarises the two result signatures,

  2651 specifying the types of all these components.

  2652

  2653 \begin{figure}

  2654 \begin{ttbox}

  2655 sig

  2656 val defs         : thm list

  2657 val mono         : thm

  2658 val unfold       : thm

  2659 val intrs        : thm list

  2660 val elims        : thm list

  2661 val elim         : thm

  2662 val mk_cases     : string -> thm

  2663 {\it(Inductive definitions only)}

  2664 val induct       : thm

  2665 {\it(coinductive definitions only)}

  2666 val coinduct     : thm

  2667 end

  2668 \end{ttbox}

  2669 \hrule

  2670 \caption{The {\ML} result of a (co)inductive definition} \label{def-result-fig}

  2671 \end{figure}

  2672

  2673 \subsection{The syntax of a (co)inductive definition}

  2674 An inductive definition has the form

  2675 \begin{ttbox}

  2676 inductive    {\it inductive sets}

  2677   intrs      {\it introduction rules}

  2678   monos      {\it monotonicity theorems}

  2679 \end{ttbox}

  2680 A coinductive definition is identical, except that it starts with the keyword

  2681 \texttt{coinductive}.

  2682

  2683 The \texttt{monos} section is optional; if present it is specified by a list

  2684 of identifiers.

  2685

  2686 \begin{itemize}

  2687 \item The \textit{inductive sets} are specified by one or more strings.

  2688

  2689 \item The \textit{introduction rules} specify one or more introduction rules in

  2690   the form \textit{ident\/}~\textit{string}, where the identifier gives the name of

  2691   the rule in the result structure.

  2692

  2693 \item The \textit{monotonicity theorems} are required for each operator

  2694   applied to a recursive set in the introduction rules.  There {\bf must}

  2695   be a theorem of the form $A\subseteq B\Imp M(A)\subseteq M(B)$, for each

  2696   premise $t\in M(R@i)$ in an introduction rule!

  2697

  2698 \item The \textit{constructor definitions} contain definitions of constants

  2699   appearing in the introduction rules.  In most cases it can be omitted.

  2700 \end{itemize}

  2701

  2702

  2703 \subsection{*Monotonicity theorems}

  2704

  2705 Each theory contains a default set of theorems that are used in monotonicity

  2706 proofs. New rules can be added to this set via the \texttt{mono} attribute.

  2707 Theory \texttt{Inductive} shows how this is done. In general, the following

  2708 monotonicity theorems may be added:

  2709 \begin{itemize}

  2710 \item Theorems of the form $A\subseteq B\Imp M(A)\subseteq M(B)$, for proving

  2711   monotonicity of inductive definitions whose introduction rules have premises

  2712   involving terms such as $t\in M(R@i)$.

  2713 \item Monotonicity theorems for logical operators, which are of the general form

  2714   $\List{\cdots \to \cdots;~\ldots;~\cdots \to \cdots} \Imp   2715 \cdots \to \cdots$.

  2716   For example, in the case of the operator $\lor$, the corresponding theorem is

  2717   $  2718 \infer{P@1 \lor P@2 \to Q@1 \lor Q@2}   2719 {P@1 \to Q@1 & P@2 \to Q@2}   2720$

  2721 \item De Morgan style equations for reasoning about the polarity'' of expressions, e.g.

  2722   $  2723 (\lnot \lnot P) ~=~ P \qquad\qquad   2724 (\lnot (P \land Q)) ~=~ (\lnot P \lor \lnot Q)   2725$

  2726 \item Equations for reducing complex operators to more primitive ones whose

  2727   monotonicity can easily be proved, e.g.

  2728   $  2729 (P \to Q) ~=~ (\lnot P \lor Q) \qquad\qquad   2730 \mathtt{Ball}~A~P ~\equiv~ \forall x.~x \in A \to P~x   2731$

  2732 \end{itemize}

  2733

  2734 \subsection{Example of an inductive definition}

  2735 Two declarations, included in a theory file, define the finite powerset

  2736 operator.  First we declare the constant~\texttt{Fin}.  Then we declare it

  2737 inductively, with two introduction rules:

  2738 \begin{ttbox}

  2739 consts Fin :: 'a set => 'a set set

  2740 inductive "Fin A"

  2741   intrs

  2742     emptyI  "{\ttlbrace}{\ttrbrace} : Fin A"

  2743     insertI "[| a: A;  b: Fin A |] ==> insert a b : Fin A"

  2744 \end{ttbox}

  2745 The resulting theory structure contains a substructure, called~\texttt{Fin}.

  2746 It contains the \texttt{Fin}$~A$ introduction rules as the list \texttt{Fin.intrs},

  2747 and also individually as \texttt{Fin.emptyI} and \texttt{Fin.consI}.  The induction

  2748 rule is \texttt{Fin.induct}.

  2749

  2750 For another example, here is a theory file defining the accessible part of a

  2751 relation.  The paper \cite{paulson-CADE} discusses a ZF version of this

  2752 example in more detail.

  2753 \begin{ttbox}

  2754 Acc = WF + Inductive +

  2755

  2756 consts acc :: "('a * 'a)set => 'a set"   (* accessible part *)

  2757

  2758 inductive "acc r"

  2759   intrs

  2760     accI "ALL y. (y, x) : r --> y : acc r ==> x : acc r"

  2761

  2762 end

  2763 \end{ttbox}

  2764 The Isabelle distribution contains many other inductive definitions.  Simple

  2765 examples are collected on subdirectory \texttt{HOL/Induct}.  The theory

  2766 \texttt{HOL/Induct/LList} contains coinductive definitions.  Larger examples

  2767 may be found on other subdirectories of \texttt{HOL}, such as \texttt{IMP},

  2768 \texttt{Lambda} and \texttt{Auth}.

  2769

  2770 \index{*coinductive|)} \index{*inductive|)}

  2771

  2772

  2773 \section{Executable specifications}

  2774 \index{code generator}

  2775

  2776 For validation purposes, it is often useful to {\em execute} specifications.

  2777 In principle, specifications could be executed'' using Isabelle's

  2778 inference kernel, i.e. by a combination of resolution and simplification.

  2779 Unfortunately, this approach is rather inefficient. A more efficient way

  2780 of executing specifications is to translate them into a functional

  2781 programming language such as ML. Isabelle's built-in code generator

  2782 supports this.

  2783

  2784 \railalias{verblbrace}{\texttt{\ttlbrace*}}

  2785 \railalias{verbrbrace}{\texttt{*\ttrbrace}}

  2786 \railterm{verblbrace}

  2787 \railterm{verbrbrace}

  2788

  2789 \begin{figure}

  2790 \begin{rail}

  2791 codegen : ( 'code_module' | 'code_library' ) modespec ? name ? \\

  2792   ( 'file' name ) ? ( 'imports' ( name + ) ) ? \\

  2793   'contains' ( ( name '=' term ) + | term + );

  2794

  2795 modespec : '(' ( name * ) ')';

  2796 \end{rail}

  2797 \caption{Code generator invocation syntax}

  2798 \label{fig:HOL:codegen-invocation}

  2799 \end{figure}

  2800

  2801 \begin{figure}

  2802 \begin{rail}

  2803 constscode : 'consts_code' (codespec +);

  2804

  2805 codespec : const template attachment ?;

  2806

  2807 typescode : 'types_code' (tycodespec +);

  2808

  2809 tycodespec : name template attachment ?;

  2810

  2811 const : term;

  2812

  2813 template: '(' string ')';

  2814

  2815 attachment: 'attach' modespec ? verblbrace text verbrbrace;

  2816 \end{rail}

  2817 \caption{Code generator configuration syntax}

  2818 \label{fig:HOL:codegen-configuration}

  2819 \end{figure}

  2820

  2821 \subsection{Invoking the code generator}

  2822

  2823 The code generator is invoked via the \ttindex{code_module} and

  2824 \ttindex{code_library} commands (see Fig.~\ref{fig:HOL:codegen-invocation}),

  2825 which correspond to {\em incremental} and {\em modular} code generation,

  2826 respectively.

  2827 \begin{description}

  2828 \item[Modular] For each theory, an ML structure is generated, containing the

  2829   code generated from the constants defined in this theory.

  2830 \item[Incremental] All the generated code is emitted into the same structure.

  2831   This structure may import code from previously generated structures, which

  2832   can be specified via \texttt{imports}.

  2833   Moreover, the generated structure may also be referred to in later invocations

  2834   of the code generator.

  2835 \end{description}

  2836 After the \texttt{code_module} and \texttt{code_library} keywords, the user

  2837 may specify an optional list of modes'' in parentheses. These can be used

  2838 to instruct the code generator to emit additional code for special purposes,

  2839 e.g.\ functions for converting elements of generated datatypes to Isabelle terms,

  2840 or test data generators. The list of modes is followed by a module name.

  2841 The module name is optional for modular code generation, but must be specified

  2842 for incremental code generation.

  2843 The code can either be written to a file,

  2844 in which case a file name has to be specified after the \texttt{file} keyword, or be

  2845 loaded directly into Isabelle's ML environment. In the latter case,

  2846 the \texttt{ML} theory command can be used to inspect the results

  2847 interactively.

  2848 The terms from which to generate code can be specified after the

  2849 \texttt{contains} keyword, either as a list of bindings, or just as

  2850 a list of terms. In the latter case, the code generator just produces

  2851 code for all constants and types occuring in the term, but does not

  2852 bind the compiled terms to ML identifiers.

  2853 For example,

  2854 \begin{ttbox}

  2855 code_module Test

  2856 contains

  2857   test = "foldl op + (0::int) [1,2,3,4,5]"

  2858 \end{ttbox}

  2859 binds the result of compiling the term

  2860 \texttt{foldl op + (0::int) [1,2,3,4,5]}

  2861 (i.e.~\texttt{15}) to the ML identifier \texttt{Test.test}.

  2862

  2863 \subsection{Configuring the code generator}

  2864

  2865 When generating code for a complex term, the code generator recursively

  2866 calls itself for all subterms.

  2867 When it arrives at a constant, the default strategy of the code

  2868 generator is to look up its definition and try to generate code for it.

  2869 Constants which have no definitions that

  2870 are immediately executable, may be associated with a piece of ML

  2871 code manually using the \ttindex{consts_code} command

  2872 (see Fig.~\ref{fig:HOL:codegen-configuration}).

  2873 It takes a list whose elements consist of a constant (given in usual term syntax

  2874 -- an explicit type constraint accounts for overloading), and a

  2875 mixfix template describing the ML code. The latter is very much the

  2876 same as the mixfix templates used when declaring new constants.

  2877 The most notable difference is that terms may be included in the ML

  2878 template using antiquotation brackets \verb|{*|~$\ldots$~\verb|*}|.

  2879 A similar mechanism is available for

  2880 types: \ttindex{types_code} associates type constructors with

  2881 specific ML code. For example, the declaration

  2882 \begin{ttbox}

  2883 types_code

  2884   "*"     ("(_ */ _)")

  2885

  2886 consts_code

  2887   "Pair"    ("(_,/ _)")

  2888 \end{ttbox}

  2889 in theory \texttt{Product_Type} describes how the product type of Isabelle/HOL

  2890 should be compiled to ML. Sometimes, the code associated with a

  2891 constant or type may need to refer to auxiliary functions, which

  2892 have to be emitted when the constant is used. Code for such auxiliary

  2893 functions can be declared using \texttt{attach}. For example, the

  2894 \texttt{wfrec} function from theory \texttt{Wellfounded_Recursion}

  2895 is implemented as follows:

  2896 \begin{ttbox}

  2897 consts_code

  2898   "wfrec"   ("\bs<module>wfrec?")

  2899 attach \{*

  2900 fun wfrec f x = f (wfrec f) x;

  2901 *\}

  2902 \end{ttbox}

  2903 If the code containing a call to \texttt{wfrec} resides in an ML structure

  2904 different from the one containing the function definition attached to

  2905 \texttt{wfrec}, the name of the ML structure (followed by a \texttt{.}'')

  2906 is inserted in place of \texttt{\bs<module>}'' in the above template.

  2907 The \texttt{?}'' means that the code generator should ignore the first

  2908 argument of \texttt{wfrec}, i.e.\ the termination relation, which is

  2909 usually not executable.

  2910

  2911 Another possibility of configuring the code generator is to register

  2912 theorems to be used for code generation. Theorems can be registered

  2913 via the \ttindex{code} attribute. It takes an optional name as

  2914 an argument, which indicates the format of the theorem. Currently

  2915 supported formats are equations (this is the default when no name

  2916 is specified) and horn clauses (this is indicated by the name

  2917 \texttt{ind}). The left-hand sides of equations may only contain

  2918 constructors and distinct variables, whereas horn clauses must have

  2919 the same format as introduction rules of inductive definitions.

  2920 For example, the declaration

  2921 \begin{ttbox}

  2922 lemma Suc_less_eq [iff, code]: "(Suc m < Suc n) = (m < n)" $$\langle\ldots\rangle$$

  2923 lemma [code]: "((n::nat) < 0) = False" by simp

  2924 lemma [code]: "(0 < Suc n) = True" by simp

  2925 \end{ttbox}

  2926 in theory \texttt{Nat} specifies three equations from which to generate

  2927 code for \texttt{<} on natural numbers.

  2928

  2929 \subsection{Specific HOL code generators}

  2930

  2931 The basic code generator framework offered by Isabelle/Pure has

  2932 already been extended with additional code generators for specific

  2933 HOL constructs. These include datatypes, recursive functions and

  2934 inductive relations. The code generator for inductive relations

  2935 can handle expressions of the form $(t@1,\ldots,t@n) \in r$, where

  2936 $r$ is an inductively defined relation. If at least one of the

  2937 $t@i$ is a dummy pattern $_$'', the above expression evaluates to a

  2938 sequence of possible answers. If all of the $t@i$ are proper

  2939 terms, the expression evaluates to a boolean value.

  2940 \begin{small}

  2941 \begin{alltt}

  2942   theory Test = Lambda:

  2943

  2944   code_module Test

  2945   contains

  2946     test1 = "Abs (Var 0) $$\circ$$ Var 0 -> Var 0"

  2947     test2 = "Abs (Abs (Var 0 $$\circ$$ Var 0) $$\circ$$ (Abs (Var 0) $$\circ$$ Var 0)) -> _"

  2948 \end{alltt}

  2949 \end{small}

  2950 In the above example, \texttt{Test.test1} evaluates to the boolean

  2951 value \texttt{true}, whereas \texttt{Test.test2} is a sequence whose

  2952 elements can be inspected using \texttt{Seq.pull} or similar functions.

  2953 \begin{ttbox}

  2954 ML \{* Seq.pull Test.test2 *\}  -- \{* This is the first answer *\}

  2955 ML \{* Seq.pull (snd (the it)) *\}  -- \{* This is the second answer *\}

  2956 \end{ttbox}

  2957 The theory

  2958 underlying the HOL code generator is described more detailed in

  2959 \cite{Berghofer-Nipkow:2002}. More examples that illustrate the usage

  2960 of the code generator can be found e.g.~in theories

  2961 \texttt{MicroJava/J/JListExample} and \texttt{MicroJava/JVM/JVMListExample}.

  2962

  2963 \section{The examples directories}

  2964

  2965 Directory \texttt{HOL/Auth} contains theories for proving the correctness of

  2966 cryptographic protocols~\cite{paulson-jcs}.  The approach is based upon

  2967 operational semantics rather than the more usual belief logics.  On the same

  2968 directory are proofs for some standard examples, such as the Needham-Schroeder

  2969 public-key authentication protocol and the Otway-Rees

  2970 protocol.

  2971

  2972 Directory \texttt{HOL/IMP} contains a formalization of various denotational,

  2973 operational and axiomatic semantics of a simple while-language, the necessary

  2974 equivalence proofs, soundness and completeness of the Hoare rules with

  2975 respect to the denotational semantics, and soundness and completeness of a

  2976 verification condition generator.  Much of development is taken from

  2977 Winskel~\cite{winskel93}.  For details see~\cite{nipkow-IMP}.

  2978

  2979 Directory \texttt{HOL/Hoare} contains a user friendly surface syntax for Hoare

  2980 logic, including a tactic for generating verification-conditions.

  2981

  2982 Directory \texttt{HOL/MiniML} contains a formalization of the type system of

  2983 the core functional language Mini-ML and a correctness proof for its type

  2984 inference algorithm $\cal W$~\cite{milner78,nipkow-W}.

  2985

  2986 Directory \texttt{HOL/Lambda} contains a formalization of untyped

  2987 $\lambda$-calculus in de~Bruijn notation and Church-Rosser proofs for $\beta$

  2988 and $\eta$ reduction~\cite{Nipkow-CR}.

  2989

  2990 Directory \texttt{HOL/Subst} contains Martin Coen's mechanization of a theory

  2991 of substitutions and unifiers.  It is based on Paulson's previous

  2992 mechanisation in LCF~\cite{paulson85} of Manna and Waldinger's

  2993 theory~\cite{mw81}.  It demonstrates a complicated use of \texttt{recdef},

  2994 with nested recursion.

  2995

  2996 Directory \texttt{HOL/Induct} presents simple examples of (co)inductive

  2997 definitions and datatypes.

  2998 \begin{itemize}

  2999 \item Theory \texttt{PropLog} proves the soundness and completeness of

  3000   classical propositional logic, given a truth table semantics.  The only

  3001   connective is $\imp$.  A Hilbert-style axiom system is specified, and its

  3002   set of theorems defined inductively.  A similar proof in ZF is described

  3003   elsewhere~\cite{paulson-set-II}.

  3004

  3005 \item Theory \texttt{Term} defines the datatype \texttt{term}.

  3006

  3007 \item Theory \texttt{ABexp} defines arithmetic and boolean expressions

  3008  as mutually recursive datatypes.

  3009

  3010 \item The definition of lazy lists demonstrates methods for handling

  3011   infinite data structures and coinduction in higher-order

  3012   logic~\cite{paulson-coind}.%

  3013 \footnote{To be precise, these lists are \emph{potentially infinite} rather

  3014   than lazy.  Lazy implies a particular operational semantics.}

  3015   Theory \thydx{LList} defines an operator for

  3016   corecursion on lazy lists, which is used to define a few simple functions

  3017   such as map and append.   A coinduction principle is defined

  3018   for proving equations on lazy lists.

  3019

  3020 \item Theory \thydx{LFilter} defines the filter functional for lazy lists.

  3021   This functional is notoriously difficult to define because finding the next

  3022   element meeting the predicate requires possibly unlimited search.  It is not

  3023   computable, but can be expressed using a combination of induction and

  3024   corecursion.

  3025

  3026 \item Theory \thydx{Exp} illustrates the use of iterated inductive definitions

  3027   to express a programming language semantics that appears to require mutual

  3028   induction.  Iterated induction allows greater modularity.

  3029 \end{itemize}

  3030

  3031 Directory \texttt{HOL/ex} contains other examples and experimental proofs in

  3032 HOL.

  3033 \begin{itemize}

  3034 \item Theory \texttt{Recdef} presents many examples of using \texttt{recdef}

  3035   to define recursive functions.  Another example is \texttt{Fib}, which

  3036   defines the Fibonacci function.

  3037

  3038 \item Theory \texttt{Primes} defines the Greatest Common Divisor of two

  3039   natural numbers and proves a key lemma of the Fundamental Theorem of

  3040   Arithmetic: if $p$ is prime and $p$ divides $m\times n$ then $p$ divides~$m$

  3041   or $p$ divides~$n$.

  3042

  3043 \item Theory \texttt{Primrec} develops some computation theory.  It

  3044   inductively defines the set of primitive recursive functions and presents a

  3045   proof that Ackermann's function is not primitive recursive.

  3046

  3047 \item File \texttt{cla.ML} demonstrates the classical reasoner on over sixty

  3048   predicate calculus theorems, ranging from simple tautologies to

  3049   moderately difficult problems involving equality and quantifiers.

  3050

  3051 \item File \texttt{meson.ML} contains an experimental implementation of the {\sc

  3052     meson} proof procedure, inspired by Plaisted~\cite{plaisted90}.  It is

  3053   much more powerful than Isabelle's classical reasoner.  But it is less

  3054   useful in practice because it works only for pure logic; it does not

  3055   accept derived rules for the set theory primitives, for example.

  3056

  3057 \item File \texttt{mesontest.ML} contains test data for the {\sc meson} proof

  3058   procedure.  These are mostly taken from Pelletier \cite{pelletier86}.

  3059

  3060 \item File \texttt{set.ML} proves Cantor's Theorem, which is presented in

  3061   {\S}\ref{sec:hol-cantor} below, and the Schr{\"o}der-Bernstein Theorem.

  3062

  3063 \item Theory \texttt{MT} contains Jacob Frost's formalization~\cite{frost93} of

  3064   Milner and Tofte's coinduction example~\cite{milner-coind}.  This

  3065   substantial proof concerns the soundness of a type system for a simple

  3066   functional language.  The semantics of recursion is given by a cyclic

  3067   environment, which makes a coinductive argument appropriate.

  3068 \end{itemize}

  3069

  3070

  3071 \goodbreak

  3072 \section{Example: Cantor's Theorem}\label{sec:hol-cantor}

  3073 Cantor's Theorem states that every set has more subsets than it has

  3074 elements.  It has become a favourite example in higher-order logic since

  3075 it is so easily expressed:

  3076 $\forall f::\alpha \To \alpha \To bool. \exists S::\alpha\To bool.   3077 \forall x::\alpha. f~x \not= S   3078$

  3079 %

  3080 Viewing types as sets, $\alpha\To bool$ represents the powerset

  3081 of~$\alpha$.  This version states that for every function from $\alpha$ to

  3082 its powerset, some subset is outside its range.

  3083

  3084 The Isabelle proof uses HOL's set theory, with the type $\alpha\,set$ and

  3085 the operator \cdx{range}.

  3086 \begin{ttbox}

  3087 context Set.thy;

  3088 \end{ttbox}

  3089 The set~$S$ is given as an unknown instead of a

  3090 quantified variable so that we may inspect the subset found by the proof.

  3091 \begin{ttbox}

  3092 Goal "?S ~: range\thinspace(f :: 'a=>'a set)";

  3093 {\out Level 0}

  3094 {\out ?S ~: range f}

  3095 {\out  1. ?S ~: range f}

  3096 \end{ttbox}

  3097 The first two steps are routine.  The rule \tdx{rangeE} replaces

  3098 $\Var{S}\in \texttt{range} \, f$ by $\Var{S}=f~x$ for some~$x$.

  3099 \begin{ttbox}

  3100 by (resolve_tac [notI] 1);

  3101 {\out Level 1}

  3102 {\out ?S ~: range f}

  3103 {\out  1. ?S : range f ==> False}

  3104 \ttbreak

  3105 by (eresolve_tac [rangeE] 1);

  3106 {\out Level 2}

  3107 {\out ?S ~: range f}

  3108 {\out  1. !!x. ?S = f x ==> False}

  3109 \end{ttbox}

  3110 Next, we apply \tdx{equalityCE}, reasoning that since $\Var{S}=f~x$,

  3111 we have $\Var{c}\in \Var{S}$ if and only if $\Var{c}\in f~x$ for

  3112 any~$\Var{c}$.

  3113 \begin{ttbox}

  3114 by (eresolve_tac [equalityCE] 1);

  3115 {\out Level 3}

  3116 {\out ?S ~: range f}

  3117 {\out  1. !!x. [| ?c3 x : ?S; ?c3 x : f x |] ==> False}

  3118 {\out  2. !!x. [| ?c3 x ~: ?S; ?c3 x ~: f x |] ==> False}

  3119 \end{ttbox}

  3120 Now we use a bit of creativity.  Suppose that~$\Var{S}$ has the form of a

  3121 comprehension.  Then $\Var{c}\in\{x.\Var{P}~x\}$ implies

  3122 $\Var{P}~\Var{c}$.   Destruct-resolution using \tdx{CollectD}

  3123 instantiates~$\Var{S}$ and creates the new assumption.

  3124 \begin{ttbox}

  3125 by (dresolve_tac [CollectD] 1);

  3126 {\out Level 4}

  3127 {\out {\ttlbrace}x. ?P7 x{\ttrbrace} ~: range f}

  3128 {\out  1. !!x. [| ?c3 x : f x; ?P7(?c3 x) |] ==> False}

  3129 {\out  2. !!x. [| ?c3 x ~: {\ttlbrace}x. ?P7 x{\ttrbrace}; ?c3 x ~: f x |] ==> False}

  3130 \end{ttbox}

  3131 Forcing a contradiction between the two assumptions of subgoal~1

  3132 completes the instantiation of~$S$.  It is now the set $\{x. x\not\in   3133 f~x\}$, which is the standard diagonal construction.

  3134 \begin{ttbox}

  3135 by (contr_tac 1);

  3136 {\out Level 5}

  3137 {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f}

  3138 {\out  1. !!x. [| x ~: {\ttlbrace}x. x ~: f x{\ttrbrace}; x ~: f x |] ==> False}

  3139 \end{ttbox}

  3140 The rest should be easy.  To apply \tdx{CollectI} to the negated

  3141 assumption, we employ \ttindex{swap_res_tac}:

  3142 \begin{ttbox}

  3143 by (swap_res_tac [CollectI] 1);

  3144 {\out Level 6}

  3145 {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f}

  3146 {\out  1. !!x. [| x ~: f x; ~ False |] ==> x ~: f x}

  3147 \ttbreak

  3148 by (assume_tac 1);

  3149 {\out Level 7}

  3150 {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f}

  3151 {\out No subgoals!}

  3152 \end{ttbox}

  3153 How much creativity is required?  As it happens, Isabelle can prove this

  3154 theorem automatically.  The default classical set \texttt{claset()} contains

  3155 rules for most of the constructs of HOL's set theory.  We must augment it with

  3156 \tdx{equalityCE} to break up set equalities, and then apply best-first search.

  3157 Depth-first search would diverge, but best-first search successfully navigates

  3158 through the large search space.  \index{search!best-first}

  3159 \begin{ttbox}

  3160 choplev 0;

  3161 {\out Level 0}

  3162 {\out ?S ~: range f}

  3163 {\out  1. ?S ~: range f}

  3164 \ttbreak

  3165 by (best_tac (claset() addSEs [equalityCE]) 1);

  3166 {\out Level 1}

  3167 {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f}

  3168 {\out No subgoals!}

  3169 \end{ttbox}

  3170 If you run this example interactively, make sure your current theory contains

  3171 theory \texttt{Set}, for example by executing \ttindex{context}~{\tt Set.thy}.

  3172 Otherwise the default claset may not contain the rules for set theory.

  3173 \index{higher-order logic|)}

  3174

  3175 %%% Local Variables:

  3176 %%% mode: latex

  3177 %%% TeX-master: "logics-HOL"

  3178 %%% End: