summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Mon, 12 May 1997 17:13:58 +0200 | |

changeset 3163 | 4af68e6f4eae |

parent 3162 | 78fa85d44e68 |

child 3164 | ddb0b1fdfdea |

move to Inductive/

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

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

doc-src/ind-defs.bbl | file | annotate | diff | comparison | revisions | |

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

--- a/doc-src/Makefile Mon May 12 17:13:12 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,17 +0,0 @@ -# $Id$ -######################################################################### -# # -# Makefile for the report "A Fixedpoint Approach ..." # -# # -######################################################################### - - -FILES = ind-defs.tex iman.sty extra.sty - -ind-defs.dvi.gz: $(FILES) - -rm ind-defs.dvi.gz - latex209 ind-defs - bibtex ind-defs - latex209 ind-defs - latex209 ind-defs - gzip -f ind-defs.dvi

--- a/doc-src/ind-defs-slides.tex Mon May 12 17:13:12 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,195 +0,0 @@ -%process by latex ind-defs-slides; dvips -Plime ind-defs-slides -% ghostview -magstep -2 -landscape ind-defs-slides.ps -% $Id$ -\documentclass[a4,slidesonly,semlayer]{seminar} - -\usepackage{fancybox} -\usepackage{semhelv} -\usepackage{epsf} -\def\printlandscape{\special{landscape}} % Works with dvips. - -\slidesmag{5}\articlemag{2} %the difference is 3 instead of 4! -\extraslideheight{30pt} - -\renewcommand\slidefuzz{6pt} -\sloppy\hfuzz2pt %sloppy defines \hfuzz0.5pt but it's mainly for text - -\newcommand\sbs{\subseteq} -\newcommand\Pow{{\cal P}} -\newcommand\lfp{\hbox{\tt lfp}} -\newcommand\gfp{\hbox{\tt gfp}} -\newcommand\lst{\hbox{\tt list}} -\newcommand\term{\hbox{\tt term}} - -\newcommand\heading[1]{% - \begin{center}\large\bf\shadowbox{#1}\end{center} - \vspace{1ex minus 1ex}} - -\newpagestyle{mine}% - {L. Paulson\hfil A Fixedpoint Approach to (Co)Inductive Definitions\hfil - \thepage}% - {\hfil\special{psfile=cuarms.eps hscale=20 vscale=20 voffset=-6 - hoffset=-14}\hfil} -\pagestyle{mine} - - -\begin{document} -\slidefonts - -\begin{slide}\centering -\shadowbox{% - \begin{Bcenter} - {\Large\bf A Fixedpoint Approach to}\\[2ex] - {\Large\bf (Co)Inductive Definitions} - \end{Bcenter}} -\bigskip - - \begin{Bcenter} - Lawrence C. Paulson\\ - Computer Laboratory\\ - University of Cambridge\\ - England\\[1ex] - \verb|lcp@cl.cam.ac.uk| - \end{Bcenter} -\bigskip - -{\footnotesize Thanks: SERC grants GR/G53279, GR/H40570; ESPRIT Project 6453 - `Types'} -\end{slide} - - -\begin{slide} -\heading{Inductive Definitions} -\begin{itemize} - \item {\bf datatypes} - \begin{itemize} - \item finite lists, trees - \item syntax of expressions, \ldots - \end{itemize} - \item {\bf inference systems} - \begin{itemize} - \item transitive closure of a relation - \item transition systems - \item structural operational semantics - \end{itemize} -\end{itemize} - -Supported by Boyer/Moore, HOL, Coq, \ldots, Isabelle/ZF -\end{slide} - - -\begin{slide} -\heading{Coinductive Definitions} -\begin{itemize} - \item {\bf codatatypes} - \begin{itemize} - \item {\it infinite\/} lists, trees - \item syntax of {\it infinite\/} expressions, \ldots - \end{itemize} - \item {\bf bisimulation relations} - \begin{itemize} - \item process equivalence - \item uses in functional programming (Abramksy, Howe) - \end{itemize} -\end{itemize} - -Supported by \ldots ?, \ldots, Isabelle/ZF -\end{slide} - - -\begin{slide} -\heading{The Knaster-Tarksi Fixedpoint Theorem} -$h$ a monotone function - -$D$ a set such that $h(D)\sbs D$ - -The {\bf least} fixedpoint $\lfp(D,h)$ yields {\bf inductive} definitions - -The {\bf greatest} fixedpoint $\gfp(D,h)$ yields {\bf coinductive} definitions - -{\it A general approach\/}: -\begin{itemize} - \item handles all provably monotone definitions - \item works for set theory, higher-order logic, \ldots -\end{itemize} -\end{slide} - - -\begin{slide} -\heading{An Implementation in Isabelle/ZF}\centering -\begin{itemize} - \item {\bf Input} - \begin{itemize} - \item description of {\it introduction rules\/} \& tree's {\it - constructors\/} - \item {\it theorems\/} implying that the definition is {\it monotonic\/} - \end{itemize} - \item {\bf Output} - \begin{itemize} - \item (co)induction rules - \item case analysis rule and {\it rule inversion\/} tools, \ldots - \end{itemize} -\end{itemize} - -\vfill -{\it flexible, secure, \ldots but fast\/} -\end{slide} - - -\begin{slide} -\heading{Working Examples} -\begin{itemize} - \item lists - \item terms recursive over lists: $\term(A) = A\times\lst(\term(A))$ - \item primitive recursive functions - \item lazy lists - \item bisimulations for lazy lists - \item combinator reductions; Church-Rosser Theorem - \item mutually recursive trees \& forests -\end{itemize} -\end{slide} - - -\begin{slide} -\heading{Other Work Using Fixedpoints} -{\bf The HOL system}: -\begin{itemize} - \item Melham's induction package: special case of Fixedpoint Theorem - \item Andersen \& Petersen's induction package - \item (no HOL datatype package uses fixedpoints) -\end{itemize} - -{\bf Coq and LEGO}: -\begin{itemize} - \item (Co)induction {\it almost\/} expressible in base logic (CoC) - \item \ldots{} inductive definitions are built-in -\end{itemize} -\end{slide} - - -\begin{slide} -\heading{Limitations \& Future Developments}\centering -\begin{itemize} - \item {\bf infinite-branching trees} - \begin{itemize} - \item justification requires proof - \item would be easier to {\it build them in\/}! - \end{itemize} - \item {\bf recursive function definitions} - \begin{itemize} - \item use {\it well-founded\/} recursion - \item distinct from datatype definitions - \end{itemize} - \item {\bf port to Isabelle/HOL} -\end{itemize} -\end{slide} - -\end{document} - - -{\it flat\/} ordered pairs used to define infinite lists, \ldots - -\begin{slide} -\heading{}\centering -\end{slide} -

--- a/doc-src/ind-defs.bbl Mon May 12 17:13:12 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,214 +0,0 @@ -\begin{thebibliography}{10} - -\bibitem{abramsky90} -Abramsky, S., -\newblock The lazy lambda calculus, -\newblock In {\em Research Topics in Functional Programming}, D.~A. Turner, Ed. - Addison-Wesley, 1977, pp.~65--116 - -\bibitem{aczel77} -Aczel, P., -\newblock An introduction to inductive definitions, -\newblock In {\em Handbook of Mathematical Logic}, J.~Barwise, Ed. - North-Holland, 1977, pp.~739--782 - -\bibitem{aczel88} -Aczel, P., -\newblock {\em Non-Well-Founded Sets}, -\newblock CSLI, 1988 - -\bibitem{bm79} -Boyer, R.~S., Moore, J.~S., -\newblock {\em A Computational Logic}, -\newblock Academic Press, 1979 - -\bibitem{camilleri92} -Camilleri, J., Melham, T.~F., -\newblock Reasoning with inductively defined relations in the {HOL} theorem - prover, -\newblock Tech. Rep. 265, Comp. Lab., Univ. Cambridge, Aug. 1992 - -\bibitem{davey&priestley} -Davey, B.~A., Priestley, H.~A., -\newblock {\em Introduction to Lattices and Order}, -\newblock Cambridge Univ. Press, 1990 - -\bibitem{dybjer91} -Dybjer, P., -\newblock Inductive sets and families in {Martin-L\"of's} type theory and their - set-theoretic semantics, -\newblock In {\em Logical Frameworks}, G.~Huet G.~Plotkin, Eds. Cambridge Univ. - Press, 1991, pp.~280--306 - -\bibitem{types94} -Dybjer, P., Nordstr{\"om}, B., Smith, J., Eds., -\newblock {\em Types for Proofs and Programs: International Workshop {TYPES - '94}}, -\newblock LNCS 996. Springer, published 1995 - -\bibitem{IMPS} -Farmer, W.~M., Guttman, J.~D., Thayer, F.~J., -\newblock {IMPS}: An interactive mathematical proof system, -\newblock {\em J. Auto. Reas. {\bf 11}}, 2 (1993), 213--248 - -\bibitem{frost95} -Frost, J., -\newblock A case study of co-induction in {Isabelle}, -\newblock Tech. Rep. 359, Comp. Lab., Univ. Cambridge, Feb. 1995 - -\bibitem{gimenez-codifying} -Gim{\'e}nez, E., -\newblock Codifying guarded definitions with recursive schemes, -\newblock In Dybjer et~al. \cite{types94}, pp.~39--59 - -\bibitem{gunter-trees} -Gunter, E.~L., -\newblock A broader class of trees for recursive type definitions for {HOL}, -\newblock In {\em Higher Order Logic Theorem Proving and Its Applications: HUG - '93\/} (Published 1994), J.~Joyce C.~Seger, Eds., LNCS 780, Springer, - pp.~141--154 - -\bibitem{hennessy90} -Hennessy, M., -\newblock {\em The Semantics of Programming Languages: An Elementary - Introduction Using Structural Operational Semantics}, -\newblock Wiley, 1990 - -\bibitem{huet88} -Huet, G., -\newblock Induction principles formalized in the {Calculus of Constructions}, -\newblock In {\em Programming of Future Generation Computers\/} (1988), - K.~Fuchi M.~Nivat, Eds., Elsevier, pp.~205--216 - -\bibitem{melham89} -Melham, T.~F., -\newblock Automating recursive type definitions in higher order logic, -\newblock In {\em Current Trends in Hardware Verification and Automated Theorem - Proving}, G.~Birtwistle P.~A. Subrahmanyam, Eds. Springer, 1989, pp.~341--386 - -\bibitem{milner-ind} -Milner, R., -\newblock How to derive inductions in {LCF}, -\newblock note, Dept. Comp. Sci., Univ. Edinburgh, 1980 - -\bibitem{milner89} -Milner, R., -\newblock {\em Communication and Concurrency}, -\newblock Prentice-Hall, 1989 - -\bibitem{milner-coind} -Milner, R., Tofte, M., -\newblock Co-induction in relational semantics, -\newblock {\em Theoretical Comput. Sci. {\bf 87}\/} (1991), 209--220 - -\bibitem{monahan84} -Monahan, B.~Q., -\newblock {\em Data Type Proofs using Edinburgh {LCF}}, -\newblock PhD thesis, University of Edinburgh, 1984 - -\bibitem{nipkow-CR} -Nipkow, T., -\newblock More {Church-Rosser} proofs (in {Isabelle/HOL}), -\newblock In {\em Automated Deduction --- {CADE}-13 International Conference\/} - (1996), M.~McRobbie J.~K. Slaney, Eds., LNAI 1104, Springer, pp.~733--747 - -\bibitem{pvs-language} -Owre, S., Shankar, N., Rushby, J.~M., -\newblock {\em The {PVS} specification language}, -\newblock Computer Science Laboratory, SRI International, Menlo Park, CA, Apr. - 1993, -\newblock Beta release - -\bibitem{paulin-tlca} -Paulin-Mohring, C., -\newblock Inductive definitions in the system {Coq}: Rules and properties, -\newblock In {\em Typed Lambda Calculi and Applications\/} (1993), M.~Bezem - J.~Groote, Eds., LNCS 664, Springer, pp.~328--345 - -\bibitem{paulson-markt} -Paulson, L.~C., -\newblock Tool support for logics of programs, -\newblock In {\em Mathematical Methods in Program Development: Summer School - Marktoberdorf 1996}, M.~Broy, Ed., NATO ASI Series F. Springer, -\newblock In press - -\bibitem{paulson87} -Paulson, L.~C., -\newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}, -\newblock Cambridge Univ. Press, 1987 - -\bibitem{paulson-set-I} -Paulson, L.~C., -\newblock Set theory for verification: {I}. {From} foundations to functions, -\newblock {\em J. Auto. Reas. {\bf 11}}, 3 (1993), 353--389 - -\bibitem{paulson-isa-book} -Paulson, L.~C., -\newblock {\em Isabelle: A Generic Theorem Prover}, -\newblock Springer, 1994, -\newblock LNCS 828 - -\bibitem{paulson-set-II} -Paulson, L.~C., -\newblock Set theory for verification: {II}. {Induction} and recursion, -\newblock {\em J. Auto. Reas. {\bf 15}}, 2 (1995), 167--215 - -\bibitem{paulson-coind} -Paulson, L.~C., -\newblock Mechanizing coinduction and corecursion in higher-order logic, -\newblock {\em J. Logic and Comput. {\bf 7}}, 2 (Mar. 1997), 175--204 - -\bibitem{paulson-final} -Paulson, L.~C., -\newblock A concrete final coalgebra theorem for {ZF} set theory, -\newblock In Dybjer et~al. \cite{types94}, pp.~120--139 - -\bibitem{paulson-gr} -Paulson, L.~C., Gr\c{a}bczewski, K., -\newblock Mechanizing set theory: Cardinal arithmetic and the axiom of choice, -\newblock {\em J. Auto. Reas. {\bf 17}}, 3 (Dec. 1996), 291--323 - -\bibitem{pitts94} -Pitts, A.~M., -\newblock A co-induction principle for recursively defined domains, -\newblock {\em Theoretical Comput. Sci. {\bf 124}\/} (1994), 195--219 - -\bibitem{rasmussen95} -Rasmussen, O., -\newblock The {Church-Rosser} theorem in {Isabelle}: A proof porting - experiment, -\newblock Tech. Rep. 364, Computer Laboratory, University of Cambridge, May - 1995 - -\bibitem{saaltink-fme} -Saaltink, M., Kromodimoeljo, S., Pase, B., Craigen, D., Meisels, I., -\newblock An {EVES} data abstraction example, -\newblock In {\em FME '93: Industrial-Strength Formal Methods\/} (1993), - J.~C.~P. Woodcock P.~G. Larsen, Eds., LNCS 670, Springer, pp.~578--596 - -\bibitem{slind-tfl} -Slind, K., -\newblock Function definition in higher-order logic, -\newblock In {\em Theorem Proving in Higher Order Logics: {TPHOLs} '96\/} - (1996), J.~von Wright, J.~Grundy, J.~Harrison, Eds., LNCS 1125 - -\bibitem{szasz93} -Szasz, N., -\newblock A machine checked proof that {Ackermann's} function is not primitive - recursive, -\newblock In {\em Logical Environments}, G.~Huet G.~Plotkin, Eds. Cambridge - Univ. Press, 1993, pp.~317--338 - -\bibitem{voelker95} -V\"olker, N., -\newblock On the representation of datatypes in {Isabelle/HOL}, -\newblock In {\em Proceedings of the First Isabelle Users Workshop\/} (Sept. - 1995), L.~C. Paulson, Ed., Technical Report 379, Comp. Lab., Univ. Cambridge, - pp.~206--218 - -\bibitem{winskel93} -Winskel, G., -\newblock {\em The Formal Semantics of Programming Languages}, -\newblock MIT Press, 1993 - -\end{thebibliography}

--- a/doc-src/ind-defs.tex Mon May 12 17:13:12 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1592 +0,0 @@ -\documentstyle[a4,alltt,iman,extra,proof209,12pt]{article} -\newif\ifshort%''Short'' means a published version, not the documentation -\shortfalse%%%%%\shorttrue - -\title{A Fixedpoint Approach to\\ - (Co)Inductive and (Co)Datatype Definitions% - \thanks{J. Grundy and S. Thompson made detailed comments. Mads Tofte and - the referees were also helpful. The research was funded by the SERC - grants GR/G53279, GR/H40570 and by the ESPRIT Project 6453 ``Types''.}} - -\author{Lawrence C. Paulson\\{\tt lcp@cl.cam.ac.uk}\\ - Computer Laboratory, University of Cambridge, England} -\date{\today} -\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} - -\newcommand\sbs{\subseteq} -\let\To=\Rightarrow - -\newcommand\emph[1]{{\em#1\/}} -\newcommand\defn[1]{{\bf#1}} -\newcommand\textsc[1]{{\sc#1}} -\newcommand\texttt[1]{{\tt#1}} - -\newcommand\pow{{\cal P}} -%%%\let\pow=\wp -\newcommand\RepFun{\hbox{\tt RepFun}} -\newcommand\cons{\hbox{\tt cons}} -\def\succ{\hbox{\tt succ}} -\newcommand\split{\hbox{\tt split}} -\newcommand\fst{\hbox{\tt fst}} -\newcommand\snd{\hbox{\tt snd}} -\newcommand\converse{\hbox{\tt converse}} -\newcommand\domain{\hbox{\tt domain}} -\newcommand\range{\hbox{\tt range}} -\newcommand\field{\hbox{\tt field}} -\newcommand\lfp{\hbox{\tt lfp}} -\newcommand\gfp{\hbox{\tt gfp}} -\newcommand\id{\hbox{\tt id}} -\newcommand\trans{\hbox{\tt trans}} -\newcommand\wf{\hbox{\tt wf}} -\newcommand\nat{\hbox{\tt nat}} -\newcommand\rank{\hbox{\tt rank}} -\newcommand\univ{\hbox{\tt univ}} -\newcommand\Vrec{\hbox{\tt Vrec}} -\newcommand\Inl{\hbox{\tt Inl}} -\newcommand\Inr{\hbox{\tt Inr}} -\newcommand\case{\hbox{\tt case}} -\newcommand\lst{\hbox{\tt list}} -\newcommand\Nil{\hbox{\tt Nil}} -\newcommand\Cons{\hbox{\tt Cons}} -\newcommand\lstcase{\hbox{\tt list\_case}} -\newcommand\lstrec{\hbox{\tt list\_rec}} -\newcommand\length{\hbox{\tt length}} -\newcommand\listn{\hbox{\tt listn}} -\newcommand\acc{\hbox{\tt acc}} -\newcommand\primrec{\hbox{\tt primrec}} -\newcommand\SC{\hbox{\tt SC}} -\newcommand\CONST{\hbox{\tt CONST}} -\newcommand\PROJ{\hbox{\tt PROJ}} -\newcommand\COMP{\hbox{\tt COMP}} -\newcommand\PREC{\hbox{\tt PREC}} - -\newcommand\quniv{\hbox{\tt quniv}} -\newcommand\llist{\hbox{\tt llist}} -\newcommand\LNil{\hbox{\tt LNil}} -\newcommand\LCons{\hbox{\tt LCons}} -\newcommand\lconst{\hbox{\tt lconst}} -\newcommand\lleq{\hbox{\tt lleq}} -\newcommand\map{\hbox{\tt map}} -\newcommand\term{\hbox{\tt term}} -\newcommand\Apply{\hbox{\tt Apply}} -\newcommand\termcase{\hbox{\tt term\_case}} -\newcommand\rev{\hbox{\tt rev}} -\newcommand\reflect{\hbox{\tt reflect}} -\newcommand\tree{\hbox{\tt tree}} -\newcommand\forest{\hbox{\tt forest}} -\newcommand\Part{\hbox{\tt Part}} -\newcommand\TF{\hbox{\tt tree\_forest}} -\newcommand\Tcons{\hbox{\tt Tcons}} -\newcommand\Fcons{\hbox{\tt Fcons}} -\newcommand\Fnil{\hbox{\tt Fnil}} -\newcommand\TFcase{\hbox{\tt TF\_case}} -\newcommand\Fin{\hbox{\tt Fin}} -\newcommand\QInl{\hbox{\tt QInl}} -\newcommand\QInr{\hbox{\tt QInr}} -\newcommand\qsplit{\hbox{\tt qsplit}} -\newcommand\qcase{\hbox{\tt qcase}} -\newcommand\Con{\hbox{\tt Con}} -\newcommand\data{\hbox{\tt data}} - -\binperiod %%%treat . like a binary operator - -\begin{document} -\pagestyle{empty} -\begin{titlepage} -\maketitle -\begin{abstract} - This paper presents a fixedpoint approach to inductive definitions. - Instead of using a syntactic test such as ``strictly positive,'' the - approach lets definitions involve any operators that have been proved - monotone. It is conceptually simple, which has allowed the easy - implementation of mutual recursion and iterated definitions. It also - handles coinductive definitions: simply replace the least fixedpoint by a - greatest fixedpoint. - - The method has been implemented in two of Isabelle's logics, \textsc{zf} set - theory and higher-order logic. It should be applicable to any logic in - which the Knaster-Tarski theorem can be proved. Examples include lists of - $n$ elements, the accessible part of a relation and the set of primitive - recursive functions. One example of a coinductive definition is - bisimulations for lazy lists. Recursive datatypes are examined in detail, - as well as one example of a \defn{codatatype}: lazy lists. - - The Isabelle package has been applied in several large case studies, - including two proofs of the Church-Rosser theorem and a coinductive proof of - semantic consistency. The package can be trusted because it proves theorems - from definitions, instead of asserting desired properties as axioms. -\end{abstract} -% -\bigskip -\centerline{Copyright \copyright{} \number\year{} by Lawrence C. Paulson} -\thispagestyle{empty} -\end{titlepage} -\tableofcontents\cleardoublepage\pagestyle{plain} - -\setcounter{page}{1} - -\section{Introduction} -Several theorem provers provide commands for formalizing recursive data -structures, like lists and trees. Robin Milner implemented one of the first -of these, for Edinburgh \textsc{lcf}~\cite{milner-ind}. Given a description -of the desired data structure, Milner's package formulated appropriate -definitions and proved the characteristic theorems. Similar is Melham's -recursive type package for the Cambridge \textsc{hol} system~\cite{melham89}. -Such data structures are called \defn{datatypes} -below, by analogy with datatype declarations in Standard~\textsc{ml}\@. -Some logics take datatypes as primitive; consider Boyer and Moore's shell -principle~\cite{bm79} and the Coq type theory~\cite{paulin-tlca}. - -A datatype is but one example of an \defn{inductive definition}. Such a -definition~\cite{aczel77} specifies the least set~$R$ \defn{closed under} -given rules: applying a rule to elements of~$R$ yields a result within~$R$. -Inductive definitions have many applications. The collection of theorems in a -logic is inductively defined. A structural operational -semantics~\cite{hennessy90} is an inductive definition of a reduction or -evaluation relation on programs. A few theorem provers provide commands for -formalizing inductive definitions; these include Coq~\cite{paulin-tlca} and -again the \textsc{hol} system~\cite{camilleri92}. - -The dual notion is that of a \defn{coinductive definition}. Such a definition -specifies the greatest set~$R$ \defn{consistent with} given rules: every -element of~$R$ can be seen as arising by applying a rule to elements of~$R$. -Important examples include using bisimulation relations to formalize -equivalence of processes~\cite{milner89} or lazy functional -programs~\cite{abramsky90}. Other examples include lazy lists and other -infinite data structures; these are called \defn{codatatypes} below. - -Not all inductive definitions are meaningful. \defn{Monotone} inductive -definitions are a large, well-behaved class. Monotonicity can be enforced -by syntactic conditions such as ``strictly positive,'' but this could lead to -monotone definitions being rejected on the grounds of their syntactic form. -More flexible is to formalize monotonicity within the logic and allow users -to prove it. - -This paper describes a package based on a fixedpoint approach. Least -fixedpoints yield inductive definitions; greatest fixedpoints yield -coinductive definitions. Most of the discussion below applies equally to -inductive and coinductive definitions, and most of the code is shared. - -The package supports mutual recursion and infinitely-branching datatypes and -codatatypes. It allows use of any operators that have been proved monotone, -thus accepting all provably monotone inductive definitions, including -iterated definitions. - -The package has been implemented in -Isabelle~\cite{paulson-markt,paulson-isa-book} using -\textsc{zf} set theory \cite{paulson-set-I,paulson-set-II}; part of it has -since been ported to Isabelle/\textsc{hol} (higher-order logic). The -recursion equations are specified as introduction rules for the mutually -recursive sets. The package transforms these rules into a mapping over sets, -and attempts to prove that the mapping is monotonic and well-typed. If -successful, the package makes fixedpoint definitions and proves the -introduction, elimination and (co)induction rules. Users invoke the package -by making simple declarations in Isabelle theory files. - -Most datatype packages equip the new datatype with some means of expressing -recursive functions. This is the main omission from my package. Its -fixedpoint operators define only recursive sets. The Isabelle/\textsc{zf} -theory provides well-founded recursion~\cite{paulson-set-II}, which is harder -to use than structural recursion but considerably more general. -Slind~\cite{slind-tfl} has written a package to automate the definition of -well-founded recursive functions in Isabelle/\textsc{hol}. - -\paragraph*{Outline.} Section~2 introduces the least and greatest fixedpoint -operators. Section~3 discusses the form of introduction rules, mutual -recursion and other points common to inductive and coinductive definitions. -Section~4 discusses induction and coinduction rules separately. Section~5 -presents several examples, including a coinductive definition. Section~6 -describes datatype definitions. Section~7 presents related work. -Section~8 draws brief conclusions. \ifshort\else The appendices are simple -user's manuals for this Isabelle package.\fi - -Most of the definitions and theorems shown below have been generated by the -package. I have renamed some variables to improve readability. - -\section{Fixedpoint operators} -In set theory, the least and greatest fixedpoint operators are defined as -follows: -\begin{eqnarray*} - \lfp(D,h) & \equiv & \inter\{X\sbs D. h(X)\sbs X\} \\ - \gfp(D,h) & \equiv & \union\{X\sbs D. X\sbs h(X)\} -\end{eqnarray*} -Let $D$ be a set. Say that $h$ is \defn{bounded by}~$D$ if $h(D)\sbs D$, and -\defn{monotone below~$D$} if -$h(A)\sbs h(B)$ for all $A$ and $B$ such that $A\sbs B\sbs D$. If $h$ is -bounded by~$D$ and monotone then both operators yield fixedpoints: -\begin{eqnarray*} - \lfp(D,h) & = & h(\lfp(D,h)) \\ - \gfp(D,h) & = & h(\gfp(D,h)) -\end{eqnarray*} -These equations are instances of the Knaster-Tarski theorem, which states -that every monotonic function over a complete lattice has a -fixedpoint~\cite{davey&priestley}. It is obvious from their definitions -that $\lfp$ must be the least fixedpoint, and $\gfp$ the greatest. - -This fixedpoint theory is simple. The Knaster-Tarski theorem is easy to -prove. Showing monotonicity of~$h$ is trivial, in typical cases. We must -also exhibit a bounding set~$D$ for~$h$. Frequently this is trivial, as when -a set of theorems is (co)inductively defined over some previously existing set -of formul{\ae}. Isabelle/\textsc{zf} provides suitable bounding sets for -infinitely-branching (co)datatype definitions; see~\S\ref{univ-sec}. Bounding -sets are also called \defn{domains}. - -The powerset operator is monotone, but by Cantor's theorem there is no -set~$A$ such that $A=\pow(A)$. We cannot put $A=\lfp(D,\pow)$ because -there is no suitable domain~$D$. But \S\ref{acc-sec} demonstrates -that~$\pow$ is still useful in inductive definitions. - -\section{Elements of an inductive or coinductive definition}\label{basic-sec} -Consider a (co)inductive definition of the sets $R_1$, \ldots,~$R_n$, in -mutual recursion. They will be constructed from domains $D_1$, -\ldots,~$D_n$, respectively. The construction yields not $R_i\sbs D_i$ but -$R_i\sbs D_1+\cdots+D_n$, where $R_i$ is contained in the image of~$D_i$ -under an injection. Reasons for this are discussed -elsewhere~\cite[\S4.5]{paulson-set-II}. - -The definition may involve arbitrary parameters $\vec{p}=p_1$, -\ldots,~$p_k$. Each recursive set then has the form $R_i(\vec{p})$. The -parameters must be identical every time they occur within a definition. This -would appear to be a serious restriction compared with other systems such as -Coq~\cite{paulin-tlca}. For instance, we cannot define the lists of -$n$ elements as the set $\listn(A,n)$ using rules where the parameter~$n$ -varies. Section~\ref{listn-sec} describes how to express this set using the -inductive definition package. - -To avoid clutter below, the recursive sets are shown as simply $R_i$ -instead of~$R_i(\vec{p})$. - -\subsection{The form of the introduction rules}\label{intro-sec} -The body of the definition consists of the desired introduction rules. The -conclusion of each rule must have the form $t\in R_i$, where $t$ is any term. -Premises typically have the same form, but they can have the more general form -$t\in M(R_i)$ or express arbitrary side-conditions. - -The premise $t\in M(R_i)$ is permitted if $M$ is a monotonic operator on -sets, satisfying the rule -\[ \infer{M(A)\sbs M(B)}{A\sbs B} \] -The user must supply the package with monotonicity rules for all such premises. - -The ability to introduce new monotone operators makes the approach -flexible. A suitable choice of~$M$ and~$t$ can express a lot. The -powerset operator $\pow$ is monotone, and the premise $t\in\pow(R)$ -expresses $t\sbs R$; see \S\ref{acc-sec} for an example. The \emph{list of} -operator is monotone, as is easily proved by induction. The premise -$t\in\lst(R)$ avoids having to encode the effect of~$\lst(R)$ using mutual -recursion; see \S\ref{primrec-sec} and also my earlier -paper~\cite[\S4.4]{paulson-set-II}. - -Introduction rules may also contain \defn{side-conditions}. These are -premises consisting of arbitrary formul{\ae} not mentioning the recursive -sets. Side-conditions typically involve type-checking. One example is the -premise $a\in A$ in the following rule from the definition of lists: -\[ \infer{\Cons(a,l)\in\lst(A)}{a\in A & l\in\lst(A)} \] - -\subsection{The fixedpoint definitions} -The package translates the list of desired introduction rules into a fixedpoint -definition. Consider, as a running example, the finite powerset operator -$\Fin(A)$: the set of all finite subsets of~$A$. It can be -defined as the least set closed under the rules -\[ \emptyset\in\Fin(A) \qquad - \infer{\{a\}\un b\in\Fin(A)}{a\in A & b\in\Fin(A)} -\] - -The domain in a (co)inductive definition must be some existing set closed -under the rules. A suitable domain for $\Fin(A)$ is $\pow(A)$, the set of all -subsets of~$A$. The package generates the definition -\[ \Fin(A) \equiv \lfp(\pow(A), \, - \begin{array}[t]{r@{\,}l} - \lambda X. \{z\in\pow(A). & z=\emptyset \disj{} \\ - &(\exists a\,b. z=\{a\}\un b\conj a\in A\conj b\in X)\}) - \end{array} -\] -The contribution of each rule to the definition of $\Fin(A)$ should be -obvious. A coinductive definition is similar but uses $\gfp$ instead -of~$\lfp$. - -The package must prove that the fixedpoint operator is applied to a -monotonic function. If the introduction rules have the form described -above, and if the package is supplied a monotonicity theorem for every -$t\in M(R_i)$ premise, then this proof is trivial.\footnote{Due to the - presence of logical connectives in the fixedpoint's body, the - monotonicity proof requires some unusual rules. These state that the - connectives $\conj$, $\disj$ and $\exists$ preserve monotonicity with respect - to the partial ordering on unary predicates given by $P\sqsubseteq Q$ if and - only if $\forall x.P(x)\imp Q(x)$.} - -The package returns its result as an \textsc{ml} structure, which consists of named -components; we may regard it as a record. The result structure contains -the definitions of the recursive sets as a theorem list called {\tt defs}. -It also contains some theorems; {\tt dom\_subset} is an inclusion such as -$\Fin(A)\sbs\pow(A)$, while {\tt bnd\_mono} asserts that the fixedpoint -definition is monotonic. - -Internally the package uses the theorem {\tt unfold}, a fixedpoint equation -such as -\[ - \begin{array}[t]{r@{\,}l} - \Fin(A) = \{z\in\pow(A). & z=\emptyset \disj{} \\ - &(\exists a\,b. z=\{a\}\un b\conj a\in A\conj b\in \Fin(A))\} - \end{array} -\] -In order to save space, this theorem is not exported. - - -\subsection{Mutual recursion} \label{mutual-sec} -In a mutually recursive definition, the domain of the fixedpoint construction -is the disjoint sum of the domain~$D_i$ of each~$R_i$, for $i=1$, -\ldots,~$n$. The package uses the injections of the -binary disjoint sum, typically $\Inl$ and~$\Inr$, to express injections -$h_{1n}$, \ldots, $h_{nn}$ for the $n$-ary disjoint sum $D_1+\cdots+D_n$. - -As discussed elsewhere \cite[\S4.5]{paulson-set-II}, Isabelle/\textsc{zf} defines the -operator $\Part$ to support mutual recursion. The set $\Part(A,h)$ -contains those elements of~$A$ having the form~$h(z)$: -\[ \Part(A,h) \equiv \{x\in A. \exists z. x=h(z)\}. \] -For mutually recursive sets $R_1$, \ldots,~$R_n$ with -$n>1$, the package makes $n+1$ definitions. The first defines a set $R$ using -a fixedpoint operator. The remaining $n$ definitions have the form -\[ R_i \equiv \Part(R,h_{in}), \qquad i=1,\ldots, n. \] -It follows that $R=R_1\un\cdots\un R_n$, where the $R_i$ are pairwise disjoint. - - -\subsection{Proving the introduction rules} -The user supplies the package with the desired form of the introduction -rules. Once it has derived the theorem {\tt unfold}, it attempts -to prove those rules. From the user's point of view, this is the -trickiest stage; the proofs often fail. The task is to show that the domain -$D_1+\cdots+D_n$ of the combined set $R_1\un\cdots\un R_n$ is -closed under all the introduction rules. This essentially involves replacing -each~$R_i$ by $D_1+\cdots+D_n$ in each of the introduction rules and -attempting to prove the result. - -Consider the $\Fin(A)$ example. After substituting $\pow(A)$ for $\Fin(A)$ -in the rules, the package must prove -\[ \emptyset\in\pow(A) \qquad - \infer{\{a\}\un b\in\pow(A)}{a\in A & b\in\pow(A)} -\] -Such proofs can be regarded as type-checking the definition.\footnote{The - Isabelle/\textsc{hol} version does not require these proofs, as \textsc{hol} - has implicit type-checking.} The user supplies the package with -type-checking rules to apply. Usually these are general purpose rules from -the \textsc{zf} theory. They could however be rules specifically proved for a -particular inductive definition; sometimes this is the easiest way to get the -definition through! - -The result structure contains the introduction rules as the theorem list {\tt -intrs}. - -\subsection{The case analysis rule} -The elimination rule, called {\tt elim}, performs case analysis. It is a -simple consequence of {\tt unfold}. There is one case for each introduction -rule. If $x\in\Fin(A)$ then either $x=\emptyset$ or else $x=\{a\}\un b$ for -some $a\in A$ and $b\in\Fin(A)$. Formally, the elimination rule for $\Fin(A)$ -is written -\[ \infer{Q}{x\in\Fin(A) & \infer*{Q}{[x=\emptyset]} - & \infer*{Q}{[x=\{a\}\un b & a\in A &b\in\Fin(A)]_{a,b}} } -\] -The subscripted variables $a$ and~$b$ above the third premise are -eigenvariables, subject to the usual ``not free in \ldots'' proviso. - - -\section{Induction and coinduction rules} -Here we must consider inductive and coinductive definitions separately. For -an inductive definition, the package returns an induction rule derived -directly from the properties of least fixedpoints, as well as a modified rule -for mutual recursion. For a coinductive definition, the package returns a -basic coinduction rule. - -\subsection{The basic induction rule}\label{basic-ind-sec} -The basic rule, called {\tt induct}, is appropriate in most situations. -For inductive definitions, it is strong rule induction~\cite{camilleri92}; for -datatype definitions (see below), it is just structural induction. - -The induction rule for an inductively defined set~$R$ has the form described -below. For the time being, assume that $R$'s domain is not a Cartesian -product; inductively defined relations are treated slightly differently. - -The major premise is $x\in R$. There is a minor premise for each -introduction rule: -\begin{itemize} -\item If the introduction rule concludes $t\in R_i$, then the minor premise -is~$P(t)$. - -\item The minor premise's eigenvariables are precisely the introduction -rule's free variables that are not parameters of~$R$. For instance, the -eigenvariables in the $\Fin(A)$ rule below are $a$ and $b$, but not~$A$. - -\item If the introduction rule has a premise $t\in R_i$, then the minor -premise discharges the assumption $t\in R_i$ and the induction -hypothesis~$P(t)$. If the introduction rule has a premise $t\in M(R_i)$ -then the minor premise discharges the single assumption -\[ t\in M(\{z\in R_i. P(z)\}). \] -Because $M$ is monotonic, this assumption implies $t\in M(R_i)$. The -occurrence of $P$ gives the effect of an induction hypothesis, which may be -exploited by appealing to properties of~$M$. -\end{itemize} -The induction rule for $\Fin(A)$ resembles the elimination rule shown above, -but includes an induction hypothesis: -\[ \infer{P(x)}{x\in\Fin(A) & P(\emptyset) - & \infer*{P(\{a\}\un b)}{[a\in A & b\in\Fin(A) & P(b)]_{a,b}} } -\] -Stronger induction rules often suggest themselves. We can derive a rule for -$\Fin(A)$ whose third premise discharges the extra assumption $a\not\in b$. -The package provides rules for mutual induction and inductive relations. The -Isabelle/\textsc{zf} theory also supports well-founded induction and recursion -over datatypes, by reasoning about the \defn{rank} of a -set~\cite[\S3.4]{paulson-set-II}. - - -\subsection{Modified induction rules} - -If the domain of $R$ is a Cartesian product $A_1\times\cdots\times A_m$ -(however nested), then the corresponding predicate $P_i$ takes $m$ arguments. -The major premise becomes $\pair{z_1,\ldots,z_m}\in R$ instead of $x\in R$; -the conclusion becomes $P(z_1,\ldots,z_m)$. This simplifies reasoning about -inductively defined relations, eliminating the need to express properties of -$z_1$, \ldots,~$z_m$ as properties of the tuple $\pair{z_1,\ldots,z_m}$. -Occasionally it may require you to split up the induction variable -using {\tt SigmaE} and {\tt dom\_subset}, especially if the constant {\tt - split} appears in the rule. - -The mutual induction rule is called {\tt -mutual\_induct}. It differs from the basic rule in two respects: -\begin{itemize} -\item Instead of a single predicate~$P$, it uses $n$ predicates $P_1$, -\ldots,~$P_n$: one for each recursive set. - -\item There is no major premise such as $x\in R_i$. Instead, the conclusion -refers to all the recursive sets: -\[ (\forall z.z\in R_1\imp P_1(z))\conj\cdots\conj - (\forall z.z\in R_n\imp P_n(z)) -\] -Proving the premises establishes $P_i(z)$ for $z\in R_i$ and $i=1$, -\ldots,~$n$. -\end{itemize} -% -If the domain of some $R_i$ is a Cartesian product, then the mutual induction -rule is modified accordingly. The predicates are made to take $m$ separate -arguments instead of a tuple, and the quantification in the conclusion is over -the separate variables $z_1$, \ldots, $z_m$. - -\subsection{Coinduction}\label{coind-sec} -A coinductive definition yields a primitive coinduction rule, with no -refinements such as those for the induction rules. (Experience may suggest -refinements later.) Consider the codatatype of lazy lists as an example. For -suitable definitions of $\LNil$ and $\LCons$, lazy lists may be defined as the -greatest set consistent with the rules -\[ \LNil\in\llist(A) \qquad - \infer[(-)]{\LCons(a,l)\in\llist(A)}{a\in A & l\in\llist(A)} -\] -The $(-)$ tag stresses that this is a coinductive definition. A suitable -domain for $\llist(A)$ is $\quniv(A)$; this set is closed under the variant -forms of sum and product that are used to represent non-well-founded data -structures (see~\S\ref{univ-sec}). - -The package derives an {\tt unfold} theorem similar to that for $\Fin(A)$. -Then it proves the theorem {\tt coinduct}, which expresses that $\llist(A)$ -is the greatest solution to this equation contained in $\quniv(A)$: -\[ \infer{x\in\llist(A)}{x\in X & X\sbs \quniv(A) & - \infer*{ - \begin{array}[b]{r@{}l} - z=\LNil\disj - \bigl(\exists a\,l.\, & z=\LCons(a,l) \conj a\in A \conj{}\\ - & l\in X\un\llist(A) \bigr) - \end{array} }{[z\in X]_z}} -\] -This rule complements the introduction rules; it provides a means of showing -$x\in\llist(A)$ when $x$ is infinite. For instance, if $x=\LCons(0,x)$ then -applying the rule with $X=\{x\}$ proves $x\in\llist(\nat)$. (Here $\nat$ -is the set of natural numbers.) - -Having $X\un\llist(A)$ instead of simply $X$ in the third premise above -represents a slight strengthening of the greatest fixedpoint property. I -discuss several forms of coinduction rules elsewhere~\cite{paulson-coind}. - -The clumsy form of the third premise makes the rule hard to use, especially in -large definitions. Probably a constant should be declared to abbreviate the -large disjunction, and rules derived to allow proving the separate disjuncts. - - -\section{Examples of inductive and coinductive definitions}\label{ind-eg-sec} -This section presents several examples from the literature: the finite -powerset operator, lists of $n$ elements, bisimulations on lazy lists, the -well-founded part of a relation, and the primitive recursive functions. - -\subsection{The finite powerset operator} -This operator has been discussed extensively above. Here is the -corresponding invocation in an Isabelle theory file. Note that -$\cons(a,b)$ abbreviates $\{a\}\un b$ in Isabelle/\textsc{zf}. -\begin{ttbox} -Finite = Arith + -consts Fin :: i=>i -inductive - domains "Fin(A)" <= "Pow(A)" - intrs - emptyI "0 : Fin(A)" - consI "[| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)" - type_intrs "[empty_subsetI, cons_subsetI, PowI]" - type_elims "[make_elim PowD]" -end -\end{ttbox} -Theory {\tt Finite} extends the parent theory {\tt Arith} by declaring the -unary function symbol~$\Fin$, which is defined inductively. Its domain is -specified as $\pow(A)$, where $A$ is the parameter appearing in the -introduction rules. For type-checking, we supply two introduction -rules: -\[ \emptyset\sbs A \qquad - \infer{\{a\}\un B\sbs C}{a\in C & B\sbs C} -\] -A further introduction rule and an elimination rule express both -directions of the equivalence $A\in\pow(B)\bimp A\sbs B$. Type-checking -involves mostly introduction rules. - -Like all Isabelle theory files, this one yields a structure containing the -new theory as an \textsc{ml} value. Structure {\tt Finite} also has a -substructure, called~{\tt Fin}. After declaring \hbox{\tt open Finite;} we -can refer to the $\Fin(A)$ introduction rules as the list {\tt Fin.intrs} -or individually as {\tt Fin.emptyI} and {\tt Fin.consI}. The induction -rule is {\tt Fin.induct}. - - -\subsection{Lists of $n$ elements}\label{listn-sec} -This has become a standard example of an inductive definition. Following -Paulin-Mohring~\cite{paulin-tlca}, we could attempt to define a new datatype -$\listn(A,n)$, for lists of length~$n$, as an $n$-indexed family of sets. -But her introduction rules -\[ \hbox{\tt Niln}\in\listn(A,0) \qquad - \infer{\hbox{\tt Consn}(n,a,l)\in\listn(A,\succ(n))} - {n\in\nat & a\in A & l\in\listn(A,n)} -\] -are not acceptable to the inductive definition package: -$\listn$ occurs with three different parameter lists in the definition. - -The Isabelle version of this example suggests a general treatment of -varying parameters. It uses the existing datatype definition of -$\lst(A)$, with constructors $\Nil$ and~$\Cons$, and incorporates the -parameter~$n$ into the inductive set itself. It defines $\listn(A)$ as a -relation consisting of pairs $\pair{n,l}$ such that $n\in\nat$ -and~$l\in\lst(A)$ and $l$ has length~$n$. In fact, $\listn(A)$ is the -converse of the length function on~$\lst(A)$. The Isabelle/\textsc{zf} introduction -rules are -\[ \pair{0,\Nil}\in\listn(A) \qquad - \infer{\pair{\succ(n),\Cons(a,l)}\in\listn(A)} - {a\in A & \pair{n,l}\in\listn(A)} -\] -The Isabelle theory file takes, as parent, the theory~{\tt List} of lists. -We declare the constant~$\listn$ and supply an inductive definition, -specifying the domain as $\nat\times\lst(A)$: -\begin{ttbox} -ListN = List + -consts listn :: i=>i -inductive - domains "listn(A)" <= "nat*list(A)" - intrs - NilI "<0,Nil>: listn(A)" - ConsI "[| a: A; <n,l>: listn(A) |] ==> <succ(n), Cons(a,l)>: listn(A)" - type_intrs "nat_typechecks @ list.intrs" -end -\end{ttbox} -The type-checking rules include those for 0, $\succ$, $\Nil$ and $\Cons$. -Because $\listn(A)$ is a set of pairs, type-checking requires the -equivalence $\pair{a,b}\in A\times B \bimp a\in A \conj b\in B$. The -package always includes the rules for ordered pairs. - -The package returns introduction, elimination and induction rules for -$\listn$. The basic induction rule, {\tt listn.induct}, is -\[ \infer{P(z_1,z_2)}{\pair{z_1,z_2}\in\listn(A) & P(0,\Nil) & - \infer*{P(\succ(n),\Cons(a,l))} - {[a\in A & \pair{n,l}\in\listn(A) & P(n,l)]_{a,l,n}}} -\] -This rule lets the induction formula to be a -binary property of pairs, $P(n,l)$. -It is now a simple matter to prove theorems about $\listn(A)$, such as -\[ \forall l\in\lst(A). \pair{\length(l),\, l}\in\listn(A) \] -\[ \listn(A)``\{n\} = \{l\in\lst(A). \length(l)=n\} \] -This latter result --- here $r``X$ denotes the image of $X$ under $r$ ---- asserts that the inductive definition agrees with the obvious notion of -$n$-element list. - -A ``list of $n$ elements'' really is a list, namely an element of ~$\lst(A)$. -It is subject to list operators such as append (concatenation). For example, -a trivial induction on $\pair{m,l}\in\listn(A)$ yields -\[ \infer{\pair{m\mathbin{+} m',\, l@l'}\in\listn(A)} - {\pair{m,l}\in\listn(A) & \pair{m',l'}\in\listn(A)} -\] -where $+$ denotes addition on the natural numbers and @ denotes append. - -\subsection{Rule inversion: the function {\tt mk\_cases}} -The elimination rule, {\tt listn.elim}, is cumbersome: -\[ \infer{Q}{x\in\listn(A) & - \infer*{Q}{[x = \pair{0,\Nil}]} & - \infer*{Q} - {\left[\begin{array}{l} - x = \pair{\succ(n),\Cons(a,l)} \\ - a\in A \\ - \pair{n,l}\in\listn(A) - \end{array} \right]_{a,l,n}}} -\] -The \textsc{ml} function {\tt listn.mk\_cases} generates simplified instances of -this rule. It works by freeness reasoning on the list constructors: -$\Cons(a,l)$ is injective in its two arguments and differs from~$\Nil$. If -$x$ is $\pair{i,\Nil}$ or $\pair{i,\Cons(a,l)}$ then {\tt listn.mk\_cases} -deduces the corresponding form of~$i$; this is called rule inversion. -Here is a sample session: -\begin{ttbox} -listn.mk_cases list.con_defs "<i,Nil> : listn(A)"; -{\out "[| <?i, []> : listn(?A); ?i = 0 ==> ?Q |] ==> ?Q" : thm} -listn.mk_cases list.con_defs "<i,Cons(a,l)> : listn(A)"; -{\out "[| <?i, Cons(?a, ?l)> : listn(?A);} -{\out !!n. [| ?a : ?A; <n, ?l> : listn(?A); ?i = succ(n) |] ==> ?Q } -{\out |] ==> ?Q" : thm} -\end{ttbox} -Each of these rules has only two premises. In conventional notation, the -second rule is -\[ \infer{Q}{\pair{i, \Cons(a,l)}\in\listn(A) & - \infer*{Q} - {\left[\begin{array}{l} - a\in A \\ \pair{n,l}\in\listn(A) \\ i = \succ(n) - \end{array} \right]_{n}}} -\] -The package also has built-in rules for freeness reasoning about $0$ -and~$\succ$. So if $x$ is $\pair{0,l}$ or $\pair{\succ(i),l}$, then {\tt -listn.mk\_cases} can deduce the corresponding form of~$l$. - -The function {\tt mk\_cases} is also useful with datatype definitions. The -instance from the definition of lists, namely {\tt list.mk\_cases}, can -prove that $\Cons(a,l)\in\lst(A)$ implies $a\in A $ and $l\in\lst(A)$: -\[ \infer{Q}{\Cons(a,l)\in\lst(A) & - & \infer*{Q}{[a\in A &l\in\lst(A)]} } -\] -A typical use of {\tt mk\_cases} concerns inductive definitions of evaluation -relations. Then rule inversion yields case analysis on possible evaluations. -For example, Isabelle/\textsc{zf} includes a short proof of the -diamond property for parallel contraction on combinators. Ole Rasmussen used -{\tt mk\_cases} extensively in his development of the theory of -residuals~\cite{rasmussen95}. - - -\subsection{A coinductive definition: bisimulations on lazy lists} -This example anticipates the definition of the codatatype $\llist(A)$, which -consists of finite and infinite lists over~$A$. Its constructors are $\LNil$ -and~$\LCons$, satisfying the introduction rules shown in~\S\ref{coind-sec}. -Because $\llist(A)$ is defined as a greatest fixedpoint and uses the variant -pairing and injection operators, it contains non-well-founded elements such as -solutions to $\LCons(a,l)=l$. - -The next step in the development of lazy lists is to define a coinduction -principle for proving equalities. This is done by showing that the equality -relation on lazy lists is the greatest fixedpoint of some monotonic -operation. The usual approach~\cite{pitts94} is to define some notion of -bisimulation for lazy lists, define equivalence to be the greatest -bisimulation, and finally to prove that two lazy lists are equivalent if and -only if they are equal. The coinduction rule for equivalence then yields a -coinduction principle for equalities. - -A binary relation $R$ on lazy lists is a \defn{bisimulation} provided $R\sbs -R^+$, where $R^+$ is the relation -\[ \{\pair{\LNil,\LNil}\} \un - \{\pair{\LCons(a,l),\LCons(a,l')} . a\in A \conj \pair{l,l'}\in R\}. -\] -A pair of lazy lists are \defn{equivalent} if they belong to some -bisimulation. Equivalence can be coinductively defined as the greatest -fixedpoint for the introduction rules -\[ \pair{\LNil,\LNil} \in\lleq(A) \qquad - \infer[(-)]{\pair{\LCons(a,l),\LCons(a,l')} \in\lleq(A)} - {a\in A & \pair{l,l'}\in \lleq(A)} -\] -To make this coinductive definition, the theory file includes (after the -declaration of $\llist(A)$) the following lines: -\begin{ttbox} -consts lleq :: i=>i -coinductive - domains "lleq(A)" <= "llist(A) * llist(A)" - intrs - LNil "<LNil,LNil> : lleq(A)" - LCons "[| a:A; <l,l'>: lleq(A) |] ==> <LCons(a,l),LCons(a,l')>: lleq(A)" - type_intrs "llist.intrs" -\end{ttbox} -The domain of $\lleq(A)$ is $\llist(A)\times\llist(A)$. The type-checking -rules include the introduction rules for $\llist(A)$, whose -declaration is discussed below (\S\ref{lists-sec}). - -The package returns the introduction rules and the elimination rule, as -usual. But instead of induction rules, it returns a coinduction rule. -The rule is too big to display in the usual notation; its conclusion is -$x\in\lleq(A)$ and its premises are $x\in X$, -${X\sbs\llist(A)\times\llist(A)}$ and -\[ \infer*{z=\pair{\LNil,\LNil}\disj \bigl(\exists a\,l\,l'.\, - \begin{array}[t]{@{}l} - z=\pair{\LCons(a,l),\LCons(a,l')} \conj a\in A \conj{}\\ - \pair{l,l'}\in X\un\lleq(A) \bigr) - \end{array} - }{[z\in X]_z} -\] -Thus if $x\in X$, where $X$ is a bisimulation contained in the -domain of $\lleq(A)$, then $x\in\lleq(A)$. It is easy to show that -$\lleq(A)$ is reflexive: the equality relation is a bisimulation. And -$\lleq(A)$ is symmetric: its converse is a bisimulation. But showing that -$\lleq(A)$ coincides with the equality relation takes some work. - -\subsection{The accessible part of a relation}\label{acc-sec} -Let $\prec$ be a binary relation on~$D$; in short, $(\prec)\sbs D\times D$. -The \defn{accessible} or \defn{well-founded} part of~$\prec$, written -$\acc(\prec)$, is essentially that subset of~$D$ for which $\prec$ admits -no infinite decreasing chains~\cite{aczel77}. Formally, $\acc(\prec)$ is -inductively defined to be the least set that contains $a$ if it contains -all $\prec$-predecessors of~$a$, for $a\in D$. Thus we need an -introduction rule of the form -\[ \infer{a\in\acc(\prec)}{\forall y.y\prec a\imp y\in\acc(\prec)} \] -Paulin-Mohring treats this example in Coq~\cite{paulin-tlca}, but it causes -difficulties for other systems. Its premise is not acceptable to the -inductive definition package of the Cambridge \textsc{hol} -system~\cite{camilleri92}. It is also unacceptable to the Isabelle package -(recall \S\ref{intro-sec}), but fortunately can be transformed into the -acceptable form $t\in M(R)$. - -The powerset operator is monotonic, and $t\in\pow(R)$ is equivalent to -$t\sbs R$. This in turn is equivalent to $\forall y\in t. y\in R$. To -express $\forall y.y\prec a\imp y\in\acc(\prec)$ we need only find a -term~$t$ such that $y\in t$ if and only if $y\prec a$. A suitable $t$ is -the inverse image of~$\{a\}$ under~$\prec$. - -The definition below follows this approach. Here $r$ is~$\prec$ and -$\field(r)$ refers to~$D$, the domain of $\acc(r)$. (The field of a -relation is the union of its domain and range.) Finally $r^{-}``\{a\}$ -denotes the inverse image of~$\{a\}$ under~$r$. We supply the theorem {\tt - Pow\_mono}, which asserts that $\pow$ is monotonic. -\begin{ttbox} -consts acc :: i=>i -inductive - domains "acc(r)" <= "field(r)" - intrs - vimage "[| r-``\{a\}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)" - monos "[Pow_mono]" -\end{ttbox} -The Isabelle theory proceeds to prove facts about $\acc(\prec)$. For -instance, $\prec$ is well-founded if and only if its field is contained in -$\acc(\prec)$. - -As mentioned in~\S\ref{basic-ind-sec}, a premise of the form $t\in M(R)$ -gives rise to an unusual induction hypothesis. Let us examine the -induction rule, {\tt acc.induct}: -\[ \infer{P(x)}{x\in\acc(r) & - \infer*{P(a)}{\left[ - \begin{array}{r@{}l} - r^{-}``\{a\} &\, \in\pow(\{z\in\acc(r).P(z)\}) \\ - a &\, \in\field(r) - \end{array} - \right]_a}} -\] -The strange induction hypothesis is equivalent to -$\forall y. \pair{y,a}\in r\imp y\in\acc(r)\conj P(y)$. -Therefore the rule expresses well-founded induction on the accessible part -of~$\prec$. - -The use of inverse image is not essential. The Isabelle package can accept -introduction rules with arbitrary premises of the form $\forall -\vec{y}.P(\vec{y})\imp f(\vec{y})\in R$. The premise can be expressed -equivalently as -\[ \{z\in D. P(\vec{y}) \conj z=f(\vec{y})\} \in \pow(R) \] -provided $f(\vec{y})\in D$ for all $\vec{y}$ such that~$P(\vec{y})$. The -following section demonstrates another use of the premise $t\in M(R)$, -where $M=\lst$. - -\subsection{The primitive recursive functions}\label{primrec-sec} -The primitive recursive functions are traditionally defined inductively, as -a subset of the functions over the natural numbers. One difficulty is that -functions of all arities are taken together, but this is easily -circumvented by regarding them as functions on lists. Another difficulty, -the notion of composition, is less easily circumvented. - -Here is a more precise definition. Letting $\vec{x}$ abbreviate -$x_0,\ldots,x_{n-1}$, we can write lists such as $[\vec{x}]$, -$[y+1,\vec{x}]$, etc. A function is \defn{primitive recursive} if it -belongs to the least set of functions in $\lst(\nat)\to\nat$ containing -\begin{itemize} -\item The \defn{successor} function $\SC$, such that $\SC[y,\vec{x}]=y+1$. -\item All \defn{constant} functions $\CONST(k)$, such that - $\CONST(k)[\vec{x}]=k$. -\item All \defn{projection} functions $\PROJ(i)$, such that - $\PROJ(i)[\vec{x}]=x_i$ if $0\leq i<n$. -\item All \defn{compositions} $\COMP(g,[f_0,\ldots,f_{m-1}])$, -where $g$ and $f_0$, \ldots, $f_{m-1}$ are primitive recursive, -such that -\[ \COMP(g,[f_0,\ldots,f_{m-1}])[\vec{x}] = - g[f_0[\vec{x}],\ldots,f_{m-1}[\vec{x}]]. \] - -\item All \defn{recursions} $\PREC(f,g)$, where $f$ and $g$ are primitive - recursive, such that -\begin{eqnarray*} - \PREC(f,g)[0,\vec{x}] & = & f[\vec{x}] \\ - \PREC(f,g)[y+1,\vec{x}] & = & g[\PREC(f,g)[y,\vec{x}],\, y,\, \vec{x}]. -\end{eqnarray*} -\end{itemize} -Composition is awkward because it combines not two functions, as is usual, -but $m+1$ functions. In her proof that Ackermann's function is not -primitive recursive, Nora Szasz was unable to formalize this definition -directly~\cite{szasz93}. So she generalized primitive recursion to -tuple-valued functions. This modified the inductive definition such that -each operation on primitive recursive functions combined just two functions. - -\begin{figure} -\begin{ttbox} -Primrec = List + -consts - primrec :: i - SC :: i - \(\vdots\) -defs - SC_def "SC == lam l:list(nat).list_case(0, \%x xs.succ(x), l)" - \(\vdots\) -inductive - domains "primrec" <= "list(nat)->nat" - intrs - SC "SC : primrec" - CONST "k: nat ==> CONST(k) : primrec" - PROJ "i: nat ==> PROJ(i) : primrec" - COMP "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec" - PREC "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec" - monos "[list_mono]" - con_defs "[SC_def,CONST_def,PROJ_def,COMP_def,PREC_def]" - type_intrs "nat_typechecks @ list.intrs @ - [lam_type, list_case_type, drop_type, map_type, - apply_type, rec_type]" -end -\end{ttbox} -\hrule -\caption{Inductive definition of the primitive recursive functions} -\label{primrec-fig} -\end{figure} -\def\fs{{\it fs}} - -Szasz was using \textsc{alf}, but Coq and \textsc{hol} would also have -problems accepting this definition. Isabelle's package accepts it easily -since $[f_0,\ldots,f_{m-1}]$ is a list of primitive recursive functions and -$\lst$ is monotonic. There are five introduction rules, one for each of the -five forms of primitive recursive function. Let us examine the one for -$\COMP$: -\[ \infer{\COMP(g,\fs)\in\primrec}{g\in\primrec & \fs\in\lst(\primrec)} \] -The induction rule for $\primrec$ has one case for each introduction rule. -Due to the use of $\lst$ as a monotone operator, the composition case has -an unusual induction hypothesis: - \[ \infer*{P(\COMP(g,\fs))} - {[g\in\primrec & \fs\in\lst(\{z\in\primrec.P(z)\})]_{\fs,g}} -\] -The hypothesis states that $\fs$ is a list of primitive recursive functions, -each satisfying the induction formula. Proving the $\COMP$ case typically -requires structural induction on lists, yielding two subcases: either -$\fs=\Nil$ or else $\fs=\Cons(f,\fs')$, where $f\in\primrec$, $P(f)$, and -$\fs'$ is another list of primitive recursive functions satisfying~$P$. - -Figure~\ref{primrec-fig} presents the theory file. Theory {\tt Primrec} -defines the constants $\SC$, $\CONST$, etc. These are not constructors of -a new datatype, but functions over lists of numbers. Their definitions, -most of which are omitted, consist of routine list programming. In -Isabelle/\textsc{zf}, the primitive recursive functions are defined as a subset of -the function set $\lst(\nat)\to\nat$. - -The Isabelle theory goes on to formalize Ackermann's function and prove -that it is not primitive recursive, using the induction rule {\tt - primrec.induct}. The proof follows Szasz's excellent account. - - -\section{Datatypes and codatatypes}\label{data-sec} -A (co)datatype definition is a (co)inductive definition with automatically -defined constructors and a case analysis operator. The package proves that -the case operator inverts the constructors and can prove freeness theorems -involving any pair of constructors. - - -\subsection{Constructors and their domain}\label{univ-sec} -A (co)inductive definition selects a subset of an existing set; a (co)datatype -definition creates a new set. The package reduces the latter to the former. -Isabelle/\textsc{zf} supplies sets having strong closure properties to serve -as domains for (co)inductive definitions. - -Isabelle/\textsc{zf} defines the Cartesian product $A\times -B$, containing ordered pairs $\pair{a,b}$; it also defines the -disjoint sum $A+B$, containing injections $\Inl(a)\equiv\pair{0,a}$ and -$\Inr(b)\equiv\pair{1,b}$. For use below, define the $m$-tuple -$\pair{x_1,\ldots,x_m}$ to be the empty set~$\emptyset$ if $m=0$, simply $x_1$ -if $m=1$ and $\pair{x_1,\pair{x_2,\ldots,x_m}}$ if $m\geq2$. - -A datatype constructor $\Con(x_1,\ldots,x_m)$ is defined to be -$h(\pair{x_1,\ldots,x_m})$, where $h$ is composed of $\Inl$ and~$\Inr$. -In a mutually recursive definition, all constructors for the set~$R_i$ have -the outer form~$h_{in}$, where $h_{in}$ is the injection described -in~\S\ref{mutual-sec}. Further nested injections ensure that the -constructors for~$R_i$ are pairwise distinct. - -Isabelle/\textsc{zf} defines the set $\univ(A)$, which contains~$A$ and -furthermore contains $\pair{a,b}$, $\Inl(a)$ and $\Inr(b)$ for $a$, -$b\in\univ(A)$. In a typical datatype definition with set parameters -$A_1$, \ldots, $A_k$, a suitable domain for all the recursive sets is -$\univ(A_1\un\cdots\un A_k)$. This solves the problem for -datatypes~\cite[\S4.2]{paulson-set-II}. - -The standard pairs and injections can only yield well-founded -constructions. This eases the (manual!) definition of recursive functions -over datatypes. But they are unsuitable for codatatypes, which typically -contain non-well-founded objects. - -To support codatatypes, Isabelle/\textsc{zf} defines a variant notion of -ordered pair, written~$\pair{a;b}$. It also defines the corresponding variant -notion of Cartesian product $A\otimes B$, variant injections $\QInl(a)$ -and~$\QInr(b)$ and variant disjoint sum $A\oplus B$. Finally it defines the -set $\quniv(A)$, which contains~$A$ and furthermore contains $\pair{a;b}$, -$\QInl(a)$ and $\QInr(b)$ for $a$, $b\in\quniv(A)$. In a typical codatatype -definition with set parameters $A_1$, \ldots, $A_k$, a suitable domain is -$\quniv(A_1\un\cdots\un A_k)$. Details are published -elsewhere~\cite{paulson-final}. - -\subsection{The case analysis operator} -The (co)datatype package automatically defines a case analysis operator, -called {\tt$R$\_case}. A mutually recursive definition still has only one -operator, whose name combines those of the recursive sets: it is called -{\tt$R_1$\_\ldots\_$R_n$\_case}. The case operator is analogous to those -for products and sums. - -Datatype definitions employ standard products and sums, whose operators are -$\split$ and $\case$ and satisfy the equations -\begin{eqnarray*} - \split(f,\pair{x,y}) & = & f(x,y) \\ - \case(f,g,\Inl(x)) & = & f(x) \\ - \case(f,g,\Inr(y)) & = & g(y) -\end{eqnarray*} -Suppose the datatype has $k$ constructors $\Con_1$, \ldots,~$\Con_k$. Then -its case operator takes $k+1$ arguments and satisfies an equation for each -constructor: -\[ R\hbox{\_case}(f_1,\ldots,f_k, {\tt Con}_i(\vec{x})) = f_i(\vec{x}), - \qquad i = 1, \ldots, k -\] -The case operator's definition takes advantage of Isabelle's representation of -syntax in the typed $\lambda$-calculus; it could readily be adapted to a -theorem prover for higher-order logic. If $f$ and~$g$ have meta-type $i\To i$ -then so do $\split(f)$ and $\case(f,g)$. This works because $\split$ and -$\case$ operate on their last argument. They are easily combined to make -complex case analysis operators. For example, $\case(f,\case(g,h))$ performs -case analysis for $A+(B+C)$; let us verify one of the three equations: -\[ \case(f,\case(g,h), \Inr(\Inl(b))) = \case(g,h,\Inl(b)) = g(b) \] -Codatatype definitions are treated in precisely the same way. They express -case operators using those for the variant products and sums, namely -$\qsplit$ and~$\qcase$. - -\medskip - -To see how constructors and the case analysis operator are defined, let us -examine some examples. Further details are available -elsewhere~\cite{paulson-set-II}. - - -\subsection{Example: lists and lazy lists}\label{lists-sec} -Here is a declaration of the datatype of lists, as it might appear in a theory -file: -\begin{ttbox} -consts list :: i=>i -datatype "list(A)" = Nil | Cons ("a:A", "l: list(A)") -\end{ttbox} -And here is a declaration of the codatatype of lazy lists: -\begin{ttbox} -consts llist :: i=>i -codatatype "llist(A)" = LNil | LCons ("a: A", "l: llist(A)") -\end{ttbox} - -Each form of list has two constructors, one for the empty list and one for -adding an element to a list. Each takes a parameter, defining the set of -lists over a given set~$A$. Each is automatically given the appropriate -domain: $\univ(A)$ for $\lst(A)$ and $\quniv(A)$ for $\llist(A)$. The default -can be overridden. - -\ifshort -Now $\lst(A)$ is a datatype and enjoys the usual induction rule. -\else -Since $\lst(A)$ is a datatype, it enjoys a structural induction rule, {\tt - list.induct}: -\[ \infer{P(x)}{x\in\lst(A) & P(\Nil) - & \infer*{P(\Cons(a,l))}{[a\in A & l\in\lst(A) & P(l)]_{a,l}} } -\] -Induction and freeness yield the law $l\not=\Cons(a,l)$. To strengthen this, -Isabelle/\textsc{zf} defines the rank of a set and proves that the standard -pairs and injections have greater rank than their components. An immediate -consequence, which justifies structural recursion on lists -\cite[\S4.3]{paulson-set-II}, is -\[ \rank(l) < \rank(\Cons(a,l)). \] -\par -\fi -But $\llist(A)$ is a codatatype and has no induction rule. Instead it has -the coinduction rule shown in \S\ref{coind-sec}. Since variant pairs and -injections are monotonic and need not have greater rank than their -components, fixedpoint operators can create cyclic constructions. For -example, the definition -\[ \lconst(a) \equiv \lfp(\univ(a), \lambda l. \LCons(a,l)) \] -yields $\lconst(a) = \LCons(a,\lconst(a))$. - -\ifshort -\typeout{****SHORT VERSION} -\typeout{****Omitting discussion of constructors!} -\else -\medskip -It may be instructive to examine the definitions of the constructors and -case operator for $\lst(A)$. The definitions for $\llist(A)$ are similar. -The list constructors are defined as follows: -\begin{eqnarray*} - \Nil & \equiv & \Inl(\emptyset) \\ - \Cons(a,l) & \equiv & \Inr(\pair{a,l}) -\end{eqnarray*} -The operator $\lstcase$ performs case analysis on these two alternatives: -\[ \lstcase(c,h) \equiv \case(\lambda u.c, \split(h)) \] -Let us verify the two equations: -\begin{eqnarray*} - \lstcase(c, h, \Nil) & = & - \case(\lambda u.c, \split(h), \Inl(\emptyset)) \\ - & = & (\lambda u.c)(\emptyset) \\ - & = & c\\[1ex] - \lstcase(c, h, \Cons(x,y)) & = & - \case(\lambda u.c, \split(h), \Inr(\pair{x,y})) \\ - & = & \split(h, \pair{x,y}) \\ - & = & h(x,y) -\end{eqnarray*} -\fi - - -\ifshort -\typeout{****Omitting mutual recursion example!} -\else -\subsection{Example: mutual recursion} -In mutually recursive trees and forests~\cite[\S4.5]{paulson-set-II}, trees -have the one constructor $\Tcons$, while forests have the two constructors -$\Fnil$ and~$\Fcons$: -\begin{ttbox} -consts tree, forest, tree_forest :: i=>i -datatype "tree(A)" = Tcons ("a: A", "f: forest(A)") -and "forest(A)" = Fnil | Fcons ("t: tree(A)", "f: forest(A)") -\end{ttbox} -The three introduction rules define the mutual recursion. The -distinguishing feature of this example is its two induction rules. - -The basic induction rule is called {\tt tree\_forest.induct}: -\[ \infer{P(x)}{x\in\TF(A) & - \infer*{P(\Tcons(a,f))} - {\left[\begin{array}{l} a\in A \\ - f\in\forest(A) \\ P(f) - \end{array} - \right]_{a,f}} - & P(\Fnil) - & \infer*{P(\Fcons(t,f))} - {\left[\begin{array}{l} t\in\tree(A) \\ P(t) \\ - f\in\forest(A) \\ P(f) - \end{array} - \right]_{t,f}} } -\] -This rule establishes a single predicate for $\TF(A)$, the union of the -recursive sets. Although such reasoning is sometimes useful -\cite[\S4.5]{paulson-set-II}, a proper mutual induction rule should establish -separate predicates for $\tree(A)$ and $\forest(A)$. The package calls this -rule {\tt tree\_forest.mutual\_induct}. Observe the usage of $P$ and $Q$ in -the induction hypotheses: -\[ \infer{(\forall z. z\in\tree(A)\imp P(z)) \conj - (\forall z. z\in\forest(A)\imp Q(z))} - {\infer*{P(\Tcons(a,f))} - {\left[\begin{array}{l} a\in A \\ - f\in\forest(A) \\ Q(f) - \end{array} - \right]_{a,f}} - & Q(\Fnil) - & \infer*{Q(\Fcons(t,f))} - {\left[\begin{array}{l} t\in\tree(A) \\ P(t) \\ - f\in\forest(A) \\ Q(f) - \end{array} - \right]_{t,f}} } -\] -Elsewhere I describe how to define mutually recursive functions over trees and -forests \cite[\S4.5]{paulson-set-II}. - -Both forest constructors have the form $\Inr(\cdots)$, -while the tree constructor has the form $\Inl(\cdots)$. This pattern would -hold regardless of how many tree or forest constructors there were. -\begin{eqnarray*} - \Tcons(a,l) & \equiv & \Inl(\pair{a,l}) \\ - \Fnil & \equiv & \Inr(\Inl(\emptyset)) \\ - \Fcons(a,l) & \equiv & \Inr(\Inr(\pair{a,l})) -\end{eqnarray*} -There is only one case operator; it works on the union of the trees and -forests: -\[ {\tt tree\_forest\_case}(f,c,g) \equiv - \case(\split(f),\, \case(\lambda u.c, \split(g))) -\] -\fi - - -\subsection{Example: a four-constructor datatype} -A bigger datatype will illustrate some efficiency -refinements. It has four constructors $\Con_0$, \ldots, $\Con_3$, with the -corresponding arities. -\begin{ttbox} -consts data :: [i,i] => i -datatype "data(A,B)" = Con0 - | Con1 ("a: A") - | Con2 ("a: A", "b: B") - | Con3 ("a: A", "b: B", "d: data(A,B)") -\end{ttbox} -Because this datatype has two set parameters, $A$ and~$B$, the package -automatically supplies $\univ(A\un B)$ as its domain. The structural -induction rule has four minor premises, one per constructor, and only the last -has an induction hypothesis. (Details are left to the reader.) - -The constructors are defined by the equations -\begin{eqnarray*} - \Con_0 & \equiv & \Inl(\Inl(\emptyset)) \\ - \Con_1(a) & \equiv & \Inl(\Inr(a)) \\ - \Con_2(a,b) & \equiv & \Inr(\Inl(\pair{a,b})) \\ - \Con_3(a,b,c) & \equiv & \Inr(\Inr(\pair{a,b,c})). -\end{eqnarray*} -The case analysis operator is -\[ {\tt data\_case}(f_0,f_1,f_2,f_3) \equiv - \case(\begin{array}[t]{@{}l} - \case(\lambda u.f_0,\; f_1),\, \\ - \case(\split(f_2),\; \split(\lambda v.\split(f_3(v)))) ) - \end{array} -\] -This may look cryptic, but the case equations are trivial to verify. - -In the constructor definitions, the injections are balanced. A more naive -approach is to define $\Con_3(a,b,c)$ as $\Inr(\Inr(\Inr(\pair{a,b,c})))$; -instead, each constructor has two injections. The difference here is small. -But the \textsc{zf} examples include a 60-element enumeration type, where each -constructor has 5 or~6 injections. The naive approach would require 1 to~59 -injections; the definitions would be quadratic in size. It is like the -advantage of binary notation over unary. - -The result structure contains the case operator and constructor definitions as -the theorem list \verb|con_defs|. It contains the case equations, such as -\[ {\tt data\_case}(f_0,f_1,f_2,f_3,\Con_3(a,b,c)) = f_3(a,b,c), \] -as the theorem list \verb|case_eqns|. There is one equation per constructor. - -\subsection{Proving freeness theorems} -There are two kinds of freeness theorems: -\begin{itemize} -\item \defn{injectiveness} theorems, such as -\[ \Con_2(a,b) = \Con_2(a',b') \bimp a=a' \conj b=b' \] - -\item \defn{distinctness} theorems, such as -\[ \Con_1(a) \not= \Con_2(a',b') \] -\end{itemize} -Since the number of such theorems is quadratic in the number of constructors, -the package does not attempt to prove them all. Instead it returns tools for -proving desired theorems --- either manually or during -simplification or classical reasoning. - -The theorem list \verb|free_iffs| enables the simplifier to perform freeness -reasoning. This works by incremental unfolding of constructors that appear in -equations. The theorem list contains logical equivalences such as -\begin{eqnarray*} - \Con_0=c & \bimp & c=\Inl(\Inl(\emptyset)) \\ - \Con_1(a)=c & \bimp & c=\Inl(\Inr(a)) \\ - & \vdots & \\ - \Inl(a)=\Inl(b) & \bimp & a=b \\ - \Inl(a)=\Inr(b) & \bimp & {\tt False} \\ - \pair{a,b} = \pair{a',b'} & \bimp & a=a' \conj b=b' -\end{eqnarray*} -For example, these rewrite $\Con_1(a)=\Con_1(b)$ to $a=b$ in four steps. - -The theorem list \verb|free_SEs| enables the classical -reasoner to perform similar replacements. It consists of elimination rules -to replace $\Con_0=c$ by $c=\Inl(\Inl(\emptyset))$ and so forth, in the -assumptions. - -Such incremental unfolding combines freeness reasoning with other proof -steps. It has the unfortunate side-effect of unfolding definitions of -constructors in contexts such as $\exists x.\Con_1(a)=x$, where they should -be left alone. Calling the Isabelle tactic {\tt fold\_tac con\_defs} -restores the defined constants. - - -\section{Related work}\label{related} -The use of least fixedpoints to express inductive definitions seems -obvious. Why, then, has this technique so seldom been implemented? - -Most automated logics can only express inductive definitions by asserting -axioms. Little would be left of Boyer and Moore's logic~\cite{bm79} if their -shell principle were removed. With \textsc{alf} the situation is more -complex; earlier versions of Martin-L\"of's type theory could (using -wellordering types) express datatype definitions, but the version underlying -\textsc{alf} requires new rules for each definition~\cite{dybjer91}. With Coq -the situation is subtler still; its underlying Calculus of Constructions can -express inductive definitions~\cite{huet88}, but cannot quite handle datatype -definitions~\cite{paulin-tlca}. It seems that researchers tried hard to -circumvent these problems before finally extending the Calculus with rule -schemes for strictly positive operators. Recently Gim{\'e}nez has extended -the Calculus of Constructions with inductive and coinductive -types~\cite{gimenez-codifying}, with mechanized support in Coq. - -Higher-order logic can express inductive definitions through quantification -over unary predicates. The following formula expresses that~$i$ belongs to the -least set containing~0 and closed under~$\succ$: -\[ \forall P. P(0)\conj (\forall x.P(x)\imp P(\succ(x))) \imp P(i) \] -This technique can be used to prove the Knaster-Tarski theorem, which (in its -general form) is little used in the Cambridge \textsc{hol} system. -Melham~\cite{melham89} describes the development. The natural numbers are -defined as shown above, but lists are defined as functions over the natural -numbers. Unlabelled trees are defined using G\"odel numbering; a labelled -tree consists of an unlabelled tree paired with a list of labels. Melham's -datatype package expresses the user's datatypes in terms of labelled trees. -It has been highly successful, but a fixedpoint approach might have yielded -greater power with less effort. - -Elsa Gunter~\cite{gunter-trees} reports an ongoing project to generalize the -Cambridge \textsc{hol} system with mutual recursion and infinitely-branching -trees. She retains many features of Melham's approach. - -Melham's inductive definition package~\cite{camilleri92} also uses -quantification over predicates. But instead of formalizing the notion of -monotone function, it requires definitions to consist of finitary rules, a -syntactic form that excludes many monotone inductive definitions. - -\textsc{pvs}~\cite{pvs-language} is another proof assistant based on -higher-order logic. It supports both inductive definitions and datatypes, -apparently by asserting axioms. Datatypes may not be iterated in general, but -may use recursion over the built-in $\lst$ type. - -The earliest use of least fixedpoints is probably Robin Milner's. Brian -Monahan extended this package considerably~\cite{monahan84}, as did I in -unpublished work.\footnote{The datatype package described in my \textsc{lcf} - book~\cite{paulson87} does {\it not\/} make definitions, but merely asserts - axioms.} \textsc{lcf} is a first-order logic of domain theory; the relevant -fixedpoint theorem is not Knaster-Tarski but concerns fixedpoints of -continuous functions over domains. \textsc{lcf} is too weak to express -recursive predicates. The Isabelle package might be the first to be based on -the Knaster-Tarski theorem. - - -\section{Conclusions and future work} -Higher-order logic and set theory are both powerful enough to express -inductive definitions. A growing number of theorem provers implement one -of these~\cite{IMPS,saaltink-fme}. The easiest sort of inductive -definition package to write is one that asserts new axioms, not one that -makes definitions and proves theorems about them. But asserting axioms -could introduce unsoundness. - -The fixedpoint approach makes it fairly easy to implement a package for -(co)in\-duc\-tive definitions that does not assert axioms. It is efficient: -it processes most definitions in seconds and even a 60-constructor datatype -requires only a few minutes. It is also simple: The first working version took -under a week to code, consisting of under 1100 lines (35K bytes) of Standard -\textsc{ml}. - -In set theory, care is needed to ensure that the inductive definition yields -a set (rather than a proper class). This problem is inherent to set theory, -whether or not the Knaster-Tarski theorem is employed. We must exhibit a -bounding set (called a domain above). For inductive definitions, this is -often trivial. For datatype definitions, I have had to formalize much set -theory. To justify infinitely-branching datatype definitions, I have had to -develop a theory of cardinal arithmetic~\cite{paulson-gr}, such as the theorem -that if $\kappa$ is an infinite cardinal and $|X(\alpha)| \le \kappa$ for all -$\alpha<\kappa$ then $|\union\sb{\alpha<\kappa} X(\alpha)| \le \kappa$. -The need for such efforts is not a drawback of the fixedpoint approach, for -the alternative is to take such definitions on faith. - -Care is also needed to ensure that the greatest fixedpoint really yields a -coinductive definition. In set theory, standard pairs admit only well-founded -constructions. Aczel's anti-foundation axiom~\cite{aczel88} could be used to -get non-well-founded objects, but it does not seem easy to mechanize. -Isabelle/\textsc{zf} instead uses a variant notion of ordered pairing, which -can be generalized to a variant notion of function. Elsewhere I have -proved that this simple approach works (yielding final coalgebras) for a broad -class of definitions~\cite{paulson-final}. - -Several large studies make heavy use of inductive definitions. L\"otzbeyer -and Sandner have formalized two chapters of a semantics book~\cite{winskel93}, -proving the equivalence between the operational and denotational semantics of -a simple imperative language. A single theory file contains three datatype -definitions (of arithmetic expressions, boolean expressions and commands) and -three inductive definitions (the corresponding operational rules). Using -different techniques, Nipkow~\cite{nipkow-CR} and Rasmussen~\cite{rasmussen95} -have both proved the Church-Rosser theorem; inductive definitions specify -several reduction relations on $\lambda$-terms. Recently, I have applied -inductive definitions to the analysis of cryptographic -protocols~\cite{paulson-markt}. - -To demonstrate coinductive definitions, Frost~\cite{frost95} has proved the -consistency of the dynamic and static semantics for a small functional -language. The example is due to Milner and Tofte~\cite{milner-coind}. It -concerns an extended correspondence relation, which is defined coinductively. -A codatatype definition specifies values and value environments in mutual -recursion. Non-well-founded values represent recursive functions. Value -environments are variant functions from variables into values. This one key -definition uses most of the package's novel features. - -The approach is not restricted to set theory. It should be suitable for any -logic that has some notion of set and the Knaster-Tarski theorem. I have -ported the (co)inductive definition package from Isabelle/\textsc{zf} to -Isabelle/\textsc{hol} (higher-order logic). V\"olker~\cite{voelker95} -is investigating how to port the (co)datatype package. \textsc{hol} -represents sets by unary predicates; defining the corresponding types may -cause complications. - - -\begin{footnotesize} -\bibliographystyle{springer} -\bibliography{string-abbrv,atp,theory,funprog,isabelle,crossref} -\end{footnotesize} -%%%%%\doendnotes - -\ifshort\typeout{****Omitting appendices} -\else -\newpage -\appendix -\section{Inductive and coinductive definitions: users guide} -A theory file may contain any number of inductive and coinductive -definitions. They may be intermixed with other declarations; in -particular, the (co)inductive sets \defn{must} be declared separately as -constants, and may have mixfix syntax or be subject to syntax translations. - -The syntax is rather complicated. Please consult the examples above and the -theory files on the \textsc{zf} source directory. - -Each (co)inductive definition adds definitions to the theory and also proves -some theorems. Each definition creates an \textsc{ml} structure, which is a -substructure of the main theory structure. - -Inductive and datatype definitions can take up considerable storage. The -introduction rules are replicated in slightly different forms as fixedpoint -definitions, elimination rules and induction rules. L\"otzbeyer and Sandner's -six definitions occupy over 600K in total. Defining the 60-constructor -datatype requires nearly 560K\@. - -\subsection{The result structure} -Many of the result structure's components have been discussed -in~\S\ref{basic-sec}; others are self-explanatory. -\begin{description} -\item[\tt thy] is the new theory containing the recursive sets. - -\item[\tt defs] is the list of definitions of the recursive sets. - -\item[\tt bnd\_mono] is a monotonicity theorem for the fixedpoint operator. - -\item[\tt dom\_subset] is a theorem stating inclusion in the domain. - -\item[\tt intrs] is the list of introduction rules, now proved as theorems, for -the recursive sets. The rules are also available individually, using the -names given them in the theory file. - -\item[\tt elim] is the elimination rule. - -\item[\tt mk\_cases] is a function to create simplified instances of {\tt -elim}, using freeness reasoning on some underlying datatype. -\end{description} - -For an inductive definition, the result structure contains two induction -rules, {\tt induct} and \verb|mutual_induct|. (To save storage, the latter -rule is just {\tt True} unless more than one set is being defined.) For a -coinductive definition, it contains the rule \verb|coinduct|. - -Figure~\ref{def-result-fig} summarizes the two result signatures, -specifying the types of all these components. - -\begin{figure} -\begin{ttbox} -sig -val thy : theory -val defs : thm list -val bnd_mono : thm -val dom_subset : thm -val intrs : thm list -val elim : thm -val mk_cases : thm list -> string -> thm -{\it(Inductive definitions only)} -val induct : thm -val mutual_induct: thm -{\it(Coinductive definitions only)} -val coinduct : thm -end -\end{ttbox} -\hrule -\caption{The result of a (co)inductive definition} \label{def-result-fig} -\end{figure} - -\subsection{The syntax of a (co)inductive definition} -An inductive definition has the form -\begin{ttbox} -inductive - domains {\it domain declarations} - intrs {\it introduction rules} - monos {\it monotonicity theorems} - con_defs {\it constructor definitions} - type_intrs {\it introduction rules for type-checking} - type_elims {\it elimination rules for type-checking} -\end{ttbox} -A coinductive definition is identical, but starts with the keyword -{\tt coinductive}. - -The {\tt monos}, {\tt con\_defs}, {\tt type\_intrs} and {\tt type\_elims} -sections are optional. If present, each is specified as a string, which -must be a valid \textsc{ml} expression of type {\tt thm list}. It is simply -inserted into the {\tt .thy.ML} file; if it is ill-formed, it will trigger -\textsc{ml} error messages. You can then inspect the file on your directory. - -\begin{description} -\item[\it domain declarations] consist of one or more items of the form - {\it string\/}~{\tt <=}~{\it string}, associating each recursive set with - its domain. - -\item[\it introduction rules] specify one or more introduction rules in - the form {\it ident\/}~{\it string}, where the identifier gives the name of - the rule in the result structure. - -\item[\it monotonicity theorems] are required for each operator applied to - a recursive set in the introduction rules. There \defn{must} be a theorem - of the form $A\sbs B\Imp M(A)\sbs M(B)$, for each premise $t\in M(R_i)$ - in an introduction rule! - -\item[\it constructor definitions] contain definitions of constants - appearing in the introduction rules. The (co)datatype package supplies - the constructors' definitions here. Most (co)inductive definitions omit - this section; one exception is the primitive recursive functions example - (\S\ref{primrec-sec}). - -\item[\it type\_intrs] consists of introduction rules for type-checking the - definition, as discussed in~\S\ref{basic-sec}. They are applied using - depth-first search; you can trace the proof by setting - - \verb|trace_DEPTH_FIRST := true|. - -\item[\it type\_elims] consists of elimination rules for type-checking the - definition. They are presumed to be safe and are applied as much as - possible, prior to the {\tt type\_intrs} search. -\end{description} - -The package has a few notable restrictions: -\begin{itemize} -\item The theory must separately declare the recursive sets as - constants. - -\item The names of the recursive sets must be identifiers, not infix -operators. - -\item Side-conditions must not be conjunctions. However, an introduction rule -may contain any number of side-conditions. - -\item Side-conditions of the form $x=t$, where the variable~$x$ does not - occur in~$t$, will be substituted through the rule \verb|mutual_induct|. -\end{itemize} - -Isabelle/\textsc{hol} uses a simplified syntax for inductive definitions, -thanks to type-checking. There are no \texttt{domains}, \texttt{type\_intrs} -or \texttt{type\_elims} parts. - - -\section{Datatype and codatatype definitions: users guide} -This section explains how to include (co)datatype declarations in a theory -file. Please include {\tt Datatype} as a parent theory; this makes available -the definitions of $\univ$ and $\quniv$. - - -\subsection{The result structure} -The result structure extends that of (co)inductive definitions -(Figure~\ref{def-result-fig}) with several additional items: -\begin{ttbox} -val con_defs : thm list -val case_eqns : thm list -val free_iffs : thm list -val free_SEs : thm list -val mk_free : string -> thm -\end{ttbox} -Most of these have been discussed in~\S\ref{data-sec}. Here is a summary: -\begin{description} -\item[\tt con\_defs] is a list of definitions: the case operator followed by -the constructors. This theorem list can be supplied to \verb|mk_cases|, for -example. - -\item[\tt case\_eqns] is a list of equations, stating that the case operator -inverts each constructor. - -\item[\tt free\_iffs] is a list of logical equivalences to perform freeness -reasoning by rewriting. A typical application has the form -\begin{ttbox} -by (asm_simp_tac (ZF_ss addsimps free_iffs) 1); -\end{ttbox} - -\item[\tt free\_SEs] is a list of safe elimination rules to perform freeness -reasoning. It can be supplied to \verb|eresolve_tac| or to the classical -reasoner: -\begin{ttbox} -by (fast_tac (ZF_cs addSEs free_SEs) 1); -\end{ttbox} - -\item[\tt mk\_free] is a function to prove freeness properties, specified as -strings. The theorems can be expressed in various forms, such as logical -equivalences or elimination rules. -\end{description} - -The result structure also inherits everything from the underlying -(co)inductive definition, such as the introduction rules, elimination rule, -and (co)induction rule. - - -\subsection{The syntax of a (co)datatype definition} -A datatype definition has the form -\begin{ttbox} -datatype <={\it domain} - {\it datatype declaration} and {\it datatype declaration} and \ldots - monos {\it monotonicity theorems} - type_intrs {\it introduction rules for type-checking} - type_elims {\it elimination rules for type-checking} -\end{ttbox} -A codatatype definition is identical save that it starts with the keyword {\tt - codatatype}. - -The {\tt monos}, {\tt type\_intrs} and {\tt type\_elims} sections are -optional. They are treated like their counterparts in a (co)inductive -definition, as described above. The package supplements your type-checking -rules (if any) with additional ones that should cope with any -finitely-branching (co)datatype definition. - -\begin{description} -\item[\it domain] specifies a single domain to use for all the mutually - recursive (co)datatypes. If it (and the preceeding~{\tt <=}) are - omitted, the package supplies a domain automatically. Suppose the - definition involves the set parameters $A_1$, \ldots, $A_k$. Then - $\univ(A_1\un\cdots\un A_k)$ is used for a datatype definition and - $\quniv(A_1\un\cdots\un A_k)$ is used for a codatatype definition. - - These choices should work for all finitely-branching (co)datatype - definitions. For examples of infinitely-branching datatypes, - see file {\tt ZF/ex/Brouwer.thy}. - -\item[\it datatype declaration] has the form -\begin{quote} - {\it string\/} {\tt =} {\it constructor} {\tt|} {\it constructor} {\tt|} - \ldots -\end{quote} -The {\it string\/} is the datatype, say {\tt"list(A)"}. Each -{\it constructor\/} has the form -\begin{quote} - {\it name\/} {\tt(} {\it premise} {\tt,} {\it premise} {\tt,} \ldots {\tt)} - {\it mixfix\/} -\end{quote} -The {\it name\/} specifies a new constructor while the {\it premises\/} its -typing conditions. The optional {\it mixfix\/} phrase may give -the constructor infix, for example. - -Mutually recursive {\it datatype declarations\/} are separated by the -keyword~{\tt and}. -\end{description} - -Isabelle/\textsc{hol}'s datatype definition package is (as of this writing) -entirely different from Isabelle/\textsc{zf}'s. The syntax is different, and -instead of making an inductive definition it asserts axioms. - -\paragraph*{Note.} -In the definitions of the constructors, the right-hand sides may overlap. -For instance, the datatype of combinators has constructors defined by -\begin{eqnarray*} - {\tt K} & \equiv & \Inl(\emptyset) \\ - {\tt S} & \equiv & \Inr(\Inl(\emptyset)) \\ - p{\tt\#}q & \equiv & \Inr(\Inl(\pair{p,q})) -\end{eqnarray*} -Unlike in previous versions of Isabelle, \verb|fold_tac| now ensures that the -longest right-hand sides are folded first. - -\fi -\end{document}