# HG changeset patch # User lcp # Date 766407742 -7200 # Node ID ebf62069d88950029a570d99de1071416389c8c9 # Parent d1ef723e943deeb006f731efeccfa9d75b5f9a47 penultimate Springer draft diff -r d1ef723e943d -r ebf62069d889 doc-src/Logics/Old_HOL.tex --- 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 = -\idx{snd_def} snd(p) == @b. ? a. p = -\idx{split_def} split(p,c) == c(fst(p),snd(p)) -\idx{Sigma_def} Sigma(A,B) == UN x:A. UN y:B(x). \{\} -\subcaption{Definitions} +\tdx{fst_def} fst(p) == @a. ? b. p = +\tdx{snd_def} snd(p) == @b. ? a. p = +\tdx{split_def} split(p,c) == c(fst(p),snd(p)) +\tdx{Sigma_def} Sigma(A,B) == UN x:A. UN y:B(x). \{\} -\idx{Pair_inject} [| = ; [| a=a'; b=b' |] ==> R |] ==> R -\idx{fst} fst() = a -\idx{snd} snd() = b -\idx{split} split(, c) = c(a,b) +\tdx{Pair_inject} [| = ; [| a=a'; b=b' |] ==> R |] ==> R +\tdx{fst} fst() = a +\tdx{snd} snd() = b +\tdx{split} split(, c) = c(a,b) -\idx{surjective_pairing} p = +\tdx{surjective_pairing} p = -\idx{SigmaI} [| a:A; b:B(a) |] ==> : Sigma(A,B) +\tdx{SigmaI} [| a:A; b:B(a) |] ==> : Sigma(A,B) -\idx{SigmaE} [| c: Sigma(A,B); +\tdx{SigmaE} [| c: Sigma(A,B); !!x y.[| x:A; y:B(x); c= |] ==> 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 = \} -\idx{less_def} m:pred_nat^+ -\idx{nat_rec_def} nat_rec(n,c,d) == +\tdx{pred_nat_def} pred_nat == \{p. ? n. p = \} +\tdx{less_def} m: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 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} : pred_nat -\idx{pred_natE} +\tdx{pred_natI} : pred_nat +\tdx{pred_natE} [| p : pred_nat; !!x n. [| p = |] ==> 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 i i ~ m ~ m P(m) |] ==> P(n) |] ==> P(n) +\tdx{Suc_less_eq} (Suc(m) < Suc(n)) = (m P(m) |] ==> P(n) |] ==> P(n) -\idx{less_linear} m $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|)}