--- 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
overloading of the operators {\tt+}, {\tt-} and {\tt*}. In particular,
{\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
+their~{\ML} names. Some of the rules deserve additional comments:
+\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} f``A == \{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} f``A == \{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) : f``A
-\idx{imageE} [| b : f``A; !!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) : f``A
+\tdx{imageE} [| b : f``A; !!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
-
-\idx{inj_onto_contraD}
+\tdx{inj_onto_contraD}
[| 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(A``C) Un Union(B``C)
+\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(A``C) Un Union(B``C)
-\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(A``C) Int Inter(B``C)
+\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(A``C) Int Inter(B``C)
\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
+their representations are made explicitly.
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$}
-\HOL\ defines the natural numbers in a roundabout but traditional way.
-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,
+Isabelle provides no means of verifying that such overloading is sensible;
+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|)}