author | wenzelm |

Tue Aug 28 13:12:03 2012 +0200 (2012-08-28) | |

changeset 48964 | 3ec847562782 |

parent 48963 | f11d88bfa934 |

child 48965 | 1fead823c7c6 |

removed historic manual;

doc-src/Inductive/Makefile | file | annotate | diff | revisions | |

doc-src/Inductive/ind-defs-slides.tex | file | annotate | diff | revisions | |

doc-src/Inductive/ind-defs.tex | file | annotate | diff | revisions | |

doc/Contents | file | annotate | diff | revisions |

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 +