doc-src/Logics/HOL.tex
author nipkow
Thu, 16 Oct 1997 13:13:03 +0200
changeset 3881 73be08b4da3f
parent 3489 afa802078173
child 3959 033633d9a032
permissions -rw-r--r--
Added last, butlast, dropped ttl.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
     1
%% $Id$
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
     2
\chapter{Higher-Order Logic}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
     3
\index{higher-order logic|(}
1163
c080ff36d24e changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents: 1162
diff changeset
     4
\index{HOL system@{\sc hol} system}
1162
7be0684950a3 changes made by Lawrence Paulson
clasohm
parents: 1113
diff changeset
     5
7be0684950a3 changes made by Lawrence Paulson
clasohm
parents: 1113
diff changeset
     6
The theory~\thydx{HOL} implements higher-order logic.  It is based on
7be0684950a3 changes made by Lawrence Paulson
clasohm
parents: 1113
diff changeset
     7
Gordon's~{\sc hol} system~\cite{mgordon-hol}, which itself is based on
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
     8
Church's original paper~\cite{church40}.  Andrews's
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
     9
book~\cite{andrews86} is a full description of the original
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
    10
Church-style higher-order logic.  Experience with the {\sc hol} system
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
    11
has demonstrated that higher-order logic is widely applicable in many
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
    12
areas of mathematics and computer science, not just hardware
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
    13
verification, {\sc hol}'s original \textit{raison d'\^etre\/}.  It is
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
    14
weaker than {\ZF} set theory but for most applications this does not
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
    15
matter.  If you prefer {\ML} to Lisp, you will probably prefer \HOL\ 
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
    16
to~{\ZF}.
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    17
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
    18
The syntax of \HOL\footnote{Earlier versions of Isabelle's \HOL\ used a
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
    19
different syntax.  Ancient releases of Isabelle included still another version
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
    20
of~\HOL, with explicit type inference rules~\cite{paulson-COLOG}.  This
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
    21
version no longer exists, but \thydx{ZF} supports a similar style of
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
    22
reasoning.} follows $\lambda$-calculus and functional programming.  Function
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
    23
application is curried.  To apply the function~$f$ of type
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
    24
$\tau@1\To\tau@2\To\tau@3$ to the arguments~$a$ and~$b$ in \HOL, you simply
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
    25
write $f\,a\,b$.  There is no `apply' operator as in \thydx{ZF}.  Note that
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
    26
$f(a,b)$ means ``$f$ applied to the pair $(a,b)$'' in \HOL.  We write ordered
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
    27
pairs as $(a,b)$, not $\langle a,b\rangle$ as in {\ZF}.
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    28
1162
7be0684950a3 changes made by Lawrence Paulson
clasohm
parents: 1113
diff changeset
    29
\HOL\ has a distinct feel, compared with {\ZF} and {\CTT}.  It
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    30
identifies object-level types with meta-level types, taking advantage of
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    31
Isabelle's built-in type checker.  It identifies object-level functions
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    32
with meta-level functions, so it uses Isabelle's operations for abstraction
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
    33
and application.
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    34
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
    35
These identifications allow Isabelle to support \HOL\ particularly
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
    36
nicely, but they also mean that \HOL\ requires more sophistication
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
    37
from the user --- in particular, an understanding of Isabelle's type
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
    38
system.  Beginners should work with \texttt{show_types} (or even
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
    39
\texttt{show_sorts}) set to \texttt{true}.
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
    40
%  Gain experience by
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
    41
%working in first-order logic before attempting to use higher-order logic.
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
    42
%This chapter assumes familiarity with~{\FOL{}}.
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    43
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    44
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
    45
\begin{figure}
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
    46
\begin{constants}
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
    47
  \it name      &\it meta-type  & \it description \\
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    48
  \cdx{Trueprop}& $bool\To prop$                & coercion to $prop$\\
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
    49
  \cdx{Not}     & $bool\To bool$                & negation ($\neg$) \\
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    50
  \cdx{True}    & $bool$                        & tautology ($\top$) \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    51
  \cdx{False}   & $bool$                        & absurdity ($\bot$) \\
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
    52
  \cdx{If}      & $[bool,\alpha,\alpha]\To\alpha$ & conditional \\
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    53
  \cdx{Let}     & $[\alpha,\alpha\To\beta]\To\beta$ & let binder
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
    54
\end{constants}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    55
\subcaption{Constants}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    56
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
    57
\begin{constants}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    58
\index{"@@{\tt\at} symbol}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    59
\index{*"! symbol}\index{*"? symbol}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    60
\index{*"?"! symbol}\index{*"E"X"! symbol}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    61
  \it symbol &\it name     &\it meta-type & \it description \\
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
    62
  \tt\at & \cdx{Eps}  & $(\alpha\To bool)\To\alpha$ & 
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
    63
        Hilbert description ($\varepsilon$) \\
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
    64
  {\tt!~} or \sdx{ALL}  & \cdx{All}  & $(\alpha\To bool)\To bool$ & 
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    65
        universal quantifier ($\forall$) \\
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
    66
  {\tt?~} or \sdx{EX}   & \cdx{Ex}   & $(\alpha\To bool)\To bool$ & 
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    67
        existential quantifier ($\exists$) \\
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
    68
  {\tt?!} or \texttt{EX!}  & \cdx{Ex1}  & $(\alpha\To bool)\To bool$ & 
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
    69
        unique existence ($\exists!$)\\
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
    70
  \texttt{LEAST}  & \cdx{Least}  & $(\alpha::ord \To bool)\To\alpha$ & 
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
    71
        least element
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
    72
\end{constants}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    73
\subcaption{Binders} 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    74
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
    75
\begin{constants}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    76
\index{*"= symbol}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    77
\index{&@{\tt\&} symbol}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    78
\index{*"| symbol}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    79
\index{*"-"-"> symbol}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    80
  \it symbol    & \it meta-type & \it priority & \it description \\ 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    81
  \sdx{o}       & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ & 
1234
56ee5cc35510 updated "o" in HOL: (infixl 55)
nipkow
parents: 1163
diff changeset
    82
        Left 55 & composition ($\circ$) \\
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
    83
  \tt =         & $[\alpha,\alpha]\To bool$ & Left 50 & equality ($=$) \\
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    84
  \tt <         & $[\alpha::ord,\alpha]\To bool$ & Left 50 & less than ($<$) \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    85
  \tt <=        & $[\alpha::ord,\alpha]\To bool$ & Left 50 & 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    86
                less than or equals ($\leq$)\\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    87
  \tt \&        & $[bool,bool]\To bool$ & Right 35 & conjunction ($\conj$) \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    88
  \tt |         & $[bool,bool]\To bool$ & Right 30 & disjunction ($\disj$) \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    89
  \tt -->       & $[bool,bool]\To bool$ & Right 25 & implication ($\imp$)
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
    90
\end{constants}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    91
\subcaption{Infixes}
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
    92
\caption{Syntax of \texttt{HOL}} \label{hol-constants}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    93
\end{figure}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    94
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    95
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    96
\begin{figure}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    97
\index{*let symbol}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    98
\index{*in symbol}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
    99
\dquotes
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   100
\[\begin{array}{rclcl}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   101
    term & = & \hbox{expression of class~$term$} \\
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   102
         & | & "\at~" id " . " formula \\
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   103
         & | & 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   104
    \multicolumn{3}{l}{"let"~id~"="~term";"\dots";"~id~"="~term~"in"~term} \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   105
         & | & 
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   106
    \multicolumn{3}{l}{"if"~formula~"then"~term~"else"~term} \\
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   107
         & | & "LEAST"~ id " . " formula \\[2ex]
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   108
 formula & = & \hbox{expression of type~$bool$} \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   109
         & | & term " = " term \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   110
         & | & term " \ttilde= " term \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   111
         & | & term " < " term \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   112
         & | & term " <= " term \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   113
         & | & "\ttilde\ " formula \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   114
         & | & formula " \& " formula \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   115
         & | & formula " | " formula \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   116
         & | & formula " --> " formula \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   117
         & | & "!~~~" id~id^* " . " formula 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   118
         & | & "ALL~" id~id^* " . " formula \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   119
         & | & "?~~~" id~id^* " . " formula 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   120
         & | & "EX~~" id~id^* " . " formula \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   121
         & | & "?!~~" id~id^* " . " formula 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   122
         & | & "EX!~" id~id^* " . " formula
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   123
  \end{array}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   124
\]
1163
c080ff36d24e changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents: 1162
diff changeset
   125
\caption{Full grammar for \HOL} \label{hol-grammar}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   126
\end{figure} 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   127
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   128
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   129
\section{Syntax}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   130
1163
c080ff36d24e changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents: 1162
diff changeset
   131
Figure~\ref{hol-constants} lists the constants (including infixes and
c080ff36d24e changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents: 1162
diff changeset
   132
binders), while Fig.\ts\ref{hol-grammar} presents the grammar of
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   133
higher-order logic.  Note that $a$\verb|~=|$b$ is translated to
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   134
$\neg(a=b)$.
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   135
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   136
\begin{warn}
1162
7be0684950a3 changes made by Lawrence Paulson
clasohm
parents: 1113
diff changeset
   137
  \HOL\ has no if-and-only-if connective; logical equivalence is expressed
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   138
  using equality.  But equality has a high priority, as befitting a
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   139
  relation, while if-and-only-if typically has the lowest priority.  Thus,
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   140
  $\neg\neg P=P$ abbreviates $\neg\neg (P=P)$ and not $(\neg\neg P)=P$.
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   141
  When using $=$ to mean logical equivalence, enclose both operands in
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   142
  parentheses.
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   143
\end{warn}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   144
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   145
\subsection{Types and classes}
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   146
The universal type class of higher-order terms is called~\cldx{term}.
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   147
By default, explicit type variables have class \cldx{term}.  In
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   148
particular the equality symbol and quantifiers are polymorphic over
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   149
class \texttt{term}.
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   150
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   151
The type of formulae, \tydx{bool}, belongs to class \cldx{term}; thus,
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   152
formulae are terms.  The built-in type~\tydx{fun}, which constructs
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   153
function types, is overloaded with arity {\tt(term,\thinspace
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   154
  term)\thinspace term}.  Thus, $\sigma\To\tau$ belongs to class~{\tt
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   155
  term} if $\sigma$ and~$\tau$ do, allowing quantification over
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   156
functions.
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   157
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   158
\HOL\ offers various methods for introducing new types.
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   159
See~\S\ref{sec:HOL:Types} and~\S\ref{sec:HOL:datatype}.
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   160
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   161
Theory \thydx{Ord} defines the syntactic class \cldx{ord} of order
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   162
signatures; the relations $<$ and $\leq$ are polymorphic over this
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   163
class, as are the functions \cdx{mono}, \cdx{min} and \cdx{max}, and
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   164
the \cdx{LEAST} operator. \thydx{Ord} also defines a subclass
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   165
\cldx{order} of \cldx{ord} which axiomatizes partially ordered types
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   166
(w.r.t.\ $\le$).
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   167
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   168
Three other syntactic type classes --- \cldx{plus}, \cldx{minus} and
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   169
\cldx{times} --- permit overloading of the operators {\tt+},\index{*"+
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   170
  symbol} {\tt-}\index{*"- symbol} and {\tt*}.\index{*"* symbol} In
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   171
particular, {\tt-} is instantiated for set difference and subtraction
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   172
on natural numbers.
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   173
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   174
If you state a goal containing overloaded functions, you may need to include
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   175
type constraints.  Type inference may otherwise make the goal more
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   176
polymorphic than you intended, with confusing results.  For example, the
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   177
variables $i$, $j$ and $k$ in the goal $i \le j \Imp i \le j+k$ have type
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   178
$\alpha::\{ord,plus\}$, although you may have expected them to have some
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   179
numeric type, e.g. $nat$.  Instead you should have stated the goal as
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   180
$(i::nat) \le j \Imp i \le j+k$, which causes all three variables to have
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   181
type $nat$.
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   182
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   183
\begin{warn}
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   184
  If resolution fails for no obvious reason, try setting
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   185
  \ttindex{show_types} to \texttt{true}, causing Isabelle to display
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   186
  types of terms.  Possibly set \ttindex{show_sorts} to \texttt{true} as
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   187
  well, causing Isabelle to display type classes and sorts.
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   188
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   189
  \index{unification!incompleteness of}
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   190
  Where function types are involved, Isabelle's unification code does not
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   191
  guarantee to find instantiations for type variables automatically.  Be
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   192
  prepared to use \ttindex{res_inst_tac} instead of \texttt{resolve_tac},
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   193
  possibly instantiating type variables.  Setting
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   194
  \ttindex{Unify.trace_types} to \texttt{true} causes Isabelle to report
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   195
  omitted search paths during unification.\index{tracing!of unification}
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   196
\end{warn}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   197
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   198
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   199
\subsection{Binders}
3160
08e364dfe518 minor tuning;
wenzelm
parents: 3152
diff changeset
   200
08e364dfe518 minor tuning;
wenzelm
parents: 3152
diff changeset
   201
Hilbert's {\bf description} operator~$\varepsilon x.P[x]$ stands for
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   202
some~$x$ satisfying~$P$, if such exists.  Since all terms in \HOL\ 
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   203
denote something, a description is always meaningful, but we do not
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   204
know its value unless $P$ defines it uniquely.  We may write
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   205
descriptions as \cdx{Eps}($\lambda x.P[x]$) or use the syntax
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   206
\hbox{\tt \at $x$.$P[x]$}.
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   207
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   208
Existential quantification is defined by
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   209
\[ \exists x.P~x \;\equiv\; P(\varepsilon x.P~x). \]
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   210
The unique existence quantifier, $\exists!x.P$, is defined in terms
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   211
of~$\exists$ and~$\forall$.  An Isabelle binder, it admits nested
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   212
quantifications.  For instance, $\exists!x\,y.P\,x\,y$ abbreviates
3160
08e364dfe518 minor tuning;
wenzelm
parents: 3152
diff changeset
   213
$\exists!x. \exists!y.P\,x\,y$; note that this does not mean that there
08e364dfe518 minor tuning;
wenzelm
parents: 3152
diff changeset
   214
exists a unique pair $(x,y)$ satisfying~$P\,x\,y$.
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   215
1162
7be0684950a3 changes made by Lawrence Paulson
clasohm
parents: 1113
diff changeset
   216
\index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system}
7be0684950a3 changes made by Lawrence Paulson
clasohm
parents: 1113
diff changeset
   217
Quantifiers have two notations.  As in Gordon's {\sc hol} system, \HOL\
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   218
uses~{\tt!}\ and~{\tt?}\ to stand for $\forall$ and $\exists$.  The
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   219
existential quantifier must be followed by a space; thus {\tt?x} is an
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   220
unknown, while \verb'? x.f x=y' is a quantification.  Isabelle's usual
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   221
notation for quantifiers, \sdx{ALL} and \sdx{EX}, is also
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   222
available.  Both notations are accepted for input.  The {\ML} reference
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   223
\ttindexbold{HOL_quantifiers} governs the output notation.  If set to {\tt
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   224
true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default.  If set
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   225
to \texttt{false}, then~{\tt ALL} and~{\tt EX} are displayed.
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   226
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   227
If $\tau$ is a type of class \cldx{ord}, $P$ a formula and $x$ a
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   228
variable of type $\tau$, then the term \cdx{LEAST}~$x.P[x]$ is defined
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   229
to be the least (w.r.t.\ $\le$) $x$ such that $P~x$ holds (see
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   230
Fig.~\ref{hol-defs}).  The definition uses Hilbert's $\varepsilon$
3160
08e364dfe518 minor tuning;
wenzelm
parents: 3152
diff changeset
   231
choice operator, so \texttt{Least} is always meaningful, but may yield
08e364dfe518 minor tuning;
wenzelm
parents: 3152
diff changeset
   232
nothing useful in case there is not a unique least element satisfying
08e364dfe518 minor tuning;
wenzelm
parents: 3152
diff changeset
   233
$P$.\footnote{Class $ord$ does not require much of its instances, so
08e364dfe518 minor tuning;
wenzelm
parents: 3152
diff changeset
   234
  $\le$ need not be a well-ordering, not even an order at all!}
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   235
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   236
\medskip All these binders have priority 10.
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   237
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   238
\begin{warn}
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   239
The low priority of binders means that they need to be enclosed in
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   240
parenthesis when they occur in the context of other operations.  For example,
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   241
instead of $P \land \forall x.Q$ you need to write $P \land (\forall x.Q)$.
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   242
\end{warn}
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   243
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   244
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   245
\subsection{The \sdx{let} and \sdx{case} constructions}
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   246
Local abbreviations can be introduced by a \texttt{let} construct whose
1163
c080ff36d24e changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents: 1162
diff changeset
   247
syntax appears in Fig.\ts\ref{hol-grammar}.  Internally it is translated into
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   248
the constant~\cdx{Let}.  It can be expanded by rewriting with its
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   249
definition, \tdx{Let_def}.
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   250
1162
7be0684950a3 changes made by Lawrence Paulson
clasohm
parents: 1113
diff changeset
   251
\HOL\ also defines the basic syntax
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   252
\[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n\] 
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   253
as a uniform means of expressing \texttt{case} constructs.  Therefore \texttt{case}
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   254
and \sdx{of} are reserved words.  Initially, this is mere syntax and has no
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   255
logical meaning.  By declaring translations, you can cause instances of the
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   256
{\tt case} construct to denote applications of particular case operators.
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   257
This is what happens automatically for each \texttt{datatype} definition
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   258
(see~\S\ref{sec:HOL:datatype}).
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   259
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   260
\begin{warn}
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   261
Both \texttt{if} and \texttt{case} constructs have as low a priority as
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   262
quantifiers, which requires additional enclosing parentheses in the context
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   263
of most other operations.  For example, instead of $f~x = if \dots then \dots
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   264
else \dots$ you need to write $f~x = (if \dots then \dots else
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   265
\dots)$.
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   266
\end{warn}
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   267
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   268
\section{Rules of inference}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   269
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   270
\begin{figure}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   271
\begin{ttbox}\makeatother
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   272
\tdx{refl}           t = (t::'a)
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   273
\tdx{subst}          [| s = t; P s |] ==> P (t::'a)
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   274
\tdx{ext}            (!!x::'a. (f x :: 'b) = g x) ==> (\%x.f x) = (\%x.g x)
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   275
\tdx{impI}           (P ==> Q) ==> P-->Q
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   276
\tdx{mp}             [| P-->Q;  P |] ==> Q
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   277
\tdx{iff}            (P-->Q) --> (Q-->P) --> (P=Q)
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   278
\tdx{selectI}        P(x::'a) ==> P(@x.P x)
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   279
\tdx{True_or_False}  (P=True) | (P=False)
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   280
\end{ttbox}
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   281
\caption{The \texttt{HOL} rules} \label{hol-rules}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   282
\end{figure}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   283
3160
08e364dfe518 minor tuning;
wenzelm
parents: 3152
diff changeset
   284
Figure~\ref{hol-rules} shows the primitive inference rules of~\HOL{},
08e364dfe518 minor tuning;
wenzelm
parents: 3152
diff changeset
   285
with their~{\ML} names.  Some of the rules deserve additional
08e364dfe518 minor tuning;
wenzelm
parents: 3152
diff changeset
   286
comments:
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   287
\begin{ttdescription}
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   288
\item[\tdx{ext}] expresses extensionality of functions.
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   289
\item[\tdx{iff}] asserts that logically equivalent formulae are
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   290
  equal.
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   291
\item[\tdx{selectI}] gives the defining property of the Hilbert
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   292
  $\varepsilon$-operator.  It is a form of the Axiom of Choice.  The derived rule
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   293
  \tdx{select_equality} (see below) is often easier to use.
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   294
\item[\tdx{True_or_False}] makes the logic classical.\footnote{In
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   295
    fact, the $\varepsilon$-operator already makes the logic classical, as
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   296
    shown by Diaconescu; see Paulson~\cite{paulson-COLOG} for details.}
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   297
\end{ttdescription}
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   298
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   299
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   300
\begin{figure}\hfuzz=4pt%suppress "Overfull \hbox" message
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   301
\begin{ttbox}\makeatother
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   302
\tdx{True_def}   True     == ((\%x::bool.x)=(\%x.x))
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   303
\tdx{All_def}    All      == (\%P. P = (\%x.True))
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   304
\tdx{Ex_def}     Ex       == (\%P. P(@x.P x))
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   305
\tdx{False_def}  False    == (!P.P)
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   306
\tdx{not_def}    not      == (\%P. P-->False)
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   307
\tdx{and_def}    op &     == (\%P Q. !R. (P-->Q-->R) --> R)
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   308
\tdx{or_def}     op |     == (\%P Q. !R. (P-->R) --> (Q-->R) --> R)
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   309
\tdx{Ex1_def}    Ex1      == (\%P. ? x. P x & (! y. P y --> y=x))
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   310
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   311
\tdx{o_def}      op o     == (\%(f::'b=>'c) g x::'a. f(g x))
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   312
\tdx{if_def}     If P x y ==
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   313
              (\%P x y. @z::'a.(P=True --> z=x) & (P=False --> z=y))
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   314
\tdx{Let_def}    Let s f  == f s
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   315
\tdx{Least_def}  Least P  == @x. P(x) & (ALL y. P(y) --> x <= y)"
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   316
\end{ttbox}
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   317
\caption{The \texttt{HOL} definitions} \label{hol-defs}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   318
\end{figure}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   319
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   320
1162
7be0684950a3 changes made by Lawrence Paulson
clasohm
parents: 1113
diff changeset
   321
\HOL{} follows standard practice in higher-order logic: only a few
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   322
connectives are taken as primitive, with the remainder defined obscurely
1163
c080ff36d24e changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents: 1162
diff changeset
   323
(Fig.\ts\ref{hol-defs}).  Gordon's {\sc hol} system expresses the
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   324
corresponding definitions \cite[page~270]{mgordon-hol} using
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   325
object-equality~({\tt=}), which is possible because equality in
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   326
higher-order logic may equate formulae and even functions over formulae.
1162
7be0684950a3 changes made by Lawrence Paulson
clasohm
parents: 1113
diff changeset
   327
But theory~\HOL{}, like all other Isabelle theories, uses
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   328
meta-equality~({\tt==}) for definitions.
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   329
\begin{warn}
3132
8e956415412f Documents directory Induct; stylistic improvements
paulson
parents: 3045
diff changeset
   330
The definitions above should never be expanded and are shown for completeness
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   331
only.  Instead users should reason in terms of the derived rules shown below
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   332
or, better still, using high-level tactics
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   333
(see~\S\ref{sec:HOL:generic-packages}).
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   334
\end{warn}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   335
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   336
Some of the rules mention type variables; for example, \texttt{refl}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   337
mentions the type variable~{\tt'a}.  This allows you to instantiate
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   338
type variables explicitly by calling \texttt{res_inst_tac}.
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   339
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   340
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   341
\begin{figure}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   342
\begin{ttbox}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   343
\tdx{sym}         s=t ==> t=s
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   344
\tdx{trans}       [| r=s; s=t |] ==> r=t
1489
78e1ce42a825 Small changes.
nipkow
parents: 1471
diff changeset
   345
\tdx{ssubst}      [| t=s; P s |] ==> P t
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   346
\tdx{box_equals}  [| a=b;  a=c;  b=d |] ==> c=d  
1489
78e1ce42a825 Small changes.
nipkow
parents: 1471
diff changeset
   347
\tdx{arg_cong}    x = y ==> f x = f y
78e1ce42a825 Small changes.
nipkow
parents: 1471
diff changeset
   348
\tdx{fun_cong}    f = g ==> f x = g x
78e1ce42a825 Small changes.
nipkow
parents: 1471
diff changeset
   349
\tdx{cong}        [| f = g; x = y |] ==> f x = g y
78e1ce42a825 Small changes.
nipkow
parents: 1471
diff changeset
   350
\tdx{not_sym}     t ~= s ==> s ~= t
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   351
\subcaption{Equality}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   352
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   353
\tdx{TrueI}       True 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   354
\tdx{FalseE}      False ==> P
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   355
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   356
\tdx{conjI}       [| P; Q |] ==> P&Q
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   357
\tdx{conjunct1}   [| P&Q |] ==> P
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   358
\tdx{conjunct2}   [| P&Q |] ==> Q 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   359
\tdx{conjE}       [| P&Q;  [| P; Q |] ==> R |] ==> R
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   360
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   361
\tdx{disjI1}      P ==> P|Q
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   362
\tdx{disjI2}      Q ==> P|Q
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   363
\tdx{disjE}       [| P | Q; P ==> R; Q ==> R |] ==> R
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   364
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   365
\tdx{notI}        (P ==> False) ==> ~ P
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   366
\tdx{notE}        [| ~ P;  P |] ==> R
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   367
\tdx{impE}        [| P-->Q;  P;  Q ==> R |] ==> R
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   368
\subcaption{Propositional logic}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   369
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   370
\tdx{iffI}        [| P ==> Q;  Q ==> P |] ==> P=Q
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   371
\tdx{iffD1}       [| P=Q; P |] ==> Q
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   372
\tdx{iffD2}       [| P=Q; Q |] ==> P
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   373
\tdx{iffE}        [| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R
1489
78e1ce42a825 Small changes.
nipkow
parents: 1471
diff changeset
   374
%
78e1ce42a825 Small changes.
nipkow
parents: 1471
diff changeset
   375
%\tdx{eqTrueI}     P ==> P=True 
78e1ce42a825 Small changes.
nipkow
parents: 1471
diff changeset
   376
%\tdx{eqTrueE}     P=True ==> P 
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   377
\subcaption{Logical equivalence}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   378
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   379
\end{ttbox}
1163
c080ff36d24e changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents: 1162
diff changeset
   380
\caption{Derived rules for \HOL} \label{hol-lemmas1}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   381
\end{figure}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   382
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   383
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   384
\begin{figure}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   385
\begin{ttbox}\makeatother
1489
78e1ce42a825 Small changes.
nipkow
parents: 1471
diff changeset
   386
\tdx{allI}      (!!x. P x) ==> !x. P x
78e1ce42a825 Small changes.
nipkow
parents: 1471
diff changeset
   387
\tdx{spec}      !x.P x ==> P x
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   388
\tdx{allE}      [| !x.P x;  P x ==> R |] ==> R
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   389
\tdx{all_dupE}  [| !x.P x;  [| P x; !x.P x |] ==> R |] ==> R
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   390
1489
78e1ce42a825 Small changes.
nipkow
parents: 1471
diff changeset
   391
\tdx{exI}       P x ==> ? x. P x
78e1ce42a825 Small changes.
nipkow
parents: 1471
diff changeset
   392
\tdx{exE}       [| ? x. P x; !!x. P x ==> Q |] ==> Q
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   393
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   394
\tdx{ex1I}      [| P a;  !!x. P x ==> x=a |] ==> ?! x. P x
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   395
\tdx{ex1E}      [| ?! x.P x;  !!x. [| P x;  ! y. P y --> y=x |] ==> R 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   396
          |] ==> R
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   397
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   398
\tdx{select_equality} [| P a;  !!x. P x ==> x=a |] ==> (@x.P x) = a
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   399
\subcaption{Quantifiers and descriptions}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   400
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   401
\tdx{ccontr}          (~P ==> False) ==> P
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   402
\tdx{classical}       (~P ==> P) ==> P
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   403
\tdx{excluded_middle} ~P | P
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   404
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   405
\tdx{disjCI}          (~Q ==> P) ==> P|Q
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   406
\tdx{exCI}            (! x. ~ P x ==> P a) ==> ? x.P x
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   407
\tdx{impCE}           [| P-->Q; ~ P ==> R; Q ==> R |] ==> R
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   408
\tdx{iffCE}           [| P=Q;  [| P;Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   409
\tdx{notnotD}         ~~P ==> P
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   410
\tdx{swap}            ~P ==> (~Q ==> P) ==> Q
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   411
\subcaption{Classical logic}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   412
1489
78e1ce42a825 Small changes.
nipkow
parents: 1471
diff changeset
   413
%\tdx{if_True}         (if True then x else y) = x
78e1ce42a825 Small changes.
nipkow
parents: 1471
diff changeset
   414
%\tdx{if_False}        (if False then x else y) = y
1163
c080ff36d24e changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents: 1162
diff changeset
   415
\tdx{if_P}            P ==> (if P then x else y) = x
c080ff36d24e changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents: 1162
diff changeset
   416
\tdx{if_not_P}        ~ P ==> (if P then x else y) = y
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   417
\tdx{expand_if}       P(if Q then x else y) = ((Q --> P x) & (~Q --> P y))
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   418
\subcaption{Conditionals}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   419
\end{ttbox}
1163
c080ff36d24e changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents: 1162
diff changeset
   420
\caption{More derived rules} \label{hol-lemmas2}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   421
\end{figure}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   422
1163
c080ff36d24e changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents: 1162
diff changeset
   423
Some derived rules are shown in Figures~\ref{hol-lemmas1}
c080ff36d24e changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents: 1162
diff changeset
   424
and~\ref{hol-lemmas2}, with their {\ML} names.  These include natural rules
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   425
for the logical connectives, as well as sequent-style elimination rules for
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   426
conjunctions, implications, and universal quantifiers.  
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   427
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   428
Note the equality rules: \tdx{ssubst} performs substitution in
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   429
backward proofs, while \tdx{box_equals} supports reasoning by
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   430
simplifying both sides of an equation.
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   431
1489
78e1ce42a825 Small changes.
nipkow
parents: 1471
diff changeset
   432
The following simple tactics are occasionally useful:
78e1ce42a825 Small changes.
nipkow
parents: 1471
diff changeset
   433
\begin{ttdescription}
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   434
\item[\ttindexbold{strip_tac} $i$] applies \texttt{allI} and \texttt{impI}
1489
78e1ce42a825 Small changes.
nipkow
parents: 1471
diff changeset
   435
  repeatedly to remove all outermost universal quantifiers and implications
78e1ce42a825 Small changes.
nipkow
parents: 1471
diff changeset
   436
  from subgoal $i$.
78e1ce42a825 Small changes.
nipkow
parents: 1471
diff changeset
   437
\item[\ttindexbold{case_tac} {\tt"}$P${\tt"} $i$] performs case distinction
78e1ce42a825 Small changes.
nipkow
parents: 1471
diff changeset
   438
  on $P$ for subgoal $i$: the latter is replaced by two identical subgoals
78e1ce42a825 Small changes.
nipkow
parents: 1471
diff changeset
   439
  with the added assumptions $P$ and $\neg P$, respectively.
78e1ce42a825 Small changes.
nipkow
parents: 1471
diff changeset
   440
\end{ttdescription}
78e1ce42a825 Small changes.
nipkow
parents: 1471
diff changeset
   441
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   442
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   443
\begin{figure} 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   444
\begin{center}
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   445
\begin{tabular}{rrr}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   446
  \it name      &\it meta-type  & \it description \\ 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   447
\index{{}@\verb'{}' symbol}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   448
  \verb|{}|     & $\alpha\,set$         & the empty set \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   449
  \cdx{insert}  & $[\alpha,\alpha\,set]\To \alpha\,set$
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   450
        & insertion of element \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   451
  \cdx{Collect} & $(\alpha\To bool)\To\alpha\,set$
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   452
        & comprehension \\
3160
08e364dfe518 minor tuning;
wenzelm
parents: 3152
diff changeset
   453
  \cdx{Compl}   & $\alpha\,set\To\alpha\,set$
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   454
        & complement \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   455
  \cdx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   456
        & intersection over a set\\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   457
  \cdx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   458
        & union over a set\\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   459
  \cdx{Inter} & $(\alpha\,set)set\To\alpha\,set$
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   460
        &set of sets intersection \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   461
  \cdx{Union} & $(\alpha\,set)set\To\alpha\,set$
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   462
        &set of sets union \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   463
  \cdx{Pow}   & $\alpha\,set \To (\alpha\,set)set$
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   464
        & powerset \\[1ex]
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   465
  \cdx{range}   & $(\alpha\To\beta )\To\beta\,set$
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   466
        & range of a function \\[1ex]
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   467
  \cdx{Ball}~~\cdx{Bex} & $[\alpha\,set,\alpha\To bool]\To bool$
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   468
        & bounded quantifiers
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   469
\end{tabular}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   470
\end{center}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   471
\subcaption{Constants}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   472
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   473
\begin{center}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   474
\begin{tabular}{llrrr} 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   475
  \it symbol &\it name     &\it meta-type & \it priority & \it description \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   476
  \sdx{INT}  & \cdx{INTER1}  & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 & 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   477
        intersection over a type\\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   478
  \sdx{UN}  & \cdx{UNION1}  & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 & 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   479
        union over a type
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   480
\end{tabular}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   481
\end{center}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   482
\subcaption{Binders} 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   483
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   484
\begin{center}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   485
\index{*"`"` symbol}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   486
\index{*": symbol}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   487
\index{*"<"= symbol}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   488
\begin{tabular}{rrrr} 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   489
  \it symbol    & \it meta-type & \it priority & \it description \\ 
3161
d2c6f15f38f4 minor tuning;
wenzelm
parents: 3160
diff changeset
   490
  \tt ``        & $[\alpha\To\beta ,\alpha\,set]\To  \beta\,set$
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   491
        & Left 90 & image \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   492
  \sdx{Int}     & $[\alpha\,set,\alpha\,set]\To\alpha\,set$
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   493
        & Left 70 & intersection ($\int$) \\
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   494
  \sdx{Un}      & $[\alpha\,set,\alpha\,set]\To\alpha\,set$
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   495
        & Left 65 & union ($\un$) \\
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   496
  \tt:          & $[\alpha ,\alpha\,set]\To bool$       
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   497
        & Left 50 & membership ($\in$) \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   498
  \tt <=        & $[\alpha\,set,\alpha\,set]\To bool$
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   499
        & Left 50 & subset ($\subseteq$) 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   500
\end{tabular}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   501
\end{center}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   502
\subcaption{Infixes}
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   503
\caption{Syntax of the theory \texttt{Set}} \label{hol-set-syntax}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   504
\end{figure} 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   505
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   506
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   507
\begin{figure} 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   508
\begin{center} \tt\frenchspacing
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   509
\index{*"! symbol}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   510
\begin{tabular}{rrr} 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   511
  \it external          & \it internal  & \it description \\ 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   512
  $a$ \ttilde: $b$      & \ttilde($a$ : $b$)    & \rm non-membership\\
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   513
  {\ttlbrace}$a@1$, $\ldots${\ttrbrace}  &  insert $a@1$ $\ldots$ {\ttlbrace}{\ttrbrace} & \rm finite set \\
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   514
  {\ttlbrace}$x$.$P[x]${\ttrbrace}        &  Collect($\lambda x.P[x]$) &
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   515
        \rm comprehension \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   516
  \sdx{INT} $x$:$A$.$B[x]$      & INTER $A$ $\lambda x.B[x]$ &
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   517
        \rm intersection \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   518
  \sdx{UN}{\tt\ }  $x$:$A$.$B[x]$      & UNION $A$ $\lambda x.B[x]$ &
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   519
        \rm union \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   520
  \tt ! $x$:$A$.$P[x]$ or \sdx{ALL} $x$:$A$.$P[x]$ & 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   521
        Ball $A$ $\lambda x.P[x]$ & 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   522
        \rm bounded $\forall$ \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   523
  \sdx{?} $x$:$A$.$P[x]$ or \sdx{EX}{\tt\ } $x$:$A$.$P[x]$ & 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   524
        Bex $A$ $\lambda x.P[x]$ & \rm bounded $\exists$
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   525
\end{tabular}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   526
\end{center}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   527
\subcaption{Translations}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   528
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   529
\dquotes
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   530
\[\begin{array}{rclcl}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   531
    term & = & \hbox{other terms\ldots} \\
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   532
         & | & "{\ttlbrace}{\ttrbrace}" \\
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   533
         & | & "{\ttlbrace} " term\; ("," term)^* " {\ttrbrace}" \\
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   534
         & | & "{\ttlbrace} " id " . " formula " {\ttrbrace}" \\
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   535
         & | & term " `` " term \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   536
         & | & term " Int " term \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   537
         & | & term " Un " term \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   538
         & | & "INT~~"  id ":" term " . " term \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   539
         & | & "UN~~~"  id ":" term " . " term \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   540
         & | & "INT~~"  id~id^* " . " term \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   541
         & | & "UN~~~"  id~id^* " . " term \\[2ex]
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   542
 formula & = & \hbox{other formulae\ldots} \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   543
         & | & term " : " term \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   544
         & | & term " \ttilde: " term \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   545
         & | & term " <= " term \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   546
         & | & "!~" id ":" term " . " formula 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   547
         & | & "ALL " id ":" term " . " formula \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   548
         & | & "?~" id ":" term " . " formula 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   549
         & | & "EX~~" id ":" term " . " formula
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   550
  \end{array}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   551
\]
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   552
\subcaption{Full Grammar}
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   553
\caption{Syntax of the theory \texttt{Set} (continued)} \label{hol-set-syntax2}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   554
\end{figure} 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   555
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   556
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   557
\section{A formulation of set theory}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   558
Historically, higher-order logic gives a foundation for Russell and
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   559
Whitehead's theory of classes.  Let us use modern terminology and call them
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   560
{\bf sets}, but note that these sets are distinct from those of {\ZF} set
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   561
theory, and behave more like {\ZF} classes.
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   562
\begin{itemize}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   563
\item
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   564
Sets are given by predicates over some type~$\sigma$.  Types serve to
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   565
define universes for sets, but type checking is still significant.
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   566
\item
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   567
There is a universal set (for each type).  Thus, sets have complements, and
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   568
may be defined by absolute comprehension.
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   569
\item
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   570
Although sets may contain other sets as elements, the containing set must
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   571
have a more complex type.
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   572
\end{itemize}
1162
7be0684950a3 changes made by Lawrence Paulson
clasohm
parents: 1113
diff changeset
   573
Finite unions and intersections have the same behaviour in \HOL\ as they
7be0684950a3 changes made by Lawrence Paulson
clasohm
parents: 1113
diff changeset
   574
do in~{\ZF}.  In \HOL\ the intersection of the empty set is well-defined,
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   575
denoting the universal set for the given type.
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   576
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   577
\subsection{Syntax of set theory}\index{*set type}
1162
7be0684950a3 changes made by Lawrence Paulson
clasohm
parents: 1113
diff changeset
   578
\HOL's set theory is called \thydx{Set}.  The type $\alpha\,set$ is
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   579
essentially the same as $\alpha\To bool$.  The new type is defined for
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   580
clarity and to avoid complications involving function types in unification.
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   581
The isomorphisms between the two types are declared explicitly.  They are
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   582
very natural: \texttt{Collect} maps $\alpha\To bool$ to $\alpha\,set$, while
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   583
\hbox{\tt op :} maps in the other direction (ignoring argument order).
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   584
1163
c080ff36d24e changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents: 1162
diff changeset
   585
Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax
c080ff36d24e changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents: 1162
diff changeset
   586
translations.  Figure~\ref{hol-set-syntax2} presents the grammar of the new
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   587
constructs.  Infix operators include union and intersection ($A\un B$
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   588
and $A\int B$), the subset and membership relations, and the image
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   589
operator~{\tt``}\@.  Note that $a$\verb|~:|$b$ is translated to
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   590
$\neg(a\in b)$.  
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   591
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   592
The $\{a@1,\ldots\}$ notation abbreviates finite sets constructed in
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   593
the obvious manner using~{\tt insert} and~$\{\}$:
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   594
\begin{eqnarray*}
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   595
  \{a, b, c\} & \equiv &
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   596
  \texttt{insert} \, a \, ({\tt insert} \, b \, ({\tt insert} \, c \, \{\}))
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   597
\end{eqnarray*}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   598
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   599
The set \hbox{\tt{\ttlbrace}$x$.$P[x]${\ttrbrace}} consists of all $x$ (of suitable type)
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   600
that satisfy~$P[x]$, where $P[x]$ is a formula that may contain free
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   601
occurrences of~$x$.  This syntax expands to \cdx{Collect}$(\lambda
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   602
x.P[x])$.  It defines sets by absolute comprehension, which is impossible
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   603
in~{\ZF}; the type of~$x$ implicitly restricts the comprehension.
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   604
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   605
The set theory defines two {\bf bounded quantifiers}:
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   606
\begin{eqnarray*}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   607
   \forall x\in A.P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   608
   \exists x\in A.P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x]
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   609
\end{eqnarray*}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   610
The constants~\cdx{Ball} and~\cdx{Bex} are defined
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   611
accordingly.  Instead of \texttt{Ball $A$ $P$} and \texttt{Bex $A$ $P$} we may
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   612
write\index{*"! symbol}\index{*"? symbol}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   613
\index{*ALL symbol}\index{*EX symbol} 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   614
%
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   615
\hbox{\tt !~$x$:$A$.$P[x]$} and \hbox{\tt ?~$x$:$A$.$P[x]$}.  Isabelle's
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   616
usual quantifier symbols, \sdx{ALL} and \sdx{EX}, are also accepted
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   617
for input.  As with the primitive quantifiers, the {\ML} reference
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   618
\ttindex{HOL_quantifiers} specifies which notation to use for output.
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   619
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   620
Unions and intersections over sets, namely $\bigcup@{x\in A}B[x]$ and
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   621
$\bigcap@{x\in A}B[x]$, are written 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   622
\sdx{UN}~\hbox{\tt$x$:$A$.$B[x]$} and
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   623
\sdx{INT}~\hbox{\tt$x$:$A$.$B[x]$}.  
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   624
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   625
Unions and intersections over types, namely $\bigcup@x B[x]$ and $\bigcap@x
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   626
B[x]$, are written \sdx{UN}~\hbox{\tt$x$.$B[x]$} and
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   627
\sdx{INT}~\hbox{\tt$x$.$B[x]$}.  They are equivalent to the previous
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   628
union and intersection operators when $A$ is the universal set.
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   629
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   630
The operators $\bigcup A$ and $\bigcap A$ act upon sets of sets.  They are
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   631
not binders, but are equal to $\bigcup@{x\in A}x$ and $\bigcap@{x\in A}x$,
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   632
respectively.
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   633
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   634
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   635
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   636
\begin{figure} \underscoreon
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   637
\begin{ttbox}
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   638
\tdx{mem_Collect_eq}    (a : {\ttlbrace}x.P x{\ttrbrace}) = P a
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   639
\tdx{Collect_mem_eq}    {\ttlbrace}x.x:A{\ttrbrace} = A
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   640
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   641
\tdx{empty_def}         {\ttlbrace}{\ttrbrace}          == {\ttlbrace}x.False{\ttrbrace}
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   642
\tdx{insert_def}        insert a B  == {\ttlbrace}x.x=a{\ttrbrace} Un B
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   643
\tdx{Ball_def}          Ball A P    == ! x. x:A --> P x
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   644
\tdx{Bex_def}           Bex A P     == ? x. x:A & P x
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   645
\tdx{subset_def}        A <= B      == ! x:A. x:B
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   646
\tdx{Un_def}            A Un B      == {\ttlbrace}x.x:A | x:B{\ttrbrace}
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   647
\tdx{Int_def}           A Int B     == {\ttlbrace}x.x:A & x:B{\ttrbrace}
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   648
\tdx{set_diff_def}      A - B       == {\ttlbrace}x.x:A & x~:B{\ttrbrace}
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   649
\tdx{Compl_def}         Compl A     == {\ttlbrace}x. ~ x:A{\ttrbrace}
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   650
\tdx{INTER_def}         INTER A B   == {\ttlbrace}y. ! x:A. y: B x{\ttrbrace}
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   651
\tdx{UNION_def}         UNION A B   == {\ttlbrace}y. ? x:A. y: B x{\ttrbrace}
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   652
\tdx{INTER1_def}        INTER1 B    == INTER {\ttlbrace}x.True{\ttrbrace} B 
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   653
\tdx{UNION1_def}        UNION1 B    == UNION {\ttlbrace}x.True{\ttrbrace} B 
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   654
\tdx{Inter_def}         Inter S     == (INT x:S. x)
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   655
\tdx{Union_def}         Union S     == (UN  x:S. x)
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   656
\tdx{Pow_def}           Pow A       == {\ttlbrace}B. B <= A{\ttrbrace}
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   657
\tdx{image_def}         f``A        == {\ttlbrace}y. ? x:A. y=f x{\ttrbrace}
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   658
\tdx{range_def}         range f     == {\ttlbrace}y. ? x. y=f x{\ttrbrace}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   659
\end{ttbox}
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   660
\caption{Rules of the theory \texttt{Set}} \label{hol-set-rules}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   661
\end{figure}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   662
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   663
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   664
\begin{figure} \underscoreon
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   665
\begin{ttbox}
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   666
\tdx{CollectI}        [| P a |] ==> a : {\ttlbrace}x.P x{\ttrbrace}
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   667
\tdx{CollectD}        [| a : {\ttlbrace}x.P x{\ttrbrace} |] ==> P a
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   668
\tdx{CollectE}        [| a : {\ttlbrace}x.P x{\ttrbrace};  P a ==> W |] ==> W
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   669
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   670
\tdx{ballI}           [| !!x. x:A ==> P x |] ==> ! x:A. P x
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   671
\tdx{bspec}           [| ! x:A. P x;  x:A |] ==> P x
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   672
\tdx{ballE}           [| ! x:A. P x;  P x ==> Q;  ~ x:A ==> Q |] ==> Q
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   673
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   674
\tdx{bexI}            [| P x;  x:A |] ==> ? x:A. P x
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   675
\tdx{bexCI}           [| ! x:A. ~ P x ==> P a;  a:A |] ==> ? x:A.P x
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   676
\tdx{bexE}            [| ? x:A. P x;  !!x. [| x:A; P x |] ==> Q  |] ==> Q
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   677
\subcaption{Comprehension and Bounded quantifiers}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   678
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   679
\tdx{subsetI}         (!!x.x:A ==> x:B) ==> A <= B
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   680
\tdx{subsetD}         [| A <= B;  c:A |] ==> c:B
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   681
\tdx{subsetCE}        [| A <= B;  ~ (c:A) ==> P;  c:B ==> P |] ==> P
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   682
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   683
\tdx{subset_refl}     A <= A
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   684
\tdx{subset_trans}    [| A<=B;  B<=C |] ==> A<=C
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   685
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   686
\tdx{equalityI}       [| A <= B;  B <= A |] ==> A = B
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   687
\tdx{equalityD1}      A = B ==> A<=B
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   688
\tdx{equalityD2}      A = B ==> B<=A
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   689
\tdx{equalityE}       [| A = B;  [| A<=B; B<=A |] ==> P |]  ==>  P
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   690
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   691
\tdx{equalityCE}      [| A = B;  [| c:A; c:B |] ==> P;  
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   692
                           [| ~ c:A; ~ c:B |] ==> P 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   693
                |]  ==>  P
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   694
\subcaption{The subset and equality relations}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   695
\end{ttbox}
1163
c080ff36d24e changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents: 1162
diff changeset
   696
\caption{Derived rules for set theory} \label{hol-set1}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   697
\end{figure}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   698
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   699
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   700
\begin{figure} \underscoreon
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   701
\begin{ttbox}
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   702
\tdx{emptyE}   a : {\ttlbrace}{\ttrbrace} ==> P
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   703
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   704
\tdx{insertI1} a : insert a B
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   705
\tdx{insertI2} a : B ==> a : insert b B
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   706
\tdx{insertE}  [| a : insert b A;  a=b ==> P;  a:A ==> P |] ==> P
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   707
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   708
\tdx{ComplI}   [| c:A ==> False |] ==> c : Compl A
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   709
\tdx{ComplD}   [| c : Compl A |] ==> ~ c:A
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   710
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   711
\tdx{UnI1}     c:A ==> c : A Un B
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   712
\tdx{UnI2}     c:B ==> c : A Un B
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   713
\tdx{UnCI}     (~c:B ==> c:A) ==> c : A Un B
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   714
\tdx{UnE}      [| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   715
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   716
\tdx{IntI}     [| c:A;  c:B |] ==> c : A Int B
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   717
\tdx{IntD1}    c : A Int B ==> c:A
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   718
\tdx{IntD2}    c : A Int B ==> c:B
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   719
\tdx{IntE}     [| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   720
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   721
\tdx{UN_I}     [| a:A;  b: B a |] ==> b: (UN x:A. B x)
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   722
\tdx{UN_E}     [| b: (UN x:A. B x);  !!x.[| x:A;  b:B x |] ==> R |] ==> R
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   723
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   724
\tdx{INT_I}    (!!x. x:A ==> b: B x) ==> b : (INT x:A. B x)
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   725
\tdx{INT_D}    [| b: (INT x:A. B x);  a:A |] ==> b: B a
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   726
\tdx{INT_E}    [| b: (INT x:A. B x);  b: B a ==> R;  ~ a:A ==> R |] ==> R
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   727
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   728
\tdx{UnionI}   [| X:C;  A:X |] ==> A : Union C
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   729
\tdx{UnionE}   [| A : Union C;  !!X.[| A:X;  X:C |] ==> R |] ==> R
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   730
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   731
\tdx{InterI}   [| !!X. X:C ==> A:X |] ==> A : Inter C
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   732
\tdx{InterD}   [| A : Inter C;  X:C |] ==> A:X
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   733
\tdx{InterE}   [| A : Inter C;  A:X ==> R;  ~ X:C ==> R |] ==> R
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   734
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   735
\tdx{PowI}     A<=B ==> A: Pow B
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   736
\tdx{PowD}     A: Pow B ==> A<=B
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   737
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   738
\tdx{imageI}   [| x:A |] ==> f x : f``A
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   739
\tdx{imageE}   [| b : f``A;  !!x.[| b=f x;  x:A |] ==> P |] ==> P
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   740
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   741
\tdx{rangeI}   f x : range f
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   742
\tdx{rangeE}   [| b : range f;  !!x.[| b=f x |] ==> P |] ==> P
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   743
\end{ttbox}
1163
c080ff36d24e changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents: 1162
diff changeset
   744
\caption{Further derived rules for set theory} \label{hol-set2}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   745
\end{figure}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   746
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   747
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   748
\subsection{Axioms and rules of set theory}
1163
c080ff36d24e changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents: 1162
diff changeset
   749
Figure~\ref{hol-set-rules} presents the rules of theory \thydx{Set}.  The
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   750
axioms \tdx{mem_Collect_eq} and \tdx{Collect_mem_eq} assert
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   751
that the functions \texttt{Collect} and \hbox{\tt op :} are isomorphisms.  Of
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   752
course, \hbox{\tt op :} also serves as the membership relation.
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   753
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   754
All the other axioms are definitions.  They include the empty set, bounded
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   755
quantifiers, unions, intersections, complements and the subset relation.
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   756
They also include straightforward constructions on functions: image~({\tt``})
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   757
and \texttt{range}.
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   758
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   759
%The predicate \cdx{inj_onto} is used for simulating type definitions.
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   760
%The statement ${\tt inj_onto}~f~A$ asserts that $f$ is injective on the
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   761
%set~$A$, which specifies a subset of its domain type.  In a type
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   762
%definition, $f$ is the abstraction function and $A$ is the set of valid
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   763
%representations; we should not expect $f$ to be injective outside of~$A$.
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   764
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   765
%\begin{figure} \underscoreon
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   766
%\begin{ttbox}
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   767
%\tdx{Inv_f_f}    inj f ==> Inv f (f x) = x
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   768
%\tdx{f_Inv_f}    y : range f ==> f(Inv f y) = y
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   769
%
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   770
%\tdx{Inv_injective}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   771
%    [| Inv f x=Inv f y; x: range f;  y: range f |] ==> x=y
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   772
%
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   773
%
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   774
%\tdx{monoI}      [| !!A B. A <= B ==> f A <= f B |] ==> mono f
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   775
%\tdx{monoD}      [| mono f;  A <= B |] ==> f A <= f B
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   776
%
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   777
%\tdx{injI}       [| !! x y. f x = f y ==> x=y |] ==> inj f
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   778
%\tdx{inj_inverseI}              (!!x. g(f x) = x) ==> inj f
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   779
%\tdx{injD}       [| inj f; f x = f y |] ==> x=y
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   780
%
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   781
%\tdx{inj_ontoI}  (!!x y. [| f x=f y; x:A; y:A |] ==> x=y) ==> inj_onto f A
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   782
%\tdx{inj_ontoD}  [| inj_onto f A;  f x=f y;  x:A;  y:A |] ==> x=y
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   783
%
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   784
%\tdx{inj_onto_inverseI}
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   785
%    (!!x. x:A ==> g(f x) = x) ==> inj_onto f A
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   786
%\tdx{inj_onto_contraD}
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   787
%    [| inj_onto f A;  x~=y;  x:A;  y:A |] ==> ~ f x=f y
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   788
%\end{ttbox}
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   789
%\caption{Derived rules involving functions} \label{hol-fun}
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   790
%\end{figure}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   791
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   792
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   793
\begin{figure} \underscoreon
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   794
\begin{ttbox}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   795
\tdx{Union_upper}     B:A ==> B <= Union A
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   796
\tdx{Union_least}     [| !!X. X:A ==> X<=C |] ==> Union A <= C
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   797
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   798
\tdx{Inter_lower}     B:A ==> Inter A <= B
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   799
\tdx{Inter_greatest}  [| !!X. X:A ==> C<=X |] ==> C <= Inter A
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   800
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   801
\tdx{Un_upper1}       A <= A Un B
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   802
\tdx{Un_upper2}       B <= A Un B
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   803
\tdx{Un_least}        [| A<=C;  B<=C |] ==> A Un B <= C
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   804
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   805
\tdx{Int_lower1}      A Int B <= A
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   806
\tdx{Int_lower2}      A Int B <= B
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   807
\tdx{Int_greatest}    [| C<=A;  C<=B |] ==> C <= A Int B
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   808
\end{ttbox}
1163
c080ff36d24e changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents: 1162
diff changeset
   809
\caption{Derived rules involving subsets} \label{hol-subset}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   810
\end{figure}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   811
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   812
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   813
\begin{figure} \underscoreon   \hfuzz=4pt%suppress "Overfull \hbox" message
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   814
\begin{ttbox}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   815
\tdx{Int_absorb}        A Int A = A
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   816
\tdx{Int_commute}       A Int B = B Int A
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   817
\tdx{Int_assoc}         (A Int B) Int C  =  A Int (B Int C)
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   818
\tdx{Int_Un_distrib}    (A Un B)  Int C  =  (A Int C) Un (B Int C)
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   819
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   820
\tdx{Un_absorb}         A Un A = A
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   821
\tdx{Un_commute}        A Un B = B Un A
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   822
\tdx{Un_assoc}          (A Un B)  Un C  =  A Un (B Un C)
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   823
\tdx{Un_Int_distrib}    (A Int B) Un C  =  (A Un C) Int (B Un C)
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   824
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   825
\tdx{Compl_disjoint}    A Int (Compl A) = {\ttlbrace}x.False{\ttrbrace}
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   826
\tdx{Compl_partition}   A Un  (Compl A) = {\ttlbrace}x.True{\ttrbrace}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   827
\tdx{double_complement} Compl(Compl A) = A
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   828
\tdx{Compl_Un}          Compl(A Un B)  = (Compl A) Int (Compl B)
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   829
\tdx{Compl_Int}         Compl(A Int B) = (Compl A) Un (Compl B)
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   830
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   831
\tdx{Union_Un_distrib}  Union(A Un B) = (Union A) Un (Union B)
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   832
\tdx{Int_Union}         A Int (Union B) = (UN C:B. A Int C)
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   833
\tdx{Un_Union_image}    (UN x:C.(A x) Un (B x)) = Union(A``C) Un Union(B``C)
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   834
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   835
\tdx{Inter_Un_distrib}  Inter(A Un B) = (Inter A) Int (Inter B)
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   836
\tdx{Un_Inter}          A Un (Inter B) = (INT C:B. A Un C)
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   837
\tdx{Int_Inter_image}   (INT x:C.(A x) Int (B x)) = Inter(A``C) Int Inter(B``C)
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   838
\end{ttbox}
1163
c080ff36d24e changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents: 1162
diff changeset
   839
\caption{Set equalities} \label{hol-equalities}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   840
\end{figure}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   841
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   842
1163
c080ff36d24e changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents: 1162
diff changeset
   843
Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules.  Most are
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   844
obvious and resemble rules of Isabelle's {\ZF} set theory.  Certain rules,
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   845
such as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI},
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   846
are designed for classical reasoning; the rules \tdx{subsetD},
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   847
\tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are not
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   848
strictly necessary but yield more natural proofs.  Similarly,
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   849
\tdx{equalityCE} supports classical reasoning about extensionality,
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   850
after the fashion of \tdx{iffCE}.  See the file \texttt{HOL/Set.ML} for
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   851
proofs pertaining to set theory.
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   852
1163
c080ff36d24e changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents: 1162
diff changeset
   853
Figure~\ref{hol-subset} presents lattice properties of the subset relation.
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   854
Unions form least upper bounds; non-empty intersections form greatest lower
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   855
bounds.  Reasoning directly about subsets often yields clearer proofs than
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   856
reasoning about the membership relation.  See the file \texttt{HOL/subset.ML}.
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   857
1163
c080ff36d24e changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents: 1162
diff changeset
   858
Figure~\ref{hol-equalities} presents many common set equalities.  They
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   859
include commutative, associative and distributive laws involving unions,
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   860
intersections and complements.  For a complete listing see the file {\tt
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   861
HOL/equalities.ML}.
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   862
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   863
\begin{warn}
3132
8e956415412f Documents directory Induct; stylistic improvements
paulson
parents: 3045
diff changeset
   864
\texttt{Blast_tac} proves many set-theoretic theorems automatically.
8e956415412f Documents directory Induct; stylistic improvements
paulson
parents: 3045
diff changeset
   865
Hence you seldom need to refer to the theorems above.
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   866
\end{warn}
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   867
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   868
\begin{figure}
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   869
\begin{center}
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   870
\begin{tabular}{rrr}
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   871
  \it name      &\it meta-type  & \it description \\ 
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   872
  \cdx{inj}~~\cdx{surj}& $(\alpha\To\beta )\To bool$
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   873
        & injective/surjective \\
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   874
  \cdx{inj_onto}        & $[\alpha\To\beta ,\alpha\,set]\To bool$
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   875
        & injective over subset\\
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   876
  \cdx{inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & inverse function
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   877
\end{tabular}
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   878
\end{center}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   879
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   880
\underscoreon
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   881
\begin{ttbox}
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   882
\tdx{inj_def}           inj f        == ! x y. f x=f y --> x=y
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   883
\tdx{surj_def}          surj f       == ! y. ? x. y=f x
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   884
\tdx{inj_onto_def}      inj_onto f A == !x:A. !y:A. f x=f y --> x=y
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   885
\tdx{inv_def}           inv f        == (\%y. @x. f(x)=y)
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   886
\end{ttbox}
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   887
\caption{Theory \thydx{Fun}} \label{fig:HOL:Fun}
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   888
\end{figure}
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   889
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   890
\subsection{Properties of functions}\nopagebreak
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   891
Figure~\ref{fig:HOL:Fun} presents a theory of simple properties of functions.
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   892
Note that ${\tt inv}~f$ uses Hilbert's $\varepsilon$ to yield an inverse
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   893
of~$f$.  See the file \texttt{HOL/Fun.ML} for a complete listing of the derived
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   894
rules.  Reasoning about function composition (the operator~\sdx{o}) and the
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   895
predicate~\cdx{surj} is done simply by expanding the definitions.
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   896
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   897
There is also a large collection of monotonicity theorems for constructions
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   898
on sets in the file \texttt{HOL/mono.ML}.
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   899
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   900
\section{Generic packages}
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   901
\label{sec:HOL:generic-packages}
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   902
3132
8e956415412f Documents directory Induct; stylistic improvements
paulson
parents: 3045
diff changeset
   903
\HOL\ instantiates most of Isabelle's generic packages, making available the
8e956415412f Documents directory Induct; stylistic improvements
paulson
parents: 3045
diff changeset
   904
simplifier and the classical reasoner.
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   905
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   906
\subsection{Simplification and substitution}
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   907
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   908
The simplifier is available in \HOL.  Tactics such as {\tt
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   909
  Asm_simp_tac} and \texttt{Full_simp_tac} use the default simpset
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   910
({\tt!simpset}), which works for most purposes.  A quite minimal
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   911
simplification set for higher-order logic is~\ttindexbold{HOL_ss},
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   912
even more frugal is \ttindexbold{HOL_basic_ss}.  Equality~($=$), which
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   913
also expresses logical equivalence, may be used for rewriting.  See
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   914
the file \texttt{HOL/simpdata.ML} for a complete listing of the basic
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   915
simplification rules.
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   916
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   917
See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   918
{Chaps.\ts\ref{substitution} and~\ref{simp-chap}} for details of substitution
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   919
and simplification.
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   920
3132
8e956415412f Documents directory Induct; stylistic improvements
paulson
parents: 3045
diff changeset
   921
\begin{warn}\index{simplification!of conjunctions}%
8e956415412f Documents directory Induct; stylistic improvements
paulson
parents: 3045
diff changeset
   922
  Reducing $a=b\conj P(a)$ to $a=b\conj P(b)$ is sometimes advantageous.  The
8e956415412f Documents directory Induct; stylistic improvements
paulson
parents: 3045
diff changeset
   923
  left part of a conjunction helps in simplifying the right part.  This effect
8e956415412f Documents directory Induct; stylistic improvements
paulson
parents: 3045
diff changeset
   924
  is not available by default: it can be slow.  It can be obtained by
8e956415412f Documents directory Induct; stylistic improvements
paulson
parents: 3045
diff changeset
   925
  including \ttindex{conj_cong} in a simpset, \verb$addcongs [conj_cong]$.
1234
56ee5cc35510 updated "o" in HOL: (infixl 55)
nipkow
parents: 1163
diff changeset
   926
\end{warn}
56ee5cc35510 updated "o" in HOL: (infixl 55)
nipkow
parents: 1163
diff changeset
   927
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   928
If the simplifier cannot use a certain rewrite rule --- either because
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   929
of nontermination or because its left-hand side is too flexible ---
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   930
then you might try \texttt{stac}:
1489
78e1ce42a825 Small changes.
nipkow
parents: 1471
diff changeset
   931
\begin{ttdescription}
78e1ce42a825 Small changes.
nipkow
parents: 1471
diff changeset
   932
\item[\ttindexbold{stac} $thm$ $i,$] where $thm$ is of the form $lhs = rhs$,
78e1ce42a825 Small changes.
nipkow
parents: 1471
diff changeset
   933
  replaces in subgoal $i$ instances of $lhs$ by corresponding instances of
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   934
  $rhs$.  In case of multiple instances of $lhs$ in subgoal $i$, backtracking
1489
78e1ce42a825 Small changes.
nipkow
parents: 1471
diff changeset
   935
  may be necessary to select the desired ones.
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   936
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   937
If $thm$ is a conditional equality, the instantiated condition becomes an
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   938
additional (first) subgoal.
1489
78e1ce42a825 Small changes.
nipkow
parents: 1471
diff changeset
   939
\end{ttdescription}
78e1ce42a825 Small changes.
nipkow
parents: 1471
diff changeset
   940
3132
8e956415412f Documents directory Induct; stylistic improvements
paulson
parents: 3045
diff changeset
   941
 \HOL{} provides the tactic \ttindex{hyp_subst_tac}, which substitutes
8e956415412f Documents directory Induct; stylistic improvements
paulson
parents: 3045
diff changeset
   942
  for an equality throughout a subgoal and its hypotheses.  This tactic uses
8e956415412f Documents directory Induct; stylistic improvements
paulson
parents: 3045
diff changeset
   943
  \HOL's general substitution rule.
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   944
1489
78e1ce42a825 Small changes.
nipkow
parents: 1471
diff changeset
   945
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   946
\subsection{Classical reasoning}
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   947
1162
7be0684950a3 changes made by Lawrence Paulson
clasohm
parents: 1113
diff changeset
   948
\HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   949
well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
1163
c080ff36d24e changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents: 1162
diff changeset
   950
rule; recall Fig.\ts\ref{hol-lemmas2} above.
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   951
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   952
The classical reasoner is installed.  Tactics such as \texttt{Blast_tac} and {\tt
2495
82ec47e0a8d3 New discussion of implicit simpsets & clasets
paulson
parents: 1859
diff changeset
   953
Best_tac} use the default claset ({\tt!claset}), which works for most
82ec47e0a8d3 New discussion of implicit simpsets & clasets
paulson
parents: 1859
diff changeset
   954
purposes.  Named clasets include \ttindexbold{prop_cs}, which includes the
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   955
propositional rules, and \ttindexbold{HOL_cs}, which also includes quantifier
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   956
rules.  See the file \texttt{HOL/cladata.ML} for lists of the classical rules,
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   957
and \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   958
{Chap.\ts\ref{chap:classical}} for more discussion of classical proof methods.
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   959
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   960
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   961
\section{Types}\label{sec:HOL:Types}
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   962
This section describes \HOL's basic predefined types ($\alpha \times
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   963
\beta$, $\alpha + \beta$, $nat$ and $\alpha \; list$) and ways for
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   964
introducing new types in general.  The most important type
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
   965
construction, the \texttt{datatype}, is treated separately in
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   966
\S\ref{sec:HOL:datatype}.
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   967
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   968
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
   969
\subsection{Product and sum types}\index{*"* type}\index{*"+ type}
2994
3bb5d1b9c3aa Tuple patterns are allowed now in `case'
nipkow
parents: 2975
diff changeset
   970
\label{subsec:prod-sum}
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   971
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   972
\begin{figure}[htbp]
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   973
\begin{constants}
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   974
  \it symbol    & \it meta-type &           & \it description \\ 
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   975
  \cdx{Pair}    & $[\alpha,\beta]\To \alpha\times\beta$
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   976
        & & ordered pairs $(a,b)$ \\
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   977
  \cdx{fst}     & $\alpha\times\beta \To \alpha$        & & first projection\\
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   978
  \cdx{snd}     & $\alpha\times\beta \To \beta$         & & second projection\\
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   979
  \cdx{split}   & $[[\alpha,\beta]\To\gamma, \alpha\times\beta] \To \gamma$ 
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   980
        & & generalized projection\\
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   981
  \cdx{Sigma}  & 
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   982
        $[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ &
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   983
        & general sum of sets
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   984
\end{constants}
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   985
\begin{ttbox}\makeatletter
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   986
%\tdx{fst_def}      fst p     == @a. ? b. p = (a,b)
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   987
%\tdx{snd_def}      snd p     == @b. ? a. p = (a,b)
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   988
%\tdx{split_def}    split c p == c (fst p) (snd p)
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
   989
\tdx{Sigma_def}    Sigma A B == UN x:A. UN y:B x. {\ttlbrace}(x,y){\ttrbrace}
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   990
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
   991
\tdx{Pair_eq}      ((a,b) = (a',b')) = (a=a' & b=b')
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   992
\tdx{Pair_inject}  [| (a, b) = (a',b');  [| a=a';  b=b' |] ==> R |] ==> R
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   993
\tdx{PairE}        [| !!x y. p = (x,y) ==> Q |] ==> Q
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   994
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   995
\tdx{fst_conv}     fst (a,b) = a
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   996
\tdx{snd_conv}     snd (a,b) = b
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   997
\tdx{surjective_pairing}  p = (fst p,snd p)
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   998
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
   999
\tdx{split}        split c (a,b) = c a b
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1000
\tdx{expand_split} R(split c p) = (! x y. p = (x,y) --> R(c x y))
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1001
3132
8e956415412f Documents directory Induct; stylistic improvements
paulson
parents: 3045
diff changeset
  1002
\tdx{SigmaI}    [| a:A;  b:B a |] ==> (a,b) : Sigma A B
8e956415412f Documents directory Induct; stylistic improvements
paulson
parents: 3045
diff changeset
  1003
\tdx{SigmaE}    [| c:Sigma A B; !!x y.[| x:A; y:B x; c=(x,y) |] ==> P |] ==> P
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1004
\end{ttbox}
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1005
\caption{Type $\alpha\times\beta$}\label{hol-prod}
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1006
\end{figure} 
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1007
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1008
Theory \thydx{Prod} (Fig.\ts\ref{hol-prod}) defines the product type
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1009
$\alpha\times\beta$, with the ordered pair syntax $(a, b)$.  General
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
  1010
tuples are simulated by pairs nested to the right:
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1011
\begin{center}
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1012
\begin{tabular}{|c|c|}
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1013
\hline
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1014
external & internal \\
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1015
\hline
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
  1016
$\tau@1 \times \dots \times \tau@n$ & $\tau@1 \times (\dots (\tau@{n-1} \times \tau@n)\dots)$ \\
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1017
\hline
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1018
$(t@1,\dots,t@n)$ & $(t@1,(\dots,(t@{n-1},t@n)\dots)$ \\
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1019
\hline
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1020
\end{tabular}
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1021
\end{center}
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1022
In addition, it is possible to use tuples
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1023
as patterns in abstractions:
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1024
\begin{center}
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1025
{\tt\%($x$,$y$).$t$} \quad stands for\quad \texttt{split(\%$x$\thinspace$y$.$t$)} 
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1026
\end{center}
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1027
Nested patterns are also supported.  They are translated stepwise:
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1028
{\tt\%($x$,$y$,$z$).$t$} $\leadsto$ {\tt\%($x$,($y$,$z$)).$t$} $\leadsto$
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1029
{\tt split(\%$x$.\%($y$,$z$).$t$)} $\leadsto$ \texttt{split(\%$x$.split(\%$y$
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1030
  $z$.$t$))}.  The reverse translation is performed upon printing.
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1031
\begin{warn}
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1032
  The translation between patterns and \texttt{split} is performed automatically
1448
77379ae9ff0d Stylistic changes to discussion of pattern-matching
paulson
parents: 1429
diff changeset
  1033
  by the parser and printer.  Thus the internal and external form of a term
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1034
  may differ, which can affects proofs.  For example the term {\tt
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1035
  (\%(x,y).(y,x))(a,b)} requires the theorem \texttt{split} (which is in the
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1036
  default simpset) to rewrite to {\tt(b,a)}.
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1037
\end{warn}
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1038
In addition to explicit $\lambda$-abstractions, patterns can be used in any
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1039
variable binding construct which is internally described by a
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1040
$\lambda$-abstraction.  Some important examples are
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1041
\begin{description}
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1042
\item[Let:] \texttt{let {\it pattern} = $t$ in $u$}
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1043
\item[Quantifiers:] \texttt{!~{\it pattern}:$A$.~$P$}
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1044
\item[Choice:] {\underscoreon \tt @~{\it pattern}~.~$P$}
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1045
\item[Set operations:] \texttt{UN~{\it pattern}:$A$.~$B$}
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1046
\item[Sets:] \texttt{{\ttlbrace}~{\it pattern}~.~$P$~{\ttrbrace}}
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1047
\end{description}
1471
b088c0a1f2bd documented split_all_tac in HOL.
nipkow
parents: 1448
diff changeset
  1048
b088c0a1f2bd documented split_all_tac in HOL.
nipkow
parents: 1448
diff changeset
  1049
There is a simple tactic which supports reasoning about patterns:
b088c0a1f2bd documented split_all_tac in HOL.
nipkow
parents: 1448
diff changeset
  1050
\begin{ttdescription}
b088c0a1f2bd documented split_all_tac in HOL.
nipkow
parents: 1448
diff changeset
  1051
\item[\ttindexbold{split_all_tac} $i$] replaces in subgoal $i$ all
b088c0a1f2bd documented split_all_tac in HOL.
nipkow
parents: 1448
diff changeset
  1052
  {\tt!!}-quantified variables of product type by individual variables for
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1053
  each component.  A simple example:
1471
b088c0a1f2bd documented split_all_tac in HOL.
nipkow
parents: 1448
diff changeset
  1054
\begin{ttbox}
b088c0a1f2bd documented split_all_tac in HOL.
nipkow
parents: 1448
diff changeset
  1055
{\out 1. !!p. (\%(x,y,z). (x, y, z)) p = p}
b088c0a1f2bd documented split_all_tac in HOL.
nipkow
parents: 1448
diff changeset
  1056
by(split_all_tac 1);
b088c0a1f2bd documented split_all_tac in HOL.
nipkow
parents: 1448
diff changeset
  1057
{\out 1. !!x xa ya. (\%(x,y,z). (x, y, z)) (x, xa, ya) = (x, xa, ya)}
b088c0a1f2bd documented split_all_tac in HOL.
nipkow
parents: 1448
diff changeset
  1058
\end{ttbox}
b088c0a1f2bd documented split_all_tac in HOL.
nipkow
parents: 1448
diff changeset
  1059
\end{ttdescription}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1060
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1061
Theory \texttt{Prod} also introduces the degenerate product type \texttt{unit}
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1062
which contains only a single element named {\tt()} with the property
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1063
\begin{ttbox}
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1064
\tdx{unit_eq}       u = ()
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1065
\end{ttbox}
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1066
\bigskip
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1067
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1068
Theory \thydx{Sum} (Fig.~\ref{hol-sum}) defines the sum type $\alpha+\beta$
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1069
which associates to the right and has a lower priority than $*$: $\tau@1 +
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1070
\tau@2 + \tau@3*\tau@4$ means $\tau@1 + (\tau@2 + (\tau@3*\tau@4))$.
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1071
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
  1072
The definition of products and sums in terms of existing types is not
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
  1073
shown.  The constructions are fairly standard and can be found in the
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
  1074
respective theory files.
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1075
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1076
\begin{figure}
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1077
\begin{constants}
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1078
  \it symbol    & \it meta-type &           & \it description \\ 
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1079
  \cdx{Inl}     & $\alpha \To \alpha+\beta$    & & first injection\\
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1080
  \cdx{Inr}     & $\beta \To \alpha+\beta$     & & second injection\\
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1081
  \cdx{sum_case} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1082
        & & conditional
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1083
\end{constants}
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1084
\begin{ttbox}\makeatletter
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1085
%\tdx{sum_case_def}   sum_case == (\%f g p. @z. (!x. p=Inl x --> z=f x) &
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1086
%                                        (!y. p=Inr y --> z=g y))
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1087
%
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
  1088
\tdx{Inl_not_Inr}    Inl a ~= Inr b
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1089
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1090
\tdx{inj_Inl}        inj Inl
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1091
\tdx{inj_Inr}        inj Inr
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1092
1489
78e1ce42a825 Small changes.
nipkow
parents: 1471
diff changeset
  1093
\tdx{sumE}           [| !!x. P(Inl x);  !!y. P(Inr y) |] ==> P s
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1094
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1095
\tdx{sum_case_Inl}   sum_case f g (Inl x) = f x
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1096
\tdx{sum_case_Inr}   sum_case f g (Inr x) = g x
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1097
1489
78e1ce42a825 Small changes.
nipkow
parents: 1471
diff changeset
  1098
\tdx{surjective_sum} sum_case (\%x. f(Inl x)) (\%y. f(Inr y)) s = f s
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1099
\tdx{expand_sum_case} R(sum_case f g s) = ((! x. s = Inl(x) --> R(f(x))) &
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1100
                                     (! y. s = Inr(y) --> R(g(y))))
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1101
\end{ttbox}
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1102
\caption{Type $\alpha+\beta$}\label{hol-sum}
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1103
\end{figure}
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1104
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1105
\begin{figure}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1106
\index{*"< symbol}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1107
\index{*"* symbol}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1108
\index{*div symbol}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1109
\index{*mod symbol}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1110
\index{*"+ symbol}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1111
\index{*"- symbol}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1112
\begin{constants}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1113
  \it symbol    & \it meta-type & \it priority & \it description \\ 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1114
  \cdx{0}       & $nat$         & & zero \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1115
  \cdx{Suc}     & $nat \To nat$ & & successor function\\
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1116
% \cdx{nat_case} & $[\alpha, nat\To\alpha, nat] \To\alpha$ & & conditional\\
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1117
% \cdx{nat_rec} & $[nat, \alpha, [nat, \alpha]\To\alpha] \To \alpha$
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1118
%        & & primitive recursor\\
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1119
  \tt *         & $[nat,nat]\To nat$    &  Left 70      & multiplication \\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1120
  \tt div       & $[nat,nat]\To nat$    &  Left 70      & division\\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1121
  \tt mod       & $[nat,nat]\To nat$    &  Left 70      & modulus\\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1122
  \tt +         & $[nat,nat]\To nat$    &  Left 65      & addition\\
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1123
  \tt -         & $[nat,nat]\To nat$    &  Left 65      & subtraction
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1124
\end{constants}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1125
\subcaption{Constants and infixes}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1126
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1127
\begin{ttbox}\makeatother
3045
4ef28e05781b Added 'induct_tac'
nipkow
parents: 2994
diff changeset
  1128
\tdx{nat_induct}     [| P 0; !!n. P n ==> P(Suc n) |]  ==> P n
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1129
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1130
\tdx{Suc_not_Zero}   Suc m ~= 0
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1131
\tdx{inj_Suc}        inj Suc
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1132
\tdx{n_not_Suc_n}    n~=Suc n
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1133
\subcaption{Basic properties}
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1134
\end{ttbox}
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1135
\caption{The type of natural numbers, \tydx{nat}} \label{hol-nat1}
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1136
\end{figure}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1137
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1138
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1139
\begin{figure}
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1140
\begin{ttbox}\makeatother
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1141
              0+n           = n
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1142
              (Suc m)+n     = Suc(m+n)
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1143
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1144
              m-0           = m
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1145
              0-n           = n
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1146
              Suc(m)-Suc(n) = m-n
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1147
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1148
              0*n           = 0
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1149
              Suc(m)*n      = n + m*n
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1150
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1151
\tdx{mod_less}      m<n ==> m mod n = m
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1152
\tdx{mod_geq}       [| 0<n;  ~m<n |] ==> m mod n = (m-n) mod n
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1153
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1154
\tdx{div_less}      m<n ==> m div n = 0
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1155
\tdx{div_geq}       [| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1156
\end{ttbox}
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1157
\caption{Recursion equations for the arithmetic operators} \label{hol-nat2}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1158
\end{figure}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1159
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1160
\subsection{The type of natural numbers, \textit{nat}}
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1161
\index{nat@{\textit{nat}} type|(}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1162
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1163
The theory \thydx{NatDef} defines the natural numbers in a roundabout but
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1164
traditional way.  The axiom of infinity postulates a type~\tydx{ind} of
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1165
individuals, which is non-empty and closed under an injective operation.  The
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1166
natural numbers are inductively generated by choosing an arbitrary individual
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1167
for~0 and using the injective operation to take successors.  This is a least
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1168
fixedpoint construction.  For details see the file \texttt{NatDef.thy}.
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1169
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1170
Type~\tydx{nat} is an instance of class~\cldx{ord}, which makes the
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1171
overloaded functions of this class (esp.\ \cdx{<} and \cdx{<=}, but also
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1172
\cdx{min}, \cdx{max} and \cdx{LEAST}) available on \tydx{nat}.  Theory
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1173
\thydx{Nat} builds on \texttt{NatDef} and shows that {\tt<=} is a partial order,
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1174
so \tydx{nat} is also an instance of class \cldx{order}.
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1175
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1176
Theory \thydx{Arith} develops arithmetic on the natural numbers.  It defines
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1177
addition, multiplication and subtraction.  Theory \thydx{Divides} defines
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1178
division, remainder and the ``divides'' relation.  The numerous theorems
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1179
proved include commutative, associative, distributive, identity and
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1180
cancellation laws.  See Figs.\ts\ref{hol-nat1} and~\ref{hol-nat2}.  The
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1181
recursion equations for the operators \texttt{+}, \texttt{-} and \texttt{*} on
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1182
\texttt{nat} are part of the default simpset.
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1183
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1184
Functions on \tydx{nat} can be defined by primitive or well-founded recursion;
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1185
see \S\ref{sec:HOL:recursive}.  A simple example is addition.
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1186
Here, \texttt{op +} is the name of the infix operator~\texttt{+}, following
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1187
the standard convention.
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1188
\begin{ttbox}
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1189
\sdx{primrec} "op +" nat 
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1190
  "    0 + n = n"
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1191
  "Suc m + n = Suc(m + n)"
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1192
\end{ttbox}
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1193
There is also a \sdx{case}-construct
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1194
of the form
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1195
\begin{ttbox}
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1196
case \(e\) of 0 => \(a\) | Suc \(m\) => \(b\)
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1197
\end{ttbox}
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1198
Note that Isabelle insists on precisely this format; you may not even change
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1199
the order of the two cases.
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1200
Both \texttt{primrec} and \texttt{case} are realized by a recursion operator
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1201
\cdx{nat_rec}, the details of which can be found in theory \texttt{NatDef}.
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1202
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1203
%The predecessor relation, \cdx{pred_nat}, is shown to be well-founded.
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1204
%Recursion along this relation resembles primitive recursion, but is
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1205
%stronger because we are in higher-order logic; using primitive recursion to
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1206
%define a higher-order function, we can easily Ackermann's function, which
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1207
%is not primitive recursive \cite[page~104]{thompson91}.
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1208
%The transitive closure of \cdx{pred_nat} is~$<$.  Many functions on the
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1209
%natural numbers are most easily expressed using recursion along~$<$.
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1210
3045
4ef28e05781b Added 'induct_tac'
nipkow
parents: 2994
diff changeset
  1211
Tactic {\tt\ttindex{induct_tac} "$n$" $i$} performs induction on variable~$n$
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1212
in subgoal~$i$ using theorem \texttt{nat_induct}.  There is also the derived
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
  1213
theorem \tdx{less_induct}:
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1214
\begin{ttbox}
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1215
[| !!n. [| ! m. m<n --> P m |] ==> P n |]  ==>  P n
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1216
\end{ttbox}
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1217
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1218
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1219
Reasoning about arithmetic inequalities can be tedious.  A minimal amount of
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1220
automation is provided by the tactic \ttindex{trans_tac} of type \texttt{int ->
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1221
tactic} that deals with simple inequalities.  Note that it only knows about
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1222
{\tt 0}, \texttt{Suc}, {\tt<} and {\tt<=}.  The following goals are all solved by
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1223
{\tt trans_tac 1}:
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1224
\begin{ttbox}
3152
065c701c7827 misc tuning, cleanup, improvements;
wenzelm
parents: 3132
diff changeset
  1225
{\out  1. \dots ==> m <= Suc(Suc m)}
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1226
{\out  1. [| \dots i <= j \dots Suc j <= k \dots |] ==> i < k}
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1227
{\out  1. [| \dots Suc m <= n \dots ~ m < n \dots |] ==> \dots}
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1228
\end{ttbox}
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1229
For a complete description of the limitations of the tactic and how to avoid
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1230
some of them, see the comments at the start of the file {\tt
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1231
Provers/nat_transitive.ML}.
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1232
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1233
If \texttt{trans_tac} fails you, try to find relevant arithmetic results in
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1234
the library.  The theory \texttt{NatDef} contains theorems about {\tt<} and
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1235
{\tt<=}, the theory \texttt{Arith} contains theorems about \texttt{+},
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1236
\texttt{-} and \texttt{*}, and theory \texttt{Divides} contains theorems about
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1237
\texttt{div} and \texttt{mod}.  Use the \texttt{find}-functions to locate them
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1238
(see the {\em Reference Manual\/}).
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1239
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1240
\begin{figure}
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1241
\index{#@{\tt[]} symbol}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1242
\index{#@{\tt\#} symbol}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1243
\index{"@@{\tt\at} symbol}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1244
\begin{constants}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1245
  \it symbol & \it meta-type & \it priority & \it description \\
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1246
  \tt[]    & $\alpha\,list$ & & empty list\\
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1247
  \tt \#   & $[\alpha,\alpha\,list]\To \alpha\,list$ & Right 65 & 
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1248
        list constructor \\
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1249
  \cdx{null}    & $\alpha\,list \To bool$ & & emptiness test\\
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1250
  \cdx{hd}      & $\alpha\,list \To \alpha$ & & head \\
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1251
  \cdx{tl}      & $\alpha\,list \To \alpha\,list$ & & tail \\
3881
73be08b4da3f Added last, butlast, dropped ttl.
nipkow
parents: 3489
diff changeset
  1252
  \cdx{last}    & $\alpha\,list \To \alpha$ & & last element \\
73be08b4da3f Added last, butlast, dropped ttl.
nipkow
parents: 3489
diff changeset
  1253
  \cdx{butlast} & $\alpha\,list \To \alpha\,list$ & & drop last element \\
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1254
  \tt\at  & $[\alpha\,list,\alpha\,list]\To \alpha\,list$ & Left 65 & append \\
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1255
  \cdx{map}     & $(\alpha\To\beta) \To (\alpha\,list \To \beta\,list)$
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1256
        & & apply to all\\
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1257
  \cdx{filter}  & $(\alpha \To bool) \To (\alpha\,list \To \alpha\,list)$
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1258
        & & filter functional\\
3487
62a6a08471e4 set_of_list -> set
nipkow
parents: 3315
diff changeset
  1259
  \cdx{set}& $\alpha\,list \To \alpha\,set$ & & elements\\
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1260
  \sdx{mem}  & $[\alpha,\alpha\,list]\To bool$    &  Left 55   & membership\\
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1261
  \cdx{foldl}   & $(\beta\To\alpha\To\beta) \To \beta \To \alpha\,list \To \beta$ &
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1262
  & iteration \\
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1263
  \cdx{concat}   & $(\alpha\,list)list\To \alpha\,list$ & & concatenation \\
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1264
  \cdx{rev}     & $\alpha\,list \To \alpha\,list$ & & reverse \\
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1265
  \cdx{length}  & $\alpha\,list \To nat$ & & length \\
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1266
  \cdx{nth}  & $nat \To \alpha\,list \To \alpha$ & & indexing \\
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1267
  \cdx{take}, \cdx{drop} & $nat \To \alpha\,list \To \alpha\,list$ &&
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1268
    take or drop a prefix \\
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1269
  \cdx{takeWhile},\\
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1270
  \cdx{dropWhile} &
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1271
    $(\alpha \To bool) \To \alpha\,list \To \alpha\,list$ &&
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1272
    take or drop a prefix
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1273
\end{constants}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1274
\subcaption{Constants and infixes}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1275
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1276
\begin{center} \tt\frenchspacing
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1277
\begin{tabular}{rrr} 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1278
  \it external        & \it internal  & \it description \\{}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1279
  [$x@1$, $\dots$, $x@n$]  &  $x@1$ \# $\cdots$ \# $x@n$ \# [] &
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1280
        \rm finite list \\{}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1281
  [$x$:$l$. $P$]  & filter ($\lambda x{.}P$) $l$ & 
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1282
        \rm list comprehension
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1283
\end{tabular}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1284
\end{center}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1285
\subcaption{Translations}
1163
c080ff36d24e changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents: 1162
diff changeset
  1286
\caption{The theory \thydx{List}} \label{hol-list}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1287
\end{figure}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1288
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1289
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1290
\begin{figure}
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1291
\begin{ttbox}\makeatother
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1292
null [] = True
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1293
null (x#xs) = False
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1294
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1295
hd (x#xs) = x
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1296
tl (x#xs) = xs
3881
73be08b4da3f Added last, butlast, dropped ttl.
nipkow
parents: 3489
diff changeset
  1297
tl [] = []
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1298
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1299
[] @ ys = ys
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1300
(x#xs) @ ys = x # xs @ ys
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1301
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1302
map f [] = []
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1303
map f (x#xs) = f x # map f xs
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1304
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1305
filter P [] = []
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1306
filter P (x#xs) = (if P x then x#filter P xs else filter P xs)
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1307
3487
62a6a08471e4 set_of_list -> set
nipkow
parents: 3315
diff changeset
  1308
set [] = \ttlbrace\ttrbrace
62a6a08471e4 set_of_list -> set
nipkow
parents: 3315
diff changeset
  1309
set (x#xs) = insert x (set xs)
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1310
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1311
x mem [] = False
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1312
x mem (y#ys) = (if y=x then True else x mem ys)
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1313
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1314
foldl f a [] = a
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1315
foldl f a (x#xs) = foldl f (f a x) xs
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1316
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1317
concat([]) = []
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1318
concat(x#xs) = x @ concat(xs)
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1319
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1320
rev([]) = []
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1321
rev(x#xs) = rev(xs) @ [x]
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1322
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1323
length([]) = 0
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1324
length(x#xs) = Suc(length(xs))
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1325
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1326
nth 0 xs = hd xs
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1327
nth (Suc n) xs = nth n (tl xs)
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1328
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1329
take n [] = []
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1330
take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1331
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1332
drop n [] = []
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1333
drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1334
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1335
takeWhile P [] = []
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1336
takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1337
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1338
dropWhile P [] = []
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1339
dropWhile P (x#xs) = (if P x then dropWhile P xs else xs)
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1340
\end{ttbox}
2926
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1341
\caption{Recursions equations for list processing functions}
15c21c1ad71d Thorough update.
nipkow
parents: 2495
diff changeset
  1342
\label{fig:HOL:list-simps}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1343
\end{figure}
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1344
\index{nat@{\textit{nat}} type|)}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1345
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1346
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1347
\subsection{The type constructor for lists, \textit{list}}
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1348
\index{list@{\textit{list}} type|(}
1113
dd7284573601 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff changeset
  1349
1422
bc628f4ef0cb New version of type sections and many small changes.
nipkow
parents: 1389
diff changeset
  1350
Figure~\ref{hol-list} presents the theory \thydx{List}: the basic list
3489
afa802078173 Added documentation for recdef, and tidied some other material
paulson
parents: 3487
diff changeset
  1351
operations with their types and syntax.  Type $\alpha \; list$ is