# HG changeset patch # User clasohm # Date 800008999 -7200 # Node ID dd72845736014b82c9569985356832b6c47f4b65 # Parent 737a1a0df75479db74416a1660e7a69baab6b462 converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex diff -r 737a1a0df754 -r dd7284573601 doc-src/Logics/CHOL.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Logics/CHOL.tex Tue May 09 10:43:19 1995 +0200 @@ -0,0 +1,1898 @@ +%% $Id$ +\chapter{Higher-Order Logic} +\index{higher-order logic|(} +\index{CHOL system@{\sc chol} system} + +The theory~\thydx{CHOL} implements higher-order logic with curried +function application. It is based on Gordon's~{\sc hol} +system~\cite{mgordon-hol}, which itself is 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 \CHOL\ to~{\ZF}. + +\CHOL\ is a modified version of Isabelle's \HOL\ and uses curried function +application. Therefore the expression $f(a,b)$ (which in \HOL\ means +``f applied to the two arguments $a$ and $b$'') means ``f applied to +the pair $(a,b)$'' in \CHOL. N.B. that ordered pairs in \HOL\ are written as +$$ while in \CHOL\ the syntax $(a,b)$ is used. Previous +releases of Isabelle also 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. + +\CHOL\ 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 +written as simply~$f~a$ rather than $f{\tt`}a$. + +These identifications allow Isabelle to support \CHOL\ particularly nicely, +but they also mean that \CHOL\ requires more sophistication from the user +--- in particular, an understanding of Isabelle's type system. Beginners +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 \\ + \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} symbol} +\index{*"! symbol}\index{*"? symbol} +\index{*"?"! symbol}\index{*"E"X"! symbol} +\begin{tabular}{llrrr} + \it symbol &\it name &\it meta-type & \it description \\ + \tt\at & \cdx{Eps} & $(\alpha\To bool)\To\alpha::term$ & + Hilbert description ($\epsilon$) \\ + {\tt!~} or \sdx{ALL} & \cdx{All} & $(\alpha::term\To bool)\To bool$ & + universal quantifier ($\forall$) \\ + {\tt?~} or \sdx{EX} & \cdx{Ex} & $(\alpha::term\To bool)\To bool$ & + existential quantifier ($\exists$) \\ + {\tt?!} or {\tt EX!} & \cdx{Ex1} & $(\alpha::term\To bool)\To bool$ & + unique existence ($\exists!$) +\end{tabular} +\end{center} +\subcaption{Binders} + +\begin{center} +\index{*"= symbol} +\index{&@{\tt\&} symbol} +\index{*"| symbol} +\index{*"-"-"> symbol} +\begin{tabular}{rrrr} + \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$) +\end{tabular} +\end{center} +\subcaption{Infixes} +\caption{Syntax of {\tt HOL}} \label{chol-constants} +\end{figure} + + +\begin{figure} +\index{*let symbol} +\index{*in symbol} +\dquotes +\[\begin{array}{rclcl} + term & = & \hbox{expression of class~$term$} \\ + & | & "\at~" id~id^* " . " formula \\ + & | & + \multicolumn{3}{l}{"let"~id~"="~term";"\dots";"~id~"="~term~"in"~term} \\ + & | & + \multicolumn{3}{l}{"if"~formula~"then"~term~"else"~term} \\[2ex] + formula & = & \hbox{expression of type~$bool$} \\ + & | & term " = " term \\ + & | & term " \ttilde= " term \\ + & | & term " < " term \\ + & | & term " <= " term \\ + & | & "\ttilde\ " formula \\ + & | & formula " \& " formula \\ + & | & formula " | " formula \\ + & | & formula " --> " formula \\ + & | & "!~~~" id~id^* " . " formula + & | & "ALL~" id~id^* " . " formula \\ + & | & "?~~~" id~id^* " . " formula + & | & "EX~~" id~id^* " . " formula \\ + & | & "?!~~" id~id^* " . " formula + & | & "EX!~" id~id^* " . " formula + \end{array} +\] +\caption{Full grammar for \CHOL} \label{chol-grammar} +\end{figure} + + +\section{Syntax} +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 \cldx{ord} consists of all ordered types; the relations $<$ and +$\leq$ are polymorphic over this class, as are the functions +\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{*"+ symbol} +\index{*"- symbol} +\index{*"* symbol} + +Figure~\ref{chol-constants} lists the constants (including infixes and +binders), while Fig.\ts\ref{chol-grammar} presents the grammar of +higher-order logic. Note that $a$\verb|~=|$b$ is translated to +$\neg(a=b)$. + +\begin{warn} + \CHOL\ 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{CHOL-types} +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 \CHOL\ 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$ +specifies a non-empty subset of~$\sigma$, and the new type denotes this +subset. New function constants are generated to establish an isomorphism +between the new type and the subset. If type~$\sigma$ involves type +variables $\alpha@1$, \ldots, $\alpha@n$, then the type definition creates +a type constructor $(\alpha@1,\ldots,\alpha@n)ty$ rather than a particular +type. Melham~\cite{melham89} discusses type definitions at length, with +examples. + +Isabelle does not support type definitions at present. Instead, they are +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} +Hilbert's {\bf description} operator~$\epsilon x.P[x]$ stands for some~$a$ +satisfying~$P[a]$, if such exists. Since all terms in \CHOL\ 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 +\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{*"! symbol}\index{*"? symbol}\index{CHOL system@{\sc hol} system} +Quantifiers have two notations. As in Gordon's {\sc hol} system, \CHOL\ +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, \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. + +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{chol-grammar}. Internally it is translated into +the constant~\cdx{Let}. It can be expanded by rewriting with its +definition, \tdx{Let_def}. + +\CHOL\ 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{chol-list} 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 CHOL} rules} \label{chol-rules} +\end{figure} + + +\begin{figure}\hfuzz=4pt%suppress "Overfull \hbox" message +\begin{ttbox}\makeatother +\tdx{True_def} True == ((\%x::bool.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 == (\%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 CHOL} definitions} \label{chol-defs} +\end{figure} + + +\section{Rules of inference} +Figure~\ref{chol-rules} shows the inference rules of~\CHOL{}, 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} + +\CHOL{} follows standard practice in higher-order logic: only a few +connectives are taken as primitive, with the remainder defined obscurely +(Fig.\ts\ref{chol-defs}). Gordon's {\sc hol} system expresses the +corresponding definitions \cite[page~270]{mgordon-hol} using +object-equality~({\tt=}), which is possible because equality in +higher-order logic may equate formulae and even functions over formulae. +But theory~\CHOL{}, like all other Isabelle theories, uses +meta-equality~({\tt==}) for definitions. + +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}. + +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} +\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} x=y ==> f x=f y +\tdx{fun_cong} f=g ==> f x=g x +\subcaption{Equality} + +\tdx{TrueI} True +\tdx{FalseE} False ==> P + +\tdx{conjI} [| P; Q |] ==> P&Q +\tdx{conjunct1} [| P&Q |] ==> P +\tdx{conjunct2} [| P&Q |] ==> Q +\tdx{conjE} [| P&Q; [| P; Q |] ==> R |] ==> R + +\tdx{disjI1} P ==> P|Q +\tdx{disjI2} Q ==> P|Q +\tdx{disjE} [| P | Q; P ==> R; Q ==> R |] ==> R + +\tdx{notI} (P ==> False) ==> ~ P +\tdx{notE} [| ~ P; P |] ==> R +\tdx{impE} [| P-->Q; P; Q ==> R |] ==> R +\subcaption{Propositional logic} + +\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 + +\tdx{eqTrueI} P ==> P=True +\tdx{eqTrueE} P=True ==> P +\subcaption{Logical equivalence} + +\end{ttbox} +\caption{Derived rules for \CHOL} \label{chol-lemmas1} +\end{figure} + + +\begin{figure} +\begin{ttbox}\makeatother +\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 + +\tdx{exI} P x ==> ? x::'a.P x +\tdx{exE} [| ? x::'a.P x; !!x. P x ==> Q |] ==> Q + +\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 + +\tdx{select_equality} [| P a; !!x. P x ==> x=a |] ==> (@x.P x) = a +\subcaption{Quantifiers and descriptions} + +\tdx{ccontr} (~P ==> False) ==> P +\tdx{classical} (~P ==> P) ==> P +\tdx{excluded_middle} ~P | P + +\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} + +\tdx{if_True} if True then x else y = x +\tdx{if_False} if False then x else y = y +\tdx{if_P} P ==> if P then x else y = x +\tdx{if_not_P} ~ P ==> if P then x else y = y +\tdx{expand_if} P(if Q then x else y) = ((Q --> P x) & (~Q --> P y)) +\subcaption{Conditionals} +\end{ttbox} +\caption{More derived rules} \label{chol-lemmas2} +\end{figure} + + +Some derived rules are shown in Figures~\ref{chol-lemmas1} +and~\ref{chol-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: \tdx{ssubst} performs substitution in +backward proofs, while \tdx{box_equals} supports reasoning by +simplifying both sides of an equation. + + +\begin{figure} +\begin{center} +\begin{tabular}{rrr} + \it name &\it meta-type & \it description \\ +\index{{}@\verb'{}' symbol} + \verb|{}| & $\alpha\,set$ & the empty set \\ + \cdx{insert} & $[\alpha,\alpha\,set]\To \alpha\,set$ + & insertion of element \\ + \cdx{Collect} & $(\alpha\To bool)\To\alpha\,set$ + & comprehension \\ + \cdx{Compl} & $(\alpha\,set)\To\alpha\,set$ + & complement \\ + \cdx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$ + & intersection over a set\\ + \cdx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$ + & union over a set\\ + \cdx{Inter} & $(\alpha\,set)set\To\alpha\,set$ + &set of sets intersection \\ + \cdx{Union} & $(\alpha\,set)set\To\alpha\,set$ + &set of sets union \\ + \cdx{Pow} & $\alpha\,set \To (\alpha\,set)set$ + & powerset \\[1ex] + \cdx{range} & $(\alpha\To\beta )\To\beta\,set$ + & range of a function \\[1ex] + \cdx{Ball}~~\cdx{Bex} & $[\alpha\,set,\alpha\To bool]\To bool$ + & bounded quantifiers \\ + \cdx{mono} & $(\alpha\,set\To\beta\,set)\To bool$ + & monotonicity \\ + \cdx{inj}~~\cdx{surj}& $(\alpha\To\beta )\To bool$ + & injective/surjective \\ + \cdx{inj_onto} & $[\alpha\To\beta ,\alpha\,set]\To bool$ + & injective over subset +\end{tabular} +\end{center} +\subcaption{Constants} + +\begin{center} +\begin{tabular}{llrrr} + \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\\ + \sdx{UN} & \cdx{UNION1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 & + union over a type +\end{tabular} +\end{center} +\subcaption{Binders} + +\begin{center} +\index{*"`"` symbol} +\index{*": symbol} +\index{*"<"= symbol} +\begin{tabular}{rrrr} + \it symbol & \it meta-type & \it priority & \it description \\ + \tt `` & $[\alpha\To\beta ,\alpha\,set]\To (\beta\,set)$ + & Left 90 & image \\ + \sdx{Int} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$ + & Left 70 & intersection ($\inter$) \\ + \sdx{Un} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$ + & Left 65 & union ($\union$) \\ + \tt: & $[\alpha ,\alpha\,set]\To bool$ + & Left 50 & membership ($\in$) \\ + \tt <= & $[\alpha\,set,\alpha\,set]\To bool$ + & Left 50 & subset ($\subseteq$) +\end{tabular} +\end{center} +\subcaption{Infixes} +\caption{Syntax of the theory {\tt Set}} \label{chol-set-syntax} +\end{figure} + + +\begin{figure} +\begin{center} \tt\frenchspacing +\index{*"! symbol} +\begin{tabular}{rrr} + \it external & \it internal & \it description \\ + $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 \\ + \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$ \\ + \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}{rclcl} + term & = & \hbox{other terms\ldots} \\ + & | & "\{\}" \\ + & | & "\{ " term\; ("," term)^* " \}" \\ + & | & "\{ " id " . " formula " \}" \\ + & | & term " `` " term \\ + & | & term " Int " term \\ + & | & term " Un " term \\ + & | & "INT~~" id ":" term " . " term \\ + & | & "UN~~~" id ":" term " . " term \\ + & | & "INT~~" id~id^* " . " term \\ + & | & "UN~~~" id~id^* " . " term \\[2ex] + formula & = & \hbox{other formulae\ldots} \\ + & | & term " : " term \\ + & | & term " \ttilde: " term \\ + & | & term " <= " term \\ + & | & "!~" id ":" term " . " formula + & | & "ALL " id ":" term " . " formula \\ + & | & "?~" id ":" term " . " formula + & | & "EX~~" id ":" term " . " formula + \end{array} +\] +\subcaption{Full Grammar} +\caption{Syntax of the theory {\tt Set} (continued)} \label{chol-set-syntax2} +\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 +{\bf sets}, but note that these sets are distinct from those of {\ZF} set +theory, and behave more like {\ZF} classes. +\begin{itemize} +\item +Sets are given by predicates over some type~$\sigma$. Types serve to +define universes for sets, but type checking is still significant. +\item +There is a universal set (for each type). Thus, sets have complements, and +may be defined by absolute comprehension. +\item +Although sets may contain other sets as elements, the containing set must +have a more complex type. +\end{itemize} +Finite unions and intersections have the same behaviour in \CHOL\ as they +do in~{\ZF}. In \CHOL\ the intersection of the empty set is well-defined, +denoting the universal set for the given type. + + +\subsection{Syntax of set theory}\index{*set type} +\CHOL'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{CHOL-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{chol-set-syntax} lists the constants, infixes, and syntax +translations. Figure~\ref{chol-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 +$\neg(a\in b)$. + +The {\tt\{\ldots\}} notation abbreviates finite sets constructed in the +obvious manner using~{\tt insert} and~$\{\}$: +\begin{eqnarray*} + \{a@1, \ldots, a@n\} & \equiv & + {\tt insert}~a@1~({\tt insert}\ldots({\tt insert}~a@n~\{\})\ldots) +\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 \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{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~\cdx{Ball} and~\cdx{Bex} are defined +accordingly. Instead of {\tt Ball $A$ $P$} and {\tt Bex $A$ $P$} we may +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 +\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 + +\tdx{empty_def} \{\} == \{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{Pow_def} Pow A == \{B. B <= A\} +\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{chol-set-rules} +\end{figure} + + +\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_trans} [| A<=B; B<=C |] ==> A<=C + +\tdx{equalityI} [| A <= B; B <= A |] ==> 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{chol-set1} +\end{figure} + + +\begin{figure} \underscoreon +\begin{ttbox} +\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 + +\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 + +\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 + +\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 + +\tdx{PowI} A<=B ==> A: Pow B +\tdx{PowD} A: Pow B ==> A<=B +\end{ttbox} +\caption{Further derived rules for set theory} \label{chol-set2} +\end{figure} + + +\subsection{Axioms and rules of set theory} +Figure~\ref{chol-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. + +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 + +%\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 + +\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 +\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{chol-fun} +\end{figure} + + +\begin{figure} \underscoreon +\begin{ttbox} +\tdx{Union_upper} B:A ==> B <= Union A +\tdx{Union_least} [| !!X. X:A ==> X<=C |] ==> Union A <= C + +\tdx{Inter_lower} B:A ==> Inter A <= B +\tdx{Inter_greatest} [| !!X. X:A ==> C<=X |] ==> C <= Inter A + +\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 + +\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{chol-subset} +\end{figure} + + +\begin{figure} \underscoreon \hfuzz=4pt%suppress "Overfull \hbox" message +\begin{ttbox} +\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) + +\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) + +\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) + +\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) + +\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{chol-equalities} +\end{figure} + + +Figures~\ref{chol-set1} and~\ref{chol-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 CHOL/Set.ML} for +proofs pertaining to set theory. + +Figure~\ref{chol-fun} presents derived inference rules involving functions. +They also include rules for \cdx{Inv}, which is defined in theory~{\tt + CHOL}; 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 CHOL/fun.ML} for a complete listing of the derived rules. + +Figure~\ref{chol-subset} presents lattice properties of the subset relation. +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 CHOL/subset.ML}. + +Figure~\ref{chol-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 CHOL/equalities.ML}. + + +\begin{figure} +\begin{constants} + \it symbol & \it meta-type & & \it description \\ + \cdx{Pair} & $[\alpha,\beta]\To \alpha\times\beta$ + & & ordered pairs $(a,b)$ \\ + \cdx{fst} & $\alpha\times\beta \To \alpha$ & & first projection\\ + \cdx{snd} & $\alpha\times\beta \To \beta$ & & second projection\\ + \cdx{split} & $[[\alpha,\beta]\To\gamma, \alpha\times\beta] \To \gamma$ + & & generalized projection\\ + \cdx{Sigma} & + $[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ & + & general sum of sets +\end{constants} +\begin{ttbox}\makeatletter +\tdx{fst_def} fst p == @a. ? b. p = (a,b) +\tdx{snd_def} snd p == @b. ? a. p = (a,b) +\tdx{split_def} split c p == c (fst p) (snd p) +\tdx{Sigma_def} Sigma A B == UN x:A. UN y:B x. \{(x,y)\} + + +\tdx{Pair_inject} [| (a, b) = (a',b'); [| a=a'; b=b' |] ==> R |] ==> R +\tdx{fst_conv} fst (a,b) = a +\tdx{snd_conv} snd (a,b) = b +\tdx{split} split c (a,b) = c a b + +\tdx{surjective_pairing} p = (fst p,snd p) + +\tdx{SigmaI} [| a:A; b:B a |] ==> (a,b) : Sigma A B + +\tdx{SigmaE} [| c: Sigma A B; + !!x y.[| x:A; y:B x; c=(x,y) |] ==> P |] ==> P +\end{ttbox} +\caption{Type $\alpha\times\beta$}\label{chol-prod} +\end{figure} + + +\begin{figure} +\begin{constants} + \it symbol & \it meta-type & & \it description \\ + \cdx{Inl} & $\alpha \To \alpha+\beta$ & & first injection\\ + \cdx{Inr} & $\beta \To \alpha+\beta$ & & second injection\\ + \cdx{sum_case} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$ + & & conditional +\end{constants} +\begin{ttbox}\makeatletter +\tdx{sum_case_def} sum_case == (\%f g p. @z. (!x. p=Inl x --> z=f x) & + (!y. p=Inr y --> z=g y)) + +\tdx{Inl_not_Inr} ~ Inl a=Inr b + +\tdx{inj_Inl} inj Inl +\tdx{inj_Inr} inj Inr + +\tdx{sumE} [| !!x::'a. P(Inl x); !!y::'b. P(Inr y) |] ==> P s + +\tdx{sum_case_Inl} sum_case f g (Inl x) = f x +\tdx{sum_case_Inr} sum_case f g (Inr x) = g x + +\tdx{surjective_sum} sum_case (\%x::'a. f(Inl x)) (\%y::'b. f(Inr y)) s = f s +\end{ttbox} +\caption{Type $\alpha+\beta$}\label{chol-sum} +\end{figure} + + +\section{Generic packages and classical reasoning} +\CHOL\ instantiates most of Isabelle's generic packages; +see {\tt CHOL/ROOT.ML} for details. +\begin{itemize} +\item +Because it includes a general substitution rule, \CHOL\ instantiates the +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 +simplification set for higher-order logic. Equality~($=$), which also +expresses logical equivalence, may be used for rewriting. See the file +{\tt CHOL/simpdata.ML} for a complete listing of the simplification +rules. +\item +It instantiates the classical reasoner, as described below. +\end{itemize} +\CHOL\ derives classical introduction rules for $\disj$ and~$\exists$, as +well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap +rule; recall Fig.\ts\ref{chol-lemmas2} above. + +The classical reasoner is set up 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: +\begin{ttbox} +prop_cs : claset +HOL_cs : claset +set_cs : claset +\end{ttbox} +\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~{\tt refl}. + +\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{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 \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% + {Chap.\ts\ref{chap:classical}} +for more discussion of classical proof methods. + + +\section{Types} +The basic higher-order logic is augmented with a tremendous amount of +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 by 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}\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{chol-prod} and~\ref{chol-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 \tdx{select_equality}. + +\begin{figure} +\index{*"< symbol} +\index{*"* symbol} +\index{*div symbol} +\index{*mod 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} & $[\alpha, nat\To\alpha, nat] \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 div & $[nat,nat]\To nat$ & Left 70 & division\\ + \tt mod & $[nat,nat]\To nat$ & Left 70 & modulus\\ + \tt + & $[nat,nat]\To nat$ & Left 65 & addition\\ + \tt - & $[nat,nat]\To nat$ & Left 65 & subtraction +\end{constants} +\subcaption{Constants and infixes} + +\begin{ttbox}\makeatother +\tdx{nat_case_def} nat_case == (\%a f n. @z. (n=0 --> z=a) & + (!x. n=Suc x --> z=f x)) +\tdx{pred_nat_def} pred_nat == \{p. ? n. p = (n, Suc n)\} +\tdx{less_def} m P(Suc k) |] ==> P n + +\tdx{Suc_not_Zero} Suc m ~= 0 +\tdx{inj_Suc} inj Suc +\tdx{n_not_Suc_n} n~=Suc n +\subcaption{Basic properties} + +\tdx{pred_natI} (n, Suc n) : pred_nat +\tdx{pred_natE} + [| p : pred_nat; !!x n. [| p = (n, Suc n) |] ==> R |] ==> R + +\tdx{nat_case_0} nat_case a f 0 = a +\tdx{nat_case_Suc} nat_case a f (Suc k) = f k + +\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} + +\tdx{less_trans} [| i i ~ m P m |] ==> P n |] ==> P n + +\tdx{less_linear} m P x#xs) |] ==> P l + +\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 theory \thydx{List}} \label{chol-list} +\end{figure} + +\begin{figure} +\begin{ttbox}\makeatother +\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 c h x#xs = 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 then True else x mem ys + +\tdx{filter_Nil} filter P [] = [] +\tdx{filter_Cons} filter P x#xs = if P x then x#filter P xs else 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{chol-list-simps} +\end{figure} + + +\subsection{The type constructor for lists, {\tt list}} +\index{*list type} + +\CHOL's definition of lists is an example of an experimental method for +handling recursive data types. Figure~\ref{chol-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: +{\dquotes +\begin{eqnarray*} + \begin{array}{r@{\;}l@{}l} + "case " e " of" & "[]" & " => " a\\ + "|" & x"\#"xs & " => " b + \end{array} + & \equiv & + "list_case"~a~(\lambda x\;xs.b)~e +\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{chol-list-simps}. + +The tactic {\tt\ttindex{list_ind_tac} "$xs$" $i$} performs induction over the +variable~$xs$ in subgoal~$i$. + + +\section{Datatype declarations} +\index{*datatype|(} + +\underscoreon + +It is often necessary to extend a theory with \ML-like datatypes. This +extension consists of the new type, declarations of its constructors and +rules that describe the new type. The theory definition section {\tt + datatype} represents a compact way of doing this. + + +\subsection{Foundations} + +A datatype declaration has the following general structure: +\[ \mbox{\tt datatype}~ (\alpha_1,\dots,\alpha_n)t ~=~ + C_1~\tau_{11}~\dots~\tau_{1k_1} ~\mid~ \dots ~\mid~ + C_m~\tau_{m1}~\dots~\tau_{mk_m} +\] +where $\alpha_i$ are type variables, $C_i$ are distinct constructor names and +$\tau_{ij}$ are one of the following: +\begin{itemize} +\item type variables $\alpha_1,\dots,\alpha_n$, +\item types $(\beta_1,\dots,\beta_l)s$ where $s$ is a previously declared + type or type synonym and $\{\beta_1,\dots,\beta_l\} \subseteq + \{\alpha_1,\dots,\alpha_n\}$, +\item the newly defined type $(\alpha_1,\dots,\alpha_n)t$ \footnote{This + makes it a recursive type. To ensure that the new type is not empty at + least one constructor must consist of only non-recursive type + components.} +\end{itemize} +If you would like one of the $\tau_{ij}$ to be a complex type expression +$\tau$ you need to declare a new type synonym $syn = \tau$ first and use +$syn$ in place of $\tau$. Of course this does not work if $\tau$ mentions the +recursive type itself, thus ruling out problematic cases like \[ \mbox{\tt + datatype}~ t ~=~ C(t \To t) \] together with unproblematic ones like \[ +\mbox{\tt datatype}~ t ~=~ C(t~list). \] + +The constructors are automatically defined as functions of their respective +type: +\[ C_j : [\tau_{j1},\dots,\tau_{jk_j}] \To (\alpha_1,\dots,\alpha_n)t \] +These functions have certain {\em freeness} properties: +\begin{description} +\item[\tt distinct] They are distinct: +\[ C_i~x_1~\dots~x_{k_i} \neq C_j~y_1~\dots~y_{k_j} \qquad + \mbox{for all}~ i \neq j. +\] +\item[\tt inject] They are injective: +\[ (C_j~x_1~\dots~x_{k_j} = C_j~y_1~\dots~y_{k_j}) = + (x_1 = y_1 \land \dots \land x_{k_j} = y_{k_j}) +\] +\end{description} +Because the number of inequalities is quadratic in the number of +constructors, a different method is used if their number exceeds +a certain value, currently 4. In that case every constructor is mapped to a +natural number +\[ +\begin{array}{lcl} +\mbox{\it t\_ord}(C_1~x_1~\dots~x_{k_1}) & = & 0 \\ +& \vdots & \\ +\mbox{\it t\_ord}(C_m x_1~\dots~x_{k_m}) & = & m-1 +\end{array} +\] +and distinctness of constructors is expressed by: +\[ +\mbox{\it t\_ord}~x \neq \mbox{\it t\_ord}~y \Imp x \neq y. +\] +In addition a structural induction axiom {\tt induct} is provided: +\[ +\infer{P x} +{\begin{array}{lcl} +\Forall x_1\dots x_{k_1}. + \List{P~x_{r_{11}}; \dots; P~x_{r_{1l_1}}} & + \Imp & P(C_1~x_1~\dots~x_{k_1}) \\ + & \vdots & \\ +\Forall x_1\dots x_{k_m}. + \List{P~x_{r_{m1}}; \dots; P~x_{r_{ml_m}}} & + \Imp & P(C_m~x_1~\dots~x_{k_m}) +\end{array}} +\] +where $\{r_{j1},\dots,r_{jl_j}\} = \{i \in \{1,\dots k_j\} ~\mid~ \tau_{ji} += (\alpha_1,\dots,\alpha_n)t \}$, i.e.\ the property $P$ can be assumed for +all arguments of the recursive type. + +The type also comes with an \ML-like \sdx{case}-construct: +\[ +\begin{array}{rrcl} +\mbox{\tt case}~e~\mbox{\tt of} & C_1~x_{11}~\dots~x_{1k_1} & \To & e_1 \\ + \vdots \\ + \mid & C_m~x_{m1}~\dots~x_{mk_m} & \To & e_m +\end{array} +\] +In contrast to \ML, {\em all} constructors must be present, their order is +fixed, and nested patterns are not supported. + + +\subsection{Defining datatypes} + +A datatype is defined in a theory definition file using the keyword {\tt + datatype}. The definition following {\tt datatype} must conform to the +syntax of {\em typedecl} specified in Fig.~\ref{datatype-grammar} and must +obey the rules in the previous section. As a result the theory is extended +with the new type, the constructors, and the theorems listed in the previous +section. + +\begin{figure} +\begin{rail} +typedecl : typevarlist id '=' (cons + '|') + ; +cons : (id | string) ( () | '(' (typ + ',') ')' ) ( () | mixfix ) + ; +typ : typevarlist id + | tid + ; +typevarlist : () | tid | '(' (tid + ',') ')' + ; +\end{rail} +\caption{Syntax of datatype declarations} +\label{datatype-grammar} +\end{figure} + +Reading the theory file produces a structure which, in addition to the usual +components, contains a structure named $t$ for each datatype $t$ defined in +the file.\footnote{Otherwise multiple datatypes in the same theory file would + lead to name clashes.} Each structure $t$ contains the following elements: +\begin{ttbox} +val distinct : thm list +val inject : thm list +val induct : thm +val cases : thm list +val simps : thm list +val induct_tac : string -> int -> tactic +\end{ttbox} +{\tt distinct}, {\tt inject} and {\tt induct} contain the theorems described +above. For convenience {\tt distinct} contains inequalities in both +directions. +\begin{warn} + If there are five or more constructors, the {\em t\_ord} scheme is used for + {\tt distinct}. In this case the theory {\tt Arith} must be contained + in the current theory, if necessary by including it explicitly. +\end{warn} +The reduction rules of the {\tt case}-construct are in {\tt cases}. All +theorems from {\tt distinct}, {\tt inject} and {\tt cases} are combined in +{\tt simps} for use with the simplifier. The tactic {\verb$induct_tac$~{\em + var i}\/} applies structural induction over variable {\em var} to +subgoal {\em i}. + + +\subsection{Examples} + +\subsubsection{The datatype $\alpha~list$} + +We want to define the type $\alpha~list$.\footnote{Of course there is a list + type in CHOL already. This is only an example.} To do this we have to build +a new theory that contains the type definition. We start from {\tt CHOL}. +\begin{ttbox} +MyList = CHOL + + datatype 'a list = Nil | Cons 'a ('a list) +end +\end{ttbox} +After loading the theory (\verb$use_thy "MyList"$), we can prove +$Cons~x~xs\neq xs$. First we build a suitable simpset for the simplifier: +\begin{ttbox} +val mylist_ss = HOL_ss addsimps MyList.list.simps; +goal MyList.thy "!x. Cons x xs ~= xs"; +{\out Level 0} +{\out ! x. Cons x xs ~= xs} +{\out 1. ! x. Cons x xs ~= xs} +\end{ttbox} +This can be proved by the structural induction tactic: +\begin{ttbox} +by (MyList.list.induct_tac "xs" 1); +{\out Level 1} +{\out ! x. Cons x xs ~= xs} +{\out 1. ! x. Cons x Nil ~= Nil} +{\out 2. !!a list.} +{\out ! x. Cons x list ~= list ==>} +{\out ! x. Cons x (Cons a list) ~= Cons a list} +\end{ttbox} +The first subgoal can be proved with the simplifier and the distinctness +axioms which are part of \verb$mylist_ss$. +\begin{ttbox} +by (simp_tac mylist_ss 1); +{\out Level 2} +{\out ! x. Cons x xs ~= xs} +{\out 1. !!a list.} +{\out ! x. Cons x list ~= list ==>} +{\out ! x. Cons x (Cons a list) ~= Cons a list} +\end{ttbox} +Using the freeness axioms we can quickly prove the remaining goal. +\begin{ttbox} +by (asm_simp_tac mylist_ss 1); +{\out Level 3} +{\out ! x. Cons x xs ~= xs} +{\out No subgoals!} +\end{ttbox} +Because both subgoals were proved by almost the same tactic we could have +done that in one step using +\begin{ttbox} +by (ALLGOALS (asm_simp_tac mylist_ss)); +\end{ttbox} + + +\subsubsection{The datatype $\alpha~list$ with mixfix syntax} + +In this example we define the type $\alpha~list$ again but this time we want +to write {\tt []} instead of {\tt Nil} and we want to use the infix operator +\verb|#| instead of {\tt Cons}. To do this we simply add mixfix annotations +after the constructor declarations as follows: +\begin{ttbox} +MyList = CHOL + + datatype 'a list = "[]" ("[]") + | "#" 'a ('a list) (infixr 70) +end +\end{ttbox} +Now the theorem in the previous example can be written \verb|x#xs ~= xs|. The +proof is the same. + + +\subsubsection{A datatype for weekdays} + +This example shows a datatype that consists of more than four constructors: +\begin{ttbox} +Days = Arith + + datatype days = Mo | Tu | We | Th | Fr | Sa | So +end +\end{ttbox} +Because there are more than four constructors, the theory must be based on +{\tt Arith}. Inequality is defined via a function \verb|days_ord|. Although +the expression \verb|Mo ~= Tu| is not directly contained in {\tt distinct}, +it can be proved by the simplifier if \verb$arith_ss$ is used: +\begin{ttbox} +val days_ss = arith_ss addsimps Days.days.simps; + +goal Days.thy "Mo ~= Tu"; +by (simp_tac days_ss 1); +\end{ttbox} +Note that usually it is not necessary to derive these inequalities explicitly +because the simplifier will dispose of them automatically. + +\subsection{Primitive recursive functions} +\index{primitive recursion|(} +\index{*primrec|(} + +Datatypes come with a uniform way of defining functions, {\bf primitive + recursion}. Although it is possible to define primitive recursive functions +by asserting their reduction rules as new axioms, e.g.\ +\begin{ttbox} +Append = MyList + +consts app :: "['a list,'a list] => 'a list" +rules + app_Nil "app [] ys = ys" + app_Cons "app x#xs ys = x#app xs ys" +end +\end{ttbox} +this carries with it the danger of accidentally asserting an inconsistency, +as in \verb$app [] ys = us$. Therefore primitive recursive functions on +datatypes can be defined with a special syntax: +\begin{ttbox} +Append = MyList + +consts app :: "'['a list,'a list] => 'a list" +primrec app MyList.list + app_Nil "app [] ys = ys" + app_Cons "app x#xs ys = x#app xs ys" +end +\end{ttbox} +The system will now check that the two rules \verb$app_Nil$ and +\verb$app_Cons$ do indeed form a primitive recursive definition, thus +ensuring that consistency is maintained. For example +\begin{ttbox} +primrec app MyList.list + app_Nil "app [] ys = us" +\end{ttbox} +is rejected: +\begin{ttbox} +Extra variables on rhs +\end{ttbox} +\bigskip + +The general form of a primitive recursive definition is +\begin{ttbox} +primrec {\it function} {\it type} + {\it reduction rules} +\end{ttbox} +where +\begin{itemize} +\item {\it function} is the name of the function, either as an {\it id} or a + {\it string}. The function must already have been declared. +\item {\it type} is the name of the datatype, either as an {\it id} or in the + long form {\it Thy.t}, where {\it Thy} is the name of the parent theory the + datatype was declared in, and $t$ the name of the datatype. The long form + is required if the {\tt datatype} and the {\tt primrec} sections are in + different theories. +\item {\it reduction rules} specify one or more named equations of the form + {\it id\/}~{\it string}, where the identifier gives the name of the rule in + the result structure, and {\it string} is a reduction rule of the form \[ + f~x_1~\dots~x_m~(C~y_1~\dots~y_k)~z_1~\dots~z_n = r \] such that $C$ is a + constructor of the datatype, $r$ contains only the free variables on the + left-hand side, and all recursive calls in $r$ are of the form + $f~\dots~y_i~\dots$ for some $i$. There must be exactly one reduction + rule for each constructor. +\end{itemize} +A theory file may contain any number of {\tt primrec} sections which may be +intermixed with other declarations. + +For the consistency-sensitive user it may be reassuring to know that {\tt + primrec} does not assert the reduction rules as new axioms but derives them +as theorems from an explicit definition of the recursive function in terms of +a recursion operator on the datatype. + +The primitive recursive function can also use infix or mixfix syntax: +\begin{ttbox} +Append = MyList + +consts "@" :: "['a list,'a list] => 'a list" (infixr 60) +primrec "op @" MyList.list + app_Nil "[] @ ys = ys" + app_Cons "(x#xs) @ ys = x#(xs @ ys)" +end +\end{ttbox} + +The reduction rules become part of the ML structure \verb$Append$ and can +be used to prove theorems about the function: +\begin{ttbox} +val append_ss = HOL_ss addsimps [Append.app_Nil,Append.app_Cons]; + +goal Append.thy "(xs @ ys) @ zs = xs @ (ys @ zs)"; +by (MyList.list.induct_tac "xs" 1); +by (ALLGOALS(asm_simp_tac append_ss)); +\end{ttbox} + +%Note that underdefined primitive recursive functions are allowed: +%\begin{ttbox} +%Tl = MyList + +%consts tl :: "'a list => 'a list" +%primrec tl MyList.list +% tl_Cons "tl(x#xs) = xs" +%end +%\end{ttbox} +%Nevertheless {\tt tl} is total, although we do not know what the result of +%\verb$tl([])$ is. + +\index{primitive recursion|)} +\index{*primrec|)} +\index{*datatype|)} + + +\section{Inductive and coinductive definitions} +\index{*inductive|(} +\index{*coinductive|(} + +An {\bf inductive definition} specifies the least set closed under given +rules. For example, a structural operational semantics is an inductive +definition of an evaluation relation. Dually, a {\bf coinductive + definition} specifies the greatest set closed under given rules. An +important example is using bisimulation relations to formalize equivalence +of processes and infinite data structures. + +A theory file may contain any number of inductive and coinductive +definitions. They may be intermixed with other declarations; in +particular, the (co)inductive sets {\bf must} be declared separately as +constants, and may have mixfix syntax or be subject to syntax translations. + +Each (co)inductive definition adds definitions to the theory and also +proves some theorems. Each definition creates an ML structure, which is a +substructure of the main theory structure. + +This package is derived from the ZF one, described in a +separate paper,\footnote{It appeared in CADE~\cite{paulson-CADE} and a + longer version is distributed with Isabelle.} which you should refer to +in case of difficulties. The package is simpler than ZF's, thanks to CHOL's +automatic type-checking. The type of the (co)inductive determines the +domain of the fixedpoint definition, and the package does not use inference +rules for type-checking. + + +\subsection{The result structure} +Many of the result structure's components have been discussed in the paper; +others are self-explanatory. +\begin{description} +\item[\tt thy] is the new theory containing the recursive sets. + +\item[\tt defs] is the list of definitions of the recursive sets. + +\item[\tt mono] is a monotonicity theorem for the fixedpoint operator. + +\item[\tt unfold] is a fixedpoint equation for the recursive set (the union of +the recursive sets, in the case of mutual recursion). + +\item[\tt intrs] is the list of introduction rules, now proved as theorems, for +the recursive sets. The rules are also available individually, using the +names given them in the theory file. + +\item[\tt elim] is the elimination rule. + +\item[\tt mk\_cases] is a function to create simplified instances of {\tt +elim}, using freeness reasoning on some underlying datatype. +\end{description} + +For an inductive definition, the result structure contains two induction rules, +{\tt induct} and \verb|mutual_induct|. For a coinductive definition, it +contains the rule \verb|coinduct|. + +Figure~\ref{def-result-fig} summarizes the two result signatures, +specifying the types of all these components. + +\begin{figure} +\begin{ttbox} +sig +val thy : theory +val defs : thm list +val mono : thm +val unfold : thm +val intrs : thm list +val elim : thm +val mk_cases : thm list -> string -> thm +{\it(Inductive definitions only)} +val induct : thm +val mutual_induct: thm +{\it(Coinductive definitions only)} +val coinduct : thm +end +\end{ttbox} +\hrule +\caption{The result of a (co)inductive definition} \label{def-result-fig} +\end{figure} + +\subsection{The syntax of a (co)inductive definition} +An inductive definition has the form +\begin{ttbox} +inductive {\it inductive sets} + intrs {\it introduction rules} + monos {\it monotonicity theorems} + con_defs {\it constructor definitions} +\end{ttbox} +A coinductive definition is identical, except that it starts with the keyword +{\tt coinductive}. + +The {\tt monos} and {\tt con\_defs} sections are optional. If present, +each is specified as a string, which must be a valid ML expression of type +{\tt thm list}. It is simply inserted into the {\tt .thy.ML} file; if it +is ill-formed, it will trigger ML error messages. You can then inspect the +file on your directory. + +\begin{itemize} +\item The {\it inductive sets} are specified by one or more strings. + +\item The {\it introduction rules} specify one or more introduction rules in + the form {\it ident\/}~{\it string}, where the identifier gives the name of + the rule in the result structure. + +\item The {\it monotonicity theorems} are required for each operator + applied to a recursive set in the introduction rules. There {\bf must} + be a theorem of the form $A\subseteq B\Imp M(A)\subseteq M(B)$, for each + premise $t\in M(R_i)$ in an introduction rule! + +\item The {\it constructor definitions} contain definitions of constants + appearing in the introduction rules. In most cases it can be omitted. +\end{itemize} + +The package has a few notable restrictions: +\begin{itemize} +\item The theory must separately declare the recursive sets as + constants. + +\item The names of the recursive sets must be identifiers, not infix +operators. + +\item Side-conditions must not be conjunctions. However, an introduction rule +may contain any number of side-conditions. + +\item Side-conditions of the form $x=t$, where the variable~$x$ does not + occur in~$t$, will be substituted through the rule \verb|mutual_induct|. +\end{itemize} + + +\subsection{Example of an inductive definition} +Two declarations, included in a theory file, define the finite powerset +operator. First we declare the constant~{\tt Fin}. Then we declare it +inductively, with two introduction rules: +\begin{ttbox} +consts Fin :: "'a set => 'a set set" +inductive "Fin A" + intrs + emptyI "{} : Fin A" + insertI "[| a: A; b: Fin A |] ==> insert a b : Fin A" +\end{ttbox} +The resulting theory structure contains a substructure, called~{\tt Fin}. +It contains the {\tt Fin}$~A$ introduction rules as the list {\tt Fin.intrs}, +and also individually as {\tt Fin.emptyI} and {\tt Fin.consI}. The induction +rule is {\tt Fin.induct}. + +For another example, here is a theory file defining the accessible part of a +relation. The main thing to note is the use of~{\tt Pow} in the sole +introduction rule, and the corresponding mention of the rule +\verb|Pow_mono| in the {\tt monos} list. The paper discusses a ZF version +of this example in more detail. +\begin{ttbox} +Acc = WF + +consts pred :: "['b, ('a * 'b)set] => 'a set" (*Set of predecessors*) + acc :: "('a * 'a)set => 'a set" (*Accessible part*) +defs pred_def "pred x r == {y. (y,x):r}" +inductive "acc r" + intrs + pred "pred a r: Pow(acc r) ==> a: acc r" + monos "[Pow_mono]" +end +\end{ttbox} +The CHOL distribution contains many other inductive definitions, such as the +theory {\tt CHOL/ex/PropLog.thy} and the directory {\tt CHOL/IMP}. The +theory {\tt CHOL/ex/LList.thy} contains coinductive definitions. + +\index{*coinductive|)} \index{*inductive|)} \underscoreoff + + +\section{The examples directories} +Directory {\tt CHOL/Subst} contains Martin Coen's mechanisation of a theory of +substitutions and unifiers. It is based on Paulson's previous +mechanisation in {\LCF}~\cite{paulson85} of Manna and Waldinger's +theory~\cite{mw81}. + +Directory {\tt CHOL/IMP} contains a mechanised version of a semantic +equivalence proof taken from Winskel~\cite{winskel93}. It formalises the +denotational and operational semantics of a simple while-language, then +proves the two equivalent. It contains several datatype and inductive +definitions, and demonstrates their use. + +Directory {\tt CHOL/ex} contains other examples and experimental proofs in +{\CHOL}. Here is an overview of the more interesting files. +\begin{itemize} +\item File {\tt cla.ML} demonstrates the classical reasoner on over sixty + predicate calculus theorems, ranging from simple tautologies to + moderately difficult problems involving equality and quantifiers. + +\item File {\tt 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 File {\tt mesontest.ML} contains test data for the {\sc meson} proof + procedure. These are mostly taken from Pelletier \cite{pelletier86}. + +\item File {\tt set.ML} proves Cantor's Theorem, which is presented in + \S\ref{sec:chol-cantor} below, and the Schr\"oder-Bernstein Theorem. + +\item Theories {\tt InSort} and {\tt Qsort} prove correctness properties of + insertion sort and quick sort. + +\item The definition of lazy lists demonstrates methods for handling + infinite data structures and coinduction in higher-order + logic~\cite{paulson-coind}. Theory \thydx{LList} 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 coinduction principle is defined + for proving equations on lazy lists. + +\item Theory {\tt PropLog} 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. A similar proof in \ZF{} is + described elsewhere~\cite{paulson-set-II}. + +\item Theory {\tt Term} develops an experimental recursive type definition; + the recursion goes through the type constructor~\tydx{list}. + +\item Theory {\tt Simult} constructs mutually recursive sets of trees and + forests, including induction and recursion rules. + +\item Theory {\tt MT} 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{itemize} + + +\goodbreak +\section{Example: Cantor's Theorem}\label{sec:chol-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 \CHOL'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 \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} +{\out ~ ?S : range f} +{\out 1. ?S : range f ==> False} +\ttbreak +by (eresolve_tac [rangeE] 1); +{\out Level 2} +{\out ~ ?S : range f} +{\out 1. !!x. ?S = f x ==> False} +\end{ttbox} +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} +by (eresolve_tac [equalityCE] 1); +{\out Level 3} +{\out ~ ?S : range f} +{\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 +comprehension. Then $\Var{c}\in\{x.\Var{P}~x\}$ implies +$\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} +{\out ~ \{x. ?P7 x\} : range f} +{\out 1. !!x. [| ?c3 x : f x; ?P7(?c3 x) |] ==> False} +{\out 2. !!x. [| ~ ?c3 x : \{x. ?P7 x\}; ~ ?c3 x : f x |] ==> False} +\end{ttbox} +Forcing a contradiction between the two assumptions of subgoal~1 completes +the instantiation of~$S$. It is now the set $\{x. x\not\in f~x\}$, which +is the standard diagonal construction. +\begin{ttbox} +by (contr_tac 1); +{\out Level 5} +{\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 \tdx{CollectI} to the negated +assumption, we employ \ttindex{swap_res_tac}: +\begin{ttbox} +by (swap_res_tac [CollectI] 1); +{\out Level 6} +{\out ~ \{x. ~ x : f x\} : range f} +{\out 1. !!x. [| ~ x : f x; ~ False |] ==> ~ x : f x} +\ttbreak +by (assume_tac 1); +{\out Level 7} +{\out ~ \{x. ~ x : f x\} : range f} +{\out No subgoals!} +\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 \CHOL'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} +{\out ~ ?S : range f} +{\out 1. ~ ?S : range f} +\ttbreak +by (best_tac (set_cs addSEs [equalityCE]) 1); +{\out Level 1} +{\out ~ \{x. ~ x : f x\} : range f} +{\out No subgoals!} +\end{ttbox} + +\index{higher-order logic|)} diff -r 737a1a0df754 -r dd7284573601 doc-src/Logics/HOL.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Logics/HOL.tex Tue May 09 10:43:19 1995 +0200 @@ -0,0 +1,1898 @@ +%% $Id$ +\chapter{Higher-Order Logic} +\index{higher-order logic|(} +\index{CHOL system@{\sc chol} system} + +The theory~\thydx{CHOL} implements higher-order logic with curried +function application. It is based on Gordon's~{\sc hol} +system~\cite{mgordon-hol}, which itself is 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 \CHOL\ to~{\ZF}. + +\CHOL\ is a modified version of Isabelle's \HOL\ and uses curried function +application. Therefore the expression $f(a,b)$ (which in \HOL\ means +``f applied to the two arguments $a$ and $b$'') means ``f applied to +the pair $(a,b)$'' in \CHOL. N.B. that ordered pairs in \HOL\ are written as +$$ while in \CHOL\ the syntax $(a,b)$ is used. Previous +releases of Isabelle also 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. + +\CHOL\ 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 +written as simply~$f~a$ rather than $f{\tt`}a$. + +These identifications allow Isabelle to support \CHOL\ particularly nicely, +but they also mean that \CHOL\ requires more sophistication from the user +--- in particular, an understanding of Isabelle's type system. Beginners +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 \\ + \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} symbol} +\index{*"! symbol}\index{*"? symbol} +\index{*"?"! symbol}\index{*"E"X"! symbol} +\begin{tabular}{llrrr} + \it symbol &\it name &\it meta-type & \it description \\ + \tt\at & \cdx{Eps} & $(\alpha\To bool)\To\alpha::term$ & + Hilbert description ($\epsilon$) \\ + {\tt!~} or \sdx{ALL} & \cdx{All} & $(\alpha::term\To bool)\To bool$ & + universal quantifier ($\forall$) \\ + {\tt?~} or \sdx{EX} & \cdx{Ex} & $(\alpha::term\To bool)\To bool$ & + existential quantifier ($\exists$) \\ + {\tt?!} or {\tt EX!} & \cdx{Ex1} & $(\alpha::term\To bool)\To bool$ & + unique existence ($\exists!$) +\end{tabular} +\end{center} +\subcaption{Binders} + +\begin{center} +\index{*"= symbol} +\index{&@{\tt\&} symbol} +\index{*"| symbol} +\index{*"-"-"> symbol} +\begin{tabular}{rrrr} + \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$) +\end{tabular} +\end{center} +\subcaption{Infixes} +\caption{Syntax of {\tt HOL}} \label{chol-constants} +\end{figure} + + +\begin{figure} +\index{*let symbol} +\index{*in symbol} +\dquotes +\[\begin{array}{rclcl} + term & = & \hbox{expression of class~$term$} \\ + & | & "\at~" id~id^* " . " formula \\ + & | & + \multicolumn{3}{l}{"let"~id~"="~term";"\dots";"~id~"="~term~"in"~term} \\ + & | & + \multicolumn{3}{l}{"if"~formula~"then"~term~"else"~term} \\[2ex] + formula & = & \hbox{expression of type~$bool$} \\ + & | & term " = " term \\ + & | & term " \ttilde= " term \\ + & | & term " < " term \\ + & | & term " <= " term \\ + & | & "\ttilde\ " formula \\ + & | & formula " \& " formula \\ + & | & formula " | " formula \\ + & | & formula " --> " formula \\ + & | & "!~~~" id~id^* " . " formula + & | & "ALL~" id~id^* " . " formula \\ + & | & "?~~~" id~id^* " . " formula + & | & "EX~~" id~id^* " . " formula \\ + & | & "?!~~" id~id^* " . " formula + & | & "EX!~" id~id^* " . " formula + \end{array} +\] +\caption{Full grammar for \CHOL} \label{chol-grammar} +\end{figure} + + +\section{Syntax} +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 \cldx{ord} consists of all ordered types; the relations $<$ and +$\leq$ are polymorphic over this class, as are the functions +\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{*"+ symbol} +\index{*"- symbol} +\index{*"* symbol} + +Figure~\ref{chol-constants} lists the constants (including infixes and +binders), while Fig.\ts\ref{chol-grammar} presents the grammar of +higher-order logic. Note that $a$\verb|~=|$b$ is translated to +$\neg(a=b)$. + +\begin{warn} + \CHOL\ 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{CHOL-types} +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 \CHOL\ 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$ +specifies a non-empty subset of~$\sigma$, and the new type denotes this +subset. New function constants are generated to establish an isomorphism +between the new type and the subset. If type~$\sigma$ involves type +variables $\alpha@1$, \ldots, $\alpha@n$, then the type definition creates +a type constructor $(\alpha@1,\ldots,\alpha@n)ty$ rather than a particular +type. Melham~\cite{melham89} discusses type definitions at length, with +examples. + +Isabelle does not support type definitions at present. Instead, they are +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} +Hilbert's {\bf description} operator~$\epsilon x.P[x]$ stands for some~$a$ +satisfying~$P[a]$, if such exists. Since all terms in \CHOL\ 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 +\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{*"! symbol}\index{*"? symbol}\index{CHOL system@{\sc hol} system} +Quantifiers have two notations. As in Gordon's {\sc hol} system, \CHOL\ +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, \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. + +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{chol-grammar}. Internally it is translated into +the constant~\cdx{Let}. It can be expanded by rewriting with its +definition, \tdx{Let_def}. + +\CHOL\ 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{chol-list} 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 CHOL} rules} \label{chol-rules} +\end{figure} + + +\begin{figure}\hfuzz=4pt%suppress "Overfull \hbox" message +\begin{ttbox}\makeatother +\tdx{True_def} True == ((\%x::bool.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 == (\%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 CHOL} definitions} \label{chol-defs} +\end{figure} + + +\section{Rules of inference} +Figure~\ref{chol-rules} shows the inference rules of~\CHOL{}, 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} + +\CHOL{} follows standard practice in higher-order logic: only a few +connectives are taken as primitive, with the remainder defined obscurely +(Fig.\ts\ref{chol-defs}). Gordon's {\sc hol} system expresses the +corresponding definitions \cite[page~270]{mgordon-hol} using +object-equality~({\tt=}), which is possible because equality in +higher-order logic may equate formulae and even functions over formulae. +But theory~\CHOL{}, like all other Isabelle theories, uses +meta-equality~({\tt==}) for definitions. + +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}. + +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} +\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} x=y ==> f x=f y +\tdx{fun_cong} f=g ==> f x=g x +\subcaption{Equality} + +\tdx{TrueI} True +\tdx{FalseE} False ==> P + +\tdx{conjI} [| P; Q |] ==> P&Q +\tdx{conjunct1} [| P&Q |] ==> P +\tdx{conjunct2} [| P&Q |] ==> Q +\tdx{conjE} [| P&Q; [| P; Q |] ==> R |] ==> R + +\tdx{disjI1} P ==> P|Q +\tdx{disjI2} Q ==> P|Q +\tdx{disjE} [| P | Q; P ==> R; Q ==> R |] ==> R + +\tdx{notI} (P ==> False) ==> ~ P +\tdx{notE} [| ~ P; P |] ==> R +\tdx{impE} [| P-->Q; P; Q ==> R |] ==> R +\subcaption{Propositional logic} + +\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 + +\tdx{eqTrueI} P ==> P=True +\tdx{eqTrueE} P=True ==> P +\subcaption{Logical equivalence} + +\end{ttbox} +\caption{Derived rules for \CHOL} \label{chol-lemmas1} +\end{figure} + + +\begin{figure} +\begin{ttbox}\makeatother +\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 + +\tdx{exI} P x ==> ? x::'a.P x +\tdx{exE} [| ? x::'a.P x; !!x. P x ==> Q |] ==> Q + +\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 + +\tdx{select_equality} [| P a; !!x. P x ==> x=a |] ==> (@x.P x) = a +\subcaption{Quantifiers and descriptions} + +\tdx{ccontr} (~P ==> False) ==> P +\tdx{classical} (~P ==> P) ==> P +\tdx{excluded_middle} ~P | P + +\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} + +\tdx{if_True} if True then x else y = x +\tdx{if_False} if False then x else y = y +\tdx{if_P} P ==> if P then x else y = x +\tdx{if_not_P} ~ P ==> if P then x else y = y +\tdx{expand_if} P(if Q then x else y) = ((Q --> P x) & (~Q --> P y)) +\subcaption{Conditionals} +\end{ttbox} +\caption{More derived rules} \label{chol-lemmas2} +\end{figure} + + +Some derived rules are shown in Figures~\ref{chol-lemmas1} +and~\ref{chol-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: \tdx{ssubst} performs substitution in +backward proofs, while \tdx{box_equals} supports reasoning by +simplifying both sides of an equation. + + +\begin{figure} +\begin{center} +\begin{tabular}{rrr} + \it name &\it meta-type & \it description \\ +\index{{}@\verb'{}' symbol} + \verb|{}| & $\alpha\,set$ & the empty set \\ + \cdx{insert} & $[\alpha,\alpha\,set]\To \alpha\,set$ + & insertion of element \\ + \cdx{Collect} & $(\alpha\To bool)\To\alpha\,set$ + & comprehension \\ + \cdx{Compl} & $(\alpha\,set)\To\alpha\,set$ + & complement \\ + \cdx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$ + & intersection over a set\\ + \cdx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$ + & union over a set\\ + \cdx{Inter} & $(\alpha\,set)set\To\alpha\,set$ + &set of sets intersection \\ + \cdx{Union} & $(\alpha\,set)set\To\alpha\,set$ + &set of sets union \\ + \cdx{Pow} & $\alpha\,set \To (\alpha\,set)set$ + & powerset \\[1ex] + \cdx{range} & $(\alpha\To\beta )\To\beta\,set$ + & range of a function \\[1ex] + \cdx{Ball}~~\cdx{Bex} & $[\alpha\,set,\alpha\To bool]\To bool$ + & bounded quantifiers \\ + \cdx{mono} & $(\alpha\,set\To\beta\,set)\To bool$ + & monotonicity \\ + \cdx{inj}~~\cdx{surj}& $(\alpha\To\beta )\To bool$ + & injective/surjective \\ + \cdx{inj_onto} & $[\alpha\To\beta ,\alpha\,set]\To bool$ + & injective over subset +\end{tabular} +\end{center} +\subcaption{Constants} + +\begin{center} +\begin{tabular}{llrrr} + \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\\ + \sdx{UN} & \cdx{UNION1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 & + union over a type +\end{tabular} +\end{center} +\subcaption{Binders} + +\begin{center} +\index{*"`"` symbol} +\index{*": symbol} +\index{*"<"= symbol} +\begin{tabular}{rrrr} + \it symbol & \it meta-type & \it priority & \it description \\ + \tt `` & $[\alpha\To\beta ,\alpha\,set]\To (\beta\,set)$ + & Left 90 & image \\ + \sdx{Int} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$ + & Left 70 & intersection ($\inter$) \\ + \sdx{Un} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$ + & Left 65 & union ($\union$) \\ + \tt: & $[\alpha ,\alpha\,set]\To bool$ + & Left 50 & membership ($\in$) \\ + \tt <= & $[\alpha\,set,\alpha\,set]\To bool$ + & Left 50 & subset ($\subseteq$) +\end{tabular} +\end{center} +\subcaption{Infixes} +\caption{Syntax of the theory {\tt Set}} \label{chol-set-syntax} +\end{figure} + + +\begin{figure} +\begin{center} \tt\frenchspacing +\index{*"! symbol} +\begin{tabular}{rrr} + \it external & \it internal & \it description \\ + $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 \\ + \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$ \\ + \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}{rclcl} + term & = & \hbox{other terms\ldots} \\ + & | & "\{\}" \\ + & | & "\{ " term\; ("," term)^* " \}" \\ + & | & "\{ " id " . " formula " \}" \\ + & | & term " `` " term \\ + & | & term " Int " term \\ + & | & term " Un " term \\ + & | & "INT~~" id ":" term " . " term \\ + & | & "UN~~~" id ":" term " . " term \\ + & | & "INT~~" id~id^* " . " term \\ + & | & "UN~~~" id~id^* " . " term \\[2ex] + formula & = & \hbox{other formulae\ldots} \\ + & | & term " : " term \\ + & | & term " \ttilde: " term \\ + & | & term " <= " term \\ + & | & "!~" id ":" term " . " formula + & | & "ALL " id ":" term " . " formula \\ + & | & "?~" id ":" term " . " formula + & | & "EX~~" id ":" term " . " formula + \end{array} +\] +\subcaption{Full Grammar} +\caption{Syntax of the theory {\tt Set} (continued)} \label{chol-set-syntax2} +\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 +{\bf sets}, but note that these sets are distinct from those of {\ZF} set +theory, and behave more like {\ZF} classes. +\begin{itemize} +\item +Sets are given by predicates over some type~$\sigma$. Types serve to +define universes for sets, but type checking is still significant. +\item +There is a universal set (for each type). Thus, sets have complements, and +may be defined by absolute comprehension. +\item +Although sets may contain other sets as elements, the containing set must +have a more complex type. +\end{itemize} +Finite unions and intersections have the same behaviour in \CHOL\ as they +do in~{\ZF}. In \CHOL\ the intersection of the empty set is well-defined, +denoting the universal set for the given type. + + +\subsection{Syntax of set theory}\index{*set type} +\CHOL'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{CHOL-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{chol-set-syntax} lists the constants, infixes, and syntax +translations. Figure~\ref{chol-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 +$\neg(a\in b)$. + +The {\tt\{\ldots\}} notation abbreviates finite sets constructed in the +obvious manner using~{\tt insert} and~$\{\}$: +\begin{eqnarray*} + \{a@1, \ldots, a@n\} & \equiv & + {\tt insert}~a@1~({\tt insert}\ldots({\tt insert}~a@n~\{\})\ldots) +\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 \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{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~\cdx{Ball} and~\cdx{Bex} are defined +accordingly. Instead of {\tt Ball $A$ $P$} and {\tt Bex $A$ $P$} we may +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 +\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 + +\tdx{empty_def} \{\} == \{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{Pow_def} Pow A == \{B. B <= A\} +\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{chol-set-rules} +\end{figure} + + +\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_trans} [| A<=B; B<=C |] ==> A<=C + +\tdx{equalityI} [| A <= B; B <= A |] ==> 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{chol-set1} +\end{figure} + + +\begin{figure} \underscoreon +\begin{ttbox} +\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 + +\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 + +\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 + +\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 + +\tdx{PowI} A<=B ==> A: Pow B +\tdx{PowD} A: Pow B ==> A<=B +\end{ttbox} +\caption{Further derived rules for set theory} \label{chol-set2} +\end{figure} + + +\subsection{Axioms and rules of set theory} +Figure~\ref{chol-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. + +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 + +%\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 + +\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 +\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{chol-fun} +\end{figure} + + +\begin{figure} \underscoreon +\begin{ttbox} +\tdx{Union_upper} B:A ==> B <= Union A +\tdx{Union_least} [| !!X. X:A ==> X<=C |] ==> Union A <= C + +\tdx{Inter_lower} B:A ==> Inter A <= B +\tdx{Inter_greatest} [| !!X. X:A ==> C<=X |] ==> C <= Inter A + +\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 + +\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{chol-subset} +\end{figure} + + +\begin{figure} \underscoreon \hfuzz=4pt%suppress "Overfull \hbox" message +\begin{ttbox} +\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) + +\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) + +\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) + +\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) + +\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{chol-equalities} +\end{figure} + + +Figures~\ref{chol-set1} and~\ref{chol-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 CHOL/Set.ML} for +proofs pertaining to set theory. + +Figure~\ref{chol-fun} presents derived inference rules involving functions. +They also include rules for \cdx{Inv}, which is defined in theory~{\tt + CHOL}; 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 CHOL/fun.ML} for a complete listing of the derived rules. + +Figure~\ref{chol-subset} presents lattice properties of the subset relation. +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 CHOL/subset.ML}. + +Figure~\ref{chol-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 CHOL/equalities.ML}. + + +\begin{figure} +\begin{constants} + \it symbol & \it meta-type & & \it description \\ + \cdx{Pair} & $[\alpha,\beta]\To \alpha\times\beta$ + & & ordered pairs $(a,b)$ \\ + \cdx{fst} & $\alpha\times\beta \To \alpha$ & & first projection\\ + \cdx{snd} & $\alpha\times\beta \To \beta$ & & second projection\\ + \cdx{split} & $[[\alpha,\beta]\To\gamma, \alpha\times\beta] \To \gamma$ + & & generalized projection\\ + \cdx{Sigma} & + $[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ & + & general sum of sets +\end{constants} +\begin{ttbox}\makeatletter +\tdx{fst_def} fst p == @a. ? b. p = (a,b) +\tdx{snd_def} snd p == @b. ? a. p = (a,b) +\tdx{split_def} split c p == c (fst p) (snd p) +\tdx{Sigma_def} Sigma A B == UN x:A. UN y:B x. \{(x,y)\} + + +\tdx{Pair_inject} [| (a, b) = (a',b'); [| a=a'; b=b' |] ==> R |] ==> R +\tdx{fst_conv} fst (a,b) = a +\tdx{snd_conv} snd (a,b) = b +\tdx{split} split c (a,b) = c a b + +\tdx{surjective_pairing} p = (fst p,snd p) + +\tdx{SigmaI} [| a:A; b:B a |] ==> (a,b) : Sigma A B + +\tdx{SigmaE} [| c: Sigma A B; + !!x y.[| x:A; y:B x; c=(x,y) |] ==> P |] ==> P +\end{ttbox} +\caption{Type $\alpha\times\beta$}\label{chol-prod} +\end{figure} + + +\begin{figure} +\begin{constants} + \it symbol & \it meta-type & & \it description \\ + \cdx{Inl} & $\alpha \To \alpha+\beta$ & & first injection\\ + \cdx{Inr} & $\beta \To \alpha+\beta$ & & second injection\\ + \cdx{sum_case} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$ + & & conditional +\end{constants} +\begin{ttbox}\makeatletter +\tdx{sum_case_def} sum_case == (\%f g p. @z. (!x. p=Inl x --> z=f x) & + (!y. p=Inr y --> z=g y)) + +\tdx{Inl_not_Inr} ~ Inl a=Inr b + +\tdx{inj_Inl} inj Inl +\tdx{inj_Inr} inj Inr + +\tdx{sumE} [| !!x::'a. P(Inl x); !!y::'b. P(Inr y) |] ==> P s + +\tdx{sum_case_Inl} sum_case f g (Inl x) = f x +\tdx{sum_case_Inr} sum_case f g (Inr x) = g x + +\tdx{surjective_sum} sum_case (\%x::'a. f(Inl x)) (\%y::'b. f(Inr y)) s = f s +\end{ttbox} +\caption{Type $\alpha+\beta$}\label{chol-sum} +\end{figure} + + +\section{Generic packages and classical reasoning} +\CHOL\ instantiates most of Isabelle's generic packages; +see {\tt CHOL/ROOT.ML} for details. +\begin{itemize} +\item +Because it includes a general substitution rule, \CHOL\ instantiates the +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 +simplification set for higher-order logic. Equality~($=$), which also +expresses logical equivalence, may be used for rewriting. See the file +{\tt CHOL/simpdata.ML} for a complete listing of the simplification +rules. +\item +It instantiates the classical reasoner, as described below. +\end{itemize} +\CHOL\ derives classical introduction rules for $\disj$ and~$\exists$, as +well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap +rule; recall Fig.\ts\ref{chol-lemmas2} above. + +The classical reasoner is set up 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: +\begin{ttbox} +prop_cs : claset +HOL_cs : claset +set_cs : claset +\end{ttbox} +\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~{\tt refl}. + +\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{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 \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% + {Chap.\ts\ref{chap:classical}} +for more discussion of classical proof methods. + + +\section{Types} +The basic higher-order logic is augmented with a tremendous amount of +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 by 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}\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{chol-prod} and~\ref{chol-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 \tdx{select_equality}. + +\begin{figure} +\index{*"< symbol} +\index{*"* symbol} +\index{*div symbol} +\index{*mod 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} & $[\alpha, nat\To\alpha, nat] \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 div & $[nat,nat]\To nat$ & Left 70 & division\\ + \tt mod & $[nat,nat]\To nat$ & Left 70 & modulus\\ + \tt + & $[nat,nat]\To nat$ & Left 65 & addition\\ + \tt - & $[nat,nat]\To nat$ & Left 65 & subtraction +\end{constants} +\subcaption{Constants and infixes} + +\begin{ttbox}\makeatother +\tdx{nat_case_def} nat_case == (\%a f n. @z. (n=0 --> z=a) & + (!x. n=Suc x --> z=f x)) +\tdx{pred_nat_def} pred_nat == \{p. ? n. p = (n, Suc n)\} +\tdx{less_def} m P(Suc k) |] ==> P n + +\tdx{Suc_not_Zero} Suc m ~= 0 +\tdx{inj_Suc} inj Suc +\tdx{n_not_Suc_n} n~=Suc n +\subcaption{Basic properties} + +\tdx{pred_natI} (n, Suc n) : pred_nat +\tdx{pred_natE} + [| p : pred_nat; !!x n. [| p = (n, Suc n) |] ==> R |] ==> R + +\tdx{nat_case_0} nat_case a f 0 = a +\tdx{nat_case_Suc} nat_case a f (Suc k) = f k + +\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} + +\tdx{less_trans} [| i i ~ m P m |] ==> P n |] ==> P n + +\tdx{less_linear} m P x#xs) |] ==> P l + +\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 theory \thydx{List}} \label{chol-list} +\end{figure} + +\begin{figure} +\begin{ttbox}\makeatother +\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 c h x#xs = 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 then True else x mem ys + +\tdx{filter_Nil} filter P [] = [] +\tdx{filter_Cons} filter P x#xs = if P x then x#filter P xs else 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{chol-list-simps} +\end{figure} + + +\subsection{The type constructor for lists, {\tt list}} +\index{*list type} + +\CHOL's definition of lists is an example of an experimental method for +handling recursive data types. Figure~\ref{chol-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: +{\dquotes +\begin{eqnarray*} + \begin{array}{r@{\;}l@{}l} + "case " e " of" & "[]" & " => " a\\ + "|" & x"\#"xs & " => " b + \end{array} + & \equiv & + "list_case"~a~(\lambda x\;xs.b)~e +\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{chol-list-simps}. + +The tactic {\tt\ttindex{list_ind_tac} "$xs$" $i$} performs induction over the +variable~$xs$ in subgoal~$i$. + + +\section{Datatype declarations} +\index{*datatype|(} + +\underscoreon + +It is often necessary to extend a theory with \ML-like datatypes. This +extension consists of the new type, declarations of its constructors and +rules that describe the new type. The theory definition section {\tt + datatype} represents a compact way of doing this. + + +\subsection{Foundations} + +A datatype declaration has the following general structure: +\[ \mbox{\tt datatype}~ (\alpha_1,\dots,\alpha_n)t ~=~ + C_1~\tau_{11}~\dots~\tau_{1k_1} ~\mid~ \dots ~\mid~ + C_m~\tau_{m1}~\dots~\tau_{mk_m} +\] +where $\alpha_i$ are type variables, $C_i$ are distinct constructor names and +$\tau_{ij}$ are one of the following: +\begin{itemize} +\item type variables $\alpha_1,\dots,\alpha_n$, +\item types $(\beta_1,\dots,\beta_l)s$ where $s$ is a previously declared + type or type synonym and $\{\beta_1,\dots,\beta_l\} \subseteq + \{\alpha_1,\dots,\alpha_n\}$, +\item the newly defined type $(\alpha_1,\dots,\alpha_n)t$ \footnote{This + makes it a recursive type. To ensure that the new type is not empty at + least one constructor must consist of only non-recursive type + components.} +\end{itemize} +If you would like one of the $\tau_{ij}$ to be a complex type expression +$\tau$ you need to declare a new type synonym $syn = \tau$ first and use +$syn$ in place of $\tau$. Of course this does not work if $\tau$ mentions the +recursive type itself, thus ruling out problematic cases like \[ \mbox{\tt + datatype}~ t ~=~ C(t \To t) \] together with unproblematic ones like \[ +\mbox{\tt datatype}~ t ~=~ C(t~list). \] + +The constructors are automatically defined as functions of their respective +type: +\[ C_j : [\tau_{j1},\dots,\tau_{jk_j}] \To (\alpha_1,\dots,\alpha_n)t \] +These functions have certain {\em freeness} properties: +\begin{description} +\item[\tt distinct] They are distinct: +\[ C_i~x_1~\dots~x_{k_i} \neq C_j~y_1~\dots~y_{k_j} \qquad + \mbox{for all}~ i \neq j. +\] +\item[\tt inject] They are injective: +\[ (C_j~x_1~\dots~x_{k_j} = C_j~y_1~\dots~y_{k_j}) = + (x_1 = y_1 \land \dots \land x_{k_j} = y_{k_j}) +\] +\end{description} +Because the number of inequalities is quadratic in the number of +constructors, a different method is used if their number exceeds +a certain value, currently 4. In that case every constructor is mapped to a +natural number +\[ +\begin{array}{lcl} +\mbox{\it t\_ord}(C_1~x_1~\dots~x_{k_1}) & = & 0 \\ +& \vdots & \\ +\mbox{\it t\_ord}(C_m x_1~\dots~x_{k_m}) & = & m-1 +\end{array} +\] +and distinctness of constructors is expressed by: +\[ +\mbox{\it t\_ord}~x \neq \mbox{\it t\_ord}~y \Imp x \neq y. +\] +In addition a structural induction axiom {\tt induct} is provided: +\[ +\infer{P x} +{\begin{array}{lcl} +\Forall x_1\dots x_{k_1}. + \List{P~x_{r_{11}}; \dots; P~x_{r_{1l_1}}} & + \Imp & P(C_1~x_1~\dots~x_{k_1}) \\ + & \vdots & \\ +\Forall x_1\dots x_{k_m}. + \List{P~x_{r_{m1}}; \dots; P~x_{r_{ml_m}}} & + \Imp & P(C_m~x_1~\dots~x_{k_m}) +\end{array}} +\] +where $\{r_{j1},\dots,r_{jl_j}\} = \{i \in \{1,\dots k_j\} ~\mid~ \tau_{ji} += (\alpha_1,\dots,\alpha_n)t \}$, i.e.\ the property $P$ can be assumed for +all arguments of the recursive type. + +The type also comes with an \ML-like \sdx{case}-construct: +\[ +\begin{array}{rrcl} +\mbox{\tt case}~e~\mbox{\tt of} & C_1~x_{11}~\dots~x_{1k_1} & \To & e_1 \\ + \vdots \\ + \mid & C_m~x_{m1}~\dots~x_{mk_m} & \To & e_m +\end{array} +\] +In contrast to \ML, {\em all} constructors must be present, their order is +fixed, and nested patterns are not supported. + + +\subsection{Defining datatypes} + +A datatype is defined in a theory definition file using the keyword {\tt + datatype}. The definition following {\tt datatype} must conform to the +syntax of {\em typedecl} specified in Fig.~\ref{datatype-grammar} and must +obey the rules in the previous section. As a result the theory is extended +with the new type, the constructors, and the theorems listed in the previous +section. + +\begin{figure} +\begin{rail} +typedecl : typevarlist id '=' (cons + '|') + ; +cons : (id | string) ( () | '(' (typ + ',') ')' ) ( () | mixfix ) + ; +typ : typevarlist id + | tid + ; +typevarlist : () | tid | '(' (tid + ',') ')' + ; +\end{rail} +\caption{Syntax of datatype declarations} +\label{datatype-grammar} +\end{figure} + +Reading the theory file produces a structure which, in addition to the usual +components, contains a structure named $t$ for each datatype $t$ defined in +the file.\footnote{Otherwise multiple datatypes in the same theory file would + lead to name clashes.} Each structure $t$ contains the following elements: +\begin{ttbox} +val distinct : thm list +val inject : thm list +val induct : thm +val cases : thm list +val simps : thm list +val induct_tac : string -> int -> tactic +\end{ttbox} +{\tt distinct}, {\tt inject} and {\tt induct} contain the theorems described +above. For convenience {\tt distinct} contains inequalities in both +directions. +\begin{warn} + If there are five or more constructors, the {\em t\_ord} scheme is used for + {\tt distinct}. In this case the theory {\tt Arith} must be contained + in the current theory, if necessary by including it explicitly. +\end{warn} +The reduction rules of the {\tt case}-construct are in {\tt cases}. All +theorems from {\tt distinct}, {\tt inject} and {\tt cases} are combined in +{\tt simps} for use with the simplifier. The tactic {\verb$induct_tac$~{\em + var i}\/} applies structural induction over variable {\em var} to +subgoal {\em i}. + + +\subsection{Examples} + +\subsubsection{The datatype $\alpha~list$} + +We want to define the type $\alpha~list$.\footnote{Of course there is a list + type in CHOL already. This is only an example.} To do this we have to build +a new theory that contains the type definition. We start from {\tt CHOL}. +\begin{ttbox} +MyList = CHOL + + datatype 'a list = Nil | Cons 'a ('a list) +end +\end{ttbox} +After loading the theory (\verb$use_thy "MyList"$), we can prove +$Cons~x~xs\neq xs$. First we build a suitable simpset for the simplifier: +\begin{ttbox} +val mylist_ss = HOL_ss addsimps MyList.list.simps; +goal MyList.thy "!x. Cons x xs ~= xs"; +{\out Level 0} +{\out ! x. Cons x xs ~= xs} +{\out 1. ! x. Cons x xs ~= xs} +\end{ttbox} +This can be proved by the structural induction tactic: +\begin{ttbox} +by (MyList.list.induct_tac "xs" 1); +{\out Level 1} +{\out ! x. Cons x xs ~= xs} +{\out 1. ! x. Cons x Nil ~= Nil} +{\out 2. !!a list.} +{\out ! x. Cons x list ~= list ==>} +{\out ! x. Cons x (Cons a list) ~= Cons a list} +\end{ttbox} +The first subgoal can be proved with the simplifier and the distinctness +axioms which are part of \verb$mylist_ss$. +\begin{ttbox} +by (simp_tac mylist_ss 1); +{\out Level 2} +{\out ! x. Cons x xs ~= xs} +{\out 1. !!a list.} +{\out ! x. Cons x list ~= list ==>} +{\out ! x. Cons x (Cons a list) ~= Cons a list} +\end{ttbox} +Using the freeness axioms we can quickly prove the remaining goal. +\begin{ttbox} +by (asm_simp_tac mylist_ss 1); +{\out Level 3} +{\out ! x. Cons x xs ~= xs} +{\out No subgoals!} +\end{ttbox} +Because both subgoals were proved by almost the same tactic we could have +done that in one step using +\begin{ttbox} +by (ALLGOALS (asm_simp_tac mylist_ss)); +\end{ttbox} + + +\subsubsection{The datatype $\alpha~list$ with mixfix syntax} + +In this example we define the type $\alpha~list$ again but this time we want +to write {\tt []} instead of {\tt Nil} and we want to use the infix operator +\verb|#| instead of {\tt Cons}. To do this we simply add mixfix annotations +after the constructor declarations as follows: +\begin{ttbox} +MyList = CHOL + + datatype 'a list = "[]" ("[]") + | "#" 'a ('a list) (infixr 70) +end +\end{ttbox} +Now the theorem in the previous example can be written \verb|x#xs ~= xs|. The +proof is the same. + + +\subsubsection{A datatype for weekdays} + +This example shows a datatype that consists of more than four constructors: +\begin{ttbox} +Days = Arith + + datatype days = Mo | Tu | We | Th | Fr | Sa | So +end +\end{ttbox} +Because there are more than four constructors, the theory must be based on +{\tt Arith}. Inequality is defined via a function \verb|days_ord|. Although +the expression \verb|Mo ~= Tu| is not directly contained in {\tt distinct}, +it can be proved by the simplifier if \verb$arith_ss$ is used: +\begin{ttbox} +val days_ss = arith_ss addsimps Days.days.simps; + +goal Days.thy "Mo ~= Tu"; +by (simp_tac days_ss 1); +\end{ttbox} +Note that usually it is not necessary to derive these inequalities explicitly +because the simplifier will dispose of them automatically. + +\subsection{Primitive recursive functions} +\index{primitive recursion|(} +\index{*primrec|(} + +Datatypes come with a uniform way of defining functions, {\bf primitive + recursion}. Although it is possible to define primitive recursive functions +by asserting their reduction rules as new axioms, e.g.\ +\begin{ttbox} +Append = MyList + +consts app :: "['a list,'a list] => 'a list" +rules + app_Nil "app [] ys = ys" + app_Cons "app x#xs ys = x#app xs ys" +end +\end{ttbox} +this carries with it the danger of accidentally asserting an inconsistency, +as in \verb$app [] ys = us$. Therefore primitive recursive functions on +datatypes can be defined with a special syntax: +\begin{ttbox} +Append = MyList + +consts app :: "'['a list,'a list] => 'a list" +primrec app MyList.list + app_Nil "app [] ys = ys" + app_Cons "app x#xs ys = x#app xs ys" +end +\end{ttbox} +The system will now check that the two rules \verb$app_Nil$ and +\verb$app_Cons$ do indeed form a primitive recursive definition, thus +ensuring that consistency is maintained. For example +\begin{ttbox} +primrec app MyList.list + app_Nil "app [] ys = us" +\end{ttbox} +is rejected: +\begin{ttbox} +Extra variables on rhs +\end{ttbox} +\bigskip + +The general form of a primitive recursive definition is +\begin{ttbox} +primrec {\it function} {\it type} + {\it reduction rules} +\end{ttbox} +where +\begin{itemize} +\item {\it function} is the name of the function, either as an {\it id} or a + {\it string}. The function must already have been declared. +\item {\it type} is the name of the datatype, either as an {\it id} or in the + long form {\it Thy.t}, where {\it Thy} is the name of the parent theory the + datatype was declared in, and $t$ the name of the datatype. The long form + is required if the {\tt datatype} and the {\tt primrec} sections are in + different theories. +\item {\it reduction rules} specify one or more named equations of the form + {\it id\/}~{\it string}, where the identifier gives the name of the rule in + the result structure, and {\it string} is a reduction rule of the form \[ + f~x_1~\dots~x_m~(C~y_1~\dots~y_k)~z_1~\dots~z_n = r \] such that $C$ is a + constructor of the datatype, $r$ contains only the free variables on the + left-hand side, and all recursive calls in $r$ are of the form + $f~\dots~y_i~\dots$ for some $i$. There must be exactly one reduction + rule for each constructor. +\end{itemize} +A theory file may contain any number of {\tt primrec} sections which may be +intermixed with other declarations. + +For the consistency-sensitive user it may be reassuring to know that {\tt + primrec} does not assert the reduction rules as new axioms but derives them +as theorems from an explicit definition of the recursive function in terms of +a recursion operator on the datatype. + +The primitive recursive function can also use infix or mixfix syntax: +\begin{ttbox} +Append = MyList + +consts "@" :: "['a list,'a list] => 'a list" (infixr 60) +primrec "op @" MyList.list + app_Nil "[] @ ys = ys" + app_Cons "(x#xs) @ ys = x#(xs @ ys)" +end +\end{ttbox} + +The reduction rules become part of the ML structure \verb$Append$ and can +be used to prove theorems about the function: +\begin{ttbox} +val append_ss = HOL_ss addsimps [Append.app_Nil,Append.app_Cons]; + +goal Append.thy "(xs @ ys) @ zs = xs @ (ys @ zs)"; +by (MyList.list.induct_tac "xs" 1); +by (ALLGOALS(asm_simp_tac append_ss)); +\end{ttbox} + +%Note that underdefined primitive recursive functions are allowed: +%\begin{ttbox} +%Tl = MyList + +%consts tl :: "'a list => 'a list" +%primrec tl MyList.list +% tl_Cons "tl(x#xs) = xs" +%end +%\end{ttbox} +%Nevertheless {\tt tl} is total, although we do not know what the result of +%\verb$tl([])$ is. + +\index{primitive recursion|)} +\index{*primrec|)} +\index{*datatype|)} + + +\section{Inductive and coinductive definitions} +\index{*inductive|(} +\index{*coinductive|(} + +An {\bf inductive definition} specifies the least set closed under given +rules. For example, a structural operational semantics is an inductive +definition of an evaluation relation. Dually, a {\bf coinductive + definition} specifies the greatest set closed under given rules. An +important example is using bisimulation relations to formalize equivalence +of processes and infinite data structures. + +A theory file may contain any number of inductive and coinductive +definitions. They may be intermixed with other declarations; in +particular, the (co)inductive sets {\bf must} be declared separately as +constants, and may have mixfix syntax or be subject to syntax translations. + +Each (co)inductive definition adds definitions to the theory and also +proves some theorems. Each definition creates an ML structure, which is a +substructure of the main theory structure. + +This package is derived from the ZF one, described in a +separate paper,\footnote{It appeared in CADE~\cite{paulson-CADE} and a + longer version is distributed with Isabelle.} which you should refer to +in case of difficulties. The package is simpler than ZF's, thanks to CHOL's +automatic type-checking. The type of the (co)inductive determines the +domain of the fixedpoint definition, and the package does not use inference +rules for type-checking. + + +\subsection{The result structure} +Many of the result structure's components have been discussed in the paper; +others are self-explanatory. +\begin{description} +\item[\tt thy] is the new theory containing the recursive sets. + +\item[\tt defs] is the list of definitions of the recursive sets. + +\item[\tt mono] is a monotonicity theorem for the fixedpoint operator. + +\item[\tt unfold] is a fixedpoint equation for the recursive set (the union of +the recursive sets, in the case of mutual recursion). + +\item[\tt intrs] is the list of introduction rules, now proved as theorems, for +the recursive sets. The rules are also available individually, using the +names given them in the theory file. + +\item[\tt elim] is the elimination rule. + +\item[\tt mk\_cases] is a function to create simplified instances of {\tt +elim}, using freeness reasoning on some underlying datatype. +\end{description} + +For an inductive definition, the result structure contains two induction rules, +{\tt induct} and \verb|mutual_induct|. For a coinductive definition, it +contains the rule \verb|coinduct|. + +Figure~\ref{def-result-fig} summarizes the two result signatures, +specifying the types of all these components. + +\begin{figure} +\begin{ttbox} +sig +val thy : theory +val defs : thm list +val mono : thm +val unfold : thm +val intrs : thm list +val elim : thm +val mk_cases : thm list -> string -> thm +{\it(Inductive definitions only)} +val induct : thm +val mutual_induct: thm +{\it(Coinductive definitions only)} +val coinduct : thm +end +\end{ttbox} +\hrule +\caption{The result of a (co)inductive definition} \label{def-result-fig} +\end{figure} + +\subsection{The syntax of a (co)inductive definition} +An inductive definition has the form +\begin{ttbox} +inductive {\it inductive sets} + intrs {\it introduction rules} + monos {\it monotonicity theorems} + con_defs {\it constructor definitions} +\end{ttbox} +A coinductive definition is identical, except that it starts with the keyword +{\tt coinductive}. + +The {\tt monos} and {\tt con\_defs} sections are optional. If present, +each is specified as a string, which must be a valid ML expression of type +{\tt thm list}. It is simply inserted into the {\tt .thy.ML} file; if it +is ill-formed, it will trigger ML error messages. You can then inspect the +file on your directory. + +\begin{itemize} +\item The {\it inductive sets} are specified by one or more strings. + +\item The {\it introduction rules} specify one or more introduction rules in + the form {\it ident\/}~{\it string}, where the identifier gives the name of + the rule in the result structure. + +\item The {\it monotonicity theorems} are required for each operator + applied to a recursive set in the introduction rules. There {\bf must} + be a theorem of the form $A\subseteq B\Imp M(A)\subseteq M(B)$, for each + premise $t\in M(R_i)$ in an introduction rule! + +\item The {\it constructor definitions} contain definitions of constants + appearing in the introduction rules. In most cases it can be omitted. +\end{itemize} + +The package has a few notable restrictions: +\begin{itemize} +\item The theory must separately declare the recursive sets as + constants. + +\item The names of the recursive sets must be identifiers, not infix +operators. + +\item Side-conditions must not be conjunctions. However, an introduction rule +may contain any number of side-conditions. + +\item Side-conditions of the form $x=t$, where the variable~$x$ does not + occur in~$t$, will be substituted through the rule \verb|mutual_induct|. +\end{itemize} + + +\subsection{Example of an inductive definition} +Two declarations, included in a theory file, define the finite powerset +operator. First we declare the constant~{\tt Fin}. Then we declare it +inductively, with two introduction rules: +\begin{ttbox} +consts Fin :: "'a set => 'a set set" +inductive "Fin A" + intrs + emptyI "{} : Fin A" + insertI "[| a: A; b: Fin A |] ==> insert a b : Fin A" +\end{ttbox} +The resulting theory structure contains a substructure, called~{\tt Fin}. +It contains the {\tt Fin}$~A$ introduction rules as the list {\tt Fin.intrs}, +and also individually as {\tt Fin.emptyI} and {\tt Fin.consI}. The induction +rule is {\tt Fin.induct}. + +For another example, here is a theory file defining the accessible part of a +relation. The main thing to note is the use of~{\tt Pow} in the sole +introduction rule, and the corresponding mention of the rule +\verb|Pow_mono| in the {\tt monos} list. The paper discusses a ZF version +of this example in more detail. +\begin{ttbox} +Acc = WF + +consts pred :: "['b, ('a * 'b)set] => 'a set" (*Set of predecessors*) + acc :: "('a * 'a)set => 'a set" (*Accessible part*) +defs pred_def "pred x r == {y. (y,x):r}" +inductive "acc r" + intrs + pred "pred a r: Pow(acc r) ==> a: acc r" + monos "[Pow_mono]" +end +\end{ttbox} +The CHOL distribution contains many other inductive definitions, such as the +theory {\tt CHOL/ex/PropLog.thy} and the directory {\tt CHOL/IMP}. The +theory {\tt CHOL/ex/LList.thy} contains coinductive definitions. + +\index{*coinductive|)} \index{*inductive|)} \underscoreoff + + +\section{The examples directories} +Directory {\tt CHOL/Subst} contains Martin Coen's mechanisation of a theory of +substitutions and unifiers. It is based on Paulson's previous +mechanisation in {\LCF}~\cite{paulson85} of Manna and Waldinger's +theory~\cite{mw81}. + +Directory {\tt CHOL/IMP} contains a mechanised version of a semantic +equivalence proof taken from Winskel~\cite{winskel93}. It formalises the +denotational and operational semantics of a simple while-language, then +proves the two equivalent. It contains several datatype and inductive +definitions, and demonstrates their use. + +Directory {\tt CHOL/ex} contains other examples and experimental proofs in +{\CHOL}. Here is an overview of the more interesting files. +\begin{itemize} +\item File {\tt cla.ML} demonstrates the classical reasoner on over sixty + predicate calculus theorems, ranging from simple tautologies to + moderately difficult problems involving equality and quantifiers. + +\item File {\tt 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 File {\tt mesontest.ML} contains test data for the {\sc meson} proof + procedure. These are mostly taken from Pelletier \cite{pelletier86}. + +\item File {\tt set.ML} proves Cantor's Theorem, which is presented in + \S\ref{sec:chol-cantor} below, and the Schr\"oder-Bernstein Theorem. + +\item Theories {\tt InSort} and {\tt Qsort} prove correctness properties of + insertion sort and quick sort. + +\item The definition of lazy lists demonstrates methods for handling + infinite data structures and coinduction in higher-order + logic~\cite{paulson-coind}. Theory \thydx{LList} 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 coinduction principle is defined + for proving equations on lazy lists. + +\item Theory {\tt PropLog} 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. A similar proof in \ZF{} is + described elsewhere~\cite{paulson-set-II}. + +\item Theory {\tt Term} develops an experimental recursive type definition; + the recursion goes through the type constructor~\tydx{list}. + +\item Theory {\tt Simult} constructs mutually recursive sets of trees and + forests, including induction and recursion rules. + +\item Theory {\tt MT} 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{itemize} + + +\goodbreak +\section{Example: Cantor's Theorem}\label{sec:chol-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 \CHOL'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 \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} +{\out ~ ?S : range f} +{\out 1. ?S : range f ==> False} +\ttbreak +by (eresolve_tac [rangeE] 1); +{\out Level 2} +{\out ~ ?S : range f} +{\out 1. !!x. ?S = f x ==> False} +\end{ttbox} +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} +by (eresolve_tac [equalityCE] 1); +{\out Level 3} +{\out ~ ?S : range f} +{\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 +comprehension. Then $\Var{c}\in\{x.\Var{P}~x\}$ implies +$\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} +{\out ~ \{x. ?P7 x\} : range f} +{\out 1. !!x. [| ?c3 x : f x; ?P7(?c3 x) |] ==> False} +{\out 2. !!x. [| ~ ?c3 x : \{x. ?P7 x\}; ~ ?c3 x : f x |] ==> False} +\end{ttbox} +Forcing a contradiction between the two assumptions of subgoal~1 completes +the instantiation of~$S$. It is now the set $\{x. x\not\in f~x\}$, which +is the standard diagonal construction. +\begin{ttbox} +by (contr_tac 1); +{\out Level 5} +{\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 \tdx{CollectI} to the negated +assumption, we employ \ttindex{swap_res_tac}: +\begin{ttbox} +by (swap_res_tac [CollectI] 1); +{\out Level 6} +{\out ~ \{x. ~ x : f x\} : range f} +{\out 1. !!x. [| ~ x : f x; ~ False |] ==> ~ x : f x} +\ttbreak +by (assume_tac 1); +{\out Level 7} +{\out ~ \{x. ~ x : f x\} : range f} +{\out No subgoals!} +\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 \CHOL'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} +{\out ~ ?S : range f} +{\out 1. ~ ?S : range f} +\ttbreak +by (best_tac (set_cs addSEs [equalityCE]) 1); +{\out Level 1} +{\out ~ \{x. ~ x : f x\} : range f} +{\out No subgoals!} +\end{ttbox} + +\index{higher-order logic|)} diff -r 737a1a0df754 -r dd7284573601 doc-src/Logics/logics.tex --- a/doc-src/Logics/logics.tex Tue May 09 10:42:23 1995 +0200 +++ b/doc-src/Logics/logics.tex Tue May 09 10:43:19 1995 +0200 @@ -47,7 +47,7 @@ \include{intro} \include{FOL} \include{ZF} -\include{HOL} +\include{CHOL} \include{LK} %%\include{Modal} \include{CTT}