removed historic manual;
authorwenzelm
Tue Aug 28 13:12:03 2012 +0200 (2012-08-28)
changeset 489643ec847562782
parent 48963 f11d88bfa934
child 48965 1fead823c7c6
removed historic manual;
doc-src/Inductive/Makefile
doc-src/Inductive/ind-defs-slides.tex
doc-src/Inductive/ind-defs.tex
doc/Contents
     1.1 --- a/doc-src/Inductive/Makefile	Tue Aug 28 13:09:01 2012 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,30 +0,0 @@
     1.4 -
     1.5 -## targets
     1.6 -
     1.7 -default: dvi
     1.8 -
     1.9 -
    1.10 -## dependencies
    1.11 -
    1.12 -include ../Makefile.in
    1.13 -
    1.14 -NAME = ind-defs
    1.15 -FILES = ind-defs.tex ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
    1.16 -
    1.17 -dvi: $(NAME).dvi
    1.18 -
    1.19 -$(NAME).dvi: $(FILES)
    1.20 -	$(LATEX) $(NAME)
    1.21 -	$(BIBTEX) $(NAME)
    1.22 -	$(LATEX) $(NAME)
    1.23 -	$(LATEX) $(NAME)
    1.24 -
    1.25 -pdf: $(NAME).pdf
    1.26 -
    1.27 -$(NAME).pdf: $(FILES)
    1.28 -	$(PDFLATEX) $(NAME)
    1.29 -	$(BIBTEX) $(NAME)
    1.30 -	$(PDFLATEX) $(NAME)
    1.31 -	$(PDFLATEX) $(NAME)
    1.32 -	$(FIXBOOKMARKS) $(NAME).out
    1.33 -	$(PDFLATEX) $(NAME)
     2.1 --- a/doc-src/Inductive/ind-defs-slides.tex	Tue Aug 28 13:09:01 2012 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,194 +0,0 @@
     2.4 -%process by     latex ind-defs-slides; dvips -Plime ind-defs-slides
     2.5 -%               ghostview -magstep -2 -landscape ind-defs-slides.ps
     2.6 -\documentclass[a4,slidesonly,semlayer]{seminar}
     2.7 -
     2.8 -\usepackage{fancybox}
     2.9 -\usepackage{semhelv}
    2.10 -\usepackage{epsf}
    2.11 -\def\printlandscape{\special{landscape}}    % Works with dvips.
    2.12 -
    2.13 -\slidesmag{5}\articlemag{2}    %the difference is 3 instead of 4!
    2.14 -\extraslideheight{30pt}
    2.15 -
    2.16 -\renewcommand\slidefuzz{6pt}
    2.17 -\sloppy\hfuzz2pt   %sloppy defines \hfuzz0.5pt but it's mainly for text
    2.18 -
    2.19 -\newcommand\sbs{\subseteq}
    2.20 -\newcommand\Pow{{\cal P}}
    2.21 -\newcommand\lfp{\hbox{\tt lfp}}
    2.22 -\newcommand\gfp{\hbox{\tt gfp}}
    2.23 -\newcommand\lst{\hbox{\tt list}}
    2.24 -\newcommand\term{\hbox{\tt term}}
    2.25 -
    2.26 -\newcommand\heading[1]{%
    2.27 -  \begin{center}\large\bf\shadowbox{#1}\end{center}
    2.28 -  \vspace{1ex minus 1ex}}
    2.29 -
    2.30 -\newpagestyle{mine}%
    2.31 -  {L. Paulson\hfil A Fixedpoint Approach to (Co)Inductive Definitions\hfil
    2.32 -      \thepage}%
    2.33 -  {\hfil\special{psfile=cuarms.eps hscale=20 vscale=20 voffset=-6
    2.34 -      hoffset=-14}\hfil}
    2.35 -\pagestyle{mine}
    2.36 -
    2.37 -
    2.38 -\begin{document}
    2.39 -\slidefonts
    2.40 -
    2.41 -\begin{slide}\centering
    2.42 -\shadowbox{% 
    2.43 -    \begin{Bcenter}
    2.44 -    {\Large\bf A Fixedpoint Approach to}\\[2ex]
    2.45 -    {\Large\bf (Co)Inductive Definitions}
    2.46 -    \end{Bcenter}}
    2.47 -\bigskip
    2.48 -
    2.49 -    \begin{Bcenter}
    2.50 -    Lawrence C. Paulson\\
    2.51 -    Computer Laboratory\\
    2.52 -    University of Cambridge\\
    2.53 -    England\\[1ex]
    2.54 -    \verb|lcp@cl.cam.ac.uk|
    2.55 -    \end{Bcenter}
    2.56 -\bigskip
    2.57 -
    2.58 -{\footnotesize Thanks: SERC grants GR/G53279, GR/H40570; ESPRIT Project 6453
    2.59 -  `Types'} 
    2.60 -\end{slide}
    2.61 -
    2.62 -
    2.63 -\begin{slide}
    2.64 -\heading{Inductive Definitions}
    2.65 -\begin{itemize}
    2.66 -  \item {\bf datatypes}
    2.67 -    \begin{itemize}
    2.68 -      \item finite lists, trees
    2.69 -      \item syntax of expressions, \ldots
    2.70 -    \end{itemize}
    2.71 -  \item {\bf inference systems}
    2.72 -    \begin{itemize}
    2.73 -      \item transitive closure of a relation
    2.74 -      \item transition systems
    2.75 -      \item structural operational semantics
    2.76 -    \end{itemize}
    2.77 -\end{itemize}
    2.78 -
    2.79 -Supported by Boyer/Moore, HOL, Coq, \ldots, Isabelle/ZF
    2.80 -\end{slide}
    2.81 -
    2.82 -
    2.83 -\begin{slide}
    2.84 -\heading{Coinductive Definitions}
    2.85 -\begin{itemize}
    2.86 -  \item {\bf codatatypes}
    2.87 -    \begin{itemize}
    2.88 -      \item {\it infinite\/} lists, trees
    2.89 -      \item  syntax of {\it infinite\/} expressions, \ldots
    2.90 -    \end{itemize}
    2.91 -  \item {\bf bisimulation relations}
    2.92 -    \begin{itemize}
    2.93 -      \item process equivalence
    2.94 -      \item uses in functional programming (Abramksy, Howe)
    2.95 -    \end{itemize}
    2.96 -\end{itemize}
    2.97 -
    2.98 -Supported by \ldots ?, \ldots, Isabelle/ZF
    2.99 -\end{slide}
   2.100 -
   2.101 -
   2.102 -\begin{slide}
   2.103 -\heading{The Knaster-Tarksi Fixedpoint Theorem}
   2.104 -$h$ a monotone function
   2.105 -
   2.106 -$D$ a set such that $h(D)\sbs D$
   2.107 -
   2.108 -The {\bf least} fixedpoint $\lfp(D,h)$ yields {\bf inductive} definitions
   2.109 -
   2.110 -The {\bf greatest} fixedpoint $\gfp(D,h)$ yields {\bf coinductive} definitions
   2.111 -
   2.112 -{\it A general approach\/}:
   2.113 -\begin{itemize}
   2.114 -  \item handles all provably monotone definitions
   2.115 -  \item works for set theory, higher-order logic, \ldots
   2.116 -\end{itemize}
   2.117 -\end{slide}
   2.118 -
   2.119 -
   2.120 -\begin{slide}
   2.121 -\heading{An Implementation in Isabelle/ZF}\centering
   2.122 -\begin{itemize}
   2.123 -  \item {\bf Input} 
   2.124 -     \begin{itemize}
   2.125 -      \item description of {\it introduction rules\/} \& tree's {\it
   2.126 -          constructors\/} 
   2.127 -      \item {\it theorems\/} implying that the definition is {\it monotonic\/}
   2.128 -    \end{itemize}
   2.129 -  \item {\bf Output} 
   2.130 -     \begin{itemize}
   2.131 -      \item (co)induction rules
   2.132 -      \item case analysis rule and {\it rule inversion\/} tools, \ldots
   2.133 -    \end{itemize}
   2.134 -\end{itemize}
   2.135 -
   2.136 -\vfill
   2.137 -{\it flexible, secure, \ldots but fast\/}
   2.138 -\end{slide}
   2.139 -
   2.140 -
   2.141 -\begin{slide}
   2.142 -\heading{Working Examples}
   2.143 -\begin{itemize}
   2.144 -  \item lists
   2.145 -  \item terms recursive over lists: $\term(A) = A\times\lst(\term(A))$
   2.146 -  \item primitive recursive functions
   2.147 -  \item lazy lists
   2.148 -  \item bisimulations for lazy lists
   2.149 -  \item combinator reductions; Church-Rosser Theorem
   2.150 -  \item mutually recursive trees \& forests
   2.151 -\end{itemize}
   2.152 -\end{slide}
   2.153 -
   2.154 -
   2.155 -\begin{slide}
   2.156 -\heading{Other Work Using Fixedpoints}
   2.157 -{\bf The HOL system}:
   2.158 -\begin{itemize}
   2.159 -  \item Melham's induction package: special case of Fixedpoint Theorem
   2.160 -  \item Andersen \& Petersen's induction package
   2.161 -  \item (no HOL datatype package uses fixedpoints)
   2.162 -\end{itemize}
   2.163 -
   2.164 -{\bf Coq and LEGO}:
   2.165 -\begin{itemize}
   2.166 -  \item (Co)induction {\it almost\/} expressible in base logic (CoC)
   2.167 -  \item \ldots{} inductive definitions are built-in
   2.168 -\end{itemize}
   2.169 -\end{slide}
   2.170 -
   2.171 -
   2.172 -\begin{slide}
   2.173 -\heading{Limitations \& Future Developments}\centering
   2.174 -\begin{itemize}
   2.175 -  \item {\bf infinite-branching trees}
   2.176 -    \begin{itemize}
   2.177 -      \item justification requires proof
   2.178 -      \item would be easier to {\it build them in\/}!
   2.179 -    \end{itemize}
   2.180 -  \item {\bf recursive function definitions}
   2.181 -    \begin{itemize}
   2.182 -      \item use {\it well-founded\/} recursion
   2.183 -      \item distinct from datatype definitions
   2.184 -    \end{itemize}
   2.185 -  \item {\bf port to Isabelle/HOL}
   2.186 -\end{itemize}
   2.187 -\end{slide}
   2.188 -
   2.189 -\end{document}
   2.190 -
   2.191 -
   2.192 -{\it flat\/} ordered pairs used to define infinite lists, \ldots
   2.193 -
   2.194 -\begin{slide}
   2.195 -\heading{}\centering
   2.196 -\end{slide}
   2.197 -
     3.1 --- a/doc-src/Inductive/ind-defs.tex	Tue Aug 28 13:09:01 2012 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,1333 +0,0 @@
     3.4 -\documentclass[12pt,a4paper]{article}
     3.5 -\usepackage{latexsym,../iman,../extra,../ttbox,../proof,../pdfsetup}
     3.6 -
     3.7 -\newif\ifshort%''Short'' means a published version, not the documentation
     3.8 -\shortfalse%%%%%\shorttrue
     3.9 -
    3.10 -\title{A Fixedpoint Approach to\\ 
    3.11 -  (Co)Inductive and (Co)Datatype Definitions%
    3.12 -  \thanks{J. Grundy and S. Thompson made detailed comments.  Mads Tofte and
    3.13 -    the referees were also helpful.  The research was funded by the SERC
    3.14 -    grants GR/G53279, GR/H40570 and by the ESPRIT Project 6453 ``Types''.}}
    3.15 -
    3.16 -\author{Lawrence C. Paulson\\{\tt lcp@cl.cam.ac.uk}\\
    3.17 -        Computer Laboratory, University of Cambridge, England}
    3.18 -\date{\today} 
    3.19 -\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
    3.20 -
    3.21 -\newcommand\sbs{\subseteq}
    3.22 -\let\To=\Rightarrow
    3.23 -
    3.24 -\newcommand\defn[1]{{\bf#1}}
    3.25 -
    3.26 -\newcommand\pow{{\cal P}}
    3.27 -\newcommand\RepFun{\hbox{\tt RepFun}}
    3.28 -\newcommand\cons{\hbox{\tt cons}}
    3.29 -\def\succ{\hbox{\tt succ}}
    3.30 -\newcommand\split{\hbox{\tt split}}
    3.31 -\newcommand\fst{\hbox{\tt fst}}
    3.32 -\newcommand\snd{\hbox{\tt snd}}
    3.33 -\newcommand\converse{\hbox{\tt converse}}
    3.34 -\newcommand\domain{\hbox{\tt domain}}
    3.35 -\newcommand\range{\hbox{\tt range}}
    3.36 -\newcommand\field{\hbox{\tt field}}
    3.37 -\newcommand\lfp{\hbox{\tt lfp}}
    3.38 -\newcommand\gfp{\hbox{\tt gfp}}
    3.39 -\newcommand\id{\hbox{\tt id}}
    3.40 -\newcommand\trans{\hbox{\tt trans}}
    3.41 -\newcommand\wf{\hbox{\tt wf}}
    3.42 -\newcommand\nat{\hbox{\tt nat}}
    3.43 -\newcommand\rank{\hbox{\tt rank}}
    3.44 -\newcommand\univ{\hbox{\tt univ}}
    3.45 -\newcommand\Vrec{\hbox{\tt Vrec}}
    3.46 -\newcommand\Inl{\hbox{\tt Inl}}
    3.47 -\newcommand\Inr{\hbox{\tt Inr}}
    3.48 -\newcommand\case{\hbox{\tt case}}
    3.49 -\newcommand\lst{\hbox{\tt list}}
    3.50 -\newcommand\Nil{\hbox{\tt Nil}}
    3.51 -\newcommand\Cons{\hbox{\tt Cons}}
    3.52 -\newcommand\lstcase{\hbox{\tt list\_case}}
    3.53 -\newcommand\lstrec{\hbox{\tt list\_rec}}
    3.54 -\newcommand\length{\hbox{\tt length}}
    3.55 -\newcommand\listn{\hbox{\tt listn}}
    3.56 -\newcommand\acc{\hbox{\tt acc}}
    3.57 -\newcommand\primrec{\hbox{\tt primrec}}
    3.58 -\newcommand\SC{\hbox{\tt SC}}
    3.59 -\newcommand\CONST{\hbox{\tt CONST}}
    3.60 -\newcommand\PROJ{\hbox{\tt PROJ}}
    3.61 -\newcommand\COMP{\hbox{\tt COMP}}
    3.62 -\newcommand\PREC{\hbox{\tt PREC}}
    3.63 -
    3.64 -\newcommand\quniv{\hbox{\tt quniv}}
    3.65 -\newcommand\llist{\hbox{\tt llist}}
    3.66 -\newcommand\LNil{\hbox{\tt LNil}}
    3.67 -\newcommand\LCons{\hbox{\tt LCons}}
    3.68 -\newcommand\lconst{\hbox{\tt lconst}}
    3.69 -\newcommand\lleq{\hbox{\tt lleq}}
    3.70 -\newcommand\map{\hbox{\tt map}}
    3.71 -\newcommand\term{\hbox{\tt term}}
    3.72 -\newcommand\Apply{\hbox{\tt Apply}}
    3.73 -\newcommand\termcase{\hbox{\tt term\_case}}
    3.74 -\newcommand\rev{\hbox{\tt rev}}
    3.75 -\newcommand\reflect{\hbox{\tt reflect}}
    3.76 -\newcommand\tree{\hbox{\tt tree}}
    3.77 -\newcommand\forest{\hbox{\tt forest}}
    3.78 -\newcommand\Part{\hbox{\tt Part}}
    3.79 -\newcommand\TF{\hbox{\tt tree\_forest}}
    3.80 -\newcommand\Tcons{\hbox{\tt Tcons}}
    3.81 -\newcommand\Fcons{\hbox{\tt Fcons}}
    3.82 -\newcommand\Fnil{\hbox{\tt Fnil}}
    3.83 -\newcommand\TFcase{\hbox{\tt TF\_case}}
    3.84 -\newcommand\Fin{\hbox{\tt Fin}}
    3.85 -\newcommand\QInl{\hbox{\tt QInl}}
    3.86 -\newcommand\QInr{\hbox{\tt QInr}}
    3.87 -\newcommand\qsplit{\hbox{\tt qsplit}}
    3.88 -\newcommand\qcase{\hbox{\tt qcase}}
    3.89 -\newcommand\Con{\hbox{\tt Con}}
    3.90 -\newcommand\data{\hbox{\tt data}}
    3.91 -
    3.92 -\binperiod     %%%treat . like a binary operator
    3.93 -
    3.94 -\begin{document}
    3.95 -\pagestyle{empty}
    3.96 -\begin{titlepage}
    3.97 -\maketitle 
    3.98 -\begin{abstract}
    3.99 -  This paper presents a fixedpoint approach to inductive definitions.
   3.100 -  Instead of using a syntactic test such as ``strictly positive,'' the
   3.101 -  approach lets definitions involve any operators that have been proved
   3.102 -  monotone.  It is conceptually simple, which has allowed the easy
   3.103 -  implementation of mutual recursion and iterated definitions.  It also
   3.104 -  handles coinductive definitions: simply replace the least fixedpoint by a
   3.105 -  greatest fixedpoint.  
   3.106 -
   3.107 -  The method has been implemented in two of Isabelle's logics, \textsc{zf} set
   3.108 -  theory and higher-order logic.  It should be applicable to any logic in
   3.109 -  which the Knaster-Tarski theorem can be proved.  Examples include lists of
   3.110 -  $n$ elements, the accessible part of a relation and the set of primitive
   3.111 -  recursive functions.  One example of a coinductive definition is
   3.112 -  bisimulations for lazy lists.  Recursive datatypes are examined in detail,
   3.113 -  as well as one example of a \defn{codatatype}: lazy lists.
   3.114 -
   3.115 -  The Isabelle package has been applied in several large case studies,
   3.116 -  including two proofs of the Church-Rosser theorem and a coinductive proof of
   3.117 -  semantic consistency.  The package can be trusted because it proves theorems
   3.118 -  from definitions, instead of asserting desired properties as axioms.
   3.119 -\end{abstract}
   3.120 -%
   3.121 -\bigskip
   3.122 -\centerline{Copyright \copyright{} \number\year{} by Lawrence C. Paulson}
   3.123 -\thispagestyle{empty} 
   3.124 -\end{titlepage}
   3.125 -\tableofcontents\cleardoublepage\pagestyle{plain}
   3.126 -
   3.127 -\setcounter{page}{1}
   3.128 -
   3.129 -\section{Introduction}
   3.130 -Several theorem provers provide commands for formalizing recursive data
   3.131 -structures, like lists and trees.  Robin Milner implemented one of the first
   3.132 -of these, for Edinburgh \textsc{lcf}~\cite{milner-ind}.  Given a description
   3.133 -of the desired data structure, Milner's package formulated appropriate
   3.134 -definitions and proved the characteristic theorems.  Similar is Melham's
   3.135 -recursive type package for the Cambridge \textsc{hol} system~\cite{melham89}.
   3.136 -Such data structures are called \defn{datatypes}
   3.137 -below, by analogy with datatype declarations in Standard~\textsc{ml}\@.
   3.138 -Some logics take datatypes as primitive; consider Boyer and Moore's shell
   3.139 -principle~\cite{bm79} and the Coq type theory~\cite{paulin-tlca}.
   3.140 -
   3.141 -A datatype is but one example of an \defn{inductive definition}.  Such a
   3.142 -definition~\cite{aczel77} specifies the least set~$R$ \defn{closed under}
   3.143 -given rules: applying a rule to elements of~$R$ yields a result within~$R$.
   3.144 -Inductive definitions have many applications.  The collection of theorems in a
   3.145 -logic is inductively defined.  A structural operational
   3.146 -semantics~\cite{hennessy90} is an inductive definition of a reduction or
   3.147 -evaluation relation on programs.  A few theorem provers provide commands for
   3.148 -formalizing inductive definitions; these include Coq~\cite{paulin-tlca} and
   3.149 -again the \textsc{hol} system~\cite{camilleri92}.
   3.150 -
   3.151 -The dual notion is that of a \defn{coinductive definition}.  Such a definition
   3.152 -specifies the greatest set~$R$ \defn{consistent with} given rules: every
   3.153 -element of~$R$ can be seen as arising by applying a rule to elements of~$R$.
   3.154 -Important examples include using bisimulation relations to formalize
   3.155 -equivalence of processes~\cite{milner89} or lazy functional
   3.156 -programs~\cite{abramsky90}.  Other examples include lazy lists and other
   3.157 -infinite data structures; these are called \defn{codatatypes} below.
   3.158 -
   3.159 -Not all inductive definitions are meaningful.  \defn{Monotone} inductive
   3.160 -definitions are a large, well-behaved class.  Monotonicity can be enforced
   3.161 -by syntactic conditions such as ``strictly positive,'' but this could lead to
   3.162 -monotone definitions being rejected on the grounds of their syntactic form.
   3.163 -More flexible is to formalize monotonicity within the logic and allow users
   3.164 -to prove it.
   3.165 -
   3.166 -This paper describes a package based on a fixedpoint approach.  Least
   3.167 -fixedpoints yield inductive definitions; greatest fixedpoints yield
   3.168 -coinductive definitions.  Most of the discussion below applies equally to
   3.169 -inductive and coinductive definitions, and most of the code is shared.  
   3.170 -
   3.171 -The package supports mutual recursion and infinitely-branching datatypes and
   3.172 -codatatypes.  It allows use of any operators that have been proved monotone,
   3.173 -thus accepting all provably monotone inductive definitions, including
   3.174 -iterated definitions.
   3.175 -
   3.176 -The package has been implemented in
   3.177 -Isabelle~\cite{paulson-markt,paulson-isa-book} using 
   3.178 -\textsc{zf} set theory \cite{paulson-set-I,paulson-set-II}; part of it has
   3.179 -since been ported to Isabelle/\textsc{hol} (higher-order logic).  The
   3.180 -recursion equations are specified as introduction rules for the mutually
   3.181 -recursive sets.  The package transforms these rules into a mapping over sets,
   3.182 -and attempts to prove that the mapping is monotonic and well-typed.  If
   3.183 -successful, the package makes fixedpoint definitions and proves the
   3.184 -introduction, elimination and (co)induction rules.  Users invoke the package
   3.185 -by making simple declarations in Isabelle theory files.
   3.186 -
   3.187 -Most datatype packages equip the new datatype with some means of expressing
   3.188 -recursive functions.  This is the main omission from my package.  Its
   3.189 -fixedpoint operators define only recursive sets.  The Isabelle/\textsc{zf}
   3.190 -theory provides well-founded recursion~\cite{paulson-set-II}, which is harder
   3.191 -to use than structural recursion but considerably more general.
   3.192 -Slind~\cite{slind-tfl} has written a package to automate the definition of
   3.193 -well-founded recursive functions in Isabelle/\textsc{hol}.
   3.194 -
   3.195 -\paragraph*{Outline.} Section~2 introduces the least and greatest fixedpoint
   3.196 -operators.  Section~3 discusses the form of introduction rules, mutual
   3.197 -recursion and other points common to inductive and coinductive definitions.
   3.198 -Section~4 discusses induction and coinduction rules separately.  Section~5
   3.199 -presents several examples, including a coinductive definition.  Section~6
   3.200 -describes datatype definitions.  Section~7 presents related work.
   3.201 -Section~8 draws brief conclusions.  \ifshort\else The appendices are simple
   3.202 -user's manuals for this Isabelle package.\fi
   3.203 -
   3.204 -Most of the definitions and theorems shown below have been generated by the
   3.205 -package.  I have renamed some variables to improve readability.
   3.206 - 
   3.207 -\section{Fixedpoint operators}
   3.208 -In set theory, the least and greatest fixedpoint operators are defined as
   3.209 -follows:
   3.210 -\begin{eqnarray*}
   3.211 -   \lfp(D,h)  & \equiv & \inter\{X\sbs D. h(X)\sbs X\} \\
   3.212 -   \gfp(D,h)  & \equiv & \union\{X\sbs D. X\sbs h(X)\}
   3.213 -\end{eqnarray*}   
   3.214 -Let $D$ be a set.  Say that $h$ is \defn{bounded by}~$D$ if $h(D)\sbs D$, and
   3.215 -\defn{monotone below~$D$} if
   3.216 -$h(A)\sbs h(B)$ for all $A$ and $B$ such that $A\sbs B\sbs D$.  If $h$ is
   3.217 -bounded by~$D$ and monotone then both operators yield fixedpoints:
   3.218 -\begin{eqnarray*}
   3.219 -   \lfp(D,h)  & = & h(\lfp(D,h)) \\
   3.220 -   \gfp(D,h)  & = & h(\gfp(D,h)) 
   3.221 -\end{eqnarray*}   
   3.222 -These equations are instances of the Knaster-Tarski theorem, which states
   3.223 -that every monotonic function over a complete lattice has a
   3.224 -fixedpoint~\cite{davey-priestley}.  It is obvious from their definitions
   3.225 -that $\lfp$ must be the least fixedpoint, and $\gfp$ the greatest.
   3.226 -
   3.227 -This fixedpoint theory is simple.  The Knaster-Tarski theorem is easy to
   3.228 -prove.  Showing monotonicity of~$h$ is trivial, in typical cases.  We must
   3.229 -also exhibit a bounding set~$D$ for~$h$.  Frequently this is trivial, as when
   3.230 -a set of theorems is (co)inductively defined over some previously existing set
   3.231 -of formul{\ae}.  Isabelle/\textsc{zf} provides suitable bounding sets for
   3.232 -infinitely-branching (co)datatype definitions; see~\S\ref{univ-sec}.  Bounding
   3.233 -sets are also called \defn{domains}.
   3.234 -
   3.235 -The powerset operator is monotone, but by Cantor's theorem there is no
   3.236 -set~$A$ such that $A=\pow(A)$.  We cannot put $A=\lfp(D,\pow)$ because
   3.237 -there is no suitable domain~$D$.  But \S\ref{acc-sec} demonstrates
   3.238 -that~$\pow$ is still useful in inductive definitions.
   3.239 -
   3.240 -\section{Elements of an inductive or coinductive definition}\label{basic-sec}
   3.241 -Consider a (co)inductive definition of the sets $R_1$, \ldots,~$R_n$, in
   3.242 -mutual recursion.  They will be constructed from domains $D_1$,
   3.243 -\ldots,~$D_n$, respectively.  The construction yields not $R_i\sbs D_i$ but
   3.244 -$R_i\sbs D_1+\cdots+D_n$, where $R_i$ is contained in the image of~$D_i$
   3.245 -under an injection.  Reasons for this are discussed
   3.246 -elsewhere~\cite[\S4.5]{paulson-set-II}.
   3.247 -
   3.248 -The definition may involve arbitrary parameters $\vec{p}=p_1$,
   3.249 -\ldots,~$p_k$.  Each recursive set then has the form $R_i(\vec{p})$.  The
   3.250 -parameters must be identical every time they occur within a definition.  This
   3.251 -would appear to be a serious restriction compared with other systems such as
   3.252 -Coq~\cite{paulin-tlca}.  For instance, we cannot define the lists of
   3.253 -$n$ elements as the set $\listn(A,n)$ using rules where the parameter~$n$
   3.254 -varies.  Section~\ref{listn-sec} describes how to express this set using the
   3.255 -inductive definition package.
   3.256 -
   3.257 -To avoid clutter below, the recursive sets are shown as simply $R_i$
   3.258 -instead of~$R_i(\vec{p})$.
   3.259 -
   3.260 -\subsection{The form of the introduction rules}\label{intro-sec}
   3.261 -The body of the definition consists of the desired introduction rules.  The
   3.262 -conclusion of each rule must have the form $t\in R_i$, where $t$ is any term.
   3.263 -Premises typically have the same form, but they can have the more general form
   3.264 -$t\in M(R_i)$ or express arbitrary side-conditions.
   3.265 -
   3.266 -The premise $t\in M(R_i)$ is permitted if $M$ is a monotonic operator on
   3.267 -sets, satisfying the rule 
   3.268 -\[ \infer{M(A)\sbs M(B)}{A\sbs B} \]
   3.269 -The user must supply the package with monotonicity rules for all such premises.
   3.270 -
   3.271 -The ability to introduce new monotone operators makes the approach
   3.272 -flexible.  A suitable choice of~$M$ and~$t$ can express a lot.  The
   3.273 -powerset operator $\pow$ is monotone, and the premise $t\in\pow(R)$
   3.274 -expresses $t\sbs R$; see \S\ref{acc-sec} for an example.  The \emph{list of}
   3.275 -operator is monotone, as is easily proved by induction.  The premise
   3.276 -$t\in\lst(R)$ avoids having to encode the effect of~$\lst(R)$ using mutual
   3.277 -recursion; see \S\ref{primrec-sec} and also my earlier
   3.278 -paper~\cite[\S4.4]{paulson-set-II}.
   3.279 -
   3.280 -Introduction rules may also contain \defn{side-conditions}.  These are
   3.281 -premises consisting of arbitrary formul{\ae} not mentioning the recursive
   3.282 -sets. Side-conditions typically involve type-checking.  One example is the
   3.283 -premise $a\in A$ in the following rule from the definition of lists:
   3.284 -\[ \infer{\Cons(a,l)\in\lst(A)}{a\in A & l\in\lst(A)} \]
   3.285 -
   3.286 -\subsection{The fixedpoint definitions}
   3.287 -The package translates the list of desired introduction rules into a fixedpoint
   3.288 -definition.  Consider, as a running example, the finite powerset operator
   3.289 -$\Fin(A)$: the set of all finite subsets of~$A$.  It can be
   3.290 -defined as the least set closed under the rules
   3.291 -\[  \emptyset\in\Fin(A)  \qquad 
   3.292 -    \infer{\{a\}\un b\in\Fin(A)}{a\in A & b\in\Fin(A)} 
   3.293 -\]
   3.294 -
   3.295 -The domain in a (co)inductive definition must be some existing set closed
   3.296 -under the rules.  A suitable domain for $\Fin(A)$ is $\pow(A)$, the set of all
   3.297 -subsets of~$A$.  The package generates the definition
   3.298 -\[  \Fin(A) \equiv \lfp(\pow(A), \,
   3.299 -  \begin{array}[t]{r@{\,}l}
   3.300 -      \lambda X. \{z\in\pow(A). & z=\emptyset \disj{} \\
   3.301 -                  &(\exists a\,b. z=\{a\}\un b\conj a\in A\conj b\in X)\})
   3.302 -  \end{array}
   3.303 -\]
   3.304 -The contribution of each rule to the definition of $\Fin(A)$ should be
   3.305 -obvious.  A coinductive definition is similar but uses $\gfp$ instead
   3.306 -of~$\lfp$.
   3.307 -
   3.308 -The package must prove that the fixedpoint operator is applied to a
   3.309 -monotonic function.  If the introduction rules have the form described
   3.310 -above, and if the package is supplied a monotonicity theorem for every
   3.311 -$t\in M(R_i)$ premise, then this proof is trivial.\footnote{Due to the
   3.312 -  presence of logical connectives in the fixedpoint's body, the
   3.313 -  monotonicity proof requires some unusual rules.  These state that the
   3.314 -  connectives $\conj$, $\disj$ and $\exists$ preserve monotonicity with respect
   3.315 -  to the partial ordering on unary predicates given by $P\sqsubseteq Q$ if and
   3.316 -  only if $\forall x.P(x)\imp Q(x)$.}
   3.317 -
   3.318 -The package returns its result as an \textsc{ml} structure, which consists of named
   3.319 -components; we may regard it as a record.  The result structure contains
   3.320 -the definitions of the recursive sets as a theorem list called {\tt defs}.
   3.321 -It also contains some theorems; {\tt dom\_subset} is an inclusion such as 
   3.322 -$\Fin(A)\sbs\pow(A)$, while {\tt bnd\_mono} asserts that the fixedpoint
   3.323 -definition is monotonic.
   3.324 -
   3.325 -Internally the package uses the theorem {\tt unfold}, a fixedpoint equation
   3.326 -such as
   3.327 -\[
   3.328 -  \begin{array}[t]{r@{\,}l}
   3.329 -     \Fin(A) = \{z\in\pow(A). & z=\emptyset \disj{} \\
   3.330 -             &(\exists a\,b. z=\{a\}\un b\conj a\in A\conj b\in \Fin(A))\}
   3.331 -  \end{array}
   3.332 -\]
   3.333 -In order to save space, this theorem is not exported.  
   3.334 -
   3.335 -
   3.336 -\subsection{Mutual recursion} \label{mutual-sec}
   3.337 -In a mutually recursive definition, the domain of the fixedpoint construction
   3.338 -is the disjoint sum of the domain~$D_i$ of each~$R_i$, for $i=1$,
   3.339 -\ldots,~$n$.  The package uses the injections of the
   3.340 -binary disjoint sum, typically $\Inl$ and~$\Inr$, to express injections
   3.341 -$h_{1n}$, \ldots, $h_{nn}$ for the $n$-ary disjoint sum $D_1+\cdots+D_n$.
   3.342 -
   3.343 -As discussed elsewhere \cite[\S4.5]{paulson-set-II}, Isabelle/\textsc{zf} defines the
   3.344 -operator $\Part$ to support mutual recursion.  The set $\Part(A,h)$
   3.345 -contains those elements of~$A$ having the form~$h(z)$:
   3.346 -\[ \Part(A,h)  \equiv \{x\in A. \exists z. x=h(z)\}. \]   
   3.347 -For mutually recursive sets $R_1$, \ldots,~$R_n$ with
   3.348 -$n>1$, the package makes $n+1$ definitions.  The first defines a set $R$ using
   3.349 -a fixedpoint operator. The remaining $n$ definitions have the form
   3.350 -\[ R_i \equiv \Part(R,h_{in}), \qquad i=1,\ldots, n.  \] 
   3.351 -It follows that $R=R_1\un\cdots\un R_n$, where the $R_i$ are pairwise disjoint.
   3.352 -
   3.353 -
   3.354 -\subsection{Proving the introduction rules}
   3.355 -The user supplies the package with the desired form of the introduction
   3.356 -rules.  Once it has derived the theorem {\tt unfold}, it attempts
   3.357 -to prove those rules.  From the user's point of view, this is the
   3.358 -trickiest stage; the proofs often fail.  The task is to show that the domain 
   3.359 -$D_1+\cdots+D_n$ of the combined set $R_1\un\cdots\un R_n$ is
   3.360 -closed under all the introduction rules.  This essentially involves replacing
   3.361 -each~$R_i$ by $D_1+\cdots+D_n$ in each of the introduction rules and
   3.362 -attempting to prove the result.
   3.363 -
   3.364 -Consider the $\Fin(A)$ example.  After substituting $\pow(A)$ for $\Fin(A)$
   3.365 -in the rules, the package must prove
   3.366 -\[  \emptyset\in\pow(A)  \qquad 
   3.367 -    \infer{\{a\}\un b\in\pow(A)}{a\in A & b\in\pow(A)} 
   3.368 -\]
   3.369 -Such proofs can be regarded as type-checking the definition.\footnote{The
   3.370 -  Isabelle/\textsc{hol} version does not require these proofs, as \textsc{hol}
   3.371 -  has implicit type-checking.} The user supplies the package with
   3.372 -type-checking rules to apply.  Usually these are general purpose rules from
   3.373 -the \textsc{zf} theory.  They could however be rules specifically proved for a
   3.374 -particular inductive definition; sometimes this is the easiest way to get the
   3.375 -definition through!
   3.376 -
   3.377 -The result structure contains the introduction rules as the theorem list {\tt
   3.378 -intrs}.
   3.379 -
   3.380 -\subsection{The case analysis rule}
   3.381 -The elimination rule, called {\tt elim}, performs case analysis.  It is a
   3.382 -simple consequence of {\tt unfold}.  There is one case for each introduction
   3.383 -rule.  If $x\in\Fin(A)$ then either $x=\emptyset$ or else $x=\{a\}\un b$ for
   3.384 -some $a\in A$ and $b\in\Fin(A)$.  Formally, the elimination rule for $\Fin(A)$
   3.385 -is written
   3.386 -\[ \infer{Q}{x\in\Fin(A) & \infer*{Q}{[x=\emptyset]}
   3.387 -                 & \infer*{Q}{[x=\{a\}\un b & a\in A &b\in\Fin(A)]_{a,b}} }
   3.388 -\]
   3.389 -The subscripted variables $a$ and~$b$ above the third premise are
   3.390 -eigenvariables, subject to the usual ``not free in \ldots'' proviso.
   3.391 -
   3.392 -
   3.393 -\section{Induction and coinduction rules}
   3.394 -Here we must consider inductive and coinductive definitions separately.  For
   3.395 -an inductive definition, the package returns an induction rule derived
   3.396 -directly from the properties of least fixedpoints, as well as a modified rule
   3.397 -for mutual recursion.  For a coinductive definition, the package returns a
   3.398 -basic coinduction rule.
   3.399 -
   3.400 -\subsection{The basic induction rule}\label{basic-ind-sec}
   3.401 -The basic rule, called {\tt induct}, is appropriate in most situations.
   3.402 -For inductive definitions, it is strong rule induction~\cite{camilleri92}; for
   3.403 -datatype definitions (see below), it is just structural induction.  
   3.404 -
   3.405 -The induction rule for an inductively defined set~$R$ has the form described
   3.406 -below.  For the time being, assume that $R$'s domain is not a Cartesian
   3.407 -product; inductively defined relations are treated slightly differently.
   3.408 -
   3.409 -The major premise is $x\in R$.  There is a minor premise for each
   3.410 -introduction rule:
   3.411 -\begin{itemize}
   3.412 -\item If the introduction rule concludes $t\in R_i$, then the minor premise
   3.413 -is~$P(t)$.
   3.414 -
   3.415 -\item The minor premise's eigenvariables are precisely the introduction
   3.416 -rule's free variables that are not parameters of~$R$.  For instance, the
   3.417 -eigenvariables in the $\Fin(A)$ rule below are $a$ and $b$, but not~$A$.
   3.418 -
   3.419 -\item If the introduction rule has a premise $t\in R_i$, then the minor
   3.420 -premise discharges the assumption $t\in R_i$ and the induction
   3.421 -hypothesis~$P(t)$.  If the introduction rule has a premise $t\in M(R_i)$
   3.422 -then the minor premise discharges the single assumption
   3.423 -\[ t\in M(\{z\in R_i. P(z)\}). \] 
   3.424 -Because $M$ is monotonic, this assumption implies $t\in M(R_i)$.  The
   3.425 -occurrence of $P$ gives the effect of an induction hypothesis, which may be
   3.426 -exploited by appealing to properties of~$M$.
   3.427 -\end{itemize}
   3.428 -The induction rule for $\Fin(A)$ resembles the elimination rule shown above,
   3.429 -but includes an induction hypothesis:
   3.430 -\[ \infer{P(x)}{x\in\Fin(A) & P(\emptyset)
   3.431 -        & \infer*{P(\{a\}\un b)}{[a\in A & b\in\Fin(A) & P(b)]_{a,b}} }
   3.432 -\] 
   3.433 -Stronger induction rules often suggest themselves.  We can derive a rule for
   3.434 -$\Fin(A)$ whose third premise discharges the extra assumption $a\not\in b$.
   3.435 -The package provides rules for mutual induction and inductive relations.  The
   3.436 -Isabelle/\textsc{zf} theory also supports well-founded induction and recursion
   3.437 -over datatypes, by reasoning about the \defn{rank} of a
   3.438 -set~\cite[\S3.4]{paulson-set-II}.
   3.439 -
   3.440 -
   3.441 -\subsection{Modified induction rules}
   3.442 -
   3.443 -If the domain of $R$ is a Cartesian product $A_1\times\cdots\times A_m$
   3.444 -(however nested), then the corresponding predicate $P_i$ takes $m$ arguments.
   3.445 -The major premise becomes $\pair{z_1,\ldots,z_m}\in R$ instead of $x\in R$;
   3.446 -the conclusion becomes $P(z_1,\ldots,z_m)$.  This simplifies reasoning about
   3.447 -inductively defined relations, eliminating the need to express properties of
   3.448 -$z_1$, \ldots,~$z_m$ as properties of the tuple $\pair{z_1,\ldots,z_m}$.
   3.449 -Occasionally it may require you to split up the induction variable
   3.450 -using {\tt SigmaE} and {\tt dom\_subset}, especially if the constant {\tt
   3.451 -  split} appears in the rule.
   3.452 -
   3.453 -The mutual induction rule is called {\tt
   3.454 -mutual\_induct}.  It differs from the basic rule in two respects:
   3.455 -\begin{itemize}
   3.456 -\item Instead of a single predicate~$P$, it uses $n$ predicates $P_1$,
   3.457 -\ldots,~$P_n$: one for each recursive set.
   3.458 -
   3.459 -\item There is no major premise such as $x\in R_i$.  Instead, the conclusion
   3.460 -refers to all the recursive sets:
   3.461 -\[ (\forall z.z\in R_1\imp P_1(z))\conj\cdots\conj
   3.462 -   (\forall z.z\in R_n\imp P_n(z))
   3.463 -\]
   3.464 -Proving the premises establishes $P_i(z)$ for $z\in R_i$ and $i=1$,
   3.465 -\ldots,~$n$.
   3.466 -\end{itemize}
   3.467 -%
   3.468 -If the domain of some $R_i$ is a Cartesian product, then the mutual induction
   3.469 -rule is modified accordingly.  The predicates are made to take $m$ separate
   3.470 -arguments instead of a tuple, and the quantification in the conclusion is over
   3.471 -the separate variables $z_1$, \ldots, $z_m$.
   3.472 -
   3.473 -\subsection{Coinduction}\label{coind-sec}
   3.474 -A coinductive definition yields a primitive coinduction rule, with no
   3.475 -refinements such as those for the induction rules.  (Experience may suggest
   3.476 -refinements later.)  Consider the codatatype of lazy lists as an example.  For
   3.477 -suitable definitions of $\LNil$ and $\LCons$, lazy lists may be defined as the
   3.478 -greatest set consistent with the rules
   3.479 -\[  \LNil\in\llist(A)  \qquad 
   3.480 -    \infer[(-)]{\LCons(a,l)\in\llist(A)}{a\in A & l\in\llist(A)}
   3.481 -\]
   3.482 -The $(-)$ tag stresses that this is a coinductive definition.  A suitable
   3.483 -domain for $\llist(A)$ is $\quniv(A)$; this set is closed under the variant
   3.484 -forms of sum and product that are used to represent non-well-founded data
   3.485 -structures (see~\S\ref{univ-sec}).
   3.486 -
   3.487 -The package derives an {\tt unfold} theorem similar to that for $\Fin(A)$. 
   3.488 -Then it proves the theorem {\tt coinduct}, which expresses that $\llist(A)$
   3.489 -is the greatest solution to this equation contained in $\quniv(A)$:
   3.490 -\[ \infer{x\in\llist(A)}{x\in X & X\sbs \quniv(A) &
   3.491 -    \infer*{
   3.492 -     \begin{array}[b]{r@{}l}
   3.493 -       z=\LNil\disj 
   3.494 -       \bigl(\exists a\,l.\, & z=\LCons(a,l) \conj a\in A \conj{}\\
   3.495 -                             & l\in X\un\llist(A) \bigr)
   3.496 -     \end{array}  }{[z\in X]_z}}
   3.497 -\]
   3.498 -This rule complements the introduction rules; it provides a means of showing
   3.499 -$x\in\llist(A)$ when $x$ is infinite.  For instance, if $x=\LCons(0,x)$ then
   3.500 -applying the rule with $X=\{x\}$ proves $x\in\llist(\nat)$.  (Here $\nat$
   3.501 -is the set of natural numbers.)
   3.502 -
   3.503 -Having $X\un\llist(A)$ instead of simply $X$ in the third premise above
   3.504 -represents a slight strengthening of the greatest fixedpoint property.  I
   3.505 -discuss several forms of coinduction rules elsewhere~\cite{paulson-coind}.
   3.506 -
   3.507 -The clumsy form of the third premise makes the rule hard to use, especially in
   3.508 -large definitions.  Probably a constant should be declared to abbreviate the
   3.509 -large disjunction, and rules derived to allow proving the separate disjuncts.
   3.510 -
   3.511 -
   3.512 -\section{Examples of inductive and coinductive definitions}\label{ind-eg-sec}
   3.513 -This section presents several examples from the literature: the finite
   3.514 -powerset operator, lists of $n$ elements, bisimulations on lazy lists, the
   3.515 -well-founded part of a relation, and the primitive recursive functions.
   3.516 -
   3.517 -\subsection{The finite powerset operator}
   3.518 -This operator has been discussed extensively above.  Here is the
   3.519 -corresponding invocation in an Isabelle theory file.  Note that
   3.520 -$\cons(a,b)$ abbreviates $\{a\}\un b$ in Isabelle/\textsc{zf}.
   3.521 -\begin{ttbox}
   3.522 -Finite = Arith + 
   3.523 -consts      Fin :: i=>i
   3.524 -inductive
   3.525 -  domains   "Fin(A)" <= "Pow(A)"
   3.526 -  intrs
   3.527 -    emptyI  "0 : Fin(A)"
   3.528 -    consI   "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"
   3.529 -  type_intrs  empty_subsetI, cons_subsetI, PowI
   3.530 -  type_elims "[make_elim PowD]"
   3.531 -end
   3.532 -\end{ttbox}
   3.533 -Theory {\tt Finite} extends the parent theory {\tt Arith} by declaring the
   3.534 -unary function symbol~$\Fin$, which is defined inductively.  Its domain is
   3.535 -specified as $\pow(A)$, where $A$ is the parameter appearing in the
   3.536 -introduction rules.  For type-checking, we supply two introduction
   3.537 -rules:
   3.538 -\[ \emptyset\sbs A              \qquad
   3.539 -   \infer{\{a\}\un B\sbs C}{a\in C & B\sbs C}
   3.540 -\]
   3.541 -A further introduction rule and an elimination rule express both
   3.542 -directions of the equivalence $A\in\pow(B)\bimp A\sbs B$.  Type-checking
   3.543 -involves mostly introduction rules.  
   3.544 -
   3.545 -Like all Isabelle theory files, this one yields a structure containing the
   3.546 -new theory as an \textsc{ml} value.  Structure {\tt Finite} also has a
   3.547 -substructure, called~{\tt Fin}.  After declaring \hbox{\tt open Finite;} we
   3.548 -can refer to the $\Fin(A)$ introduction rules as the list {\tt Fin.intrs}
   3.549 -or individually as {\tt Fin.emptyI} and {\tt Fin.consI}.  The induction
   3.550 -rule is {\tt Fin.induct}.
   3.551 -
   3.552 -
   3.553 -\subsection{Lists of $n$ elements}\label{listn-sec}
   3.554 -This has become a standard example of an inductive definition.  Following
   3.555 -Paulin-Mohring~\cite{paulin-tlca}, we could attempt to define a new datatype
   3.556 -$\listn(A,n)$, for lists of length~$n$, as an $n$-indexed family of sets.
   3.557 -But her introduction rules
   3.558 -\[ \hbox{\tt Niln}\in\listn(A,0)  \qquad
   3.559 -   \infer{\hbox{\tt Consn}(n,a,l)\in\listn(A,\succ(n))}
   3.560 -         {n\in\nat & a\in A & l\in\listn(A,n)}
   3.561 -\]
   3.562 -are not acceptable to the inductive definition package:
   3.563 -$\listn$ occurs with three different parameter lists in the definition.
   3.564 -
   3.565 -The Isabelle version of this example suggests a general treatment of
   3.566 -varying parameters.  It uses the existing datatype definition of
   3.567 -$\lst(A)$, with constructors $\Nil$ and~$\Cons$, and incorporates the
   3.568 -parameter~$n$ into the inductive set itself.  It defines $\listn(A)$ as a
   3.569 -relation consisting of pairs $\pair{n,l}$ such that $n\in\nat$
   3.570 -and~$l\in\lst(A)$ and $l$ has length~$n$.  In fact, $\listn(A)$ is the
   3.571 -converse of the length function on~$\lst(A)$.  The Isabelle/\textsc{zf} introduction
   3.572 -rules are
   3.573 -\[ \pair{0,\Nil}\in\listn(A)  \qquad
   3.574 -   \infer{\pair{\succ(n),\Cons(a,l)}\in\listn(A)}
   3.575 -         {a\in A & \pair{n,l}\in\listn(A)}
   3.576 -\]
   3.577 -The Isabelle theory file takes, as parent, the theory~{\tt List} of lists.
   3.578 -We declare the constant~$\listn$ and supply an inductive definition,
   3.579 -specifying the domain as $\nat\times\lst(A)$:
   3.580 -\begin{ttbox}
   3.581 -ListN = List +
   3.582 -consts  listn :: i=>i
   3.583 -inductive
   3.584 -  domains   "listn(A)" <= "nat*list(A)"
   3.585 -  intrs
   3.586 -    NilI  "<0,Nil>: listn(A)"
   3.587 -    ConsI "[| a:A; <n,l>:listn(A) |] ==> <succ(n), Cons(a,l)>: listn(A)"
   3.588 -  type_intrs "nat_typechecks @ list.intrs"
   3.589 -end
   3.590 -\end{ttbox}
   3.591 -The type-checking rules include those for 0, $\succ$, $\Nil$ and $\Cons$.
   3.592 -Because $\listn(A)$ is a set of pairs, type-checking requires the
   3.593 -equivalence $\pair{a,b}\in A\times B \bimp a\in A \conj b\in B$.  The
   3.594 -package always includes the rules for ordered pairs.
   3.595 -
   3.596 -The package returns introduction, elimination and induction rules for
   3.597 -$\listn$.  The basic induction rule, {\tt listn.induct}, is
   3.598 -\[ \infer{P(z_1,z_2)}{\pair{z_1,z_2}\in\listn(A) & P(0,\Nil) &
   3.599 -             \infer*{P(\succ(n),\Cons(a,l))}
   3.600 -                {[a\in A & \pair{n,l}\in\listn(A) & P(n,l)]_{a,l,n}}}
   3.601 -\]
   3.602 -This rule lets the induction formula to be a 
   3.603 -binary property of pairs, $P(n,l)$.  
   3.604 -It is now a simple matter to prove theorems about $\listn(A)$, such as
   3.605 -\[ \forall l\in\lst(A). \pair{\length(l),\, l}\in\listn(A) \]
   3.606 -\[ \listn(A)``\{n\} = \{l\in\lst(A). \length(l)=n\} \]
   3.607 -This latter result --- here $r``X$ denotes the image of $X$ under $r$
   3.608 ---- asserts that the inductive definition agrees with the obvious notion of
   3.609 -$n$-element list.  
   3.610 -
   3.611 -A ``list of $n$ elements'' really is a list, namely an element of ~$\lst(A)$.
   3.612 -It is subject to list operators such as append (concatenation).  For example,
   3.613 -a trivial induction on $\pair{m,l}\in\listn(A)$ yields
   3.614 -\[ \infer{\pair{m\mathbin{+} m',\, l@l'}\in\listn(A)}
   3.615 -         {\pair{m,l}\in\listn(A) & \pair{m',l'}\in\listn(A)} 
   3.616 -\]
   3.617 -where $+$ denotes addition on the natural numbers and @ denotes append.
   3.618 -
   3.619 -\subsection{Rule inversion: the function \texttt{mk\_cases}}
   3.620 -The elimination rule, {\tt listn.elim}, is cumbersome:
   3.621 -\[ \infer{Q}{x\in\listn(A) & 
   3.622 -          \infer*{Q}{[x = \pair{0,\Nil}]} &
   3.623 -          \infer*{Q}
   3.624 -             {\left[\begin{array}{l}
   3.625 -               x = \pair{\succ(n),\Cons(a,l)} \\
   3.626 -               a\in A \\
   3.627 -               \pair{n,l}\in\listn(A)
   3.628 -               \end{array} \right]_{a,l,n}}}
   3.629 -\]
   3.630 -The \textsc{ml} function {\tt listn.mk\_cases} generates simplified instances of
   3.631 -this rule.  It works by freeness reasoning on the list constructors:
   3.632 -$\Cons(a,l)$ is injective in its two arguments and differs from~$\Nil$.  If
   3.633 -$x$ is $\pair{i,\Nil}$ or $\pair{i,\Cons(a,l)}$ then {\tt listn.mk\_cases}
   3.634 -deduces the corresponding form of~$i$;  this is called rule inversion.  
   3.635 -Here is a sample session: 
   3.636 -\begin{ttbox}
   3.637 -listn.mk_cases "<i,Nil> : listn(A)";
   3.638 -{\out "[| <?i, []> : listn(?A); ?i = 0 ==> ?Q |] ==> ?Q" : thm}
   3.639 -listn.mk_cases "<i,Cons(a,l)> : listn(A)";
   3.640 -{\out "[| <?i, Cons(?a, ?l)> : listn(?A);}
   3.641 -{\out     !!n. [| ?a : ?A; <n, ?l> : listn(?A); ?i = succ(n) |] ==> ?Q }
   3.642 -{\out  |] ==> ?Q" : thm}
   3.643 -\end{ttbox}
   3.644 -Each of these rules has only two premises.  In conventional notation, the
   3.645 -second rule is
   3.646 -\[ \infer{Q}{\pair{i, \Cons(a,l)}\in\listn(A) & 
   3.647 -          \infer*{Q}
   3.648 -             {\left[\begin{array}{l}
   3.649 -               a\in A \\ \pair{n,l}\in\listn(A) \\ i = \succ(n)
   3.650 -               \end{array} \right]_{n}}}
   3.651 -\]
   3.652 -The package also has built-in rules for freeness reasoning about $0$
   3.653 -and~$\succ$.  So if $x$ is $\pair{0,l}$ or $\pair{\succ(i),l}$, then {\tt
   3.654 -listn.mk\_cases} can deduce the corresponding form of~$l$. 
   3.655 -
   3.656 -The function {\tt mk\_cases} is also useful with datatype definitions.  The
   3.657 -instance from the definition of lists, namely {\tt list.mk\_cases}, can
   3.658 -prove that $\Cons(a,l)\in\lst(A)$ implies $a\in A $ and $l\in\lst(A)$:
   3.659 -\[ \infer{Q}{\Cons(a,l)\in\lst(A) & 
   3.660 -                 & \infer*{Q}{[a\in A &l\in\lst(A)]} }
   3.661 -\]
   3.662 -A typical use of {\tt mk\_cases} concerns inductive definitions of evaluation
   3.663 -relations.  Then rule inversion yields case analysis on possible evaluations.
   3.664 -For example, Isabelle/\textsc{zf} includes a short proof of the
   3.665 -diamond property for parallel contraction on combinators.  Ole Rasmussen used
   3.666 -{\tt mk\_cases} extensively in his development of the theory of
   3.667 -residuals~\cite{rasmussen95}.
   3.668 -
   3.669 -
   3.670 -\subsection{A coinductive definition: bisimulations on lazy lists}
   3.671 -This example anticipates the definition of the codatatype $\llist(A)$, which
   3.672 -consists of finite and infinite lists over~$A$.  Its constructors are $\LNil$
   3.673 -and~$\LCons$, satisfying the introduction rules shown in~\S\ref{coind-sec}.  
   3.674 -Because $\llist(A)$ is defined as a greatest fixedpoint and uses the variant
   3.675 -pairing and injection operators, it contains non-well-founded elements such as
   3.676 -solutions to $\LCons(a,l)=l$.
   3.677 -
   3.678 -The next step in the development of lazy lists is to define a coinduction
   3.679 -principle for proving equalities.  This is done by showing that the equality
   3.680 -relation on lazy lists is the greatest fixedpoint of some monotonic
   3.681 -operation.  The usual approach~\cite{pitts94} is to define some notion of 
   3.682 -bisimulation for lazy lists, define equivalence to be the greatest
   3.683 -bisimulation, and finally to prove that two lazy lists are equivalent if and
   3.684 -only if they are equal.  The coinduction rule for equivalence then yields a
   3.685 -coinduction principle for equalities.
   3.686 -
   3.687 -A binary relation $R$ on lazy lists is a \defn{bisimulation} provided $R\sbs
   3.688 -R^+$, where $R^+$ is the relation
   3.689 -\[ \{\pair{\LNil,\LNil}\} \un 
   3.690 -   \{\pair{\LCons(a,l),\LCons(a,l')} . a\in A \conj \pair{l,l'}\in R\}.
   3.691 -\]
   3.692 -A pair of lazy lists are \defn{equivalent} if they belong to some
   3.693 -bisimulation.  Equivalence can be coinductively defined as the greatest
   3.694 -fixedpoint for the introduction rules
   3.695 -\[  \pair{\LNil,\LNil} \in\lleq(A)  \qquad 
   3.696 -    \infer[(-)]{\pair{\LCons(a,l),\LCons(a,l')} \in\lleq(A)}
   3.697 -          {a\in A & \pair{l,l'}\in \lleq(A)}
   3.698 -\]
   3.699 -To make this coinductive definition, the theory file includes (after the
   3.700 -declaration of $\llist(A)$) the following lines:
   3.701 -\bgroup\leftmargini=\parindent
   3.702 -\begin{ttbox}
   3.703 -consts    lleq :: i=>i
   3.704 -coinductive
   3.705 -  domains "lleq(A)" <= "llist(A) * llist(A)"
   3.706 -  intrs
   3.707 -    LNil  "<LNil,LNil> : lleq(A)"
   3.708 -    LCons "[| a:A; <l,l'>:lleq(A) |] ==> <LCons(a,l),LCons(a,l')>: lleq(A)"
   3.709 -  type_intrs  "llist.intrs"
   3.710 -\end{ttbox}
   3.711 -\egroup
   3.712 -The domain of $\lleq(A)$ is $\llist(A)\times\llist(A)$.  The type-checking
   3.713 -rules include the introduction rules for $\llist(A)$, whose 
   3.714 -declaration is discussed below (\S\ref{lists-sec}).
   3.715 -
   3.716 -The package returns the introduction rules and the elimination rule, as
   3.717 -usual.  But instead of induction rules, it returns a coinduction rule.
   3.718 -The rule is too big to display in the usual notation; its conclusion is
   3.719 -$x\in\lleq(A)$ and its premises are $x\in X$, 
   3.720 -${X\sbs\llist(A)\times\llist(A)}$ and
   3.721 -\[ \infer*{z=\pair{\LNil,\LNil}\disj \bigl(\exists a\,l\,l'.\,
   3.722 -     \begin{array}[t]{@{}l}
   3.723 -       z=\pair{\LCons(a,l),\LCons(a,l')} \conj a\in A \conj{}\\
   3.724 -       \pair{l,l'}\in X\un\lleq(A) \bigr)
   3.725 -     \end{array}  
   3.726 -    }{[z\in X]_z}
   3.727 -\]
   3.728 -Thus if $x\in X$, where $X$ is a bisimulation contained in the
   3.729 -domain of $\lleq(A)$, then $x\in\lleq(A)$.  It is easy to show that
   3.730 -$\lleq(A)$ is reflexive: the equality relation is a bisimulation.  And
   3.731 -$\lleq(A)$ is symmetric: its converse is a bisimulation.  But showing that
   3.732 -$\lleq(A)$ coincides with the equality relation takes some work.
   3.733 -
   3.734 -\subsection{The accessible part of a relation}\label{acc-sec}
   3.735 -Let $\prec$ be a binary relation on~$D$; in short, $(\prec)\sbs D\times D$.
   3.736 -The \defn{accessible} or \defn{well-founded} part of~$\prec$, written
   3.737 -$\acc(\prec)$, is essentially that subset of~$D$ for which $\prec$ admits
   3.738 -no infinite decreasing chains~\cite{aczel77}.  Formally, $\acc(\prec)$ is
   3.739 -inductively defined to be the least set that contains $a$ if it contains
   3.740 -all $\prec$-predecessors of~$a$, for $a\in D$.  Thus we need an
   3.741 -introduction rule of the form 
   3.742 -\[ \infer{a\in\acc(\prec)}{\forall y.y\prec a\imp y\in\acc(\prec)} \]
   3.743 -Paulin-Mohring treats this example in Coq~\cite{paulin-tlca}, but it causes
   3.744 -difficulties for other systems.  Its premise is not acceptable to the
   3.745 -inductive definition package of the Cambridge \textsc{hol}
   3.746 -system~\cite{camilleri92}.  It is also unacceptable to the Isabelle package
   3.747 -(recall \S\ref{intro-sec}), but fortunately can be transformed into the
   3.748 -acceptable form $t\in M(R)$.
   3.749 -
   3.750 -The powerset operator is monotonic, and $t\in\pow(R)$ is equivalent to
   3.751 -$t\sbs R$.  This in turn is equivalent to $\forall y\in t. y\in R$.  To
   3.752 -express $\forall y.y\prec a\imp y\in\acc(\prec)$ we need only find a
   3.753 -term~$t$ such that $y\in t$ if and only if $y\prec a$.  A suitable $t$ is
   3.754 -the inverse image of~$\{a\}$ under~$\prec$.
   3.755 -
   3.756 -The definition below follows this approach.  Here $r$ is~$\prec$ and
   3.757 -$\field(r)$ refers to~$D$, the domain of $\acc(r)$.  (The field of a
   3.758 -relation is the union of its domain and range.)  Finally $r^{-}``\{a\}$
   3.759 -denotes the inverse image of~$\{a\}$ under~$r$.  We supply the theorem {\tt
   3.760 -  Pow\_mono}, which asserts that $\pow$ is monotonic.
   3.761 -\begin{ttbox}
   3.762 -consts    acc :: i=>i
   3.763 -inductive
   3.764 -  domains "acc(r)" <= "field(r)"
   3.765 -  intrs
   3.766 -    vimage  "[| r-``\{a\}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"
   3.767 -  monos      Pow_mono
   3.768 -\end{ttbox}
   3.769 -The Isabelle theory proceeds to prove facts about $\acc(\prec)$.  For
   3.770 -instance, $\prec$ is well-founded if and only if its field is contained in
   3.771 -$\acc(\prec)$.  
   3.772 -
   3.773 -As mentioned in~\S\ref{basic-ind-sec}, a premise of the form $t\in M(R)$
   3.774 -gives rise to an unusual induction hypothesis.  Let us examine the
   3.775 -induction rule, {\tt acc.induct}:
   3.776 -\[ \infer{P(x)}{x\in\acc(r) &
   3.777 -     \infer*{P(a)}{\left[
   3.778 -                   \begin{array}{r@{}l}
   3.779 -                     r^{-}``\{a\} &\, \in\pow(\{z\in\acc(r).P(z)\}) \\
   3.780 -                                a &\, \in\field(r)
   3.781 -                   \end{array}
   3.782 -                   \right]_a}}
   3.783 -\]
   3.784 -The strange induction hypothesis is equivalent to
   3.785 -$\forall y. \pair{y,a}\in r\imp y\in\acc(r)\conj P(y)$.
   3.786 -Therefore the rule expresses well-founded induction on the accessible part
   3.787 -of~$\prec$.
   3.788 -
   3.789 -The use of inverse image is not essential.  The Isabelle package can accept
   3.790 -introduction rules with arbitrary premises of the form $\forall
   3.791 -\vec{y}.P(\vec{y})\imp f(\vec{y})\in R$.  The premise can be expressed
   3.792 -equivalently as 
   3.793 -\[ \{z\in D. P(\vec{y}) \conj z=f(\vec{y})\} \in \pow(R) \] 
   3.794 -provided $f(\vec{y})\in D$ for all $\vec{y}$ such that~$P(\vec{y})$.  The
   3.795 -following section demonstrates another use of the premise $t\in M(R)$,
   3.796 -where $M=\lst$. 
   3.797 -
   3.798 -\subsection{The primitive recursive functions}\label{primrec-sec}
   3.799 -The primitive recursive functions are traditionally defined inductively, as
   3.800 -a subset of the functions over the natural numbers.  One difficulty is that
   3.801 -functions of all arities are taken together, but this is easily
   3.802 -circumvented by regarding them as functions on lists.  Another difficulty,
   3.803 -the notion of composition, is less easily circumvented.
   3.804 -
   3.805 -Here is a more precise definition.  Letting $\vec{x}$ abbreviate
   3.806 -$x_0,\ldots,x_{n-1}$, we can write lists such as $[\vec{x}]$,
   3.807 -$[y+1,\vec{x}]$, etc.  A function is \defn{primitive recursive} if it
   3.808 -belongs to the least set of functions in $\lst(\nat)\to\nat$ containing
   3.809 -\begin{itemize}
   3.810 -\item The \defn{successor} function $\SC$, such that $\SC[y,\vec{x}]=y+1$.
   3.811 -\item All \defn{constant} functions $\CONST(k)$, such that
   3.812 -  $\CONST(k)[\vec{x}]=k$. 
   3.813 -\item All \defn{projection} functions $\PROJ(i)$, such that
   3.814 -  $\PROJ(i)[\vec{x}]=x_i$ if $0\leq i<n$. 
   3.815 -\item All \defn{compositions} $\COMP(g,[f_0,\ldots,f_{m-1}])$, 
   3.816 -where $g$ and $f_0$, \ldots, $f_{m-1}$ are primitive recursive,
   3.817 -such that
   3.818 -\[ \COMP(g,[f_0,\ldots,f_{m-1}])[\vec{x}] = 
   3.819 -   g[f_0[\vec{x}],\ldots,f_{m-1}[\vec{x}]]. \] 
   3.820 -
   3.821 -\item All \defn{recursions} $\PREC(f,g)$, where $f$ and $g$ are primitive
   3.822 -  recursive, such that
   3.823 -\begin{eqnarray*}
   3.824 -  \PREC(f,g)[0,\vec{x}] & = & f[\vec{x}] \\
   3.825 -  \PREC(f,g)[y+1,\vec{x}] & = & g[\PREC(f,g)[y,\vec{x}],\, y,\, \vec{x}].
   3.826 -\end{eqnarray*} 
   3.827 -\end{itemize}
   3.828 -Composition is awkward because it combines not two functions, as is usual,
   3.829 -but $m+1$ functions.  In her proof that Ackermann's function is not
   3.830 -primitive recursive, Nora Szasz was unable to formalize this definition
   3.831 -directly~\cite{szasz93}.  So she generalized primitive recursion to
   3.832 -tuple-valued functions.  This modified the inductive definition such that
   3.833 -each operation on primitive recursive functions combined just two functions.
   3.834 -
   3.835 -\begin{figure}
   3.836 -\begin{ttbox}
   3.837 -Primrec_defs = Main +
   3.838 -consts SC :: i
   3.839 - \(\vdots\)
   3.840 -defs
   3.841 - SC_def    "SC == lam l:list(nat).list_case(0, \%x xs.succ(x), l)"
   3.842 - \(\vdots\)
   3.843 -end
   3.844 -
   3.845 -Primrec = Primrec_defs +
   3.846 -consts prim_rec :: i
   3.847 -inductive
   3.848 - domains "primrec" <= "list(nat)->nat"
   3.849 - intrs
   3.850 -   SC     "SC : primrec"
   3.851 -   CONST  "k: nat ==> CONST(k) : primrec"
   3.852 -   PROJ   "i: nat ==> PROJ(i) : primrec"
   3.853 -   COMP   "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec"
   3.854 -   PREC   "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"
   3.855 - monos       list_mono
   3.856 - con_defs    SC_def, CONST_def, PROJ_def, COMP_def, PREC_def
   3.857 - type_intrs "nat_typechecks @ list.intrs @                      
   3.858 -             [lam_type, list_case_type, drop_type, map_type,    
   3.859 -              apply_type, rec_type]"
   3.860 -end
   3.861 -\end{ttbox}
   3.862 -\hrule
   3.863 -\caption{Inductive definition of the primitive recursive functions} 
   3.864 -\label{primrec-fig}
   3.865 -\end{figure}
   3.866 -\def\fs{{\it fs}} 
   3.867 -
   3.868 -Szasz was using \textsc{alf}, but Coq and \textsc{hol} would also have
   3.869 -problems accepting this definition.  Isabelle's package accepts it easily
   3.870 -since $[f_0,\ldots,f_{m-1}]$ is a list of primitive recursive functions and
   3.871 -$\lst$ is monotonic.  There are five introduction rules, one for each of the
   3.872 -five forms of primitive recursive function.  Let us examine the one for
   3.873 -$\COMP$:
   3.874 -\[ \infer{\COMP(g,\fs)\in\primrec}{g\in\primrec & \fs\in\lst(\primrec)} \]
   3.875 -The induction rule for $\primrec$ has one case for each introduction rule.
   3.876 -Due to the use of $\lst$ as a monotone operator, the composition case has
   3.877 -an unusual induction hypothesis:
   3.878 - \[ \infer*{P(\COMP(g,\fs))}
   3.879 -          {[g\in\primrec & \fs\in\lst(\{z\in\primrec.P(z)\})]_{\fs,g}} 
   3.880 -\]
   3.881 -The hypothesis states that $\fs$ is a list of primitive recursive functions,
   3.882 -each satisfying the induction formula.  Proving the $\COMP$ case typically
   3.883 -requires structural induction on lists, yielding two subcases: either
   3.884 -$\fs=\Nil$ or else $\fs=\Cons(f,\fs')$, where $f\in\primrec$, $P(f)$, and
   3.885 -$\fs'$ is another list of primitive recursive functions satisfying~$P$.
   3.886 -
   3.887 -Figure~\ref{primrec-fig} presents the theory file.  Theory {\tt Primrec}
   3.888 -defines the constants $\SC$, $\CONST$, etc.  These are not constructors of
   3.889 -a new datatype, but functions over lists of numbers.  Their definitions,
   3.890 -most of which are omitted, consist of routine list programming.  In
   3.891 -Isabelle/\textsc{zf}, the primitive recursive functions are defined as a subset of
   3.892 -the function set $\lst(\nat)\to\nat$.
   3.893 -
   3.894 -The Isabelle theory goes on to formalize Ackermann's function and prove
   3.895 -that it is not primitive recursive, using the induction rule {\tt
   3.896 -  primrec.induct}.  The proof follows Szasz's excellent account.
   3.897 -
   3.898 -
   3.899 -\section{Datatypes and codatatypes}\label{data-sec}
   3.900 -A (co)datatype definition is a (co)inductive definition with automatically
   3.901 -defined constructors and a case analysis operator.  The package proves that
   3.902 -the case operator inverts the constructors and can prove freeness theorems
   3.903 -involving any pair of constructors.
   3.904 -
   3.905 -
   3.906 -\subsection{Constructors and their domain}\label{univ-sec}
   3.907 -A (co)inductive definition selects a subset of an existing set; a (co)datatype
   3.908 -definition creates a new set.  The package reduces the latter to the former.
   3.909 -Isabelle/\textsc{zf} supplies sets having strong closure properties to serve
   3.910 -as domains for (co)inductive definitions.
   3.911 -
   3.912 -Isabelle/\textsc{zf} defines the Cartesian product $A\times
   3.913 -B$, containing ordered pairs $\pair{a,b}$; it also defines the
   3.914 -disjoint sum $A+B$, containing injections $\Inl(a)\equiv\pair{0,a}$ and
   3.915 -$\Inr(b)\equiv\pair{1,b}$.  For use below, define the $m$-tuple
   3.916 -$\pair{x_1,\ldots,x_m}$ to be the empty set~$\emptyset$ if $m=0$, simply $x_1$
   3.917 -if $m=1$ and $\pair{x_1,\pair{x_2,\ldots,x_m}}$ if $m\geq2$.
   3.918 -
   3.919 -A datatype constructor $\Con(x_1,\ldots,x_m)$ is defined to be
   3.920 -$h(\pair{x_1,\ldots,x_m})$, where $h$ is composed of $\Inl$ and~$\Inr$.
   3.921 -In a mutually recursive definition, all constructors for the set~$R_i$ have
   3.922 -the outer form~$h_{in}$, where $h_{in}$ is the injection described
   3.923 -in~\S\ref{mutual-sec}.  Further nested injections ensure that the
   3.924 -constructors for~$R_i$ are pairwise distinct.  
   3.925 -
   3.926 -Isabelle/\textsc{zf} defines the set $\univ(A)$, which contains~$A$ and
   3.927 -furthermore contains $\pair{a,b}$, $\Inl(a)$ and $\Inr(b)$ for $a$,
   3.928 -$b\in\univ(A)$.  In a typical datatype definition with set parameters
   3.929 -$A_1$, \ldots, $A_k$, a suitable domain for all the recursive sets is
   3.930 -$\univ(A_1\un\cdots\un A_k)$.  This solves the problem for
   3.931 -datatypes~\cite[\S4.2]{paulson-set-II}.
   3.932 -
   3.933 -The standard pairs and injections can only yield well-founded
   3.934 -constructions.  This eases the (manual!) definition of recursive functions
   3.935 -over datatypes.  But they are unsuitable for codatatypes, which typically
   3.936 -contain non-well-founded objects.
   3.937 -
   3.938 -To support codatatypes, Isabelle/\textsc{zf} defines a variant notion of
   3.939 -ordered pair, written~$\pair{a;b}$.  It also defines the corresponding variant
   3.940 -notion of Cartesian product $A\otimes B$, variant injections $\QInl(a)$
   3.941 -and~$\QInr(b)$ and variant disjoint sum $A\oplus B$.  Finally it defines the
   3.942 -set $\quniv(A)$, which contains~$A$ and furthermore contains $\pair{a;b}$,
   3.943 -$\QInl(a)$ and $\QInr(b)$ for $a$, $b\in\quniv(A)$.  In a typical codatatype
   3.944 -definition with set parameters $A_1$, \ldots, $A_k$, a suitable domain is
   3.945 -$\quniv(A_1\un\cdots\un A_k)$.  Details are published
   3.946 -elsewhere~\cite{paulson-mscs}.
   3.947 -
   3.948 -\subsection{The case analysis operator}
   3.949 -The (co)datatype package automatically defines a case analysis operator,
   3.950 -called {\tt$R$\_case}.  A mutually recursive definition still has only one
   3.951 -operator, whose name combines those of the recursive sets: it is called
   3.952 -{\tt$R_1$\_\ldots\_$R_n$\_case}.  The case operator is analogous to those
   3.953 -for products and sums.
   3.954 -
   3.955 -Datatype definitions employ standard products and sums, whose operators are
   3.956 -$\split$ and $\case$ and satisfy the equations
   3.957 -\begin{eqnarray*}
   3.958 -  \split(f,\pair{x,y})  & = &  f(x,y) \\
   3.959 -  \case(f,g,\Inl(x))    & = &  f(x)   \\
   3.960 -  \case(f,g,\Inr(y))    & = &  g(y)
   3.961 -\end{eqnarray*}
   3.962 -Suppose the datatype has $k$ constructors $\Con_1$, \ldots,~$\Con_k$.  Then
   3.963 -its case operator takes $k+1$ arguments and satisfies an equation for each
   3.964 -constructor:
   3.965 -\[ R\hbox{\_case}(f_1,\ldots,f_k, {\tt Con}_i(\vec{x})) = f_i(\vec{x}),
   3.966 -    \qquad i = 1, \ldots, k
   3.967 -\]
   3.968 -The case operator's definition takes advantage of Isabelle's representation of
   3.969 -syntax in the typed $\lambda$-calculus; it could readily be adapted to a
   3.970 -theorem prover for higher-order logic.  If $f$ and~$g$ have meta-type $i\To i$
   3.971 -then so do $\split(f)$ and $\case(f,g)$.  This works because $\split$ and
   3.972 -$\case$ operate on their last argument.  They are easily combined to make
   3.973 -complex case analysis operators.  For example, $\case(f,\case(g,h))$ performs
   3.974 -case analysis for $A+(B+C)$; let us verify one of the three equations:
   3.975 -\[ \case(f,\case(g,h), \Inr(\Inl(b))) = \case(g,h,\Inl(b)) = g(b) \]
   3.976 -Codatatype definitions are treated in precisely the same way.  They express
   3.977 -case operators using those for the variant products and sums, namely
   3.978 -$\qsplit$ and~$\qcase$.
   3.979 -
   3.980 -\medskip
   3.981 -
   3.982 -To see how constructors and the case analysis operator are defined, let us
   3.983 -examine some examples.  Further details are available
   3.984 -elsewhere~\cite{paulson-set-II}.
   3.985 -
   3.986 -
   3.987 -\subsection{Example: lists and lazy lists}\label{lists-sec}
   3.988 -Here is a declaration of the datatype of lists, as it might appear in a theory
   3.989 -file:
   3.990 -\begin{ttbox} 
   3.991 -consts  list :: i=>i
   3.992 -datatype "list(A)" = Nil | Cons ("a:A", "l: list(A)")
   3.993 -\end{ttbox}
   3.994 -And here is a declaration of the codatatype of lazy lists:
   3.995 -\begin{ttbox}
   3.996 -consts  llist :: i=>i
   3.997 -codatatype "llist(A)" = LNil | LCons ("a: A", "l: llist(A)")
   3.998 -\end{ttbox}
   3.999 -
  3.1000 -Each form of list has two constructors, one for the empty list and one for
  3.1001 -adding an element to a list.  Each takes a parameter, defining the set of
  3.1002 -lists over a given set~$A$.  Each is automatically given the appropriate
  3.1003 -domain: $\univ(A)$ for $\lst(A)$ and $\quniv(A)$ for $\llist(A)$.  The default
  3.1004 -can be overridden.
  3.1005 -
  3.1006 -\ifshort
  3.1007 -Now $\lst(A)$ is a datatype and enjoys the usual induction rule.
  3.1008 -\else
  3.1009 -Since $\lst(A)$ is a datatype, it has a structural induction rule, {\tt
  3.1010 -  list.induct}:
  3.1011 -\[ \infer{P(x)}{x\in\lst(A) & P(\Nil)
  3.1012 -        & \infer*{P(\Cons(a,l))}{[a\in A & l\in\lst(A) & P(l)]_{a,l}} }
  3.1013 -\] 
  3.1014 -Induction and freeness yield the law $l\not=\Cons(a,l)$.  To strengthen this,
  3.1015 -Isabelle/\textsc{zf} defines the rank of a set and proves that the standard
  3.1016 -pairs and injections have greater rank than their components.  An immediate
  3.1017 -consequence, which justifies structural recursion on lists
  3.1018 -\cite[\S4.3]{paulson-set-II}, is
  3.1019 -\[ \rank(l) < \rank(\Cons(a,l)). \]
  3.1020 -\par
  3.1021 -\fi
  3.1022 -But $\llist(A)$ is a codatatype and has no induction rule.  Instead it has
  3.1023 -the coinduction rule shown in \S\ref{coind-sec}.  Since variant pairs and
  3.1024 -injections are monotonic and need not have greater rank than their
  3.1025 -components, fixedpoint operators can create cyclic constructions.  For
  3.1026 -example, the definition
  3.1027 -\[ \lconst(a) \equiv \lfp(\univ(a), \lambda l. \LCons(a,l)) \]
  3.1028 -yields $\lconst(a) = \LCons(a,\lconst(a))$.
  3.1029 -
  3.1030 -\ifshort
  3.1031 -\typeout{****SHORT VERSION}
  3.1032 -\typeout{****Omitting discussion of constructors!}
  3.1033 -\else
  3.1034 -\medskip
  3.1035 -It may be instructive to examine the definitions of the constructors and
  3.1036 -case operator for $\lst(A)$.  The definitions for $\llist(A)$ are similar.
  3.1037 -The list constructors are defined as follows:
  3.1038 -\begin{eqnarray*}
  3.1039 -  \Nil       & \equiv & \Inl(\emptyset) \\
  3.1040 -  \Cons(a,l) & \equiv & \Inr(\pair{a,l})
  3.1041 -\end{eqnarray*}
  3.1042 -The operator $\lstcase$ performs case analysis on these two alternatives:
  3.1043 -\[ \lstcase(c,h) \equiv \case(\lambda u.c, \split(h)) \]
  3.1044 -Let us verify the two equations:
  3.1045 -\begin{eqnarray*}
  3.1046 -    \lstcase(c, h, \Nil) & = & 
  3.1047 -       \case(\lambda u.c, \split(h), \Inl(\emptyset)) \\
  3.1048 -     & = & (\lambda u.c)(\emptyset) \\
  3.1049 -     & = & c\\[1ex]
  3.1050 -    \lstcase(c, h, \Cons(x,y)) & = & 
  3.1051 -       \case(\lambda u.c, \split(h), \Inr(\pair{x,y})) \\
  3.1052 -     & = & \split(h, \pair{x,y}) \\
  3.1053 -     & = & h(x,y)
  3.1054 -\end{eqnarray*} 
  3.1055 -\fi
  3.1056 -
  3.1057 -
  3.1058 -\ifshort
  3.1059 -\typeout{****Omitting mutual recursion example!}
  3.1060 -\else
  3.1061 -\subsection{Example: mutual recursion}
  3.1062 -In mutually recursive trees and forests~\cite[\S4.5]{paulson-set-II}, trees
  3.1063 -have the one constructor $\Tcons$, while forests have the two constructors
  3.1064 -$\Fnil$ and~$\Fcons$:
  3.1065 -\begin{ttbox}
  3.1066 -consts  tree, forest, tree_forest    :: i=>i
  3.1067 -datatype "tree(A)"   = Tcons ("a: A",  "f: forest(A)")
  3.1068 -and      "forest(A)" = Fnil  |  Fcons ("t: tree(A)",  "f: forest(A)")
  3.1069 -\end{ttbox}
  3.1070 -The three introduction rules define the mutual recursion.  The
  3.1071 -distinguishing feature of this example is its two induction rules.
  3.1072 -
  3.1073 -The basic induction rule is called {\tt tree\_forest.induct}:
  3.1074 -\[ \infer{P(x)}{x\in\TF(A) & 
  3.1075 -     \infer*{P(\Tcons(a,f))}
  3.1076 -        {\left[\begin{array}{l} a\in A \\ 
  3.1077 -                                f\in\forest(A) \\ P(f)
  3.1078 -               \end{array}
  3.1079 -         \right]_{a,f}}
  3.1080 -     & P(\Fnil)
  3.1081 -     & \infer*{P(\Fcons(t,f))}
  3.1082 -        {\left[\begin{array}{l} t\in\tree(A)   \\ P(t) \\
  3.1083 -                                f\in\forest(A) \\ P(f)
  3.1084 -                \end{array}
  3.1085 -         \right]_{t,f}} }
  3.1086 -\] 
  3.1087 -This rule establishes a single predicate for $\TF(A)$, the union of the
  3.1088 -recursive sets.  Although such reasoning can be useful
  3.1089 -\cite[\S4.5]{paulson-set-II}, a proper mutual induction rule should establish
  3.1090 -separate predicates for $\tree(A)$ and $\forest(A)$.  The package calls this
  3.1091 -rule {\tt tree\_forest.mutual\_induct}.  Observe the usage of $P$ and $Q$ in
  3.1092 -the induction hypotheses:
  3.1093 -\[ \infer{(\forall z. z\in\tree(A)\imp P(z)) \conj
  3.1094 -          (\forall z. z\in\forest(A)\imp Q(z))}
  3.1095 -     {\infer*{P(\Tcons(a,f))}
  3.1096 -        {\left[\begin{array}{l} a\in A \\ 
  3.1097 -                                f\in\forest(A) \\ Q(f)
  3.1098 -               \end{array}
  3.1099 -         \right]_{a,f}}
  3.1100 -     & Q(\Fnil)
  3.1101 -     & \infer*{Q(\Fcons(t,f))}
  3.1102 -        {\left[\begin{array}{l} t\in\tree(A)   \\ P(t) \\
  3.1103 -                                f\in\forest(A) \\ Q(f)
  3.1104 -                \end{array}
  3.1105 -         \right]_{t,f}} }
  3.1106 -\] 
  3.1107 -Elsewhere I describe how to define mutually recursive functions over trees and
  3.1108 -forests \cite[\S4.5]{paulson-set-II}.
  3.1109 -
  3.1110 -Both forest constructors have the form $\Inr(\cdots)$,
  3.1111 -while the tree constructor has the form $\Inl(\cdots)$.  This pattern would
  3.1112 -hold regardless of how many tree or forest constructors there were.
  3.1113 -\begin{eqnarray*}
  3.1114 -  \Tcons(a,l)  & \equiv & \Inl(\pair{a,l}) \\
  3.1115 -  \Fnil        & \equiv & \Inr(\Inl(\emptyset)) \\
  3.1116 -  \Fcons(a,l)  & \equiv & \Inr(\Inr(\pair{a,l}))
  3.1117 -\end{eqnarray*} 
  3.1118 -There is only one case operator; it works on the union of the trees and
  3.1119 -forests:
  3.1120 -\[ {\tt tree\_forest\_case}(f,c,g) \equiv 
  3.1121 -    \case(\split(f),\, \case(\lambda u.c, \split(g))) 
  3.1122 -\]
  3.1123 -\fi
  3.1124 -
  3.1125 -
  3.1126 -\subsection{Example: a four-constructor datatype}
  3.1127 -A bigger datatype will illustrate some efficiency 
  3.1128 -refinements.  It has four constructors $\Con_0$, \ldots, $\Con_3$, with the
  3.1129 -corresponding arities.
  3.1130 -\begin{ttbox}
  3.1131 -consts    data :: [i,i] => i
  3.1132 -datatype  "data(A,B)" = Con0
  3.1133 -                      | Con1 ("a: A")
  3.1134 -                      | Con2 ("a: A", "b: B")
  3.1135 -                      | Con3 ("a: A", "b: B", "d: data(A,B)")
  3.1136 -\end{ttbox}
  3.1137 -Because this datatype has two set parameters, $A$ and~$B$, the package
  3.1138 -automatically supplies $\univ(A\un B)$ as its domain.  The structural
  3.1139 -induction rule has four minor premises, one per constructor, and only the last
  3.1140 -has an induction hypothesis.  (Details are left to the reader.)
  3.1141 -
  3.1142 -The constructors are defined by the equations
  3.1143 -\begin{eqnarray*}
  3.1144 -  \Con_0         & \equiv & \Inl(\Inl(\emptyset)) \\
  3.1145 -  \Con_1(a)      & \equiv & \Inl(\Inr(a)) \\
  3.1146 -  \Con_2(a,b)    & \equiv & \Inr(\Inl(\pair{a,b})) \\
  3.1147 -  \Con_3(a,b,c)  & \equiv & \Inr(\Inr(\pair{a,b,c})).
  3.1148 -\end{eqnarray*} 
  3.1149 -The case analysis operator is
  3.1150 -\[ {\tt data\_case}(f_0,f_1,f_2,f_3) \equiv 
  3.1151 -    \case(\begin{array}[t]{@{}l}
  3.1152 -          \case(\lambda u.f_0,\; f_1),\, \\
  3.1153 -          \case(\split(f_2),\; \split(\lambda v.\split(f_3(v)))) )
  3.1154 -   \end{array} 
  3.1155 -\]
  3.1156 -This may look cryptic, but the case equations are trivial to verify.
  3.1157 -
  3.1158 -In the constructor definitions, the injections are balanced.  A more naive
  3.1159 -approach is to define $\Con_3(a,b,c)$ as $\Inr(\Inr(\Inr(\pair{a,b,c})))$;
  3.1160 -instead, each constructor has two injections.  The difference here is small.
  3.1161 -But the \textsc{zf} examples include a 60-element enumeration type, where each
  3.1162 -constructor has 5 or~6 injections.  The naive approach would require 1 to~59
  3.1163 -injections; the definitions would be quadratic in size.  It is like the
  3.1164 -advantage of binary notation over unary.
  3.1165 -
  3.1166 -The result structure contains the case operator and constructor definitions as
  3.1167 -the theorem list \verb|con_defs|. It contains the case equations, such as 
  3.1168 -\[ {\tt data\_case}(f_0,f_1,f_2,f_3,\Con_3(a,b,c)) = f_3(a,b,c), \]
  3.1169 -as the theorem list \verb|case_eqns|.  There is one equation per constructor.
  3.1170 -
  3.1171 -\subsection{Proving freeness theorems}
  3.1172 -There are two kinds of freeness theorems:
  3.1173 -\begin{itemize}
  3.1174 -\item \defn{injectiveness} theorems, such as
  3.1175 -\[ \Con_2(a,b) = \Con_2(a',b') \bimp a=a' \conj b=b' \]
  3.1176 -
  3.1177 -\item \defn{distinctness} theorems, such as
  3.1178 -\[ \Con_1(a) \not= \Con_2(a',b')  \]
  3.1179 -\end{itemize}
  3.1180 -Since the number of such theorems is quadratic in the number of constructors,
  3.1181 -the package does not attempt to prove them all.  Instead it returns tools for
  3.1182 -proving desired theorems --- either manually or during
  3.1183 -simplification or classical reasoning.
  3.1184 -
  3.1185 -The theorem list \verb|free_iffs| enables the simplifier to perform freeness
  3.1186 -reasoning.  This works by incremental unfolding of constructors that appear in
  3.1187 -equations.  The theorem list contains logical equivalences such as
  3.1188 -\begin{eqnarray*}
  3.1189 -  \Con_0=c      & \bimp &  c=\Inl(\Inl(\emptyset))     \\
  3.1190 -  \Con_1(a)=c   & \bimp &  c=\Inl(\Inr(a))             \\
  3.1191 -                & \vdots &                             \\
  3.1192 -  \Inl(a)=\Inl(b)   & \bimp &  a=b                     \\
  3.1193 -  \Inl(a)=\Inr(b)   & \bimp &  {\tt False}             \\
  3.1194 -  \pair{a,b} = \pair{a',b'} & \bimp & a=a' \conj b=b'
  3.1195 -\end{eqnarray*}
  3.1196 -For example, these rewrite $\Con_1(a)=\Con_1(b)$ to $a=b$ in four steps.
  3.1197 -
  3.1198 -The theorem list \verb|free_SEs| enables the classical
  3.1199 -reasoner to perform similar replacements.  It consists of elimination rules
  3.1200 -to replace $\Con_0=c$ by $c=\Inl(\Inl(\emptyset))$ and so forth, in the
  3.1201 -assumptions.
  3.1202 -
  3.1203 -Such incremental unfolding combines freeness reasoning with other proof
  3.1204 -steps.  It has the unfortunate side-effect of unfolding definitions of
  3.1205 -constructors in contexts such as $\exists x.\Con_1(a)=x$, where they should
  3.1206 -be left alone.  Calling the Isabelle tactic {\tt fold\_tac con\_defs}
  3.1207 -restores the defined constants.
  3.1208 -
  3.1209 -
  3.1210 -\section{Related work}\label{related}
  3.1211 -The use of least fixedpoints to express inductive definitions seems
  3.1212 -obvious.  Why, then, has this technique so seldom been implemented?
  3.1213 -
  3.1214 -Most automated logics can only express inductive definitions by asserting
  3.1215 -axioms.  Little would be left of Boyer and Moore's logic~\cite{bm79} if their
  3.1216 -shell principle were removed.  With \textsc{alf} the situation is more
  3.1217 -complex; earlier versions of Martin-L\"of's type theory could (using
  3.1218 -wellordering types) express datatype definitions, but the version underlying
  3.1219 -\textsc{alf} requires new rules for each definition~\cite{dybjer91}.  With Coq
  3.1220 -the situation is subtler still; its underlying Calculus of Constructions can
  3.1221 -express inductive definitions~\cite{huet88}, but cannot quite handle datatype
  3.1222 -definitions~\cite{paulin-tlca}.  It seems that researchers tried hard to
  3.1223 -circumvent these problems before finally extending the Calculus with rule
  3.1224 -schemes for strictly positive operators.  Recently Gim{\'e}nez has extended
  3.1225 -the Calculus of Constructions with inductive and coinductive
  3.1226 -types~\cite{gimenez-codifying}, with mechanized support in Coq.
  3.1227 -
  3.1228 -Higher-order logic can express inductive definitions through quantification
  3.1229 -over unary predicates.  The following formula expresses that~$i$ belongs to the
  3.1230 -least set containing~0 and closed under~$\succ$:
  3.1231 -\[ \forall P. P(0)\conj (\forall x.P(x)\imp P(\succ(x))) \imp P(i) \] 
  3.1232 -This technique can be used to prove the Knaster-Tarski theorem, which (in its
  3.1233 -general form) is little used in the Cambridge \textsc{hol} system.
  3.1234 -Melham~\cite{melham89} describes the development.  The natural numbers are
  3.1235 -defined as shown above, but lists are defined as functions over the natural
  3.1236 -numbers.  Unlabelled trees are defined using G\"odel numbering; a labelled
  3.1237 -tree consists of an unlabelled tree paired with a list of labels.  Melham's
  3.1238 -datatype package expresses the user's datatypes in terms of labelled trees.
  3.1239 -It has been highly successful, but a fixedpoint approach might have yielded
  3.1240 -greater power with less effort.
  3.1241 -
  3.1242 -Elsa Gunter~\cite{gunter-trees} reports an ongoing project to generalize the
  3.1243 -Cambridge \textsc{hol} system with mutual recursion and infinitely-branching
  3.1244 -trees.  She retains many features of Melham's approach.
  3.1245 -
  3.1246 -Melham's inductive definition package~\cite{camilleri92} also uses
  3.1247 -quantification over predicates.  But instead of formalizing the notion of
  3.1248 -monotone function, it requires definitions to consist of finitary rules, a
  3.1249 -syntactic form that excludes many monotone inductive definitions.
  3.1250 -
  3.1251 -\textsc{pvs}~\cite{pvs-language} is another proof assistant based on
  3.1252 -higher-order logic.  It supports both inductive definitions and datatypes,
  3.1253 -apparently by asserting axioms.  Datatypes may not be iterated in general, but
  3.1254 -may use recursion over the built-in $\lst$ type.
  3.1255 -
  3.1256 -The earliest use of least fixedpoints is probably Robin Milner's.  Brian
  3.1257 -Monahan extended this package considerably~\cite{monahan84}, as did I in
  3.1258 -unpublished work.\footnote{The datatype package described in my \textsc{lcf}
  3.1259 -  book~\cite{paulson87} does {\it not\/} make definitions, but merely asserts
  3.1260 -  axioms.} \textsc{lcf} is a first-order logic of domain theory; the relevant
  3.1261 -fixedpoint theorem is not Knaster-Tarski but concerns fixedpoints of
  3.1262 -continuous functions over domains.  \textsc{lcf} is too weak to express
  3.1263 -recursive predicates.  The Isabelle package might be the first to be based on
  3.1264 -the Knaster-Tarski theorem.
  3.1265 -
  3.1266 -
  3.1267 -\section{Conclusions and future work}
  3.1268 -Higher-order logic and set theory are both powerful enough to express
  3.1269 -inductive definitions.  A growing number of theorem provers implement one
  3.1270 -of these~\cite{IMPS,saaltink-fme}.  The easiest sort of inductive
  3.1271 -definition package to write is one that asserts new axioms, not one that
  3.1272 -makes definitions and proves theorems about them.  But asserting axioms
  3.1273 -could introduce unsoundness.
  3.1274 -
  3.1275 -The fixedpoint approach makes it fairly easy to implement a package for
  3.1276 -(co)in\-duc\-tive definitions that does not assert axioms.  It is efficient:
  3.1277 -it processes most definitions in seconds and even a 60-constructor datatype
  3.1278 -requires only a few minutes.  It is also simple: The first working version took
  3.1279 -under a week to code, consisting of under 1100 lines (35K bytes) of Standard
  3.1280 -\textsc{ml}.
  3.1281 -
  3.1282 -In set theory, care is needed to ensure that the inductive definition yields
  3.1283 -a set (rather than a proper class).  This problem is inherent to set theory,
  3.1284 -whether or not the Knaster-Tarski theorem is employed.  We must exhibit a
  3.1285 -bounding set (called a domain above).  For inductive definitions, this is
  3.1286 -often trivial.  For datatype definitions, I have had to formalize much set
  3.1287 -theory.  To justify infinitely-branching datatype definitions, I have had to
  3.1288 -develop a theory of cardinal arithmetic~\cite{paulson-gr}, such as the theorem
  3.1289 -that if $\kappa$ is an infinite cardinal and $|X(\alpha)| \le \kappa$ for all
  3.1290 -$\alpha<\kappa$ then $|\union\sb{\alpha<\kappa} X(\alpha)| \le \kappa$.  
  3.1291 -The need for such efforts is not a drawback of the fixedpoint approach, for
  3.1292 -the alternative is to take such definitions on faith.
  3.1293 -
  3.1294 -Care is also needed to ensure that the greatest fixedpoint really yields a
  3.1295 -coinductive definition.  In set theory, standard pairs admit only well-founded
  3.1296 -constructions.  Aczel's anti-foundation axiom~\cite{aczel88} could be used to
  3.1297 -get non-well-founded objects, but it does not seem easy to mechanize.
  3.1298 -Isabelle/\textsc{zf} instead uses a variant notion of ordered pairing, which
  3.1299 -can be generalized to a variant notion of function.  Elsewhere I have
  3.1300 -proved that this simple approach works (yielding final coalgebras) for a broad
  3.1301 -class of definitions~\cite{paulson-mscs}.
  3.1302 -
  3.1303 -Several large studies make heavy use of inductive definitions.  L\"otzbeyer
  3.1304 -and Sandner have formalized two chapters of a semantics book~\cite{winskel93},
  3.1305 -proving the equivalence between the operational and denotational semantics of
  3.1306 -a simple imperative language.  A single theory file contains three datatype
  3.1307 -definitions (of arithmetic expressions, boolean expressions and commands) and
  3.1308 -three inductive definitions (the corresponding operational rules).  Using
  3.1309 -different techniques, Nipkow~\cite{nipkow-CR} and Rasmussen~\cite{rasmussen95}
  3.1310 -have both proved the Church-Rosser theorem; inductive definitions specify
  3.1311 -several reduction relations on $\lambda$-terms.  Recently, I have applied
  3.1312 -inductive definitions to the analysis of cryptographic
  3.1313 -protocols~\cite{paulson-markt}. 
  3.1314 -
  3.1315 -To demonstrate coinductive definitions, Frost~\cite{frost95} has proved the
  3.1316 -consistency of the dynamic and static semantics for a small functional
  3.1317 -language.  The example is due to Milner and Tofte~\cite{milner-coind}.  It
  3.1318 -concerns an extended correspondence relation, which is defined coinductively.
  3.1319 -A codatatype definition specifies values and value environments in mutual
  3.1320 -recursion.  Non-well-founded values represent recursive functions.  Value
  3.1321 -environments are variant functions from variables into values.  This one key
  3.1322 -definition uses most of the package's novel features.
  3.1323 -
  3.1324 -The approach is not restricted to set theory.  It should be suitable for any
  3.1325 -logic that has some notion of set and the Knaster-Tarski theorem.  I have
  3.1326 -ported the (co)inductive definition package from Isabelle/\textsc{zf} to
  3.1327 -Isabelle/\textsc{hol} (higher-order logic).  
  3.1328 -
  3.1329 -
  3.1330 -\begin{footnotesize}
  3.1331 -\bibliographystyle{plain}
  3.1332 -\bibliography{../manual}
  3.1333 -\end{footnotesize}
  3.1334 -%%%%%\doendnotes
  3.1335 -
  3.1336 -\end{document}
     4.1 --- a/doc/Contents	Tue Aug 28 13:09:01 2012 +0200
     4.2 +++ b/doc/Contents	Tue Aug 28 13:12:03 2012 +0200
     4.3 @@ -21,4 +21,4 @@
     4.4    logics          Isabelle's Logics: overview and misc logics
     4.5    logics-HOL      Isabelle's Logics: HOL
     4.6    logics-ZF       Isabelle's Logics: FOL and ZF
     4.7 -  ind-defs        (Co)Inductive Definitions in ZF
     4.8 +