author | wenzelm |
Fri, 19 Aug 1994 16:13:53 +0200 | |
changeset 568 | 756b0e2a6cac |
parent 497 | 990d2573efa6 |
child 584 | 5b1a0e50c79a |
permissions | -rw-r--r-- |
497
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
1 |
\documentstyle[a4,proof,iman,extra,12pt]{llncs} |
103 | 2 |
\newif\ifCADE |
497
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
3 |
\CADEfalse |
103 | 4 |
|
355 | 5 |
\title{A Fixedpoint Approach to Implementing\\ |
6 |
(Co)Inductive Definitions\thanks{J. Grundy and S. Thompson made detailed |
|
7 |
comments; the referees were also helpful. Research funded by |
|
8 |
SERC grants GR/G53279, GR/H40570 and by the ESPRIT Project 6453 |
|
9 |
`Types'.}} |
|
103 | 10 |
|
355 | 11 |
\author{Lawrence C. Paulson\\{\tt lcp@cl.cam.ac.uk}} |
12 |
\institute{Computer Laboratory, University of Cambridge, England} |
|
103 | 13 |
\date{\today} |
14 |
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} |
|
15 |
||
16 |
\newcommand\sbs{\subseteq} |
|
17 |
\let\To=\Rightarrow |
|
18 |
||
19 |
||
355 | 20 |
\newcommand\pow{{\cal P}} |
21 |
%%%\let\pow=\wp |
|
22 |
\newcommand\RepFun{\hbox{\tt RepFun}} |
|
23 |
\newcommand\cons{\hbox{\tt cons}} |
|
24 |
\def\succ{\hbox{\tt succ}} |
|
25 |
\newcommand\split{\hbox{\tt split}} |
|
26 |
\newcommand\fst{\hbox{\tt fst}} |
|
27 |
\newcommand\snd{\hbox{\tt snd}} |
|
28 |
\newcommand\converse{\hbox{\tt converse}} |
|
29 |
\newcommand\domain{\hbox{\tt domain}} |
|
30 |
\newcommand\range{\hbox{\tt range}} |
|
31 |
\newcommand\field{\hbox{\tt field}} |
|
32 |
\newcommand\lfp{\hbox{\tt lfp}} |
|
33 |
\newcommand\gfp{\hbox{\tt gfp}} |
|
34 |
\newcommand\id{\hbox{\tt id}} |
|
35 |
\newcommand\trans{\hbox{\tt trans}} |
|
36 |
\newcommand\wf{\hbox{\tt wf}} |
|
37 |
\newcommand\nat{\hbox{\tt nat}} |
|
38 |
\newcommand\rank{\hbox{\tt rank}} |
|
39 |
\newcommand\univ{\hbox{\tt univ}} |
|
40 |
\newcommand\Vrec{\hbox{\tt Vrec}} |
|
41 |
\newcommand\Inl{\hbox{\tt Inl}} |
|
42 |
\newcommand\Inr{\hbox{\tt Inr}} |
|
43 |
\newcommand\case{\hbox{\tt case}} |
|
44 |
\newcommand\lst{\hbox{\tt list}} |
|
45 |
\newcommand\Nil{\hbox{\tt Nil}} |
|
46 |
\newcommand\Cons{\hbox{\tt Cons}} |
|
103 | 47 |
\newcommand\lstcase{\hbox{\tt list\_case}} |
48 |
\newcommand\lstrec{\hbox{\tt list\_rec}} |
|
355 | 49 |
\newcommand\length{\hbox{\tt length}} |
50 |
\newcommand\listn{\hbox{\tt listn}} |
|
51 |
\newcommand\acc{\hbox{\tt acc}} |
|
52 |
\newcommand\primrec{\hbox{\tt primrec}} |
|
53 |
\newcommand\SC{\hbox{\tt SC}} |
|
54 |
\newcommand\CONST{\hbox{\tt CONST}} |
|
55 |
\newcommand\PROJ{\hbox{\tt PROJ}} |
|
56 |
\newcommand\COMP{\hbox{\tt COMP}} |
|
57 |
\newcommand\PREC{\hbox{\tt PREC}} |
|
103 | 58 |
|
355 | 59 |
\newcommand\quniv{\hbox{\tt quniv}} |
60 |
\newcommand\llist{\hbox{\tt llist}} |
|
61 |
\newcommand\LNil{\hbox{\tt LNil}} |
|
62 |
\newcommand\LCons{\hbox{\tt LCons}} |
|
63 |
\newcommand\lconst{\hbox{\tt lconst}} |
|
64 |
\newcommand\lleq{\hbox{\tt lleq}} |
|
65 |
\newcommand\map{\hbox{\tt map}} |
|
66 |
\newcommand\term{\hbox{\tt term}} |
|
67 |
\newcommand\Apply{\hbox{\tt Apply}} |
|
68 |
\newcommand\termcase{\hbox{\tt term\_case}} |
|
69 |
\newcommand\rev{\hbox{\tt rev}} |
|
70 |
\newcommand\reflect{\hbox{\tt reflect}} |
|
71 |
\newcommand\tree{\hbox{\tt tree}} |
|
72 |
\newcommand\forest{\hbox{\tt forest}} |
|
73 |
\newcommand\Part{\hbox{\tt Part}} |
|
74 |
\newcommand\TF{\hbox{\tt tree\_forest}} |
|
75 |
\newcommand\Tcons{\hbox{\tt Tcons}} |
|
76 |
\newcommand\Fcons{\hbox{\tt Fcons}} |
|
77 |
\newcommand\Fnil{\hbox{\tt Fnil}} |
|
103 | 78 |
\newcommand\TFcase{\hbox{\tt TF\_case}} |
355 | 79 |
\newcommand\Fin{\hbox{\tt Fin}} |
80 |
\newcommand\QInl{\hbox{\tt QInl}} |
|
81 |
\newcommand\QInr{\hbox{\tt QInr}} |
|
82 |
\newcommand\qsplit{\hbox{\tt qsplit}} |
|
83 |
\newcommand\qcase{\hbox{\tt qcase}} |
|
84 |
\newcommand\Con{\hbox{\tt Con}} |
|
85 |
\newcommand\data{\hbox{\tt data}} |
|
103 | 86 |
|
87 |
\binperiod %%%treat . like a binary operator |
|
88 |
||
89 |
\begin{document} |
|
355 | 90 |
%CADE%\pagestyle{empty} |
91 |
%CADE%\begin{titlepage} |
|
103 | 92 |
\maketitle |
93 |
\begin{abstract} |
|
355 | 94 |
This paper presents a fixedpoint approach to inductive definitions. |
95 |
Instead of using a syntactic test such as `strictly positive,' the |
|
96 |
approach lets definitions involve any operators that have been proved |
|
97 |
monotone. It is conceptually simple, which has allowed the easy |
|
98 |
implementation of mutual recursion and other conveniences. It also |
|
99 |
handles coinductive definitions: simply replace the least fixedpoint by a |
|
100 |
greatest fixedpoint. This represents the first automated support for |
|
101 |
coinductive definitions. |
|
130 | 102 |
|
103 |
The method has been implemented in Isabelle's formalization of ZF set |
|
179 | 104 |
theory. It should be applicable to any logic in which the Knaster-Tarski |
355 | 105 |
Theorem can be proved. Examples include lists of $n$ elements, the |
106 |
accessible part of a relation and the set of primitive recursive |
|
107 |
functions. One example of a coinductive definition is bisimulations for |
|
108 |
lazy lists. \ifCADE\else Recursive datatypes are examined in detail, as |
|
109 |
well as one example of a {\bf codatatype}: lazy lists. The appendices |
|
110 |
are simple user's manuals for this Isabelle/ZF package.\fi |
|
103 | 111 |
\end{abstract} |
112 |
% |
|
355 | 113 |
%CADE%\bigskip\centerline{Copyright \copyright{} \number\year{} by Lawrence C. Paulson} |
114 |
%CADE%\thispagestyle{empty} |
|
115 |
%CADE%\end{titlepage} |
|
116 |
%CADE%\tableofcontents\cleardoublepage\pagestyle{headings} |
|
103 | 117 |
|
118 |
\section{Introduction} |
|
119 |
Several theorem provers provide commands for formalizing recursive data |
|
120 |
structures, like lists and trees. Examples include Boyer and Moore's shell |
|
121 |
principle~\cite{bm79} and Melham's recursive type package for the HOL |
|
122 |
system~\cite{melham89}. Such data structures are called {\bf datatypes} |
|
123 |
below, by analogy with {\tt datatype} definitions in Standard~ML\@. |
|
124 |
||
130 | 125 |
A datatype is but one example of an {\bf inductive definition}. This |
103 | 126 |
specifies the least set closed under given rules~\cite{aczel77}. The |
127 |
collection of theorems in a logic is inductively defined. A structural |
|
128 |
operational semantics~\cite{hennessy90} is an inductive definition of a |
|
129 |
reduction or evaluation relation on programs. A few theorem provers |
|
130 |
provide commands for formalizing inductive definitions; these include |
|
131 |
Coq~\cite{paulin92} and again the HOL system~\cite{camilleri92}. |
|
132 |
||
130 | 133 |
The dual notion is that of a {\bf coinductive definition}. This specifies |
103 | 134 |
the greatest set closed under given rules. Important examples include |
135 |
using bisimulation relations to formalize equivalence of |
|
136 |
processes~\cite{milner89} or lazy functional programs~\cite{abramsky90}. |
|
137 |
Other examples include lazy lists and other infinite data structures; these |
|
130 | 138 |
are called {\bf codatatypes} below. |
103 | 139 |
|
355 | 140 |
Not all inductive definitions are meaningful. {\bf Monotone} inductive |
141 |
definitions are a large, well-behaved class. Monotonicity can be enforced |
|
142 |
by syntactic conditions such as `strictly positive,' but this could lead to |
|
143 |
monotone definitions being rejected on the grounds of their syntactic form. |
|
144 |
More flexible is to formalize monotonicity within the logic and allow users |
|
145 |
to prove it. |
|
103 | 146 |
|
147 |
This paper describes a package based on a fixedpoint approach. Least |
|
148 |
fixedpoints yield inductive definitions; greatest fixedpoints yield |
|
355 | 149 |
coinductive definitions. The package has several advantages: |
103 | 150 |
\begin{itemize} |
355 | 151 |
\item It allows reference to any operators that have been proved monotone. |
152 |
Thus it accepts all provably monotone inductive definitions, including |
|
153 |
iterated definitions. |
|
154 |
\item It accepts a wide class of datatype definitions, though at present |
|
155 |
restricted to finite branching. |
|
130 | 156 |
\item It handles coinductive and codatatype definitions. Most of |
157 |
the discussion below applies equally to inductive and coinductive |
|
103 | 158 |
definitions, and most of the code is shared. To my knowledge, this is |
130 | 159 |
the only package supporting coinductive definitions. |
103 | 160 |
\item Definitions may be mutually recursive. |
161 |
\end{itemize} |
|
162 |
The package is implemented in Isabelle~\cite{isabelle-intro}, using ZF set |
|
163 |
theory \cite{paulson-set-I,paulson-set-II}. However, the fixedpoint |
|
164 |
approach is independent of Isabelle. The recursion equations are specified |
|
165 |
as introduction rules for the mutually recursive sets. The package |
|
166 |
transforms these rules into a mapping over sets, and attempts to prove that |
|
167 |
the mapping is monotonic and well-typed. If successful, the package |
|
168 |
makes fixedpoint definitions and proves the introduction, elimination and |
|
130 | 169 |
(co)induction rules. The package consists of several Standard ML |
103 | 170 |
functors~\cite{paulson91}; it accepts its argument and returns its result |
355 | 171 |
as ML structures.\footnote{This use of ML modules is not essential; the |
172 |
package could also be implemented as a function on records.} |
|
103 | 173 |
|
174 |
Most datatype packages equip the new datatype with some means of expressing |
|
355 | 175 |
recursive functions. This is the main omission from my package. Its |
176 |
fixedpoint operators define only recursive sets. To define recursive |
|
177 |
functions, the Isabelle/ZF theory provides well-founded recursion and other |
|
178 |
logical tools~\cite{paulson-set-II}. |
|
103 | 179 |
|
355 | 180 |
{\bf Outline.} Section~2 introduces the least and greatest fixedpoint |
181 |
operators. Section~3 discusses the form of introduction rules, mutual |
|
182 |
recursion and other points common to inductive and coinductive definitions. |
|
183 |
Section~4 discusses induction and coinduction rules separately. Section~5 |
|
184 |
presents several examples, including a coinductive definition. Section~6 |
|
185 |
describes datatype definitions. Section~7 presents related work. |
|
186 |
Section~8 draws brief conclusions. \ifCADE\else The appendices are simple |
|
187 |
user's manuals for this Isabelle/ZF package.\fi |
|
103 | 188 |
|
189 |
Most of the definitions and theorems shown below have been generated by the |
|
190 |
package. I have renamed some variables to improve readability. |
|
191 |
||
192 |
\section{Fixedpoint operators} |
|
193 |
In set theory, the least and greatest fixedpoint operators are defined as |
|
194 |
follows: |
|
195 |
\begin{eqnarray*} |
|
196 |
\lfp(D,h) & \equiv & \inter\{X\sbs D. h(X)\sbs X\} \\ |
|
197 |
\gfp(D,h) & \equiv & \union\{X\sbs D. X\sbs h(X)\} |
|
198 |
\end{eqnarray*} |
|
130 | 199 |
Let $D$ be a set. Say that $h$ is {\bf bounded by}~$D$ if $h(D)\sbs D$, and |
200 |
{\bf monotone below~$D$} if |
|
103 | 201 |
$h(A)\sbs h(B)$ for all $A$ and $B$ such that $A\sbs B\sbs D$. If $h$ is |
202 |
bounded by~$D$ and monotone then both operators yield fixedpoints: |
|
203 |
\begin{eqnarray*} |
|
204 |
\lfp(D,h) & = & h(\lfp(D,h)) \\ |
|
205 |
\gfp(D,h) & = & h(\gfp(D,h)) |
|
206 |
\end{eqnarray*} |
|
355 | 207 |
These equations are instances of the Knaster-Tarski Theorem, which states |
103 | 208 |
that every monotonic function over a complete lattice has a |
209 |
fixedpoint~\cite{davey&priestley}. It is obvious from their definitions |
|
210 |
that $\lfp$ must be the least fixedpoint, and $\gfp$ the greatest. |
|
211 |
||
355 | 212 |
This fixedpoint theory is simple. The Knaster-Tarski Theorem is easy to |
103 | 213 |
prove. Showing monotonicity of~$h$ is trivial, in typical cases. We must |
355 | 214 |
also exhibit a bounding set~$D$ for~$h$. Frequently this is trivial, as |
179 | 215 |
when a set of `theorems' is (co)inductively defined over some previously |
355 | 216 |
existing set of `formulae.' Isabelle/ZF provides a suitable bounding set |
217 |
for finitely branching (co)datatype definitions; see~\S\ref{univ-sec} |
|
218 |
below. Bounding sets are also called {\bf domains}. |
|
103 | 219 |
|
355 | 220 |
The powerset operator is monotone, but by Cantor's Theorem there is no |
221 |
set~$A$ such that $A=\pow(A)$. We cannot put $A=\lfp(D,\pow)$ because |
|
222 |
there is no suitable domain~$D$. But \S\ref{acc-sec} demonstrates |
|
223 |
that~$\pow$ is still useful in inductive definitions. |
|
103 | 224 |
|
130 | 225 |
\section{Elements of an inductive or coinductive definition}\label{basic-sec} |
226 |
Consider a (co)inductive definition of the sets $R_1$, \ldots,~$R_n$, in |
|
355 | 227 |
mutual recursion. They will be constructed from domains $D_1$, |
228 |
\ldots,~$D_n$, respectively. The construction yields not $R_i\sbs D_i$ but |
|
229 |
$R_i\sbs D_1+\cdots+D_n$, where $R_i$ is contained in the image of~$D_i$ |
|
230 |
under an injection. Reasons for this are discussed |
|
130 | 231 |
elsewhere~\cite[\S4.5]{paulson-set-II}. |
103 | 232 |
|
233 |
The definition may involve arbitrary parameters $\vec{p}=p_1$, |
|
234 |
\ldots,~$p_k$. Each recursive set then has the form $R_i(\vec{p})$. The |
|
235 |
parameters must be identical every time they occur within a definition. This |
|
236 |
would appear to be a serious restriction compared with other systems such as |
|
237 |
Coq~\cite{paulin92}. For instance, we cannot define the lists of |
|
238 |
$n$ elements as the set $\listn(A,n)$ using rules where the parameter~$n$ |
|
355 | 239 |
varies. Section~\ref{listn-sec} describes how to express this set using the |
130 | 240 |
inductive definition package. |
103 | 241 |
|
242 |
To avoid clutter below, the recursive sets are shown as simply $R_i$ |
|
243 |
instead of $R_i(\vec{p})$. |
|
244 |
||
245 |
\subsection{The form of the introduction rules}\label{intro-sec} |
|
246 |
The body of the definition consists of the desired introduction rules, |
|
247 |
specified as strings. The conclusion of each rule must have the form $t\in |
|
248 |
R_i$, where $t$ is any term. Premises typically have the same form, but |
|
249 |
they can have the more general form $t\in M(R_i)$ or express arbitrary |
|
250 |
side-conditions. |
|
251 |
||
252 |
The premise $t\in M(R_i)$ is permitted if $M$ is a monotonic operator on |
|
253 |
sets, satisfying the rule |
|
254 |
\[ \infer{M(A)\sbs M(B)}{A\sbs B} \] |
|
130 | 255 |
The user must supply the package with monotonicity rules for all such premises. |
103 | 256 |
|
355 | 257 |
The ability to introduce new monotone operators makes the approach |
258 |
flexible. A suitable choice of~$M$ and~$t$ can express a lot. The |
|
259 |
powerset operator $\pow$ is monotone, and the premise $t\in\pow(R)$ |
|
260 |
expresses $t\sbs R$; see \S\ref{acc-sec} for an example. The `list of' |
|
261 |
operator is monotone, as is easily proved by induction. The premise |
|
262 |
$t\in\lst(R)$ avoids having to encode the effect of~$\lst(R)$ using mutual |
|
263 |
recursion; see \S\ref{primrec-sec} and also my earlier |
|
264 |
paper~\cite[\S4.4]{paulson-set-II}. |
|
103 | 265 |
|
266 |
Introduction rules may also contain {\bf side-conditions}. These are |
|
267 |
premises consisting of arbitrary formulae not mentioning the recursive |
|
268 |
sets. Side-conditions typically involve type-checking. One example is the |
|
269 |
premise $a\in A$ in the following rule from the definition of lists: |
|
270 |
\[ \infer{\Cons(a,l)\in\lst(A)}{a\in A & l\in\lst(A)} \] |
|
271 |
||
272 |
\subsection{The fixedpoint definitions} |
|
273 |
The package translates the list of desired introduction rules into a fixedpoint |
|
455 | 274 |
definition. Consider, as a running example, the finite powerset operator |
103 | 275 |
$\Fin(A)$: the set of all finite subsets of~$A$. It can be |
276 |
defined as the least set closed under the rules |
|
277 |
\[ \emptyset\in\Fin(A) \qquad |
|
278 |
\infer{\{a\}\un b\in\Fin(A)}{a\in A & b\in\Fin(A)} |
|
279 |
\] |
|
280 |
||
130 | 281 |
The domain in a (co)inductive definition must be some existing set closed |
103 | 282 |
under the rules. A suitable domain for $\Fin(A)$ is $\pow(A)$, the set of all |
283 |
subsets of~$A$. The package generates the definition |
|
284 |
\begin{eqnarray*} |
|
285 |
\Fin(A) & \equiv & \lfp(\pow(A), \; |
|
286 |
\begin{array}[t]{r@{\,}l} |
|
287 |
\lambda X. \{z\in\pow(A). & z=\emptyset \disj{} \\ |
|
288 |
&(\exists a\,b. z=\{a\}\un b\conj a\in A\conj b\in X)\}) |
|
289 |
\end{array} |
|
130 | 290 |
\end{eqnarray*} |
103 | 291 |
The contribution of each rule to the definition of $\Fin(A)$ should be |
130 | 292 |
obvious. A coinductive definition is similar but uses $\gfp$ instead |
103 | 293 |
of~$\lfp$. |
294 |
||
295 |
The package must prove that the fixedpoint operator is applied to a |
|
296 |
monotonic function. If the introduction rules have the form described |
|
297 |
above, and if the package is supplied a monotonicity theorem for every |
|
298 |
$t\in M(R_i)$ premise, then this proof is trivial.\footnote{Due to the |
|
299 |
presence of logical connectives in the fixedpoint's body, the |
|
300 |
monotonicity proof requires some unusual rules. These state that the |
|
130 | 301 |
connectives $\conj$, $\disj$ and $\exists$ preserve monotonicity with respect |
302 |
to the partial ordering on unary predicates given by $P\sqsubseteq Q$ if and |
|
103 | 303 |
only if $\forall x.P(x)\imp Q(x)$.} |
304 |
||
355 | 305 |
The package returns its result as an ML structure, which consists of named |
306 |
components; we may regard it as a record. The result structure contains |
|
307 |
the definitions of the recursive sets as a theorem list called {\tt defs}. |
|
308 |
It also contains, as the theorem {\tt unfold}, a fixedpoint equation such |
|
309 |
as |
|
103 | 310 |
\begin{eqnarray*} |
311 |
\Fin(A) & = & |
|
312 |
\begin{array}[t]{r@{\,}l} |
|
313 |
\{z\in\pow(A). & z=\emptyset \disj{} \\ |
|
314 |
&(\exists a\,b. z=\{a\}\un b\conj a\in A\conj b\in \Fin(A))\} |
|
315 |
\end{array} |
|
316 |
\end{eqnarray*} |
|
130 | 317 |
It also contains, as the theorem {\tt dom\_subset}, an inclusion such as |
103 | 318 |
$\Fin(A)\sbs\pow(A)$. |
319 |
||
320 |
||
321 |
\subsection{Mutual recursion} \label{mutual-sec} |
|
130 | 322 |
In a mutually recursive definition, the domain of the fixedpoint construction |
103 | 323 |
is the disjoint sum of the domain~$D_i$ of each~$R_i$, for $i=1$, |
324 |
\ldots,~$n$. The package uses the injections of the |
|
325 |
binary disjoint sum, typically $\Inl$ and~$\Inr$, to express injections |
|
130 | 326 |
$h_{1n}$, \ldots, $h_{nn}$ for the $n$-ary disjoint sum $D_1+\cdots+D_n$. |
103 | 327 |
|
328 |
As discussed elsewhere \cite[\S4.5]{paulson-set-II}, Isabelle/ZF defines the |
|
329 |
operator $\Part$ to support mutual recursion. The set $\Part(A,h)$ |
|
330 |
contains those elements of~$A$ having the form~$h(z)$: |
|
331 |
\begin{eqnarray*} |
|
332 |
\Part(A,h) & \equiv & \{x\in A. \exists z. x=h(z)\}. |
|
333 |
\end{eqnarray*} |
|
334 |
For mutually recursive sets $R_1$, \ldots,~$R_n$ with |
|
335 |
$n>1$, the package makes $n+1$ definitions. The first defines a set $R$ using |
|
336 |
a fixedpoint operator. The remaining $n$ definitions have the form |
|
337 |
\begin{eqnarray*} |
|
130 | 338 |
R_i & \equiv & \Part(R,h_{in}), \qquad i=1,\ldots, n. |
103 | 339 |
\end{eqnarray*} |
340 |
It follows that $R=R_1\un\cdots\un R_n$, where the $R_i$ are pairwise disjoint. |
|
341 |
||
342 |
||
343 |
\subsection{Proving the introduction rules} |
|
130 | 344 |
The user supplies the package with the desired form of the introduction |
103 | 345 |
rules. Once it has derived the theorem {\tt unfold}, it attempts |
130 | 346 |
to prove those rules. From the user's point of view, this is the |
103 | 347 |
trickiest stage; the proofs often fail. The task is to show that the domain |
348 |
$D_1+\cdots+D_n$ of the combined set $R_1\un\cdots\un R_n$ is |
|
349 |
closed under all the introduction rules. This essentially involves replacing |
|
350 |
each~$R_i$ by $D_1+\cdots+D_n$ in each of the introduction rules and |
|
351 |
attempting to prove the result. |
|
352 |
||
353 |
Consider the $\Fin(A)$ example. After substituting $\pow(A)$ for $\Fin(A)$ |
|
354 |
in the rules, the package must prove |
|
355 |
\[ \emptyset\in\pow(A) \qquad |
|
356 |
\infer{\{a\}\un b\in\pow(A)}{a\in A & b\in\pow(A)} |
|
357 |
\] |
|
358 |
Such proofs can be regarded as type-checking the definition. The user |
|
359 |
supplies the package with type-checking rules to apply. Usually these are |
|
360 |
general purpose rules from the ZF theory. They could however be rules |
|
361 |
specifically proved for a particular inductive definition; sometimes this is |
|
362 |
the easiest way to get the definition through! |
|
363 |
||
130 | 364 |
The result structure contains the introduction rules as the theorem list {\tt |
365 |
intrs}. |
|
103 | 366 |
|
355 | 367 |
\subsection{The case analysis rule} |
368 |
The elimination rule, called {\tt elim}, performs case analysis. There is one |
|
130 | 369 |
case for each introduction rule. The elimination rule |
370 |
for $\Fin(A)$ is |
|
103 | 371 |
\[ \infer{Q}{x\in\Fin(A) & \infer*{Q}{[x=\emptyset]} |
372 |
& \infer*{Q}{[x=\{a\}\un b & a\in A &b\in\Fin(A)]_{a,b}} } |
|
373 |
\] |
|
355 | 374 |
The subscripted variables $a$ and~$b$ above the third premise are |
375 |
eigenvariables, subject to the usual `not free in \ldots' proviso. |
|
376 |
The rule states that if $x\in\Fin(A)$ then either $x=\emptyset$ or else |
|
130 | 377 |
$x=\{a\}\un b$ for some $a\in A$ and $b\in\Fin(A)$; it is a simple consequence |
378 |
of {\tt unfold}. |
|
379 |
||
355 | 380 |
The package also returns a function for generating simplified instances of |
381 |
the case analysis rule. It works for datatypes and for inductive |
|
382 |
definitions involving datatypes, such as an inductively defined relation |
|
383 |
between lists. It instantiates {\tt elim} with a user-supplied term then |
|
384 |
simplifies the cases using freeness of the underlying datatype. The |
|
385 |
simplified rules perform `rule inversion' on the inductive definition. |
|
386 |
Section~\S\ref{mkcases} presents an example. |
|
387 |
||
103 | 388 |
|
130 | 389 |
\section{Induction and coinduction rules} |
390 |
Here we must consider inductive and coinductive definitions separately. |
|
103 | 391 |
For an inductive definition, the package returns an induction rule derived |
392 |
directly from the properties of least fixedpoints, as well as a modified |
|
393 |
rule for mutual recursion and inductively defined relations. For a |
|
130 | 394 |
coinductive definition, the package returns a basic coinduction rule. |
103 | 395 |
|
396 |
\subsection{The basic induction rule}\label{basic-ind-sec} |
|
130 | 397 |
The basic rule, called {\tt induct}, is appropriate in most situations. |
103 | 398 |
For inductive definitions, it is strong rule induction~\cite{camilleri92}; for |
399 |
datatype definitions (see below), it is just structural induction. |
|
400 |
||
401 |
The induction rule for an inductively defined set~$R$ has the following form. |
|
402 |
The major premise is $x\in R$. There is a minor premise for each |
|
403 |
introduction rule: |
|
404 |
\begin{itemize} |
|
405 |
\item If the introduction rule concludes $t\in R_i$, then the minor premise |
|
406 |
is~$P(t)$. |
|
407 |
||
408 |
\item The minor premise's eigenvariables are precisely the introduction |
|
130 | 409 |
rule's free variables that are not parameters of~$R$. For instance, the |
410 |
eigenvariables in the $\Fin(A)$ rule below are $a$ and $b$, but not~$A$. |
|
103 | 411 |
|
412 |
\item If the introduction rule has a premise $t\in R_i$, then the minor |
|
413 |
premise discharges the assumption $t\in R_i$ and the induction |
|
414 |
hypothesis~$P(t)$. If the introduction rule has a premise $t\in M(R_i)$ |
|
415 |
then the minor premise discharges the single assumption |
|
416 |
\[ t\in M(\{z\in R_i. P(z)\}). \] |
|
417 |
Because $M$ is monotonic, this assumption implies $t\in M(R_i)$. The |
|
418 |
occurrence of $P$ gives the effect of an induction hypothesis, which may be |
|
419 |
exploited by appealing to properties of~$M$. |
|
420 |
\end{itemize} |
|
130 | 421 |
The induction rule for $\Fin(A)$ resembles the elimination rule shown above, |
422 |
but includes an induction hypothesis: |
|
103 | 423 |
\[ \infer{P(x)}{x\in\Fin(A) & P(\emptyset) |
424 |
& \infer*{P(\{a\}\un b)}{[a\in A & b\in\Fin(A) & P(b)]_{a,b}} } |
|
425 |
\] |
|
355 | 426 |
Stronger induction rules often suggest themselves. We can derive a rule |
427 |
for $\Fin(A)$ whose third premise discharges the extra assumption $a\not\in |
|
428 |
b$. The Isabelle/ZF theory defines the {\bf rank} of a |
|
429 |
set~\cite[\S3.4]{paulson-set-II}, which supports well-founded induction and |
|
430 |
recursion over datatypes. The package proves a rule for mutual induction |
|
431 |
and inductive relations. |
|
103 | 432 |
|
433 |
\subsection{Mutual induction} |
|
434 |
The mutual induction rule is called {\tt |
|
435 |
mutual\_induct}. It differs from the basic rule in several respects: |
|
436 |
\begin{itemize} |
|
437 |
\item Instead of a single predicate~$P$, it uses $n$ predicates $P_1$, |
|
438 |
\ldots,~$P_n$: one for each recursive set. |
|
439 |
||
440 |
\item There is no major premise such as $x\in R_i$. Instead, the conclusion |
|
441 |
refers to all the recursive sets: |
|
442 |
\[ (\forall z.z\in R_1\imp P_1(z))\conj\cdots\conj |
|
443 |
(\forall z.z\in R_n\imp P_n(z)) |
|
444 |
\] |
|
355 | 445 |
Proving the premises establishes $P_i(z)$ for $z\in R_i$ and $i=1$, |
446 |
\ldots,~$n$. |
|
103 | 447 |
|
448 |
\item If the domain of some $R_i$ is the Cartesian product |
|
449 |
$A_1\times\cdots\times A_m$, then the corresponding predicate $P_i$ takes $m$ |
|
450 |
arguments and the corresponding conjunct of the conclusion is |
|
451 |
\[ (\forall z_1\ldots z_m.\pair{z_1,\ldots,z_m}\in R_i\imp P_i(z_1,\ldots,z_m)) |
|
452 |
\] |
|
453 |
\end{itemize} |
|
454 |
The last point above simplifies reasoning about inductively defined |
|
455 |
relations. It eliminates the need to express properties of $z_1$, |
|
456 |
\ldots,~$z_m$ as properties of the tuple $\pair{z_1,\ldots,z_m}$. |
|
457 |
||
130 | 458 |
\subsection{Coinduction}\label{coind-sec} |
459 |
A coinductive definition yields a primitive coinduction rule, with no |
|
103 | 460 |
refinements such as those for the induction rules. (Experience may suggest |
130 | 461 |
refinements later.) Consider the codatatype of lazy lists as an example. For |
103 | 462 |
suitable definitions of $\LNil$ and $\LCons$, lazy lists may be defined as the |
463 |
greatest fixedpoint satisfying the rules |
|
464 |
\[ \LNil\in\llist(A) \qquad |
|
465 |
\infer[(-)]{\LCons(a,l)\in\llist(A)}{a\in A & l\in\llist(A)} |
|
466 |
\] |
|
130 | 467 |
The $(-)$ tag stresses that this is a coinductive definition. A suitable |
103 | 468 |
domain for $\llist(A)$ is $\quniv(A)$, a set closed under variant forms of |
469 |
sum and product for representing infinite data structures |
|
130 | 470 |
(see~\S\ref{univ-sec}). Coinductive definitions use these variant sums and |
103 | 471 |
products. |
472 |
||
473 |
The package derives an {\tt unfold} theorem similar to that for $\Fin(A)$. |
|
355 | 474 |
Then it proves the theorem {\tt coinduct}, which expresses that $\llist(A)$ |
103 | 475 |
is the greatest solution to this equation contained in $\quniv(A)$: |
130 | 476 |
\[ \infer{x\in\llist(A)}{x\in X & X\sbs \quniv(A) & |
103 | 477 |
\infer*{z=\LNil\disj \bigl(\exists a\,l.\, |
355 | 478 |
z=\LCons(a,l) \conj a\in A \conj l\in X\un\llist(A) \bigr)} |
479 |
{[z\in X]_z}} |
|
480 |
% \begin{array}[t]{@{}l} |
|
481 |
% z=\LCons(a,l) \conj a\in A \conj{}\\ |
|
482 |
% l\in X\un\llist(A) \bigr) |
|
483 |
% \end{array} }{[z\in X]_z}} |
|
103 | 484 |
\] |
130 | 485 |
This rule complements the introduction rules; it provides a means of showing |
486 |
$x\in\llist(A)$ when $x$ is infinite. For instance, if $x=\LCons(0,x)$ then |
|
355 | 487 |
applying the rule with $X=\{x\}$ proves $x\in\llist(\nat)$. (Here $\nat$ |
488 |
is the set of natural numbers.) |
|
130 | 489 |
|
103 | 490 |
Having $X\un\llist(A)$ instead of simply $X$ in the third premise above |
491 |
represents a slight strengthening of the greatest fixedpoint property. I |
|
130 | 492 |
discuss several forms of coinduction rules elsewhere~\cite{paulson-coind}. |
103 | 493 |
|
494 |
||
130 | 495 |
\section{Examples of inductive and coinductive definitions}\label{ind-eg-sec} |
455 | 496 |
This section presents several examples: the finite powerset operator, |
103 | 497 |
lists of $n$ elements, bisimulations on lazy lists, the well-founded part |
498 |
of a relation, and the primitive recursive functions. |
|
499 |
||
455 | 500 |
\subsection{The finite powerset operator} |
501 |
This operator has been discussed extensively above. Here |
|
103 | 502 |
is the corresponding ML invocation (note that $\cons(a,b)$ abbreviates |
503 |
$\{a\}\un b$ in Isabelle/ZF): |
|
504 |
\begin{ttbox} |
|
505 |
structure Fin = Inductive_Fun |
|
497
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
506 |
(val thy = Arith.thy |> add_consts [("Fin", "i=>i", NoSyn)] |
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
507 |
val thy_name = "Fin" |
355 | 508 |
val rec_doms = [("Fin","Pow(A)")] |
509 |
val sintrs = ["0 : Fin(A)", |
|
510 |
"[| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)"] |
|
511 |
val monos = [] |
|
512 |
val con_defs = [] |
|
513 |
val type_intrs = [empty_subsetI, cons_subsetI, PowI] |
|
103 | 514 |
val type_elims = [make_elim PowD]); |
515 |
\end{ttbox} |
|
355 | 516 |
We apply the functor {\tt Inductive\_Fun} to a structure describing the |
517 |
desired inductive definition. The parent theory~{\tt thy} is obtained from |
|
518 |
{\tt Arith.thy} by adding the unary function symbol~$\Fin$. Its domain is |
|
519 |
specified as $\pow(A)$, where $A$ is the parameter appearing in the |
|
520 |
introduction rules. For type-checking, the structure supplies introduction |
|
521 |
rules: |
|
103 | 522 |
\[ \emptyset\sbs A \qquad |
523 |
\infer{\{a\}\un B\sbs C}{a\in C & B\sbs C} |
|
524 |
\] |
|
525 |
A further introduction rule and an elimination rule express the two |
|
526 |
directions of the equivalence $A\in\pow(B)\bimp A\sbs B$. Type-checking |
|
355 | 527 |
involves mostly introduction rules. |
528 |
||
529 |
ML is Isabelle's top level, so such functor invocations can take place at |
|
530 |
any time. The result structure is declared with the name~{\tt Fin}; we can |
|
531 |
refer to the $\Fin(A)$ introduction rules as {\tt Fin.intrs}, the induction |
|
532 |
rule as {\tt Fin.induct} and so forth. There are plans to integrate the |
|
533 |
package better into Isabelle so that users can place inductive definitions |
|
534 |
in Isabelle theory files instead of applying functors. |
|
535 |
||
103 | 536 |
|
537 |
\subsection{Lists of $n$ elements}\label{listn-sec} |
|
179 | 538 |
This has become a standard example of an inductive definition. Following |
539 |
Paulin-Mohring~\cite{paulin92}, we could attempt to define a new datatype |
|
540 |
$\listn(A,n)$, for lists of length~$n$, as an $n$-indexed family of sets. |
|
541 |
But her introduction rules |
|
355 | 542 |
\[ \hbox{\tt Niln}\in\listn(A,0) \qquad |
543 |
\infer{\hbox{\tt Consn}(n,a,l)\in\listn(A,\succ(n))} |
|
103 | 544 |
{n\in\nat & a\in A & l\in\listn(A,n)} |
545 |
\] |
|
546 |
are not acceptable to the inductive definition package: |
|
547 |
$\listn$ occurs with three different parameter lists in the definition. |
|
548 |
||
549 |
\begin{figure} |
|
355 | 550 |
\begin{ttbox} |
103 | 551 |
structure ListN = Inductive_Fun |
497
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
552 |
(val thy = ListFn.thy |> add_consts [("listn","i=>i",NoSyn)] |
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
553 |
val thy_name = "ListN" |
355 | 554 |
val rec_doms = [("listn", "nat*list(A)")] |
555 |
val sintrs = |
|
556 |
["<0,Nil>: listn(A)", |
|
557 |
"[| a: A; <n,l>: listn(A) |] ==> <succ(n), Cons(a,l)>: listn(A)"] |
|
558 |
val monos = [] |
|
559 |
val con_defs = [] |
|
560 |
val type_intrs = nat_typechecks @ List.intrs @ [SigmaI] |
|
497
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
561 |
val type_elims = []); |
355 | 562 |
\end{ttbox} |
103 | 563 |
\hrule |
564 |
\caption{Defining lists of $n$ elements} \label{listn-fig} |
|
565 |
\end{figure} |
|
566 |
||
355 | 567 |
The Isabelle/ZF version of this example suggests a general treatment of |
568 |
varying parameters. Here, we use the existing datatype definition of |
|
569 |
$\lst(A)$, with constructors $\Nil$ and~$\Cons$. Then incorporate the |
|
570 |
parameter~$n$ into the inductive set itself, defining $\listn(A)$ as a |
|
571 |
relation. It consists of pairs $\pair{n,l}$ such that $n\in\nat$ |
|
572 |
and~$l\in\lst(A)$ and $l$ has length~$n$. In fact, $\listn(A)$ is the |
|
573 |
converse of the length function on~$\lst(A)$. The Isabelle/ZF introduction |
|
574 |
rules are |
|
103 | 575 |
\[ \pair{0,\Nil}\in\listn(A) \qquad |
576 |
\infer{\pair{\succ(n),\Cons(a,l)}\in\listn(A)} |
|
577 |
{a\in A & \pair{n,l}\in\listn(A)} |
|
578 |
\] |
|
579 |
Figure~\ref{listn-fig} presents the ML invocation. A theory of lists, |
|
580 |
extended with a declaration of $\listn$, is the parent theory. The domain |
|
581 |
is specified as $\nat\times\lst(A)$. The type-checking rules include those |
|
582 |
for 0, $\succ$, $\Nil$ and $\Cons$. Because $\listn(A)$ is a set of pairs, |
|
583 |
type-checking also requires introduction and elimination rules to express |
|
584 |
both directions of the equivalence $\pair{a,b}\in A\times B \bimp a\in A |
|
585 |
\conj b\in B$. |
|
586 |
||
587 |
The package returns introduction, elimination and induction rules for |
|
588 |
$\listn$. The basic induction rule, {\tt ListN.induct}, is |
|
589 |
\[ \infer{P(x)}{x\in\listn(A) & P(\pair{0,\Nil}) & |
|
590 |
\infer*{P(\pair{\succ(n),\Cons(a,l)})} |
|
591 |
{[a\in A & \pair{n,l}\in\listn(A) & P(\pair{n,l})]_{a,l,n}}} |
|
592 |
\] |
|
593 |
This rule requires the induction formula to be a |
|
594 |
unary property of pairs,~$P(\pair{n,l})$. The alternative rule, {\tt |
|
595 |
ListN.mutual\_induct}, uses a binary property instead: |
|
130 | 596 |
\[ \infer{\forall n\,l. \pair{n,l}\in\listn(A) \imp P(n,l)} |
103 | 597 |
{P(0,\Nil) & |
598 |
\infer*{P(\succ(n),\Cons(a,l))} |
|
599 |
{[a\in A & \pair{n,l}\in\listn(A) & P(n,l)]_{a,l,n}}} |
|
600 |
\] |
|
601 |
It is now a simple matter to prove theorems about $\listn(A)$, such as |
|
602 |
\[ \forall l\in\lst(A). \pair{\length(l),\, l}\in\listn(A) \] |
|
603 |
\[ \listn(A)``\{n\} = \{l\in\lst(A). \length(l)=n\} \] |
|
130 | 604 |
This latter result --- here $r``X$ denotes the image of $X$ under $r$ |
103 | 605 |
--- asserts that the inductive definition agrees with the obvious notion of |
606 |
$n$-element list. |
|
607 |
||
608 |
Unlike in Coq, the definition does not declare a new datatype. A `list of |
|
130 | 609 |
$n$ elements' really is a list and is subject to list operators such |
610 |
as append (concatenation). For example, a trivial induction on |
|
611 |
$\pair{m,l}\in\listn(A)$ yields |
|
103 | 612 |
\[ \infer{\pair{m\mathbin{+} m,\, l@l'}\in\listn(A)} |
613 |
{\pair{m,l}\in\listn(A) & \pair{m',l'}\in\listn(A)} |
|
614 |
\] |
|
615 |
where $+$ here denotes addition on the natural numbers and @ denotes append. |
|
616 |
||
355 | 617 |
\subsection{A demonstration of rule inversion}\label{mkcases} |
103 | 618 |
The elimination rule, {\tt ListN.elim}, is cumbersome: |
619 |
\[ \infer{Q}{x\in\listn(A) & |
|
620 |
\infer*{Q}{[x = \pair{0,\Nil}]} & |
|
621 |
\infer*{Q} |
|
622 |
{\left[\begin{array}{l} |
|
623 |
x = \pair{\succ(n),\Cons(a,l)} \\ |
|
624 |
a\in A \\ |
|
625 |
\pair{n,l}\in\listn(A) |
|
626 |
\end{array} \right]_{a,l,n}}} |
|
627 |
\] |
|
179 | 628 |
The ML function {\tt ListN.mk\_cases} generates simplified instances of |
629 |
this rule. It works by freeness reasoning on the list constructors: |
|
630 |
$\Cons(a,l)$ is injective in its two arguments and differs from~$\Nil$. If |
|
631 |
$x$ is $\pair{i,\Nil}$ or $\pair{i,\Cons(a,l)}$ then {\tt ListN.mk\_cases} |
|
355 | 632 |
deduces the corresponding form of~$i$; this is called rule inversion. For |
633 |
example, |
|
103 | 634 |
\begin{ttbox} |
635 |
ListN.mk_cases List.con_defs "<i,Cons(a,l)> : listn(A)" |
|
636 |
\end{ttbox} |
|
130 | 637 |
yields a rule with only two premises: |
103 | 638 |
\[ \infer{Q}{\pair{i, \Cons(a,l)}\in\listn(A) & |
639 |
\infer*{Q} |
|
640 |
{\left[\begin{array}{l} |
|
641 |
i = \succ(n) \\ a\in A \\ \pair{n,l}\in\listn(A) |
|
642 |
\end{array} \right]_{n}}} |
|
643 |
\] |
|
644 |
The package also has built-in rules for freeness reasoning about $0$ |
|
645 |
and~$\succ$. So if $x$ is $\pair{0,l}$ or $\pair{\succ(i),l}$, then {\tt |
|
646 |
ListN.mk\_cases} can similarly deduce the corresponding form of~$l$. |
|
647 |
||
355 | 648 |
The function {\tt mk\_cases} is also useful with datatype definitions. The |
649 |
instance from the definition of lists, namely {\tt List.mk\_cases}, can |
|
650 |
prove the rule |
|
103 | 651 |
\[ \infer{Q}{\Cons(a,l)\in\lst(A) & |
652 |
& \infer*{Q}{[a\in A &l\in\lst(A)]} } |
|
653 |
\] |
|
355 | 654 |
A typical use of {\tt mk\_cases} concerns inductive definitions of |
655 |
evaluation relations. Then rule inversion yields case analysis on possible |
|
656 |
evaluations. For example, the Isabelle/ZF theory includes a short proof |
|
657 |
of the diamond property for parallel contraction on combinators. |
|
103 | 658 |
|
130 | 659 |
\subsection{A coinductive definition: bisimulations on lazy lists} |
660 |
This example anticipates the definition of the codatatype $\llist(A)$, which |
|
661 |
consists of finite and infinite lists over~$A$. Its constructors are $\LNil$ |
|
662 |
and |
|
663 |
$\LCons$, satisfying the introduction rules shown in~\S\ref{coind-sec}. |
|
103 | 664 |
Because $\llist(A)$ is defined as a greatest fixedpoint and uses the variant |
665 |
pairing and injection operators, it contains non-well-founded elements such as |
|
666 |
solutions to $\LCons(a,l)=l$. |
|
667 |
||
130 | 668 |
The next step in the development of lazy lists is to define a coinduction |
103 | 669 |
principle for proving equalities. This is done by showing that the equality |
670 |
relation on lazy lists is the greatest fixedpoint of some monotonic |
|
671 |
operation. The usual approach~\cite{pitts94} is to define some notion of |
|
672 |
bisimulation for lazy lists, define equivalence to be the greatest |
|
673 |
bisimulation, and finally to prove that two lazy lists are equivalent if and |
|
130 | 674 |
only if they are equal. The coinduction rule for equivalence then yields a |
675 |
coinduction principle for equalities. |
|
103 | 676 |
|
677 |
A binary relation $R$ on lazy lists is a {\bf bisimulation} provided $R\sbs |
|
678 |
R^+$, where $R^+$ is the relation |
|
130 | 679 |
\[ \{\pair{\LNil,\LNil}\} \un |
680 |
\{\pair{\LCons(a,l),\LCons(a,l')} . a\in A \conj \pair{l,l'}\in R\}. |
|
103 | 681 |
\] |
682 |
||
683 |
A pair of lazy lists are {\bf equivalent} if they belong to some bisimulation. |
|
130 | 684 |
Equivalence can be coinductively defined as the greatest fixedpoint for the |
103 | 685 |
introduction rules |
130 | 686 |
\[ \pair{\LNil,\LNil} \in\lleq(A) \qquad |
687 |
\infer[(-)]{\pair{\LCons(a,l),\LCons(a,l')} \in\lleq(A)} |
|
688 |
{a\in A & \pair{l,l'}\in \lleq(A)} |
|
103 | 689 |
\] |
130 | 690 |
To make this coinductive definition, we invoke \verb|CoInductive_Fun|: |
103 | 691 |
\begin{ttbox} |
130 | 692 |
structure LList_Eq = CoInductive_Fun |
497
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
693 |
(val thy = LList.thy |> add_consts [("lleq","i=>i",NoSyn)] |
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
694 |
val thy_name = "LList_Eq" |
355 | 695 |
val rec_doms = [("lleq", "llist(A) * llist(A)")] |
696 |
val sintrs = |
|
697 |
["<LNil, LNil> : lleq(A)", |
|
698 |
"[| a:A; <l,l'>: lleq(A) |] ==> <LCons(a,l),LCons(a,l')>: lleq(A)"] |
|
699 |
val monos = [] |
|
700 |
val con_defs = [] |
|
497
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
701 |
val type_intrs = LList.intrs |
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
702 |
val type_elims = []); |
103 | 703 |
\end{ttbox} |
704 |
Again, {\tt addconsts} declares a constant for $\lleq$ in the parent theory. |
|
130 | 705 |
The domain of $\lleq(A)$ is $\llist(A)\times\llist(A)$. The type-checking |
706 |
rules include the introduction rules for lazy lists as well as rules |
|
707 |
for both directions of the equivalence |
|
708 |
$\pair{a,b}\in A\times B \bimp a\in A \conj b\in B$. |
|
103 | 709 |
|
710 |
The package returns the introduction rules and the elimination rule, as |
|
130 | 711 |
usual. But instead of induction rules, it returns a coinduction rule. |
103 | 712 |
The rule is too big to display in the usual notation; its conclusion is |
130 | 713 |
$x\in\lleq(A)$ and its premises are $x\in X$, |
714 |
${X\sbs\llist(A)\times\llist(A)}$ and |
|
715 |
\[ \infer*{z=\pair{\LNil,\LNil}\disj \bigl(\exists a\,l\,l'.\, |
|
355 | 716 |
z=\pair{\LCons(a,l),\LCons(a,l')} \conj |
717 |
a\in A \conj\pair{l,l'}\in X\un\lleq(A) \bigr) |
|
718 |
% \begin{array}[t]{@{}l} |
|
719 |
% z=\pair{\LCons(a,l),\LCons(a,l')} \conj a\in A \conj{}\\ |
|
720 |
% \pair{l,l'}\in X\un\lleq(A) \bigr) |
|
721 |
% \end{array} |
|
722 |
}{[z\in X]_z} |
|
103 | 723 |
\] |
130 | 724 |
Thus if $x\in X$, where $X$ is a bisimulation contained in the |
725 |
domain of $\lleq(A)$, then $x\in\lleq(A)$. It is easy to show that |
|
103 | 726 |
$\lleq(A)$ is reflexive: the equality relation is a bisimulation. And |
727 |
$\lleq(A)$ is symmetric: its converse is a bisimulation. But showing that |
|
130 | 728 |
$\lleq(A)$ coincides with the equality relation takes some work. |
103 | 729 |
|
730 |
\subsection{The accessible part of a relation}\label{acc-sec} |
|
731 |
Let $\prec$ be a binary relation on~$D$; in short, $(\prec)\sbs D\times D$. |
|
732 |
The {\bf accessible} or {\bf well-founded} part of~$\prec$, written |
|
733 |
$\acc(\prec)$, is essentially that subset of~$D$ for which $\prec$ admits |
|
734 |
no infinite decreasing chains~\cite{aczel77}. Formally, $\acc(\prec)$ is |
|
735 |
inductively defined to be the least set that contains $a$ if it contains |
|
736 |
all $\prec$-predecessors of~$a$, for $a\in D$. Thus we need an |
|
737 |
introduction rule of the form |
|
738 |
\[ \infer{a\in\acc(\prec)}{\forall y.y\prec a\imp y\in\acc(\prec)} \] |
|
739 |
Paulin-Mohring treats this example in Coq~\cite{paulin92}, but it causes |
|
740 |
difficulties for other systems. Its premise does not conform to |
|
741 |
the structure of introduction rules for HOL's inductive definition |
|
742 |
package~\cite{camilleri92}. It is also unacceptable to Isabelle package |
|
130 | 743 |
(\S\ref{intro-sec}), but fortunately can be transformed into the acceptable |
103 | 744 |
form $t\in M(R)$. |
745 |
||
746 |
The powerset operator is monotonic, and $t\in\pow(R)$ is equivalent to |
|
747 |
$t\sbs R$. This in turn is equivalent to $\forall y\in t. y\in R$. To |
|
748 |
express $\forall y.y\prec a\imp y\in\acc(\prec)$ we need only find a |
|
749 |
term~$t$ such that $y\in t$ if and only if $y\prec a$. A suitable $t$ is |
|
750 |
the inverse image of~$\{a\}$ under~$\prec$. |
|
751 |
||
752 |
The ML invocation below follows this approach. Here $r$ is~$\prec$ and |
|
130 | 753 |
$\field(r)$ refers to~$D$, the domain of $\acc(r)$. (The field of a |
754 |
relation is the union of its domain and range.) Finally |
|
755 |
$r^{-}``\{a\}$ denotes the inverse image of~$\{a\}$ under~$r$. The package is |
|
756 |
supplied the theorem {\tt Pow\_mono}, which asserts that $\pow$ is monotonic. |
|
103 | 757 |
\begin{ttbox} |
758 |
structure Acc = Inductive_Fun |
|
497
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
759 |
(val thy = WF.thy |> add_consts [("acc","i=>i",NoSyn)] |
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
760 |
val thy_name = "Acc" |
355 | 761 |
val rec_doms = [("acc", "field(r)")] |
762 |
val sintrs = ["[| r-``\{a\}:\,Pow(acc(r)); a:\,field(r) |] ==> a:\,acc(r)"] |
|
763 |
val monos = [Pow_mono] |
|
764 |
val con_defs = [] |
|
765 |
val type_intrs = [] |
|
103 | 766 |
val type_elims = []); |
767 |
\end{ttbox} |
|
768 |
The Isabelle theory proceeds to prove facts about $\acc(\prec)$. For |
|
769 |
instance, $\prec$ is well-founded if and only if its field is contained in |
|
770 |
$\acc(\prec)$. |
|
771 |
||
772 |
As mentioned in~\S\ref{basic-ind-sec}, a premise of the form $t\in M(R)$ |
|
773 |
gives rise to an unusual induction hypothesis. Let us examine the |
|
774 |
induction rule, {\tt Acc.induct}: |
|
775 |
\[ \infer{P(x)}{x\in\acc(r) & |
|
776 |
\infer*{P(a)}{[r^{-}``\{a\}\in\pow(\{z\in\acc(r).P(z)\}) & |
|
777 |
a\in\field(r)]_a}} |
|
778 |
\] |
|
779 |
The strange induction hypothesis is equivalent to |
|
780 |
$\forall y. \pair{y,a}\in r\imp y\in\acc(r)\conj P(y)$. |
|
781 |
Therefore the rule expresses well-founded induction on the accessible part |
|
782 |
of~$\prec$. |
|
783 |
||
784 |
The use of inverse image is not essential. The Isabelle package can accept |
|
785 |
introduction rules with arbitrary premises of the form $\forall |
|
786 |
\vec{y}.P(\vec{y})\imp f(\vec{y})\in R$. The premise can be expressed |
|
787 |
equivalently as |
|
130 | 788 |
\[ \{z\in D. P(\vec{y}) \conj z=f(\vec{y})\} \in \pow(R) \] |
103 | 789 |
provided $f(\vec{y})\in D$ for all $\vec{y}$ such that~$P(\vec{y})$. The |
790 |
following section demonstrates another use of the premise $t\in M(R)$, |
|
791 |
where $M=\lst$. |
|
792 |
||
793 |
\subsection{The primitive recursive functions}\label{primrec-sec} |
|
794 |
The primitive recursive functions are traditionally defined inductively, as |
|
795 |
a subset of the functions over the natural numbers. One difficulty is that |
|
796 |
functions of all arities are taken together, but this is easily |
|
797 |
circumvented by regarding them as functions on lists. Another difficulty, |
|
798 |
the notion of composition, is less easily circumvented. |
|
799 |
||
800 |
Here is a more precise definition. Letting $\vec{x}$ abbreviate |
|
801 |
$x_0,\ldots,x_{n-1}$, we can write lists such as $[\vec{x}]$, |
|
802 |
$[y+1,\vec{x}]$, etc. A function is {\bf primitive recursive} if it |
|
803 |
belongs to the least set of functions in $\lst(\nat)\to\nat$ containing |
|
804 |
\begin{itemize} |
|
805 |
\item The {\bf successor} function $\SC$, such that $\SC[y,\vec{x}]=y+1$. |
|
806 |
\item All {\bf constant} functions $\CONST(k)$, such that |
|
807 |
$\CONST(k)[\vec{x}]=k$. |
|
808 |
\item All {\bf projection} functions $\PROJ(i)$, such that |
|
809 |
$\PROJ(i)[\vec{x}]=x_i$ if $0\leq i<n$. |
|
810 |
\item All {\bf compositions} $\COMP(g,[f_0,\ldots,f_{m-1}])$, |
|
811 |
where $g$ and $f_0$, \ldots, $f_{m-1}$ are primitive recursive, |
|
812 |
such that |
|
813 |
\begin{eqnarray*} |
|
814 |
\COMP(g,[f_0,\ldots,f_{m-1}])[\vec{x}] & = & |
|
815 |
g[f_0[\vec{x}],\ldots,f_{m-1}[\vec{x}]]. |
|
816 |
\end{eqnarray*} |
|
817 |
||
818 |
\item All {\bf recursions} $\PREC(f,g)$, where $f$ and $g$ are primitive |
|
819 |
recursive, such that |
|
820 |
\begin{eqnarray*} |
|
821 |
\PREC(f,g)[0,\vec{x}] & = & f[\vec{x}] \\ |
|
822 |
\PREC(f,g)[y+1,\vec{x}] & = & g[\PREC(f,g)[y,\vec{x}],\, y,\, \vec{x}]. |
|
823 |
\end{eqnarray*} |
|
824 |
\end{itemize} |
|
825 |
Composition is awkward because it combines not two functions, as is usual, |
|
826 |
but $m+1$ functions. In her proof that Ackermann's function is not |
|
827 |
primitive recursive, Nora Szasz was unable to formalize this definition |
|
828 |
directly~\cite{szasz93}. So she generalized primitive recursion to |
|
829 |
tuple-valued functions. This modified the inductive definition such that |
|
830 |
each operation on primitive recursive functions combined just two functions. |
|
831 |
||
832 |
\begin{figure} |
|
355 | 833 |
\begin{ttbox} |
103 | 834 |
structure Primrec = Inductive_Fun |
355 | 835 |
(val thy = Primrec0.thy |
497
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
836 |
val thy_name = "Primrec" |
355 | 837 |
val rec_doms = [("primrec", "list(nat)->nat")] |
838 |
val sintrs = |
|
839 |
["SC : primrec", |
|
840 |
"k: nat ==> CONST(k) : primrec", |
|
841 |
"i: nat ==> PROJ(i) : primrec", |
|
842 |
"[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec", |
|
843 |
"[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"] |
|
844 |
val monos = [list_mono] |
|
845 |
val con_defs = [SC_def,CONST_def,PROJ_def,COMP_def,PREC_def] |
|
846 |
val type_intrs = pr0_typechecks |
|
103 | 847 |
val type_elims = []); |
355 | 848 |
\end{ttbox} |
103 | 849 |
\hrule |
850 |
\caption{Inductive definition of the primitive recursive functions} |
|
851 |
\label{primrec-fig} |
|
852 |
\end{figure} |
|
853 |
\def\fs{{\it fs}} |
|
854 |
Szasz was using ALF, but Coq and HOL would also have problems accepting |
|
855 |
this definition. Isabelle's package accepts it easily since |
|
856 |
$[f_0,\ldots,f_{m-1}]$ is a list of primitive recursive functions and |
|
857 |
$\lst$ is monotonic. There are five introduction rules, one for each of |
|
355 | 858 |
the five forms of primitive recursive function. Let us examine the one for |
859 |
$\COMP$: |
|
103 | 860 |
\[ \infer{\COMP(g,\fs)\in\primrec}{g\in\primrec & \fs\in\lst(\primrec)} \] |
861 |
The induction rule for $\primrec$ has one case for each introduction rule. |
|
862 |
Due to the use of $\lst$ as a monotone operator, the composition case has |
|
863 |
an unusual induction hypothesis: |
|
864 |
\[ \infer*{P(\COMP(g,\fs))} |
|
130 | 865 |
{[g\in\primrec & \fs\in\lst(\{z\in\primrec.P(z)\})]_{\fs,g}} \] |
103 | 866 |
The hypothesis states that $\fs$ is a list of primitive recursive functions |
867 |
satisfying the induction formula. Proving the $\COMP$ case typically requires |
|
868 |
structural induction on lists, yielding two subcases: either $\fs=\Nil$ or |
|
869 |
else $\fs=\Cons(f,\fs')$, where $f\in\primrec$, $P(f)$, and $\fs'$ is |
|
870 |
another list of primitive recursive functions satisfying~$P$. |
|
871 |
||
872 |
Figure~\ref{primrec-fig} presents the ML invocation. Theory {\tt |
|
355 | 873 |
Primrec0.thy} defines the constants $\SC$, $\CONST$, etc. These are not |
874 |
constructors of a new datatype, but functions over lists of numbers. Their |
|
875 |
definitions, which are omitted, consist of routine list programming. In |
|
876 |
Isabelle/ZF, the primitive recursive functions are defined as a subset of |
|
877 |
the function set $\lst(\nat)\to\nat$. |
|
103 | 878 |
|
355 | 879 |
The Isabelle theory goes on to formalize Ackermann's function and prove |
880 |
that it is not primitive recursive, using the induction rule {\tt |
|
881 |
Primrec.induct}. The proof follows Szasz's excellent account. |
|
103 | 882 |
|
883 |
||
130 | 884 |
\section{Datatypes and codatatypes}\label{data-sec} |
885 |
A (co)datatype definition is a (co)inductive definition with automatically |
|
355 | 886 |
defined constructors and a case analysis operator. The package proves that |
887 |
the case operator inverts the constructors and can prove freeness theorems |
|
103 | 888 |
involving any pair of constructors. |
889 |
||
890 |
||
130 | 891 |
\subsection{Constructors and their domain}\label{univ-sec} |
355 | 892 |
Conceptually, our two forms of definition are distinct. A (co)inductive |
893 |
definition selects a subset of an existing set; a (co)datatype definition |
|
894 |
creates a new set. But the package reduces the latter to the former. A |
|
895 |
set having strong closure properties must serve as the domain of the |
|
896 |
(co)inductive definition. Constructing this set requires some theoretical |
|
897 |
effort, which must be done anyway to show that (co)datatypes exist. It is |
|
898 |
not obvious that standard set theory is suitable for defining codatatypes. |
|
103 | 899 |
|
900 |
Isabelle/ZF defines the standard notion of Cartesian product $A\times B$, |
|
901 |
containing ordered pairs $\pair{a,b}$. Now the $m$-tuple |
|
355 | 902 |
$\pair{x_1,\ldots,x_m}$ is the empty set~$\emptyset$ if $m=0$, simply |
903 |
$x_1$ if $m=1$ and $\pair{x_1,\pair{x_2,\ldots,x_m}}$ if $m\geq2$. |
|
103 | 904 |
Isabelle/ZF also defines the disjoint sum $A+B$, containing injections |
905 |
$\Inl(a)\equiv\pair{0,a}$ and $\Inr(b)\equiv\pair{1,b}$. |
|
906 |
||
355 | 907 |
A datatype constructor $\Con(x_1,\ldots,x_m)$ is defined to be |
908 |
$h(\pair{x_1,\ldots,x_m})$, where $h$ is composed of $\Inl$ and~$\Inr$. |
|
103 | 909 |
In a mutually recursive definition, all constructors for the set~$R_i$ have |
130 | 910 |
the outer form~$h_{in}$, where $h_{in}$ is the injection described |
103 | 911 |
in~\S\ref{mutual-sec}. Further nested injections ensure that the |
912 |
constructors for~$R_i$ are pairwise distinct. |
|
913 |
||
914 |
Isabelle/ZF defines the set $\univ(A)$, which contains~$A$ and |
|
915 |
furthermore contains $\pair{a,b}$, $\Inl(a)$ and $\Inr(b)$ for $a$, |
|
916 |
$b\in\univ(A)$. In a typical datatype definition with set parameters |
|
917 |
$A_1$, \ldots, $A_k$, a suitable domain for all the recursive sets is |
|
918 |
$\univ(A_1\un\cdots\un A_k)$. This solves the problem for |
|
919 |
datatypes~\cite[\S4.2]{paulson-set-II}. |
|
920 |
||
921 |
The standard pairs and injections can only yield well-founded |
|
922 |
constructions. This eases the (manual!) definition of recursive functions |
|
130 | 923 |
over datatypes. But they are unsuitable for codatatypes, which typically |
103 | 924 |
contain non-well-founded objects. |
925 |
||
130 | 926 |
To support codatatypes, Isabelle/ZF defines a variant notion of ordered |
103 | 927 |
pair, written~$\pair{a;b}$. It also defines the corresponding variant |
928 |
notion of Cartesian product $A\otimes B$, variant injections $\QInl(a)$ |
|
355 | 929 |
and~$\QInr(b)$ and variant disjoint sum $A\oplus B$. Finally it defines |
103 | 930 |
the set $\quniv(A)$, which contains~$A$ and furthermore contains |
931 |
$\pair{a;b}$, $\QInl(a)$ and $\QInr(b)$ for $a$, $b\in\quniv(A)$. In a |
|
130 | 932 |
typical codatatype definition with set parameters $A_1$, \ldots, $A_k$, a |
933 |
suitable domain is $\quniv(A_1\un\cdots\un A_k)$. This approach using |
|
355 | 934 |
standard ZF set theory~\cite{paulson-final} is an alternative to adopting |
935 |
Aczel's Anti-Foundation Axiom~\cite{aczel88}. |
|
103 | 936 |
|
937 |
\subsection{The case analysis operator} |
|
130 | 938 |
The (co)datatype package automatically defines a case analysis operator, |
179 | 939 |
called {\tt$R$\_case}. A mutually recursive definition still has only one |
940 |
operator, whose name combines those of the recursive sets: it is called |
|
941 |
{\tt$R_1$\_\ldots\_$R_n$\_case}. The case operator is analogous to those |
|
942 |
for products and sums. |
|
103 | 943 |
|
944 |
Datatype definitions employ standard products and sums, whose operators are |
|
945 |
$\split$ and $\case$ and satisfy the equations |
|
946 |
\begin{eqnarray*} |
|
947 |
\split(f,\pair{x,y}) & = & f(x,y) \\ |
|
948 |
\case(f,g,\Inl(x)) & = & f(x) \\ |
|
949 |
\case(f,g,\Inr(y)) & = & g(y) |
|
950 |
\end{eqnarray*} |
|
951 |
Suppose the datatype has $k$ constructors $\Con_1$, \ldots,~$\Con_k$. Then |
|
952 |
its case operator takes $k+1$ arguments and satisfies an equation for each |
|
953 |
constructor: |
|
954 |
\begin{eqnarray*} |
|
955 |
R\hbox{\_case}(f_1,\ldots,f_k, {\tt Con}_i(\vec{x})) & = & f_i(\vec{x}), |
|
956 |
\qquad i = 1, \ldots, k |
|
957 |
\end{eqnarray*} |
|
130 | 958 |
The case operator's definition takes advantage of Isabelle's representation |
959 |
of syntax in the typed $\lambda$-calculus; it could readily be adapted to a |
|
960 |
theorem prover for higher-order logic. If $f$ and~$g$ have meta-type |
|
961 |
$i\To i$ then so do $\split(f)$ and |
|
962 |
$\case(f,g)$. This works because $\split$ and $\case$ operate on their last |
|
963 |
argument. They are easily combined to make complex case analysis |
|
103 | 964 |
operators. Here are two examples: |
965 |
\begin{itemize} |
|
966 |
\item $\split(\lambda x.\split(f(x)))$ performs case analysis for |
|
967 |
$A\times (B\times C)$, as is easily verified: |
|
968 |
\begin{eqnarray*} |
|
969 |
\split(\lambda x.\split(f(x)), \pair{a,b,c}) |
|
970 |
& = & (\lambda x.\split(f(x))(a,\pair{b,c}) \\ |
|
971 |
& = & \split(f(a), \pair{b,c}) \\ |
|
972 |
& = & f(a,b,c) |
|
973 |
\end{eqnarray*} |
|
974 |
||
975 |
\item $\case(f,\case(g,h))$ performs case analysis for $A+(B+C)$; let us |
|
976 |
verify one of the three equations: |
|
977 |
\begin{eqnarray*} |
|
978 |
\case(f,\case(g,h), \Inr(\Inl(b))) |
|
979 |
& = & \case(g,h,\Inl(b)) \\ |
|
980 |
& = & g(b) |
|
981 |
\end{eqnarray*} |
|
982 |
\end{itemize} |
|
130 | 983 |
Codatatype definitions are treated in precisely the same way. They express |
103 | 984 |
case operators using those for the variant products and sums, namely |
985 |
$\qsplit$ and~$\qcase$. |
|
986 |
||
355 | 987 |
\medskip |
103 | 988 |
|
355 | 989 |
\ifCADE The package has processed all the datatypes discussed in |
990 |
my earlier paper~\cite{paulson-set-II} and the codatatype of lazy lists. |
|
991 |
Space limitations preclude discussing these examples here, but they are |
|
992 |
distributed with Isabelle. \typeout{****Omitting datatype examples from |
|
993 |
CADE version!} \else |
|
103 | 994 |
|
995 |
To see how constructors and the case analysis operator are defined, let us |
|
996 |
examine some examples. These include lists and trees/forests, which I have |
|
997 |
discussed extensively in another paper~\cite{paulson-set-II}. |
|
998 |
||
999 |
\begin{figure} |
|
1000 |
\begin{ttbox} |
|
1001 |
structure List = Datatype_Fun |
|
355 | 1002 |
(val thy = Univ.thy |
497
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
1003 |
val thy_name = "List" |
355 | 1004 |
val rec_specs = [("list", "univ(A)", |
497
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
1005 |
[(["Nil"], "i", NoSyn), |
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
1006 |
(["Cons"], "[i,i]=>i", NoSyn)])] |
355 | 1007 |
val rec_styp = "i=>i" |
1008 |
val sintrs = ["Nil : list(A)", |
|
1009 |
"[| a: A; l: list(A) |] ==> Cons(a,l) : list(A)"] |
|
1010 |
val monos = [] |
|
1011 |
val type_intrs = datatype_intrs |
|
103 | 1012 |
val type_elims = datatype_elims); |
1013 |
\end{ttbox} |
|
1014 |
\hrule |
|
1015 |
\caption{Defining the datatype of lists} \label{list-fig} |
|
1016 |
||
1017 |
\medskip |
|
1018 |
\begin{ttbox} |
|
130 | 1019 |
structure LList = CoDatatype_Fun |
355 | 1020 |
(val thy = QUniv.thy |
497
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
1021 |
val thy_name = "LList" |
355 | 1022 |
val rec_specs = [("llist", "quniv(A)", |
497
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
1023 |
[(["LNil"], "i", NoSyn), |
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
1024 |
(["LCons"], "[i,i]=>i", NoSyn)])] |
355 | 1025 |
val rec_styp = "i=>i" |
1026 |
val sintrs = ["LNil : llist(A)", |
|
1027 |
"[| a: A; l: llist(A) |] ==> LCons(a,l) : llist(A)"] |
|
1028 |
val monos = [] |
|
1029 |
val type_intrs = codatatype_intrs |
|
130 | 1030 |
val type_elims = codatatype_elims); |
103 | 1031 |
\end{ttbox} |
1032 |
\hrule |
|
130 | 1033 |
\caption{Defining the codatatype of lazy lists} \label{llist-fig} |
103 | 1034 |
\end{figure} |
1035 |
||
1036 |
\subsection{Example: lists and lazy lists} |
|
1037 |
Figures \ref{list-fig} and~\ref{llist-fig} present the ML definitions of |
|
1038 |
lists and lazy lists, respectively. They highlight the (many) similarities |
|
130 | 1039 |
and (few) differences between datatype and codatatype definitions. |
103 | 1040 |
|
1041 |
Each form of list has two constructors, one for the empty list and one for |
|
1042 |
adding an element to a list. Each takes a parameter, defining the set of |
|
1043 |
lists over a given set~$A$. Each uses the appropriate domain from a |
|
1044 |
Isabelle/ZF theory: |
|
1045 |
\begin{itemize} |
|
1046 |
\item $\lst(A)$ specifies domain $\univ(A)$ and parent theory {\tt Univ.thy}. |
|
1047 |
||
1048 |
\item $\llist(A)$ specifies domain $\quniv(A)$ and parent theory {\tt |
|
1049 |
QUniv.thy}. |
|
1050 |
\end{itemize} |
|
1051 |
||
130 | 1052 |
Since $\lst(A)$ is a datatype, it enjoys a structural induction rule, {\tt |
1053 |
List.induct}: |
|
103 | 1054 |
\[ \infer{P(x)}{x\in\lst(A) & P(\Nil) |
1055 |
& \infer*{P(\Cons(a,l))}{[a\in A & l\in\lst(A) & P(l)]_{a,l}} } |
|
1056 |
\] |
|
1057 |
Induction and freeness yield the law $l\not=\Cons(a,l)$. To strengthen this, |
|
1058 |
Isabelle/ZF defines the rank of a set and proves that the standard pairs and |
|
1059 |
injections have greater rank than their components. An immediate consequence, |
|
1060 |
which justifies structural recursion on lists \cite[\S4.3]{paulson-set-II}, |
|
1061 |
is |
|
1062 |
\[ \rank(l) < \rank(\Cons(a,l)). \] |
|
1063 |
||
130 | 1064 |
Since $\llist(A)$ is a codatatype, it has no induction rule. Instead it has |
1065 |
the coinduction rule shown in \S\ref{coind-sec}. Since variant pairs and |
|
103 | 1066 |
injections are monotonic and need not have greater rank than their |
1067 |
components, fixedpoint operators can create cyclic constructions. For |
|
1068 |
example, the definition |
|
1069 |
\begin{eqnarray*} |
|
1070 |
\lconst(a) & \equiv & \lfp(\univ(a), \lambda l. \LCons(a,l)) |
|
1071 |
\end{eqnarray*} |
|
1072 |
yields $\lconst(a) = \LCons(a,\lconst(a))$. |
|
1073 |
||
1074 |
\medskip |
|
1075 |
It may be instructive to examine the definitions of the constructors and |
|
1076 |
case operator for $\lst(A)$. The definitions for $\llist(A)$ are similar. |
|
1077 |
The list constructors are defined as follows: |
|
1078 |
\begin{eqnarray*} |
|
1079 |
\Nil & = & \Inl(\emptyset) \\ |
|
1080 |
\Cons(a,l) & = & \Inr(\pair{a,l}) |
|
1081 |
\end{eqnarray*} |
|
1082 |
The operator $\lstcase$ performs case analysis on these two alternatives: |
|
1083 |
\begin{eqnarray*} |
|
1084 |
\lstcase(c,h) & \equiv & \case(\lambda u.c, \split(h)) |
|
1085 |
\end{eqnarray*} |
|
1086 |
Let us verify the two equations: |
|
1087 |
\begin{eqnarray*} |
|
1088 |
\lstcase(c, h, \Nil) & = & |
|
1089 |
\case(\lambda u.c, \split(h), \Inl(\emptyset)) \\ |
|
1090 |
& = & (\lambda u.c)(\emptyset) \\ |
|
130 | 1091 |
& = & c\\[1ex] |
103 | 1092 |
\lstcase(c, h, \Cons(x,y)) & = & |
1093 |
\case(\lambda u.c, \split(h), \Inr(\pair{x,y})) \\ |
|
1094 |
& = & \split(h, \pair{x,y}) \\ |
|
130 | 1095 |
& = & h(x,y) |
103 | 1096 |
\end{eqnarray*} |
1097 |
||
1098 |
\begin{figure} |
|
355 | 1099 |
\begin{ttbox} |
103 | 1100 |
structure TF = Datatype_Fun |
355 | 1101 |
(val thy = Univ.thy |
497
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
1102 |
val thy_name = "TF" |
355 | 1103 |
val rec_specs = [("tree", "univ(A)", |
497
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
1104 |
[(["Tcons"], "[i,i]=>i", NoSyn)]), |
355 | 1105 |
("forest", "univ(A)", |
497
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
1106 |
[(["Fnil"], "i", NoSyn), |
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
1107 |
(["Fcons"], "[i,i]=>i", NoSyn)])] |
355 | 1108 |
val rec_styp = "i=>i" |
1109 |
val sintrs = |
|
1110 |
["[| a:A; f: forest(A) |] ==> Tcons(a,f) : tree(A)", |
|
1111 |
"Fnil : forest(A)", |
|
1112 |
"[| t: tree(A); f: forest(A) |] ==> Fcons(t,f) : forest(A)"] |
|
1113 |
val monos = [] |
|
1114 |
val type_intrs = datatype_intrs |
|
103 | 1115 |
val type_elims = datatype_elims); |
355 | 1116 |
\end{ttbox} |
103 | 1117 |
\hrule |
1118 |
\caption{Defining the datatype of trees and forests} \label{tf-fig} |
|
1119 |
\end{figure} |
|
1120 |
||
1121 |
||
1122 |
\subsection{Example: mutual recursion} |
|
130 | 1123 |
In mutually recursive trees and forests~\cite[\S4.5]{paulson-set-II}, trees |
103 | 1124 |
have the one constructor $\Tcons$, while forests have the two constructors |
1125 |
$\Fnil$ and~$\Fcons$. Figure~\ref{tf-fig} presents the ML |
|
1126 |
definition. It has much in common with that of $\lst(A)$, including its |
|
1127 |
use of $\univ(A)$ for the domain and {\tt Univ.thy} for the parent theory. |
|
1128 |
The three introduction rules define the mutual recursion. The |
|
1129 |
distinguishing feature of this example is its two induction rules. |
|
1130 |
||
1131 |
The basic induction rule is called {\tt TF.induct}: |
|
1132 |
\[ \infer{P(x)}{x\in\TF(A) & |
|
1133 |
\infer*{P(\Tcons(a,f))} |
|
1134 |
{\left[\begin{array}{l} a\in A \\ |
|
1135 |
f\in\forest(A) \\ P(f) |
|
1136 |
\end{array} |
|
1137 |
\right]_{a,f}} |
|
1138 |
& P(\Fnil) |
|
130 | 1139 |
& \infer*{P(\Fcons(t,f))} |
103 | 1140 |
{\left[\begin{array}{l} t\in\tree(A) \\ P(t) \\ |
1141 |
f\in\forest(A) \\ P(f) |
|
1142 |
\end{array} |
|
1143 |
\right]_{t,f}} } |
|
1144 |
\] |
|
1145 |
This rule establishes a single predicate for $\TF(A)$, the union of the |
|
1146 |
recursive sets. |
|
1147 |
||
1148 |
Although such reasoning is sometimes useful |
|
1149 |
\cite[\S4.5]{paulson-set-II}, a proper mutual induction rule should establish |
|
1150 |
separate predicates for $\tree(A)$ and $\forest(A)$. The package calls this |
|
1151 |
rule {\tt TF.mutual\_induct}. Observe the usage of $P$ and $Q$ in the |
|
1152 |
induction hypotheses: |
|
1153 |
\[ \infer{(\forall z. z\in\tree(A)\imp P(z)) \conj |
|
1154 |
(\forall z. z\in\forest(A)\imp Q(z))} |
|
1155 |
{\infer*{P(\Tcons(a,f))} |
|
1156 |
{\left[\begin{array}{l} a\in A \\ |
|
1157 |
f\in\forest(A) \\ Q(f) |
|
1158 |
\end{array} |
|
1159 |
\right]_{a,f}} |
|
1160 |
& Q(\Fnil) |
|
130 | 1161 |
& \infer*{Q(\Fcons(t,f))} |
103 | 1162 |
{\left[\begin{array}{l} t\in\tree(A) \\ P(t) \\ |
1163 |
f\in\forest(A) \\ Q(f) |
|
1164 |
\end{array} |
|
1165 |
\right]_{t,f}} } |
|
1166 |
\] |
|
1167 |
As mentioned above, the package does not define a structural recursion |
|
1168 |
operator. I have described elsewhere how this is done |
|
1169 |
\cite[\S4.5]{paulson-set-II}. |
|
1170 |
||
1171 |
Both forest constructors have the form $\Inr(\cdots)$, |
|
1172 |
while the tree constructor has the form $\Inl(\cdots)$. This pattern would |
|
1173 |
hold regardless of how many tree or forest constructors there were. |
|
1174 |
\begin{eqnarray*} |
|
1175 |
\Tcons(a,l) & = & \Inl(\pair{a,l}) \\ |
|
1176 |
\Fnil & = & \Inr(\Inl(\emptyset)) \\ |
|
1177 |
\Fcons(a,l) & = & \Inr(\Inr(\pair{a,l})) |
|
1178 |
\end{eqnarray*} |
|
1179 |
There is only one case operator; it works on the union of the trees and |
|
1180 |
forests: |
|
1181 |
\begin{eqnarray*} |
|
1182 |
{\tt tree\_forest\_case}(f,c,g) & \equiv & |
|
1183 |
\case(\split(f),\, \case(\lambda u.c, \split(g))) |
|
1184 |
\end{eqnarray*} |
|
1185 |
||
1186 |
\begin{figure} |
|
355 | 1187 |
\begin{ttbox} |
103 | 1188 |
structure Data = Datatype_Fun |
355 | 1189 |
(val thy = Univ.thy |
497
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
1190 |
val thy_name = "Data" |
355 | 1191 |
val rec_specs = [("data", "univ(A Un B)", |
497
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
1192 |
[(["Con0"], "i", NoSyn), |
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
1193 |
(["Con1"], "i=>i", NoSyn), |
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
1194 |
(["Con2"], "[i,i]=>i", NoSyn), |
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
1195 |
(["Con3"], "[i,i,i]=>i", NoSyn)])] |
355 | 1196 |
val rec_styp = "[i,i]=>i" |
1197 |
val sintrs = |
|
1198 |
["Con0 : data(A,B)", |
|
1199 |
"[| a: A |] ==> Con1(a) : data(A,B)", |
|
1200 |
"[| a: A; b: B |] ==> Con2(a,b) : data(A,B)", |
|
1201 |
"[| a: A; b: B; d: data(A,B) |] ==> Con3(a,b,d) : data(A,B)"] |
|
1202 |
val monos = [] |
|
1203 |
val type_intrs = datatype_intrs |
|
103 | 1204 |
val type_elims = datatype_elims); |
355 | 1205 |
\end{ttbox} |
103 | 1206 |
\hrule |
1207 |
\caption{Defining the four-constructor sample datatype} \label{data-fig} |
|
1208 |
\end{figure} |
|
1209 |
||
1210 |
\subsection{A four-constructor datatype} |
|
1211 |
Finally let us consider a fairly general datatype. It has four |
|
130 | 1212 |
constructors $\Con_0$, \ldots, $\Con_3$, with the |
103 | 1213 |
corresponding arities. Figure~\ref{data-fig} presents the ML definition. |
1214 |
Because this datatype has two set parameters, $A$ and~$B$, it specifies |
|
1215 |
$\univ(A\un B)$ as its domain. The structural induction rule has four |
|
1216 |
minor premises, one per constructor: |
|
1217 |
\[ \infer{P(x)}{x\in\data(A,B) & |
|
1218 |
P(\Con_0) & |
|
1219 |
\infer*{P(\Con_1(a))}{[a\in A]_a} & |
|
1220 |
\infer*{P(\Con_2(a,b))} |
|
1221 |
{\left[\begin{array}{l} a\in A \\ b\in B \end{array} |
|
1222 |
\right]_{a,b}} & |
|
1223 |
\infer*{P(\Con_3(a,b,d))} |
|
1224 |
{\left[\begin{array}{l} a\in A \\ b\in B \\ |
|
1225 |
d\in\data(A,B) \\ P(d) |
|
1226 |
\end{array} |
|
1227 |
\right]_{a,b,d}} } |
|
1228 |
\] |
|
1229 |
||
1230 |
The constructor definitions are |
|
1231 |
\begin{eqnarray*} |
|
1232 |
\Con_0 & = & \Inl(\Inl(\emptyset)) \\ |
|
1233 |
\Con_1(a) & = & \Inl(\Inr(a)) \\ |
|
1234 |
\Con_2(a,b) & = & \Inr(\Inl(\pair{a,b})) \\ |
|
1235 |
\Con_3(a,b,c) & = & \Inr(\Inr(\pair{a,b,c})). |
|
1236 |
\end{eqnarray*} |
|
1237 |
The case operator is |
|
1238 |
\begin{eqnarray*} |
|
1239 |
{\tt data\_case}(f_0,f_1,f_2,f_3) & \equiv & |
|
1240 |
\case(\begin{array}[t]{@{}l} |
|
1241 |
\case(\lambda u.f_0,\; f_1),\, \\ |
|
1242 |
\case(\split(f_2),\; \split(\lambda v.\split(f_3(v)))) ) |
|
1243 |
\end{array} |
|
1244 |
\end{eqnarray*} |
|
1245 |
This may look cryptic, but the case equations are trivial to verify. |
|
1246 |
||
1247 |
In the constructor definitions, the injections are balanced. A more naive |
|
1248 |
approach is to define $\Con_3(a,b,c)$ as |
|
1249 |
$\Inr(\Inr(\Inr(\pair{a,b,c})))$; instead, each constructor has two |
|
1250 |
injections. The difference here is small. But the ZF examples include a |
|
1251 |
60-element enumeration type, where each constructor has 5 or~6 injections. |
|
1252 |
The naive approach would require 1 to~59 injections; the definitions would be |
|
1253 |
quadratic in size. It is like the difference between the binary and unary |
|
1254 |
numeral systems. |
|
1255 |
||
130 | 1256 |
The result structure contains the case operator and constructor definitions as |
1257 |
the theorem list \verb|con_defs|. It contains the case equations, such as |
|
103 | 1258 |
\begin{eqnarray*} |
1259 |
{\tt data\_case}(f_0,f_1,f_2,f_3,\Con_3(a,b,c)) & = & f_3(a,b,c), |
|
1260 |
\end{eqnarray*} |
|
1261 |
as the theorem list \verb|case_eqns|. There is one equation per constructor. |
|
1262 |
||
1263 |
\subsection{Proving freeness theorems} |
|
1264 |
There are two kinds of freeness theorems: |
|
1265 |
\begin{itemize} |
|
1266 |
\item {\bf injectiveness} theorems, such as |
|
1267 |
\[ \Con_2(a,b) = \Con_2(a',b') \bimp a=a' \conj b=b' \] |
|
1268 |
||
1269 |
\item {\bf distinctness} theorems, such as |
|
1270 |
\[ \Con_1(a) \not= \Con_2(a',b') \] |
|
1271 |
\end{itemize} |
|
1272 |
Since the number of such theorems is quadratic in the number of constructors, |
|
1273 |
the package does not attempt to prove them all. Instead it returns tools for |
|
1274 |
proving desired theorems --- either explicitly or `on the fly' during |
|
1275 |
simplification or classical reasoning. |
|
1276 |
||
1277 |
The theorem list \verb|free_iffs| enables the simplifier to perform freeness |
|
1278 |
reasoning. This works by incremental unfolding of constructors that appear in |
|
1279 |
equations. The theorem list contains logical equivalences such as |
|
1280 |
\begin{eqnarray*} |
|
1281 |
\Con_0=c & \bimp & c=\Inl(\Inl(\emptyset)) \\ |
|
1282 |
\Con_1(a)=c & \bimp & c=\Inl(\Inr(a)) \\ |
|
1283 |
& \vdots & \\ |
|
1284 |
\Inl(a)=\Inl(b) & \bimp & a=b \\ |
|
130 | 1285 |
\Inl(a)=\Inr(b) & \bimp & {\tt False} \\ |
103 | 1286 |
\pair{a,b} = \pair{a',b'} & \bimp & a=a' \conj b=b' |
1287 |
\end{eqnarray*} |
|
1288 |
For example, these rewrite $\Con_1(a)=\Con_1(b)$ to $a=b$ in four steps. |
|
1289 |
||
1290 |
The theorem list \verb|free_SEs| enables the classical |
|
1291 |
reasoner to perform similar replacements. It consists of elimination rules |
|
355 | 1292 |
to replace $\Con_0=c$ by $c=\Inl(\Inl(\emptyset))$ and so forth, in the |
103 | 1293 |
assumptions. |
1294 |
||
1295 |
Such incremental unfolding combines freeness reasoning with other proof |
|
1296 |
steps. It has the unfortunate side-effect of unfolding definitions of |
|
1297 |
constructors in contexts such as $\exists x.\Con_1(a)=x$, where they should |
|
1298 |
be left alone. Calling the Isabelle tactic {\tt fold\_tac con\_defs} |
|
1299 |
restores the defined constants. |
|
1300 |
\fi %CADE |
|
1301 |
||
355 | 1302 |
\section{Related work}\label{related} |
1303 |
The use of least fixedpoints to express inductive definitions seems |
|
1304 |
obvious. Why, then, has this technique so seldom been implemented? |
|
1305 |
||
1306 |
Most automated logics can only express inductive definitions by asserting |
|
1307 |
new axioms. Little would be left of Boyer and Moore's logic~\cite{bm79} if |
|
1308 |
their shell principle were removed. With ALF the situation is more |
|
1309 |
complex; earlier versions of Martin-L\"of's type theory could (using |
|
1310 |
wellordering types) express datatype definitions, but the version |
|
1311 |
underlying ALF requires new rules for each definition~\cite{dybjer91}. |
|
1312 |
With Coq the situation is subtler still; its underlying Calculus of |
|
1313 |
Constructions can express inductive definitions~\cite{huet88}, but cannot |
|
1314 |
quite handle datatype definitions~\cite{paulin92}. It seems that |
|
1315 |
researchers tried hard to circumvent these problems before finally |
|
1316 |
extending the Calculus with rule schemes for strictly positive operators. |
|
1317 |
||
1318 |
Higher-order logic can express inductive definitions through quantification |
|
1319 |
over unary predicates. The following formula expresses that~$i$ belongs to the |
|
1320 |
least set containing~0 and closed under~$\succ$: |
|
1321 |
\[ \forall P. P(0)\conj (\forall x.P(x)\imp P(\succ(x))) \imp P(i) \] |
|
1322 |
This technique can be used to prove the Knaster-Tarski Theorem, but it is |
|
1323 |
little used in the HOL system. Melham~\cite{melham89} clearly describes |
|
1324 |
the development. The natural numbers are defined as shown above, but lists |
|
1325 |
are defined as functions over the natural numbers. Unlabelled |
|
1326 |
trees are defined using G\"odel numbering; a labelled tree consists of an |
|
1327 |
unlabelled tree paired with a list of labels. Melham's datatype package |
|
1328 |
expresses the user's datatypes in terms of labelled trees. It has been |
|
1329 |
highly successful, but a fixedpoint approach would have yielded greater |
|
1330 |
functionality with less effort. |
|
1331 |
||
1332 |
Melham's inductive definition package~\cite{camilleri92} uses |
|
1333 |
quantification over predicates, which is implicitly a fixedpoint approach. |
|
1334 |
Instead of formalizing the notion of monotone function, it requires |
|
1335 |
definitions to consist of finitary rules, a syntactic form that excludes |
|
1336 |
many monotone inductive definitions. |
|
1337 |
||
1338 |
The earliest use of least fixedpoints is probably Robin Milner's datatype |
|
1339 |
package for Edinburgh LCF~\cite{milner-ind}. Brian Monahan extended this |
|
1340 |
package considerably~\cite{monahan84}, as did I in unpublished |
|
1341 |
work.\footnote{The datatype package described in my LCF |
|
1342 |
book~\cite{paulson87} does {\it not\/} make definitions, but merely |
|
1343 |
asserts axioms. I justified this shortcut on grounds of efficiency: |
|
1344 |
existing packages took tens of minutes to run. Such an explanation would |
|
1345 |
not do today.} |
|
1346 |
LCF is a first-order logic of domain theory; the relevant fixedpoint |
|
1347 |
theorem is not Knaster-Tarski but concerns fixedpoints of continuous |
|
1348 |
functions over domains. LCF is too weak to express recursive predicates. |
|
1349 |
Thus it would appear that the Isabelle/ZF package is the first to be based |
|
1350 |
on the Knaster-Tarski Theorem. |
|
1351 |
||
1352 |
||
103 | 1353 |
\section{Conclusions and future work} |
355 | 1354 |
Higher-order logic and set theory are both powerful enough to express |
1355 |
inductive definitions. A growing number of theorem provers implement one |
|
1356 |
of these~\cite{IMPS,saaltink-fme}. The easiest sort of inductive |
|
1357 |
definition package to write is one that asserts new axioms, not one that |
|
1358 |
makes definitions and proves theorems about them. But asserting axioms |
|
1359 |
could introduce unsoundness. |
|
1360 |
||
1361 |
The fixedpoint approach makes it fairly easy to implement a package for |
|
1362 |
(co)inductive definitions that does not assert axioms. It is efficient: it |
|
103 | 1363 |
processes most definitions in seconds and even a 60-constructor datatype |
1364 |
requires only two minutes. It is also simple: the package consists of |
|
1365 |
under 1100 lines (35K bytes) of Standard ML code. The first working |
|
1366 |
version took under a week to code. |
|
1367 |
||
355 | 1368 |
In set theory, care is required to ensure that the inductive definition |
1369 |
yields a set (rather than a proper class). This problem is inherent to set |
|
1370 |
theory, whether or not the Knaster-Tarski Theorem is employed. We must |
|
1371 |
exhibit a bounding set (called a domain above). For inductive definitions, |
|
1372 |
this is often trivial. For datatype definitions, I have had to formalize |
|
1373 |
much set theory. I intend to formalize cardinal arithmetic and the |
|
1374 |
$\aleph$-sequence to handle datatype definitions that have infinite |
|
1375 |
branching. The need for such efforts is not a drawback of the fixedpoint |
|
1376 |
approach, for the alternative is to take such definitions on faith. |
|
103 | 1377 |
|
355 | 1378 |
The approach is not restricted to set theory. It should be suitable for |
1379 |
any logic that has some notion of set and the Knaster-Tarski Theorem. I |
|
1380 |
intend to use the Isabelle/ZF package as the basis for a higher-order logic |
|
1381 |
one, using Isabelle/HOL\@. The necessary theory is already |
|
130 | 1382 |
mechanized~\cite{paulson-coind}. HOL represents sets by unary predicates; |
355 | 1383 |
defining the corresponding types may cause complications. |
103 | 1384 |
|
1385 |
||
355 | 1386 |
\bibliographystyle{springer} |
1387 |
\bibliography{string-abbrv,atp,theory,funprog,isabelle} |
|
103 | 1388 |
%%%%%\doendnotes |
1389 |
||
1390 |
\ifCADE\typeout{****Omitting appendices from CADE version!} |
|
1391 |
\else |
|
1392 |
\newpage |
|
1393 |
\appendix |
|
130 | 1394 |
\section{Inductive and coinductive definitions: users guide} |
1395 |
The ML functors \verb|Inductive_Fun| and \verb|CoInductive_Fun| build |
|
1396 |
inductive and coinductive definitions, respectively. This section describes |
|
103 | 1397 |
how to invoke them. |
1398 |
||
1399 |
\subsection{The result structure} |
|
1400 |
Many of the result structure's components have been discussed |
|
1401 |
in~\S\ref{basic-sec}; others are self-explanatory. |
|
1402 |
\begin{description} |
|
1403 |
\item[\tt thy] is the new theory containing the recursive sets. |
|
1404 |
||
1405 |
\item[\tt defs] is the list of definitions of the recursive sets. |
|
1406 |
||
1407 |
\item[\tt bnd\_mono] is a monotonicity theorem for the fixedpoint operator. |
|
1408 |
||
1409 |
\item[\tt unfold] is a fixedpoint equation for the recursive set (the union of |
|
1410 |
the recursive sets, in the case of mutual recursion). |
|
1411 |
||
1412 |
\item[\tt dom\_subset] is a theorem stating inclusion in the domain. |
|
1413 |
||
1414 |
\item[\tt intrs] is the list of introduction rules, now proved as theorems, for |
|
1415 |
the recursive sets. |
|
1416 |
||
1417 |
\item[\tt elim] is the elimination rule. |
|
1418 |
||
1419 |
\item[\tt mk\_cases] is a function to create simplified instances of {\tt |
|
1420 |
elim}, using freeness reasoning on some underlying datatype. |
|
1421 |
\end{description} |
|
1422 |
||
1423 |
For an inductive definition, the result structure contains two induction rules, |
|
130 | 1424 |
{\tt induct} and \verb|mutual_induct|. For a coinductive definition, it |
1425 |
contains the rule \verb|coinduct|. |
|
1426 |
||
1427 |
Figure~\ref{def-result-fig} summarizes the two result signatures, |
|
1428 |
specifying the types of all these components. |
|
103 | 1429 |
|
1430 |
\begin{figure} |
|
1431 |
\begin{ttbox} |
|
1432 |
sig |
|
1433 |
val thy : theory |
|
1434 |
val defs : thm list |
|
1435 |
val bnd_mono : thm |
|
1436 |
val unfold : thm |
|
1437 |
val dom_subset : thm |
|
1438 |
val intrs : thm list |
|
1439 |
val elim : thm |
|
1440 |
val mk_cases : thm list -> string -> thm |
|
1441 |
{\it(Inductive definitions only)} |
|
1442 |
val induct : thm |
|
1443 |
val mutual_induct: thm |
|
130 | 1444 |
{\it(Coinductive definitions only)} |
1445 |
val coinduct : thm |
|
103 | 1446 |
end |
1447 |
\end{ttbox} |
|
1448 |
\hrule |
|
130 | 1449 |
\caption{The result of a (co)inductive definition} \label{def-result-fig} |
103 | 1450 |
|
130 | 1451 |
\medskip |
103 | 1452 |
\begin{ttbox} |
1453 |
sig |
|
1454 |
val thy : theory |
|
497
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
1455 |
val thy_name : string |
103 | 1456 |
val rec_doms : (string*string) list |
1457 |
val sintrs : string list |
|
1458 |
val monos : thm list |
|
1459 |
val con_defs : thm list |
|
1460 |
val type_intrs : thm list |
|
1461 |
val type_elims : thm list |
|
1462 |
end |
|
1463 |
\end{ttbox} |
|
1464 |
\hrule |
|
130 | 1465 |
\caption{The argument of a (co)inductive definition} \label{def-arg-fig} |
103 | 1466 |
\end{figure} |
1467 |
||
1468 |
\subsection{The argument structure} |
|
130 | 1469 |
Both \verb|Inductive_Fun| and \verb|CoInductive_Fun| take the same argument |
103 | 1470 |
structure (Figure~\ref{def-arg-fig}). Its components are as follows: |
1471 |
\begin{description} |
|
1472 |
\item[\tt thy] is the definition's parent theory, which {\it must\/} |
|
1473 |
declare constants for the recursive sets. |
|
1474 |
||
497
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
1475 |
\item[\tt thy\_name] is a string, informing Isabelle's theory database of |
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
1476 |
the name you will give to the result structure. |
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
1477 |
|
103 | 1478 |
\item[\tt rec\_doms] is a list of pairs, associating the name of each recursive |
1479 |
set with its domain. |
|
1480 |
||
1481 |
\item[\tt sintrs] specifies the desired introduction rules as strings. |
|
1482 |
||
1483 |
\item[\tt monos] consists of monotonicity theorems for each operator applied |
|
1484 |
to a recursive set in the introduction rules. |
|
1485 |
||
1486 |
\item[\tt con\_defs] contains definitions of constants appearing in the |
|
130 | 1487 |
introduction rules. The (co)datatype package supplies the constructors' |
103 | 1488 |
definitions here. Most direct calls of \verb|Inductive_Fun| or |
130 | 1489 |
\verb|CoInductive_Fun| pass the empty list; one exception is the primitive |
103 | 1490 |
recursive functions example (\S\ref{primrec-sec}). |
1491 |
||
1492 |
\item[\tt type\_intrs] consists of introduction rules for type-checking the |
|
1493 |
definition, as discussed in~\S\ref{basic-sec}. They are applied using |
|
1494 |
depth-first search; you can trace the proof by setting |
|
1495 |
\verb|trace_DEPTH_FIRST := true|. |
|
1496 |
||
1497 |
\item[\tt type\_elims] consists of elimination rules for type-checking the |
|
1498 |
definition. They are presumed to be `safe' and are applied as much as |
|
1499 |
possible, prior to the {\tt type\_intrs} search. |
|
1500 |
\end{description} |
|
1501 |
The package has a few notable restrictions: |
|
1502 |
\begin{itemize} |
|
1503 |
\item The parent theory, {\tt thy}, must declare the recursive sets as |
|
1504 |
constants. You can extend a theory with new constants using {\tt |
|
1505 |
addconsts}, as illustrated in~\S\ref{ind-eg-sec}. If the inductive |
|
1506 |
definition also requires new concrete syntax, then it is simpler to |
|
1507 |
express the parent theory using a theory file. It is often convenient to |
|
1508 |
define an infix syntax for relations, say $a\prec b$ for $\pair{a,b}\in |
|
1509 |
R$. |
|
1510 |
||
1511 |
\item The names of the recursive sets must be identifiers, not infix |
|
1512 |
operators. |
|
1513 |
||
1514 |
\item Side-conditions must not be conjunctions. However, an introduction rule |
|
1515 |
may contain any number of side-conditions. |
|
1516 |
\end{itemize} |
|
1517 |
||
1518 |
||
130 | 1519 |
\section{Datatype and codatatype definitions: users guide} |
1520 |
The ML functors \verb|Datatype_Fun| and \verb|CoDatatype_Fun| define datatypes |
|
1521 |
and codatatypes, invoking \verb|Datatype_Fun| and |
|
1522 |
\verb|CoDatatype_Fun| to make the underlying (co)inductive definitions. |
|
103 | 1523 |
|
1524 |
||
1525 |
\subsection{The result structure} |
|
130 | 1526 |
The result structure extends that of (co)inductive definitions |
103 | 1527 |
(Figure~\ref{def-result-fig}) with several additional items: |
1528 |
\begin{ttbox} |
|
1529 |
val con_thy : theory |
|
1530 |
val con_defs : thm list |
|
1531 |
val case_eqns : thm list |
|
1532 |
val free_iffs : thm list |
|
1533 |
val free_SEs : thm list |
|
1534 |
val mk_free : string -> thm |
|
1535 |
\end{ttbox} |
|
1536 |
Most of these have been discussed in~\S\ref{data-sec}. Here is a summary: |
|
1537 |
\begin{description} |
|
1538 |
\item[\tt con\_thy] is a new theory containing definitions of the |
|
130 | 1539 |
(co)datatype's constructors and case operator. It also declares the |
103 | 1540 |
recursive sets as constants, so that it may serve as the parent |
130 | 1541 |
theory for the (co)inductive definition. |
103 | 1542 |
|
1543 |
\item[\tt con\_defs] is a list of definitions: the case operator followed by |
|
1544 |
the constructors. This theorem list can be supplied to \verb|mk_cases|, for |
|
1545 |
example. |
|
1546 |
||
1547 |
\item[\tt case\_eqns] is a list of equations, stating that the case operator |
|
1548 |
inverts each constructor. |
|
1549 |
||
1550 |
\item[\tt free\_iffs] is a list of logical equivalences to perform freeness |
|
1551 |
reasoning by rewriting. A typical application has the form |
|
1552 |
\begin{ttbox} |
|
1553 |
by (asm_simp_tac (ZF_ss addsimps free_iffs) 1); |
|
1554 |
\end{ttbox} |
|
1555 |
||
1556 |
\item[\tt free\_SEs] is a list of `safe' elimination rules to perform freeness |
|
1557 |
reasoning. It can be supplied to \verb|eresolve_tac| or to the classical |
|
1558 |
reasoner: |
|
1559 |
\begin{ttbox} |
|
1560 |
by (fast_tac (ZF_cs addSEs free_SEs) 1); |
|
1561 |
\end{ttbox} |
|
1562 |
||
1563 |
\item[\tt mk\_free] is a function to prove freeness properties, specified as |
|
1564 |
strings. The theorems can be expressed in various forms, such as logical |
|
1565 |
equivalences or elimination rules. |
|
1566 |
\end{description} |
|
1567 |
||
1568 |
The result structure also inherits everything from the underlying |
|
130 | 1569 |
(co)inductive definition, such as the introduction rules, elimination rule, |
179 | 1570 |
and (co)induction rule. |
103 | 1571 |
|
1572 |
||
1573 |
\begin{figure} |
|
1574 |
\begin{ttbox} |
|
1575 |
sig |
|
1576 |
val thy : theory |
|
497
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
1577 |
val thy_name : string |
103 | 1578 |
val rec_specs : (string * string * (string list*string)list) list |
1579 |
val rec_styp : string |
|
1580 |
val sintrs : string list |
|
1581 |
val monos : thm list |
|
1582 |
val type_intrs: thm list |
|
1583 |
val type_elims: thm list |
|
1584 |
end |
|
1585 |
\end{ttbox} |
|
1586 |
\hrule |
|
130 | 1587 |
\caption{The argument of a (co)datatype definition} \label{data-arg-fig} |
103 | 1588 |
\end{figure} |
1589 |
||
1590 |
\subsection{The argument structure} |
|
130 | 1591 |
Both (co)datatype functors take the same argument structure |
1592 |
(Figure~\ref{data-arg-fig}). It does not extend that for (co)inductive |
|
103 | 1593 |
definitions, but shares several components and passes them uninterpreted to |
497
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
1594 |
\verb|Datatype_Fun| or \verb|CoDatatype_Fun|. The new components are as |
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
1595 |
follows: |
103 | 1596 |
\begin{description} |
130 | 1597 |
\item[\tt thy] is the (co)datatype's parent theory. It {\it must not\/} |
1598 |
declare constants for the recursive sets. Recall that (co)inductive |
|
103 | 1599 |
definitions have the opposite restriction. |
1600 |
||
1601 |
\item[\tt rec\_specs] is a list of triples of the form ({\it recursive set\/}, |
|
1602 |
{\it domain\/}, {\it constructors\/}) for each mutually recursive set. {\it |
|
497
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
1603 |
Constructors\/} is a list of the form (names, type, mixfix). The mixfix |
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
1604 |
component is usually {\tt NoSyn}, specifying no special syntax for the |
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
1605 |
constructor; other useful possibilities are {\tt Infixl}~$p$ and {\tt |
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
1606 |
Infixr}~$p$, specifying an infix operator of priority~$p$. |
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset
|
1607 |
Section~\ref{data-sec} presents examples. |
103 | 1608 |
|
1609 |
\item[\tt rec\_styp] is the common meta-type of the mutually recursive sets, |
|
1610 |
specified as a string. They must all have the same type because all must |
|
1611 |
take the same parameters. |
|
1612 |
\end{description} |
|
1613 |
The choice of domain is usually simple. Isabelle/ZF defines the set |
|
1614 |
$\univ(A)$, which contains~$A$ and is closed under the standard Cartesian |
|
1615 |
products and disjoint sums \cite[\S4.2]{paulson-set-II}. In a typical |
|
1616 |
datatype definition with set parameters $A_1$, \ldots, $A_k$, a suitable |
|
1617 |
domain for all the recursive sets is $\univ(A_1\un\cdots\un A_k)$. For a |
|
130 | 1618 |
codatatype definition, the set |
103 | 1619 |
$\quniv(A)$ contains~$A$ and is closed under the variant Cartesian products |
130 | 1620 |
and disjoint sums; the appropriate domain is |
103 | 1621 |
$\quniv(A_1\un\cdots\un A_k)$. |
1622 |
||
1623 |
The {\tt sintrs} specify the introduction rules, which govern the recursive |
|
179 | 1624 |
structure of the datatype. Introduction rules may involve monotone |
1625 |
operators and side-conditions to express things that go beyond the usual |
|
1626 |
notion of datatype. The theorem lists {\tt monos}, {\tt type\_intrs} and |
|
1627 |
{\tt type\_elims} should contain precisely what is needed for the |
|
1628 |
underlying (co)inductive definition. Isabelle/ZF defines lists of |
|
1629 |
type-checking rules that can be supplied for the latter two components: |
|
103 | 1630 |
\begin{itemize} |
179 | 1631 |
\item {\tt datatype\_intrs} and {\tt datatype\_elims} are rules |
103 | 1632 |
for $\univ(A)$. |
355 | 1633 |
\item {\tt codatatype\_intrs} and {\tt codatatype\_elims} are |
103 | 1634 |
rules for $\quniv(A)$. |
1635 |
\end{itemize} |
|
1636 |
In typical definitions, these theorem lists need not be supplemented with |
|
1637 |
other theorems. |
|
1638 |
||
1639 |
The constructor definitions' right-hand sides can overlap. A |
|
1640 |
simple example is the datatype for the combinators, whose constructors are |
|
1641 |
\begin{eqnarray*} |
|
1642 |
{\tt K} & \equiv & \Inl(\emptyset) \\ |
|
1643 |
{\tt S} & \equiv & \Inr(\Inl(\emptyset)) \\ |
|
1644 |
p{\tt\#}q & \equiv & \Inr(\Inl(\pair{p,q})) |
|
1645 |
\end{eqnarray*} |
|
1646 |
Unlike in previous versions of Isabelle, \verb|fold_tac| now ensures that the |
|
1647 |
longest right-hand sides are folded first. |
|
1648 |
||
1649 |
\fi |
|
1650 |
\end{document} |