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