1 \documentstyle[a4,proof,iman,extra,times]{llncs} |
1 \documentstyle[a4,proof,iman,extra,times]{llncs} |
2 %Repetition in the two sentences that begin ``The powerset operator'' |
|
3 \newif\ifCADE |
2 \newif\ifCADE |
4 \CADEtrue |
3 \CADEtrue |
5 |
4 |
6 \title{A Fixedpoint Approach to Implementing\\ |
5 \title{A Fixedpoint Approach to Implementing\\ |
7 (Co)Inductive Definitions\thanks{J. Grundy and S. Thompson made detailed |
6 (Co)Inductive Definitions\thanks{J. Grundy and S. Thompson made detailed |
270 premise $a\in A$ in the following rule from the definition of lists: |
269 premise $a\in A$ in the following rule from the definition of lists: |
271 \[ \infer{\Cons(a,l)\in\lst(A)}{a\in A & l\in\lst(A)} \] |
270 \[ \infer{\Cons(a,l)\in\lst(A)}{a\in A & l\in\lst(A)} \] |
272 |
271 |
273 \subsection{The fixedpoint definitions} |
272 \subsection{The fixedpoint definitions} |
274 The package translates the list of desired introduction rules into a fixedpoint |
273 The package translates the list of desired introduction rules into a fixedpoint |
275 definition. Consider, as a running example, the finite set operator |
274 definition. Consider, as a running example, the finite powerset operator |
276 $\Fin(A)$: the set of all finite subsets of~$A$. It can be |
275 $\Fin(A)$: the set of all finite subsets of~$A$. It can be |
277 defined as the least set closed under the rules |
276 defined as the least set closed under the rules |
278 \[ \emptyset\in\Fin(A) \qquad |
277 \[ \emptyset\in\Fin(A) \qquad |
279 \infer{\{a\}\un b\in\Fin(A)}{a\in A & b\in\Fin(A)} |
278 \infer{\{a\}\un b\in\Fin(A)}{a\in A & b\in\Fin(A)} |
280 \] |
279 \] |
492 represents a slight strengthening of the greatest fixedpoint property. I |
491 represents a slight strengthening of the greatest fixedpoint property. I |
493 discuss several forms of coinduction rules elsewhere~\cite{paulson-coind}. |
492 discuss several forms of coinduction rules elsewhere~\cite{paulson-coind}. |
494 |
493 |
495 |
494 |
496 \section{Examples of inductive and coinductive definitions}\label{ind-eg-sec} |
495 \section{Examples of inductive and coinductive definitions}\label{ind-eg-sec} |
497 This section presents several examples: the finite set operator, |
496 This section presents several examples: the finite powerset operator, |
498 lists of $n$ elements, bisimulations on lazy lists, the well-founded part |
497 lists of $n$ elements, bisimulations on lazy lists, the well-founded part |
499 of a relation, and the primitive recursive functions. |
498 of a relation, and the primitive recursive functions. |
500 |
499 |
501 \subsection{The finite set operator} |
500 \subsection{The finite powerset operator} |
502 The definition of finite sets has been discussed extensively above. Here |
501 This operator has been discussed extensively above. Here |
503 is the corresponding ML invocation (note that $\cons(a,b)$ abbreviates |
502 is the corresponding ML invocation (note that $\cons(a,b)$ abbreviates |
504 $\{a\}\un b$ in Isabelle/ZF): |
503 $\{a\}\un b$ in Isabelle/ZF): |
505 \begin{ttbox} |
504 \begin{ttbox} |
506 structure Fin = Inductive_Fun |
505 structure Fin = Inductive_Fun |
507 (val thy = Arith.thy addconsts [(["Fin"],"i=>i")] |
506 (val thy = Arith.thy addconsts [(["Fin"],"i=>i")] |