doc-src/Logics/Old_HOL.tex
author nipkow
Tue, 12 Jul 1994 12:49:15 +0200
changeset 465 d4bf81734dfe
parent 464 552717636da4
child 471 22325fd7234e
permissions -rw-r--r--
Corrected HOL.tex
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     1
%% $Id$
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
     2
\chapter{Higher-Order Logic}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
     3
\index{higher-order logic|(}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
     4
\index{HOL system@{\sc hol} system}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
     5
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
     6
The theory~\thydx{HOL} implements higher-order logic.
344
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
     7
It is based on Gordon's~{\sc hol} system~\cite{mgordon-hol}, which itself is
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
     8
based on Church's original paper~\cite{church40}.  Andrews's
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
     9
book~\cite{andrews86} is a full description of higher-order logic.
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    10
Experience with the {\sc hol} system has demonstrated that higher-order
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    11
logic is useful for hardware verification; beyond this, it is widely
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    12
applicable in many areas of mathematics.  It is weaker than {\ZF} set
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    13
theory but for most applications this does not matter.  If you prefer {\ML}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    14
to Lisp, you will probably prefer \HOL\ to~{\ZF}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    15
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    16
Previous releases of Isabelle included a different version of~\HOL, with
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    17
explicit type inference rules~\cite{paulson-COLOG}.  This version no longer
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    18
exists, but \thydx{ZF} supports a similar style of reasoning.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    19
306
eee166d4a532 changed lists and added "let" and "case"
nipkow
parents: 287
diff changeset
    20
\HOL\ has a distinct feel, compared with {\ZF} and {\CTT}.  It
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    21
identifies object-level types with meta-level types, taking advantage of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    22
Isabelle's built-in type checker.  It identifies object-level functions
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    23
with meta-level functions, so it uses Isabelle's operations for abstraction
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    24
and application.  There is no `apply' operator: function applications are
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    25
written as simply~$f(a)$ rather than $f{\tt`}a$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    26
306
eee166d4a532 changed lists and added "let" and "case"
nipkow
parents: 287
diff changeset
    27
These identifications allow Isabelle to support \HOL\ particularly nicely,
eee166d4a532 changed lists and added "let" and "case"
nipkow
parents: 287
diff changeset
    28
but they also mean that \HOL\ requires more sophistication from the user
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    29
--- in particular, an understanding of Isabelle's type system.  Beginners
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    30
should work with {\tt show_types} set to {\tt true}.  Gain experience by
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    31
working in first-order logic before attempting to use higher-order logic.
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    32
This chapter assumes familiarity with~{\FOL{}}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    33
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    34
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    35
\begin{figure} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    36
\begin{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    37
\begin{tabular}{rrr} 
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
    38
  \it name      &\it meta-type  & \it description \\ 
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    39
  \cdx{Trueprop}& $bool\To prop$                & coercion to $prop$\\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    40
  \cdx{not}     & $bool\To bool$                & negation ($\neg$) \\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    41
  \cdx{True}    & $bool$                        & tautology ($\top$) \\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    42
  \cdx{False}   & $bool$                        & absurdity ($\bot$) \\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    43
  \cdx{if}      & $[bool,\alpha,\alpha]\To\alpha::term$ & conditional \\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    44
  \cdx{Inv}     & $(\alpha\To\beta)\To(\beta\To\alpha)$ & function inversion\\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    45
  \cdx{Let}     & $[\alpha,\alpha\To\beta]\To\beta$ & let binder
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    46
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    47
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    48
\subcaption{Constants}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    49
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    50
\begin{center}
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    51
\index{"@@{\tt\at} symbol}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    52
\index{*"! symbol}\index{*"? symbol}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    53
\index{*"?"! symbol}\index{*"E"X"! symbol}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    54
\begin{tabular}{llrrr} 
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    55
  \it symbol &\it name     &\it meta-type & \it description \\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    56
  \tt\at & \cdx{Eps}  & $(\alpha\To bool)\To\alpha::term$ & 
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
    57
        Hilbert description ($\epsilon$) \\
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    58
  {\tt!~} or \sdx{ALL}  & \cdx{All}  & $(\alpha::term\To bool)\To bool$ & 
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
    59
        universal quantifier ($\forall$) \\
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    60
  {\tt?~} or \sdx{EX}   & \cdx{Ex}   & $(\alpha::term\To bool)\To bool$ & 
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
    61
        existential quantifier ($\exists$) \\
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    62
  {\tt?!} or {\tt EX!}  & \cdx{Ex1}  & $(\alpha::term\To bool)\To bool$ & 
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
    63
        unique existence ($\exists!$)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    64
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    65
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    66
\subcaption{Binders} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    67
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    68
\begin{center}
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    69
\index{*"= symbol}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    70
\index{&@{\tt\&} symbol}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    71
\index{*"| symbol}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    72
\index{*"-"-"> symbol}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    73
\begin{tabular}{rrrr} 
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    74
  \it symbol    & \it meta-type & \it priority & \it description \\ 
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    75
  \sdx{o}       & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ & 
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
    76
        Right 50 & composition ($\circ$) \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
    77
  \tt =         & $[\alpha::term,\alpha]\To bool$ & Left 50 & equality ($=$) \\
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    78
  \tt <         & $[\alpha::ord,\alpha]\To bool$ & Left 50 & less than ($<$) \\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    79
  \tt <=        & $[\alpha::ord,\alpha]\To bool$ & Left 50 & 
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    80
                less than or equals ($\leq$)\\
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
    81
  \tt \&        & $[bool,bool]\To bool$ & Right 35 & conjunction ($\conj$) \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
    82
  \tt |         & $[bool,bool]\To bool$ & Right 30 & disjunction ($\disj$) \\
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    83
  \tt -->       & $[bool,bool]\To bool$ & Right 25 & implication ($\imp$)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    84
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    85
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    86
\subcaption{Infixes}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    87
\caption{Syntax of {\tt HOL}} \label{hol-constants}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    88
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    89
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    90
306
eee166d4a532 changed lists and added "let" and "case"
nipkow
parents: 287
diff changeset
    91
\begin{figure}
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    92
\index{*let symbol}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    93
\index{*in symbol}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    94
\dquotes
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    95
\[\begin{array}{rclcl}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    96
    term & = & \hbox{expression of class~$term$} \\
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    97
         & | & "\at~" id~id^* " . " formula \\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    98
         & | & 
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
    99
    \multicolumn{3}{l}{"let"~id~"="~term";"\dots";"~id~"="~term~"in"~term}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   100
               \\[2ex]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   101
 formula & = & \hbox{expression of type~$bool$} \\
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   102
         & | & term " = " term \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   103
         & | & term " \ttilde= " term \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   104
         & | & term " < " term \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   105
         & | & term " <= " term \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   106
         & | & "\ttilde\ " formula \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   107
         & | & formula " \& " formula \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   108
         & | & formula " | " formula \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   109
         & | & formula " --> " formula \\
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   110
         & | & "!~~~" id~id^* " . " formula 
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   111
         & | & "ALL~" id~id^* " . " formula \\
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   112
         & | & "?~~~" id~id^* " . " formula 
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   113
         & | & "EX~~" id~id^* " . " formula \\
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   114
         & | & "?!~~" id~id^* " . " formula 
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   115
         & | & "EX!~" id~id^* " . " formula
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   116
  \end{array}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   117
\]
306
eee166d4a532 changed lists and added "let" and "case"
nipkow
parents: 287
diff changeset
   118
\caption{Full grammar for \HOL} \label{hol-grammar}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   119
\end{figure} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   120
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   121
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   122
\section{Syntax}
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   123
The type class of higher-order terms is called~\cldx{term}.  Type variables
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   124
range over this class by default.  The equality symbol and quantifiers are
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   125
polymorphic over class {\tt term}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   126
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   127
Class \cldx{ord} consists of all ordered types; the relations $<$ and
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   128
$\leq$ are polymorphic over this class, as are the functions
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   129
\cdx{mono}, \cdx{min} and \cdx{max}.  Three other
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   130
type classes --- \cldx{plus}, \cldx{minus} and \cldx{times} --- permit
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   131
overloading of the operators {\tt+}, {\tt-} and {\tt*}.  In particular,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   132
{\tt-} is overloaded for set difference and subtraction.
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   133
\index{*"+ symbol}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   134
\index{*"- symbol}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   135
\index{*"* symbol}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   136
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   137
Figure~\ref{hol-constants} lists the constants (including infixes and
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   138
binders), while Fig.\ts\ref{hol-grammar} presents the grammar of
287
6b62a6ddbe15 first draft of Springer book
lcp
parents: 154
diff changeset
   139
higher-order logic.  Note that $a$\verb|~=|$b$ is translated to
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   140
$\neg(a=b)$.
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   141
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   142
\begin{warn}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   143
  \HOL\ has no if-and-only-if connective; logical equivalence is expressed
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   144
  using equality.  But equality has a high priority, as befitting a
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   145
  relation, while if-and-only-if typically has the lowest priority.  Thus,
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   146
  $\neg\neg P=P$ abbreviates $\neg\neg (P=P)$ and not $(\neg\neg P)=P$.
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   147
  When using $=$ to mean logical equivalence, enclose both operands in
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   148
  parentheses.
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   149
\end{warn}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   150
287
6b62a6ddbe15 first draft of Springer book
lcp
parents: 154
diff changeset
   151
\subsection{Types}\label{HOL-types}
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   152
The type of formulae, \tydx{bool}, belongs to class \cldx{term}; thus,
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   153
formulae are terms.  The built-in type~\tydx{fun}, which constructs function
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   154
types, is overloaded with arity {\tt(term,term)term}.  Thus, $\sigma\To\tau$
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   155
belongs to class~{\tt term} if $\sigma$ and~$\tau$ do, allowing quantification
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   156
over functions.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   157
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   158
Types in \HOL\ must be non-empty; otherwise the quantifier rules would be
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   159
unsound.  I have commented on this elsewhere~\cite[\S7]{paulson-COLOG}.
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   160
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   161
\index{type definitions}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   162
Gordon's {\sc hol} system supports {\bf type definitions}.  A type is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   163
defined by exhibiting an existing type~$\sigma$, a predicate~$P::\sigma\To
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   164
bool$, and a theorem of the form $\exists x::\sigma.P(x)$.  Thus~$P$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   165
specifies a non-empty subset of~$\sigma$, and the new type denotes this
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   166
subset.  New function constants are generated to establish an isomorphism
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   167
between the new type and the subset.  If type~$\sigma$ involves type
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   168
variables $\alpha@1$, \ldots, $\alpha@n$, then the type definition creates
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   169
a type constructor $(\alpha@1,\ldots,\alpha@n)ty$ rather than a particular
344
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   170
type.  Melham~\cite{melham89} discusses type definitions at length, with
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   171
examples. 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   172
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   173
Isabelle does not support type definitions at present.  Instead, they are
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   174
mimicked by explicit definitions of isomorphism functions.  The definitions
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   175
should be supported by theorems of the form $\exists x::\sigma.P(x)$, but
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   176
Isabelle cannot enforce this.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   177
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   178
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   179
\subsection{Binders}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   180
Hilbert's {\bf description} operator~$\epsilon x.P[x]$ stands for some~$a$
306
eee166d4a532 changed lists and added "let" and "case"
nipkow
parents: 287
diff changeset
   181
satisfying~$P[a]$, if such exists.  Since all terms in \HOL\ denote
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   182
something, a description is always meaningful, but we do not know its value
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   183
unless $P[x]$ defines it uniquely.  We may write descriptions as
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   184
\cdx{Eps}($P$) or use the syntax
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   185
\hbox{\tt \at $x$.$P[x]$}.
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   186
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   187
Existential quantification is defined by
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   188
\[ \exists x.P(x) \;\equiv\; P(\epsilon x.P(x)). \]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   189
The unique existence quantifier, $\exists!x.P[x]$, is defined in terms
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   190
of~$\exists$ and~$\forall$.  An Isabelle binder, it admits nested
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   191
quantifications.  For instance, $\exists!x y.P(x,y)$ abbreviates
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   192
$\exists!x. \exists!y.P(x,y)$; note that this does not mean that there
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   193
exists a unique pair $(x,y)$ satisfying~$P(x,y)$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   194
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   195
\index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system}
306
eee166d4a532 changed lists and added "let" and "case"
nipkow
parents: 287
diff changeset
   196
Quantifiers have two notations.  As in Gordon's {\sc hol} system, \HOL\
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   197
uses~{\tt!}\ and~{\tt?}\ to stand for $\forall$ and $\exists$.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   198
existential quantifier must be followed by a space; thus {\tt?x} is an
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   199
unknown, while \verb'? x.f(x)=y' is a quantification.  Isabelle's usual
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   200
notation for quantifiers, \sdx{ALL} and \sdx{EX}, is also
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   201
available.  Both notations are accepted for input.  The {\ML} reference
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   202
\ttindexbold{HOL_quantifiers} governs the output notation.  If set to {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   203
true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default.  If set
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   204
to {\tt false}, then~{\tt ALL} and~{\tt EX} are displayed.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   205
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   206
All these binders have priority 10. 
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   207
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   208
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   209
\subsection{The \sdx{let} and \sdx{case} constructions}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   210
Local abbreviations can be introduced by a {\tt let} construct whose
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   211
syntax appears in Fig.\ts\ref{hol-grammar}.  Internally it is translated into
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   212
the constant~\cdx{Let}.  It can be expanded by rewriting with its
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   213
definition, \tdx{Let_def}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   214
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   215
\HOL\ also defines the basic syntax
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   216
\[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n\] 
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   217
as a uniform means of expressing {\tt case} constructs.  Therefore {\tt
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   218
  case} and \sdx{of} are reserved words.  However, so far this is mere
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   219
syntax and has no logical meaning.  By declaring translations, you can
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   220
cause instances of the {\tt case} construct to denote applications of
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   221
particular case operators.  The patterns supplied for $c@1$,~\ldots,~$c@n$
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   222
distinguish among the different case operators.  For an example, see the
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   223
case construct for lists on page~\pageref{hol-list} below.
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   224
306
eee166d4a532 changed lists and added "let" and "case"
nipkow
parents: 287
diff changeset
   225
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   226
\begin{figure}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   227
\begin{ttbox}\makeatother
453
d4e82b3a06c9 added () around some of the ::
nipkow
parents: 349
diff changeset
   228
\tdx{refl}           t = (t::'a)
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   229
\tdx{subst}          [| s=t; P(s) |] ==> P(t::'a)
453
d4e82b3a06c9 added () around some of the ::
nipkow
parents: 349
diff changeset
   230
\tdx{ext}            (!!x::'a. (f(x)::'b) = g(x)) ==> (\%x.f(x)) = (\%x.g(x))
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   231
\tdx{impI}           (P ==> Q) ==> P-->Q
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   232
\tdx{mp}             [| P-->Q;  P |] ==> Q
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   233
\tdx{iff}            (P-->Q) --> (Q-->P) --> (P=Q)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   234
\tdx{selectI}        P(x::'a) ==> P(@x.P(x))
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   235
\tdx{True_or_False}  (P=True) | (P=False)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   236
\end{ttbox}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   237
\caption{The {\tt HOL} rules} \label{hol-rules}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   238
\end{figure}
306
eee166d4a532 changed lists and added "let" and "case"
nipkow
parents: 287
diff changeset
   239
eee166d4a532 changed lists and added "let" and "case"
nipkow
parents: 287
diff changeset
   240
344
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   241
\begin{figure}\hfuzz=4pt%suppress "Overfull \hbox" message
287
6b62a6ddbe15 first draft of Springer book
lcp
parents: 154
diff changeset
   242
\begin{ttbox}\makeatother
453
d4e82b3a06c9 added () around some of the ::
nipkow
parents: 349
diff changeset
   243
\tdx{True_def}   True  == ((\%x::bool.x)=(\%x.x))
344
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   244
\tdx{All_def}    All   == (\%P. P = (\%x.True))
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   245
\tdx{Ex_def}     Ex    == (\%P. P(@x.P(x)))
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   246
\tdx{False_def}  False == (!P.P)
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   247
\tdx{not_def}    not   == (\%P. P-->False)
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   248
\tdx{and_def}    op &  == (\%P Q. !R. (P-->Q-->R) --> R)
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   249
\tdx{or_def}     op |  == (\%P Q. !R. (P-->R) --> (Q-->R) --> R)
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   250
\tdx{Ex1_def}    Ex1   == (\%P. ? x. P(x) & (! y. P(y) --> y=x))
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   251
344
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   252
\tdx{Inv_def}    Inv   == (\%(f::'a=>'b) y. @x. f(x)=y)
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   253
\tdx{o_def}      op o  == (\%(f::'b=>'c) g (x::'a). f(g(x)))
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   254
\tdx{if_def}     if    == (\%P x y.@z::'a.(P=True --> z=x) & (P=False --> z=y))
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   255
\tdx{Let_def}    Let(s,f) == f(s)
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   256
\end{ttbox}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   257
\caption{The {\tt HOL} definitions} \label{hol-defs}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   258
\end{figure}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   259
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   260
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   261
\section{Rules of inference}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   262
Figure~\ref{hol-rules} shows the inference rules of~\HOL{}, with
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   263
their~{\ML} names.  Some of the rules deserve additional comments:
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   264
\begin{ttdescription}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   265
\item[\tdx{ext}] expresses extensionality of functions.
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   266
\item[\tdx{iff}] asserts that logically equivalent formulae are
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   267
  equal.
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   268
\item[\tdx{selectI}] gives the defining property of the Hilbert
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   269
  $\epsilon$-operator.  It is a form of the Axiom of Choice.  The derived rule
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   270
  \tdx{select_equality} (see below) is often easier to use.
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   271
\item[\tdx{True_or_False}] makes the logic classical.\footnote{In
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   272
    fact, the $\epsilon$-operator already makes the logic classical, as
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   273
    shown by Diaconescu; see Paulson~\cite{paulson-COLOG} for details.}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   274
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   275
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   276
\HOL{} follows standard practice in higher-order logic: only a few
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   277
connectives are taken as primitive, with the remainder defined obscurely
344
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   278
(Fig.\ts\ref{hol-defs}).  Gordon's {\sc hol} system expresses the
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   279
corresponding definitions \cite[page~270]{mgordon-hol} using
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   280
object-equality~({\tt=}), which is possible because equality in
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   281
higher-order logic may equate formulae and even functions over formulae.
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   282
But theory~\HOL{}, like all other Isabelle theories, uses
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   283
meta-equality~({\tt==}) for definitions.
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   284
344
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   285
Some of the rules mention type variables; for
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   286
example, {\tt refl} mentions the type variable~{\tt'a}.  This allows you to
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   287
instantiate type variables explicitly by calling {\tt res_inst_tac}.  By
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   288
default, explicit type variables have class \cldx{term}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   289
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   290
Include type constraints whenever you state a polymorphic goal.  Type
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   291
inference may otherwise make the goal more polymorphic than you intended,
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   292
with confusing results.
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   293
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   294
\begin{warn}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   295
  If resolution fails for no obvious reason, try setting
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   296
  \ttindex{show_types} to {\tt true}, causing Isabelle to display types of
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   297
  terms.  Possibly set \ttindex{show_sorts} to {\tt true} as well, causing
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   298
  Isabelle to display sorts.
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   299
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   300
  \index{unification!incompleteness of}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   301
  Where function types are involved, Isabelle's unification code does not
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   302
  guarantee to find instantiations for type variables automatically.  Be
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   303
  prepared to use \ttindex{res_inst_tac} instead of {\tt resolve_tac},
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   304
  possibly instantiating type variables.  Setting
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   305
  \ttindex{Unify.trace_types} to {\tt true} causes Isabelle to report
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   306
  omitted search paths during unification.\index{tracing!of unification}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   307
\end{warn}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   308
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   309
287
6b62a6ddbe15 first draft of Springer book
lcp
parents: 154
diff changeset
   310
\begin{figure}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   311
\begin{ttbox}
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   312
\tdx{sym}         s=t ==> t=s
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   313
\tdx{trans}       [| r=s; s=t |] ==> r=t
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   314
\tdx{ssubst}      [| t=s; P(s) |] ==> P(t::'a)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   315
\tdx{box_equals}  [| a=b;  a=c;  b=d |] ==> c=d  
453
d4e82b3a06c9 added () around some of the ::
nipkow
parents: 349
diff changeset
   316
\tdx{arg_cong}    x=y ==> f(x)=f(y)
d4e82b3a06c9 added () around some of the ::
nipkow
parents: 349
diff changeset
   317
\tdx{fun_cong}    f=g ==> f(x)=g(x)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   318
\subcaption{Equality}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   319
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   320
\tdx{TrueI}       True 
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   321
\tdx{FalseE}      False ==> P
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   322
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   323
\tdx{conjI}       [| P; Q |] ==> P&Q
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   324
\tdx{conjunct1}   [| P&Q |] ==> P
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   325
\tdx{conjunct2}   [| P&Q |] ==> Q 
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   326
\tdx{conjE}       [| P&Q;  [| P; Q |] ==> R |] ==> R
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   327
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   328
\tdx{disjI1}      P ==> P|Q
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   329
\tdx{disjI2}      Q ==> P|Q
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   330
\tdx{disjE}       [| P | Q; P ==> R; Q ==> R |] ==> R
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   331
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   332
\tdx{notI}        (P ==> False) ==> ~ P
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   333
\tdx{notE}        [| ~ P;  P |] ==> R
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   334
\tdx{impE}        [| P-->Q;  P;  Q ==> R |] ==> R
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   335
\subcaption{Propositional logic}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   336
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   337
\tdx{iffI}        [| P ==> Q;  Q ==> P |] ==> P=Q
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   338
\tdx{iffD1}       [| P=Q; P |] ==> Q
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   339
\tdx{iffD2}       [| P=Q; Q |] ==> P
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   340
\tdx{iffE}        [| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   341
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   342
\tdx{eqTrueI}     P ==> P=True 
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   343
\tdx{eqTrueE}     P=True ==> P 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   344
\subcaption{Logical equivalence}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   345
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   346
\end{ttbox}
306
eee166d4a532 changed lists and added "let" and "case"
nipkow
parents: 287
diff changeset
   347
\caption{Derived rules for \HOL} \label{hol-lemmas1}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   348
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   349
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   350
287
6b62a6ddbe15 first draft of Springer book
lcp
parents: 154
diff changeset
   351
\begin{figure}
6b62a6ddbe15 first draft of Springer book
lcp
parents: 154
diff changeset
   352
\begin{ttbox}\makeatother
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   353
\tdx{allI}      (!!x::'a. P(x)) ==> !x. P(x)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   354
\tdx{spec}      !x::'a.P(x) ==> P(x)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   355
\tdx{allE}      [| !x.P(x);  P(x) ==> R |] ==> R
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   356
\tdx{all_dupE}  [| !x.P(x);  [| P(x); !x.P(x) |] ==> R |] ==> R
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   357
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   358
\tdx{exI}       P(x) ==> ? x::'a.P(x)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   359
\tdx{exE}       [| ? x::'a.P(x); !!x. P(x) ==> Q |] ==> Q
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   360
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   361
\tdx{ex1I}      [| P(a);  !!x. P(x) ==> x=a |] ==> ?! x. P(x)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   362
\tdx{ex1E}      [| ?! x.P(x);  !!x. [| P(x);  ! y. P(y) --> y=x |] ==> R 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   363
          |] ==> R
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   364
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   365
\tdx{select_equality} [| P(a);  !!x. P(x) ==> x=a |] ==> (@x.P(x)) = a
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   366
\subcaption{Quantifiers and descriptions}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   367
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   368
\tdx{ccontr}          (~P ==> False) ==> P
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   369
\tdx{classical}       (~P ==> P) ==> P
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   370
\tdx{excluded_middle} ~P | P
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   371
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   372
\tdx{disjCI}          (~Q ==> P) ==> P|Q
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   373
\tdx{exCI}            (! x. ~ P(x) ==> P(a)) ==> ? x.P(x)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   374
\tdx{impCE}           [| P-->Q; ~ P ==> R; Q ==> R |] ==> R
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   375
\tdx{iffCE}           [| P=Q;  [| P;Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   376
\tdx{notnotD}         ~~P ==> P
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   377
\tdx{swap}            ~P ==> (~Q ==> P) ==> Q
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   378
\subcaption{Classical logic}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   379
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   380
\tdx{if_True}         if(True,x,y) = x
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   381
\tdx{if_False}        if(False,x,y) = y
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   382
\tdx{if_P}            P ==> if(P,x,y) = x
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   383
\tdx{if_not_P}        ~ P ==> if(P,x,y) = y
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   384
\tdx{expand_if}       P(if(Q,x,y)) = ((Q --> P(x)) & (~Q --> P(y)))
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   385
\subcaption{Conditionals}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   386
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   387
\caption{More derived rules} \label{hol-lemmas2}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   388
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   389
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   390
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   391
Some derived rules are shown in Figures~\ref{hol-lemmas1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   392
and~\ref{hol-lemmas2}, with their {\ML} names.  These include natural rules
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   393
for the logical connectives, as well as sequent-style elimination rules for
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   394
conjunctions, implications, and universal quantifiers.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   395
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   396
Note the equality rules: \tdx{ssubst} performs substitution in
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   397
backward proofs, while \tdx{box_equals} supports reasoning by
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   398
simplifying both sides of an equation.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   399
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   400
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   401
\begin{figure} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   402
\begin{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   403
\begin{tabular}{rrr} 
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   404
  \it name      &\it meta-type  & \it description \\ 
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   405
\index{{}@\verb'{}' symbol}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   406
  \verb|{}|     & $\alpha\,set$         & the empty set \\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   407
  \cdx{insert}  & $[\alpha,\alpha\,set]\To \alpha\,set$
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   408
        & insertion of element \\
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   409
  \cdx{Collect} & $(\alpha\To bool)\To\alpha\,set$
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   410
        & comprehension \\
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   411
  \cdx{Compl}   & $(\alpha\,set)\To\alpha\,set$
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   412
        & complement \\
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   413
  \cdx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   414
        & intersection over a set\\
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   415
  \cdx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   416
        & union over a set\\
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   417
  \cdx{Inter} & $((\alpha\,set)set)\To\alpha\,set$
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   418
        &set of sets intersection \\
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   419
  \cdx{Union} & $((\alpha\,set)set)\To\alpha\,set$
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   420
        &set of sets union \\
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   421
  \cdx{range}   & $(\alpha\To\beta )\To\beta\,set$
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   422
        & range of a function \\[1ex]
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   423
  \cdx{Ball}~~\cdx{Bex} & $[\alpha\,set,\alpha\To bool]\To bool$
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   424
        & bounded quantifiers \\
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   425
  \cdx{mono}    & $(\alpha\,set\To\beta\,set)\To bool$
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   426
        & monotonicity \\
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   427
  \cdx{inj}~~\cdx{surj}& $(\alpha\To\beta )\To bool$
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   428
        & injective/surjective \\
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   429
  \cdx{inj_onto}        & $[\alpha\To\beta ,\alpha\,set]\To bool$
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   430
        & injective over subset
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   431
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   432
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   433
\subcaption{Constants}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   434
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   435
\begin{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   436
\begin{tabular}{llrrr} 
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   437
  \it symbol &\it name     &\it meta-type & \it priority & \it description \\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   438
  \sdx{INT}  & \cdx{INTER1}  & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 & 
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   439
        intersection over a type\\
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   440
  \sdx{UN}  & \cdx{UNION1}  & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 & 
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   441
        union over a type
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   442
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   443
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   444
\subcaption{Binders} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   445
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   446
\begin{center}
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   447
\index{*"`"` symbol}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   448
\index{*": symbol}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   449
\index{*"<"= symbol}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   450
\begin{tabular}{rrrr} 
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   451
  \it symbol    & \it meta-type & \it priority & \it description \\ 
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   452
  \tt ``        & $[\alpha\To\beta ,\alpha\,set]\To  (\beta\,set)$
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   453
        & Left 90 & image \\
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   454
  \sdx{Int}     & $[\alpha\,set,\alpha\,set]\To\alpha\,set$
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   455
        & Left 70 & intersection ($\inter$) \\
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   456
  \sdx{Un}      & $[\alpha\,set,\alpha\,set]\To\alpha\,set$
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   457
        & Left 65 & union ($\union$) \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   458
  \tt:          & $[\alpha ,\alpha\,set]\To bool$       
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   459
        & Left 50 & membership ($\in$) \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   460
  \tt <=        & $[\alpha\,set,\alpha\,set]\To bool$
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   461
        & Left 50 & subset ($\subseteq$) 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   462
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   463
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   464
\subcaption{Infixes}
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   465
\caption{Syntax of the theory {\tt Set}} \label{hol-set-syntax}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   466
\end{figure} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   467
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   468
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   469
\begin{figure} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   470
\begin{center} \tt\frenchspacing
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   471
\index{*"! symbol}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   472
\begin{tabular}{rrr} 
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   473
  \it external          & \it internal  & \it description \\ 
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   474
  $a$ \ttilde: $b$      & \ttilde($a$ : $b$)    & \rm non-membership\\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   475
  \{$a@1$, $\ldots$\}  &  insert($a@1$, $\ldots$\{\}) & \rm finite set \\
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   476
  \{$x$.$P[x]$\}        &  Collect($\lambda x.P[x]$) &
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   477
        \rm comprehension \\
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   478
  \sdx{INT} $x$:$A$.$B[x]$      & INTER($A$,$\lambda x.B[x]$) &
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   479
        \rm intersection \\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   480
  \sdx{UN}{\tt\ }  $x$:$A$.$B[x]$      & UNION($A$,$\lambda x.B[x]$) &
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   481
        \rm union \\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   482
  \tt ! $x$:$A$.$P[x]$ or \sdx{ALL} $x$:$A$.$P[x]$ & 
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   483
        Ball($A$,$\lambda x.P[x]$) & 
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   484
        \rm bounded $\forall$ \\
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   485
  \sdx{?} $x$:$A$.$P[x]$ or \sdx{EX}{\tt\ } $x$:$A$.$P[x]$ & 
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   486
        Bex($A$,$\lambda x.P[x]$) & \rm bounded $\exists$
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   487
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   488
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   489
\subcaption{Translations}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   490
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   491
\dquotes
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   492
\[\begin{array}{rclcl}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   493
    term & = & \hbox{other terms\ldots} \\
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   494
         & | & "\{\}" \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   495
         & | & "\{ " term\; ("," term)^* " \}" \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   496
         & | & "\{ " id " . " formula " \}" \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   497
         & | & term " `` " term \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   498
         & | & term " Int " term \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   499
         & | & term " Un " term \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   500
         & | & "INT~~"  id ":" term " . " term \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   501
         & | & "UN~~~"  id ":" term " . " term \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   502
         & | & "INT~~"  id~id^* " . " term \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   503
         & | & "UN~~~"  id~id^* " . " term \\[2ex]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   504
 formula & = & \hbox{other formulae\ldots} \\
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   505
         & | & term " : " term \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   506
         & | & term " \ttilde: " term \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   507
         & | & term " <= " term \\
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   508
         & | & "!~" id ":" term " . " formula 
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   509
         & | & "ALL " id ":" term " . " formula \\
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   510
         & | & "?~" id ":" term " . " formula 
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   511
         & | & "EX~~" id ":" term " . " formula
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   512
  \end{array}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   513
\]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   514
\subcaption{Full Grammar}
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   515
\caption{Syntax of the theory {\tt Set} (continued)} \label{hol-set-syntax2}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   516
\end{figure} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   517
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   518
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   519
\section{A formulation of set theory}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   520
Historically, higher-order logic gives a foundation for Russell and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   521
Whitehead's theory of classes.  Let us use modern terminology and call them
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   522
{\bf sets}, but note that these sets are distinct from those of {\ZF} set
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   523
theory, and behave more like {\ZF} classes.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   524
\begin{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   525
\item
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   526
Sets are given by predicates over some type~$\sigma$.  Types serve to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   527
define universes for sets, but type checking is still significant.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   528
\item
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   529
There is a universal set (for each type).  Thus, sets have complements, and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   530
may be defined by absolute comprehension.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   531
\item
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   532
Although sets may contain other sets as elements, the containing set must
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   533
have a more complex type.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   534
\end{itemize}
306
eee166d4a532 changed lists and added "let" and "case"
nipkow
parents: 287
diff changeset
   535
Finite unions and intersections have the same behaviour in \HOL\ as they
eee166d4a532 changed lists and added "let" and "case"
nipkow
parents: 287
diff changeset
   536
do in~{\ZF}.  In \HOL\ the intersection of the empty set is well-defined,
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   537
denoting the universal set for the given type.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   538
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   539
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   540
\subsection{Syntax of set theory}\index{*set type}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   541
\HOL's set theory is called \thydx{Set}.  The type $\alpha\,set$ is
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   542
essentially the same as $\alpha\To bool$.  The new type is defined for
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   543
clarity and to avoid complications involving function types in unification.
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   544
Since Isabelle does not support type definitions (as mentioned in
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   545
\S\ref{HOL-types}), the isomorphisms between the two types are declared
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   546
explicitly.  Here they are natural: {\tt Collect} maps $\alpha\To bool$ to
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   547
$\alpha\,set$, while \hbox{\tt op :} maps in the other direction (ignoring
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   548
argument order).
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   549
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   550
Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   551
translations.  Figure~\ref{hol-set-syntax2} presents the grammar of the new
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   552
constructs.  Infix operators include union and intersection ($A\union B$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   553
and $A\inter B$), the subset and membership relations, and the image
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   554
operator~{\tt``}\@.  Note that $a$\verb|~:|$b$ is translated to
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   555
$\neg(a\in b)$.  
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   556
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   557
The {\tt\{\ldots\}} notation abbreviates finite sets constructed in the
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   558
obvious manner using~{\tt insert} and~$\{\}$:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   559
\begin{eqnarray*}
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   560
  \{a@1, \ldots, a@n\}  & \equiv &  
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   561
  {\tt insert}(a@1,\ldots,{\tt insert}(a@n,\{\}))
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   562
\end{eqnarray*}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   563
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   564
The set \hbox{\tt\{$x$.$P[x]$\}} consists of all $x$ (of suitable type)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   565
that satisfy~$P[x]$, where $P[x]$ is a formula that may contain free
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   566
occurrences of~$x$.  This syntax expands to \cdx{Collect}$(\lambda
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   567
x.P[x])$.  It defines sets by absolute comprehension, which is impossible
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   568
in~{\ZF}; the type of~$x$ implicitly restricts the comprehension.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   569
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   570
The set theory defines two {\bf bounded quantifiers}:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   571
\begin{eqnarray*}
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   572
   \forall x\in A.P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   573
   \exists x\in A.P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   574
\end{eqnarray*}
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   575
The constants~\cdx{Ball} and~\cdx{Bex} are defined
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   576
accordingly.  Instead of {\tt Ball($A$,$P$)} and {\tt Bex($A$,$P$)} we may
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   577
write\index{*"! symbol}\index{*"? symbol}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   578
\index{*ALL symbol}\index{*EX symbol} 
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   579
%
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   580
\hbox{\tt !~$x$:$A$.$P[x]$} and \hbox{\tt ?~$x$:$A$.$P[x]$}.  Isabelle's
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   581
usual quantifier symbols, \sdx{ALL} and \sdx{EX}, are also accepted
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   582
for input.  As with the primitive quantifiers, the {\ML} reference
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   583
\ttindex{HOL_quantifiers} specifies which notation to use for output.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   584
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   585
Unions and intersections over sets, namely $\bigcup@{x\in A}B[x]$ and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   586
$\bigcap@{x\in A}B[x]$, are written 
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   587
\sdx{UN}~\hbox{\tt$x$:$A$.$B[x]$} and
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   588
\sdx{INT}~\hbox{\tt$x$:$A$.$B[x]$}.  
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   589
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   590
Unions and intersections over types, namely $\bigcup@x B[x]$ and $\bigcap@x
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   591
B[x]$, are written \sdx{UN}~\hbox{\tt$x$.$B[x]$} and
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   592
\sdx{INT}~\hbox{\tt$x$.$B[x]$}.  They are equivalent to the previous
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   593
union and intersection operators when $A$ is the universal set.
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   594
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   595
The operators $\bigcup A$ and $\bigcap A$ act upon sets of sets.  They are
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   596
not binders, but are equal to $\bigcup@{x\in A}x$ and $\bigcap@{x\in A}x$,
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   597
respectively.
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   598
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   599
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   600
\begin{figure} \underscoreon
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   601
\begin{ttbox}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   602
\tdx{mem_Collect_eq}    (a : \{x.P(x)\}) = P(a)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   603
\tdx{Collect_mem_eq}    \{x.x:A\} = A
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   604
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   605
\tdx{empty_def}         \{\}          == \{x.x=False\}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   606
\tdx{insert_def}        insert(a,B) == \{x.x=a\} Un B
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   607
\tdx{Ball_def}          Ball(A,P)   == ! x. x:A --> P(x)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   608
\tdx{Bex_def}           Bex(A,P)    == ? x. x:A & P(x)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   609
\tdx{subset_def}        A <= B      == ! x:A. x:B
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   610
\tdx{Un_def}            A Un B      == \{x.x:A | x:B\}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   611
\tdx{Int_def}           A Int B     == \{x.x:A & x:B\}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   612
\tdx{set_diff_def}      A - B       == \{x.x:A & x~:B\}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   613
\tdx{Compl_def}         Compl(A)    == \{x. ~ x:A\}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   614
\tdx{INTER_def}         INTER(A,B)  == \{y. ! x:A. y: B(x)\}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   615
\tdx{UNION_def}         UNION(A,B)  == \{y. ? x:A. y: B(x)\}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   616
\tdx{INTER1_def}        INTER1(B)   == INTER(\{x.True\}, B)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   617
\tdx{UNION1_def}        UNION1(B)   == UNION(\{x.True\}, B)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   618
\tdx{Inter_def}         Inter(S)    == (INT x:S. x)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   619
\tdx{Union_def}         Union(S)    ==  (UN x:S. x)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   620
\tdx{image_def}         f``A        == \{y. ? x:A. y=f(x)\}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   621
\tdx{range_def}         range(f)    == \{y. ? x. y=f(x)\}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   622
\tdx{mono_def}          mono(f)     == !A B. A <= B --> f(A) <= f(B)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   623
\tdx{inj_def}           inj(f)      == ! x y. f(x)=f(y) --> x=y
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   624
\tdx{surj_def}          surj(f)     == ! y. ? x. y=f(x)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   625
\tdx{inj_onto_def}      inj_onto(f,A) == !x:A. !y:A. f(x)=f(y) --> x=y
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   626
\end{ttbox}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   627
\caption{Rules of the theory {\tt Set}} \label{hol-set-rules}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   628
\end{figure}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   629
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   630
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   631
\begin{figure} \underscoreon
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   632
\begin{ttbox}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   633
\tdx{CollectI}        [| P(a) |] ==> a : \{x.P(x)\}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   634
\tdx{CollectD}        [| a : \{x.P(x)\} |] ==> P(a)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   635
\tdx{CollectE}        [| a : \{x.P(x)\};  P(a) ==> W |] ==> W
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   636
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   637
\tdx{ballI}           [| !!x. x:A ==> P(x) |] ==> ! x:A. P(x)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   638
\tdx{bspec}           [| ! x:A. P(x);  x:A |] ==> P(x)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   639
\tdx{ballE}           [| ! x:A. P(x);  P(x) ==> Q;  ~ x:A ==> Q |] ==> Q
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   640
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   641
\tdx{bexI}            [| P(x);  x:A |] ==> ? x:A. P(x)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   642
\tdx{bexCI}           [| ! x:A. ~ P(x) ==> P(a);  a:A |] ==> ? x:A.P(x)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   643
\tdx{bexE}            [| ? x:A. P(x);  !!x. [| x:A; P(x) |] ==> Q  |] ==> Q
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   644
\subcaption{Comprehension and Bounded quantifiers}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   645
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   646
\tdx{subsetI}         (!!x.x:A ==> x:B) ==> A <= B
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   647
\tdx{subsetD}         [| A <= B;  c:A |] ==> c:B
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   648
\tdx{subsetCE}        [| A <= B;  ~ (c:A) ==> P;  c:B ==> P |] ==> P
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   649
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   650
\tdx{subset_refl}     A <= A
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   651
\tdx{subset_antisym}  [| A <= B;  B <= A |] ==> A = B
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   652
\tdx{subset_trans}    [| A<=B;  B<=C |] ==> A<=C
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   653
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   654
\tdx{set_ext}         [| !!x. (x:A) = (x:B) |] ==> A = B
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   655
\tdx{equalityD1}      A = B ==> A<=B
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   656
\tdx{equalityD2}      A = B ==> B<=A
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   657
\tdx{equalityE}       [| A = B;  [| A<=B; B<=A |] ==> P |]  ==>  P
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   658
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   659
\tdx{equalityCE}      [| A = B;  [| c:A; c:B |] ==> P;  
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   660
                           [| ~ c:A; ~ c:B |] ==> P 
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   661
                |]  ==>  P
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   662
\subcaption{The subset and equality relations}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   663
\end{ttbox}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   664
\caption{Derived rules for set theory} \label{hol-set1}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   665
\end{figure}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   666
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   667
287
6b62a6ddbe15 first draft of Springer book
lcp
parents: 154
diff changeset
   668
\begin{figure} \underscoreon
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   669
\begin{ttbox}
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   670
\tdx{emptyE}   a : \{\} ==> P
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   671
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   672
\tdx{insertI1} a : insert(a,B)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   673
\tdx{insertI2} a : B ==> a : insert(b,B)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   674
\tdx{insertE}  [| a : insert(b,A);  a=b ==> P;  a:A ==> P |] ==> P
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   675
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   676
\tdx{ComplI}   [| c:A ==> False |] ==> c : Compl(A)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   677
\tdx{ComplD}   [| c : Compl(A) |] ==> ~ c:A
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   678
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   679
\tdx{UnI1}     c:A ==> c : A Un B
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   680
\tdx{UnI2}     c:B ==> c : A Un B
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   681
\tdx{UnCI}     (~c:B ==> c:A) ==> c : A Un B
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   682
\tdx{UnE}      [| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   683
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   684
\tdx{IntI}     [| c:A;  c:B |] ==> c : A Int B
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   685
\tdx{IntD1}    c : A Int B ==> c:A
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   686
\tdx{IntD2}    c : A Int B ==> c:B
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   687
\tdx{IntE}     [| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   688
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   689
\tdx{UN_I}     [| a:A;  b: B(a) |] ==> b: (UN x:A. B(x))
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   690
\tdx{UN_E}     [| b: (UN x:A. B(x));  !!x.[| x:A;  b:B(x) |] ==> R |] ==> R
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   691
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   692
\tdx{INT_I}    (!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   693
\tdx{INT_D}    [| b: (INT x:A. B(x));  a:A |] ==> b: B(a)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   694
\tdx{INT_E}    [| b: (INT x:A. B(x));  b: B(a) ==> R;  ~ a:A ==> R |] ==> R
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   695
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   696
\tdx{UnionI}   [| X:C;  A:X |] ==> A : Union(C)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   697
\tdx{UnionE}   [| A : Union(C);  !!X.[| A:X;  X:C |] ==> R |] ==> R
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   698
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   699
\tdx{InterI}   [| !!X. X:C ==> A:X |] ==> A : Inter(C)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   700
\tdx{InterD}   [| A : Inter(C);  X:C |] ==> A:X
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   701
\tdx{InterE}   [| A : Inter(C);  A:X ==> R;  ~ X:C ==> R |] ==> R
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   702
\end{ttbox}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   703
\caption{Further derived rules for set theory} \label{hol-set2}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   704
\end{figure}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   705
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   706
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   707
\subsection{Axioms and rules of set theory}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   708
Figure~\ref{hol-set-rules} presents the rules of theory \thydx{Set}.  The
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   709
axioms \tdx{mem_Collect_eq} and \tdx{Collect_mem_eq} assert
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   710
that the functions {\tt Collect} and \hbox{\tt op :} are isomorphisms.  Of
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   711
course, \hbox{\tt op :} also serves as the membership relation.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   712
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   713
All the other axioms are definitions.  They include the empty set, bounded
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   714
quantifiers, unions, intersections, complements and the subset relation.
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   715
They also include straightforward properties of functions: image~({\tt``}) and
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   716
{\tt range}, and predicates concerning monotonicity, injectiveness and
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   717
surjectiveness.  
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   718
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   719
The predicate \cdx{inj_onto} is used for simulating type definitions.
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   720
The statement ${\tt inj_onto}(f,A)$ asserts that $f$ is injective on the
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   721
set~$A$, which specifies a subset of its domain type.  In a type
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   722
definition, $f$ is the abstraction function and $A$ is the set of valid
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   723
representations; we should not expect $f$ to be injective outside of~$A$.
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   724
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   725
\begin{figure} \underscoreon
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   726
\begin{ttbox}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   727
\tdx{Inv_f_f}    inj(f) ==> Inv(f,f(x)) = x
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   728
\tdx{f_Inv_f}    y : range(f) ==> f(Inv(f,y)) = y
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   729
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   730
%\tdx{Inv_injective}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   731
%    [| Inv(f,x)=Inv(f,y); x: range(f);  y: range(f) |] ==> x=y
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   732
%
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   733
\tdx{imageI}     [| x:A |] ==> f(x) : f``A
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   734
\tdx{imageE}     [| b : f``A;  !!x.[| b=f(x);  x:A |] ==> P |] ==> P
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   735
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   736
\tdx{rangeI}     f(x) : range(f)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   737
\tdx{rangeE}     [| b : range(f);  !!x.[| b=f(x) |] ==> P |] ==> P
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   738
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   739
\tdx{monoI}      [| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   740
\tdx{monoD}      [| mono(f);  A <= B |] ==> f(A) <= f(B)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   741
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   742
\tdx{injI}       [| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   743
\tdx{inj_inverseI}              (!!x. g(f(x)) = x) ==> inj(f)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   744
\tdx{injD}       [| inj(f); f(x) = f(y) |] ==> x=y
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   745
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   746
\tdx{inj_ontoI}  (!!x y. [| f(x)=f(y); x:A; y:A |] ==> x=y) ==> inj_onto(f,A)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   747
\tdx{inj_ontoD}  [| inj_onto(f,A);  f(x)=f(y);  x:A;  y:A |] ==> x=y
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   748
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   749
\tdx{inj_onto_inverseI}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   750
    (!!x. x:A ==> g(f(x)) = x) ==> inj_onto(f,A)
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   751
\tdx{inj_onto_contraD}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   752
    [| inj_onto(f,A);  x~=y;  x:A;  y:A |] ==> ~ f(x)=f(y)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   753
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   754
\caption{Derived rules involving functions} \label{hol-fun}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   755
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   756
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   757
287
6b62a6ddbe15 first draft of Springer book
lcp
parents: 154
diff changeset
   758
\begin{figure} \underscoreon
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   759
\begin{ttbox}
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   760
\tdx{Union_upper}     B:A ==> B <= Union(A)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   761
\tdx{Union_least}     [| !!X. X:A ==> X<=C |] ==> Union(A) <= C
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   762
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   763
\tdx{Inter_lower}     B:A ==> Inter(A) <= B
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   764
\tdx{Inter_greatest}  [| !!X. X:A ==> C<=X |] ==> C <= Inter(A)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   765
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   766
\tdx{Un_upper1}       A <= A Un B
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   767
\tdx{Un_upper2}       B <= A Un B
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   768
\tdx{Un_least}        [| A<=C;  B<=C |] ==> A Un B <= C
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   769
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   770
\tdx{Int_lower1}      A Int B <= A
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   771
\tdx{Int_lower2}      A Int B <= B
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   772
\tdx{Int_greatest}    [| C<=A;  C<=B |] ==> C <= A Int B
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   773
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   774
\caption{Derived rules involving subsets} \label{hol-subset}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   775
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   776
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   777
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   778
\begin{figure} \underscoreon   \hfuzz=4pt%suppress "Overfull \hbox" message
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   779
\begin{ttbox}
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   780
\tdx{Int_absorb}        A Int A = A
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   781
\tdx{Int_commute}       A Int B = B Int A
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   782
\tdx{Int_assoc}         (A Int B) Int C  =  A Int (B Int C)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   783
\tdx{Int_Un_distrib}    (A Un B)  Int C  =  (A Int C) Un (B Int C)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   784
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   785
\tdx{Un_absorb}         A Un A = A
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   786
\tdx{Un_commute}        A Un B = B Un A
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   787
\tdx{Un_assoc}          (A Un B)  Un C  =  A Un (B Un C)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   788
\tdx{Un_Int_distrib}    (A Int B) Un C  =  (A Un C) Int (B Un C)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   789
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   790
\tdx{Compl_disjoint}    A Int Compl(A) = \{x.False\}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   791
\tdx{Compl_partition}   A Un  Compl(A) = \{x.True\}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   792
\tdx{double_complement} Compl(Compl(A)) = A
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   793
\tdx{Compl_Un}          Compl(A Un B)  = Compl(A) Int Compl(B)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   794
\tdx{Compl_Int}         Compl(A Int B) = Compl(A) Un Compl(B)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   795
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   796
\tdx{Union_Un_distrib}  Union(A Un B) = Union(A) Un Union(B)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   797
\tdx{Int_Union}         A Int Union(B) = (UN C:B. A Int C)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   798
\tdx{Un_Union_image}    (UN x:C. A(x) Un B(x)) = Union(A``C) Un Union(B``C)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   799
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   800
\tdx{Inter_Un_distrib}  Inter(A Un B) = Inter(A) Int Inter(B)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   801
\tdx{Un_Inter}          A Un Inter(B) = (INT C:B. A Un C)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   802
\tdx{Int_Inter_image}   (INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   803
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   804
\caption{Set equalities} \label{hol-equalities}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   805
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   806
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   807
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   808
Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules.  Most are
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   809
obvious and resemble rules of Isabelle's {\ZF} set theory.  Certain rules,
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   810
such as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI},
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   811
are designed for classical reasoning; the rules \tdx{subsetD},
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   812
\tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are not
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   813
strictly necessary but yield more natural proofs.  Similarly,
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   814
\tdx{equalityCE} supports classical reasoning about extensionality,
344
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   815
after the fashion of \tdx{iffCE}.  See the file {\tt HOL/Set.ML} for
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   816
proofs pertaining to set theory.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   817
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   818
Figure~\ref{hol-fun} presents derived inference rules involving functions.
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   819
They also include rules for \cdx{Inv}, which is defined in theory~{\tt
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   820
  HOL}; note that ${\tt Inv}(f)$ applies the Axiom of Choice to yield an
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   821
inverse of~$f$.  They also include natural deduction rules for the image
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   822
and range operators, and for the predicates {\tt inj} and {\tt inj_onto}.
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   823
Reasoning about function composition (the operator~\sdx{o}) and the
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   824
predicate~\cdx{surj} is done simply by expanding the definitions.  See
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   825
the file {\tt HOL/fun.ML} for a complete listing of the derived rules.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   826
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   827
Figure~\ref{hol-subset} presents lattice properties of the subset relation.
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   828
Unions form least upper bounds; non-empty intersections form greatest lower
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   829
bounds.  Reasoning directly about subsets often yields clearer proofs than
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   830
reasoning about the membership relation.  See the file {\tt HOL/subset.ML}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   831
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   832
Figure~\ref{hol-equalities} presents many common set equalities.  They
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   833
include commutative, associative and distributive laws involving unions,
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   834
intersections and complements.  The proofs are mostly trivial, using the
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   835
classical reasoner; see file {\tt HOL/equalities.ML}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   836
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   837
287
6b62a6ddbe15 first draft of Springer book
lcp
parents: 154
diff changeset
   838
\begin{figure}
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   839
\begin{constants}
344
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   840
  \it symbol    & \it meta-type &           & \it description \\ 
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   841
  \cdx{Pair}    & $[\alpha,\beta]\To \alpha\times\beta$
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   842
        & & ordered pairs $\langle a,b\rangle$ \\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   843
  \cdx{fst}     & $\alpha\times\beta \To \alpha$        & & first projection\\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   844
  \cdx{snd}     & $\alpha\times\beta \To \beta$         & & second projection\\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   845
  \cdx{split}   & $[\alpha\times\beta, [\alpha,\beta]\To\gamma] \To \gamma$ 
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   846
        & & generalized projection\\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   847
  \cdx{Sigma}  & 
287
6b62a6ddbe15 first draft of Springer book
lcp
parents: 154
diff changeset
   848
        $[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ &
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   849
        & general sum of sets
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   850
\end{constants}
287
6b62a6ddbe15 first draft of Springer book
lcp
parents: 154
diff changeset
   851
\begin{ttbox}\makeatletter
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   852
\tdx{fst_def}      fst(p)     == @a. ? b. p = <a,b>
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   853
\tdx{snd_def}      snd(p)     == @b. ? a. p = <a,b>
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   854
\tdx{split_def}    split(p,c) == c(fst(p),snd(p))
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   855
\tdx{Sigma_def}    Sigma(A,B) == UN x:A. UN y:B(x). \{<x,y>\}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   856
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   857
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   858
\tdx{Pair_inject}  [| <a, b> = <a',b'>;  [| a=a';  b=b' |] ==> R |] ==> R
349
0ddc495e8b83 post-CRC corrections
lcp
parents: 344
diff changeset
   859
\tdx{fst_conv}     fst(<a,b>) = a
0ddc495e8b83 post-CRC corrections
lcp
parents: 344
diff changeset
   860
\tdx{snd_conv}     snd(<a,b>) = b
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   861
\tdx{split}        split(<a,b>, c) = c(a,b)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   862
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   863
\tdx{surjective_pairing}  p = <fst(p),snd(p)>
287
6b62a6ddbe15 first draft of Springer book
lcp
parents: 154
diff changeset
   864
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   865
\tdx{SigmaI}       [| a:A;  b:B(a) |] ==> <a,b> : Sigma(A,B)
287
6b62a6ddbe15 first draft of Springer book
lcp
parents: 154
diff changeset
   866
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   867
\tdx{SigmaE}       [| c: Sigma(A,B);  
287
6b62a6ddbe15 first draft of Springer book
lcp
parents: 154
diff changeset
   868
                !!x y.[| x:A; y:B(x); c=<x,y> |] ==> P |] ==> P
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   869
\end{ttbox}
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   870
\caption{Type $\alpha\times\beta$}\label{hol-prod}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   871
\end{figure} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   872
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   873
287
6b62a6ddbe15 first draft of Springer book
lcp
parents: 154
diff changeset
   874
\begin{figure}
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   875
\begin{constants}
344
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   876
  \it symbol    & \it meta-type &           & \it description \\ 
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   877
  \cdx{Inl}     & $\alpha \To \alpha+\beta$    & & first injection\\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   878
  \cdx{Inr}     & $\beta \To \alpha+\beta$     & & second injection\\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   879
  \cdx{sum_case} & $[\alpha+\beta, \alpha\To\gamma, \beta\To\gamma] \To\gamma$
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   880
        & & conditional
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   881
\end{constants}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   882
\begin{ttbox}\makeatletter
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   883
\tdx{sum_case_def}   sum_case == (\%p f g. @z. (!x. p=Inl(x) --> z=f(x)) &
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   884
                                        (!y. p=Inr(y) --> z=g(y)))
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   885
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   886
\tdx{Inl_not_Inr}    ~ Inl(a)=Inr(b)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   887
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   888
\tdx{inj_Inl}        inj(Inl)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   889
\tdx{inj_Inr}        inj(Inr)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   890
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   891
\tdx{sumE}           [| !!x::'a. P(Inl(x));  !!y::'b. P(Inr(y)) |] ==> P(s)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   892
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   893
\tdx{sum_case_Inl}   sum_case(Inl(x), f, g) = f(x)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   894
\tdx{sum_case_Inr}   sum_case(Inr(x), f, g) = g(x)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   895
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   896
\tdx{surjective_sum} sum_case(s, \%x::'a. f(Inl(x)), \%y::'b. f(Inr(y))) = f(s)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   897
\end{ttbox}
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   898
\caption{Type $\alpha+\beta$}\label{hol-sum}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   899
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   900
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   901
344
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   902
\section{Generic packages and classical reasoning}
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   903
\HOL\ instantiates most of Isabelle's generic packages;
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   904
see {\tt HOL/ROOT.ML} for details.
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   905
\begin{itemize}
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   906
\item 
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   907
Because it includes a general substitution rule, \HOL\ instantiates the
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   908
tactic {\tt hyp_subst_tac}, which substitutes for an equality
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   909
throughout a subgoal and its hypotheses.
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   910
\item 
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   911
It instantiates the simplifier, defining~\ttindexbold{HOL_ss} as the
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   912
simplification set for higher-order logic.  Equality~($=$), which also
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   913
expresses logical equivalence, may be used for rewriting.  See the file
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   914
{\tt HOL/simpdata.ML} for a complete listing of the simplification
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   915
rules. 
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   916
\item 
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   917
It instantiates the classical reasoner, as described below. 
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   918
\end{itemize}
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   919
\HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   920
well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   921
rule; recall Fig.\ts\ref{hol-lemmas2} above.
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   922
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   923
The classical reasoner is set up as the structure
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   924
{\tt Classical}.  This structure is open, so {\ML} identifiers such
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   925
as {\tt step_tac}, {\tt fast_tac}, {\tt best_tac}, etc., refer to it.
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   926
\HOL\ defines the following classical rule sets:
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   927
\begin{ttbox} 
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   928
prop_cs    : claset
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   929
HOL_cs     : claset
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   930
HOL_dup_cs : claset
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   931
set_cs     : claset
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   932
\end{ttbox}
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   933
\begin{ttdescription}
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   934
\item[\ttindexbold{prop_cs}] contains the propositional rules, namely
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   935
those for~$\top$, $\bot$, $\conj$, $\disj$, $\neg$, $\imp$ and~$\bimp$,
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   936
along with the rule~{\tt refl}.
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   937
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   938
\item[\ttindexbold{HOL_cs}] extends {\tt prop_cs} with the safe rules
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   939
  {\tt allI} and~{\tt exE} and the unsafe rules {\tt allE}
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   940
  and~{\tt exI}, as well as rules for unique existence.  Search using
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   941
  this classical set is incomplete: quantified formulae are used at most
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   942
  once.
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   943
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   944
\item[\ttindexbold{HOL_dup_cs}] extends {\tt prop_cs} with the safe rules
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   945
  {\tt allI} and~{\tt exE} and the unsafe rules \tdx{all_dupE}
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   946
  and~\tdx{exCI}, as well as rules for unique existence.  Search using
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   947
  this is complete --- quantified formulae may be duplicated --- but
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   948
  frequently fails to terminate.  It is generally unsuitable for
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   949
  depth-first search.
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   950
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   951
\item[\ttindexbold{set_cs}] extends {\tt HOL_cs} with rules for the bounded
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   952
  quantifiers, subsets, comprehensions, unions and intersections,
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   953
  complements, finite sets, images and ranges.
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   954
\end{ttdescription}
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   955
\noindent
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   956
See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   957
        {Chap.\ts\ref{chap:classical}} 
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   958
for more discussion of classical proof methods.
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   959
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   960
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   961
\section{Types}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   962
The basic higher-order logic is augmented with a tremendous amount of
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   963
material, including support for recursive function and type definitions.  A
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   964
detailed discussion appears elsewhere~\cite{paulson-coind}.  The simpler
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   965
definitions are the same as those used the {\sc hol} system, but my
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   966
treatment of recursive types differs from Melham's~\cite{melham89}.  The
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   967
present section describes product, sum, natural number and list types.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   968
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   969
\subsection{Product and sum types}\index{*"* type}\index{*"+ type}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   970
Theory \thydx{Prod} defines the product type $\alpha\times\beta$, with
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   971
the ordered pair syntax {\tt<$a$,$b$>}.  Theory \thydx{Sum} defines the
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   972
sum type $\alpha+\beta$.  These use fairly standard constructions; see
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   973
Figs.\ts\ref{hol-prod} and~\ref{hol-sum}.  Because Isabelle does not
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   974
support abstract type definitions, the isomorphisms between these types and
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   975
their representations are made explicitly.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   976
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   977
Most of the definitions are suppressed, but observe that the projections
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   978
and conditionals are defined as descriptions.  Their properties are easily
344
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   979
proved using \tdx{select_equality}.  
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   980
287
6b62a6ddbe15 first draft of Springer book
lcp
parents: 154
diff changeset
   981
\begin{figure} 
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   982
\index{*"< symbol}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   983
\index{*"* symbol}
344
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   984
\index{*div symbol}
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   985
\index{*mod symbol}
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   986
\index{*"+ symbol}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   987
\index{*"- symbol}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   988
\begin{constants}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   989
  \it symbol    & \it meta-type & \it priority & \it description \\ 
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   990
  \cdx{0}       & $nat$         & & zero \\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   991
  \cdx{Suc}     & $nat \To nat$ & & successor function\\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   992
  \cdx{nat_case} & $[nat, \alpha, nat\To\alpha] \To\alpha$
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   993
        & & conditional\\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   994
  \cdx{nat_rec} & $[nat, \alpha, [nat, \alpha]\To\alpha] \To \alpha$
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   995
        & & primitive recursor\\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
   996
  \cdx{pred_nat} & $(nat\times nat) set$ & & predecessor relation\\
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   997
  \tt *         & $[nat,nat]\To nat$    &  Left 70      & multiplication \\
344
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   998
  \tt div       & $[nat,nat]\To nat$    &  Left 70      & division\\
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
   999
  \tt mod       & $[nat,nat]\To nat$    &  Left 70      & modulus\\
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1000
  \tt +         & $[nat,nat]\To nat$    &  Left 65      & addition\\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
  1001
  \tt -         & $[nat,nat]\To nat$    &  Left 65      & subtraction
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1002
\end{constants}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1003
\subcaption{Constants and infixes}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1004
287
6b62a6ddbe15 first draft of Springer book
lcp
parents: 154
diff changeset
  1005
\begin{ttbox}\makeatother
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1006
\tdx{nat_case_def}  nat_case == (\%n a f. @z. (n=0 --> z=a) & 
344
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
  1007
                                       (!x. n=Suc(x) --> z=f(x)))
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1008
\tdx{pred_nat_def}  pred_nat == \{p. ? n. p = <n, Suc(n)>\} 
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1009
\tdx{less_def}      m<n      == <m,n>:pred_nat^+
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1010
\tdx{nat_rec_def}   nat_rec(n,c,d) == 
287
6b62a6ddbe15 first draft of Springer book
lcp
parents: 154
diff changeset
  1011
               wfrec(pred_nat, n, \%l g.nat_case(l, c, \%m.d(m,g(m))))
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1012
344
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
  1013
\tdx{add_def}   m+n     == nat_rec(m, n, \%u v.Suc(v))
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
  1014
\tdx{diff_def}  m-n     == nat_rec(n, m, \%u v. nat_rec(v, 0, \%x y.x))
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
  1015
\tdx{mult_def}  m*n     == nat_rec(m, 0, \%u v. n + v)
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
  1016
\tdx{mod_def}   m mod n == wfrec(trancl(pred_nat), m, \%j f. if(j<n,j,f(j-n)))
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
  1017
\tdx{quo_def}   m div n == wfrec(trancl(pred_nat), 
287
6b62a6ddbe15 first draft of Springer book
lcp
parents: 154
diff changeset
  1018
                        m, \%j f. if(j<n,0,Suc(f(j-n))))
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1019
\subcaption{Definitions}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1020
\end{ttbox}
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1021
\caption{Defining {\tt nat}, the type of natural numbers} \label{hol-nat1}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1022
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1023
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1024
287
6b62a6ddbe15 first draft of Springer book
lcp
parents: 154
diff changeset
  1025
\begin{figure} \underscoreon
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1026
\begin{ttbox}
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1027
\tdx{nat_induct}     [| P(0); !!k. [| P(k) |] ==> P(Suc(k)) |]  ==> P(n)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1028
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1029
\tdx{Suc_not_Zero}   Suc(m) ~= 0
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1030
\tdx{inj_Suc}        inj(Suc)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1031
\tdx{n_not_Suc_n}    n~=Suc(n)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1032
\subcaption{Basic properties}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1033
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1034
\tdx{pred_natI}      <n, Suc(n)> : pred_nat
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1035
\tdx{pred_natE}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1036
    [| p : pred_nat;  !!x n. [| p = <n, Suc(n)> |] ==> R |] ==> R
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1037
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1038
\tdx{nat_case_0}     nat_case(0, a, f) = a
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1039
\tdx{nat_case_Suc}   nat_case(Suc(k), a, f) = f(k)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1040
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1041
\tdx{wf_pred_nat}    wf(pred_nat)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1042
\tdx{nat_rec_0}      nat_rec(0,c,h) = c
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1043
\tdx{nat_rec_Suc}    nat_rec(Suc(n), c, h) = h(n, nat_rec(n,c,h))
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1044
\subcaption{Case analysis and primitive recursion}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1045
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1046
\tdx{less_trans}     [| i<j;  j<k |] ==> i<k
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1047
\tdx{lessI}          n < Suc(n)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1048
\tdx{zero_less_Suc}  0 < Suc(n)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1049
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1050
\tdx{less_not_sym}   n<m --> ~ m<n 
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1051
\tdx{less_not_refl}  ~ n<n
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1052
\tdx{not_less0}      ~ n<0
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1053
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1054
\tdx{Suc_less_eq}    (Suc(m) < Suc(n)) = (m<n)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1055
\tdx{less_induct}    [| !!n. [| ! m. m<n --> P(m) |] ==> P(n) |]  ==>  P(n)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1056
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1057
\tdx{less_linear}    m<n | m=n | n<m
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1058
\subcaption{The less-than relation}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1059
\end{ttbox}
344
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
  1060
\caption{Derived rules for {\tt nat}} \label{hol-nat2}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1061
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1062
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1063
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1064
\subsection{The type of natural numbers, {\tt nat}}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1065
The theory \thydx{Nat} defines the natural numbers in a roundabout but
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1066
traditional way.  The axiom of infinity postulates an type~\tydx{ind} of
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1067
individuals, which is non-empty and closed under an injective operation.
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1068
The natural numbers are inductively generated by choosing an arbitrary
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1069
individual for~0 and using the injective operation to take successors.  As
344
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
  1070
usual, the isomorphisms between~\tydx{nat} and its representation are made
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1071
explicitly.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1072
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1073
The definition makes use of a least fixed point operator \cdx{lfp},
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1074
defined using the Knaster-Tarski theorem.  This is used to define the
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1075
operator \cdx{trancl}, for taking the transitive closure of a relation.
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1076
Primitive recursion makes use of \cdx{wfrec}, an operator for recursion
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1077
along arbitrary well-founded relations.  The corresponding theories are
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1078
called {\tt Lfp}, {\tt Trancl} and {\tt WF}\@.  Elsewhere I have described
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1079
similar constructions in the context of set theory~\cite{paulson-set-II}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1080
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1081
Type~\tydx{nat} is postulated to belong to class~\cldx{ord}, which
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1082
overloads $<$ and $\leq$ on the natural numbers.  As of this writing,
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1083
Isabelle provides no means of verifying that such overloading is sensible;
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1084
there is no means of specifying the operators' properties and verifying
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1085
that instances of the operators satisfy those properties.  To be safe, the
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1086
\HOL\ theory includes no polymorphic axioms asserting general properties of
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1087
$<$ and~$\leq$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1088
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1089
Theory \thydx{Arith} develops arithmetic on the natural numbers.  It
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1090
defines addition, multiplication, subtraction, division, and remainder.
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1091
Many of their properties are proved: commutative, associative and
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1092
distributive laws, identity and cancellation laws, etc.  The most
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1093
interesting result is perhaps the theorem $a \bmod b + (a/b)\times b = a$.
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1094
Division and remainder are defined by repeated subtraction, which requires
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1095
well-founded rather than primitive recursion.  See Figs.\ts\ref{hol-nat1}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1096
and~\ref{hol-nat2}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1097
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1098
The predecessor relation, \cdx{pred_nat}, is shown to be well-founded.
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1099
Recursion along this relation resembles primitive recursion, but is
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1100
stronger because we are in higher-order logic; using primitive recursion to
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1101
define a higher-order function, we can easily Ackermann's function, which
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1102
is not primitive recursive \cite[page~104]{thompson91}.
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1103
The transitive closure of \cdx{pred_nat} is~$<$.  Many functions on the
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1104
natural numbers are most easily expressed using recursion along~$<$.
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1105
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1106
The tactic {\tt\ttindex{nat_ind_tac} "$n$" $i$} performs induction over the
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1107
variable~$n$ in subgoal~$i$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1108
287
6b62a6ddbe15 first draft of Springer book
lcp
parents: 154
diff changeset
  1109
\begin{figure}
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1110
\index{#@{\tt\#} symbol}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1111
\index{"@@{\tt\at} symbol}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1112
\begin{constants}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1113
  \it symbol & \it meta-type & \it priority & \it description \\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1114
  \cdx{Nil}     & $\alpha list$ & & empty list\\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1115
  \tt \#   & $[\alpha,\alpha list]\To \alpha list$ & Right 65 & 
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1116
        list constructor \\
344
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
  1117
  \cdx{null}    & $\alpha list \To bool$ & & emptiness test\\
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1118
  \cdx{hd}      & $\alpha list \To \alpha$ & & head \\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1119
  \cdx{tl}      & $\alpha list \To \alpha list$ & & tail \\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1120
  \cdx{ttl}     & $\alpha list \To \alpha list$ & & total tail \\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1121
  \tt\at  & $[\alpha list,\alpha list]\To \alpha list$ & Left 65 & append \\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1122
  \sdx{mem}  & $[\alpha,\alpha list]\To bool$    &  Left 55   & membership\\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1123
  \cdx{map}     & $(\alpha\To\beta) \To (\alpha list \To \beta list)$
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1124
        & & mapping functional\\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1125
  \cdx{filter}  & $(\alpha \To bool) \To (\alpha list \To \alpha list)$
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1126
        & & filter functional\\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1127
  \cdx{list_all}& $(\alpha \To bool) \To (\alpha list \To bool)$
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1128
        & & forall functional\\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1129
  \cdx{list_rec}        & $[\alpha list, \beta, [\alpha ,\alpha list,
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1130
\beta]\To\beta] \To \beta$
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1131
        & & list recursor
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1132
\end{constants}
306
eee166d4a532 changed lists and added "let" and "case"
nipkow
parents: 287
diff changeset
  1133
\subcaption{Constants and infixes}
eee166d4a532 changed lists and added "let" and "case"
nipkow
parents: 287
diff changeset
  1134
eee166d4a532 changed lists and added "let" and "case"
nipkow
parents: 287
diff changeset
  1135
\begin{center} \tt\frenchspacing
eee166d4a532 changed lists and added "let" and "case"
nipkow
parents: 287
diff changeset
  1136
\begin{tabular}{rrr} 
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1137
  \it external        & \it internal  & \it description \\{}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1138
  \sdx{[]}            & Nil           & \rm empty list \\{}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1139
  [$x@1$, $\dots$, $x@n$]  &  $x@1$ \# $\cdots$ \# $x@n$ \# [] &
306
eee166d4a532 changed lists and added "let" and "case"
nipkow
parents: 287
diff changeset
  1140
        \rm finite list \\{}
344
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
  1141
  [$x$:$l$. $P$]  & filter($\lambda x{.}P$, $l$) & 
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1142
        \rm list comprehension
306
eee166d4a532 changed lists and added "let" and "case"
nipkow
parents: 287
diff changeset
  1143
\end{tabular}
eee166d4a532 changed lists and added "let" and "case"
nipkow
parents: 287
diff changeset
  1144
\end{center}
eee166d4a532 changed lists and added "let" and "case"
nipkow
parents: 287
diff changeset
  1145
\subcaption{Translations}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1146
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1147
\begin{ttbox}
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1148
\tdx{list_induct}    [| P([]);  !!x xs. [| P(xs) |] ==> P(x#xs)) |]  ==> P(l)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1149
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1150
\tdx{Cons_not_Nil}   (x # xs) ~= []
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1151
\tdx{Cons_Cons_eq}   ((x # xs) = (y # ys)) = (x=y & xs=ys)
306
eee166d4a532 changed lists and added "let" and "case"
nipkow
parents: 287
diff changeset
  1152
\subcaption{Induction and freeness}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1153
\end{ttbox}
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1154
\caption{The theory \thydx{List}} \label{hol-list}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1155
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1156
306
eee166d4a532 changed lists and added "let" and "case"
nipkow
parents: 287
diff changeset
  1157
\begin{figure}
eee166d4a532 changed lists and added "let" and "case"
nipkow
parents: 287
diff changeset
  1158
\begin{ttbox}\makeatother
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1159
\tdx{list_rec_Nil}      list_rec([],c,h) = c  
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1160
\tdx{list_rec_Cons}     list_rec(a \# l, c, h) = h(a, l, list_rec(l,c,h))
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1161
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1162
\tdx{list_case_Nil}     list_case([],c,h) = c 
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1163
\tdx{list_case_Cons}    list_case(x # xs, c, h) = h(x, xs)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1164
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1165
\tdx{map_Nil}           map(f,[]) = []
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1166
\tdx{map_Cons}          map(f, x \# xs) = f(x) \# map(f,xs)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1167
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1168
\tdx{null_Nil}          null([]) = True
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1169
\tdx{null_Cons}         null(x # xs) = False
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1170
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1171
\tdx{hd_Cons}           hd(x # xs) = x
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1172
\tdx{tl_Cons}           tl(x # xs) = xs
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1173
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1174
\tdx{ttl_Nil}           ttl([]) = []
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1175
\tdx{ttl_Cons}          ttl(x # xs) = xs
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1176
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1177
\tdx{append_Nil}        [] @ ys = ys
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1178
\tdx{append_Cons}       (x # xs) \at ys = x # xs \at ys
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1179
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1180
\tdx{mem_Nil}           x mem [] = False
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1181
\tdx{mem_Cons}          x mem y # ys = if(y = x, True, x mem ys)
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1182
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1183
\tdx{filter_Nil}        filter(P, []) = []
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1184
\tdx{filter_Cons}       filter(P,x#xs) = if(P(x),x#filter(P,xs),filter(P,xs))
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1185
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1186
\tdx{list_all_Nil}      list_all(P,[]) = True
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1187
\tdx{list_all_Cons}     list_all(P, x # xs) = (P(x) & list_all(P, xs))
306
eee166d4a532 changed lists and added "let" and "case"
nipkow
parents: 287
diff changeset
  1188
\end{ttbox}
eee166d4a532 changed lists and added "let" and "case"
nipkow
parents: 287
diff changeset
  1189
\caption{Rewrite rules for lists} \label{hol-list-simps}
eee166d4a532 changed lists and added "let" and "case"
nipkow
parents: 287
diff changeset
  1190
\end{figure}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1191
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1192
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1193
\subsection{The type constructor for lists, {\tt list}}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1194
\index{*list type}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1195
306
eee166d4a532 changed lists and added "let" and "case"
nipkow
parents: 287
diff changeset
  1196
\HOL's definition of lists is an example of an experimental method for
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1197
handling recursive data types.  Figure~\ref{hol-list} presents the theory
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1198
\thydx{List}: the basic list operations with their types and properties.
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1199
344
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
  1200
The \sdx{case} construct is defined by the following translation:
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1201
{\dquotes
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1202
\begin{eqnarray*}
344
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
  1203
  \begin{array}{r@{\;}l@{}l}
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1204
  "case " e " of" & "[]"    & " => " a\\
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1205
              "|" & x"\#"xs & " => " b
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1206
  \end{array} 
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1207
  & \equiv &
344
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
  1208
  "list_case"(e, a, \lambda x\;xs.b)
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
  1209
\end{eqnarray*}}%
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1210
The theory includes \cdx{list_rec}, a primitive recursion operator
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1211
for lists.  It is derived from well-founded recursion, a general principle
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1212
that can express arbitrary total recursive functions.
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1213
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1214
The simpset \ttindex{list_ss} contains, along with additional useful lemmas,
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1215
the basic rewrite rules that appear in Fig.\ts\ref{hol-list-simps}.
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1216
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1217
The tactic {\tt\ttindex{list_ind_tac} "$xs$" $i$} performs induction over the
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1218
variable~$xs$ in subgoal~$i$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1219
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1220
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1221
\subsection{The type constructor for lazy lists, {\tt llist}}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1222
\index{*llist type}
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1223
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1224
The definition of lazy lists demonstrates methods for handling infinite
344
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
  1225
data structures and coinduction in higher-order logic.  Theory
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
  1226
\thydx{LList} defines an operator for corecursion on lazy lists, which is
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
  1227
used to define a few simple functions such as map and append.  Corecursion
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
  1228
cannot easily define operations such as filter, which can compute
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
  1229
indefinitely before yielding the next element (if any!) of the lazy list.
753b50b07c46 final Springer copy
lcp
parents: 315
diff changeset
  1230
A coinduction principle is defined for proving equations on lazy lists.
315
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1231
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1232
I have written a paper discussing the treatment of lazy lists; it also
ebf62069d889 penultimate Springer draft
lcp
parents: 306
diff changeset
  1233
covers finite lists~\cite{paulson-coind}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1234
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1235
464
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1236
\section{Datatype declarations}
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1237
\index{*datatype|(}
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1238
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1239
\underscoreon
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1240
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1241
It is often necessary to extend a theory with \ML-like datatypes.  This
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1242
extension consists of the new type, declarations of its constructors and
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1243
rules that describe the new type. The theory definition section {\tt
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1244
  datatype} represents a compact way of doing this.
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1245
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1246
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1247
\subsection{Foundations}
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1248
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1249
A datatype declaration has the following general structure:
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1250
\[ \mbox{\tt datatype}~ (\alpha_1,\dots,\alpha_n)t ~=~
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1251
      c_1(\tau_{11},\dots,\tau_{1k_1}) ~\mid~ \dots ~\mid~
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1252
      c_m(\tau_{m1},\dots,\tau_{mk_m}) 
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1253
\]
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1254
where $\alpha_i$ are type variables, $c_i$ are distinct constructor names and
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1255
$\tau_{ij}$ are one of the following:
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1256
\begin{itemize}
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1257
\item type variables $\alpha_1,\dots,\alpha_n$,
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1258
\item types $(\beta_1,\dots,\beta_l)s$ where $s$ is a previously declared
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1259
  type or type synonym and $\{\beta_1,\dots,\beta_l\} \subseteq
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1260
  \{\alpha_1,\dots,\alpha_n\}$,
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1261
\item the newly defined type $(\alpha_1,\dots,\alpha_n)t$ \footnote{This
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1262
    makes it a recursive type. To ensure that the new type is not empty at
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1263
    least one constructor must consist of only non-recursive type
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1264
    components.}
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1265
\end{itemize}
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1266
The constructors are automatically defined as functions of their respective
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1267
type:
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1268
\[ c_j : [\tau_{j1},\dots,\tau_{jk_j}] \To (\alpha_1,\dots,\alpha_n)t \]
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1269
These functions have certain {\em freeness} properties:
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1270
\begin{description}
465
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 464
diff changeset
  1271
\item[\tt distinct] They are distinct:
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 464
diff changeset
  1272
\[ c_i(x_1,\dots,x_{k_i}) \neq c_j(y_1,\dots,y_{k_j}) \qquad
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 464
diff changeset
  1273
   \mbox{for all}~ i \neq j.
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 464
diff changeset
  1274
\]
464
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1275
\item[\tt inject] They are injective:
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1276
\[ (c_j(x_1,\dots,x_{k_j}) = c_j(y_1,\dots,y_{k_j})) =
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1277
   (x_1 = y_1 \land \dots \land x_{k_j} = y_{k_j})
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1278
\]
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1279
\end{description}
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1280
Because the number of inequalities is quadratic in the number of
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1281
constructors, a different method is used if their number exceeds
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1282
a certain value, currently 4. In that case every constructor is mapped to a
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1283
natural number
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1284
\[
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1285
\begin{array}{lcl}
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1286
\mbox{\it t\_ord}(c_1(x_1,\dots,x_{k_1})) & = & 0 \\
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1287
& \vdots & \\
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1288
\mbox{\it t\_ord}(c_m(x_1,\dots,x_{k_m})) & = & m-1
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1289
\end{array}
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1290
\]
465
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 464
diff changeset
  1291
and distinctness of constructors is expressed by:
464
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1292
\[
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1293
\mbox{\it t\_ord}(x) \neq \mbox{\it t\_ord}(y) \Imp x \neq y.
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1294
\]
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1295
In addition a structural induction axiom {\tt induct} is provided: 
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1296
\[
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1297
\infer{P(x)}
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1298
{\begin{array}{lcl}
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1299
\Forall x_1\dots x_{k_1}.
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1300
  \List{P(x_{r_{11}}); \dots; P(x_{r_{1l_1}})} &
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1301
  \Imp  & P(c_1(x_1,\dots,x_{k_1})) \\
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1302
 & \vdots & \\
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1303
\Forall x_1\dots x_{k_m}.
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1304
  \List{P(x_{r_{m1}}); \dots; P(x_{r_{ml_m}})} &
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1305
  \Imp & P(c_m(x_1,\dots,x_{k_m}))
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1306
\end{array}}
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1307
\]
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1308
where $\{r_{j1},\dots,r_{jl_j}\} = \{i \in \{1,\dots k_j\} ~\mid~ \tau_{ji}
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1309
= (\alpha_1,\dots,\alpha_n)t \}$, i.e.\ the property $P$ can be assumed for
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1310
all arguments of the recursive type.
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1311
465
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 464
diff changeset
  1312
The type also comes with an \ML-like \sdx{case}-construct:
464
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1313
\[
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1314
\begin{array}{rrcl}
465
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 464
diff changeset
  1315
\mbox{\tt case}~e~\mbox{\tt of} & c_1(x_{11},\dots,x_{1k_1}) & \To & e_1 \\
464
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1316
                           \vdots \\
465
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 464
diff changeset
  1317
                           \mid & c_m(x_{m1},\dots,x_{mk_m}) & \To & e_m
464
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1318
\end{array}
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1319
\]
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1320
In contrast to \ML, {\em all} constructors must be present, their order is
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1321
fixed, and nested patterns are not supported.
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1322
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1323
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1324
\subsection{Defining datatypes}
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1325
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1326
A datatype is defined in a theory definition file using the keyword {\tt
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1327
  datatype}. The definition following {\tt datatype} must conform to the
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1328
syntax of {\em typedecl} specified in Fig.~\ref{datatype-grammar} and must
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1329
obey the rules in the previous section. As a result the theory is extended
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1330
with the new type, the constructors, and the theorems listed in the previous
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1331
section.
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1332
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1333
\begin{figure}
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1334
\begin{rail}
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1335
typedecl : typevarlist id '=' (cons + '|')
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1336
         ;
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1337
cons     : (id | string) ( () | '(' (typ + ',') ')' ) ( () | mixfix )
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1338
         ;
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1339
typ      : typevarlist id
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1340
           | tid
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1341
	 ;
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1342
typevarlist : () | tid | '(' (tid + ',') ')'
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1343
         ;
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1344
\end{rail}
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1345
\caption{Syntax of datatype declarations}
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1346
\label{datatype-grammar}
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1347
\end{figure}
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1348
465
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 464
diff changeset
  1349
Reading the theory file produces a structure which, in addition to the usual
464
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1350
components, contains a structure named $t$ for each datatype $t$ defined in
465
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 464
diff changeset
  1351
the file.\footnote{Otherwise multiple datatypes in the same theory file would
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 464
diff changeset
  1352
  lead to name clashes.} Each structure $t$ contains the following elements:
464
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1353
\begin{ttbox}
465
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 464
diff changeset
  1354
val distinct : thm list
464
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1355
val inject : thm list
465
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 464
diff changeset
  1356
val induct : thm
464
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1357
val cases : thm list
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1358
val simps : thm list
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1359
val induct_tac : string -> int -> tactic
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1360
\end{ttbox}
465
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 464
diff changeset
  1361
{\tt distinct}, {\tt inject} and {\tt induct} contain the theorems described
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 464
diff changeset
  1362
above. For convenience {\tt distinct} contains inequalities in both
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 464
diff changeset
  1363
directions.
464
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1364
\begin{warn}
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1365
  If there are five or more constructors, the {\em t\_ord} scheme is used for
465
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 464
diff changeset
  1366
  {\tt distinct}.  In this case the theory {\tt Arith} must be contained
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 464
diff changeset
  1367
  in the current theory, if necessary by including it explicitly.
464
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1368
\end{warn}
465
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 464
diff changeset
  1369
The reduction rules of the {\tt case}-construct are in {\tt cases}.  All
d4bf81734dfe Corrected HOL.tex
nipkow
parents: 464
diff changeset
  1370
theorems from {\tt distinct}, {\tt inject} and {\tt cases} are combined in
464
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1371
{\tt simps} for use with the simplifier. The tactic ``{\verb$induct_tac$~{\em
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1372
    var i}\/}'' applies structural induction over variable {\em var} to
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1373
subgoal {\em i}.
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1374
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1375
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1376
\subsection{Examples}
552717636da4 added datatype section
nipkow
parents: 453
diff changeset
  1377
<