# HG changeset patch # User lcp # Date 767265625 -7200 # Node ID 753b50b07c4651c11733cce426a5834cbe88d3be # Parent 8d77f767bd26fd791a38c9c68922c9fd4f0af590 final Springer copy diff -r 8d77f767bd26 -r 753b50b07c46 doc-src/Logics/Old_HOL.tex --- a/doc-src/Logics/Old_HOL.tex Mon Apr 25 11:05:58 1994 +0200 +++ b/doc-src/Logics/Old_HOL.tex Mon Apr 25 11:20:25 1994 +0200 @@ -4,7 +4,7 @@ \index{HOL system@{\sc hol} system} The theory~\thydx{HOL} implements higher-order logic. -It is based on Gordon's~{\sc hol} system~\cite{mgordon88a}, which itself is +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 @@ -167,7 +167,8 @@ 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. +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 @@ -237,21 +238,21 @@ \end{figure} -\begin{figure} +\begin{figure}\hfuzz=4pt%suppress "Overfull \hbox" message \begin{ttbox}\makeatother -\tdx{True_def} True = ((\%x.x)=(\%x.x)) -\tdx{All_def} All = (\%P. P = (\%x.True)) -\tdx{Ex_def} Ex = (\%P. P(@x.P(x))) -\tdx{False_def} False = (!P.P) -\tdx{not_def} not = (\%P. P-->False) -\tdx{and_def} op & = (\%P Q. !R. (P-->Q-->R) --> R) -\tdx{or_def} op | = (\%P Q. !R. (P-->R) --> (Q-->R) --> R) -\tdx{Ex1_def} Ex1 = (\%P. ? x. P(x) & (! y. P(y) --> y=x)) +\tdx{True_def} True == ((\%x.x)=(\%x.x)) +\tdx{All_def} All == (\%P. P = (\%x.True)) +\tdx{Ex_def} Ex == (\%P. P(@x.P(x))) +\tdx{False_def} False == (!P.P) +\tdx{not_def} not == (\%P. P-->False) +\tdx{and_def} op & == (\%P Q. !R. (P-->Q-->R) --> R) +\tdx{or_def} op | == (\%P Q. !R. (P-->R) --> (Q-->R) --> R) +\tdx{Ex1_def} Ex1 == (\%P. ? x. P(x) & (! y. P(y) --> y=x)) -\tdx{Inv_def} Inv = (\%(f::'a=>'b) y. @x. f(x)=y) -\tdx{o_def} op o = (\%(f::'b=>'c) g (x::'a). f(g(x))) -\tdx{if_def} if = (\%P x y.@z::'a.(P=True --> z=x) & (P=False --> z=y)) -\tdx{Let_def} Let(s,f) = f(s) +\tdx{Inv_def} Inv == (\%(f::'a=>'b) y. @x. f(x)=y) +\tdx{o_def} op o == (\%(f::'b=>'c) g (x::'a). f(g(x))) +\tdx{if_def} if == (\%P x y.@z::'a.(P=True --> z=x) & (P=False --> z=y)) +\tdx{Let_def} Let(s,f) == f(s) \end{ttbox} \caption{The {\tt HOL} definitions} \label{hol-defs} \end{figure} @@ -274,17 +275,17 @@ \HOL{} follows standard practice in higher-order logic: only a few connectives are taken as primitive, with the remainder defined obscurely -(Fig.\ts\ref{hol-defs}). Unusually, the definitions are expressed using -object-equality~({\tt=}) rather than meta-equality~({\tt==}). This is -possible because equality in higher-order logic may equate formulae and -even functions over formulae. On the other hand, meta-equality is -Isabelle's usual symbol for making definitions. Take care to note which -form of equality is used before attempting a proof. +(Fig.\ts\ref{hol-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~\HOL{}, 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}. +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, @@ -396,30 +397,6 @@ backward proofs, while \tdx{box_equals} supports reasoning by simplifying both sides of an equation. -See the files {\tt HOL/hol.thy} and -{\tt HOL/hol.ML} for complete listings of the rules and -derived rules. - - -\section{Generic packages} -\HOL\ instantiates most of Isabelle's generic packages; -see {\tt HOL/ROOT.ML} for details. -\begin{itemize} -\item -Because it includes a general substitution rule, \HOL\ 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 HOL/simpdata.ML} for a complete listing of the simplification -rules. -\item -It instantiates the classical reasoning module. See~\S\ref{hol-cla-prover} -for details. -\end{itemize} - \begin{figure} \begin{center} @@ -835,7 +812,7 @@ \tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are not strictly necessary but yield more natural proofs. Similarly, \tdx{equalityCE} supports classical reasoning about extensionality, -after the fashion of \tdx{iffCE}. See the file {\tt HOL/set.ML} for +after the fashion of \tdx{iffCE}. See the file {\tt HOL/Set.ML} for proofs pertaining to set theory. Figure~\ref{hol-fun} presents derived inference rules involving functions. @@ -860,6 +837,7 @@ \begin{figure} \begin{constants} + \it symbol & \it meta-type & & \it description \\ \cdx{Pair} & $[\alpha,\beta]\To \alpha\times\beta$ & & ordered pairs $\langle a,b\rangle$ \\ \cdx{fst} & $\alpha\times\beta \To \alpha$ & & first projection\\ @@ -895,6 +873,7 @@ \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+\beta, \alpha\To\gamma, \beta\To\gamma] \To\gamma$ @@ -920,6 +899,65 @@ \end{figure} +\section{Generic packages and classical reasoning} +\HOL\ instantiates most of Isabelle's generic packages; +see {\tt HOL/ROOT.ML} for details. +\begin{itemize} +\item +Because it includes a general substitution rule, \HOL\ 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 HOL/simpdata.ML} for a complete listing of the simplification +rules. +\item +It instantiates the classical reasoner, as described below. +\end{itemize} +\HOL\ 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{hol-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 +HOL_dup_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{HOL_dup_cs}] extends {\tt prop_cs} with the safe rules + {\tt allI} and~{\tt exE} and the unsafe rules \tdx{all_dupE} + and~\tdx{exCI}, as well as rules for unique existence. Search using + this is complete --- quantified formulae may be duplicated --- but + frequently fails to terminate. It is generally unsuitable for + depth-first search. + +\item[\ttindexbold{set_cs}] extends {\tt HOL_cs} with rules for the bounded + quantifiers, subsets, comprehensions, unions 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 @@ -938,14 +976,13 @@ 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}. See {\tt HOL/prod.thy} and -{\tt HOL/sum.thy} for details. +proved using \tdx{select_equality}. \begin{figure} \index{*"< symbol} \index{*"* symbol} -\index{/@{\tt/} symbol} -\index{//@{\tt//} symbol} +\index{*div symbol} +\index{*mod symbol} \index{*"+ symbol} \index{*"- symbol} \begin{constants} @@ -958,8 +995,8 @@ & & primitive recursor\\ \cdx{pred_nat} & $(nat\times nat) set$ & & predecessor relation\\ \tt * & $[nat,nat]\To nat$ & Left 70 & multiplication \\ - \tt / & $[nat,nat]\To nat$ & Left 70 & division\\ - \tt // & $[nat,nat]\To nat$ & Left 70 & modulus\\ + \tt 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} @@ -967,17 +1004,17 @@ \begin{ttbox}\makeatother \tdx{nat_case_def} nat_case == (\%n a f. @z. (n=0 --> z=a) & - (!x. n=Suc(x) --> z=f(x))) + (!x. n=Suc(x) --> z=f(x))) \tdx{pred_nat_def} pred_nat == \{p. ? n. p = \} \tdx{less_def} m:pred_nat^+ \tdx{nat_rec_def} nat_rec(n,c,d) == wfrec(pred_nat, n, \%l g.nat_case(l, c, \%m.d(m,g(m)))) -\tdx{add_def} m+n == nat_rec(m, n, \%u v.Suc(v)) -\tdx{diff_def} m-n == nat_rec(n, m, \%u v. nat_rec(v, 0, \%x y.x)) -\tdx{mult_def} m*n == nat_rec(m, 0, \%u v. n + v) -\tdx{mod_def} m//n == wfrec(trancl(pred_nat), m, \%j f. if(j " a\\ "|" & x"\#"xs & " => " b \end{array} & \equiv & - "list_case"(e, a, \lambda x\;xs.b[x,xs]) -\end{eqnarray*}} + "list_case"(e, a, \lambda x\;xs.b) +\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. @@ -1186,71 +1222,30 @@ \index{*llist type} The definition of lazy lists demonstrates methods for handling infinite -data structures and coinduction in higher-order logic. It defines an -operator for corecursion on lazy lists, which is used to define a few -simple functions such as map and append. Corecursion cannot easily define -operations such as filter, which can compute indefinitely before yielding -the next element (if any!) of the lazy list. A coinduction principle is -defined for proving equations on lazy lists. See the files {\tt - HOL/llist.thy} and {\tt HOL/llist.ML} for the formal derivations. +data structures and coinduction in higher-order logic. 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. I have written a paper discussing the treatment of lazy lists; it also covers finite lists~\cite{paulson-coind}. -\section{Classical proof procedures} \label{hol-cla-prover} -\HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as -well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap -rule; recall Fig.\ts\ref{hol-lemmas2} above. - -The classical reasoner is set up for \HOL, as the structure -{\tt Classical}. This structure is open, so {\ML} identifiers such -as {\tt step_tac}, {\tt fast_tac}, {\tt best_tac}, etc., refer to it. - -\HOL\ defines the following classical rule sets: -\begin{ttbox} -prop_cs : claset -HOL_cs : claset -HOL_dup_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{HOL_dup_cs}] extends {\tt prop_cs} with the safe rules - {\tt allI} and~{\tt exE} and the unsafe rules \tdx{all_dupE} - and~\tdx{exCI}, as well as rules for unique existence. Search using - this is complete --- quantified formulae may be duplicated --- but - frequently fails to terminate. It is generally unsuitable for - depth-first search. - -\item[\ttindexbold{set_cs}] extends {\tt HOL_cs} with rules for the bounded - quantifiers, subsets, comprehensions, unions 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{The examples directories} -Directory {\tt HOL/Subst} contains Martin Coen's mechanization of a theory of +Directory {\tt HOL/Subst} contains Martin Coen's mechanisation of a theory of substitutions and unifiers. It is based on Paulson's previous -mechanization in {\LCF}~\cite{paulson85} of Manna and Waldinger's +mechanisation in {\LCF}~\cite{paulson85} of Manna and Waldinger's theory~\cite{mw81}. Directory {\tt HOL/ex} contains other examples and experimental proofs in {\HOL}. Here is an overview of the more interesting files. \begin{ttdescription} +\item[HOL/ex/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[HOL/ex/meson.ML] contains an experimental implementation of the {\sc meson} proof procedure, inspired by Plaisted~\cite{plaisted90}. It is much more powerful than Isabelle's classical reasoner. But it is less @@ -1263,24 +1258,25 @@ \item[HOL/ex/set.ML] proves Cantor's Theorem, which is presented in \S\ref{sec:hol-cantor} below, and the Schr\"oder-Bernstein Theorem. -\item[HOL/ex/insort.ML] and {\tt HOL/ex/qsort.ML} contain correctness +\item[HOL/ex/InSort.ML] and {\tt HOL/ex/Qsort.ML} contain correctness proofs about insertion sort and quick sort. -\item[HOL/ex/pl.ML] proves the soundness and completeness of classical +\item[HOL/ex/PL.ML] proves the soundness and completeness of classical propositional logic, given a truth table semantics. The only connective is $\imp$. A Hilbert-style axiom system is specified, and its set of - theorems defined inductively. + theorems defined inductively. A similar proof in \ZF{} is described + elsewhere~\cite{paulson-set-II}. -\item[HOL/ex/term.ML] +\item[HOL/ex/Term.ML] contains proofs about an experimental recursive type definition; the recursion goes through the type constructor~\tydx{list}. -\item[HOL/ex/simult.ML] defines primitives for solving mutually recursive +\item[HOL/ex/Simult.ML] defines primitives for solving mutually recursive equations over sets. It constructs sets of trees and forests as an example, including induction and recursion rules that handle the mutual recursion. -\item[HOL/ex/mt.ML] contains Jacob Frost's formalization~\cite{frost93} of +\item[HOL/ex/MT.ML] contains Jacob Frost's formalization~\cite{frost93} of Milner and Tofte's coinduction example~\cite{milner-coind}. This substantial proof concerns the soundness of a type system for a simple functional language. The semantics of recursion is given by a cyclic @@ -1288,120 +1284,7 @@ \end{ttdescription} -\section{Example: deriving the conjunction rules} -The theory {\HOL} comes with a body of derived rules, ranging from simple -properties of the logical constants and set theory to well-founded -recursion. Many of them are worth studying. - -Deriving natural deduction rules for the logical constants from their -definitions is an archetypal example of higher-order reasoning. Let us -verify two conjunction rules: -\[ \infer[({\conj}I)]{P\conj Q}{P & Q} \qquad\qquad - \infer[({\conj}E1)]{P}{P\conj Q} -\] - -\subsection{The introduction rule} -We begin by stating the rule as the goal. The list of premises $[P,Q]$ is -bound to the {\ML} variable~{\tt prems}. -\begin{ttbox} -val prems = goal HOL.thy "[| P; Q |] ==> P&Q"; -{\out Level 0} -{\out P & Q} -{\out 1. P & Q} -{\out val prems = ["P [P]", "Q [Q]"] : thm list} -\end{ttbox} -The next step is to unfold the definition of conjunction. But -\tdx{and_def} uses \HOL's internal equality, so -\ttindex{rewrite_goals_tac} is unsuitable. -Instead, we perform substitution using the rule \tdx{ssubst}: -\begin{ttbox} -by (resolve_tac [and_def RS ssubst] 1); -{\out Level 1} -{\out P & Q} -{\out 1. ! R. (P --> Q --> R) --> R} -\end{ttbox} -We now apply $(\forall I)$ and $({\imp}I)$: -\begin{ttbox} -by (resolve_tac [allI] 1); -{\out Level 2} -{\out P & Q} -{\out 1. !!R. (P --> Q --> R) --> R} -\ttbreak -by (resolve_tac [impI] 1); -{\out Level 3} -{\out P & Q} -{\out 1. !!R. P --> Q --> R ==> R} -\end{ttbox} -The assumption is a nested implication, which may be eliminated -using~\tdx{mp} resolved with itself. Elim-resolution, here, performs -backwards chaining. More straightforward would be to use~\tdx{impE} -twice. -\index{*RS} -\begin{ttbox} -by (eresolve_tac [mp RS mp] 1); -{\out Level 4} -{\out P & Q} -{\out 1. !!R. P} -{\out 2. !!R. Q} -\end{ttbox} -These two subgoals are simply the premises: -\begin{ttbox} -by (REPEAT (resolve_tac prems 1)); -{\out Level 5} -{\out P & Q} -{\out No subgoals!} -\end{ttbox} - - -\subsection{The elimination rule} -Again, we bind the list of premises (in this case $[P\conj Q]$) -to~{\tt prems}. -\begin{ttbox} -val prems = goal HOL.thy "[| P & Q |] ==> P"; -{\out Level 0} -{\out P} -{\out 1. P} -{\out val prems = ["P & Q [P & Q]"] : thm list} -\end{ttbox} -Working with premises that involve defined constants can be tricky. We -must expand the definition of conjunction in the meta-assumption $P\conj -Q$. The rule \tdx{subst} performs substitution in forward proofs. -We get {\it two\/} resolvents since the vacuous substitution is valid: -\begin{ttbox} -prems RL [and_def RS subst]; -{\out val it = ["! R. (P --> Q --> R) --> R [P & Q]",} -{\out "P & Q [P & Q]"] : thm list} -\end{ttbox} -By applying $(\forall E)$ and $({\imp}E)$ to the resolvents, we dispose of -the vacuous one and put the other into a convenient form:\footnote {Why use - {\tt [spec] RL [mp]} instead of {\tt [spec RS mp]} to join the rules? In - higher-order logic, {\tt spec RS mp} fails because the resolution yields - two results, namely ${\List{\forall x.x; P}\Imp Q}$ and ${\List{\forall - x.P(x)\imp Q(x); P(x)}\Imp Q(x)}$. In first-order logic, the - resolution yields only the latter result because $\forall x.x$ is not a - first-order formula; in fact, it is equivalent to falsity.} \index{*RL} -\begin{ttbox} -prems RL [and_def RS subst] RL [spec] RL [mp]; -{\out val it = ["P --> Q --> ?Q ==> ?Q [P & Q]"] : thm list} -\end{ttbox} -This is a list containing a single rule, which is directly applicable to -our goal: -\begin{ttbox} -by (resolve_tac it 1); -{\out Level 1} -{\out P} -{\out 1. P --> Q --> P} -\end{ttbox} -The subgoal is a trivial implication. Recall that \ttindex{ares_tac} is a -combination of {\tt assume_tac} and {\tt resolve_tac}. -\begin{ttbox} -by (REPEAT (ares_tac [impI] 1)); -{\out Level 2} -{\out P} -{\out No subgoals!} -\end{ttbox} - - +\goodbreak \section{Example: Cantor's Theorem}\label{sec:hol-cantor} Cantor's Theorem states that every set has more subsets than it has elements. It has become a favourite example in higher-order logic since @@ -1412,9 +1295,10 @@ % Viewing types as sets, $\alpha\To bool$ represents the powerset of~$\alpha$. This version states that for every function from $\alpha$ to -its powerset, some subset is outside its range. The Isabelle proof uses -\HOL's set theory, with the type $\alpha\,set$ and the operator -\cdx{range}. The set~$S$ is given as an unknown instead of a +its powerset, some subset is outside its range. + +The Isabelle proof uses \HOL's set theory, with the type $\alpha\,set$ and +the operator \cdx{range}. The set~$S$ is given as an unknown instead of a quantified variable so that we may inspect the subset found by the proof. \begin{ttbox} goal Set.thy "~ ?S : range(f :: 'a=>'a set)"; @@ -1457,8 +1341,8 @@ {\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)\}$, the -standard diagonal construction. +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}