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