doc-src/Logics/Old_HOL.tex
author paulson
Fri Feb 16 18:00:47 1996 +0100 (1996-02-16)
changeset 1512 ce37c64244c0
parent 1086 46a7b619e62e
child 2975 230f456956a2
permissions -rw-r--r--
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
lcp@104
     1
%% $Id$
lcp@315
     2
\chapter{Higher-Order Logic}
lcp@315
     3
\index{higher-order logic|(}
lcp@315
     4
\index{HOL system@{\sc hol} system}
lcp@315
     5
lcp@315
     6
The theory~\thydx{HOL} implements higher-order logic.
lcp@344
     7
It is based on Gordon's~{\sc hol} system~\cite{mgordon-hol}, which itself is
lcp@315
     8
based on Church's original paper~\cite{church40}.  Andrews's
lcp@315
     9
book~\cite{andrews86} is a full description of higher-order logic.
lcp@315
    10
Experience with the {\sc hol} system has demonstrated that higher-order
lcp@315
    11
logic is useful for hardware verification; beyond this, it is widely
lcp@315
    12
applicable in many areas of mathematics.  It is weaker than {\ZF} set
lcp@315
    13
theory but for most applications this does not matter.  If you prefer {\ML}
lcp@315
    14
to Lisp, you will probably prefer \HOL\ to~{\ZF}.
lcp@104
    15
lcp@315
    16
Previous releases of Isabelle included a different version of~\HOL, with
lcp@315
    17
explicit type inference rules~\cite{paulson-COLOG}.  This version no longer
lcp@315
    18
exists, but \thydx{ZF} supports a similar style of reasoning.
lcp@104
    19
nipkow@306
    20
\HOL\ has a distinct feel, compared with {\ZF} and {\CTT}.  It
lcp@104
    21
identifies object-level types with meta-level types, taking advantage of
lcp@104
    22
Isabelle's built-in type checker.  It identifies object-level functions
lcp@104
    23
with meta-level functions, so it uses Isabelle's operations for abstraction
lcp@315
    24
and application.  There is no `apply' operator: function applications are
lcp@104
    25
written as simply~$f(a)$ rather than $f{\tt`}a$.
lcp@104
    26
nipkow@306
    27
These identifications allow Isabelle to support \HOL\ particularly nicely,
nipkow@306
    28
but they also mean that \HOL\ requires more sophistication from the user
lcp@104
    29
--- in particular, an understanding of Isabelle's type system.  Beginners
lcp@315
    30
should work with {\tt show_types} set to {\tt true}.  Gain experience by
lcp@315
    31
working in first-order logic before attempting to use higher-order logic.
lcp@315
    32
This chapter assumes familiarity with~{\FOL{}}.
lcp@104
    33
lcp@104
    34
lcp@104
    35
\begin{figure} 
lcp@104
    36
\begin{center}
lcp@104
    37
\begin{tabular}{rrr} 
lcp@111
    38
  \it name      &\it meta-type  & \it description \\ 
lcp@315
    39
  \cdx{Trueprop}& $bool\To prop$                & coercion to $prop$\\
lcp@315
    40
  \cdx{not}     & $bool\To bool$                & negation ($\neg$) \\
lcp@315
    41
  \cdx{True}    & $bool$                        & tautology ($\top$) \\
lcp@315
    42
  \cdx{False}   & $bool$                        & absurdity ($\bot$) \\
lcp@315
    43
  \cdx{if}      & $[bool,\alpha,\alpha]\To\alpha::term$ & conditional \\
lcp@315
    44
  \cdx{Inv}     & $(\alpha\To\beta)\To(\beta\To\alpha)$ & function inversion\\
lcp@315
    45
  \cdx{Let}     & $[\alpha,\alpha\To\beta]\To\beta$ & let binder
lcp@104
    46
\end{tabular}
lcp@104
    47
\end{center}
lcp@104
    48
\subcaption{Constants}
lcp@104
    49
lcp@104
    50
\begin{center}
lcp@315
    51
\index{"@@{\tt\at} symbol}
lcp@315
    52
\index{*"! symbol}\index{*"? symbol}
lcp@315
    53
\index{*"?"! symbol}\index{*"E"X"! symbol}
lcp@104
    54
\begin{tabular}{llrrr} 
lcp@315
    55
  \it symbol &\it name     &\it meta-type & \it description \\
lcp@315
    56
  \tt\at & \cdx{Eps}  & $(\alpha\To bool)\To\alpha::term$ & 
lcp@111
    57
        Hilbert description ($\epsilon$) \\
lcp@315
    58
  {\tt!~} or \sdx{ALL}  & \cdx{All}  & $(\alpha::term\To bool)\To bool$ & 
lcp@111
    59
        universal quantifier ($\forall$) \\
lcp@315
    60
  {\tt?~} or \sdx{EX}   & \cdx{Ex}   & $(\alpha::term\To bool)\To bool$ & 
lcp@111
    61
        existential quantifier ($\exists$) \\
lcp@315
    62
  {\tt?!} or {\tt EX!}  & \cdx{Ex1}  & $(\alpha::term\To bool)\To bool$ & 
lcp@111
    63
        unique existence ($\exists!$)
lcp@104
    64
\end{tabular}
lcp@104
    65
\end{center}
lcp@104
    66
\subcaption{Binders} 
lcp@104
    67
lcp@104
    68
\begin{center}
lcp@315
    69
\index{*"= symbol}
lcp@315
    70
\index{&@{\tt\&} symbol}
lcp@315
    71
\index{*"| symbol}
lcp@315
    72
\index{*"-"-"> symbol}
lcp@104
    73
\begin{tabular}{rrrr} 
lcp@315
    74
  \it symbol    & \it meta-type & \it priority & \it description \\ 
lcp@315
    75
  \sdx{o}       & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ & 
lcp@111
    76
        Right 50 & composition ($\circ$) \\
lcp@111
    77
  \tt =         & $[\alpha::term,\alpha]\To bool$ & Left 50 & equality ($=$) \\
lcp@315
    78
  \tt <         & $[\alpha::ord,\alpha]\To bool$ & Left 50 & less than ($<$) \\
lcp@315
    79
  \tt <=        & $[\alpha::ord,\alpha]\To bool$ & Left 50 & 
lcp@315
    80
                less than or equals ($\leq$)\\
lcp@111
    81
  \tt \&        & $[bool,bool]\To bool$ & Right 35 & conjunction ($\conj$) \\
lcp@111
    82
  \tt |         & $[bool,bool]\To bool$ & Right 30 & disjunction ($\disj$) \\
lcp@315
    83
  \tt -->       & $[bool,bool]\To bool$ & Right 25 & implication ($\imp$)
lcp@104
    84
\end{tabular}
lcp@104
    85
\end{center}
lcp@104
    86
\subcaption{Infixes}
lcp@104
    87
\caption{Syntax of {\tt HOL}} \label{hol-constants}
lcp@104
    88
\end{figure}
lcp@104
    89
lcp@104
    90
nipkow@306
    91
\begin{figure}
lcp@315
    92
\index{*let symbol}
lcp@315
    93
\index{*in symbol}
lcp@104
    94
\dquotes
lcp@315
    95
\[\begin{array}{rclcl}
lcp@104
    96
    term & = & \hbox{expression of class~$term$} \\
lcp@315
    97
         & | & "\at~" id~id^* " . " formula \\
lcp@315
    98
         & | & 
lcp@315
    99
    \multicolumn{3}{l}{"let"~id~"="~term";"\dots";"~id~"="~term~"in"~term}
lcp@315
   100
               \\[2ex]
lcp@104
   101
 formula & = & \hbox{expression of type~$bool$} \\
lcp@111
   102
         & | & term " = " term \\
lcp@111
   103
         & | & term " \ttilde= " term \\
lcp@111
   104
         & | & term " < " term \\
lcp@111
   105
         & | & term " <= " term \\
lcp@111
   106
         & | & "\ttilde\ " formula \\
lcp@111
   107
         & | & formula " \& " formula \\
lcp@111
   108
         & | & formula " | " formula \\
lcp@111
   109
         & | & formula " --> " formula \\
lcp@315
   110
         & | & "!~~~" id~id^* " . " formula 
lcp@111
   111
         & | & "ALL~" id~id^* " . " formula \\
lcp@315
   112
         & | & "?~~~" id~id^* " . " formula 
lcp@111
   113
         & | & "EX~~" id~id^* " . " formula \\
lcp@315
   114
         & | & "?!~~" id~id^* " . " formula 
lcp@111
   115
         & | & "EX!~" id~id^* " . " formula
lcp@104
   116
  \end{array}
lcp@104
   117
\]
nipkow@306
   118
\caption{Full grammar for \HOL} \label{hol-grammar}
lcp@104
   119
\end{figure} 
lcp@104
   120
lcp@104
   121
lcp@104
   122
\section{Syntax}
lcp@315
   123
The type class of higher-order terms is called~\cldx{term}.  Type variables
lcp@315
   124
range over this class by default.  The equality symbol and quantifiers are
lcp@315
   125
polymorphic over class {\tt term}.
lcp@104
   126
lcp@315
   127
Class \cldx{ord} consists of all ordered types; the relations $<$ and
lcp@104
   128
$\leq$ are polymorphic over this class, as are the functions
lcp@315
   129
\cdx{mono}, \cdx{min} and \cdx{max}.  Three other
lcp@315
   130
type classes --- \cldx{plus}, \cldx{minus} and \cldx{times} --- permit
lcp@104
   131
overloading of the operators {\tt+}, {\tt-} and {\tt*}.  In particular,
lcp@104
   132
{\tt-} is overloaded for set difference and subtraction.
lcp@315
   133
\index{*"+ symbol}
lcp@315
   134
\index{*"- symbol}
lcp@315
   135
\index{*"* symbol}
lcp@104
   136
lcp@104
   137
Figure~\ref{hol-constants} lists the constants (including infixes and
lcp@315
   138
binders), while Fig.\ts\ref{hol-grammar} presents the grammar of
lcp@287
   139
higher-order logic.  Note that $a$\verb|~=|$b$ is translated to
lcp@315
   140
$\neg(a=b)$.
lcp@315
   141
lcp@315
   142
\begin{warn}
lcp@315
   143
  \HOL\ has no if-and-only-if connective; logical equivalence is expressed
lcp@315
   144
  using equality.  But equality has a high priority, as befitting a
lcp@315
   145
  relation, while if-and-only-if typically has the lowest priority.  Thus,
lcp@315
   146
  $\neg\neg P=P$ abbreviates $\neg\neg (P=P)$ and not $(\neg\neg P)=P$.
lcp@315
   147
  When using $=$ to mean logical equivalence, enclose both operands in
lcp@315
   148
  parentheses.
lcp@315
   149
\end{warn}
lcp@104
   150
lcp@287
   151
\subsection{Types}\label{HOL-types}
lcp@315
   152
The type of formulae, \tydx{bool}, belongs to class \cldx{term}; thus,
lcp@315
   153
formulae are terms.  The built-in type~\tydx{fun}, which constructs function
lcp@315
   154
types, is overloaded with arity {\tt(term,term)term}.  Thus, $\sigma\To\tau$
lcp@315
   155
belongs to class~{\tt term} if $\sigma$ and~$\tau$ do, allowing quantification
lcp@315
   156
over functions.
lcp@104
   157
lcp@315
   158
Types in \HOL\ must be non-empty; otherwise the quantifier rules would be
lcp@315
   159
unsound.  I have commented on this elsewhere~\cite[\S7]{paulson-COLOG}.
lcp@315
   160
lcp@315
   161
\index{type definitions}
lcp@104
   162
Gordon's {\sc hol} system supports {\bf type definitions}.  A type is
lcp@104
   163
defined by exhibiting an existing type~$\sigma$, a predicate~$P::\sigma\To
lcp@104
   164
bool$, and a theorem of the form $\exists x::\sigma.P(x)$.  Thus~$P$
lcp@104
   165
specifies a non-empty subset of~$\sigma$, and the new type denotes this
lcp@104
   166
subset.  New function constants are generated to establish an isomorphism
lcp@104
   167
between the new type and the subset.  If type~$\sigma$ involves type
lcp@104
   168
variables $\alpha@1$, \ldots, $\alpha@n$, then the type definition creates
lcp@104
   169
a type constructor $(\alpha@1,\ldots,\alpha@n)ty$ rather than a particular
lcp@344
   170
type.  Melham~\cite{melham89} discusses type definitions at length, with
lcp@344
   171
examples. 
lcp@104
   172
lcp@104
   173
Isabelle does not support type definitions at present.  Instead, they are
lcp@315
   174
mimicked by explicit definitions of isomorphism functions.  The definitions
lcp@315
   175
should be supported by theorems of the form $\exists x::\sigma.P(x)$, but
lcp@315
   176
Isabelle cannot enforce this.
lcp@104
   177
lcp@104
   178
lcp@104
   179
\subsection{Binders}
lcp@104
   180
Hilbert's {\bf description} operator~$\epsilon x.P[x]$ stands for some~$a$
nipkow@306
   181
satisfying~$P[a]$, if such exists.  Since all terms in \HOL\ denote
lcp@104
   182
something, a description is always meaningful, but we do not know its value
lcp@104
   183
unless $P[x]$ defines it uniquely.  We may write descriptions as
lcp@315
   184
\cdx{Eps}($P$) or use the syntax
lcp@315
   185
\hbox{\tt \at $x$.$P[x]$}.
lcp@315
   186
lcp@315
   187
Existential quantification is defined by
lcp@315
   188
\[ \exists x.P(x) \;\equiv\; P(\epsilon x.P(x)). \]
lcp@104
   189
The unique existence quantifier, $\exists!x.P[x]$, is defined in terms
lcp@104
   190
of~$\exists$ and~$\forall$.  An Isabelle binder, it admits nested
lcp@104
   191
quantifications.  For instance, $\exists!x y.P(x,y)$ abbreviates
lcp@104
   192
$\exists!x. \exists!y.P(x,y)$; note that this does not mean that there
lcp@104
   193
exists a unique pair $(x,y)$ satisfying~$P(x,y)$.
lcp@104
   194
lcp@315
   195
\index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system}
nipkow@306
   196
Quantifiers have two notations.  As in Gordon's {\sc hol} system, \HOL\
lcp@104
   197
uses~{\tt!}\ and~{\tt?}\ to stand for $\forall$ and $\exists$.  The
lcp@104
   198
existential quantifier must be followed by a space; thus {\tt?x} is an
lcp@104
   199
unknown, while \verb'? x.f(x)=y' is a quantification.  Isabelle's usual
lcp@315
   200
notation for quantifiers, \sdx{ALL} and \sdx{EX}, is also
lcp@104
   201
available.  Both notations are accepted for input.  The {\ML} reference
lcp@104
   202
\ttindexbold{HOL_quantifiers} governs the output notation.  If set to {\tt
lcp@104
   203
true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default.  If set
lcp@104
   204
to {\tt false}, then~{\tt ALL} and~{\tt EX} are displayed.
lcp@104
   205
lcp@315
   206
All these binders have priority 10. 
lcp@315
   207
lcp@315
   208
lcp@315
   209
\subsection{The \sdx{let} and \sdx{case} constructions}
lcp@315
   210
Local abbreviations can be introduced by a {\tt let} construct whose
lcp@315
   211
syntax appears in Fig.\ts\ref{hol-grammar}.  Internally it is translated into
lcp@315
   212
the constant~\cdx{Let}.  It can be expanded by rewriting with its
lcp@315
   213
definition, \tdx{Let_def}.
lcp@104
   214
lcp@315
   215
\HOL\ also defines the basic syntax
lcp@315
   216
\[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n\] 
lcp@315
   217
as a uniform means of expressing {\tt case} constructs.  Therefore {\tt
lcp@315
   218
  case} and \sdx{of} are reserved words.  However, so far this is mere
lcp@315
   219
syntax and has no logical meaning.  By declaring translations, you can
lcp@315
   220
cause instances of the {\tt case} construct to denote applications of
lcp@315
   221
particular case operators.  The patterns supplied for $c@1$,~\ldots,~$c@n$
lcp@315
   222
distinguish among the different case operators.  For an example, see the
lcp@315
   223
case construct for lists on page~\pageref{hol-list} below.
lcp@315
   224
nipkow@306
   225
lcp@315
   226
\begin{figure}
lcp@315
   227
\begin{ttbox}\makeatother
nipkow@453
   228
\tdx{refl}           t = (t::'a)
lcp@315
   229
\tdx{subst}          [| s=t; P(s) |] ==> P(t::'a)
nipkow@453
   230
\tdx{ext}            (!!x::'a. (f(x)::'b) = g(x)) ==> (\%x.f(x)) = (\%x.g(x))
lcp@315
   231
\tdx{impI}           (P ==> Q) ==> P-->Q
lcp@315
   232
\tdx{mp}             [| P-->Q;  P |] ==> Q
lcp@315
   233
\tdx{iff}            (P-->Q) --> (Q-->P) --> (P=Q)
lcp@315
   234
\tdx{selectI}        P(x::'a) ==> P(@x.P(x))
lcp@315
   235
\tdx{True_or_False}  (P=True) | (P=False)
lcp@315
   236
\end{ttbox}
lcp@315
   237
\caption{The {\tt HOL} rules} \label{hol-rules}
lcp@315
   238
\end{figure}
nipkow@306
   239
nipkow@306
   240
lcp@344
   241
\begin{figure}\hfuzz=4pt%suppress "Overfull \hbox" message
lcp@287
   242
\begin{ttbox}\makeatother
nipkow@453
   243
\tdx{True_def}   True  == ((\%x::bool.x)=(\%x.x))
lcp@344
   244
\tdx{All_def}    All   == (\%P. P = (\%x.True))
lcp@344
   245
\tdx{Ex_def}     Ex    == (\%P. P(@x.P(x)))
lcp@344
   246
\tdx{False_def}  False == (!P.P)
lcp@344
   247
\tdx{not_def}    not   == (\%P. P-->False)
lcp@344
   248
\tdx{and_def}    op &  == (\%P Q. !R. (P-->Q-->R) --> R)
lcp@344
   249
\tdx{or_def}     op |  == (\%P Q. !R. (P-->R) --> (Q-->R) --> R)
lcp@344
   250
\tdx{Ex1_def}    Ex1   == (\%P. ? x. P(x) & (! y. P(y) --> y=x))
lcp@315
   251
lcp@344
   252
\tdx{Inv_def}    Inv   == (\%(f::'a=>'b) y. @x. f(x)=y)
lcp@344
   253
\tdx{o_def}      op o  == (\%(f::'b=>'c) g (x::'a). f(g(x)))
lcp@344
   254
\tdx{if_def}     if    == (\%P x y.@z::'a.(P=True --> z=x) & (P=False --> z=y))
lcp@344
   255
\tdx{Let_def}    Let(s,f) == f(s)
lcp@315
   256
\end{ttbox}
lcp@315
   257
\caption{The {\tt HOL} definitions} \label{hol-defs}
lcp@315
   258
\end{figure}
lcp@315
   259
lcp@315
   260
lcp@315
   261
\section{Rules of inference}
lcp@315
   262
Figure~\ref{hol-rules} shows the inference rules of~\HOL{}, with
lcp@315
   263
their~{\ML} names.  Some of the rules deserve additional comments:
lcp@315
   264
\begin{ttdescription}
lcp@315
   265
\item[\tdx{ext}] expresses extensionality of functions.
lcp@315
   266
\item[\tdx{iff}] asserts that logically equivalent formulae are
lcp@315
   267
  equal.
lcp@315
   268
\item[\tdx{selectI}] gives the defining property of the Hilbert
lcp@315
   269
  $\epsilon$-operator.  It is a form of the Axiom of Choice.  The derived rule
lcp@315
   270
  \tdx{select_equality} (see below) is often easier to use.
lcp@315
   271
\item[\tdx{True_or_False}] makes the logic classical.\footnote{In
lcp@315
   272
    fact, the $\epsilon$-operator already makes the logic classical, as
lcp@315
   273
    shown by Diaconescu; see Paulson~\cite{paulson-COLOG} for details.}
lcp@315
   274
\end{ttdescription}
lcp@104
   275
lcp@315
   276
\HOL{} follows standard practice in higher-order logic: only a few
lcp@315
   277
connectives are taken as primitive, with the remainder defined obscurely
lcp@344
   278
(Fig.\ts\ref{hol-defs}).  Gordon's {\sc hol} system expresses the
lcp@344
   279
corresponding definitions \cite[page~270]{mgordon-hol} using
lcp@344
   280
object-equality~({\tt=}), which is possible because equality in
lcp@344
   281
higher-order logic may equate formulae and even functions over formulae.
lcp@344
   282
But theory~\HOL{}, like all other Isabelle theories, uses
lcp@344
   283
meta-equality~({\tt==}) for definitions.
lcp@315
   284
lcp@344
   285
Some of the rules mention type variables; for
lcp@344
   286
example, {\tt refl} mentions the type variable~{\tt'a}.  This allows you to
lcp@344
   287
instantiate type variables explicitly by calling {\tt res_inst_tac}.  By
lcp@344
   288
default, explicit type variables have class \cldx{term}.
lcp@104
   289
lcp@315
   290
Include type constraints whenever you state a polymorphic goal.  Type
lcp@315
   291
inference may otherwise make the goal more polymorphic than you intended,
lcp@315
   292
with confusing results.
lcp@315
   293
lcp@315
   294
\begin{warn}
lcp@315
   295
  If resolution fails for no obvious reason, try setting
lcp@315
   296
  \ttindex{show_types} to {\tt true}, causing Isabelle to display types of
lcp@315
   297
  terms.  Possibly set \ttindex{show_sorts} to {\tt true} as well, causing
lcp@315
   298
  Isabelle to display sorts.
lcp@315
   299
lcp@315
   300
  \index{unification!incompleteness of}
lcp@315
   301
  Where function types are involved, Isabelle's unification code does not
lcp@315
   302
  guarantee to find instantiations for type variables automatically.  Be
lcp@315
   303
  prepared to use \ttindex{res_inst_tac} instead of {\tt resolve_tac},
lcp@315
   304
  possibly instantiating type variables.  Setting
lcp@315
   305
  \ttindex{Unify.trace_types} to {\tt true} causes Isabelle to report
lcp@315
   306
  omitted search paths during unification.\index{tracing!of unification}
lcp@315
   307
\end{warn}
lcp@104
   308
lcp@104
   309
lcp@287
   310
\begin{figure}
lcp@104
   311
\begin{ttbox}
lcp@315
   312
\tdx{sym}         s=t ==> t=s
lcp@315
   313
\tdx{trans}       [| r=s; s=t |] ==> r=t
lcp@315
   314
\tdx{ssubst}      [| t=s; P(s) |] ==> P(t::'a)
lcp@315
   315
\tdx{box_equals}  [| a=b;  a=c;  b=d |] ==> c=d  
nipkow@453
   316
\tdx{arg_cong}    x=y ==> f(x)=f(y)
nipkow@453
   317
\tdx{fun_cong}    f=g ==> f(x)=g(x)
lcp@104
   318
\subcaption{Equality}
lcp@104
   319
lcp@315
   320
\tdx{TrueI}       True 
lcp@315
   321
\tdx{FalseE}      False ==> P
lcp@104
   322
lcp@315
   323
\tdx{conjI}       [| P; Q |] ==> P&Q
lcp@315
   324
\tdx{conjunct1}   [| P&Q |] ==> P
lcp@315
   325
\tdx{conjunct2}   [| P&Q |] ==> Q 
lcp@315
   326
\tdx{conjE}       [| P&Q;  [| P; Q |] ==> R |] ==> R
lcp@104
   327
lcp@315
   328
\tdx{disjI1}      P ==> P|Q
lcp@315
   329
\tdx{disjI2}      Q ==> P|Q
lcp@315
   330
\tdx{disjE}       [| P | Q; P ==> R; Q ==> R |] ==> R
lcp@104
   331
lcp@315
   332
\tdx{notI}        (P ==> False) ==> ~ P
lcp@315
   333
\tdx{notE}        [| ~ P;  P |] ==> R
lcp@315
   334
\tdx{impE}        [| P-->Q;  P;  Q ==> R |] ==> R
lcp@104
   335
\subcaption{Propositional logic}
lcp@104
   336
lcp@315
   337
\tdx{iffI}        [| P ==> Q;  Q ==> P |] ==> P=Q
lcp@315
   338
\tdx{iffD1}       [| P=Q; P |] ==> Q
lcp@315
   339
\tdx{iffD2}       [| P=Q; Q |] ==> P
lcp@315
   340
\tdx{iffE}        [| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R
lcp@104
   341
lcp@315
   342
\tdx{eqTrueI}     P ==> P=True 
lcp@315
   343
\tdx{eqTrueE}     P=True ==> P 
lcp@104
   344
\subcaption{Logical equivalence}
lcp@104
   345
lcp@104
   346
\end{ttbox}
nipkow@306
   347
\caption{Derived rules for \HOL} \label{hol-lemmas1}
lcp@104
   348
\end{figure}
lcp@104
   349
lcp@104
   350
lcp@287
   351
\begin{figure}
lcp@287
   352
\begin{ttbox}\makeatother
lcp@315
   353
\tdx{allI}      (!!x::'a. P(x)) ==> !x. P(x)
lcp@315
   354
\tdx{spec}      !x::'a.P(x) ==> P(x)
lcp@315
   355
\tdx{allE}      [| !x.P(x);  P(x) ==> R |] ==> R
lcp@315
   356
\tdx{all_dupE}  [| !x.P(x);  [| P(x); !x.P(x) |] ==> R |] ==> R
lcp@104
   357
lcp@315
   358
\tdx{exI}       P(x) ==> ? x::'a.P(x)
lcp@315
   359
\tdx{exE}       [| ? x::'a.P(x); !!x. P(x) ==> Q |] ==> Q
lcp@104
   360
lcp@315
   361
\tdx{ex1I}      [| P(a);  !!x. P(x) ==> x=a |] ==> ?! x. P(x)
lcp@315
   362
\tdx{ex1E}      [| ?! x.P(x);  !!x. [| P(x);  ! y. P(y) --> y=x |] ==> R 
lcp@104
   363
          |] ==> R
lcp@104
   364
lcp@315
   365
\tdx{select_equality} [| P(a);  !!x. P(x) ==> x=a |] ==> (@x.P(x)) = a
lcp@104
   366
\subcaption{Quantifiers and descriptions}
lcp@104
   367
lcp@315
   368
\tdx{ccontr}          (~P ==> False) ==> P
lcp@315
   369
\tdx{classical}       (~P ==> P) ==> P
lcp@315
   370
\tdx{excluded_middle} ~P | P
lcp@104
   371
lcp@315
   372
\tdx{disjCI}          (~Q ==> P) ==> P|Q
lcp@315
   373
\tdx{exCI}            (! x. ~ P(x) ==> P(a)) ==> ? x.P(x)
lcp@315
   374
\tdx{impCE}           [| P-->Q; ~ P ==> R; Q ==> R |] ==> R
lcp@315
   375
\tdx{iffCE}           [| P=Q;  [| P;Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R
lcp@315
   376
\tdx{notnotD}         ~~P ==> P
lcp@315
   377
\tdx{swap}            ~P ==> (~Q ==> P) ==> Q
lcp@104
   378
\subcaption{Classical logic}
lcp@104
   379
lcp@315
   380
\tdx{if_True}         if(True,x,y) = x
lcp@315
   381
\tdx{if_False}        if(False,x,y) = y
lcp@315
   382
\tdx{if_P}            P ==> if(P,x,y) = x
lcp@315
   383
\tdx{if_not_P}        ~ P ==> if(P,x,y) = y
lcp@315
   384
\tdx{expand_if}       P(if(Q,x,y)) = ((Q --> P(x)) & (~Q --> P(y)))
lcp@104
   385
\subcaption{Conditionals}
lcp@104
   386
\end{ttbox}
lcp@104
   387
\caption{More derived rules} \label{hol-lemmas2}
lcp@104
   388
\end{figure}
lcp@104
   389
lcp@104
   390
lcp@104
   391
Some derived rules are shown in Figures~\ref{hol-lemmas1}
lcp@104
   392
and~\ref{hol-lemmas2}, with their {\ML} names.  These include natural rules
lcp@104
   393
for the logical connectives, as well as sequent-style elimination rules for
lcp@104
   394
conjunctions, implications, and universal quantifiers.  
lcp@104
   395
lcp@315
   396
Note the equality rules: \tdx{ssubst} performs substitution in
lcp@315
   397
backward proofs, while \tdx{box_equals} supports reasoning by
lcp@104
   398
simplifying both sides of an equation.
lcp@104
   399
lcp@104
   400
lcp@104
   401
\begin{figure} 
lcp@104
   402
\begin{center}
lcp@104
   403
\begin{tabular}{rrr} 
lcp@111
   404
  \it name      &\it meta-type  & \it description \\ 
lcp@315
   405
\index{{}@\verb'{}' symbol}
lcp@315
   406
  \verb|{}|     & $\alpha\,set$         & the empty set \\
lcp@315
   407
  \cdx{insert}  & $[\alpha,\alpha\,set]\To \alpha\,set$
lcp@111
   408
        & insertion of element \\
lcp@315
   409
  \cdx{Collect} & $(\alpha\To bool)\To\alpha\,set$
lcp@111
   410
        & comprehension \\
lcp@315
   411
  \cdx{Compl}   & $(\alpha\,set)\To\alpha\,set$
lcp@111
   412
        & complement \\
lcp@315
   413
  \cdx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
lcp@111
   414
        & intersection over a set\\
lcp@315
   415
  \cdx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
lcp@111
   416
        & union over a set\\
lcp@594
   417
  \cdx{Inter} & $(\alpha\,set)set\To\alpha\,set$
lcp@111
   418
        &set of sets intersection \\
lcp@594
   419
  \cdx{Union} & $(\alpha\,set)set\To\alpha\,set$
lcp@111
   420
        &set of sets union \\
lcp@594
   421
  \cdx{Pow}   & $\alpha\,set \To (\alpha\,set)set$
lcp@594
   422
        & powerset \\[1ex]
lcp@315
   423
  \cdx{range}   & $(\alpha\To\beta )\To\beta\,set$
lcp@111
   424
        & range of a function \\[1ex]
lcp@315
   425
  \cdx{Ball}~~\cdx{Bex} & $[\alpha\,set,\alpha\To bool]\To bool$
lcp@111
   426
        & bounded quantifiers \\
lcp@315
   427
  \cdx{mono}    & $(\alpha\,set\To\beta\,set)\To bool$
lcp@111
   428
        & monotonicity \\
lcp@315
   429
  \cdx{inj}~~\cdx{surj}& $(\alpha\To\beta )\To bool$
lcp@111
   430
        & injective/surjective \\
lcp@315
   431
  \cdx{inj_onto}        & $[\alpha\To\beta ,\alpha\,set]\To bool$
lcp@111
   432
        & injective over subset
lcp@104
   433
\end{tabular}
lcp@104
   434
\end{center}
lcp@104
   435
\subcaption{Constants}
lcp@104
   436
lcp@104
   437
\begin{center}
lcp@104
   438
\begin{tabular}{llrrr} 
lcp@315
   439
  \it symbol &\it name     &\it meta-type & \it priority & \it description \\
lcp@315
   440
  \sdx{INT}  & \cdx{INTER1}  & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 & 
lcp@111
   441
        intersection over a type\\
lcp@315
   442
  \sdx{UN}  & \cdx{UNION1}  & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 & 
lcp@111
   443
        union over a type
lcp@104
   444
\end{tabular}
lcp@104
   445
\end{center}
lcp@104
   446
\subcaption{Binders} 
lcp@104
   447
lcp@104
   448
\begin{center}
lcp@315
   449
\index{*"`"` symbol}
lcp@315
   450
\index{*": symbol}
lcp@315
   451
\index{*"<"= symbol}
lcp@104
   452
\begin{tabular}{rrrr} 
lcp@315
   453
  \it symbol    & \it meta-type & \it priority & \it description \\ 
lcp@111
   454
  \tt ``        & $[\alpha\To\beta ,\alpha\,set]\To  (\beta\,set)$
lcp@111
   455
        & Left 90 & image \\
lcp@315
   456
  \sdx{Int}     & $[\alpha\,set,\alpha\,set]\To\alpha\,set$
lcp@111
   457
        & Left 70 & intersection ($\inter$) \\
lcp@315
   458
  \sdx{Un}      & $[\alpha\,set,\alpha\,set]\To\alpha\,set$
lcp@111
   459
        & Left 65 & union ($\union$) \\
lcp@111
   460
  \tt:          & $[\alpha ,\alpha\,set]\To bool$       
lcp@111
   461
        & Left 50 & membership ($\in$) \\
lcp@111
   462
  \tt <=        & $[\alpha\,set,\alpha\,set]\To bool$
lcp@111
   463
        & Left 50 & subset ($\subseteq$) 
lcp@104
   464
\end{tabular}
lcp@104
   465
\end{center}
lcp@104
   466
\subcaption{Infixes}
lcp@315
   467
\caption{Syntax of the theory {\tt Set}} \label{hol-set-syntax}
lcp@104
   468
\end{figure} 
lcp@104
   469
lcp@104
   470
lcp@104
   471
\begin{figure} 
lcp@104
   472
\begin{center} \tt\frenchspacing
lcp@315
   473
\index{*"! symbol}
lcp@104
   474
\begin{tabular}{rrr} 
lcp@111
   475
  \it external          & \it internal  & \it description \\ 
lcp@315
   476
  $a$ \ttilde: $b$      & \ttilde($a$ : $b$)    & \rm non-membership\\
lcp@315
   477
  \{$a@1$, $\ldots$\}  &  insert($a@1$, $\ldots$\{\}) & \rm finite set \\
lcp@111
   478
  \{$x$.$P[x]$\}        &  Collect($\lambda x.P[x]$) &
lcp@104
   479
        \rm comprehension \\
lcp@315
   480
  \sdx{INT} $x$:$A$.$B[x]$      & INTER($A$,$\lambda x.B[x]$) &
lcp@315
   481
        \rm intersection \\
lcp@315
   482
  \sdx{UN}{\tt\ }  $x$:$A$.$B[x]$      & UNION($A$,$\lambda x.B[x]$) &
lcp@315
   483
        \rm union \\
lcp@315
   484
  \tt ! $x$:$A$.$P[x]$ or \sdx{ALL} $x$:$A$.$P[x]$ & 
lcp@315
   485
        Ball($A$,$\lambda x.P[x]$) & 
lcp@111
   486
        \rm bounded $\forall$ \\
lcp@315
   487
  \sdx{?} $x$:$A$.$P[x]$ or \sdx{EX}{\tt\ } $x$:$A$.$P[x]$ & 
lcp@315
   488
        Bex($A$,$\lambda x.P[x]$) & \rm bounded $\exists$
lcp@104
   489
\end{tabular}
lcp@104
   490
\end{center}
lcp@104
   491
\subcaption{Translations}
lcp@104
   492
lcp@104
   493
\dquotes
lcp@315
   494
\[\begin{array}{rclcl}
lcp@104
   495
    term & = & \hbox{other terms\ldots} \\
lcp@111
   496
         & | & "\{\}" \\
lcp@111
   497
         & | & "\{ " term\; ("," term)^* " \}" \\
lcp@111
   498
         & | & "\{ " id " . " formula " \}" \\
lcp@111
   499
         & | & term " `` " term \\
lcp@111
   500
         & | & term " Int " term \\
lcp@111
   501
         & | & term " Un " term \\
lcp@111
   502
         & | & "INT~~"  id ":" term " . " term \\
lcp@111
   503
         & | & "UN~~~"  id ":" term " . " term \\
lcp@111
   504
         & | & "INT~~"  id~id^* " . " term \\
lcp@111
   505
         & | & "UN~~~"  id~id^* " . " term \\[2ex]
lcp@104
   506
 formula & = & \hbox{other formulae\ldots} \\
lcp@111
   507
         & | & term " : " term \\
lcp@111
   508
         & | & term " \ttilde: " term \\
lcp@111
   509
         & | & term " <= " term \\
lcp@315
   510
         & | & "!~" id ":" term " . " formula 
lcp@111
   511
         & | & "ALL " id ":" term " . " formula \\
lcp@315
   512
         & | & "?~" id ":" term " . " formula 
lcp@111
   513
         & | & "EX~~" id ":" term " . " formula
lcp@104
   514
  \end{array}
lcp@104
   515
\]
lcp@104
   516
\subcaption{Full Grammar}
lcp@315
   517
\caption{Syntax of the theory {\tt Set} (continued)} \label{hol-set-syntax2}
lcp@104
   518
\end{figure} 
lcp@104
   519
lcp@104
   520
lcp@104
   521
\section{A formulation of set theory}
lcp@104
   522
Historically, higher-order logic gives a foundation for Russell and
lcp@104
   523
Whitehead's theory of classes.  Let us use modern terminology and call them
lcp@104
   524
{\bf sets}, but note that these sets are distinct from those of {\ZF} set
lcp@104
   525
theory, and behave more like {\ZF} classes.
lcp@104
   526
\begin{itemize}
lcp@104
   527
\item
lcp@104
   528
Sets are given by predicates over some type~$\sigma$.  Types serve to
lcp@104
   529
define universes for sets, but type checking is still significant.
lcp@104
   530
\item
lcp@104
   531
There is a universal set (for each type).  Thus, sets have complements, and
lcp@104
   532
may be defined by absolute comprehension.
lcp@104
   533
\item
lcp@104
   534
Although sets may contain other sets as elements, the containing set must
lcp@104
   535
have a more complex type.
lcp@104
   536
\end{itemize}
nipkow@306
   537
Finite unions and intersections have the same behaviour in \HOL\ as they
nipkow@306
   538
do in~{\ZF}.  In \HOL\ the intersection of the empty set is well-defined,
lcp@104
   539
denoting the universal set for the given type.
lcp@104
   540
lcp@315
   541
lcp@315
   542
\subsection{Syntax of set theory}\index{*set type}
lcp@315
   543
\HOL's set theory is called \thydx{Set}.  The type $\alpha\,set$ is
lcp@315
   544
essentially the same as $\alpha\To bool$.  The new type is defined for
lcp@315
   545
clarity and to avoid complications involving function types in unification.
lcp@315
   546
Since Isabelle does not support type definitions (as mentioned in
lcp@315
   547
\S\ref{HOL-types}), the isomorphisms between the two types are declared
lcp@315
   548
explicitly.  Here they are natural: {\tt Collect} maps $\alpha\To bool$ to
lcp@315
   549
$\alpha\,set$, while \hbox{\tt op :} maps in the other direction (ignoring
lcp@315
   550
argument order).
lcp@104
   551
lcp@104
   552
Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax
lcp@104
   553
translations.  Figure~\ref{hol-set-syntax2} presents the grammar of the new
lcp@104
   554
constructs.  Infix operators include union and intersection ($A\union B$
lcp@104
   555
and $A\inter B$), the subset and membership relations, and the image
lcp@315
   556
operator~{\tt``}\@.  Note that $a$\verb|~:|$b$ is translated to
lcp@315
   557
$\neg(a\in b)$.  
lcp@315
   558
lcp@315
   559
The {\tt\{\ldots\}} notation abbreviates finite sets constructed in the
lcp@315
   560
obvious manner using~{\tt insert} and~$\{\}$:
lcp@104
   561
\begin{eqnarray*}
lcp@315
   562
  \{a@1, \ldots, a@n\}  & \equiv &  
lcp@315
   563
  {\tt insert}(a@1,\ldots,{\tt insert}(a@n,\{\}))
lcp@104
   564
\end{eqnarray*}
lcp@104
   565
lcp@104
   566
The set \hbox{\tt\{$x$.$P[x]$\}} consists of all $x$ (of suitable type)
lcp@104
   567
that satisfy~$P[x]$, where $P[x]$ is a formula that may contain free
lcp@315
   568
occurrences of~$x$.  This syntax expands to \cdx{Collect}$(\lambda
lcp@315
   569
x.P[x])$.  It defines sets by absolute comprehension, which is impossible
lcp@315
   570
in~{\ZF}; the type of~$x$ implicitly restricts the comprehension.
lcp@104
   571
lcp@104
   572
The set theory defines two {\bf bounded quantifiers}:
lcp@104
   573
\begin{eqnarray*}
lcp@315
   574
   \forall x\in A.P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\
lcp@315
   575
   \exists x\in A.P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x]
lcp@104
   576
\end{eqnarray*}
lcp@315
   577
The constants~\cdx{Ball} and~\cdx{Bex} are defined
lcp@104
   578
accordingly.  Instead of {\tt Ball($A$,$P$)} and {\tt Bex($A$,$P$)} we may
lcp@315
   579
write\index{*"! symbol}\index{*"? symbol}
lcp@315
   580
\index{*ALL symbol}\index{*EX symbol} 
lcp@315
   581
%
lcp@315
   582
\hbox{\tt !~$x$:$A$.$P[x]$} and \hbox{\tt ?~$x$:$A$.$P[x]$}.  Isabelle's
lcp@315
   583
usual quantifier symbols, \sdx{ALL} and \sdx{EX}, are also accepted
lcp@315
   584
for input.  As with the primitive quantifiers, the {\ML} reference
lcp@315
   585
\ttindex{HOL_quantifiers} specifies which notation to use for output.
lcp@104
   586
lcp@104
   587
Unions and intersections over sets, namely $\bigcup@{x\in A}B[x]$ and
lcp@104
   588
$\bigcap@{x\in A}B[x]$, are written 
lcp@315
   589
\sdx{UN}~\hbox{\tt$x$:$A$.$B[x]$} and
lcp@315
   590
\sdx{INT}~\hbox{\tt$x$:$A$.$B[x]$}.  
lcp@315
   591
lcp@315
   592
Unions and intersections over types, namely $\bigcup@x B[x]$ and $\bigcap@x
lcp@315
   593
B[x]$, are written \sdx{UN}~\hbox{\tt$x$.$B[x]$} and
lcp@315
   594
\sdx{INT}~\hbox{\tt$x$.$B[x]$}.  They are equivalent to the previous
lcp@315
   595
union and intersection operators when $A$ is the universal set.
lcp@315
   596
lcp@315
   597
The operators $\bigcup A$ and $\bigcap A$ act upon sets of sets.  They are
lcp@315
   598
not binders, but are equal to $\bigcup@{x\in A}x$ and $\bigcap@{x\in A}x$,
lcp@315
   599
respectively.
lcp@315
   600
lcp@315
   601
lcp@315
   602
\begin{figure} \underscoreon
lcp@315
   603
\begin{ttbox}
lcp@315
   604
\tdx{mem_Collect_eq}    (a : \{x.P(x)\}) = P(a)
lcp@315
   605
\tdx{Collect_mem_eq}    \{x.x:A\} = A
lcp@104
   606
wenzelm@841
   607
\tdx{empty_def}         \{\}          == \{x.False\}
lcp@315
   608
\tdx{insert_def}        insert(a,B) == \{x.x=a\} Un B
lcp@315
   609
\tdx{Ball_def}          Ball(A,P)   == ! x. x:A --> P(x)
lcp@315
   610
\tdx{Bex_def}           Bex(A,P)    == ? x. x:A & P(x)
lcp@315
   611
\tdx{subset_def}        A <= B      == ! x:A. x:B
lcp@315
   612
\tdx{Un_def}            A Un B      == \{x.x:A | x:B\}
lcp@315
   613
\tdx{Int_def}           A Int B     == \{x.x:A & x:B\}
lcp@315
   614
\tdx{set_diff_def}      A - B       == \{x.x:A & x~:B\}
lcp@315
   615
\tdx{Compl_def}         Compl(A)    == \{x. ~ x:A\}
lcp@315
   616
\tdx{INTER_def}         INTER(A,B)  == \{y. ! x:A. y: B(x)\}
lcp@315
   617
\tdx{UNION_def}         UNION(A,B)  == \{y. ? x:A. y: B(x)\}
lcp@315
   618
\tdx{INTER1_def}        INTER1(B)   == INTER(\{x.True\}, B)
lcp@315
   619
\tdx{UNION1_def}        UNION1(B)   == UNION(\{x.True\}, B)
lcp@315
   620
\tdx{Inter_def}         Inter(S)    == (INT x:S. x)
lcp@594
   621
\tdx{Union_def}         Union(S)    == (UN  x:S. x)
lcp@594
   622
\tdx{Pow_def}           Pow(A)      == \{B. B <= A\}
lcp@315
   623
\tdx{image_def}         f``A        == \{y. ? x:A. y=f(x)\}
lcp@315
   624
\tdx{range_def}         range(f)    == \{y. ? x. y=f(x)\}
lcp@315
   625
\tdx{mono_def}          mono(f)     == !A B. A <= B --> f(A) <= f(B)
lcp@315
   626
\tdx{inj_def}           inj(f)      == ! x y. f(x)=f(y) --> x=y
lcp@315
   627
\tdx{surj_def}          surj(f)     == ! y. ? x. y=f(x)
lcp@315
   628
\tdx{inj_onto_def}      inj_onto(f,A) == !x:A. !y:A. f(x)=f(y) --> x=y
lcp@315
   629
\end{ttbox}
lcp@315
   630
\caption{Rules of the theory {\tt Set}} \label{hol-set-rules}
lcp@315
   631
\end{figure}
lcp@315
   632
lcp@104
   633
lcp@315
   634
\begin{figure} \underscoreon
lcp@315
   635
\begin{ttbox}
lcp@315
   636
\tdx{CollectI}        [| P(a) |] ==> a : \{x.P(x)\}
lcp@315
   637
\tdx{CollectD}        [| a : \{x.P(x)\} |] ==> P(a)
lcp@315
   638
\tdx{CollectE}        [| a : \{x.P(x)\};  P(a) ==> W |] ==> W
lcp@315
   639
lcp@315
   640
\tdx{ballI}           [| !!x. x:A ==> P(x) |] ==> ! x:A. P(x)
lcp@315
   641
\tdx{bspec}           [| ! x:A. P(x);  x:A |] ==> P(x)
lcp@315
   642
\tdx{ballE}           [| ! x:A. P(x);  P(x) ==> Q;  ~ x:A ==> Q |] ==> Q
lcp@315
   643
lcp@315
   644
\tdx{bexI}            [| P(x);  x:A |] ==> ? x:A. P(x)
lcp@315
   645
\tdx{bexCI}           [| ! x:A. ~ P(x) ==> P(a);  a:A |] ==> ? x:A.P(x)
lcp@315
   646
\tdx{bexE}            [| ? x:A. P(x);  !!x. [| x:A; P(x) |] ==> Q  |] ==> Q
lcp@315
   647
\subcaption{Comprehension and Bounded quantifiers}
lcp@315
   648
lcp@315
   649
\tdx{subsetI}         (!!x.x:A ==> x:B) ==> A <= B
lcp@315
   650
\tdx{subsetD}         [| A <= B;  c:A |] ==> c:B
lcp@315
   651
\tdx{subsetCE}        [| A <= B;  ~ (c:A) ==> P;  c:B ==> P |] ==> P
lcp@315
   652
lcp@315
   653
\tdx{subset_refl}     A <= A
lcp@315
   654
\tdx{subset_trans}    [| A<=B;  B<=C |] ==> A<=C
lcp@315
   655
lcp@471
   656
\tdx{equalityI}       [| A <= B;  B <= A |] ==> A = B
lcp@315
   657
\tdx{equalityD1}      A = B ==> A<=B
lcp@315
   658
\tdx{equalityD2}      A = B ==> B<=A
lcp@315
   659
\tdx{equalityE}       [| A = B;  [| A<=B; B<=A |] ==> P |]  ==>  P
lcp@315
   660
lcp@315
   661
\tdx{equalityCE}      [| A = B;  [| c:A; c:B |] ==> P;  
lcp@315
   662
                           [| ~ c:A; ~ c:B |] ==> P 
lcp@315
   663
                |]  ==>  P
lcp@315
   664
\subcaption{The subset and equality relations}
lcp@315
   665
\end{ttbox}
lcp@315
   666
\caption{Derived rules for set theory} \label{hol-set1}
lcp@315
   667
\end{figure}
lcp@315
   668
lcp@104
   669
lcp@287
   670
\begin{figure} \underscoreon
lcp@104
   671
\begin{ttbox}
lcp@315
   672
\tdx{emptyE}   a : \{\} ==> P
lcp@315
   673
lcp@315
   674
\tdx{insertI1} a : insert(a,B)
lcp@315
   675
\tdx{insertI2} a : B ==> a : insert(b,B)
lcp@315
   676
\tdx{insertE}  [| a : insert(b,A);  a=b ==> P;  a:A ==> P |] ==> P
lcp@104
   677
lcp@315
   678
\tdx{ComplI}   [| c:A ==> False |] ==> c : Compl(A)
lcp@315
   679
\tdx{ComplD}   [| c : Compl(A) |] ==> ~ c:A
lcp@315
   680
lcp@315
   681
\tdx{UnI1}     c:A ==> c : A Un B
lcp@315
   682
\tdx{UnI2}     c:B ==> c : A Un B
lcp@315
   683
\tdx{UnCI}     (~c:B ==> c:A) ==> c : A Un B
lcp@315
   684
\tdx{UnE}      [| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P
lcp@104
   685
lcp@315
   686
\tdx{IntI}     [| c:A;  c:B |] ==> c : A Int B
lcp@315
   687
\tdx{IntD1}    c : A Int B ==> c:A
lcp@315
   688
\tdx{IntD2}    c : A Int B ==> c:B
lcp@315
   689
\tdx{IntE}     [| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P
lcp@315
   690
lcp@315
   691
\tdx{UN_I}     [| a:A;  b: B(a) |] ==> b: (UN x:A. B(x))
lcp@315
   692
\tdx{UN_E}     [| b: (UN x:A. B(x));  !!x.[| x:A;  b:B(x) |] ==> R |] ==> R
lcp@104
   693
lcp@315
   694
\tdx{INT_I}    (!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))
lcp@315
   695
\tdx{INT_D}    [| b: (INT x:A. B(x));  a:A |] ==> b: B(a)
lcp@315
   696
\tdx{INT_E}    [| b: (INT x:A. B(x));  b: B(a) ==> R;  ~ a:A ==> R |] ==> R
lcp@315
   697
lcp@315
   698
\tdx{UnionI}   [| X:C;  A:X |] ==> A : Union(C)
lcp@315
   699
\tdx{UnionE}   [| A : Union(C);  !!X.[| A:X;  X:C |] ==> R |] ==> R
lcp@315
   700
lcp@315
   701
\tdx{InterI}   [| !!X. X:C ==> A:X |] ==> A : Inter(C)
lcp@315
   702
\tdx{InterD}   [| A : Inter(C);  X:C |] ==> A:X
lcp@315
   703
\tdx{InterE}   [| A : Inter(C);  A:X ==> R;  ~ X:C ==> R |] ==> R
lcp@594
   704
lcp@594
   705
\tdx{PowI}     A<=B ==> A: Pow(B)
lcp@594
   706
\tdx{PowD}     A: Pow(B) ==> A<=B
lcp@315
   707
\end{ttbox}
lcp@315
   708
\caption{Further derived rules for set theory} \label{hol-set2}
lcp@315
   709
\end{figure}
lcp@315
   710
lcp@104
   711
lcp@315
   712
\subsection{Axioms and rules of set theory}
lcp@315
   713
Figure~\ref{hol-set-rules} presents the rules of theory \thydx{Set}.  The
lcp@315
   714
axioms \tdx{mem_Collect_eq} and \tdx{Collect_mem_eq} assert
lcp@315
   715
that the functions {\tt Collect} and \hbox{\tt op :} are isomorphisms.  Of
lcp@315
   716
course, \hbox{\tt op :} also serves as the membership relation.
lcp@104
   717
lcp@315
   718
All the other axioms are definitions.  They include the empty set, bounded
lcp@315
   719
quantifiers, unions, intersections, complements and the subset relation.
lcp@315
   720
They also include straightforward properties of functions: image~({\tt``}) and
lcp@315
   721
{\tt range}, and predicates concerning monotonicity, injectiveness and
lcp@315
   722
surjectiveness.  
lcp@315
   723
lcp@315
   724
The predicate \cdx{inj_onto} is used for simulating type definitions.
lcp@315
   725
The statement ${\tt inj_onto}(f,A)$ asserts that $f$ is injective on the
lcp@315
   726
set~$A$, which specifies a subset of its domain type.  In a type
lcp@315
   727
definition, $f$ is the abstraction function and $A$ is the set of valid
lcp@315
   728
representations; we should not expect $f$ to be injective outside of~$A$.
lcp@315
   729
lcp@315
   730
\begin{figure} \underscoreon
lcp@315
   731
\begin{ttbox}
lcp@315
   732
\tdx{Inv_f_f}    inj(f) ==> Inv(f,f(x)) = x
lcp@315
   733
\tdx{f_Inv_f}    y : range(f) ==> f(Inv(f,y)) = y
lcp@104
   734
lcp@315
   735
%\tdx{Inv_injective}
lcp@315
   736
%    [| Inv(f,x)=Inv(f,y); x: range(f);  y: range(f) |] ==> x=y
lcp@315
   737
%
lcp@315
   738
\tdx{imageI}     [| x:A |] ==> f(x) : f``A
lcp@315
   739
\tdx{imageE}     [| b : f``A;  !!x.[| b=f(x);  x:A |] ==> P |] ==> P
lcp@315
   740
lcp@315
   741
\tdx{rangeI}     f(x) : range(f)
lcp@315
   742
\tdx{rangeE}     [| b : range(f);  !!x.[| b=f(x) |] ==> P |] ==> P
lcp@104
   743
lcp@315
   744
\tdx{monoI}      [| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)
lcp@315
   745
\tdx{monoD}      [| mono(f);  A <= B |] ==> f(A) <= f(B)
lcp@315
   746
lcp@315
   747
\tdx{injI}       [| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)
lcp@315
   748
\tdx{inj_inverseI}              (!!x. g(f(x)) = x) ==> inj(f)
lcp@315
   749
\tdx{injD}       [| inj(f); f(x) = f(y) |] ==> x=y
lcp@315
   750
lcp@315
   751
\tdx{inj_ontoI}  (!!x y. [| f(x)=f(y); x:A; y:A |] ==> x=y) ==> inj_onto(f,A)
lcp@315
   752
\tdx{inj_ontoD}  [| inj_onto(f,A);  f(x)=f(y);  x:A;  y:A |] ==> x=y
lcp@315
   753
lcp@315
   754
\tdx{inj_onto_inverseI}
lcp@104
   755
    (!!x. x:A ==> g(f(x)) = x) ==> inj_onto(f,A)
lcp@315
   756
\tdx{inj_onto_contraD}
lcp@104
   757
    [| inj_onto(f,A);  x~=y;  x:A;  y:A |] ==> ~ f(x)=f(y)
lcp@104
   758
\end{ttbox}
lcp@104
   759
\caption{Derived rules involving functions} \label{hol-fun}
lcp@104
   760
\end{figure}
lcp@104
   761
lcp@104
   762
lcp@287
   763
\begin{figure} \underscoreon
lcp@104
   764
\begin{ttbox}
lcp@315
   765
\tdx{Union_upper}     B:A ==> B <= Union(A)
lcp@315
   766
\tdx{Union_least}     [| !!X. X:A ==> X<=C |] ==> Union(A) <= C
lcp@104
   767
lcp@315
   768
\tdx{Inter_lower}     B:A ==> Inter(A) <= B
lcp@315
   769
\tdx{Inter_greatest}  [| !!X. X:A ==> C<=X |] ==> C <= Inter(A)
lcp@104
   770
lcp@315
   771
\tdx{Un_upper1}       A <= A Un B
lcp@315
   772
\tdx{Un_upper2}       B <= A Un B
lcp@315
   773
\tdx{Un_least}        [| A<=C;  B<=C |] ==> A Un B <= C
lcp@104
   774
lcp@315
   775
\tdx{Int_lower1}      A Int B <= A
lcp@315
   776
\tdx{Int_lower2}      A Int B <= B
lcp@315
   777
\tdx{Int_greatest}    [| C<=A;  C<=B |] ==> C <= A Int B
lcp@104
   778
\end{ttbox}
lcp@104
   779
\caption{Derived rules involving subsets} \label{hol-subset}
lcp@104
   780
\end{figure}
lcp@104
   781
lcp@104
   782
lcp@315
   783
\begin{figure} \underscoreon   \hfuzz=4pt%suppress "Overfull \hbox" message
lcp@104
   784
\begin{ttbox}
lcp@315
   785
\tdx{Int_absorb}        A Int A = A
lcp@315
   786
\tdx{Int_commute}       A Int B = B Int A
lcp@315
   787
\tdx{Int_assoc}         (A Int B) Int C  =  A Int (B Int C)
lcp@315
   788
\tdx{Int_Un_distrib}    (A Un B)  Int C  =  (A Int C) Un (B Int C)
lcp@104
   789
lcp@315
   790
\tdx{Un_absorb}         A Un A = A
lcp@315
   791
\tdx{Un_commute}        A Un B = B Un A
lcp@315
   792
\tdx{Un_assoc}          (A Un B)  Un C  =  A Un (B Un C)
lcp@315
   793
\tdx{Un_Int_distrib}    (A Int B) Un C  =  (A Un C) Int (B Un C)
lcp@104
   794
lcp@315
   795
\tdx{Compl_disjoint}    A Int Compl(A) = \{x.False\}
lcp@315
   796
\tdx{Compl_partition}   A Un  Compl(A) = \{x.True\}
lcp@315
   797
\tdx{double_complement} Compl(Compl(A)) = A
lcp@315
   798
\tdx{Compl_Un}          Compl(A Un B)  = Compl(A) Int Compl(B)
lcp@315
   799
\tdx{Compl_Int}         Compl(A Int B) = Compl(A) Un Compl(B)
lcp@104
   800
lcp@315
   801
\tdx{Union_Un_distrib}  Union(A Un B) = Union(A) Un Union(B)
lcp@315
   802
\tdx{Int_Union}         A Int Union(B) = (UN C:B. A Int C)
lcp@315
   803
\tdx{Un_Union_image}    (UN x:C. A(x) Un B(x)) = Union(A``C) Un Union(B``C)
lcp@104
   804
lcp@315
   805
\tdx{Inter_Un_distrib}  Inter(A Un B) = Inter(A) Int Inter(B)
lcp@315
   806
\tdx{Un_Inter}          A Un Inter(B) = (INT C:B. A Un C)
lcp@315
   807
\tdx{Int_Inter_image}   (INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)
lcp@104
   808
\end{ttbox}
lcp@104
   809
\caption{Set equalities} \label{hol-equalities}
lcp@104
   810
\end{figure}
lcp@104
   811
lcp@104
   812
lcp@315
   813
Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules.  Most are
lcp@315
   814
obvious and resemble rules of Isabelle's {\ZF} set theory.  Certain rules,
lcp@315
   815
such as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI},
lcp@315
   816
are designed for classical reasoning; the rules \tdx{subsetD},
lcp@315
   817
\tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are not
lcp@315
   818
strictly necessary but yield more natural proofs.  Similarly,
lcp@315
   819
\tdx{equalityCE} supports classical reasoning about extensionality,
lcp@344
   820
after the fashion of \tdx{iffCE}.  See the file {\tt HOL/Set.ML} for
lcp@315
   821
proofs pertaining to set theory.
lcp@104
   822
lcp@315
   823
Figure~\ref{hol-fun} presents derived inference rules involving functions.
lcp@315
   824
They also include rules for \cdx{Inv}, which is defined in theory~{\tt
lcp@315
   825
  HOL}; note that ${\tt Inv}(f)$ applies the Axiom of Choice to yield an
lcp@315
   826
inverse of~$f$.  They also include natural deduction rules for the image
lcp@315
   827
and range operators, and for the predicates {\tt inj} and {\tt inj_onto}.
lcp@315
   828
Reasoning about function composition (the operator~\sdx{o}) and the
lcp@315
   829
predicate~\cdx{surj} is done simply by expanding the definitions.  See
lcp@315
   830
the file {\tt HOL/fun.ML} for a complete listing of the derived rules.
lcp@104
   831
lcp@104
   832
Figure~\ref{hol-subset} presents lattice properties of the subset relation.
lcp@315
   833
Unions form least upper bounds; non-empty intersections form greatest lower
lcp@315
   834
bounds.  Reasoning directly about subsets often yields clearer proofs than
lcp@315
   835
reasoning about the membership relation.  See the file {\tt HOL/subset.ML}.
lcp@104
   836
lcp@315
   837
Figure~\ref{hol-equalities} presents many common set equalities.  They
lcp@315
   838
include commutative, associative and distributive laws involving unions,
lcp@315
   839
intersections and complements.  The proofs are mostly trivial, using the
lcp@315
   840
classical reasoner; see file {\tt HOL/equalities.ML}.
lcp@104
   841
lcp@104
   842
lcp@287
   843
\begin{figure}
lcp@315
   844
\begin{constants}
lcp@344
   845
  \it symbol    & \it meta-type &           & \it description \\ 
lcp@315
   846
  \cdx{Pair}    & $[\alpha,\beta]\To \alpha\times\beta$
lcp@315
   847
        & & ordered pairs $\langle a,b\rangle$ \\
lcp@315
   848
  \cdx{fst}     & $\alpha\times\beta \To \alpha$        & & first projection\\
lcp@315
   849
  \cdx{snd}     & $\alpha\times\beta \To \beta$         & & second projection\\
lcp@705
   850
  \cdx{split}   & $[[\alpha,\beta]\To\gamma, \alpha\times\beta] \To \gamma$ 
lcp@315
   851
        & & generalized projection\\
lcp@315
   852
  \cdx{Sigma}  & 
lcp@287
   853
        $[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ &
lcp@315
   854
        & general sum of sets
lcp@315
   855
\end{constants}
lcp@287
   856
\begin{ttbox}\makeatletter
lcp@315
   857
\tdx{fst_def}      fst(p)     == @a. ? b. p = <a,b>
lcp@315
   858
\tdx{snd_def}      snd(p)     == @b. ? a. p = <a,b>
lcp@705
   859
\tdx{split_def}    split(c,p) == c(fst(p),snd(p))
lcp@315
   860
\tdx{Sigma_def}    Sigma(A,B) == UN x:A. UN y:B(x). \{<x,y>\}
lcp@104
   861
lcp@104
   862
lcp@315
   863
\tdx{Pair_inject}  [| <a, b> = <a',b'>;  [| a=a';  b=b' |] ==> R |] ==> R
lcp@349
   864
\tdx{fst_conv}     fst(<a,b>) = a
lcp@349
   865
\tdx{snd_conv}     snd(<a,b>) = b
lcp@705
   866
\tdx{split}        split(c, <a,b>) = c(a,b)
lcp@104
   867
lcp@315
   868
\tdx{surjective_pairing}  p = <fst(p),snd(p)>
lcp@287
   869
lcp@315
   870
\tdx{SigmaI}       [| a:A;  b:B(a) |] ==> <a,b> : Sigma(A,B)
lcp@287
   871
lcp@315
   872
\tdx{SigmaE}       [| c: Sigma(A,B);  
lcp@287
   873
                !!x y.[| x:A; y:B(x); c=<x,y> |] ==> P |] ==> P
lcp@104
   874
\end{ttbox}
lcp@315
   875
\caption{Type $\alpha\times\beta$}\label{hol-prod}
lcp@104
   876
\end{figure} 
lcp@104
   877
lcp@104
   878
lcp@287
   879
\begin{figure}
lcp@315
   880
\begin{constants}
lcp@344
   881
  \it symbol    & \it meta-type &           & \it description \\ 
lcp@315
   882
  \cdx{Inl}     & $\alpha \To \alpha+\beta$    & & first injection\\
lcp@315
   883
  \cdx{Inr}     & $\beta \To \alpha+\beta$     & & second injection\\
lcp@705
   884
  \cdx{sum_case} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$
lcp@315
   885
        & & conditional
lcp@315
   886
\end{constants}
lcp@315
   887
\begin{ttbox}\makeatletter
lcp@705
   888
\tdx{sum_case_def}   sum_case == (\%f g p. @z. (!x. p=Inl(x) --> z=f(x)) &
lcp@315
   889
                                        (!y. p=Inr(y) --> z=g(y)))
lcp@104
   890
lcp@315
   891
\tdx{Inl_not_Inr}    ~ Inl(a)=Inr(b)
lcp@104
   892
lcp@315
   893
\tdx{inj_Inl}        inj(Inl)
lcp@315
   894
\tdx{inj_Inr}        inj(Inr)
lcp@104
   895
lcp@315
   896
\tdx{sumE}           [| !!x::'a. P(Inl(x));  !!y::'b. P(Inr(y)) |] ==> P(s)
lcp@104
   897
lcp@705
   898
\tdx{sum_case_Inl}   sum_case(f, g, Inl(x)) = f(x)
lcp@705
   899
\tdx{sum_case_Inr}   sum_case(f, g, Inr(x)) = g(x)
lcp@104
   900
lcp@705
   901
\tdx{surjective_sum} sum_case(\%x::'a. f(Inl(x)), \%y::'b. f(Inr(y)), s) = f(s)
lcp@104
   902
\end{ttbox}
lcp@315
   903
\caption{Type $\alpha+\beta$}\label{hol-sum}
lcp@104
   904
\end{figure}
lcp@104
   905
lcp@104
   906
lcp@344
   907
\section{Generic packages and classical reasoning}
lcp@344
   908
\HOL\ instantiates most of Isabelle's generic packages;
lcp@344
   909
see {\tt HOL/ROOT.ML} for details.
lcp@344
   910
\begin{itemize}
lcp@344
   911
\item 
lcp@344
   912
Because it includes a general substitution rule, \HOL\ instantiates the
lcp@344
   913
tactic {\tt hyp_subst_tac}, which substitutes for an equality
lcp@344
   914
throughout a subgoal and its hypotheses.
lcp@344
   915
\item 
lcp@344
   916
It instantiates the simplifier, defining~\ttindexbold{HOL_ss} as the
lcp@344
   917
simplification set for higher-order logic.  Equality~($=$), which also
lcp@344
   918
expresses logical equivalence, may be used for rewriting.  See the file
lcp@344
   919
{\tt HOL/simpdata.ML} for a complete listing of the simplification
lcp@344
   920
rules. 
lcp@344
   921
\item 
lcp@344
   922
It instantiates the classical reasoner, as described below. 
lcp@344
   923
\end{itemize}
lcp@344
   924
\HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as
lcp@344
   925
well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
lcp@344
   926
rule; recall Fig.\ts\ref{hol-lemmas2} above.
lcp@344
   927
lcp@344
   928
The classical reasoner is set up as the structure
lcp@344
   929
{\tt Classical}.  This structure is open, so {\ML} identifiers such
lcp@344
   930
as {\tt step_tac}, {\tt fast_tac}, {\tt best_tac}, etc., refer to it.
lcp@344
   931
\HOL\ defines the following classical rule sets:
lcp@344
   932
\begin{ttbox} 
lcp@344
   933
prop_cs    : claset
lcp@344
   934
HOL_cs     : claset
lcp@344
   935
set_cs     : claset
lcp@344
   936
\end{ttbox}
lcp@344
   937
\begin{ttdescription}
lcp@344
   938
\item[\ttindexbold{prop_cs}] contains the propositional rules, namely
lcp@344
   939
those for~$\top$, $\bot$, $\conj$, $\disj$, $\neg$, $\imp$ and~$\bimp$,
lcp@344
   940
along with the rule~{\tt refl}.
lcp@344
   941
lcp@344
   942
\item[\ttindexbold{HOL_cs}] extends {\tt prop_cs} with the safe rules
lcp@344
   943
  {\tt allI} and~{\tt exE} and the unsafe rules {\tt allE}
lcp@344
   944
  and~{\tt exI}, as well as rules for unique existence.  Search using
lcp@344
   945
  this classical set is incomplete: quantified formulae are used at most
lcp@344
   946
  once.
lcp@344
   947
lcp@344
   948
\item[\ttindexbold{set_cs}] extends {\tt HOL_cs} with rules for the bounded
lcp@344
   949
  quantifiers, subsets, comprehensions, unions and intersections,
lcp@344
   950
  complements, finite sets, images and ranges.
lcp@344
   951
\end{ttdescription}
lcp@344
   952
\noindent
lcp@344
   953
See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
lcp@344
   954
        {Chap.\ts\ref{chap:classical}} 
lcp@344
   955
for more discussion of classical proof methods.
lcp@344
   956
lcp@344
   957
lcp@104
   958
\section{Types}
lcp@104
   959
The basic higher-order logic is augmented with a tremendous amount of
lcp@315
   960
material, including support for recursive function and type definitions.  A
lcp@315
   961
detailed discussion appears elsewhere~\cite{paulson-coind}.  The simpler
lcp@315
   962
definitions are the same as those used the {\sc hol} system, but my
lcp@315
   963
treatment of recursive types differs from Melham's~\cite{melham89}.  The
lcp@315
   964
present section describes product, sum, natural number and list types.
lcp@104
   965
lcp@315
   966
\subsection{Product and sum types}\index{*"* type}\index{*"+ type}
lcp@315
   967
Theory \thydx{Prod} defines the product type $\alpha\times\beta$, with
lcp@315
   968
the ordered pair syntax {\tt<$a$,$b$>}.  Theory \thydx{Sum} defines the
lcp@315
   969
sum type $\alpha+\beta$.  These use fairly standard constructions; see
lcp@315
   970
Figs.\ts\ref{hol-prod} and~\ref{hol-sum}.  Because Isabelle does not
lcp@315
   971
support abstract type definitions, the isomorphisms between these types and
lcp@315
   972
their representations are made explicitly.
lcp@104
   973
lcp@104
   974
Most of the definitions are suppressed, but observe that the projections
lcp@104
   975
and conditionals are defined as descriptions.  Their properties are easily
lcp@344
   976
proved using \tdx{select_equality}.  
lcp@104
   977
lcp@287
   978
\begin{figure} 
lcp@315
   979
\index{*"< symbol}
lcp@315
   980
\index{*"* symbol}
lcp@344
   981
\index{*div symbol}
lcp@344
   982
\index{*mod symbol}
lcp@315
   983
\index{*"+ symbol}
lcp@315
   984
\index{*"- symbol}
lcp@315
   985
\begin{constants}
lcp@315
   986
  \it symbol    & \it meta-type & \it priority & \it description \\ 
lcp@315
   987
  \cdx{0}       & $nat$         & & zero \\
lcp@315
   988
  \cdx{Suc}     & $nat \To nat$ & & successor function\\
lcp@705
   989
  \cdx{nat_case} & $[\alpha, nat\To\alpha, nat] \To\alpha$
lcp@315
   990
        & & conditional\\
lcp@315
   991
  \cdx{nat_rec} & $[nat, \alpha, [nat, \alpha]\To\alpha] \To \alpha$
lcp@315
   992
        & & primitive recursor\\
lcp@315
   993
  \cdx{pred_nat} & $(nat\times nat) set$ & & predecessor relation\\
lcp@111
   994
  \tt *         & $[nat,nat]\To nat$    &  Left 70      & multiplication \\
lcp@344
   995
  \tt div       & $[nat,nat]\To nat$    &  Left 70      & division\\
lcp@344
   996
  \tt mod       & $[nat,nat]\To nat$    &  Left 70      & modulus\\
lcp@111
   997
  \tt +         & $[nat,nat]\To nat$    &  Left 65      & addition\\
lcp@111
   998
  \tt -         & $[nat,nat]\To nat$    &  Left 65      & subtraction
lcp@315
   999
\end{constants}
lcp@104
  1000
\subcaption{Constants and infixes}
lcp@104
  1001
lcp@287
  1002
\begin{ttbox}\makeatother
lcp@705
  1003
\tdx{nat_case_def}  nat_case == (\%a f n. @z. (n=0 --> z=a) & 
lcp@344
  1004
                                       (!x. n=Suc(x) --> z=f(x)))
lcp@315
  1005
\tdx{pred_nat_def}  pred_nat == \{p. ? n. p = <n, Suc(n)>\} 
lcp@315
  1006
\tdx{less_def}      m<n      == <m,n>:pred_nat^+
lcp@315
  1007
\tdx{nat_rec_def}   nat_rec(n,c,d) == 
lcp@705
  1008
               wfrec(pred_nat, n, nat_case(\%g.c, \%m g. d(m,g(m))))
lcp@104
  1009
lcp@344
  1010
\tdx{add_def}   m+n     == nat_rec(m, n, \%u v.Suc(v))
lcp@344
  1011
\tdx{diff_def}  m-n     == nat_rec(n, m, \%u v. nat_rec(v, 0, \%x y.x))
lcp@344
  1012
\tdx{mult_def}  m*n     == nat_rec(m, 0, \%u v. n + v)
lcp@344
  1013
\tdx{mod_def}   m mod n == wfrec(trancl(pred_nat), m, \%j f. if(j<n,j,f(j-n)))
lcp@344
  1014
\tdx{quo_def}   m div n == wfrec(trancl(pred_nat), 
lcp@287
  1015
                        m, \%j f. if(j<n,0,Suc(f(j-n))))
lcp@104
  1016
\subcaption{Definitions}
lcp@104
  1017
\end{ttbox}
lcp@315
  1018
\caption{Defining {\tt nat}, the type of natural numbers} \label{hol-nat1}
lcp@104
  1019
\end{figure}
lcp@104
  1020
lcp@104
  1021
lcp@287
  1022
\begin{figure} \underscoreon
lcp@104
  1023
\begin{ttbox}
lcp@315
  1024
\tdx{nat_induct}     [| P(0); !!k. [| P(k) |] ==> P(Suc(k)) |]  ==> P(n)
lcp@104
  1025
lcp@315
  1026
\tdx{Suc_not_Zero}   Suc(m) ~= 0
lcp@315
  1027
\tdx{inj_Suc}        inj(Suc)
lcp@315
  1028
\tdx{n_not_Suc_n}    n~=Suc(n)
lcp@104
  1029
\subcaption{Basic properties}
lcp@104
  1030
lcp@315
  1031
\tdx{pred_natI}      <n, Suc(n)> : pred_nat
lcp@315
  1032
\tdx{pred_natE}
lcp@104
  1033
    [| p : pred_nat;  !!x n. [| p = <n, Suc(n)> |] ==> R |] ==> R
lcp@104
  1034
lcp@705
  1035
\tdx{nat_case_0}     nat_case(a, f, 0) = a
lcp@705
  1036
\tdx{nat_case_Suc}   nat_case(a, f, Suc(k)) = f(k)
lcp@104
  1037
lcp@315
  1038
\tdx{wf_pred_nat}    wf(pred_nat)
lcp@315
  1039
\tdx{nat_rec_0}      nat_rec(0,c,h) = c
lcp@315
  1040
\tdx{nat_rec_Suc}    nat_rec(Suc(n), c, h) = h(n, nat_rec(n,c,h))
lcp@104
  1041
\subcaption{Case analysis and primitive recursion}
lcp@104
  1042
lcp@315
  1043
\tdx{less_trans}     [| i<j;  j<k |] ==> i<k
lcp@315
  1044
\tdx{lessI}          n < Suc(n)
lcp@315
  1045
\tdx{zero_less_Suc}  0 < Suc(n)
lcp@104
  1046
lcp@315
  1047
\tdx{less_not_sym}   n<m --> ~ m<n 
lcp@315
  1048
\tdx{less_not_refl}  ~ n<n
lcp@315
  1049
\tdx{not_less0}      ~ n<0
lcp@104
  1050
lcp@315
  1051
\tdx{Suc_less_eq}    (Suc(m) < Suc(n)) = (m<n)
lcp@315
  1052
\tdx{less_induct}    [| !!n. [| ! m. m<n --> P(m) |] ==> P(n) |]  ==>  P(n)
lcp@104
  1053
lcp@315
  1054
\tdx{less_linear}    m<n | m=n | n<m
lcp@104
  1055
\subcaption{The less-than relation}
lcp@104
  1056
\end{ttbox}
lcp@344
  1057
\caption{Derived rules for {\tt nat}} \label{hol-nat2}
lcp@104
  1058
\end{figure}
lcp@104
  1059
lcp@104
  1060
lcp@315
  1061
\subsection{The type of natural numbers, {\tt nat}}
lcp@315
  1062
The theory \thydx{Nat} defines the natural numbers in a roundabout but
lcp@315
  1063
traditional way.  The axiom of infinity postulates an type~\tydx{ind} of
lcp@315
  1064
individuals, which is non-empty and closed under an injective operation.
lcp@315
  1065
The natural numbers are inductively generated by choosing an arbitrary
lcp@315
  1066
individual for~0 and using the injective operation to take successors.  As
lcp@344
  1067
usual, the isomorphisms between~\tydx{nat} and its representation are made
lcp@315
  1068
explicitly.
lcp@104
  1069
lcp@315
  1070
The definition makes use of a least fixed point operator \cdx{lfp},
lcp@315
  1071
defined using the Knaster-Tarski theorem.  This is used to define the
lcp@315
  1072
operator \cdx{trancl}, for taking the transitive closure of a relation.
lcp@315
  1073
Primitive recursion makes use of \cdx{wfrec}, an operator for recursion
lcp@315
  1074
along arbitrary well-founded relations.  The corresponding theories are
lcp@315
  1075
called {\tt Lfp}, {\tt Trancl} and {\tt WF}\@.  Elsewhere I have described
lcp@315
  1076
similar constructions in the context of set theory~\cite{paulson-set-II}.
lcp@104
  1077
lcp@315
  1078
Type~\tydx{nat} is postulated to belong to class~\cldx{ord}, which
lcp@315
  1079
overloads $<$ and $\leq$ on the natural numbers.  As of this writing,
lcp@315
  1080
Isabelle provides no means of verifying that such overloading is sensible;
lcp@315
  1081
there is no means of specifying the operators' properties and verifying
lcp@315
  1082
that instances of the operators satisfy those properties.  To be safe, the
lcp@315
  1083
\HOL\ theory includes no polymorphic axioms asserting general properties of
lcp@315
  1084
$<$ and~$\leq$.
lcp@104
  1085
lcp@315
  1086
Theory \thydx{Arith} develops arithmetic on the natural numbers.  It
lcp@315
  1087
defines addition, multiplication, subtraction, division, and remainder.
lcp@315
  1088
Many of their properties are proved: commutative, associative and
lcp@315
  1089
distributive laws, identity and cancellation laws, etc.  The most
lcp@315
  1090
interesting result is perhaps the theorem $a \bmod b + (a/b)\times b = a$.
lcp@315
  1091
Division and remainder are defined by repeated subtraction, which requires
lcp@315
  1092
well-founded rather than primitive recursion.  See Figs.\ts\ref{hol-nat1}
lcp@315
  1093
and~\ref{hol-nat2}.
lcp@104
  1094
lcp@315
  1095
The predecessor relation, \cdx{pred_nat}, is shown to be well-founded.
lcp@315
  1096
Recursion along this relation resembles primitive recursion, but is
lcp@315
  1097
stronger because we are in higher-order logic; using primitive recursion to
lcp@315
  1098
define a higher-order function, we can easily Ackermann's function, which
lcp@315
  1099
is not primitive recursive \cite[page~104]{thompson91}.
lcp@315
  1100
The transitive closure of \cdx{pred_nat} is~$<$.  Many functions on the
lcp@315
  1101
natural numbers are most easily expressed using recursion along~$<$.
lcp@315
  1102
lcp@315
  1103
The tactic {\tt\ttindex{nat_ind_tac} "$n$" $i$} performs induction over the
lcp@315
  1104
variable~$n$ in subgoal~$i$.
lcp@104
  1105
lcp@287
  1106
\begin{figure}
lcp@315
  1107
\index{#@{\tt\#} symbol}
lcp@315
  1108
\index{"@@{\tt\at} symbol}
lcp@315
  1109
\begin{constants}
lcp@315
  1110
  \it symbol & \it meta-type & \it priority & \it description \\
lcp@315
  1111
  \cdx{Nil}     & $\alpha list$ & & empty list\\
lcp@315
  1112
  \tt \#   & $[\alpha,\alpha list]\To \alpha list$ & Right 65 & 
lcp@315
  1113
        list constructor \\
lcp@344
  1114
  \cdx{null}    & $\alpha list \To bool$ & & emptiness test\\
lcp@315
  1115
  \cdx{hd}      & $\alpha list \To \alpha$ & & head \\
lcp@315
  1116
  \cdx{tl}      & $\alpha list \To \alpha list$ & & tail \\
lcp@315
  1117
  \cdx{ttl}     & $\alpha list \To \alpha list$ & & total tail \\
lcp@315
  1118
  \tt\at  & $[\alpha list,\alpha list]\To \alpha list$ & Left 65 & append \\
lcp@315
  1119
  \sdx{mem}  & $[\alpha,\alpha list]\To bool$    &  Left 55   & membership\\
lcp@315
  1120
  \cdx{map}     & $(\alpha\To\beta) \To (\alpha list \To \beta list)$
lcp@315
  1121
        & & mapping functional\\
lcp@315
  1122
  \cdx{filter}  & $(\alpha \To bool) \To (\alpha list \To \alpha list)$
lcp@315
  1123
        & & filter functional\\
lcp@315
  1124
  \cdx{list_all}& $(\alpha \To bool) \To (\alpha list \To bool)$
lcp@315
  1125
        & & forall functional\\
lcp@315
  1126
  \cdx{list_rec}        & $[\alpha list, \beta, [\alpha ,\alpha list,
lcp@104
  1127
\beta]\To\beta] \To \beta$
lcp@315
  1128
        & & list recursor
lcp@315
  1129
\end{constants}
nipkow@306
  1130
\subcaption{Constants and infixes}
nipkow@306
  1131
nipkow@306
  1132
\begin{center} \tt\frenchspacing
nipkow@306
  1133
\begin{tabular}{rrr} 
lcp@315
  1134
  \it external        & \it internal  & \it description \\{}
lcp@315
  1135
  \sdx{[]}            & Nil           & \rm empty list \\{}
lcp@315
  1136
  [$x@1$, $\dots$, $x@n$]  &  $x@1$ \# $\cdots$ \# $x@n$ \# [] &
nipkow@306
  1137
        \rm finite list \\{}
lcp@344
  1138
  [$x$:$l$. $P$]  & filter($\lambda x{.}P$, $l$) & 
lcp@315
  1139
        \rm list comprehension
nipkow@306
  1140
\end{tabular}
nipkow@306
  1141
\end{center}
nipkow@306
  1142
\subcaption{Translations}
lcp@104
  1143
lcp@104
  1144
\begin{ttbox}
lcp@315
  1145
\tdx{list_induct}    [| P([]);  !!x xs. [| P(xs) |] ==> P(x#xs)) |]  ==> P(l)
lcp@104
  1146
lcp@315
  1147
\tdx{Cons_not_Nil}   (x # xs) ~= []
lcp@315
  1148
\tdx{Cons_Cons_eq}   ((x # xs) = (y # ys)) = (x=y & xs=ys)
nipkow@306
  1149
\subcaption{Induction and freeness}
lcp@104
  1150
\end{ttbox}
lcp@315
  1151
\caption{The theory \thydx{List}} \label{hol-list}
lcp@104
  1152
\end{figure}
lcp@104
  1153
nipkow@306
  1154
\begin{figure}
nipkow@306
  1155
\begin{ttbox}\makeatother
lcp@471
  1156
\tdx{list_rec_Nil}    list_rec([],c,h) = c  
lcp@471
  1157
\tdx{list_rec_Cons}   list_rec(a#l, c, h) = h(a, l, list_rec(l,c,h))
lcp@315
  1158
lcp@705
  1159
\tdx{list_case_Nil}   list_case(c, h, []) = c 
lcp@705
  1160
\tdx{list_case_Cons}  list_case(c, h, x#xs) = h(x, xs)
lcp@315
  1161
lcp@471
  1162
\tdx{map_Nil}         map(f,[]) = []
lcp@471
  1163
\tdx{map_Cons}        map(f, x \# xs) = f(x) \# map(f,xs)
lcp@315
  1164
lcp@471
  1165
\tdx{null_Nil}        null([]) = True
lcp@471
  1166
\tdx{null_Cons}       null(x#xs) = False
lcp@315
  1167
lcp@471
  1168
\tdx{hd_Cons}         hd(x#xs) = x
lcp@471
  1169
\tdx{tl_Cons}         tl(x#xs) = xs
lcp@315
  1170
lcp@471
  1171
\tdx{ttl_Nil}         ttl([]) = []
lcp@471
  1172
\tdx{ttl_Cons}        ttl(x#xs) = xs
lcp@315
  1173
lcp@471
  1174
\tdx{append_Nil}      [] @ ys = ys
lcp@471
  1175
\tdx{append_Cons}     (x#xs) \at ys = x # xs \at ys
lcp@315
  1176
lcp@471
  1177
\tdx{mem_Nil}         x mem [] = False
lcp@471
  1178
\tdx{mem_Cons}        x mem (y#ys) = if(y=x, True, x mem ys)
lcp@315
  1179
lcp@471
  1180
\tdx{filter_Nil}      filter(P, []) = []
lcp@471
  1181
\tdx{filter_Cons}     filter(P,x#xs) = if(P(x), x#filter(P,xs), filter(P,xs))
lcp@315
  1182
lcp@471
  1183
\tdx{list_all_Nil}    list_all(P,[]) = True
lcp@471
  1184
\tdx{list_all_Cons}   list_all(P, x#xs) = (P(x) & list_all(P, xs))
nipkow@306
  1185
\end{ttbox}
nipkow@306
  1186
\caption{Rewrite rules for lists} \label{hol-list-simps}
nipkow@306
  1187
\end{figure}
lcp@104
  1188
lcp@315
  1189
lcp@315
  1190
\subsection{The type constructor for lists, {\tt list}}
lcp@315
  1191
\index{*list type}
lcp@315
  1192
nipkow@306
  1193
\HOL's definition of lists is an example of an experimental method for
lcp@315
  1194
handling recursive data types.  Figure~\ref{hol-list} presents the theory
lcp@315
  1195
\thydx{List}: the basic list operations with their types and properties.
lcp@315
  1196
lcp@344
  1197
The \sdx{case} construct is defined by the following translation:
lcp@315
  1198
{\dquotes
lcp@315
  1199
\begin{eqnarray*}
lcp@344
  1200
  \begin{array}{r@{\;}l@{}l}
lcp@315
  1201
  "case " e " of" & "[]"    & " => " a\\
lcp@315
  1202
              "|" & x"\#"xs & " => " b
lcp@315
  1203
  \end{array} 
lcp@315
  1204
  & \equiv &
lcp@705
  1205
  "list_case"(a, \lambda x\;xs.b, e)
lcp@344
  1206
\end{eqnarray*}}%
lcp@315
  1207
The theory includes \cdx{list_rec}, a primitive recursion operator
lcp@315
  1208
for lists.  It is derived from well-founded recursion, a general principle
lcp@315
  1209
that can express arbitrary total recursive functions.
lcp@315
  1210
lcp@315
  1211
The simpset \ttindex{list_ss} contains, along with additional useful lemmas,
lcp@315
  1212
the basic rewrite rules that appear in Fig.\ts\ref{hol-list-simps}.
lcp@315
  1213
lcp@315
  1214
The tactic {\tt\ttindex{list_ind_tac} "$xs$" $i$} performs induction over the
lcp@315
  1215
variable~$xs$ in subgoal~$i$.
lcp@104
  1216
lcp@104
  1217
nipkow@464
  1218
\section{Datatype declarations}
nipkow@464
  1219
\index{*datatype|(}
nipkow@464
  1220
nipkow@464
  1221
\underscoreon
nipkow@464
  1222
nipkow@464
  1223
It is often necessary to extend a theory with \ML-like datatypes.  This
nipkow@464
  1224
extension consists of the new type, declarations of its constructors and
nipkow@464
  1225
rules that describe the new type. The theory definition section {\tt
nipkow@464
  1226
  datatype} represents a compact way of doing this.
nipkow@464
  1227
nipkow@464
  1228
nipkow@464
  1229
\subsection{Foundations}
nipkow@464
  1230
nipkow@464
  1231
A datatype declaration has the following general structure:
nipkow@464
  1232
\[ \mbox{\tt datatype}~ (\alpha_1,\dots,\alpha_n)t ~=~
nipkow@580
  1233
      C_1(\tau_{11},\dots,\tau_{1k_1}) ~\mid~ \dots ~\mid~
nipkow@580
  1234
      C_m(\tau_{m1},\dots,\tau_{mk_m}) 
nipkow@464
  1235
\]
nipkow@580
  1236
where $\alpha_i$ are type variables, $C_i$ are distinct constructor names and
nipkow@464
  1237
$\tau_{ij}$ are one of the following:
nipkow@464
  1238
\begin{itemize}
nipkow@464
  1239
\item type variables $\alpha_1,\dots,\alpha_n$,
nipkow@464
  1240
\item types $(\beta_1,\dots,\beta_l)s$ where $s$ is a previously declared
nipkow@464
  1241
  type or type synonym and $\{\beta_1,\dots,\beta_l\} \subseteq
nipkow@464
  1242
  \{\alpha_1,\dots,\alpha_n\}$,
nipkow@464
  1243
\item the newly defined type $(\alpha_1,\dots,\alpha_n)t$ \footnote{This
nipkow@464
  1244
    makes it a recursive type. To ensure that the new type is not empty at
nipkow@464
  1245
    least one constructor must consist of only non-recursive type
nipkow@464
  1246
    components.}
nipkow@464
  1247
\end{itemize}
nipkow@580
  1248
If you would like one of the $\tau_{ij}$ to be a complex type expression
nipkow@580
  1249
$\tau$ you need to declare a new type synonym $syn = \tau$ first and use
nipkow@580
  1250
$syn$ in place of $\tau$. Of course this does not work if $\tau$ mentions the
nipkow@580
  1251
recursive type itself, thus ruling out problematic cases like \[ \mbox{\tt
nipkow@580
  1252
  datatype}~ t ~=~ C(t \To t) \] together with unproblematic ones like \[
nipkow@580
  1253
\mbox{\tt datatype}~ t ~=~ C(t~list). \]
nipkow@580
  1254
nipkow@464
  1255
The constructors are automatically defined as functions of their respective
nipkow@464
  1256
type:
nipkow@580
  1257
\[ C_j : [\tau_{j1},\dots,\tau_{jk_j}] \To (\alpha_1,\dots,\alpha_n)t \]
nipkow@464
  1258
These functions have certain {\em freeness} properties:
nipkow@464
  1259
\begin{description}
nipkow@465
  1260
\item[\tt distinct] They are distinct:
nipkow@580
  1261
\[ C_i(x_1,\dots,x_{k_i}) \neq C_j(y_1,\dots,y_{k_j}) \qquad
nipkow@465
  1262
   \mbox{for all}~ i \neq j.
nipkow@465
  1263
\]
nipkow@464
  1264
\item[\tt inject] They are injective:
nipkow@580
  1265
\[ (C_j(x_1,\dots,x_{k_j}) = C_j(y_1,\dots,y_{k_j})) =
nipkow@464
  1266
   (x_1 = y_1 \land \dots \land x_{k_j} = y_{k_j})
nipkow@464
  1267
\]
nipkow@464
  1268
\end{description}
nipkow@464
  1269
Because the number of inequalities is quadratic in the number of
nipkow@464
  1270
constructors, a different method is used if their number exceeds
nipkow@464
  1271
a certain value, currently 4. In that case every constructor is mapped to a
nipkow@464
  1272
natural number
nipkow@464
  1273
\[
nipkow@464
  1274
\begin{array}{lcl}
nipkow@580
  1275
\mbox{\it t\_ord}(C_1(x_1,\dots,x_{k_1})) & = & 0 \\
nipkow@464
  1276
& \vdots & \\
nipkow@580
  1277
\mbox{\it t\_ord}(C_m(x_1,\dots,x_{k_m})) & = & m-1
nipkow@464
  1278
\end{array}
nipkow@464
  1279
\]
nipkow@465
  1280
and distinctness of constructors is expressed by:
nipkow@464
  1281
\[
nipkow@464
  1282
\mbox{\it t\_ord}(x) \neq \mbox{\it t\_ord}(y) \Imp x \neq y.
nipkow@464
  1283
\]
nipkow@464
  1284
In addition a structural induction axiom {\tt induct} is provided: 
nipkow@464
  1285
\[
nipkow@464
  1286
\infer{P(x)}
nipkow@464
  1287
{\begin{array}{lcl}
nipkow@464
  1288
\Forall x_1\dots x_{k_1}.
nipkow@464
  1289
  \List{P(x_{r_{11}}); \dots; P(x_{r_{1l_1}})} &
nipkow@580
  1290
  \Imp  & P(C_1(x_1,\dots,x_{k_1})) \\
nipkow@464
  1291
 & \vdots & \\
nipkow@464
  1292
\Forall x_1\dots x_{k_m}.
nipkow@464
  1293
  \List{P(x_{r_{m1}}); \dots; P(x_{r_{ml_m}})} &
nipkow@580
  1294
  \Imp & P(C_m(x_1,\dots,x_{k_m}))
nipkow@464
  1295
\end{array}}
nipkow@464
  1296
\]
nipkow@464
  1297
where $\{r_{j1},\dots,r_{jl_j}\} = \{i \in \{1,\dots k_j\} ~\mid~ \tau_{ji}
nipkow@464
  1298
= (\alpha_1,\dots,\alpha_n)t \}$, i.e.\ the property $P$ can be assumed for
nipkow@464
  1299
all arguments of the recursive type.
nipkow@464
  1300
nipkow@465
  1301
The type also comes with an \ML-like \sdx{case}-construct:
nipkow@464
  1302
\[
nipkow@464
  1303
\begin{array}{rrcl}
nipkow@580
  1304
\mbox{\tt case}~e~\mbox{\tt of} & C_1(x_{11},\dots,x_{1k_1}) & \To & e_1 \\
nipkow@464
  1305
                           \vdots \\
nipkow@580
  1306
                           \mid & C_m(x_{m1},\dots,x_{mk_m}) & \To & e_m
nipkow@464
  1307
\end{array}
nipkow@464
  1308
\]
nipkow@464
  1309
In contrast to \ML, {\em all} constructors must be present, their order is
nipkow@464
  1310
fixed, and nested patterns are not supported.
nipkow@464
  1311
nipkow@464
  1312
nipkow@464
  1313
\subsection{Defining datatypes}
nipkow@464
  1314
nipkow@464
  1315
A datatype is defined in a theory definition file using the keyword {\tt
nipkow@464
  1316
  datatype}. The definition following {\tt datatype} must conform to the
nipkow@464
  1317
syntax of {\em typedecl} specified in Fig.~\ref{datatype-grammar} and must
nipkow@464
  1318
obey the rules in the previous section. As a result the theory is extended
nipkow@464
  1319
with the new type, the constructors, and the theorems listed in the previous
nipkow@464
  1320
section.
nipkow@464
  1321
nipkow@464
  1322
\begin{figure}
nipkow@464
  1323
\begin{rail}
nipkow@464
  1324
typedecl : typevarlist id '=' (cons + '|')
nipkow@464
  1325
         ;
nipkow@464
  1326
cons     : (id | string) ( () | '(' (typ + ',') ')' ) ( () | mixfix )
nipkow@464
  1327
         ;
nipkow@464
  1328
typ      : typevarlist id
nipkow@464
  1329
           | tid
lcp@594
  1330
         ;
nipkow@464
  1331
typevarlist : () | tid | '(' (tid + ',') ')'
nipkow@464
  1332
         ;
nipkow@464
  1333
\end{rail}
nipkow@464
  1334
\caption{Syntax of datatype declarations}
nipkow@464
  1335
\label{datatype-grammar}
nipkow@464
  1336
\end{figure}
nipkow@464
  1337
nipkow@465
  1338
Reading the theory file produces a structure which, in addition to the usual
nipkow@464
  1339
components, contains a structure named $t$ for each datatype $t$ defined in
nipkow@465
  1340
the file.\footnote{Otherwise multiple datatypes in the same theory file would
nipkow@465
  1341
  lead to name clashes.} Each structure $t$ contains the following elements:
nipkow@464
  1342
\begin{ttbox}
nipkow@465
  1343
val distinct : thm list
nipkow@464
  1344
val inject : thm list
nipkow@465
  1345
val induct : thm
nipkow@464
  1346
val cases : thm list
nipkow@464
  1347
val simps : thm list
nipkow@464
  1348
val induct_tac : string -> int -> tactic
nipkow@464
  1349
\end{ttbox}
nipkow@465
  1350
{\tt distinct}, {\tt inject} and {\tt induct} contain the theorems described
nipkow@465
  1351
above. For convenience {\tt distinct} contains inequalities in both
nipkow@465
  1352
directions.
nipkow@464
  1353
\begin{warn}
nipkow@464
  1354
  If there are five or more constructors, the {\em t\_ord} scheme is used for
nipkow@465
  1355
  {\tt distinct}.  In this case the theory {\tt Arith} must be contained
nipkow@465
  1356
  in the current theory, if necessary by including it explicitly.
nipkow@464
  1357
\end{warn}
nipkow@465
  1358
The reduction rules of the {\tt case}-construct are in {\tt cases}.  All
nipkow@465
  1359
theorems from {\tt distinct}, {\tt inject} and {\tt cases} are combined in
lcp@1086
  1360
{\tt simps} for use with the simplifier. The tactic {\verb$induct_tac$~{\em
lcp@1086
  1361
    var i}\/} applies structural induction over variable {\em var} to
nipkow@464
  1362
subgoal {\em i}.
nipkow@464
  1363
nipkow@464
  1364
nipkow@464
  1365
\subsection{Examples}
nipkow@464
  1366
nipkow@464
  1367
\subsubsection{The datatype $\alpha~list$}
nipkow@464
  1368
nipkow@465
  1369
We want to define the type $\alpha~list$.\footnote{Of course there is a list
nipkow@465
  1370
  type in HOL already. This is only an example.} To do this we have to build
nipkow@465
  1371
a new theory that contains the type definition. We start from {\tt HOL}.
nipkow@464
  1372
\begin{ttbox}
nipkow@464
  1373
MyList = HOL +
nipkow@464
  1374
  datatype 'a list = Nil | Cons ('a, 'a list)
nipkow@464
  1375
end
nipkow@464
  1376
\end{ttbox}
nipkow@465
  1377
After loading the theory (\verb$use_thy "MyList"$), we can prove
nipkow@465
  1378
$Cons(x,xs)\neq xs$.  First we build a suitable simpset for the simplifier:
nipkow@464
  1379
\begin{ttbox}
nipkow@464
  1380
val mylist_ss = HOL_ss addsimps MyList.list.simps;
nipkow@464
  1381
goal MyList.thy "!x. Cons(x,xs) ~= xs";
nipkow@464
  1382
{\out Level 0}
nipkow@464
  1383
{\out ! x. Cons(x, xs) ~= xs}
nipkow@464
  1384
{\out  1. ! x. Cons(x, xs) ~= xs}
nipkow@464
  1385
\end{ttbox}
nipkow@464
  1386
This can be proved by the structural induction tactic:
nipkow@464
  1387
\begin{ttbox}
nipkow@464
  1388
by (MyList.list.induct_tac "xs" 1);
nipkow@464
  1389
{\out Level 1}
nipkow@464
  1390
{\out ! x. Cons(x, xs) ~= xs}
nipkow@464
  1391
{\out  1. ! x. Cons(x, Nil) ~= Nil}
nipkow@464
  1392
{\out  2. !!a list.}
nipkow@464
  1393
{\out        ! x. Cons(x, list) ~= list ==>}
nipkow@464
  1394
{\out        ! x. Cons(x, Cons(a, list)) ~= Cons(a, list)}
nipkow@464
  1395
\end{ttbox}
nipkow@465
  1396
The first subgoal can be proved with the simplifier and the distinctness
nipkow@465
  1397
axioms which are part of \verb$mylist_ss$.
nipkow@464
  1398
\begin{ttbox}
nipkow@464
  1399
by (simp_tac mylist_ss 1);
nipkow@464
  1400
{\out Level 2}
nipkow@464
  1401
{\out ! x. Cons(x, xs) ~= xs}
nipkow@464
  1402
{\out  1. !!a list.}
nipkow@464
  1403
{\out        ! x. Cons(x, list) ~= list ==>}
nipkow@464
  1404
{\out        ! x. Cons(x, Cons(a, list)) ~= Cons(a, list)}
nipkow@464
  1405
\end{ttbox}
nipkow@465
  1406
Using the freeness axioms we can quickly prove the remaining goal.
nipkow@464
  1407
\begin{ttbox}
nipkow@464
  1408
by (asm_simp_tac mylist_ss 1);
nipkow@464
  1409
{\out Level 3}
nipkow@464
  1410
{\out ! x. Cons(x, xs) ~= xs}
nipkow@464
  1411
{\out No subgoals!}
nipkow@464
  1412
\end{ttbox}
nipkow@464
  1413
Because both subgoals were proved by almost the same tactic we could have
nipkow@464
  1414
done that in one step using
nipkow@464
  1415
\begin{ttbox}
nipkow@464
  1416
by (ALLGOALS (asm_simp_tac mylist_ss));
nipkow@464
  1417
\end{ttbox}
nipkow@464
  1418
nipkow@464
  1419
nipkow@464
  1420
\subsubsection{The datatype $\alpha~list$ with mixfix syntax}
nipkow@464
  1421
nipkow@464
  1422
In this example we define the type $\alpha~list$ again but this time we want
nipkow@464
  1423
to write {\tt []} instead of {\tt Nil} and we want to use the infix operator
nipkow@464
  1424
\verb|#| instead of {\tt Cons}. To do this we simply add mixfix annotations
nipkow@464
  1425
after the constructor declarations as follows:
nipkow@464
  1426
\begin{ttbox}
nipkow@464
  1427
MyList = HOL +
nipkow@464
  1428
  datatype 'a list = "[]" ("[]") 
nipkow@464
  1429
                   | "#" ('a, 'a list) (infixr 70)
nipkow@464
  1430
end
nipkow@464
  1431
\end{ttbox}
nipkow@464
  1432
Now the theorem in the previous example can be written \verb|x#xs ~= xs|. The
nipkow@464
  1433
proof is the same.
nipkow@464
  1434
nipkow@464
  1435
nipkow@464
  1436
\subsubsection{A datatype for weekdays}
nipkow@464
  1437
nipkow@464
  1438
This example shows a datatype that consists of more than four constructors:
nipkow@464
  1439
\begin{ttbox}
nipkow@464
  1440
Days = Arith +
nipkow@464
  1441
  datatype days = Mo | Tu | We | Th | Fr | Sa | So
nipkow@464
  1442
end
nipkow@464
  1443
\end{ttbox}
nipkow@464
  1444
Because there are more than four constructors, the theory must be based on
nipkow@464
  1445
{\tt Arith}. Inequality is defined via a function \verb|days_ord|. Although
nipkow@465
  1446
the expression \verb|Mo ~= Tu| is not directly contained in {\tt distinct},
nipkow@465
  1447
it can be proved by the simplifier if \verb$arith_ss$ is used:
nipkow@464
  1448
\begin{ttbox}
nipkow@464
  1449
val days_ss = arith_ss addsimps Days.days.simps;
nipkow@464
  1450
nipkow@464
  1451
goal Days.thy "Mo ~= Tu";
nipkow@464
  1452
by (simp_tac days_ss 1);
nipkow@464
  1453
\end{ttbox}
nipkow@464
  1454
Note that usually it is not necessary to derive these inequalities explicitly
nipkow@464
  1455
because the simplifier will dispose of them automatically.
nipkow@464
  1456
nipkow@600
  1457
\subsection{Primitive recursive functions}
nipkow@600
  1458
\index{primitive recursion|(}
nipkow@600
  1459
\index{*primrec|(}
nipkow@600
  1460
nipkow@600
  1461
Datatypes come with a uniform way of defining functions, {\bf primitive
nipkow@600
  1462
  recursion}. Although it is possible to define primitive recursive functions
nipkow@600
  1463
by asserting their reduction rules as new axioms, e.g.\
nipkow@600
  1464
\begin{ttbox}
nipkow@600
  1465
Append = MyList +
nipkow@600
  1466
consts app :: "['a list,'a list] => 'a list"
nipkow@600
  1467
rules 
nipkow@600
  1468
   app_Nil   "app([],ys) = ys"
nipkow@600
  1469
   app_Cons  "app(x#xs, ys) = x#app(xs,ys)"
nipkow@600
  1470
end
nipkow@600
  1471
\end{ttbox}
nipkow@600
  1472
this carries with it the danger of accidentally asserting an inconsistency,
nipkow@600
  1473
as in \verb$app([],ys) = us$. Therefore primitive recursive functions on
nipkow@600
  1474
datatypes can be defined with a special syntax:
nipkow@600
  1475
\begin{ttbox}
nipkow@600
  1476
Append = MyList +
nipkow@600
  1477
consts app :: "['a list,'a list] => 'a list"
nipkow@600
  1478
primrec app MyList.list
nipkow@600
  1479
   app_Nil   "app([],ys) = ys"
nipkow@600
  1480
   app_Cons  "app(x#xs, ys) = x#app(xs,ys)"
nipkow@600
  1481
end
nipkow@600
  1482
\end{ttbox}
nipkow@600
  1483
The system will now check that the two rules \verb$app_Nil$ and
nipkow@600
  1484
\verb$app_Cons$ do indeed form a primitive recursive definition, thus
nipkow@600
  1485
ensuring that consistency is maintained. For example
nipkow@600
  1486
\begin{ttbox}
nipkow@600
  1487
primrec app MyList.list
nipkow@600
  1488
    app_Nil   "app([],ys) = us"
nipkow@600
  1489
\end{ttbox}
nipkow@600
  1490
is rejected:
nipkow@600
  1491
\begin{ttbox}
nipkow@600
  1492
Extra variables on rhs
nipkow@600
  1493
\end{ttbox}
nipkow@600
  1494
\bigskip
nipkow@600
  1495
nipkow@600
  1496
The general form of a primitive recursive definition is
nipkow@600
  1497
\begin{ttbox}
nipkow@600
  1498
primrec {\it function} {\it type}
nipkow@600
  1499
    {\it reduction rules}
nipkow@600
  1500
\end{ttbox}
nipkow@600
  1501
where
nipkow@600
  1502
\begin{itemize}
nipkow@600
  1503
\item {\it function} is the name of the function, either as an {\it id} or a
nipkow@600
  1504
  {\it string}. The function must already have been declared.
nipkow@600
  1505
\item {\it type} is the name of the datatype, either as an {\it id} or in the
nipkow@600
  1506
  long form {\it Thy.t}, where {\it Thy} is the name of the parent theory the
nipkow@600
  1507
  datatype was declared in, and $t$ the name of the datatype. The long form
nipkow@600
  1508
  is required if the {\tt datatype} and the {\tt primrec} sections are in
nipkow@600
  1509
  different theories.
nipkow@600
  1510
\item {\it reduction rules} specify one or more named equations of the form
nipkow@600
  1511
  {\it id\/}~{\it string}, where the identifier gives the name of the rule in
nipkow@600
  1512
  the result structure, and {\it string} is a reduction rule of the form \[
nipkow@600
  1513
  f(x_1,\dots,x_m,C(y_1,\dots,y_k),z_1,\dots,z_n) = r \] such that $C$ is a
nipkow@600
  1514
  constructor of the datatype, $r$ contains only the free variables on the
nipkow@600
  1515
  left-hand side, and all recursive calls in $r$ are of the form
nipkow@600
  1516
  $f(\dots,y_i,\dots)$ for some $i$. There must be exactly one reduction
nipkow@600
  1517
  rule for each constructor.
nipkow@600
  1518
\end{itemize}
nipkow@600
  1519
A theory file may contain any number of {\tt primrec} sections which may be
nipkow@600
  1520
intermixed with other declarations.
nipkow@600
  1521
nipkow@600
  1522
For the consistency-sensitive user it may be reassuring to know that {\tt
nipkow@600
  1523
  primrec} does not assert the reduction rules as new axioms but derives them
nipkow@600
  1524
as theorems from an explicit definition of the recursive function in terms of
nipkow@600
  1525
a recursion operator on the datatype.
nipkow@600
  1526
nipkow@600
  1527
The primitive recursive function can also use infix or mixfix syntax:
nipkow@600
  1528
\begin{ttbox}
nipkow@600
  1529
Append = MyList +
nipkow@600
  1530
consts "@"  :: "['a list,'a list] => 'a list"  (infixr 60)
nipkow@600
  1531
primrec "op @" MyList.list
nipkow@600
  1532
   app_Nil   "[] @ ys = ys"
nipkow@600
  1533
   app_Cons  "(x#xs) @ ys = x#(xs @ ys)"
nipkow@600
  1534
end
nipkow@600
  1535
\end{ttbox}
nipkow@600
  1536
nipkow@600
  1537
The reduction rules become part of the ML structure \verb$Append$ and can
nipkow@600
  1538
be used to prove theorems about the function:
nipkow@600
  1539
\begin{ttbox}
nipkow@600
  1540
val append_ss = HOL_ss addsimps [Append.app_Nil,Append.app_Cons];
nipkow@600
  1541
nipkow@600
  1542
goal Append.thy "(xs @ ys) @ zs = xs @ (ys @ zs)";
nipkow@600
  1543
by (MyList.list.induct_tac "xs" 1);
nipkow@600
  1544
by (ALLGOALS(asm_simp_tac append_ss));
nipkow@600
  1545
\end{ttbox}
nipkow@600
  1546
nipkow@600
  1547
%Note that underdefined primitive recursive functions are allowed:
nipkow@600
  1548
%\begin{ttbox}
nipkow@600
  1549
%Tl = MyList +
nipkow@600
  1550
%consts tl  :: "'a list => 'a list"
nipkow@600
  1551
%primrec tl MyList.list
nipkow@600
  1552
%   tl_Cons "tl(x#xs) = xs"
nipkow@600
  1553
%end
nipkow@600
  1554
%\end{ttbox}
nipkow@600
  1555
%Nevertheless {\tt tl} is total, although we do not know what the result of
nipkow@600
  1556
%\verb$tl([])$ is.
nipkow@600
  1557
nipkow@600
  1558
\index{primitive recursion|)}
nipkow@600
  1559
\index{*primrec|)}
lcp@861
  1560
\index{*datatype|)}
lcp@594
  1561
lcp@594
  1562
lcp@594
  1563
\section{Inductive and coinductive definitions}
lcp@594
  1564
\index{*inductive|(}
lcp@594
  1565
\index{*coinductive|(}
lcp@594
  1566
lcp@594
  1567
An {\bf inductive definition} specifies the least set closed under given
lcp@594
  1568
rules.  For example, a structural operational semantics is an inductive
lcp@594
  1569
definition of an evaluation relation.  Dually, a {\bf coinductive
lcp@594
  1570
  definition} specifies the greatest set closed under given rules.  An
lcp@594
  1571
important example is using bisimulation relations to formalize equivalence
lcp@594
  1572
of processes and infinite data structures.
lcp@594
  1573
lcp@594
  1574
A theory file may contain any number of inductive and coinductive
lcp@594
  1575
definitions.  They may be intermixed with other declarations; in
lcp@594
  1576
particular, the (co)inductive sets {\bf must} be declared separately as
lcp@594
  1577
constants, and may have mixfix syntax or be subject to syntax translations.
lcp@594
  1578
lcp@594
  1579
Each (co)inductive definition adds definitions to the theory and also
lcp@594
  1580
proves some theorems.  Each definition creates an ML structure, which is a
lcp@594
  1581
substructure of the main theory structure.
lcp@594
  1582
lcp@594
  1583
This package is derived from the ZF one, described in a
lcp@594
  1584
separate paper,\footnote{It appeared in CADE~\cite{paulson-CADE} and a
lcp@594
  1585
  longer version is distributed with Isabelle.} which you should refer to
lcp@594
  1586
in case of difficulties.  The package is simpler than ZF's, thanks to HOL's
lcp@594
  1587
automatic type-checking.  The type of the (co)inductive determines the
lcp@594
  1588
domain of the fixedpoint definition, and the package does not use inference
lcp@594
  1589
rules for type-checking.
lcp@594
  1590
lcp@594
  1591
lcp@594
  1592
\subsection{The result structure}
lcp@594
  1593
Many of the result structure's components have been discussed in the paper;
lcp@594
  1594
others are self-explanatory.
lcp@594
  1595
\begin{description}
lcp@594
  1596
\item[\tt thy] is the new theory containing the recursive sets.
lcp@594
  1597
lcp@594
  1598
\item[\tt defs] is the list of definitions of the recursive sets.
lcp@594
  1599
lcp@594
  1600
\item[\tt mono] is a monotonicity theorem for the fixedpoint operator.
lcp@594
  1601
lcp@594
  1602
\item[\tt unfold] is a fixedpoint equation for the recursive set (the union of
lcp@594
  1603
the recursive sets, in the case of mutual recursion).
lcp@594
  1604
lcp@594
  1605
\item[\tt intrs] is the list of introduction rules, now proved as theorems, for
lcp@594
  1606
the recursive sets.  The rules are also available individually, using the
lcp@594
  1607
names given them in the theory file. 
lcp@594
  1608
lcp@594
  1609
\item[\tt elim] is the elimination rule.
lcp@594
  1610
lcp@594
  1611
\item[\tt mk\_cases] is a function to create simplified instances of {\tt
lcp@594
  1612
elim}, using freeness reasoning on some underlying datatype.
lcp@594
  1613
\end{description}
lcp@594
  1614
lcp@594
  1615
For an inductive definition, the result structure contains two induction rules,
lcp@594
  1616
{\tt induct} and \verb|mutual_induct|.  For a coinductive definition, it
lcp@594
  1617
contains the rule \verb|coinduct|.
lcp@594
  1618
lcp@594
  1619
Figure~\ref{def-result-fig} summarizes the two result signatures,
lcp@594
  1620
specifying the types of all these components.
lcp@594
  1621
lcp@594
  1622
\begin{figure}
lcp@594
  1623
\begin{ttbox}
lcp@594
  1624
sig
lcp@594
  1625
val thy          : theory
lcp@594
  1626
val defs         : thm list
lcp@594
  1627
val mono         : thm
lcp@594
  1628
val unfold       : thm
lcp@594
  1629
val intrs        : thm list
lcp@594
  1630
val elim         : thm
lcp@594
  1631
val mk_cases     : thm list -> string -> thm
lcp@594
  1632
{\it(Inductive definitions only)} 
lcp@594
  1633
val induct       : thm
lcp@594
  1634
val mutual_induct: thm
lcp@594
  1635
{\it(Coinductive definitions only)}
lcp@594
  1636
val coinduct    : thm
lcp@594
  1637
end
lcp@594
  1638
\end{ttbox}
lcp@594
  1639
\hrule
lcp@594
  1640
\caption{The result of a (co)inductive definition} \label{def-result-fig}
lcp@594
  1641
\end{figure}
nipkow@464
  1642
lcp@594
  1643
\subsection{The syntax of a (co)inductive definition}
lcp@594
  1644
An inductive definition has the form
lcp@594
  1645
\begin{ttbox}
lcp@594
  1646
inductive    {\it inductive sets}
lcp@594
  1647
  intrs      {\it introduction rules}
lcp@594
  1648
  monos      {\it monotonicity theorems}
lcp@594
  1649
  con_defs   {\it constructor definitions}
lcp@594
  1650
\end{ttbox}
lcp@594
  1651
A coinductive definition is identical, except that it starts with the keyword
lcp@594
  1652
{\tt coinductive}.  
lcp@594
  1653
lcp@594
  1654
The {\tt monos} and {\tt con\_defs} sections are optional.  If present,
lcp@594
  1655
each is specified as a string, which must be a valid ML expression of type
lcp@594
  1656
{\tt thm list}.  It is simply inserted into the {\tt .thy.ML} file; if it
lcp@594
  1657
is ill-formed, it will trigger ML error messages.  You can then inspect the
lcp@594
  1658
file on your directory.
lcp@594
  1659
lcp@594
  1660
\begin{itemize}
lcp@594
  1661
\item The {\it inductive sets} are specified by one or more strings.
lcp@594
  1662
lcp@594
  1663
\item The {\it introduction rules} specify one or more introduction rules in
lcp@594
  1664
  the form {\it ident\/}~{\it string}, where the identifier gives the name of
lcp@594
  1665
  the rule in the result structure.
lcp@594
  1666
lcp@594
  1667
\item The {\it monotonicity theorems} are required for each operator
lcp@594
  1668
  applied to a recursive set in the introduction rules.  There {\bf must}
lcp@594
  1669
  be a theorem of the form $A\subseteq B\Imp M(A)\subseteq M(B)$, for each
lcp@594
  1670
  premise $t\in M(R_i)$ in an introduction rule!
lcp@594
  1671
lcp@594
  1672
\item The {\it constructor definitions} contain definitions of constants
lcp@594
  1673
  appearing in the introduction rules.  In most cases it can be omitted.
lcp@594
  1674
\end{itemize}
lcp@594
  1675
lcp@594
  1676
The package has a few notable restrictions:
lcp@594
  1677
\begin{itemize}
lcp@594
  1678
\item The theory must separately declare the recursive sets as
lcp@594
  1679
  constants.
lcp@594
  1680
lcp@594
  1681
\item The names of the recursive sets must be identifiers, not infix
lcp@594
  1682
operators.  
lcp@594
  1683
lcp@594
  1684
\item Side-conditions must not be conjunctions.  However, an introduction rule
lcp@594
  1685
may contain any number of side-conditions.
lcp@594
  1686
lcp@594
  1687
\item Side-conditions of the form $x=t$, where the variable~$x$ does not
lcp@594
  1688
  occur in~$t$, will be substituted through the rule \verb|mutual_induct|.
lcp@594
  1689
\end{itemize}
lcp@594
  1690
lcp@594
  1691
lcp@594
  1692
\subsection{Example of an inductive definition}
lcp@594
  1693
Two declarations, included in a theory file, define the finite powerset
lcp@594
  1694
operator.  First we declare the constant~{\tt Fin}.  Then we declare it
lcp@594
  1695
inductively, with two introduction rules:
lcp@594
  1696
\begin{ttbox}
lcp@594
  1697
consts Fin :: "'a set => 'a set set"
lcp@594
  1698
inductive "Fin(A)"
lcp@594
  1699
  intrs
lcp@594
  1700
    emptyI  "{} : Fin(A)"
lcp@594
  1701
    insertI "[| a: A;  b: Fin(A) |] ==> insert(a,b) : Fin(A)"
lcp@594
  1702
\end{ttbox}
lcp@594
  1703
The resulting theory structure contains a substructure, called~{\tt Fin}.
lcp@594
  1704
It contains the {\tt Fin}$(A)$ introduction rules as the list {\tt Fin.intrs},
lcp@594
  1705
and also individually as {\tt Fin.emptyI} and {\tt Fin.consI}.  The induction
lcp@594
  1706
rule is {\tt Fin.induct}.
lcp@594
  1707
lcp@594
  1708
For another example, here is a theory file defining the accessible part of a
lcp@594
  1709
relation.  The main thing to note is the use of~{\tt Pow} in the sole
lcp@594
  1710
introduction rule, and the corresponding mention of the rule
lcp@594
  1711
\verb|Pow_mono| in the {\tt monos} list.  The paper discusses a ZF version
lcp@594
  1712
of this example in more detail.
lcp@594
  1713
\begin{ttbox}
lcp@594
  1714
Acc = WF + 
lcp@594
  1715
consts pred :: "['b, ('a * 'b)set] => 'a set"   (*Set of predecessors*)
lcp@594
  1716
       acc  :: "('a * 'a)set => 'a set"         (*Accessible part*)
lcp@594
  1717
defs   pred_def  "pred(x,r) == {y. <y,x>:r}"
lcp@594
  1718
inductive "acc(r)"
lcp@594
  1719
  intrs
lcp@594
  1720
     pred "pred(a,r): Pow(acc(r)) ==> a: acc(r)"
lcp@594
  1721
  monos   "[Pow_mono]"
lcp@594
  1722
end
lcp@594
  1723
\end{ttbox}
lcp@594
  1724
The HOL distribution contains many other inductive definitions, such as the
lcp@594
  1725
theory {\tt HOL/ex/PropLog.thy} and the directory {\tt HOL/IMP}.  The
lcp@629
  1726
theory {\tt HOL/ex/LList.thy} contains coinductive definitions.
lcp@594
  1727
lcp@594
  1728
\index{*coinductive|)} \index{*inductive|)} \underscoreoff
nipkow@464
  1729
nipkow@464
  1730
lcp@111
  1731
\section{The examples directories}
lcp@344
  1732
Directory {\tt HOL/Subst} contains Martin Coen's mechanisation of a theory of
lcp@111
  1733
substitutions and unifiers.  It is based on Paulson's previous
lcp@344
  1734
mechanisation in {\LCF}~\cite{paulson85} of Manna and Waldinger's
lcp@111
  1735
theory~\cite{mw81}. 
lcp@111
  1736
lcp@594
  1737
Directory {\tt HOL/IMP} contains a mechanised version of a semantic
lcp@594
  1738
equivalence proof taken from Winskel~\cite{winskel93}.  It formalises the
lcp@594
  1739
denotational and operational semantics of a simple while-language, then
lcp@594
  1740
proves the two equivalent.  It contains several datatype and inductive
lcp@594
  1741
definitions, and demonstrates their use.
lcp@594
  1742
lcp@315
  1743
Directory {\tt HOL/ex} contains other examples and experimental proofs in
lcp@315
  1744
{\HOL}.  Here is an overview of the more interesting files.
lcp@594
  1745
\begin{itemize}
lcp@594
  1746
\item File {\tt cla.ML} demonstrates the classical reasoner on over sixty
lcp@344
  1747
  predicate calculus theorems, ranging from simple tautologies to
lcp@344
  1748
  moderately difficult problems involving equality and quantifiers.
lcp@344
  1749
lcp@594
  1750
\item File {\tt meson.ML} contains an experimental implementation of the {\sc
lcp@315
  1751
    meson} proof procedure, inspired by Plaisted~\cite{plaisted90}.  It is
lcp@315
  1752
  much more powerful than Isabelle's classical reasoner.  But it is less
lcp@315
  1753
  useful in practice because it works only for pure logic; it does not
lcp@315
  1754
  accept derived rules for the set theory primitives, for example.
lcp@104
  1755
lcp@594
  1756
\item File {\tt mesontest.ML} contains test data for the {\sc meson} proof
lcp@315
  1757
  procedure.  These are mostly taken from Pelletier \cite{pelletier86}.
lcp@104
  1758
lcp@594
  1759
\item File {\tt set.ML} proves Cantor's Theorem, which is presented in
lcp@315
  1760
  \S\ref{sec:hol-cantor} below, and the Schr\"oder-Bernstein Theorem.
lcp@315
  1761
lcp@594
  1762
\item Theories {\tt InSort} and {\tt Qsort} prove correctness properties of
lcp@594
  1763
  insertion sort and quick sort.
lcp@104
  1764
lcp@629
  1765
\item The definition of lazy lists demonstrates methods for handling
lcp@629
  1766
  infinite data structures and coinduction in higher-order
lcp@629
  1767
  logic~\cite{paulson-coind}.  Theory \thydx{LList} defines an operator for
lcp@629
  1768
  corecursion on lazy lists, which is used to define a few simple functions
lcp@629
  1769
  such as map and append.  Corecursion cannot easily define operations such
lcp@629
  1770
  as filter, which can compute indefinitely before yielding the next
lcp@629
  1771
  element (if any!) of the lazy list.  A coinduction principle is defined
lcp@629
  1772
  for proving equations on lazy lists.
lcp@629
  1773
lcp@594
  1774
\item Theory {\tt PropLog} proves the soundness and completeness of
lcp@594
  1775
  classical propositional logic, given a truth table semantics.  The only
lcp@594
  1776
  connective is $\imp$.  A Hilbert-style axiom system is specified, and its
lcp@594
  1777
  set of theorems defined inductively.  A similar proof in \ZF{} is
lcp@594
  1778
  described elsewhere~\cite{paulson-set-II}.
lcp@104
  1779
lcp@594
  1780
\item Theory {\tt Term} develops an experimental recursive type definition;
lcp@315
  1781
  the recursion goes through the type constructor~\tydx{list}.
lcp@104
  1782
lcp@594
  1783
\item Theory {\tt Simult} constructs mutually recursive sets of trees and
lcp@594
  1784
  forests, including induction and recursion rules.
lcp@111
  1785
lcp@594
  1786
\item Theory {\tt MT} contains Jacob Frost's formalization~\cite{frost93} of
lcp@315
  1787
  Milner and Tofte's coinduction example~\cite{milner-coind}.  This
lcp@315
  1788
  substantial proof concerns the soundness of a type system for a simple
lcp@315
  1789
  functional language.  The semantics of recursion is given by a cyclic
lcp@315
  1790
  environment, which makes a coinductive argument appropriate.
lcp@594
  1791
\end{itemize}
lcp@104
  1792
lcp@104
  1793
lcp@344
  1794
\goodbreak
lcp@315
  1795
\section{Example: Cantor's Theorem}\label{sec:hol-cantor}
lcp@104
  1796
Cantor's Theorem states that every set has more subsets than it has
lcp@104
  1797
elements.  It has become a favourite example in higher-order logic since
lcp@104
  1798
it is so easily expressed:
lcp@104
  1799
\[  \forall f::[\alpha,\alpha]\To bool. \exists S::\alpha\To bool.
lcp@104
  1800
    \forall x::\alpha. f(x) \not= S 
lcp@104
  1801
\] 
lcp@315
  1802
%
lcp@104
  1803
Viewing types as sets, $\alpha\To bool$ represents the powerset
lcp@104
  1804
of~$\alpha$.  This version states that for every function from $\alpha$ to
lcp@344
  1805
its powerset, some subset is outside its range.  
lcp@344
  1806
lcp@344
  1807
The Isabelle proof uses \HOL's set theory, with the type $\alpha\,set$ and
lcp@344
  1808
the operator \cdx{range}.  The set~$S$ is given as an unknown instead of a
lcp@315
  1809
quantified variable so that we may inspect the subset found by the proof.
lcp@104
  1810
\begin{ttbox}
lcp@104
  1811
goal Set.thy "~ ?S : range(f :: 'a=>'a set)";
lcp@104
  1812
{\out Level 0}
lcp@104
  1813
{\out ~ ?S : range(f)}
lcp@104
  1814
{\out  1. ~ ?S : range(f)}
lcp@104
  1815
\end{ttbox}
lcp@315
  1816
The first two steps are routine.  The rule \tdx{rangeE} replaces
lcp@315
  1817
$\Var{S}\in {\tt range}(f)$ by $\Var{S}=f(x)$ for some~$x$.
lcp@104
  1818
\begin{ttbox}
lcp@104
  1819
by (resolve_tac [notI] 1);
lcp@104
  1820
{\out Level 1}
lcp@104
  1821
{\out ~ ?S : range(f)}
lcp@104
  1822
{\out  1. ?S : range(f) ==> False}
lcp@287
  1823
\ttbreak
lcp@104
  1824
by (eresolve_tac [rangeE] 1);
lcp@104
  1825
{\out Level 2}
lcp@104
  1826
{\out ~ ?S : range(f)}
lcp@104
  1827
{\out  1. !!x. ?S = f(x) ==> False}
lcp@104
  1828
\end{ttbox}
lcp@315
  1829
Next, we apply \tdx{equalityCE}, reasoning that since $\Var{S}=f(x)$,
lcp@104
  1830
we have $\Var{c}\in \Var{S}$ if and only if $\Var{c}\in f(x)$ for
lcp@104
  1831
any~$\Var{c}$.
lcp@104
  1832
\begin{ttbox}
lcp@104
  1833
by (eresolve_tac [equalityCE] 1);
lcp@104
  1834
{\out Level 3}
lcp@104
  1835
{\out ~ ?S : range(f)}
lcp@104
  1836
{\out  1. !!x. [| ?c3(x) : ?S; ?c3(x) : f(x) |] ==> False}
lcp@104
  1837
{\out  2. !!x. [| ~ ?c3(x) : ?S; ~ ?c3(x) : f(x) |] ==> False}
lcp@104
  1838
\end{ttbox}
lcp@315
  1839
Now we use a bit of creativity.  Suppose that~$\Var{S}$ has the form of a
lcp@104
  1840
comprehension.  Then $\Var{c}\in\{x.\Var{P}(x)\}$ implies
lcp@315
  1841
$\Var{P}(\Var{c})$.   Destruct-resolution using \tdx{CollectD}
lcp@315
  1842
instantiates~$\Var{S}$ and creates the new assumption.
lcp@104
  1843
\begin{ttbox}
lcp@104
  1844
by (dresolve_tac [CollectD] 1);
lcp@104
  1845
{\out Level 4}
lcp@104
  1846
{\out ~ \{x. ?P7(x)\} : range(f)}
lcp@104
  1847
{\out  1. !!x. [| ?c3(x) : f(x); ?P7(?c3(x)) |] ==> False}
lcp@104
  1848
{\out  2. !!x. [| ~ ?c3(x) : \{x. ?P7(x)\}; ~ ?c3(x) : f(x) |] ==> False}
lcp@104
  1849
\end{ttbox}
lcp@104
  1850
Forcing a contradiction between the two assumptions of subgoal~1 completes
lcp@344
  1851
the instantiation of~$S$.  It is now the set $\{x. x\not\in f(x)\}$, which
lcp@344
  1852
is the standard diagonal construction.
lcp@104
  1853
\begin{ttbox}
lcp@104
  1854
by (contr_tac 1);
lcp@104
  1855
{\out Level 5}
lcp@104
  1856
{\out ~ \{x. ~ x : f(x)\} : range(f)}
lcp@104
  1857
{\out  1. !!x. [| ~ x : \{x. ~ x : f(x)\}; ~ x : f(x) |] ==> False}
lcp@104
  1858
\end{ttbox}
lcp@315
  1859
The rest should be easy.  To apply \tdx{CollectI} to the negated
lcp@104
  1860
assumption, we employ \ttindex{swap_res_tac}:
lcp@104
  1861
\begin{ttbox}
lcp@104
  1862
by (swap_res_tac [CollectI] 1);
lcp@104
  1863
{\out Level 6}
lcp@104
  1864
{\out ~ \{x. ~ x : f(x)\} : range(f)}
lcp@104
  1865
{\out  1. !!x. [| ~ x : f(x); ~ False |] ==> ~ x : f(x)}
lcp@287
  1866
\ttbreak
lcp@104
  1867
by (assume_tac 1);
lcp@104
  1868
{\out Level 7}
lcp@104
  1869
{\out ~ \{x. ~ x : f(x)\} : range(f)}
lcp@104
  1870
{\out No subgoals!}
lcp@104
  1871
\end{ttbox}
lcp@104
  1872
How much creativity is required?  As it happens, Isabelle can prove this
lcp@104
  1873
theorem automatically.  The classical set \ttindex{set_cs} contains rules
lcp@315
  1874
for most of the constructs of \HOL's set theory.  We must augment it with
lcp@315
  1875
\tdx{equalityCE} to break up set equalities, and then apply best-first
lcp@315
  1876
search.  Depth-first search would diverge, but best-first search
lcp@315
  1877
successfully navigates through the large search space.
lcp@315
  1878
\index{search!best-first}
lcp@104
  1879
\begin{ttbox}
lcp@104
  1880
choplev 0;
lcp@104
  1881
{\out Level 0}
lcp@104
  1882
{\out ~ ?S : range(f)}
lcp@104
  1883
{\out  1. ~ ?S : range(f)}
lcp@287
  1884
\ttbreak
lcp@104
  1885
by (best_tac (set_cs addSEs [equalityCE]) 1);
lcp@104
  1886
{\out Level 1}
lcp@104
  1887
{\out ~ \{x. ~ x : f(x)\} : range(f)}
lcp@104
  1888
{\out No subgoals!}
lcp@104
  1889
\end{ttbox}
lcp@315
  1890
lcp@315
  1891
\index{higher-order logic|)}