Logics/HOL: Section 3, added Pow and its rule. New sections 6 on the
datatype declaration and 7 on (co)inductive definitions. Added mention of
directory IMP.
1.1 --- a/doc-src/Logics/Old_HOL.tex Fri Sep 09 11:40:40 1994 +0200
1.2 +++ b/doc-src/Logics/Old_HOL.tex Fri Sep 09 11:45:44 1994 +0200
1.3 @@ -414,10 +414,12 @@
1.4 & intersection over a set\\
1.5 \cdx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
1.6 & union over a set\\
1.7 - \cdx{Inter} & $((\alpha\,set)set)\To\alpha\,set$
1.8 + \cdx{Inter} & $(\alpha\,set)set\To\alpha\,set$
1.9 &set of sets intersection \\
1.10 - \cdx{Union} & $((\alpha\,set)set)\To\alpha\,set$
1.11 + \cdx{Union} & $(\alpha\,set)set\To\alpha\,set$
1.12 &set of sets union \\
1.13 + \cdx{Pow} & $\alpha\,set \To (\alpha\,set)set$
1.14 + & powerset \\[1ex]
1.15 \cdx{range} & $(\alpha\To\beta )\To\beta\,set$
1.16 & range of a function \\[1ex]
1.17 \cdx{Ball}~~\cdx{Bex} & $[\alpha\,set,\alpha\To bool]\To bool$
1.18 @@ -616,7 +618,8 @@
1.19 \tdx{INTER1_def} INTER1(B) == INTER(\{x.True\}, B)
1.20 \tdx{UNION1_def} UNION1(B) == UNION(\{x.True\}, B)
1.21 \tdx{Inter_def} Inter(S) == (INT x:S. x)
1.22 -\tdx{Union_def} Union(S) == (UN x:S. x)
1.23 +\tdx{Union_def} Union(S) == (UN x:S. x)
1.24 +\tdx{Pow_def} Pow(A) == \{B. B <= A\}
1.25 \tdx{image_def} f``A == \{y. ? x:A. y=f(x)\}
1.26 \tdx{range_def} range(f) == \{y. ? x. y=f(x)\}
1.27 \tdx{mono_def} mono(f) == !A B. A <= B --> f(A) <= f(B)
1.28 @@ -698,6 +701,9 @@
1.29 \tdx{InterI} [| !!X. X:C ==> A:X |] ==> A : Inter(C)
1.30 \tdx{InterD} [| A : Inter(C); X:C |] ==> A:X
1.31 \tdx{InterE} [| A : Inter(C); A:X ==> R; ~ X:C ==> R |] ==> R
1.32 +
1.33 +\tdx{PowI} A<=B ==> A: Pow(B)
1.34 +\tdx{PowD} A: Pow(B) ==> A<=B
1.35 \end{ttbox}
1.36 \caption{Further derived rules for set theory} \label{hol-set2}
1.37 \end{figure}
1.38 @@ -1344,7 +1350,7 @@
1.39 ;
1.40 typ : typevarlist id
1.41 | tid
1.42 - ;
1.43 + ;
1.44 typevarlist : () | tid | '(' (tid + ',') ')'
1.45 ;
1.46 \end{rail}
1.47 @@ -1528,9 +1534,175 @@
1.48 because the simplifier will dispose of them automatically.
1.49
1.50 \index{*datatype|)}
1.51 -\underscoreoff
1.52
1.53
1.54 +\section{Inductive and coinductive definitions}
1.55 +\index{*inductive|(}
1.56 +\index{*coinductive|(}
1.57 +
1.58 +An {\bf inductive definition} specifies the least set closed under given
1.59 +rules. For example, a structural operational semantics is an inductive
1.60 +definition of an evaluation relation. Dually, a {\bf coinductive
1.61 + definition} specifies the greatest set closed under given rules. An
1.62 +important example is using bisimulation relations to formalize equivalence
1.63 +of processes and infinite data structures.
1.64 +
1.65 +A theory file may contain any number of inductive and coinductive
1.66 +definitions. They may be intermixed with other declarations; in
1.67 +particular, the (co)inductive sets {\bf must} be declared separately as
1.68 +constants, and may have mixfix syntax or be subject to syntax translations.
1.69 +
1.70 +Each (co)inductive definition adds definitions to the theory and also
1.71 +proves some theorems. Each definition creates an ML structure, which is a
1.72 +substructure of the main theory structure.
1.73 +
1.74 +This package is derived from the ZF one, described in a
1.75 +separate paper,\footnote{It appeared in CADE~\cite{paulson-CADE} and a
1.76 + longer version is distributed with Isabelle.} which you should refer to
1.77 +in case of difficulties. The package is simpler than ZF's, thanks to HOL's
1.78 +automatic type-checking. The type of the (co)inductive determines the
1.79 +domain of the fixedpoint definition, and the package does not use inference
1.80 +rules for type-checking.
1.81 +
1.82 +
1.83 +\subsection{The result structure}
1.84 +Many of the result structure's components have been discussed in the paper;
1.85 +others are self-explanatory.
1.86 +\begin{description}
1.87 +\item[\tt thy] is the new theory containing the recursive sets.
1.88 +
1.89 +\item[\tt defs] is the list of definitions of the recursive sets.
1.90 +
1.91 +\item[\tt mono] is a monotonicity theorem for the fixedpoint operator.
1.92 +
1.93 +\item[\tt unfold] is a fixedpoint equation for the recursive set (the union of
1.94 +the recursive sets, in the case of mutual recursion).
1.95 +
1.96 +\item[\tt intrs] is the list of introduction rules, now proved as theorems, for
1.97 +the recursive sets. The rules are also available individually, using the
1.98 +names given them in the theory file.
1.99 +
1.100 +\item[\tt elim] is the elimination rule.
1.101 +
1.102 +\item[\tt mk\_cases] is a function to create simplified instances of {\tt
1.103 +elim}, using freeness reasoning on some underlying datatype.
1.104 +\end{description}
1.105 +
1.106 +For an inductive definition, the result structure contains two induction rules,
1.107 +{\tt induct} and \verb|mutual_induct|. For a coinductive definition, it
1.108 +contains the rule \verb|coinduct|.
1.109 +
1.110 +Figure~\ref{def-result-fig} summarizes the two result signatures,
1.111 +specifying the types of all these components.
1.112 +
1.113 +\begin{figure}
1.114 +\begin{ttbox}
1.115 +sig
1.116 +val thy : theory
1.117 +val defs : thm list
1.118 +val mono : thm
1.119 +val unfold : thm
1.120 +val intrs : thm list
1.121 +val elim : thm
1.122 +val mk_cases : thm list -> string -> thm
1.123 +{\it(Inductive definitions only)}
1.124 +val induct : thm
1.125 +val mutual_induct: thm
1.126 +{\it(Coinductive definitions only)}
1.127 +val coinduct : thm
1.128 +end
1.129 +\end{ttbox}
1.130 +\hrule
1.131 +\caption{The result of a (co)inductive definition} \label{def-result-fig}
1.132 +\end{figure}
1.133 +
1.134 +\subsection{The syntax of a (co)inductive definition}
1.135 +An inductive definition has the form
1.136 +\begin{ttbox}
1.137 +inductive {\it inductive sets}
1.138 + intrs {\it introduction rules}
1.139 + monos {\it monotonicity theorems}
1.140 + con_defs {\it constructor definitions}
1.141 +\end{ttbox}
1.142 +A coinductive definition is identical, except that it starts with the keyword
1.143 +{\tt coinductive}.
1.144 +
1.145 +The {\tt monos} and {\tt con\_defs} sections are optional. If present,
1.146 +each is specified as a string, which must be a valid ML expression of type
1.147 +{\tt thm list}. It is simply inserted into the {\tt .thy.ML} file; if it
1.148 +is ill-formed, it will trigger ML error messages. You can then inspect the
1.149 +file on your directory.
1.150 +
1.151 +\begin{itemize}
1.152 +\item The {\it inductive sets} are specified by one or more strings.
1.153 +
1.154 +\item The {\it introduction rules} specify one or more introduction rules in
1.155 + the form {\it ident\/}~{\it string}, where the identifier gives the name of
1.156 + the rule in the result structure.
1.157 +
1.158 +\item The {\it monotonicity theorems} are required for each operator
1.159 + applied to a recursive set in the introduction rules. There {\bf must}
1.160 + be a theorem of the form $A\subseteq B\Imp M(A)\subseteq M(B)$, for each
1.161 + premise $t\in M(R_i)$ in an introduction rule!
1.162 +
1.163 +\item The {\it constructor definitions} contain definitions of constants
1.164 + appearing in the introduction rules. In most cases it can be omitted.
1.165 +\end{itemize}
1.166 +
1.167 +The package has a few notable restrictions:
1.168 +\begin{itemize}
1.169 +\item The theory must separately declare the recursive sets as
1.170 + constants.
1.171 +
1.172 +\item The names of the recursive sets must be identifiers, not infix
1.173 +operators.
1.174 +
1.175 +\item Side-conditions must not be conjunctions. However, an introduction rule
1.176 +may contain any number of side-conditions.
1.177 +
1.178 +\item Side-conditions of the form $x=t$, where the variable~$x$ does not
1.179 + occur in~$t$, will be substituted through the rule \verb|mutual_induct|.
1.180 +\end{itemize}
1.181 +
1.182 +
1.183 +\subsection{Example of an inductive definition}
1.184 +Two declarations, included in a theory file, define the finite powerset
1.185 +operator. First we declare the constant~{\tt Fin}. Then we declare it
1.186 +inductively, with two introduction rules:
1.187 +\begin{ttbox}
1.188 +consts Fin :: "'a set => 'a set set"
1.189 +inductive "Fin(A)"
1.190 + intrs
1.191 + emptyI "{} : Fin(A)"
1.192 + insertI "[| a: A; b: Fin(A) |] ==> insert(a,b) : Fin(A)"
1.193 +\end{ttbox}
1.194 +The resulting theory structure contains a substructure, called~{\tt Fin}.
1.195 +It contains the {\tt Fin}$(A)$ introduction rules as the list {\tt Fin.intrs},
1.196 +and also individually as {\tt Fin.emptyI} and {\tt Fin.consI}. The induction
1.197 +rule is {\tt Fin.induct}.
1.198 +
1.199 +For another example, here is a theory file defining the accessible part of a
1.200 +relation. The main thing to note is the use of~{\tt Pow} in the sole
1.201 +introduction rule, and the corresponding mention of the rule
1.202 +\verb|Pow_mono| in the {\tt monos} list. The paper discusses a ZF version
1.203 +of this example in more detail.
1.204 +\begin{ttbox}
1.205 +Acc = WF +
1.206 +consts pred :: "['b, ('a * 'b)set] => 'a set" (*Set of predecessors*)
1.207 + acc :: "('a * 'a)set => 'a set" (*Accessible part*)
1.208 +defs pred_def "pred(x,r) == {y. <y,x>:r}"
1.209 +inductive "acc(r)"
1.210 + intrs
1.211 + pred "pred(a,r): Pow(acc(r)) ==> a: acc(r)"
1.212 + monos "[Pow_mono]"
1.213 +end
1.214 +\end{ttbox}
1.215 +The HOL distribution contains many other inductive definitions, such as the
1.216 +theory {\tt HOL/ex/PropLog.thy} and the directory {\tt HOL/IMP}. The
1.217 +theory {\tt HOL/LList.thy} contains coinductive definitions.
1.218 +
1.219 +\index{*coinductive|)} \index{*inductive|)} \underscoreoff
1.220 +
1.221
1.222 \section{The examples directories}
1.223 Directory {\tt HOL/Subst} contains Martin Coen's mechanisation of a theory of
1.224 @@ -1538,49 +1710,52 @@
1.225 mechanisation in {\LCF}~\cite{paulson85} of Manna and Waldinger's
1.226 theory~\cite{mw81}.
1.227
1.228 +Directory {\tt HOL/IMP} contains a mechanised version of a semantic
1.229 +equivalence proof taken from Winskel~\cite{winskel93}. It formalises the
1.230 +denotational and operational semantics of a simple while-language, then
1.231 +proves the two equivalent. It contains several datatype and inductive
1.232 +definitions, and demonstrates their use.
1.233 +
1.234 Directory {\tt HOL/ex} contains other examples and experimental proofs in
1.235 {\HOL}. Here is an overview of the more interesting files.
1.236 -\begin{ttdescription}
1.237 -\item[HOL/ex/cla.ML] demonstrates the classical reasoner on over sixty
1.238 +\begin{itemize}
1.239 +\item File {\tt cla.ML} demonstrates the classical reasoner on over sixty
1.240 predicate calculus theorems, ranging from simple tautologies to
1.241 moderately difficult problems involving equality and quantifiers.
1.242
1.243 -\item[HOL/ex/meson.ML] contains an experimental implementation of the {\sc
1.244 +\item File {\tt meson.ML} contains an experimental implementation of the {\sc
1.245 meson} proof procedure, inspired by Plaisted~\cite{plaisted90}. It is
1.246 much more powerful than Isabelle's classical reasoner. But it is less
1.247 useful in practice because it works only for pure logic; it does not
1.248 accept derived rules for the set theory primitives, for example.
1.249
1.250 -\item[HOL/ex/mesontest.ML] contains test data for the {\sc meson} proof
1.251 +\item File {\tt mesontest.ML} contains test data for the {\sc meson} proof
1.252 procedure. These are mostly taken from Pelletier \cite{pelletier86}.
1.253
1.254 -\item[HOL/ex/set.ML] proves Cantor's Theorem, which is presented in
1.255 +\item File {\tt set.ML} proves Cantor's Theorem, which is presented in
1.256 \S\ref{sec:hol-cantor} below, and the Schr\"oder-Bernstein Theorem.
1.257
1.258 -\item[HOL/ex/InSort.ML] and {\tt HOL/ex/Qsort.ML} contain correctness
1.259 - proofs about insertion sort and quick sort.
1.260 +\item Theories {\tt InSort} and {\tt Qsort} prove correctness properties of
1.261 + insertion sort and quick sort.
1.262
1.263 -\item[HOL/ex/PropLog.ML] proves the soundness and completeness of classical
1.264 - propositional logic, given a truth table semantics. The only connective
1.265 - is $\imp$. A Hilbert-style axiom system is specified, and its set of
1.266 - theorems defined inductively. A similar proof in \ZF{} is described
1.267 - elsewhere~\cite{paulson-set-II}.
1.268 +\item Theory {\tt PropLog} proves the soundness and completeness of
1.269 + classical propositional logic, given a truth table semantics. The only
1.270 + connective is $\imp$. A Hilbert-style axiom system is specified, and its
1.271 + set of theorems defined inductively. A similar proof in \ZF{} is
1.272 + described elsewhere~\cite{paulson-set-II}.
1.273
1.274 -\item[HOL/ex/Term.ML]
1.275 - contains proofs about an experimental recursive type definition;
1.276 +\item Theory {\tt Term} develops an experimental recursive type definition;
1.277 the recursion goes through the type constructor~\tydx{list}.
1.278
1.279 -\item[HOL/ex/Simult.ML] defines primitives for solving mutually recursive
1.280 - equations over sets. It constructs sets of trees and forests as an
1.281 - example, including induction and recursion rules that handle the mutual
1.282 - recursion.
1.283 +\item Theory {\tt Simult} constructs mutually recursive sets of trees and
1.284 + forests, including induction and recursion rules.
1.285
1.286 -\item[HOL/ex/MT.ML] contains Jacob Frost's formalization~\cite{frost93} of
1.287 +\item Theory {\tt MT} contains Jacob Frost's formalization~\cite{frost93} of
1.288 Milner and Tofte's coinduction example~\cite{milner-coind}. This
1.289 substantial proof concerns the soundness of a type system for a simple
1.290 functional language. The semantics of recursion is given by a cyclic
1.291 environment, which makes a coinductive argument appropriate.
1.292 -\end{ttdescription}
1.293 +\end{itemize}
1.294
1.295
1.296 \goodbreak