author lcp Fri, 15 Apr 1994 13:02:22 +0200 changeset 315 ebf62069d889 parent 314 d1ef723e943d child 316 813ee27cd4d5
penultimate Springer draft
--- a/doc-src/Logics/Old_HOL.tex	Fri Apr 15 12:54:22 1994 +0200
+++ b/doc-src/Logics/Old_HOL.tex	Fri Apr 15 13:02:22 1994 +0200
@@ -1,96 +1,86 @@
%% $Id$
-\chapter{Higher-Order logic}
-The directory~\ttindexbold{HOL} contains a theory for higher-order logic.
+\chapter{Higher-Order Logic}
+\index{higher-order logic|(}
+\index{HOL system@{\sc hol} system}
+
+The theory~\thydx{HOL} implements higher-order logic.
It is based on Gordon's~{\sc hol} system~\cite{mgordon88a}, which itself is
-based on Church~\cite{church40}.  Andrews~\cite{andrews86} is a full
-description of higher-order logic.  Gordon's work has demonstrated that
-higher-order logic is useful for hardware verification; beyond this, it is
-widely applicable in many areas of mathematics.  It is weaker than {\ZF}
-set theory but for most applications this does not matter.  If you prefer
-{\ML} to Lisp, you will probably prefer \HOL\ to~{\ZF}.
+based on Church's original paper~\cite{church40}.  Andrews's
+book~\cite{andrews86} is a full description of higher-order logic.
+Experience with the {\sc hol} system has demonstrated that higher-order
+logic is useful for hardware verification; beyond this, it is widely
+applicable in many areas of mathematics.  It is weaker than {\ZF} set
+theory but for most applications this does not matter.  If you prefer {\ML}
+to Lisp, you will probably prefer \HOL\ to~{\ZF}.

-Previous releases of Isabelle included a completely different version
-of~\HOL, with explicit type inference rules~\cite{paulson-COLOG}.  This
-version no longer exists, but \ttindex{ZF} supports a similar style of
-reasoning.
+Previous releases of Isabelle included a different version of~\HOL, with
+explicit type inference rules~\cite{paulson-COLOG}.  This version no longer
+exists, but \thydx{ZF} supports a similar style of reasoning.

\HOL\ has a distinct feel, compared with {\ZF} and {\CTT}.  It
identifies object-level types with meta-level types, taking advantage of
Isabelle's built-in type checker.  It identifies object-level functions
with meta-level functions, so it uses Isabelle's operations for abstraction
-and application.  There is no apply'' operator: function applications are
+and application.  There is no apply' operator: function applications are
written as simply~$f(a)$ rather than $f{\tt}a$.

These identifications allow Isabelle to support \HOL\ particularly nicely,
but they also mean that \HOL\ requires more sophistication from the user
--- in particular, an understanding of Isabelle's type system.  Beginners
-should gain experience by working in first-order logic, before attempting
-to use higher-order logic.  This chapter assumes familiarity with~{\FOL{}}.
+should work with {\tt show_types} set to {\tt true}.  Gain experience by
+working in first-order logic before attempting to use higher-order logic.
+This chapter assumes familiarity with~{\FOL{}}.

\begin{figure}
\begin{center}
\begin{tabular}{rrr}
\it name      &\it meta-type  & \it description \\
-  \idx{Trueprop}& $bool\To prop$                & coercion to $prop$\\
-  \idx{not}     & $bool\To bool$                & negation ($\neg$) \\
-  \idx{True}    & $bool$                        & tautology ($\top$) \\
-  \idx{False}   & $bool$                        & absurdity ($\bot$) \\
-  \idx{if}      & $[bool,\alpha,\alpha]\To\alpha::term$ & conditional \\
-  \idx{Inv}     & $(\alpha\To\beta)\To(\beta\To\alpha)$ & function inversion\\
-  \idx{Let}     & $[\alpha,\alpha\To\beta]\To\beta$ & let binder
+  \cdx{Trueprop}& $bool\To prop$                & coercion to $prop$\\
+  \cdx{not}     & $bool\To bool$                & negation ($\neg$) \\
+  \cdx{True}    & $bool$                        & tautology ($\top$) \\
+  \cdx{False}   & $bool$                        & absurdity ($\bot$) \\
+  \cdx{if}      & $[bool,\alpha,\alpha]\To\alpha::term$ & conditional \\
+  \cdx{Inv}     & $(\alpha\To\beta)\To(\beta\To\alpha)$ & function inversion\\
+  \cdx{Let}     & $[\alpha,\alpha\To\beta]\To\beta$ & let binder
\end{tabular}
\end{center}
\subcaption{Constants}

\begin{center}
-\index{"@@{\tt\at}|bold}
-\index{*"!|bold}
-\index{*"?"!|bold}
+\index{"@@{\tt\at} symbol}
+\index{*"! symbol}\index{*"? symbol}
+\index{*"?"! symbol}\index{*"E"X"! symbol}
\begin{tabular}{llrrr}
-  \it symbol &\it name     &\it meta-type & \it prec & \it description \\
-  \tt\at & \idx{Eps}  & $(\alpha\To bool)\To\alpha::term$ & 10 &
+  \it symbol &\it name     &\it meta-type & \it description \\
+  \tt\at & \cdx{Eps}  & $(\alpha\To bool)\To\alpha::term$ &
Hilbert description ($\epsilon$) \\
-  \tt!  & \idx{All}  & $(\alpha::term\To bool)\To bool$ & 10 &
+  {\tt!~} or \sdx{ALL}  & \cdx{All}  & $(\alpha::term\To bool)\To bool$ &
universal quantifier ($\forall$) \\
-  \idx{?}  & \idx{Ex}   & $(\alpha::term\To bool)\To bool$ & 10 &
+  {\tt?~} or \sdx{EX}   & \cdx{Ex}   & $(\alpha::term\To bool)\To bool$ &
existential quantifier ($\exists$) \\
-  \tt?! & \idx{Ex1}  & $(\alpha::term\To bool)\To bool$ & 10 &
+  {\tt?!} or {\tt EX!}  & \cdx{Ex1}  & $(\alpha::term\To bool)\To bool$ &
unique existence ($\exists!$)
\end{tabular}
\end{center}
\subcaption{Binders}

\begin{center}
-\index{*"E"X"!|bold}
-\begin{tabular}{llrrr}
-  \it symbol &\it name     &\it meta-type & \it prec & \it description \\
-  \idx{ALL}  & \idx{All}  & $(\alpha::term\To bool)\To bool$ & 10 &
-        universal quantifier ($\forall$) \\
-  \idx{EX}   & \idx{Ex}   & $(\alpha::term\To bool)\To bool$ & 10 &
-        existential quantifier ($\exists$) \\
-  \tt EX!   & \idx{Ex1}  & $(\alpha::term\To bool)\To bool$ & 10 &
-        unique existence ($\exists!$)
-\end{tabular}
-\end{center}
-\subcaption{Alternative quantifiers}
-
-\begin{center}
-\indexbold{*"=}
-\indexbold{&@{\tt\&}}
-\indexbold{*"|}
-\indexbold{*"-"-">}
+\index{*"= symbol}
+\index{&@{\tt\&} symbol}
+\index{*"| symbol}
+\index{*"-"-"> symbol}
\begin{tabular}{rrrr}
-  \it symbol    & \it meta-type & \it precedence & \it description \\
-  \idx{o}       & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ &
+  \it symbol    & \it meta-type & \it priority & \it description \\
+  \sdx{o}       & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ &
Right 50 & composition ($\circ$) \\
\tt =         & $[\alpha::term,\alpha]\To bool$ & Left 50 & equality ($=$) \\
+  \tt <         & $[\alpha::ord,\alpha]\To bool$ & Left 50 & less than ($<$) \\
+  \tt <=        & $[\alpha::ord,\alpha]\To bool$ & Left 50 &
+                less than or equals ($\leq$)\\
\tt \&        & $[bool,bool]\To bool$ & Right 35 & conjunction ($\conj$) \\
\tt |         & $[bool,bool]\To bool$ & Right 30 & disjunction ($\disj$) \\
-  \tt -->       & $[bool,bool]\To bool$ & Right 25 & implication ($\imp$) \\
-  \tt <         & $[\alpha::ord,\alpha]\To bool$ & Left 50 & less than ($<$) \\
-  \tt <=        & $[\alpha::ord,\alpha]\To bool$ & Left 50 &
-                less than or equals ($\leq$)
+  \tt -->       & $[bool,bool]\To bool$ & Right 25 & implication ($\imp$)
\end{tabular}
\end{center}
\subcaption{Infixes}
@@ -99,13 +89,15 @@

\begin{figure}
-\indexbold{*let}
-\indexbold{*in}
+\index{*let symbol}
+\index{*in symbol}
\dquotes
-$\begin{array}{rcl} +\[\begin{array}{rclcl} term & = & \hbox{expression of class~term} \\ - & | & "\at~~" id~id^* " . " formula \\ - & | & "let"~id~"="~term";"\dots";"~id~"="~term~"in"~term \\[2ex] + & | & "\at~" id~id^* " . " formula \\ + & | & + \multicolumn{3}{l}{"let"~id~"="~term";"\dots";"~id~"="~term~"in"~term} + \\[2ex] formula & = & \hbox{expression of type~bool} \\ & | & term " = " term \\ & | & term " \ttilde= " term \\ @@ -115,46 +107,58 @@ & | & formula " \& " formula \\ & | & formula " | " formula \\ & | & formula " --> " formula \\ - & | & "!~~~" id~id^* " . " formula \\ - & | & "?~~~" id~id^* " . " formula \\ - & | & "?!~~" id~id^* " . " formula \\ + & | & "!~~~" id~id^* " . " formula & | & "ALL~" id~id^* " . " formula \\ + & | & "?~~~" id~id^* " . " formula & | & "EX~~" id~id^* " . " formula \\ + & | & "?!~~" id~id^* " . " formula & | & "EX!~" id~id^* " . " formula \end{array}$
-\subcaption{Grammar}
\caption{Full grammar for \HOL} \label{hol-grammar}
\end{figure}

\section{Syntax}
-Type inference is automatic, exploiting Isabelle's type classes.  The class
-of higher-order terms is called {\it term\/}; type variables range over
-this class by default.  The equality symbol and quantifiers are polymorphic
-over class {\it term}.
+The type class of higher-order terms is called~\cldx{term}.  Type variables
+range over this class by default.  The equality symbol and quantifiers are
+polymorphic over class {\tt term}.

-Class {\it ord\/} consists of all ordered types; the relations $<$ and
+Class \cldx{ord} consists of all ordered types; the relations $<$ and
$\leq$ are polymorphic over this class, as are the functions
-\ttindex{mono}, \ttindex{min} and \ttindex{max}.  Three other
-type classes --- {\it plus}, {\it minus\/} and {\it times} --- permit
+\cdx{mono}, \cdx{min} and \cdx{max}.  Three other
+type classes --- \cldx{plus}, \cldx{minus} and \cldx{times} --- permit
{\tt-} is overloaded for set difference and subtraction.
-\index{*"+}\index{-@{\tt-}}\index{*@{\tt*}}
+\index{*"+ symbol}
+\index{*"- symbol}
+\index{*"* symbol}

Figure~\ref{hol-constants} lists the constants (including infixes and
-binders), while Fig.\ts \ref{hol-grammar} presents the grammar of
+binders), while Fig.\ts\ref{hol-grammar} presents the grammar of
higher-order logic.  Note that $a$\verb|~=|$b$ is translated to
-\verb|~(|$a$=$b$\verb|)|.
+$\neg(a=b)$.
+
+\begin{warn}
+  \HOL\ has no if-and-only-if connective; logical equivalence is expressed
+  using equality.  But equality has a high priority, as befitting a
+  relation, while if-and-only-if typically has the lowest priority.  Thus,
+  $\neg\neg P=P$ abbreviates $\neg\neg (P=P)$ and not $(\neg\neg P)=P$.
+  When using $=$ to mean logical equivalence, enclose both operands in
+  parentheses.
+\end{warn}

\subsection{Types}\label{HOL-types}
-The type of formulae, {\it bool} belongs to class {\it term}; thus,
-formulae are terms.  The built-in type~$fun$, which constructs function
-types, is overloaded such that $\sigma\To\tau$ belongs to class~$term$ if
-$\sigma$ and~$\tau$ do; this allows quantification over functions.  Types
-in \HOL\ must be non-empty; otherwise the quantifier rules would be
-unsound~\cite[\S7]{paulson-COLOG}.
+The type of formulae, \tydx{bool}, belongs to class \cldx{term}; thus,
+formulae are terms.  The built-in type~\tydx{fun}, which constructs function
+types, is overloaded with arity {\tt(term,term)term}.  Thus, $\sigma\To\tau$
+belongs to class~{\tt term} if $\sigma$ and~$\tau$ do, allowing quantification
+over functions.

+Types in \HOL\ must be non-empty; otherwise the quantifier rules would be
+unsound.  I have commented on this elsewhere~\cite[\S7]{paulson-COLOG}.
+
+\index{type definitions}
Gordon's {\sc hol} system supports {\bf type definitions}.  A type is
defined by exhibiting an existing type~$\sigma$, a predicate~$P::\sigma\To bool$, and a theorem of the form $\exists x::\sigma.P(x)$.  Thus~$P$
@@ -166,9 +170,9 @@
type.

Isabelle does not support type definitions at present.  Instead, they are
-mimicked by explicit definitions of isomorphism functions.  These should be
-accompanied by theorems of the form $\exists x::\sigma.P(x)$, but this is
-not checked.
+mimicked by explicit definitions of isomorphism functions.  The definitions
+should be supported by theorems of the form $\exists x::\sigma.P(x)$, but
+Isabelle cannot enforce this.

\subsection{Binders}
@@ -176,116 +180,166 @@
satisfying~$P[a]$, if such exists.  Since all terms in \HOL\ denote
something, a description is always meaningful, but we do not know its value
unless $P[x]$ defines it uniquely.  We may write descriptions as
-\ttindexbold{Eps}($P$) or use the syntax
-\hbox{\tt \at $x$.$P[x]$}.  Existential quantification is defined
-by
-$\exists x.P(x) \equiv P(\epsilon x.P(x))$
+\cdx{Eps}($P$) or use the syntax
+\hbox{\tt \at $x$.$P[x]$}.
+
+Existential quantification is defined by
+$\exists x.P(x) \;\equiv\; P(\epsilon x.P(x)).$
The unique existence quantifier, $\exists!x.P[x]$, is defined in terms
of~$\exists$ and~$\forall$.  An Isabelle binder, it admits nested
quantifications.  For instance, $\exists!x y.P(x,y)$ abbreviates
$\exists!x. \exists!y.P(x,y)$; note that this does not mean that there
exists a unique pair $(x,y)$ satisfying~$P(x,y)$.

-\index{*"!}\index{*"?}
+\index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system}
Quantifiers have two notations.  As in Gordon's {\sc hol} system, \HOL\
uses~{\tt!}\ and~{\tt?}\ to stand for $\forall$ and $\exists$.  The
existential quantifier must be followed by a space; thus {\tt?x} is an
unknown, while \verb'? x.f(x)=y' is a quantification.  Isabelle's usual
-notation for quantifiers, \ttindex{ALL} and \ttindex{EX}, is also
+notation for quantifiers, \sdx{ALL} and \sdx{EX}, is also
available.  Both notations are accepted for input.  The {\ML} reference
\ttindexbold{HOL_quantifiers} governs the output notation.  If set to {\tt
true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default.  If set
to {\tt false}, then~{\tt ALL} and~{\tt EX} are displayed.

-\begin{warn}
-Although the description operator does not usually allow iteration of the
-form \hbox{\tt \at $x@1 \dots x@n$.$P[x@1,\dots,x@n]$}, there are cases where
-this is legal.  If \hbox{\tt \at $y$.$P[x,y]$} is of type~{\it bool},
-then \hbox{\tt \at $x\,y$.$P[x,y]$} is legal.  The pretty printer will
-display \hbox{\tt \at $x$.\at $y$.$P[x,y]$} as
-\hbox{\tt \at $x\,y$.$P[x,y]$}.
-\end{warn}
+All these binders have priority 10.
+
+
+\subsection{The \sdx{let} and \sdx{case} constructions}
+Local abbreviations can be introduced by a {\tt let} construct whose
+syntax appears in Fig.\ts\ref{hol-grammar}.  Internally it is translated into
+the constant~\cdx{Let}.  It can be expanded by rewriting with its
+definition, \tdx{Let_def}.

-\subsection{\idx{let} and \idx{case}}
-Local abbreviations can be introduced via a \ttindex{let}-construct whose
-syntax is shown in Fig.~\ref{hol-grammar}. Internally it is translated into
-the constant \ttindex{Let} and can be expanded by rewriting with its
-definition \ttindex{Let_def}.
+\HOL\ also defines the basic syntax
+$\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n$
+as a uniform means of expressing {\tt case} constructs.  Therefore {\tt
+  case} and \sdx{of} are reserved words.  However, so far this is mere
+syntax and has no logical meaning.  By declaring translations, you can
+cause instances of the {\tt case} construct to denote applications of
+particular case operators.  The patterns supplied for $c@1$,~\ldots,~$c@n$
+distinguish among the different case operators.  For an example, see the
+case construct for lists on page~\pageref{hol-list} below.
+

-\HOL\ also defines the basic syntax {\dquotes$"case"~e~"of"~c@1~"=>"~e@1~"|" - \dots "|"~c@n~"=>"~e@n$} for {\tt case}-constructs, which means that {\tt
-  case} and \ttindex{of} are reserved words. However, so far this is mere
-syntax and has no logical meaning. In order to be useful it needs to be
-filled with life by translating certain case constructs into meaningful
-terms. For an example see the case construct for the type of lists below.
+\begin{figure}
+\begin{ttbox}\makeatother
+\tdx{refl}           t = t::'a
+\tdx{subst}          [| s=t; P(s) |] ==> P(t::'a)
+\tdx{ext}            (!!x::'a. f(x)::'b = g(x)) ==> (\%x.f(x)) = (\%x.g(x))
+\tdx{impI}           (P ==> Q) ==> P-->Q
+\tdx{mp}             [| P-->Q;  P |] ==> Q
+\tdx{iff}            (P-->Q) --> (Q-->P) --> (P=Q)
+\tdx{selectI}        P(x::'a) ==> P(@x.P(x))
+\tdx{True_or_False}  (P=True) | (P=False)
+\end{ttbox}
+\caption{The {\tt HOL} rules} \label{hol-rules}
+\end{figure}

\begin{figure}
\begin{ttbox}\makeatother
-\idx{refl}           t = t::'a
-\idx{subst}          [| s=t; P(s) |] ==> P(t::'a)
-\idx{ext}            (!!x::'a. f(x)::'b = g(x)) ==> (\%x.f(x)) = (\%x.g(x))
-\idx{impI}           (P ==> Q) ==> P-->Q
-\idx{mp}             [| P-->Q;  P |] ==> Q
-\idx{iff}            (P-->Q) --> (Q-->P) --> (P=Q)
-\idx{selectI}        P(x::'a) ==> P(@x.P(x))
-\idx{True_or_False}  (P=True) | (P=False)
-\subcaption{basic rules}
+\tdx{True_def}   True  = ((\%x.x)=(\%x.x))
+\tdx{All_def}    All   = (\%P. P = (\%x.True))
+\tdx{Ex_def}     Ex    = (\%P. P(@x.P(x)))
+\tdx{False_def}  False = (!P.P)
+\tdx{not_def}    not   = (\%P. P-->False)
+\tdx{and_def}    op &  = (\%P Q. !R. (P-->Q-->R) --> R)
+\tdx{or_def}     op |  = (\%P Q. !R. (P-->R) --> (Q-->R) --> R)
+\tdx{Ex1_def}    Ex1   = (\%P. ? x. P(x) & (! y. P(y) --> y=x))
+
+\tdx{Inv_def}    Inv   = (\%(f::'a=>'b) y. @x. f(x)=y)
+\tdx{o_def}      op o  = (\%(f::'b=>'c) g (x::'a). f(g(x)))
+\tdx{if_def}     if    = (\%P x y.@z::'a.(P=True --> z=x) & (P=False --> z=y))
+\tdx{Let_def}    Let(s,f) = f(s)
+\end{ttbox}
+\caption{The {\tt HOL} definitions} \label{hol-defs}
+\end{figure}
+
+
+\section{Rules of inference}
+Figure~\ref{hol-rules} shows the inference rules of~\HOL{}, with
+\begin{ttdescription}
+\item[\tdx{ext}] expresses extensionality of functions.
+\item[\tdx{iff}] asserts that logically equivalent formulae are
+  equal.
+\item[\tdx{selectI}] gives the defining property of the Hilbert
+  $\epsilon$-operator.  It is a form of the Axiom of Choice.  The derived rule
+  \tdx{select_equality} (see below) is often easier to use.
+\item[\tdx{True_or_False}] makes the logic classical.\footnote{In
+    fact, the $\epsilon$-operator already makes the logic classical, as
+    shown by Diaconescu; see Paulson~\cite{paulson-COLOG} for details.}
+\end{ttdescription}

-\idx{True_def}       True  = ((\%x.x)=(\%x.x))
-\idx{All_def}        All   = (\%P. P = (\%x.True))
-\idx{Ex_def}         Ex    = (\%P. P(@x.P(x)))
-\idx{False_def}      False = (!P.P)
-\idx{not_def}        not   = (\%P. P-->False)
-\idx{and_def}        op &  = (\%P Q. !R. (P-->Q-->R) --> R)
-\idx{or_def}         op |  = (\%P Q. !R. (P-->R) --> (Q-->R) --> R)
-\idx{Ex1_def}        Ex1   = (\%P. ? x. P(x) & (! y. P(y) --> y=x))
-\subcaption{Definitions of the logical constants}
+\HOL{} follows standard practice in higher-order logic: only a few
+connectives are taken as primitive, with the remainder defined obscurely
+(Fig.\ts\ref{hol-defs}).  Unusually, the definitions are expressed using
+object-equality~({\tt=}) rather than meta-equality~({\tt==}).  This is
+possible because equality in higher-order logic may equate formulae and
+even functions over formulae.  On the other hand, meta-equality is
+Isabelle's usual symbol for making definitions.  Take care to note which
+form of equality is used before attempting a proof.
+
+Some of the rules mention type variables; for example, {\tt refl} mentions
+the type variable~{\tt'a}.  This allows you to instantiate type variables
+explicitly by calling {\tt res_inst_tac}.  By default, explicit type
+variables have class \cldx{term}.

-\idx{Inv_def}   Inv  = (\%(f::'a=>'b) y. @x. f(x)=y)
-\idx{o_def}     op o = (\%(f::'b=>'c) g (x::'a). f(g(x)))
-\idx{if_def}    if   = (\%P x y.@z::'a.(P=True --> z=x) & (P=False --> z=y))
-\idx{Let_def}   Let(s,f) = f(s)
-\subcaption{Further definitions}
-\end{ttbox}
-\caption{Rules of {\tt HOL}} \label{hol-rules}
-\end{figure}
+Include type constraints whenever you state a polymorphic goal.  Type
+inference may otherwise make the goal more polymorphic than you intended,
+with confusing results.
+
+\begin{warn}
+  If resolution fails for no obvious reason, try setting
+  \ttindex{show_types} to {\tt true}, causing Isabelle to display types of
+  terms.  Possibly set \ttindex{show_sorts} to {\tt true} as well, causing
+  Isabelle to display sorts.
+
+  \index{unification!incompleteness of}
+  Where function types are involved, Isabelle's unification code does not
+  guarantee to find instantiations for type variables automatically.  Be
+  prepared to use \ttindex{res_inst_tac} instead of {\tt resolve_tac},
+  possibly instantiating type variables.  Setting
+  \ttindex{Unify.trace_types} to {\tt true} causes Isabelle to report
+  omitted search paths during unification.\index{tracing!of unification}
+\end{warn}

\begin{figure}
\begin{ttbox}
-\idx{sym}         s=t ==> t=s
-\idx{trans}       [| r=s; s=t |] ==> r=t
-\idx{ssubst}      [| t=s; P(s) |] ==> P(t::'a)
-\idx{box_equals}  [| a=b;  a=c;  b=d |] ==> c=d
-\idx{arg_cong}    s=t ==> f(s)=f(t)
-\idx{fun_cong}    s::'a=>'b = t ==> s(x)=t(x)
+\tdx{sym}         s=t ==> t=s
+\tdx{trans}       [| r=s; s=t |] ==> r=t
+\tdx{ssubst}      [| t=s; P(s) |] ==> P(t::'a)
+\tdx{box_equals}  [| a=b;  a=c;  b=d |] ==> c=d
+\tdx{arg_cong}    s=t ==> f(s)=f(t)
+\tdx{fun_cong}    s::'a=>'b = t ==> s(x)=t(x)
\subcaption{Equality}

-\idx{TrueI}       True
-\idx{FalseE}      False ==> P
+\tdx{TrueI}       True
+\tdx{FalseE}      False ==> P

-\idx{conjI}       [| P; Q |] ==> P&Q
-\idx{conjunct1}   [| P&Q |] ==> P
-\idx{conjunct2}   [| P&Q |] ==> Q
-\idx{conjE}       [| P&Q;  [| P; Q |] ==> R |] ==> R
+\tdx{conjI}       [| P; Q |] ==> P&Q
+\tdx{conjunct1}   [| P&Q |] ==> P
+\tdx{conjunct2}   [| P&Q |] ==> Q
+\tdx{conjE}       [| P&Q;  [| P; Q |] ==> R |] ==> R

-\idx{disjI1}      P ==> P|Q
-\idx{disjI2}      Q ==> P|Q
-\idx{disjE}       [| P | Q; P ==> R; Q ==> R |] ==> R
+\tdx{disjI1}      P ==> P|Q
+\tdx{disjI2}      Q ==> P|Q
+\tdx{disjE}       [| P | Q; P ==> R; Q ==> R |] ==> R

-\idx{notI}        (P ==> False) ==> ~ P
-\idx{notE}        [| ~ P;  P |] ==> R
-\idx{impE}        [| P-->Q;  P;  Q ==> R |] ==> R
+\tdx{notI}        (P ==> False) ==> ~ P
+\tdx{notE}        [| ~ P;  P |] ==> R
+\tdx{impE}        [| P-->Q;  P;  Q ==> R |] ==> R
\subcaption{Propositional logic}

-\idx{iffI}        [| P ==> Q;  Q ==> P |] ==> P=Q
-\idx{iffD1}       [| P=Q; P |] ==> Q
-\idx{iffD2}       [| P=Q; Q |] ==> P
-\idx{iffE}        [| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R
+\tdx{iffI}        [| P ==> Q;  Q ==> P |] ==> P=Q
+\tdx{iffD1}       [| P=Q; P |] ==> Q
+\tdx{iffD2}       [| P=Q; Q |] ==> P
+\tdx{iffE}        [| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R

-\idx{eqTrueI}     P ==> P=True
-\idx{eqTrueE}     P=True ==> P
+\tdx{eqTrueI}     P ==> P=True
+\tdx{eqTrueE}     P=True ==> P
\subcaption{Logical equivalence}

\end{ttbox}
@@ -295,106 +349,51 @@

\begin{figure}
\begin{ttbox}\makeatother
-\idx{allI}      (!!x::'a. P(x)) ==> !x. P(x)
-\idx{spec}      !x::'a.P(x) ==> P(x)
-\idx{allE}      [| !x.P(x);  P(x) ==> R |] ==> R
-\idx{all_dupE}  [| !x.P(x);  [| P(x); !x.P(x) |] ==> R |] ==> R
+\tdx{allI}      (!!x::'a. P(x)) ==> !x. P(x)
+\tdx{spec}      !x::'a.P(x) ==> P(x)
+\tdx{allE}      [| !x.P(x);  P(x) ==> R |] ==> R
+\tdx{all_dupE}  [| !x.P(x);  [| P(x); !x.P(x) |] ==> R |] ==> R

-\idx{exI}       P(x) ==> ? x::'a.P(x)
-\idx{exE}       [| ? x::'a.P(x); !!x. P(x) ==> Q |] ==> Q
+\tdx{exI}       P(x) ==> ? x::'a.P(x)
+\tdx{exE}       [| ? x::'a.P(x); !!x. P(x) ==> Q |] ==> Q

-\idx{ex1I}      [| P(a);  !!x. P(x) ==> x=a |] ==> ?! x. P(x)
-\idx{ex1E}      [| ?! x.P(x);  !!x. [| P(x);  ! y. P(y) --> y=x |] ==> R
+\tdx{ex1I}      [| P(a);  !!x. P(x) ==> x=a |] ==> ?! x. P(x)
+\tdx{ex1E}      [| ?! x.P(x);  !!x. [| P(x);  ! y. P(y) --> y=x |] ==> R
|] ==> R

-\idx{select_equality}  [| P(a);  !!x. P(x) ==> x=a |] ==> (@x.P(x)) = a
+\tdx{select_equality} [| P(a);  !!x. P(x) ==> x=a |] ==> (@x.P(x)) = a
\subcaption{Quantifiers and descriptions}

-\idx{ccontr}             (~P ==> False) ==> P
-\idx{classical}          (~P ==> P) ==> P
-\idx{excluded_middle}    ~P | P
+\tdx{ccontr}          (~P ==> False) ==> P
+\tdx{classical}       (~P ==> P) ==> P
+\tdx{excluded_middle} ~P | P

-\idx{disjCI}    (~Q ==> P) ==> P|Q
-\idx{exCI}      (! x. ~ P(x) ==> P(a)) ==> ? x.P(x)
-\idx{impCE}     [| P-->Q; ~ P ==> R; Q ==> R |] ==> R
-\idx{iffCE}     [| P=Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R
-\idx{notnotD}   ~~P ==> P
-\idx{swap}      ~P ==> (~Q ==> P) ==> Q
+\tdx{disjCI}          (~Q ==> P) ==> P|Q
+\tdx{exCI}            (! x. ~ P(x) ==> P(a)) ==> ? x.P(x)
+\tdx{impCE}           [| P-->Q; ~ P ==> R; Q ==> R |] ==> R
+\tdx{iffCE}           [| P=Q;  [| P;Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R
+\tdx{notnotD}         ~~P ==> P
+\tdx{swap}            ~P ==> (~Q ==> P) ==> Q
\subcaption{Classical logic}

-\idx{if_True}    if(True,x,y) = x
-\idx{if_False}   if(False,x,y) = y
-\idx{if_P}       P ==> if(P,x,y) = x
-\idx{if_not_P}   ~ P ==> if(P,x,y) = y
-\idx{expand_if}  P(if(Q,x,y)) = ((Q --> P(x)) & (~Q --> P(y)))
+\tdx{if_True}         if(True,x,y) = x
+\tdx{if_False}        if(False,x,y) = y
+\tdx{if_P}            P ==> if(P,x,y) = x
+\tdx{if_not_P}        ~ P ==> if(P,x,y) = y
+\tdx{expand_if}       P(if(Q,x,y)) = ((Q --> P(x)) & (~Q --> P(y)))
\subcaption{Conditionals}
\end{ttbox}
\caption{More derived rules} \label{hol-lemmas2}
\end{figure}

-\section{Rules of inference}
-The basic theory has the {\ML} identifier \ttindexbold{HOL.thy}.  However,
-many further theories are defined, introducing product and sum types, the
-natural numbers, etc.
-
-Figure~\ref{hol-rules} shows the inference rules with their~{\ML} names.
-They follow standard practice in higher-order logic: only a few connectives
-are taken as primitive, with the remainder defined obscurely.
-
-Unusually, the definitions are expressed using object-equality~({\tt=})
-rather than meta-equality~({\tt==}).  This is possible because equality in
-higher-order logic may equate formulae and even functions over formulae.
-On the other hand, meta-equality is Isabelle's usual symbol for making
-definitions.  Take care to note which form of equality is used before
-attempting a proof.
-
-Some of the rules mention type variables; for example, {\tt refl} mentions
-the type variable~{\tt'a}.  This facilitates explicit instantiation of the
-type variables.  By default, such variables range over class {\it term}.
-
-\begin{warn}
-Where function types are involved, Isabelle's unification code does not
-guarantee to find instantiations for type variables automatically.  If
-resolution fails for no obvious reason, try setting \ttindex{show_types} to
-{\tt true}, causing Isabelle to display types of terms.  (Possibly, set
-\ttindex{show_sorts} to {\tt true} also, causing Isabelle to display sorts.)
-Be prepared to use \ttindex{res_inst_tac} instead of {\tt resolve_tac}.
-Setting \ttindex{Unify.trace_types} to {\tt true} causes Isabelle to
-report omitted search paths during unification.
-\end{warn}
-
-Here are further comments on the rules:
-\begin{description}
-\item[\ttindexbold{ext}]
-expresses extensionality of functions.
-\item[\ttindexbold{iff}]
-asserts that logically equivalent formulae are equal.
-\item[\ttindexbold{selectI}]
-gives the defining property of the Hilbert $\epsilon$-operator.  The
-derived rule \ttindexbold{select_equality} (see below) is often easier to use.
-\item[\ttindexbold{True_or_False}]
-makes the logic classical.\footnote{In fact, the $\epsilon$-operator
-already makes the logic classical, as shown by Diaconescu;
-see Paulson~\cite{paulson-COLOG} for details.}
-\end{description}
-
-\begin{warn}
-\HOL\ has no if-and-only-if connective; logical equivalence is expressed
-using equality.  But equality has a high precedence, as befitting a
-relation, while if-and-only-if typically has the lowest precedence.  Thus,
-$\neg\neg P=P$ abbreviates $\neg\neg (P=P)$ and not $(\neg\neg P)=P$.  When
-using $=$ to mean logical equivalence, enclose both operands in
-parentheses.
-\end{warn}
-
Some derived rules are shown in Figures~\ref{hol-lemmas1}
and~\ref{hol-lemmas2}, with their {\ML} names.  These include natural rules
for the logical connectives, as well as sequent-style elimination rules for
conjunctions, implications, and universal quantifiers.

-Note the equality rules: \ttindexbold{ssubst} performs substitution in
-backward proofs, while \ttindexbold{box_equals} supports reasoning by
+Note the equality rules: \tdx{ssubst} performs substitution in
+backward proofs, while \tdx{box_equals} supports reasoning by
simplifying both sides of an equation.

See the files {\tt HOL/hol.thy} and
@@ -408,7 +407,7 @@
\begin{itemize}
\item
Because it includes a general substitution rule, \HOL\ instantiates the
-tactic \ttindex{hyp_subst_tac}, which substitutes for an equality
+tactic {\tt hyp_subst_tac}, which substitutes for an equality
throughout a subgoal and its hypotheses.
\item
It instantiates the simplifier, defining~\ttindexbold{HOL_ss} as the
@@ -426,31 +425,31 @@
\begin{center}
\begin{tabular}{rrr}
\it name      &\it meta-type  & \it description \\
-\index{"{"}@{\tt\{\}}}
-  {\tt\{\}}     & $\alpha\,set$         & the empty set \\
-  \idx{insert}  & $[\alpha,\alpha\,set]\To \alpha\,set$
+\index{{}@\verb'{}' symbol}
+  \verb|{}|     & $\alpha\,set$         & the empty set \\
+  \cdx{insert}  & $[\alpha,\alpha\,set]\To \alpha\,set$
& insertion of element \\
-  \idx{Collect} & $(\alpha\To bool)\To\alpha\,set$
+  \cdx{Collect} & $(\alpha\To bool)\To\alpha\,set$
& comprehension \\
-  \idx{Compl}   & $(\alpha\,set)\To\alpha\,set$
+  \cdx{Compl}   & $(\alpha\,set)\To\alpha\,set$
& complement \\
-  \idx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
+  \cdx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
& intersection over a set\\
-  \idx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
+  \cdx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
& union over a set\\
-  \idx{Inter} & $((\alpha\,set)set)\To\alpha\,set$
+  \cdx{Inter} & $((\alpha\,set)set)\To\alpha\,set$
&set of sets intersection \\
-  \idx{Union} & $((\alpha\,set)set)\To\alpha\,set$
+  \cdx{Union} & $((\alpha\,set)set)\To\alpha\,set$
&set of sets union \\
-  \idx{range}   & $(\alpha\To\beta )\To\beta\,set$
+  \cdx{range}   & $(\alpha\To\beta )\To\beta\,set$
& range of a function \$1ex] - \idx{Ball}~~\idx{Bex} & [\alpha\,set,\alpha\To bool]\To bool + \cdx{Ball}~~\cdx{Bex} & [\alpha\,set,\alpha\To bool]\To bool & bounded quantifiers \\ - \idx{mono} & (\alpha\,set\To\beta\,set)\To bool + \cdx{mono} & (\alpha\,set\To\beta\,set)\To bool & monotonicity \\ - \idx{inj}~~\idx{surj}& (\alpha\To\beta )\To bool + \cdx{inj}~~\cdx{surj}& (\alpha\To\beta )\To bool & injective/surjective \\ - \idx{inj_onto} & [\alpha\To\beta ,\alpha\,set]\To bool + \cdx{inj_onto} & [\alpha\To\beta ,\alpha\,set]\To bool & injective over subset \end{tabular} \end{center} @@ -458,26 +457,26 @@ \begin{center} \begin{tabular}{llrrr} - \it symbol &\it name &\it meta-type & \it prec & \it description \\ - \idx{INT} & \idx{INTER1} & (\alpha\To\beta\,set)\To\beta\,set & 10 & + \it symbol &\it name &\it meta-type & \it priority & \it description \\ + \sdx{INT} & \cdx{INTER1} & (\alpha\To\beta\,set)\To\beta\,set & 10 & intersection over a type\\ - \idx{UN} & \idx{UNION1} & (\alpha\To\beta\,set)\To\beta\,set & 10 & + \sdx{UN} & \cdx{UNION1} & (\alpha\To\beta\,set)\To\beta\,set & 10 & union over a type \end{tabular} \end{center} \subcaption{Binders} \begin{center} -\indexbold{*""} -\indexbold{*":} -\indexbold{*"<"=} +\index{*"" symbol} +\index{*": symbol} +\index{*"<"= symbol} \begin{tabular}{rrrr} - \it symbol & \it meta-type & \it precedence & \it description \\ + \it symbol & \it meta-type & \it priority & \it description \\ \tt  & [\alpha\To\beta ,\alpha\,set]\To (\beta\,set) & Left 90 & image \\ - \idx{Int} & [\alpha\,set,\alpha\,set]\To\alpha\,set + \sdx{Int} & [\alpha\,set,\alpha\,set]\To\alpha\,set & Left 70 & intersection (\inter) \\ - \idx{Un} & [\alpha\,set,\alpha\,set]\To\alpha\,set + \sdx{Un} & [\alpha\,set,\alpha\,set]\To\alpha\,set & Left 65 & union (\union) \\ \tt: & [\alpha ,\alpha\,set]\To bool & Left 50 & membership (\in) \\ @@ -486,38 +485,34 @@ \end{tabular} \end{center} \subcaption{Infixes} -\caption{Syntax of \HOL's set theory} \label{hol-set-syntax} +\caption{Syntax of the theory {\tt Set}} \label{hol-set-syntax} \end{figure} \begin{figure} \begin{center} \tt\frenchspacing -\index{*"!|bold} +\index{*"! symbol} \begin{tabular}{rrr} \it external & \it internal & \it description \\ - a \ttilde: b & \ttilde(a : b) & \rm negated membership\\ - \{a@1, \ldots, a@n\} & insert(a@1,\cdots,insert(a@n,\{\})) & - \rm finite set \\ + a \ttilde: b & \ttilde(a : b) & \rm non-membership\\ + \{a@1, \ldots\} & insert(a@1, \ldots\{\}) & \rm finite set \\ \{x.P[x]\} & Collect(\lambda x.P[x]) & \rm comprehension \\ - \idx{INT} x:A.B[x] & INTER(A,\lambda x.B[x]) & - \rm intersection over a set \\ - \idx{UN} x:A.B[x] & UNION(A,\lambda x.B[x]) & - \rm union over a set \\ - \tt ! x:A.P[x] & Ball(A,\lambda x.P[x]) & + \sdx{INT} x:A.B[x] & INTER(A,\lambda x.B[x]) & + \rm intersection \\ + \sdx{UN}{\tt\ } x:A.B[x] & UNION(A,\lambda x.B[x]) & + \rm union \\ + \tt ! x:A.P[x] or \sdx{ALL} x:A.P[x] & + Ball(A,\lambda x.P[x]) & \rm bounded \forall \\ - \idx{?} x:A.P[x] & Bex(A,\lambda x.P[x]) & - \rm bounded \exists \\[1ex] - \idx{ALL} x:A.P[x] & Ball(A,\lambda x.P[x]) & - \rm bounded \forall \\ - \idx{EX} x:A.P[x] & Bex(A,\lambda x.P[x]) & - \rm bounded \exists + \sdx{?} x:A.P[x] or \sdx{EX}{\tt\ } x:A.P[x] & + Bex(A,\lambda x.P[x]) & \rm bounded \exists \end{tabular} \end{center} \subcaption{Translations} \dquotes -\[\begin{array}{rcl} +\[\begin{array}{rclcl} term & = & \hbox{other terms\ldots} \\ & | & "\{\}" \\ & | & "\{ " term\; ("," term)^* " \}" \\ @@ -533,130 +528,17 @@ & | & term " : " term \\ & | & term " \ttilde: " term \\ & | & term " <= " term \\ - & | & "!~~~" id ":" term " . " formula \\ - & | & "?~~~" id ":" term " . " formula \\ + & | & "!~" id ":" term " . " formula & | & "ALL " id ":" term " . " formula \\ + & | & "?~" id ":" term " . " formula & | & "EX~~" id ":" term " . " formula \end{array}$
\subcaption{Full Grammar}
-\caption{Syntax of \HOL's set theory (continued)} \label{hol-set-syntax2}
+\caption{Syntax of the theory {\tt Set} (continued)} \label{hol-set-syntax2}
\end{figure}

-\begin{figure} \underscoreon
-\begin{ttbox}
-\idx{mem_Collect_eq}    (a : \{x.P(x)\}) = P(a)
-\idx{Collect_mem_eq}    \{x.x:A\} = A
-\subcaption{Isomorphisms between predicates and sets}
-
-\idx{empty_def}         \{\}          == \{x.x=False\}
-\idx{insert_def}        insert(a,B) == \{x.x=a\} Un B
-\idx{Ball_def}          Ball(A,P)   == ! x. x:A --> P(x)
-\idx{Bex_def}           Bex(A,P)    == ? x. x:A & P(x)
-\idx{subset_def}        A <= B      == ! x:A. x:B
-\idx{Un_def}            A Un B      == \{x.x:A | x:B\}
-\idx{Int_def}           A Int B     == \{x.x:A & x:B\}
-\idx{set_diff_def}      A - B       == \{x.x:A & x~:B\}
-\idx{Compl_def}         Compl(A)    == \{x. ~ x:A\}
-\idx{INTER_def}         INTER(A,B)  == \{y. ! x:A. y: B(x)\}
-\idx{UNION_def}         UNION(A,B)  == \{y. ? x:A. y: B(x)\}
-\idx{INTER1_def}        INTER1(B)   == INTER(\{x.True\}, B)
-\idx{UNION1_def}        UNION1(B)   == UNION(\{x.True\}, B)
-\idx{Inter_def}         Inter(S)    == (INT x:S. x)
-\idx{Union_def}         Union(S)    ==  (UN x:S. x)
-\idx{image_def}         fA        == \{y. ? x:A. y=f(x)\}
-\idx{range_def}         range(f)    == \{y. ? x. y=f(x)\}
-\idx{mono_def}          mono(f)     == !A B. A <= B --> f(A) <= f(B)
-\idx{inj_def}           inj(f)      == ! x y. f(x)=f(y) --> x=y
-\idx{surj_def}          surj(f)     == ! y. ? x. y=f(x)
-\idx{inj_onto_def}      inj_onto(f,A) == !x:A. !y:A. f(x)=f(y) --> x=y
-\subcaption{Definitions}
-\end{ttbox}
-\caption{Rules of \HOL's set theory} \label{hol-set-rules}
-\end{figure}
-
-
-\begin{figure} \underscoreon
-\begin{ttbox}
-\idx{CollectI}      [| P(a) |] ==> a : \{x.P(x)\}
-\idx{CollectD}      [| a : \{x.P(x)\} |] ==> P(a)
-\idx{CollectE}      [| a : \{x.P(x)\};  P(a) ==> W |] ==> W
-\idx{Collect_cong}  [| !!x. P(x)=Q(x) |] ==> \{x. P(x)\} = \{x. Q(x)\}
-\subcaption{Comprehension}
-
-\idx{ballI}         [| !!x. x:A ==> P(x) |] ==> ! x:A. P(x)
-\idx{bspec}         [| ! x:A. P(x);  x:A |] ==> P(x)
-\idx{ballE}         [| ! x:A. P(x);  P(x) ==> Q;  ~ x:A ==> Q |] ==> Q
-\idx{ball_cong}     [| A=A';  !!x. x:A' ==> P(x) = P'(x) |] ==>
-              (! x:A. P(x)) = (! x:A'. P'(x))
-
-\idx{bexI}          [| P(x);  x:A |] ==> ? x:A. P(x)
-\idx{bexCI}         [| ! x:A. ~ P(x) ==> P(a);  a:A |] ==> ? x:A.P(x)
-\idx{bexE}          [| ? x:A. P(x);  !!x. [| x:A; P(x) |] ==> Q  |] ==> Q
-\subcaption{Bounded quantifiers}
-
-\idx{subsetI}         (!!x.x:A ==> x:B) ==> A <= B
-\idx{subsetD}         [| A <= B;  c:A |] ==> c:B
-\idx{subsetCE}        [| A <= B;  ~ (c:A) ==> P;  c:B ==> P |] ==> P
-
-\idx{subset_refl}     A <= A
-\idx{subset_antisym}  [| A <= B;  B <= A |] ==> A = B
-\idx{subset_trans}    [| A<=B;  B<=C |] ==> A<=C
-
-\idx{set_ext}         [| !!x. (x:A) = (x:B) |] ==> A = B
-\idx{equalityD1}      A = B ==> A<=B
-\idx{equalityD2}      A = B ==> B<=A
-\idx{equalityE}       [| A = B;  [| A<=B; B<=A |] ==> P |]  ==>  P
-
-\idx{equalityCE}      [| A = B;  [| c:A; c:B |] ==> P;
-                           [| ~ c:A; ~ c:B |] ==> P
-                |]  ==>  P
-\subcaption{The subset and equality relations}
-\end{ttbox}
-\caption{Derived rules for set theory} \label{hol-set1}
-\end{figure}
-
-
-\begin{figure} \underscoreon
-\begin{ttbox}
-\idx{emptyE}   a : \{\} ==> P
-
-\idx{insertI1} a : insert(a,B)
-\idx{insertI2} a : B ==> a : insert(b,B)
-\idx{insertE}  [| a : insert(b,A);  a=b ==> P;  a:A ==> P |] ==> P
-
-\idx{ComplI}   [| c:A ==> False |] ==> c : Compl(A)
-\idx{ComplD}   [| c : Compl(A) |] ==> ~ c:A
-
-\idx{UnI1}     c:A ==> c : A Un B
-\idx{UnI2}     c:B ==> c : A Un B
-\idx{UnCI}     (~c:B ==> c:A) ==> c : A Un B
-\idx{UnE}      [| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P
-
-\idx{IntI}     [| c:A;  c:B |] ==> c : A Int B
-\idx{IntD1}    c : A Int B ==> c:A
-\idx{IntD2}    c : A Int B ==> c:B
-\idx{IntE}     [| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P
-
-\idx{UN_I}     [| a:A;  b: B(a) |] ==> b: (UN x:A. B(x))
-\idx{UN_E}     [| b: (UN x:A. B(x));  !!x.[| x:A;  b:B(x) |] ==> R |] ==> R
-
-\idx{INT_I}    (!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))
-\idx{INT_D}    [| b: (INT x:A. B(x));  a:A |] ==> b: B(a)
-\idx{INT_E}    [| b: (INT x:A. B(x));  b: B(a) ==> R;  ~ a:A ==> R |] ==> R
-
-\idx{UnionI}   [| X:C;  A:X |] ==> A : Union(C)
-\idx{UnionE}   [| A : Union(C);  !!X.[| A:X;  X:C |] ==> R |] ==> R
-
-\idx{InterI}   [| !!X. X:C ==> A:X |] ==> A : Inter(C)
-\idx{InterD}   [| A : Inter(C);  X:C |] ==> A:X
-\idx{InterE}   [| A : Inter(C);  A:X ==> R;  ~ X:C ==> R |] ==> R
-\end{ttbox}
-\caption{Further derived rules for set theory} \label{hol-set2}
-\end{figure}
-
-
\section{A formulation of set theory}
Historically, higher-order logic gives a foundation for Russell and
Whitehead's theory of classes.  Let us use modern terminology and call them
@@ -677,100 +559,219 @@
do in~{\ZF}.  In \HOL\ the intersection of the empty set is well-defined,
denoting the universal set for the given type.

-\subsection{Syntax of set theory}
-The type $\alpha\,set$ is essentially the same as $\alpha\To bool$.  The
-new type is defined for clarity and to avoid complications involving
-function types in unification.  Since Isabelle does not support type
-definitions (as mentioned in \S\ref{HOL-types}), the isomorphisms between
-the two types are declared explicitly.  Here they are natural: {\tt
-  Collect} maps $\alpha\To bool$ to $\alpha\,set$, while \hbox{\tt op :}
-maps in the other direction (ignoring argument order).
+
+\subsection{Syntax of set theory}\index{*set type}
+\HOL's set theory is called \thydx{Set}.  The type $\alpha\,set$ is
+essentially the same as $\alpha\To bool$.  The new type is defined for
+clarity and to avoid complications involving function types in unification.
+Since Isabelle does not support type definitions (as mentioned in
+\S\ref{HOL-types}), the isomorphisms between the two types are declared
+explicitly.  Here they are natural: {\tt Collect} maps $\alpha\To bool$ to
+$\alpha\,set$, while \hbox{\tt op :} maps in the other direction (ignoring
+argument order).

Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax
translations.  Figure~\ref{hol-set-syntax2} presents the grammar of the new
constructs.  Infix operators include union and intersection ($A\union B$
and $A\inter B$), the subset and membership relations, and the image
-operator~{\tt}.  Note that $a$\verb|~:|$b$ is translated to
-\verb|~(|$a$:$b$\verb|)|.  The {\tt\{\ldots\}} notation abbreviates finite
-sets constructed in the obvious manner using~{\tt insert} and~$\{\}$ (the
-empty set):
+operator~{\tt}\@.  Note that $a$\verb|~:|$b$ is translated to
+$\neg(a\in b)$.
+
+The {\tt\{\ldots\}} notation abbreviates finite sets constructed in the
+obvious manner using~{\tt insert} and~$\{\}$:
\begin{eqnarray*}
- \{a,b,c\} & \equiv & {\tt insert}(a,{\tt insert}(b,{\tt insert}(c,\{\})))
+  \{a@1, \ldots, a@n\}  & \equiv &
+  {\tt insert}(a@1,\ldots,{\tt insert}(a@n,\{\}))
\end{eqnarray*}

The set \hbox{\tt\{$x$.$P[x]$\}} consists of all $x$ (of suitable type)
that satisfy~$P[x]$, where $P[x]$ is a formula that may contain free
-occurrences of~$x$.  This syntax expands to \ttindexbold{Collect}$(\lambda -x.P[x])$.
+occurrences of~$x$.  This syntax expands to \cdx{Collect}$(\lambda +x.P[x])$.  It defines sets by absolute comprehension, which is impossible
+in~{\ZF}; the type of~$x$ implicitly restricts the comprehension.

The set theory defines two {\bf bounded quantifiers}:
\begin{eqnarray*}
-   \forall x\in A.P[x] &\hbox{which abbreviates}& \forall x. x\in A\imp P[x] \\
-   \exists x\in A.P[x] &\hbox{which abbreviates}& \exists x. x\in A\conj P[x]
+   \forall x\in A.P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\
+   \exists x\in A.P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x]
\end{eqnarray*}
-The constants~\ttindexbold{Ball} and~\ttindexbold{Bex} are defined
+The constants~\cdx{Ball} and~\cdx{Bex} are defined
accordingly.  Instead of {\tt Ball($A$,$P$)} and {\tt Bex($A$,$P$)} we may
-write\index{*"!}\index{*"?}\index{*ALL}\index{*EX}
-\hbox{\tt !~$x$:$A$.$P[x]$} and \hbox{\tt ?~$x$:$A$.$P[x]$}.
-Isabelle's usual notation, \ttindex{ALL} and \ttindex{EX}, is also
-available.  As with
-ordinary quantifiers, the contents of \ttindexbold{HOL_quantifiers} specifies
-which notation should be used for output.
+write\index{*"! symbol}\index{*"? symbol}
+\index{*ALL symbol}\index{*EX symbol}
+%
+\hbox{\tt !~$x$:$A$.$P[x]$} and \hbox{\tt ?~$x$:$A$.$P[x]$}.  Isabelle's
+usual quantifier symbols, \sdx{ALL} and \sdx{EX}, are also accepted
+for input.  As with the primitive quantifiers, the {\ML} reference
+\ttindex{HOL_quantifiers} specifies which notation to use for output.

Unions and intersections over sets, namely $\bigcup@{x\in A}B[x]$ and
$\bigcap@{x\in A}B[x]$, are written
-\ttindexbold{UN}~\hbox{\tt$x$:$A$.$B[x]$} and
-\ttindexbold{INT}~\hbox{\tt$x$:$A$.$B[x]$}.
-Unions and intersections over types, namely $\bigcup@x B[x]$ and
-$\bigcap@x B[x]$, are written
-\ttindexbold{UN}~\hbox{\tt$x$.$B[x]$} and
-\ttindexbold{INT}~\hbox{\tt$x$.$B[x]$}; they are equivalent to the previous
-union/intersection operators when $A$ is the universal set.
-The set of set union and intersection operators ($\bigcup A$ and $\bigcap -A$) are not binders, but equals $\bigcup@{x\in A}x$ and $\bigcap@{x\in - A}x$, respectively.
+\sdx{UN}~\hbox{\tt$x$:$A$.$B[x]$} and
+\sdx{INT}~\hbox{\tt$x$:$A$.$B[x]$}.
+
+Unions and intersections over types, namely $\bigcup@x B[x]$ and $\bigcap@x +B[x]$, are written \sdx{UN}~\hbox{\tt$x$.$B[x]$} and
+\sdx{INT}~\hbox{\tt$x$.$B[x]$}.  They are equivalent to the previous
+union and intersection operators when $A$ is the universal set.
+
+The operators $\bigcup A$ and $\bigcap A$ act upon sets of sets.  They are
+not binders, but are equal to $\bigcup@{x\in A}x$ and $\bigcap@{x\in A}x$,
+respectively.
+
+
+\begin{figure} \underscoreon
+\begin{ttbox}
+\tdx{mem_Collect_eq}    (a : \{x.P(x)\}) = P(a)
+\tdx{Collect_mem_eq}    \{x.x:A\} = A

-\subsection{Axioms and rules of set theory}
-The axioms \ttindexbold{mem_Collect_eq} and
-\ttindexbold{Collect_mem_eq} assert that the functions {\tt Collect} and
-\hbox{\tt op :} are isomorphisms.
-All the other axioms are definitions; see Fig.\ts \ref{hol-set-rules}.
-These include straightforward properties of functions: image~({\tt}) and
-{\tt range}, and predicates concerning monotonicity, injectiveness, etc.
+\tdx{empty_def}         \{\}          == \{x.x=False\}
+\tdx{insert_def}        insert(a,B) == \{x.x=a\} Un B
+\tdx{Ball_def}          Ball(A,P)   == ! x. x:A --> P(x)
+\tdx{Bex_def}           Bex(A,P)    == ? x. x:A & P(x)
+\tdx{subset_def}        A <= B      == ! x:A. x:B
+\tdx{Un_def}            A Un B      == \{x.x:A | x:B\}
+\tdx{Int_def}           A Int B     == \{x.x:A & x:B\}
+\tdx{set_diff_def}      A - B       == \{x.x:A & x~:B\}
+\tdx{Compl_def}         Compl(A)    == \{x. ~ x:A\}
+\tdx{INTER_def}         INTER(A,B)  == \{y. ! x:A. y: B(x)\}
+\tdx{UNION_def}         UNION(A,B)  == \{y. ? x:A. y: B(x)\}
+\tdx{INTER1_def}        INTER1(B)   == INTER(\{x.True\}, B)
+\tdx{UNION1_def}        UNION1(B)   == UNION(\{x.True\}, B)
+\tdx{Inter_def}         Inter(S)    == (INT x:S. x)
+\tdx{Union_def}         Union(S)    ==  (UN x:S. x)
+\tdx{image_def}         fA        == \{y. ? x:A. y=f(x)\}
+\tdx{range_def}         range(f)    == \{y. ? x. y=f(x)\}
+\tdx{mono_def}          mono(f)     == !A B. A <= B --> f(A) <= f(B)
+\tdx{inj_def}           inj(f)      == ! x y. f(x)=f(y) --> x=y
+\tdx{surj_def}          surj(f)     == ! y. ? x. y=f(x)
+\tdx{inj_onto_def}      inj_onto(f,A) == !x:A. !y:A. f(x)=f(y) --> x=y
+\end{ttbox}
+\caption{Rules of the theory {\tt Set}} \label{hol-set-rules}
+\end{figure}
+

-\HOL's set theory has the {\ML} identifier \ttindexbold{Set.thy}.
+\begin{figure} \underscoreon
+\begin{ttbox}
+\tdx{CollectI}        [| P(a) |] ==> a : \{x.P(x)\}
+\tdx{CollectD}        [| a : \{x.P(x)\} |] ==> P(a)
+\tdx{CollectE}        [| a : \{x.P(x)\};  P(a) ==> W |] ==> W
+
+\tdx{ballI}           [| !!x. x:A ==> P(x) |] ==> ! x:A. P(x)
+\tdx{bspec}           [| ! x:A. P(x);  x:A |] ==> P(x)
+\tdx{ballE}           [| ! x:A. P(x);  P(x) ==> Q;  ~ x:A ==> Q |] ==> Q
+
+\tdx{bexI}            [| P(x);  x:A |] ==> ? x:A. P(x)
+\tdx{bexCI}           [| ! x:A. ~ P(x) ==> P(a);  a:A |] ==> ? x:A.P(x)
+\tdx{bexE}            [| ? x:A. P(x);  !!x. [| x:A; P(x) |] ==> Q  |] ==> Q
+\subcaption{Comprehension and Bounded quantifiers}
+
+\tdx{subsetI}         (!!x.x:A ==> x:B) ==> A <= B
+\tdx{subsetD}         [| A <= B;  c:A |] ==> c:B
+\tdx{subsetCE}        [| A <= B;  ~ (c:A) ==> P;  c:B ==> P |] ==> P
+
+\tdx{subset_refl}     A <= A
+\tdx{subset_antisym}  [| A <= B;  B <= A |] ==> A = B
+\tdx{subset_trans}    [| A<=B;  B<=C |] ==> A<=C
+
+\tdx{set_ext}         [| !!x. (x:A) = (x:B) |] ==> A = B
+\tdx{equalityD1}      A = B ==> A<=B
+\tdx{equalityD2}      A = B ==> B<=A
+\tdx{equalityE}       [| A = B;  [| A<=B; B<=A |] ==> P |]  ==>  P
+
+\tdx{equalityCE}      [| A = B;  [| c:A; c:B |] ==> P;
+                           [| ~ c:A; ~ c:B |] ==> P
+                |]  ==>  P
+\subcaption{The subset and equality relations}
+\end{ttbox}
+\caption{Derived rules for set theory} \label{hol-set1}
+\end{figure}
+

\begin{figure} \underscoreon
\begin{ttbox}
-\idx{imageI}     [| x:A |] ==> f(x) : fA
-\idx{imageE}     [| b : fA;  !!x.[| b=f(x);  x:A |] ==> P |] ==> P
+\tdx{emptyE}   a : \{\} ==> P
+
+\tdx{insertI1} a : insert(a,B)
+\tdx{insertI2} a : B ==> a : insert(b,B)
+\tdx{insertE}  [| a : insert(b,A);  a=b ==> P;  a:A ==> P |] ==> P

-\idx{rangeI}     f(x) : range(f)
-\idx{rangeE}     [| b : range(f);  !!x.[| b=f(x) |] ==> P |] ==> P
+\tdx{ComplI}   [| c:A ==> False |] ==> c : Compl(A)
+\tdx{ComplD}   [| c : Compl(A) |] ==> ~ c:A
+
+\tdx{UnI1}     c:A ==> c : A Un B
+\tdx{UnI2}     c:B ==> c : A Un B
+\tdx{UnCI}     (~c:B ==> c:A) ==> c : A Un B
+\tdx{UnE}      [| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P

-\idx{monoI}      [| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)
-\idx{monoD}      [| mono(f);  A <= B |] ==> f(A) <= f(B)
+\tdx{IntI}     [| c:A;  c:B |] ==> c : A Int B
+\tdx{IntD1}    c : A Int B ==> c:A
+\tdx{IntD2}    c : A Int B ==> c:B
+\tdx{IntE}     [| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P
+
+\tdx{UN_I}     [| a:A;  b: B(a) |] ==> b: (UN x:A. B(x))
+\tdx{UN_E}     [| b: (UN x:A. B(x));  !!x.[| x:A;  b:B(x) |] ==> R |] ==> R

-\idx{injI}       [| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)
-\idx{inj_inverseI}              (!!x. g(f(x)) = x) ==> inj(f)
-\idx{injD}       [| inj(f); f(x) = f(y) |] ==> x=y
+\tdx{INT_I}    (!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))
+\tdx{INT_D}    [| b: (INT x:A. B(x));  a:A |] ==> b: B(a)
+\tdx{INT_E}    [| b: (INT x:A. B(x));  b: B(a) ==> R;  ~ a:A ==> R |] ==> R
+
+\tdx{UnionI}   [| X:C;  A:X |] ==> A : Union(C)
+\tdx{UnionE}   [| A : Union(C);  !!X.[| A:X;  X:C |] ==> R |] ==> R
+
+\tdx{InterI}   [| !!X. X:C ==> A:X |] ==> A : Inter(C)
+\tdx{InterD}   [| A : Inter(C);  X:C |] ==> A:X
+\tdx{InterE}   [| A : Inter(C);  A:X ==> R;  ~ X:C ==> R |] ==> R
+\end{ttbox}
+\caption{Further derived rules for set theory} \label{hol-set2}
+\end{figure}
+

-\idx{Inv_f_f}    inj(f) ==> Inv(f,f(x)) = x
-\idx{f_Inv_f}    y : range(f) ==> f(Inv(f,y)) = y
+\subsection{Axioms and rules of set theory}
+Figure~\ref{hol-set-rules} presents the rules of theory \thydx{Set}.  The
+axioms \tdx{mem_Collect_eq} and \tdx{Collect_mem_eq} assert
+that the functions {\tt Collect} and \hbox{\tt op :} are isomorphisms.  Of
+course, \hbox{\tt op :} also serves as the membership relation.

-\idx{Inv_injective}
-    [| Inv(f,x)=Inv(f,y); x: range(f);  y: range(f) |] ==> x=y
+All the other axioms are definitions.  They include the empty set, bounded
+quantifiers, unions, intersections, complements and the subset relation.
+They also include straightforward properties of functions: image~({\tt}) and
+{\tt range}, and predicates concerning monotonicity, injectiveness and
+surjectiveness.
+
+The predicate \cdx{inj_onto} is used for simulating type definitions.
+The statement ${\tt inj_onto}(f,A)$ asserts that $f$ is injective on the
+set~$A$, which specifies a subset of its domain type.  In a type
+definition, $f$ is the abstraction function and $A$ is the set of valid
+representations; we should not expect $f$ to be injective outside of~$A$.
+
+\begin{figure} \underscoreon
+\begin{ttbox}
+\tdx{Inv_f_f}    inj(f) ==> Inv(f,f(x)) = x
+\tdx{f_Inv_f}    y : range(f) ==> f(Inv(f,y)) = y

-\idx{inj_ontoI}
-    (!! x y. [| f(x) = f(y); x:A; y:A |] ==> x=y) ==> inj_onto(f,A)
+%\tdx{Inv_injective}
+%    [| Inv(f,x)=Inv(f,y); x: range(f);  y: range(f) |] ==> x=y
+%
+\tdx{imageI}     [| x:A |] ==> f(x) : fA
+\tdx{imageE}     [| b : fA;  !!x.[| b=f(x);  x:A |] ==> P |] ==> P
+
+\tdx{rangeI}     f(x) : range(f)
+\tdx{rangeE}     [| b : range(f);  !!x.[| b=f(x) |] ==> P |] ==> P

-\idx{inj_onto_inverseI}
+\tdx{monoI}      [| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)
+\tdx{monoD}      [| mono(f);  A <= B |] ==> f(A) <= f(B)
+
+\tdx{injI}       [| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)
+\tdx{inj_inverseI}              (!!x. g(f(x)) = x) ==> inj(f)
+\tdx{injD}       [| inj(f); f(x) = f(y) |] ==> x=y
+
+\tdx{inj_ontoI}  (!!x y. [| f(x)=f(y); x:A; y:A |] ==> x=y) ==> inj_onto(f,A)
+\tdx{inj_ontoD}  [| inj_onto(f,A);  f(x)=f(y);  x:A;  y:A |] ==> x=y
+
+\tdx{inj_onto_inverseI}
(!!x. x:A ==> g(f(x)) = x) ==> inj_onto(f,A)
-
-\idx{inj_ontoD}
-    [| inj_onto(f,A);  f(x)=f(y);  x:A;  y:A |] ==> x=y
-
[| inj_onto(f,A);  x~=y;  x:A;  y:A |] ==> ~ f(x)=f(y)
\end{ttbox}
\caption{Derived rules involving functions} \label{hol-fun}
@@ -779,406 +780,431 @@

\begin{figure} \underscoreon
\begin{ttbox}
-\idx{Union_upper}     B:A ==> B <= Union(A)
-\idx{Union_least}     [| !!X. X:A ==> X<=C |] ==> Union(A) <= C
+\tdx{Union_upper}     B:A ==> B <= Union(A)
+\tdx{Union_least}     [| !!X. X:A ==> X<=C |] ==> Union(A) <= C

-\idx{Inter_lower}     B:A ==> Inter(A) <= B
-\idx{Inter_greatest}  [| !!X. X:A ==> C<=X |] ==> C <= Inter(A)
+\tdx{Inter_lower}     B:A ==> Inter(A) <= B
+\tdx{Inter_greatest}  [| !!X. X:A ==> C<=X |] ==> C <= Inter(A)

-\idx{Un_upper1}       A <= A Un B
-\idx{Un_upper2}       B <= A Un B
-\idx{Un_least}        [| A<=C;  B<=C |] ==> A Un B <= C
+\tdx{Un_upper1}       A <= A Un B
+\tdx{Un_upper2}       B <= A Un B
+\tdx{Un_least}        [| A<=C;  B<=C |] ==> A Un B <= C

-\idx{Int_lower1}      A Int B <= A
-\idx{Int_lower2}      A Int B <= B
-\idx{Int_greatest}    [| C<=A;  C<=B |] ==> C <= A Int B
+\tdx{Int_lower1}      A Int B <= A
+\tdx{Int_lower2}      A Int B <= B
+\tdx{Int_greatest}    [| C<=A;  C<=B |] ==> C <= A Int B
\end{ttbox}
\caption{Derived rules involving subsets} \label{hol-subset}
\end{figure}

-\begin{figure} \underscoreon
+\begin{figure} \underscoreon   \hfuzz=4pt%suppress "Overfull \hbox" message
\begin{ttbox}
-\idx{Int_absorb}         A Int A = A
-\idx{Int_commute}        A Int B = B Int A
-\idx{Int_assoc}          (A Int B) Int C  =  A Int (B Int C)
-\idx{Int_Un_distrib}     (A Un B)  Int C  =  (A Int C) Un (B Int C)
+\tdx{Int_absorb}        A Int A = A
+\tdx{Int_commute}       A Int B = B Int A
+\tdx{Int_assoc}         (A Int B) Int C  =  A Int (B Int C)
+\tdx{Int_Un_distrib}    (A Un B)  Int C  =  (A Int C) Un (B Int C)

-\idx{Un_absorb}          A Un A = A
-\idx{Un_commute}         A Un B = B Un A
-\idx{Un_assoc}           (A Un B)  Un C  =  A Un (B Un C)
-\idx{Un_Int_distrib}     (A Int B) Un C  =  (A Un C) Int (B Un C)
+\tdx{Un_absorb}         A Un A = A
+\tdx{Un_commute}        A Un B = B Un A
+\tdx{Un_assoc}          (A Un B)  Un C  =  A Un (B Un C)
+\tdx{Un_Int_distrib}    (A Int B) Un C  =  (A Un C) Int (B Un C)

-\idx{Compl_disjoint}     A Int Compl(A) = \{x.False\}
-\idx{Compl_partition}    A Un  Compl(A) = \{x.True\}
-\idx{double_complement}  Compl(Compl(A)) = A
-\idx{Compl_Un}           Compl(A Un B)  = Compl(A) Int Compl(B)
-\idx{Compl_Int}          Compl(A Int B) = Compl(A) Un Compl(B)
+\tdx{Compl_disjoint}    A Int Compl(A) = \{x.False\}
+\tdx{Compl_partition}   A Un  Compl(A) = \{x.True\}
+\tdx{double_complement} Compl(Compl(A)) = A
+\tdx{Compl_Un}          Compl(A Un B)  = Compl(A) Int Compl(B)
+\tdx{Compl_Int}         Compl(A Int B) = Compl(A) Un Compl(B)

-\idx{Union_Un_distrib}   Union(A Un B) = Union(A) Un Union(B)
-\idx{Int_Union}          A Int Union(B) = (UN C:B. A Int C)
-\idx{Un_Union_image}
-    (UN x:C. A(x) Un B(x)) = Union(AC)  Un  Union(BC)
+\tdx{Union_Un_distrib}  Union(A Un B) = Union(A) Un Union(B)
+\tdx{Int_Union}         A Int Union(B) = (UN C:B. A Int C)
+\tdx{Un_Union_image}    (UN x:C. A(x) Un B(x)) = Union(AC) Un Union(BC)

-\idx{Inter_Un_distrib}   Inter(A Un B) = Inter(A) Int Inter(B)
-\idx{Un_Inter}           A Un Inter(B) = (INT C:B. A Un C)
-\idx{Int_Inter_image}
-   (INT x:C. A(x) Int B(x)) = Inter(AC) Int Inter(BC)
+\tdx{Inter_Un_distrib}  Inter(A Un B) = Inter(A) Int Inter(B)
+\tdx{Un_Inter}          A Un Inter(B) = (INT C:B. A Un C)
+\tdx{Int_Inter_image}   (INT x:C. A(x) Int B(x)) = Inter(AC) Int Inter(BC)
\end{ttbox}
\caption{Set equalities} \label{hol-equalities}
\end{figure}

-\subsection{Derived rules for sets}
-Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules.  Most
-are obvious and resemble rules of Isabelle's {\ZF} set theory.  The
-rules named $XXX${\tt_cong} break down equalities.  Certain rules, such as
-\ttindexbold{subsetCE}, \ttindexbold{bexCI} and \ttindexbold{UnCI}, are
-designed for classical reasoning; the more natural rules \ttindexbold{subsetD},
-\ttindexbold{bexI}, \ttindexbold{Un1} and~\ttindexbold{Un2} are not
-strictly necessary.  Similarly, \ttindexbold{equalityCE} supports classical
-reasoning about extensionality, after the fashion of \ttindex{iffCE}.  See
-the file {\tt HOL/set.ML} for proofs pertaining to set theory.
+Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules.  Most are
+obvious and resemble rules of Isabelle's {\ZF} set theory.  Certain rules,
+such as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI},
+are designed for classical reasoning; the rules \tdx{subsetD},
+\tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are not
+strictly necessary but yield more natural proofs.  Similarly,
+\tdx{equalityCE} supports classical reasoning about extensionality,
+after the fashion of \tdx{iffCE}.  See the file {\tt HOL/set.ML} for
+proofs pertaining to set theory.

-Figure~\ref{hol-fun} presents derived inference rules involving functions.  See
-the file {\tt HOL/fun.ML} for a complete listing.
+Figure~\ref{hol-fun} presents derived inference rules involving functions.
+They also include rules for \cdx{Inv}, which is defined in theory~{\tt
+  HOL}; note that ${\tt Inv}(f)$ applies the Axiom of Choice to yield an
+inverse of~$f$.  They also include natural deduction rules for the image
+and range operators, and for the predicates {\tt inj} and {\tt inj_onto}.
+Reasoning about function composition (the operator~\sdx{o}) and the
+predicate~\cdx{surj} is done simply by expanding the definitions.  See
+the file {\tt HOL/fun.ML} for a complete listing of the derived rules.

Figure~\ref{hol-subset} presents lattice properties of the subset relation.
-See the file {\tt HOL/subset.ML}.
+Unions form least upper bounds; non-empty intersections form greatest lower
+bounds.  Reasoning directly about subsets often yields clearer proofs than
+reasoning about the membership relation.  See the file {\tt HOL/subset.ML}.

-Figure~\ref{hol-equalities} presents set equalities.  See
-{\tt HOL/equalities.ML}.
+Figure~\ref{hol-equalities} presents many common set equalities.  They
+include commutative, associative and distributive laws involving unions,
+intersections and complements.  The proofs are mostly trivial, using the
+classical reasoner; see file {\tt HOL/equalities.ML}.

\begin{figure}
-\begin{center}
-\begin{tabular}{rrr}
-  \it name      &\it meta-type  & \it description \\
-  \idx{Pair}    & $[\alpha,\beta]\To \alpha\times\beta$
-        & ordered pairs $\langle a,b\rangle$ \\
-  \idx{fst}     & $\alpha\times\beta \To \alpha$        & first projection\\
-  \idx{snd}     & $\alpha\times\beta \To \beta$         & second projection\\
-  \idx{split}   & $[\alpha\times\beta, [\alpha,\beta]\To\gamma] \To \gamma$
-        & generalized projection\\
-  \idx{Sigma}  &
+\begin{constants}
+  \cdx{Pair}    & $[\alpha,\beta]\To \alpha\times\beta$
+        & & ordered pairs $\langle a,b\rangle$ \\
+  \cdx{fst}     & $\alpha\times\beta \To \alpha$        & & first projection\\
+  \cdx{snd}     & $\alpha\times\beta \To \beta$         & & second projection\\
+  \cdx{split}   & $[\alpha\times\beta, [\alpha,\beta]\To\gamma] \To \gamma$
+        & & generalized projection\\
+  \cdx{Sigma}  &
$[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ &
-        general sum of sets
-\end{tabular}
-\end{center}
-\subcaption{Constants}
-
+        & general sum of sets
+\end{constants}
\begin{ttbox}\makeatletter
-\idx{fst_def}      fst(p)     == @a. ? b. p = <a,b>
-\idx{snd_def}      snd(p)     == @b. ? a. p = <a,b>
-\idx{split_def}    split(p,c) == c(fst(p),snd(p))
-\idx{Sigma_def}    Sigma(A,B) == UN x:A. UN y:B(x). \{<x,y>\}
-\subcaption{Definitions}
+\tdx{fst_def}      fst(p)     == @a. ? b. p = <a,b>
+\tdx{snd_def}      snd(p)     == @b. ? a. p = <a,b>
+\tdx{split_def}    split(p,c) == c(fst(p),snd(p))
+\tdx{Sigma_def}    Sigma(A,B) == UN x:A. UN y:B(x). \{<x,y>\}

-\idx{Pair_inject}  [| <a, b> = <a',b'>;  [| a=a';  b=b' |] ==> R |] ==> R

-\idx{fst}          fst(<a,b>) = a
-\idx{snd}          snd(<a,b>) = b
-\idx{split}        split(<a,b>, c) = c(a,b)
+\tdx{Pair_inject}  [| <a, b> = <a',b'>;  [| a=a';  b=b' |] ==> R |] ==> R
+\tdx{fst}          fst(<a,b>) = a
+\tdx{snd}          snd(<a,b>) = b
+\tdx{split}        split(<a,b>, c) = c(a,b)

-\idx{surjective_pairing}  p = <fst(p),snd(p)>
+\tdx{surjective_pairing}  p = <fst(p),snd(p)>

-\idx{SigmaI}       [| a:A;  b:B(a) |] ==> <a,b> : Sigma(A,B)
+\tdx{SigmaI}       [| a:A;  b:B(a) |] ==> <a,b> : Sigma(A,B)

-\idx{SigmaE}       [| c: Sigma(A,B);
+\tdx{SigmaE}       [| c: Sigma(A,B);
!!x y.[| x:A; y:B(x); c=<x,y> |] ==> P |] ==> P
-\subcaption{Derived rules}
\end{ttbox}
-\caption{Type $\alpha\times\beta$}
-\label{hol-prod}
+\caption{Type $\alpha\times\beta$}\label{hol-prod}
\end{figure}

\begin{figure}
-\begin{center}
-\begin{tabular}{rrr}
-  \it name      &\it meta-type  & \it description \\
-  \idx{Inl}     & $\alpha \To \alpha+\beta$                     & first injection\\
-  \idx{Inr}     & $\beta \To \alpha+\beta$                      & second injection\\
-  \idx{sum_case}    & $[\alpha+\beta, \alpha\To\gamma, \beta\To\gamma] \To\gamma$
-        & conditional
-\end{tabular}
-\end{center}
-\subcaption{Constants}
+\begin{constants}
+  \cdx{Inl}     & $\alpha \To \alpha+\beta$    & & first injection\\
+  \cdx{Inr}     & $\beta \To \alpha+\beta$     & & second injection\\
+  \cdx{sum_case} & $[\alpha+\beta, \alpha\To\gamma, \beta\To\gamma] \To\gamma$
+        & & conditional
+\end{constants}
+\begin{ttbox}\makeatletter
+\tdx{sum_case_def}   sum_case == (\%p f g. @z. (!x. p=Inl(x) --> z=f(x)) &
+                                        (!y. p=Inr(y) --> z=g(y)))

-\begin{ttbox}\makeatletter
-\idx{sum_case_def}     sum_case == (\%p f g. @z. (!x. p=Inl(x) --> z=f(x)) &
-                                          (!y. p=Inr(y) --> z=g(y)))
-\subcaption{Definition}
+\tdx{Inl_not_Inr}    ~ Inl(a)=Inr(b)

-\idx{Inl_not_Inr}    ~ Inl(a)=Inr(b)
+\tdx{inj_Inl}        inj(Inl)
+\tdx{inj_Inr}        inj(Inr)

-\idx{inj_Inl}        inj(Inl)
-\idx{inj_Inr}        inj(Inr)
-
-\idx{sumE}           [| !!x::'a. P(Inl(x));  !!y::'b. P(Inr(y)) |] ==> P(s)
+\tdx{sumE}           [| !!x::'a. P(Inl(x));  !!y::'b. P(Inr(y)) |] ==> P(s)

-\idx{sum_case_Inl}   sum_case(Inl(x), f, g) = f(x)
-\idx{sum_case_Inr}   sum_case(Inr(x), f, g) = g(x)
+\tdx{sum_case_Inl}   sum_case(Inl(x), f, g) = f(x)
+\tdx{sum_case_Inr}   sum_case(Inr(x), f, g) = g(x)

-\idx{surjective_sum} sum_case(s, %x::'a. f(Inl(x)), %y::'b. f(Inr(y))) = f(s)
-\subcaption{Derived rules}
+\tdx{surjective_sum} sum_case(s, \%x::'a. f(Inl(x)), \%y::'b. f(Inr(y))) = f(s)
\end{ttbox}
-\caption{Rules for type $\alpha+\beta$}
-\label{hol-sum}
+\caption{Type $\alpha+\beta$}\label{hol-sum}
\end{figure}

\section{Types}
The basic higher-order logic is augmented with a tremendous amount of
-material, including support for recursive function and type definitions.
-Space does not permit a detailed discussion.  The present section describes
-product, sum, natural number and list types.
+material, including support for recursive function and type definitions.  A
+detailed discussion appears elsewhere~\cite{paulson-coind}.  The simpler
+definitions are the same as those used the {\sc hol} system, but my
+treatment of recursive types differs from Melham's~\cite{melham89}.  The
+present section describes product, sum, natural number and list types.

-\subsection{Product and sum types}
-\HOL\ defines the product type $\alpha\times\beta$ and the sum type
-$\alpha+\beta$, with the ordered pair syntax {\tt<$a$,$b$>}, using fairly
-standard constructions (Figs.~\ref{hol-prod} and~\ref{hol-sum}).  Because
-Isabelle does not support abstract type definitions, the isomorphisms
-between these types and their representations are made explicitly.
+\subsection{Product and sum types}\index{*"* type}\index{*"+ type}
+Theory \thydx{Prod} defines the product type $\alpha\times\beta$, with
+the ordered pair syntax {\tt<$a$,$b$>}.  Theory \thydx{Sum} defines the
+sum type $\alpha+\beta$.  These use fairly standard constructions; see
+Figs.\ts\ref{hol-prod} and~\ref{hol-sum}.  Because Isabelle does not
+support abstract type definitions, the isomorphisms between these types and

Most of the definitions are suppressed, but observe that the projections
and conditionals are defined as descriptions.  Their properties are easily
-proved using \ttindex{select_equality}.  See {\tt HOL/prod.thy} and
+proved using \tdx{select_equality}.  See {\tt HOL/prod.thy} and
{\tt HOL/sum.thy} for details.

\begin{figure}
-\indexbold{*"<}
-\begin{center}
-\begin{tabular}{rrr}
-  \it symbol    & \it meta-type & \it description \\
-  \idx{0}       & $nat$         & zero \\
-  \idx{Suc}     & $nat \To nat$ & successor function\\
-  \idx{nat_case} & $[nat, \alpha, nat\To\alpha] \To\alpha$
-        & conditional\\
-  \idx{nat_rec} & $[nat, \alpha, [nat, \alpha]\To\alpha] \To \alpha$
-        & primitive recursor\\
-  \idx{pred_nat} & $(nat\times nat) set$ & predecessor relation
-\end{tabular}
-\end{center}
-
-\begin{center}
-\indexbold{*"+}
-\index{*@{\tt*}|bold}
-\index{/@{\tt/}|bold}
-\index{//@{\tt//}|bold}
-\index{+@{\tt+}|bold}
-\index{-@{\tt-}|bold}
-\begin{tabular}{rrrr}
-  \it symbol    & \it meta-type & \it precedence & \it description \\
+\index{*"< symbol}
+\index{*"* symbol}
+\index{/@{\tt/} symbol}
+\index{//@{\tt//} symbol}
+\index{*"+ symbol}
+\index{*"- symbol}
+\begin{constants}
+  \it symbol    & \it meta-type & \it priority & \it description \\
+  \cdx{0}       & $nat$         & & zero \\
+  \cdx{Suc}     & $nat \To nat$ & & successor function\\
+  \cdx{nat_case} & $[nat, \alpha, nat\To\alpha] \To\alpha$
+        & & conditional\\
+  \cdx{nat_rec} & $[nat, \alpha, [nat, \alpha]\To\alpha] \To \alpha$
+        & & primitive recursor\\
+  \cdx{pred_nat} & $(nat\times nat) set$ & & predecessor relation\\
\tt *         & $[nat,nat]\To nat$    &  Left 70      & multiplication \\
\tt /         & $[nat,nat]\To nat$    &  Left 70      & division\\
\tt //        & $[nat,nat]\To nat$    &  Left 70      & modulus\\
\tt +         & $[nat,nat]\To nat$    &  Left 65      & addition\\
\tt -         & $[nat,nat]\To nat$    &  Left 65      & subtraction
-\end{tabular}
-\end{center}
+\end{constants}
\subcaption{Constants and infixes}

\begin{ttbox}\makeatother
-\idx{nat_case_def}  nat_case == (\%n a f. @z. (n=0 --> z=a) &
+\tdx{nat_case_def}  nat_case == (\%n a f. @z. (n=0 --> z=a) &
(!x. n=Suc(x) --> z=f(x)))
-\idx{pred_nat_def}  pred_nat == \{p. ? n. p = <n, Suc(n)>\}
-\idx{less_def}      m<n      == <m,n>:pred_nat^+
-\idx{nat_rec_def}   nat_rec(n,c,d) ==
+\tdx{pred_nat_def}  pred_nat == \{p. ? n. p = <n, Suc(n)>\}
+\tdx{less_def}      m<n      == <m,n>:pred_nat^+
+\tdx{nat_rec_def}   nat_rec(n,c,d) ==
wfrec(pred_nat, n, \%l g.nat_case(l, c, \%m.d(m,g(m))))

-\idx{add_def}   m+n  == nat_rec(m, n, \%u v.Suc(v))
-\idx{diff_def}  m-n  == nat_rec(n, m, \%u v. nat_rec(v, 0, \%x y.x))
-\idx{mult_def}  m*n  == nat_rec(m, 0, \%u v. n + v)
-\idx{mod_def}   m//n == wfrec(trancl(pred_nat), m, \%j f. if(j<n,j,f(j-n)))
-\idx{quo_def}   m/n  == wfrec(trancl(pred_nat),
+\tdx{add_def}   m+n  == nat_rec(m, n, \%u v.Suc(v))
+\tdx{diff_def}  m-n  == nat_rec(n, m, \%u v. nat_rec(v, 0, \%x y.x))
+\tdx{mult_def}  m*n  == nat_rec(m, 0, \%u v. n + v)
+\tdx{mod_def}   m//n == wfrec(trancl(pred_nat), m, \%j f. if(j<n,j,f(j-n)))
+\tdx{quo_def}   m/n  == wfrec(trancl(pred_nat),
m, \%j f. if(j<n,0,Suc(f(j-n))))
\subcaption{Definitions}
\end{ttbox}
-\caption{Defining $nat$, the type of natural numbers} \label{hol-nat1}
+\caption{Defining {\tt nat}, the type of natural numbers} \label{hol-nat1}
\end{figure}

\begin{figure} \underscoreon
\begin{ttbox}
-\idx{nat_induct}     [| P(0); !!k. [| P(k) |] ==> P(Suc(k)) |]  ==> P(n)
+\tdx{nat_induct}     [| P(0); !!k. [| P(k) |] ==> P(Suc(k)) |]  ==> P(n)

-\idx{Suc_not_Zero}   Suc(m) ~= 0
-\idx{inj_Suc}        inj(Suc)
-\idx{n_not_Suc_n}    n~=Suc(n)
+\tdx{Suc_not_Zero}   Suc(m) ~= 0
+\tdx{inj_Suc}        inj(Suc)
+\tdx{n_not_Suc_n}    n~=Suc(n)
\subcaption{Basic properties}

-\idx{pred_natI}      <n, Suc(n)> : pred_nat
-\idx{pred_natE}
+\tdx{pred_natI}      <n, Suc(n)> : pred_nat
+\tdx{pred_natE}
[| p : pred_nat;  !!x n. [| p = <n, Suc(n)> |] ==> R |] ==> R

-\idx{nat_case_0}     nat_case(0, a, f) = a
-\idx{nat_case_Suc}   nat_case(Suc(k), a, f) = f(k)
+\tdx{nat_case_0}     nat_case(0, a, f) = a
+\tdx{nat_case_Suc}   nat_case(Suc(k), a, f) = f(k)

-\idx{wf_pred_nat}    wf(pred_nat)
-\idx{nat_rec_0}      nat_rec(0,c,h) = c
-\idx{nat_rec_Suc}    nat_rec(Suc(n), c, h) = h(n, nat_rec(n,c,h))
+\tdx{wf_pred_nat}    wf(pred_nat)
+\tdx{nat_rec_0}      nat_rec(0,c,h) = c
+\tdx{nat_rec_Suc}    nat_rec(Suc(n), c, h) = h(n, nat_rec(n,c,h))
\subcaption{Case analysis and primitive recursion}

-\idx{less_trans}     [| i<j;  j<k |] ==> i<k
-\idx{lessI}          n < Suc(n)
-\idx{zero_less_Suc}  0 < Suc(n)
+\tdx{less_trans}     [| i<j;  j<k |] ==> i<k
+\tdx{lessI}          n < Suc(n)
+\tdx{zero_less_Suc}  0 < Suc(n)

-\idx{less_not_sym}   n<m --> ~ m<n
-\idx{less_not_refl}  ~ n<n
-\idx{not_less0}      ~ n<0
+\tdx{less_not_sym}   n<m --> ~ m<n
+\tdx{less_not_refl}  ~ n<n
+\tdx{not_less0}      ~ n<0

-\idx{Suc_less_eq}    (Suc(m) < Suc(n)) = (m<n)
-\idx{less_induct}    [| !!n. [| ! m. m<n --> P(m) |] ==> P(n) |]  ==>  P(n)
+\tdx{Suc_less_eq}    (Suc(m) < Suc(n)) = (m<n)
+\tdx{less_induct}    [| !!n. [| ! m. m<n --> P(m) |] ==> P(n) |]  ==>  P(n)

-\idx{less_linear}    m<n | m=n | n<m
+\tdx{less_linear}    m<n | m=n | n<m
\subcaption{The less-than relation}
\end{ttbox}
\caption{Derived rules for~$nat$} \label{hol-nat2}
\end{figure}

-\subsection{The type of natural numbers, $nat$}
-The axiom of infinity postulates an type~$ind$ of individuals, which is
-non-empty and closed under an injective operation.  The natural numbers are
-inductively generated by choosing an arbitrary individual for~0 and using
-the injective operation to take successors.  As usual, the isomorphisms
-between~$nat$ and its representation are made explicitly.
+\subsection{The type of natural numbers, {\tt nat}}
+The theory \thydx{Nat} defines the natural numbers in a roundabout but
+traditional way.  The axiom of infinity postulates an type~\tydx{ind} of
+individuals, which is non-empty and closed under an injective operation.
+The natural numbers are inductively generated by choosing an arbitrary
+individual for~0 and using the injective operation to take successors.  As
+usual, the isomorphisms between~$nat$ and its representation are made
+explicitly.

-The definition makes use of a least fixed point operator \ttindex{lfp},
-defined using the Knaster-Tarski theorem.  This in turn defines an operator
-\ttindex{trancl} for taking the transitive closure of a relation.  See
-files {\tt HOL/lfp.thy} and {\tt HOL/trancl.thy} for
-details.  The definition of~$nat$ resides on {\tt HOL/nat.thy}.
+The definition makes use of a least fixed point operator \cdx{lfp},
+defined using the Knaster-Tarski theorem.  This is used to define the
+operator \cdx{trancl}, for taking the transitive closure of a relation.
+Primitive recursion makes use of \cdx{wfrec}, an operator for recursion
+along arbitrary well-founded relations.  The corresponding theories are
+called {\tt Lfp}, {\tt Trancl} and {\tt WF}\@.  Elsewhere I have described
+similar constructions in the context of set theory~\cite{paulson-set-II}.

-Type $nat$ is postulated to belong to class~$ord$, which overloads $<$ and
-$\leq$ on the natural numbers.  As of this writing, Isabelle provides no
-means of verifying that such overloading is sensible.  On the other hand,
-the \HOL\ theory includes no polymorphic axioms stating general properties
-of $<$ and $\leq$.
+Type~\tydx{nat} is postulated to belong to class~\cldx{ord}, which
+overloads $<$ and $\leq$ on the natural numbers.  As of this writing,
+there is no means of specifying the operators' properties and verifying
+that instances of the operators satisfy those properties.  To be safe, the
+\HOL\ theory includes no polymorphic axioms asserting general properties of
+$<$ and~$\leq$.

-File {\tt HOL/arith.ML} develops arithmetic on the natural numbers.
-It defines addition, multiplication, subtraction, division, and remainder,
-proving the theorem $a \bmod b + (a/b)\times b = a$.  Division and
-remainder are defined by repeated subtraction, which requires well-founded
-rather than primitive recursion.
+Theory \thydx{Arith} develops arithmetic on the natural numbers.  It
+defines addition, multiplication, subtraction, division, and remainder.
+Many of their properties are proved: commutative, associative and
+distributive laws, identity and cancellation laws, etc.  The most
+interesting result is perhaps the theorem $a \bmod b + (a/b)\times b = a$.
+Division and remainder are defined by repeated subtraction, which requires
+well-founded rather than primitive recursion.  See Figs.\ts\ref{hol-nat1}
+and~\ref{hol-nat2}.

-Primitive recursion makes use of \ttindex{wfrec}, an operator for recursion
-along arbitrary well-founded relations; see {\tt HOL/wf.ML} for the
-development.  The predecessor relation, \ttindexbold{pred_nat}, is shown to
-be well-founded; recursion along this relation is primitive recursion,
-while its transitive closure is~$<$.
+The predecessor relation, \cdx{pred_nat}, is shown to be well-founded.
+Recursion along this relation resembles primitive recursion, but is
+stronger because we are in higher-order logic; using primitive recursion to
+define a higher-order function, we can easily Ackermann's function, which
+is not primitive recursive \cite[page~104]{thompson91}.
+The transitive closure of \cdx{pred_nat} is~$<$.  Many functions on the
+natural numbers are most easily expressed using recursion along~$<$.
+
+The tactic {\tt\ttindex{nat_ind_tac} "$n$" $i$} performs induction over the
+variable~$n$ in subgoal~$i$.

\begin{figure}
-\begin{center}
-\begin{tabular}{rrr}
-  \it symbol    & \it meta-type & \it description \\
-  \idx{Nil}     & $\alpha list$ & empty list\\
-  \idx{null}    & $\alpha list \To bool$ & emptyness test\\
-  \idx{hd}      & $\alpha list \To \alpha$ & head \\
-  \idx{tl}      & $\alpha list \To \alpha list$ & tail \\
-  \idx{ttl}     & $\alpha list \To \alpha list$ & total tail \\
-  \idx{map}     & $(\alpha\To\beta) \To (\alpha list \To \beta list)$
-        & mapping functional\\
-  \idx{list_all}& $(\alpha \To bool) \To (\alpha list \To bool)$
-        & forall functional\\
-  \idx{filter}  & $(\alpha \To bool) \To (\alpha list \To \alpha list)$
-        & filter functional\\
-  \idx{list_rec}        & $[\alpha list, \beta, [\alpha ,\alpha list, +\index{#@{\tt\#} symbol} +\index{"@@{\tt\at} symbol} +\begin{constants} + \it symbol & \it meta-type & \it priority & \it description \\ + \cdx{Nil} &$\alpha list$& & empty list\\ + \tt \# &$[\alpha,\alpha list]\To \alpha list$& Right 65 & + list constructor \\ + \cdx{null} &$\alpha list \To bool$& & emptyness test\\ + \cdx{hd} &$\alpha list \To \alpha$& & head \\ + \cdx{tl} &$\alpha list \To \alpha list$& & tail \\ + \cdx{ttl} &$\alpha list \To \alpha list$& & total tail \\ + \tt\at &$[\alpha list,\alpha list]\To \alpha list$& Left 65 & append \\ + \sdx{mem} &$[\alpha,\alpha list]\To bool$& Left 55 & membership\\ + \cdx{map} &$(\alpha\To\beta) \To (\alpha list \To \beta list)$+ & & mapping functional\\ + \cdx{filter} &$(\alpha \To bool) \To (\alpha list \To \alpha list)$+ & & filter functional\\ + \cdx{list_all}&$(\alpha \To bool) \To (\alpha list \To bool)$+ & & forall functional\\ + \cdx{list_rec} &$[\alpha list, \beta, [\alpha ,\alpha list,
\beta]\To\beta] \To \beta$- & list recursor -\end{tabular} -\end{center} - -\begin{center} -\index{"# @{\tt\#}|bold} -\index{"@@{\tt\at}|bold} -\begin{tabular}{rrrr} - \it symbol & \it meta-type & \it precedence & \it description \\ - \tt \# &$[\alpha,\alpha list]\To \alpha list$& Right 65 & cons \\ - \tt\at &$[\alpha list,\alpha list]\To \alpha list$& Left 65 & append \\ - \idx{mem} &$[\alpha,\alpha list]\To bool$& Left 55 & membership -\end{tabular} -\end{center} + & & list recursor +\end{constants} \subcaption{Constants and infixes} \begin{center} \tt\frenchspacing \begin{tabular}{rrr} - \it external & \it internal & \it description \\{} - \idx{[]} & Nil & empty list \\{} - [$x@1$,$\dots$,$x@n$] &$x@1$\#$\cdots$\#$x@n$\#[] & + \it external & \it internal & \it description \\{} + \sdx{[]} & Nil & \rm empty list \\{} + [$x@1$,$\dots$,$x@n$] &$x@1$\#$\cdots$\#$x@n$\# [] & \rm finite list \\{} - [$x$:$xs$.$P$] & filter(\%$x$.$P$,$xs$) & list comprehension\\ - \begin{tabular}{r@{}l} - \idx{case}$e$of&\ [] =>$a$\\ - |&\$x$\#$xs$=>$b$- \end{tabular} & list_case($e$,$a$,\%$x~xs$.$b$) - & case analysis + [$x$:$l$.$P[x]$] & filter($\lambda x.P[x]$,$l$) & + \rm list comprehension \end{tabular} \end{center} \subcaption{Translations} \begin{ttbox} -\idx{list_induct} [| P([]); !!x xs. [| P(xs) |] ==> P(x#xs)) |] ==> P(l) +\tdx{list_induct} [| P([]); !!x xs. [| P(xs) |] ==> P(x#xs)) |] ==> P(l) -\idx{Cons_not_Nil} (x # xs) ~= [] -\idx{Cons_Cons_eq} ((x # xs) = (y # ys)) = (x=y & xs=ys) +\tdx{Cons_not_Nil} (x # xs) ~= [] +\tdx{Cons_Cons_eq} ((x # xs) = (y # ys)) = (x=y & xs=ys) \subcaption{Induction and freeness} \end{ttbox} -\caption{The type of lists and its operations} \label{hol-list} +\caption{The theory \thydx{List}} \label{hol-list} \end{figure} \begin{figure} \begin{ttbox}\makeatother -list_rec([],c,h) = c list_rec(a \# l, c, h) = h(a, l, list_rec(l,c,h)) -list_case([],c,h) = c list_case(x # xs, c, h) = h(x, xs) -map(f,[]) = [] map(f, x \# xs) = f(x) \# map(f,xs) -null([]) = True null(x # xs) = False -hd(x # xs) = x tl(x # xs) = xs -ttl([]) = [] ttl(x # xs) = xs -[] @ ys = ys (x # xs) \at ys = x # xs \at ys -x mem [] = False x mem y # ys = if(y = x, True, x mem ys) -filter(P, []) = [] filter(P,x#xs) = if(P(x),x#filter(P,xs),filter(P,xs)) -list_all(P,[]) = True list_all(P, x # xs) = (P(x) & list_all(P, xs)) +\tdx{list_rec_Nil} list_rec([],c,h) = c +\tdx{list_rec_Cons} list_rec(a \# l, c, h) = h(a, l, list_rec(l,c,h)) + +\tdx{list_case_Nil} list_case([],c,h) = c +\tdx{list_case_Cons} list_case(x # xs, c, h) = h(x, xs) + +\tdx{map_Nil} map(f,[]) = [] +\tdx{map_Cons} map(f, x \# xs) = f(x) \# map(f,xs) + +\tdx{null_Nil} null([]) = True +\tdx{null_Cons} null(x # xs) = False + +\tdx{hd_Cons} hd(x # xs) = x +\tdx{tl_Cons} tl(x # xs) = xs + +\tdx{ttl_Nil} ttl([]) = [] +\tdx{ttl_Cons} ttl(x # xs) = xs + +\tdx{append_Nil} [] @ ys = ys +\tdx{append_Cons} (x # xs) \at ys = x # xs \at ys + +\tdx{mem_Nil} x mem [] = False +\tdx{mem_Cons} x mem y # ys = if(y = x, True, x mem ys) + +\tdx{filter_Nil} filter(P, []) = [] +\tdx{filter_Cons} filter(P,x#xs) = if(P(x),x#filter(P,xs),filter(P,xs)) + +\tdx{list_all_Nil} list_all(P,[]) = True +\tdx{list_all_Cons} list_all(P, x # xs) = (P(x) & list_all(P, xs)) \end{ttbox} \caption{Rewrite rules for lists} \label{hol-list-simps} \end{figure} -\subsection{The type constructor for lists,$\alpha\,list$} + +\subsection{The type constructor for lists, {\tt list}} +\index{*list type} + \HOL's definition of lists is an example of an experimental method for -handling recursive data types. The details need not concern us here; see the -file {\tt HOL/list.ML}. Figure~\ref{hol-list} presents the basic list -operations, with their types and properties. In particular, -\ttindexbold{list_rec} is a primitive recursion operator for lists, in the -style of Martin-L\"of type theory. It is derived from well-founded -recursion, a general principle that can express arbitrary total recursive -functions. The basic rewrite rules shown in Fig.~\ref{hol-list-simps} are -contained, together with additional useful lemmas, in the simpset {\tt - list_ss}. Induction over the variable$xs$in subgoal$i$is performed by -{\tt list_ind_tac "$xs$"$i$}. +handling recursive data types. Figure~\ref{hol-list} presents the theory +\thydx{List}: the basic list operations with their types and properties. + +The \sdx{case} construct is defined by the following translation +(omitted from the figure due to lack of space): +{\dquotes +\begin{eqnarray*} + \begin{array}[t]{r@{\;}l@{}l} + "case " e " of" & "[]" & " => " a\\ + "|" & x"\#"xs & " => " b + \end{array} + & \equiv & + "list_case"(e, a, \lambda x\;xs.b[x,xs]) +\end{eqnarray*}} +The theory includes \cdx{list_rec}, a primitive recursion operator +for lists. It is derived from well-founded recursion, a general principle +that can express arbitrary total recursive functions. + +The simpset \ttindex{list_ss} contains, along with additional useful lemmas, +the basic rewrite rules that appear in Fig.\ts\ref{hol-list-simps}. + +The tactic {\tt\ttindex{list_ind_tac} "$xs$"$i$} performs induction over the +variable~$xs$in subgoal~$i$. -\subsection{The type constructor for lazy lists,$\alpha\,llist$} +\subsection{The type constructor for lazy lists, {\tt llist}} +\index{*llist type} + The definition of lazy lists demonstrates methods for handling infinite -data structures and co-induction in higher-order logic. It defines an -operator for co-recursion on lazy lists, which is used to define a few -simple functions such as map and append. Co-recursion cannot easily define +data structures and coinduction in higher-order logic. It defines an +operator for corecursion on lazy lists, which is used to define a few +simple functions such as map and append. Corecursion cannot easily define operations such as filter, which can compute indefinitely before yielding -the next element (if any!) of the lazy list. A co-induction principle is -defined for proving equations on lazy lists. See the files -{\tt HOL/llist.thy} and {\tt HOL/llist.ML} for the formal -derivations. I have written a report discussing the treatment of lazy -lists, and finite lists also~\cite{paulson-coind}. +the next element (if any!) of the lazy list. A coinduction principle is +defined for proving equations on lazy lists. See the files {\tt + HOL/llist.thy} and {\tt HOL/llist.ML} for the formal derivations. + +I have written a paper discussing the treatment of lazy lists; it also +covers finite lists~\cite{paulson-coind}. \section{Classical proof procedures} \label{hol-cla-prover} \HOL\ derives classical introduction rules for$\disj$and~$\exists$, as well as classical elimination rules for~$\imp$and~$\bimp$, and the swap -rule (Fig.~\ref{hol-lemmas2}). +rule; recall Fig.\ts\ref{hol-lemmas2} above. -The classical reasoning module is set up for \HOL, as the structure -\ttindexbold{Classical}. This structure is open, so {\ML} identifiers such +The classical reasoner is set up for \HOL, as the structure +{\tt Classical}. This structure is open, so {\ML} identifiers such as {\tt step_tac}, {\tt fast_tac}, {\tt best_tac}, etc., refer to it. \HOL\ defines the following classical rule sets: @@ -1188,80 +1214,84 @@ HOL_dup_cs : claset set_cs : claset \end{ttbox} -\begin{description} +\begin{ttdescription} \item[\ttindexbold{prop_cs}] contains the propositional rules, namely those for~$\top$,$\bot$,$\conj$,$\disj$,$\neg$,$\imp$and~$\bimp$, -along with the rule~\ttindex{refl}. +along with the rule~{\tt refl}. -\item[\ttindexbold{HOL_cs}] -extends {\tt prop_cs} with the safe rules \ttindex{allI} and~\ttindex{exE} -and the unsafe rules \ttindex{allE} and~\ttindex{exI}, as well as rules for -unique existence. Search using this is incomplete since quantified -formulae are used at most once. +\item[\ttindexbold{HOL_cs}] extends {\tt prop_cs} with the safe rules + {\tt allI} and~{\tt exE} and the unsafe rules {\tt allE} + and~{\tt exI}, as well as rules for unique existence. Search using + this classical set is incomplete: quantified formulae are used at most + once. -\item[\ttindexbold{HOL_dup_cs}] -extends {\tt prop_cs} with the safe rules \ttindex{allI} and~\ttindex{exE} -and the unsafe rules \ttindex{all_dupE} and~\ttindex{exCI}, as well as -rules for unique existence. Search using this is complete --- quantified -formulae may be duplicated --- but frequently fails to terminate. It is -generally unsuitable for depth-first search. +\item[\ttindexbold{HOL_dup_cs}] extends {\tt prop_cs} with the safe rules + {\tt allI} and~{\tt exE} and the unsafe rules \tdx{all_dupE} + and~\tdx{exCI}, as well as rules for unique existence. Search using + this is complete --- quantified formulae may be duplicated --- but + frequently fails to terminate. It is generally unsuitable for + depth-first search. -\item[\ttindexbold{set_cs}] -extends {\tt HOL_cs} with rules for the bounded quantifiers, subsets, -comprehensions, unions/intersections, complements, finite setes, images and -ranges. -\end{description} +\item[\ttindexbold{set_cs}] extends {\tt HOL_cs} with rules for the bounded + quantifiers, subsets, comprehensions, unions and intersections, + complements, finite sets, images and ranges. +\end{ttdescription} \noindent -See the {\em Reference Manual} for more discussion of classical proof -methods. +See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% + {Chap.\ts\ref{chap:classical}} +for more discussion of classical proof methods. \section{The examples directories} -Directory {\tt Subst} contains Martin Coen's mechanization of a theory of +Directory {\tt HOL/Subst} contains Martin Coen's mechanization of a theory of substitutions and unifiers. It is based on Paulson's previous mechanization in {\LCF}~\cite{paulson85} of Manna and Waldinger's theory~\cite{mw81}. -Directory {\tt ex} contains other examples and experimental proofs in -\HOL. Here is an overview of the more interesting files. -\begin{description} -\item[{\tt HOL/ex/meson.ML}] -contains an experimental implementation of the MESON proof procedure, -inspired by Plaisted~\cite{plaisted90}. It is much more powerful than -Isabelle's classical module. +Directory {\tt HOL/ex} contains other examples and experimental proofs in +{\HOL}. Here is an overview of the more interesting files. +\begin{ttdescription} +\item[HOL/ex/meson.ML] contains an experimental implementation of the {\sc + meson} proof procedure, inspired by Plaisted~\cite{plaisted90}. It is + much more powerful than Isabelle's classical reasoner. But it is less + useful in practice because it works only for pure logic; it does not + accept derived rules for the set theory primitives, for example. -\item[{\tt HOL/ex/mesontest.ML}] -contains test data for the MESON proof procedure. +\item[HOL/ex/mesontest.ML] contains test data for the {\sc meson} proof + procedure. These are mostly taken from Pelletier \cite{pelletier86}. -\item[{\tt HOL/ex/set.ML}] - proves Cantor's Theorem, which is presented below, and the - Schr\"oder-Bernstein Theorem. +\item[HOL/ex/set.ML] proves Cantor's Theorem, which is presented in + \S\ref{sec:hol-cantor} below, and the Schr\"oder-Bernstein Theorem. + +\item[HOL/ex/insort.ML] and {\tt HOL/ex/qsort.ML} contain correctness + proofs about insertion sort and quick sort. -\item[{\tt HOL/ex/pl.ML}] -proves the soundness and completeness of classical propositional logic, -given a truth table semantics. The only connective is$\imp$. A -Hilbert-style axiom system is specified, and its set of theorems defined -inductively. +\item[HOL/ex/pl.ML] proves the soundness and completeness of classical + propositional logic, given a truth table semantics. The only connective + is$\imp$. A Hilbert-style axiom system is specified, and its set of + theorems defined inductively. -\item[{\tt HOL/ex/term.ML}] +\item[HOL/ex/term.ML] contains proofs about an experimental recursive type definition; - the recursion goes through the type constructor~$list$. + the recursion goes through the type constructor~\tydx{list}. -\item[{\tt HOL/ex/simult.ML}] -defines primitives for solving mutually recursive equations over sets. -It constructs sets of trees and forests as an example, including induction -and recursion rules that handle the mutual recursion. +\item[HOL/ex/simult.ML] defines primitives for solving mutually recursive + equations over sets. It constructs sets of trees and forests as an + example, including induction and recursion rules that handle the mutual + recursion. -\item[{\tt HOL/ex/mt.ML}] -contains Jacob Frost's formalization~\cite{frost93} of a co-induction -example by Milner and Tofte~\cite{milner-coind}. -\end{description} +\item[HOL/ex/mt.ML] contains Jacob Frost's formalization~\cite{frost93} of + Milner and Tofte's coinduction example~\cite{milner-coind}. This + substantial proof concerns the soundness of a type system for a simple + functional language. The semantics of recursion is given by a cyclic + environment, which makes a coinductive argument appropriate. +\end{ttdescription} \section{Example: deriving the conjunction rules} -\HOL\ comes with a body of derived rules, ranging from simple properties -of the logical constants and set theory to well-founded recursion. Many of -them are worth studying. +The theory {\HOL} comes with a body of derived rules, ranging from simple +properties of the logical constants and set theory to well-founded +recursion. Many of them are worth studying. Deriving natural deduction rules for the logical constants from their definitions is an archetypal example of higher-order reasoning. Let us @@ -1281,9 +1311,9 @@ {\out val prems = ["P [P]", "Q [Q]"] : thm list} \end{ttbox} The next step is to unfold the definition of conjunction. But -\ttindex{and_def} uses \HOL's internal equality, so +\tdx{and_def} uses \HOL's internal equality, so \ttindex{rewrite_goals_tac} is unsuitable. -Instead, we perform substitution using the rule \ttindex{ssubst}: +Instead, we perform substitution using the rule \tdx{ssubst}: \begin{ttbox} by (resolve_tac [and_def RS ssubst] 1); {\out Level 1} @@ -1303,8 +1333,8 @@ {\out 1. !!R. P --> Q --> R ==> R} \end{ttbox} The assumption is a nested implication, which may be eliminated -using~\ttindex{mp} resolved with itself. Elim-resolution, here, performs -backwards chaining. More straightforward would be to use~\ttindex{impE} +using~\tdx{mp} resolved with itself. Elim-resolution, here, performs +backwards chaining. More straightforward would be to use~\tdx{impE} twice. \index{*RS} \begin{ttbox} @@ -1335,7 +1365,7 @@ \end{ttbox} Working with premises that involve defined constants can be tricky. We must expand the definition of conjunction in the meta-assumption$P\conj
-Q$. The rule \ttindex{subst} performs substitution in forward proofs. +Q$.  The rule \tdx{subst} performs substitution in forward proofs.
We get {\it two\/} resolvents since the vacuous substitution is valid:
\begin{ttbox}
prems RL [and_def RS subst];
@@ -1363,7 +1393,7 @@
{\out  1. P --> Q --> P}
\end{ttbox}
The subgoal is a trivial implication.  Recall that \ttindex{ares_tac} is a
-combination of \ttindex{assume_tac} and \ttindex{resolve_tac}.
+combination of {\tt assume_tac} and {\tt resolve_tac}.
\begin{ttbox}
by (REPEAT (ares_tac [impI] 1));
{\out Level 2}
@@ -1372,27 +1402,28 @@
\end{ttbox}

-\section{Example: Cantor's Theorem}
+\section{Example: Cantor's Theorem}\label{sec:hol-cantor}
Cantor's Theorem states that every set has more subsets than it has
elements.  It has become a favourite example in higher-order logic since
it is so easily expressed:
$\forall f::[\alpha,\alpha]\To bool. \exists S::\alpha\To bool. \forall x::\alpha. f(x) \not= S$
+%
Viewing types as sets, $\alpha\To bool$ represents the powerset
of~$\alpha$.  This version states that for every function from $\alpha$ to
-its powerset, some subset is outside its range.
-The Isabelle proof uses \HOL's set theory, with the type $\alpha\,set$ and
-the operator \ttindex{range}.  Since it avoids quantification, we may
-inspect the subset found by the proof.
+its powerset, some subset is outside its range.  The Isabelle proof uses
+\HOL's set theory, with the type $\alpha\,set$ and the operator
+\cdx{range}.  The set~$S$ is given as an unknown instead of a
+quantified variable so that we may inspect the subset found by the proof.
\begin{ttbox}
goal Set.thy "~ ?S : range(f :: 'a=>'a set)";
{\out Level 0}
{\out ~ ?S : range(f)}
{\out  1. ~ ?S : range(f)}
\end{ttbox}
-The first two steps are routine.  The rule \ttindex{rangeE} reasons that,
-since $\Var{S}\in range(f)$, we have $\Var{S}=f(x)$ for some~$x$.
+The first two steps are routine.  The rule \tdx{rangeE} replaces
+$\Var{S}\in {\tt range}(f)$ by $\Var{S}=f(x)$ for some~$x$.
\begin{ttbox}
by (resolve_tac [notI] 1);
{\out Level 1}
@@ -1404,7 +1435,7 @@
{\out ~ ?S : range(f)}
{\out  1. !!x. ?S = f(x) ==> False}
\end{ttbox}
-Next, we apply \ttindex{equalityCE}, reasoning that since $\Var{S}=f(x)$,
+Next, we apply \tdx{equalityCE}, reasoning that since $\Var{S}=f(x)$,
we have $\Var{c}\in \Var{S}$ if and only if $\Var{c}\in f(x)$ for
any~$\Var{c}$.
\begin{ttbox}
@@ -1414,9 +1445,10 @@
{\out  1. !!x. [| ?c3(x) : ?S; ?c3(x) : f(x) |] ==> False}
{\out  2. !!x. [| ~ ?c3(x) : ?S; ~ ?c3(x) : f(x) |] ==> False}
\end{ttbox}
-Now we use a bit of creativity.  Suppose that $\Var{S}$ has the form of a
+Now we use a bit of creativity.  Suppose that~$\Var{S}$ has the form of a
comprehension.  Then $\Var{c}\in\{x.\Var{P}(x)\}$ implies
-$\Var{P}(\Var{c})\}$.\index{*CollectD}
+$\Var{P}(\Var{c})$.   Destruct-resolution using \tdx{CollectD}
+instantiates~$\Var{S}$ and creates the new assumption.
\begin{ttbox}
by (dresolve_tac [CollectD] 1);
{\out Level 4}
@@ -1433,7 +1465,7 @@
{\out ~ \{x. ~ x : f(x)\} : range(f)}
{\out  1. !!x. [| ~ x : \{x. ~ x : f(x)\}; ~ x : f(x) |] ==> False}
\end{ttbox}
-The rest should be easy.  To apply \ttindex{CollectI} to the negated
+The rest should be easy.  To apply \tdx{CollectI} to the negated
assumption, we employ \ttindex{swap_res_tac}:
\begin{ttbox}
by (swap_res_tac [CollectI] 1);
@@ -1448,10 +1480,11 @@
\end{ttbox}
How much creativity is required?  As it happens, Isabelle can prove this
theorem automatically.  The classical set \ttindex{set_cs} contains rules
-for most of the constructs of \HOL's set theory.  We augment it with
-\ttindex{equalityCE} --- set equalities are not broken up by default ---
-and apply best-first search.  Depth-first search would diverge, but
-best-first search successfully navigates through the large search space.
+for most of the constructs of \HOL's set theory.  We must augment it with
+\tdx{equalityCE} to break up set equalities, and then apply best-first
+search.  Depth-first search would diverge, but best-first search
+successfully navigates through the large search space.
+\index{search!best-first}
\begin{ttbox}
choplev 0;
{\out Level 0}
@@ -1463,3 +1496,5 @@
{\out ~ \{x. ~ x : f(x)\} : range(f)}
{\out No subgoals!}
\end{ttbox}
+
+\index{higher-order logic|)}