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