doc-src/Inductive/ind-defs.tex
author wenzelm
Fri, 28 May 1999 11:42:07 +0200
changeset 6745 74e8f703f5f2
parent 6637 57abed64dc14
child 7829 c2672c537894
permissions -rw-r--r--
tuned manual.bib;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4265
70fc6e05120c Deleted some useless comments
paulson
parents: 4239
diff changeset
     1
%% $Id$
3162
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
     2
\documentclass[12pt]{article}
6637
57abed64dc14 pdf setup;
wenzelm
parents: 6631
diff changeset
     3
\usepackage{a4,latexsym,../iman,../extra,../proof,../pdfsetup}
3162
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
     4
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
     5
\newif\ifshort%''Short'' means a published version, not the documentation
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
     6
\shortfalse%%%%%\shorttrue
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
     7
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
     8
\title{A Fixedpoint Approach to\\ 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
     9
  (Co)Inductive and (Co)Datatype Definitions%
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    10
  \thanks{J. Grundy and S. Thompson made detailed comments.  Mads Tofte and
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    11
    the referees were also helpful.  The research was funded by the SERC
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    12
    grants GR/G53279, GR/H40570 and by the ESPRIT Project 6453 ``Types''.}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    13
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    14
\author{Lawrence C. Paulson\\{\tt lcp@cl.cam.ac.uk}\\
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    15
        Computer Laboratory, University of Cambridge, England}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    16
\date{\today} 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    17
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    18
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    19
\newcommand\sbs{\subseteq}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    20
\let\To=\Rightarrow
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    21
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    22
\newcommand\defn[1]{{\bf#1}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    23
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    24
\newcommand\pow{{\cal P}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    25
\newcommand\RepFun{\hbox{\tt RepFun}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    26
\newcommand\cons{\hbox{\tt cons}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    27
\def\succ{\hbox{\tt succ}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    28
\newcommand\split{\hbox{\tt split}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    29
\newcommand\fst{\hbox{\tt fst}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    30
\newcommand\snd{\hbox{\tt snd}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    31
\newcommand\converse{\hbox{\tt converse}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    32
\newcommand\domain{\hbox{\tt domain}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    33
\newcommand\range{\hbox{\tt range}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    34
\newcommand\field{\hbox{\tt field}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    35
\newcommand\lfp{\hbox{\tt lfp}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    36
\newcommand\gfp{\hbox{\tt gfp}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    37
\newcommand\id{\hbox{\tt id}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    38
\newcommand\trans{\hbox{\tt trans}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    39
\newcommand\wf{\hbox{\tt wf}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    40
\newcommand\nat{\hbox{\tt nat}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    41
\newcommand\rank{\hbox{\tt rank}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    42
\newcommand\univ{\hbox{\tt univ}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    43
\newcommand\Vrec{\hbox{\tt Vrec}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    44
\newcommand\Inl{\hbox{\tt Inl}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    45
\newcommand\Inr{\hbox{\tt Inr}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    46
\newcommand\case{\hbox{\tt case}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    47
\newcommand\lst{\hbox{\tt list}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    48
\newcommand\Nil{\hbox{\tt Nil}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    49
\newcommand\Cons{\hbox{\tt Cons}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    50
\newcommand\lstcase{\hbox{\tt list\_case}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    51
\newcommand\lstrec{\hbox{\tt list\_rec}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    52
\newcommand\length{\hbox{\tt length}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    53
\newcommand\listn{\hbox{\tt listn}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    54
\newcommand\acc{\hbox{\tt acc}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    55
\newcommand\primrec{\hbox{\tt primrec}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    56
\newcommand\SC{\hbox{\tt SC}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    57
\newcommand\CONST{\hbox{\tt CONST}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    58
\newcommand\PROJ{\hbox{\tt PROJ}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    59
\newcommand\COMP{\hbox{\tt COMP}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    60
\newcommand\PREC{\hbox{\tt PREC}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    61
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    62
\newcommand\quniv{\hbox{\tt quniv}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    63
\newcommand\llist{\hbox{\tt llist}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    64
\newcommand\LNil{\hbox{\tt LNil}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    65
\newcommand\LCons{\hbox{\tt LCons}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    66
\newcommand\lconst{\hbox{\tt lconst}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    67
\newcommand\lleq{\hbox{\tt lleq}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    68
\newcommand\map{\hbox{\tt map}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    69
\newcommand\term{\hbox{\tt term}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    70
\newcommand\Apply{\hbox{\tt Apply}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    71
\newcommand\termcase{\hbox{\tt term\_case}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    72
\newcommand\rev{\hbox{\tt rev}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    73
\newcommand\reflect{\hbox{\tt reflect}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    74
\newcommand\tree{\hbox{\tt tree}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    75
\newcommand\forest{\hbox{\tt forest}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    76
\newcommand\Part{\hbox{\tt Part}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    77
\newcommand\TF{\hbox{\tt tree\_forest}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    78
\newcommand\Tcons{\hbox{\tt Tcons}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    79
\newcommand\Fcons{\hbox{\tt Fcons}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    80
\newcommand\Fnil{\hbox{\tt Fnil}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    81
\newcommand\TFcase{\hbox{\tt TF\_case}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    82
\newcommand\Fin{\hbox{\tt Fin}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    83
\newcommand\QInl{\hbox{\tt QInl}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    84
\newcommand\QInr{\hbox{\tt QInr}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    85
\newcommand\qsplit{\hbox{\tt qsplit}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    86
\newcommand\qcase{\hbox{\tt qcase}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    87
\newcommand\Con{\hbox{\tt Con}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    88
\newcommand\data{\hbox{\tt data}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    89
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    90
\binperiod     %%%treat . like a binary operator
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    91
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    92
\begin{document}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    93
\pagestyle{empty}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    94
\begin{titlepage}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    95
\maketitle 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    96
\begin{abstract}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    97
  This paper presents a fixedpoint approach to inductive definitions.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    98
  Instead of using a syntactic test such as ``strictly positive,'' the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    99
  approach lets definitions involve any operators that have been proved
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   100
  monotone.  It is conceptually simple, which has allowed the easy
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   101
  implementation of mutual recursion and iterated definitions.  It also
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   102
  handles coinductive definitions: simply replace the least fixedpoint by a
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   103
  greatest fixedpoint.  
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   104
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   105
  The method has been implemented in two of Isabelle's logics, \textsc{zf} set
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   106
  theory and higher-order logic.  It should be applicable to any logic in
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   107
  which the Knaster-Tarski theorem can be proved.  Examples include lists of
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   108
  $n$ elements, the accessible part of a relation and the set of primitive
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   109
  recursive functions.  One example of a coinductive definition is
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   110
  bisimulations for lazy lists.  Recursive datatypes are examined in detail,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   111
  as well as one example of a \defn{codatatype}: lazy lists.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   112
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   113
  The Isabelle package has been applied in several large case studies,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   114
  including two proofs of the Church-Rosser theorem and a coinductive proof of
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   115
  semantic consistency.  The package can be trusted because it proves theorems
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   116
  from definitions, instead of asserting desired properties as axioms.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   117
\end{abstract}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   118
%
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   119
\bigskip
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   120
\centerline{Copyright \copyright{} \number\year{} by Lawrence C. Paulson}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   121
\thispagestyle{empty} 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   122
\end{titlepage}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   123
\tableofcontents\cleardoublepage\pagestyle{plain}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   124
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   125
\setcounter{page}{1}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   126
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   127
\section{Introduction}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   128
Several theorem provers provide commands for formalizing recursive data
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   129
structures, like lists and trees.  Robin Milner implemented one of the first
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   130
of these, for Edinburgh \textsc{lcf}~\cite{milner-ind}.  Given a description
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   131
of the desired data structure, Milner's package formulated appropriate
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   132
definitions and proved the characteristic theorems.  Similar is Melham's
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   133
recursive type package for the Cambridge \textsc{hol} system~\cite{melham89}.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   134
Such data structures are called \defn{datatypes}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   135
below, by analogy with datatype declarations in Standard~\textsc{ml}\@.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   136
Some logics take datatypes as primitive; consider Boyer and Moore's shell
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   137
principle~\cite{bm79} and the Coq type theory~\cite{paulin-tlca}.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   138
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   139
A datatype is but one example of an \defn{inductive definition}.  Such a
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   140
definition~\cite{aczel77} specifies the least set~$R$ \defn{closed under}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   141
given rules: applying a rule to elements of~$R$ yields a result within~$R$.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   142
Inductive definitions have many applications.  The collection of theorems in a
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   143
logic is inductively defined.  A structural operational
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   144
semantics~\cite{hennessy90} is an inductive definition of a reduction or
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   145
evaluation relation on programs.  A few theorem provers provide commands for
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   146
formalizing inductive definitions; these include Coq~\cite{paulin-tlca} and
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   147
again the \textsc{hol} system~\cite{camilleri92}.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   148
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   149
The dual notion is that of a \defn{coinductive definition}.  Such a definition
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   150
specifies the greatest set~$R$ \defn{consistent with} given rules: every
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   151
element of~$R$ can be seen as arising by applying a rule to elements of~$R$.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   152
Important examples include using bisimulation relations to formalize
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   153
equivalence of processes~\cite{milner89} or lazy functional
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   154
programs~\cite{abramsky90}.  Other examples include lazy lists and other
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   155
infinite data structures; these are called \defn{codatatypes} below.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   156
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   157
Not all inductive definitions are meaningful.  \defn{Monotone} inductive
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   158
definitions are a large, well-behaved class.  Monotonicity can be enforced
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   159
by syntactic conditions such as ``strictly positive,'' but this could lead to
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   160
monotone definitions being rejected on the grounds of their syntactic form.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   161
More flexible is to formalize monotonicity within the logic and allow users
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   162
to prove it.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   163
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   164
This paper describes a package based on a fixedpoint approach.  Least
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   165
fixedpoints yield inductive definitions; greatest fixedpoints yield
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   166
coinductive definitions.  Most of the discussion below applies equally to
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   167
inductive and coinductive definitions, and most of the code is shared.  
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   168
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   169
The package supports mutual recursion and infinitely-branching datatypes and
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   170
codatatypes.  It allows use of any operators that have been proved monotone,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   171
thus accepting all provably monotone inductive definitions, including
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   172
iterated definitions.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   173
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   174
The package has been implemented in
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   175
Isabelle~\cite{paulson-markt,paulson-isa-book} using 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   176
\textsc{zf} set theory \cite{paulson-set-I,paulson-set-II}; part of it has
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   177
since been ported to Isabelle/\textsc{hol} (higher-order logic).  The
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   178
recursion equations are specified as introduction rules for the mutually
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   179
recursive sets.  The package transforms these rules into a mapping over sets,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   180
and attempts to prove that the mapping is monotonic and well-typed.  If
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   181
successful, the package makes fixedpoint definitions and proves the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   182
introduction, elimination and (co)induction rules.  Users invoke the package
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   183
by making simple declarations in Isabelle theory files.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   184
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   185
Most datatype packages equip the new datatype with some means of expressing
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   186
recursive functions.  This is the main omission from my package.  Its
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   187
fixedpoint operators define only recursive sets.  The Isabelle/\textsc{zf}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   188
theory provides well-founded recursion~\cite{paulson-set-II}, which is harder
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   189
to use than structural recursion but considerably more general.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   190
Slind~\cite{slind-tfl} has written a package to automate the definition of
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   191
well-founded recursive functions in Isabelle/\textsc{hol}.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   192
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   193
\paragraph*{Outline.} Section~2 introduces the least and greatest fixedpoint
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   194
operators.  Section~3 discusses the form of introduction rules, mutual
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   195
recursion and other points common to inductive and coinductive definitions.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   196
Section~4 discusses induction and coinduction rules separately.  Section~5
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   197
presents several examples, including a coinductive definition.  Section~6
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   198
describes datatype definitions.  Section~7 presents related work.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   199
Section~8 draws brief conclusions.  \ifshort\else The appendices are simple
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   200
user's manuals for this Isabelle package.\fi
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   201
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   202
Most of the definitions and theorems shown below have been generated by the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   203
package.  I have renamed some variables to improve readability.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   204
 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   205
\section{Fixedpoint operators}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   206
In set theory, the least and greatest fixedpoint operators are defined as
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   207
follows:
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   208
\begin{eqnarray*}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   209
   \lfp(D,h)  & \equiv & \inter\{X\sbs D. h(X)\sbs X\} \\
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   210
   \gfp(D,h)  & \equiv & \union\{X\sbs D. X\sbs h(X)\}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   211
\end{eqnarray*}   
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   212
Let $D$ be a set.  Say that $h$ is \defn{bounded by}~$D$ if $h(D)\sbs D$, and
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   213
\defn{monotone below~$D$} if
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   214
$h(A)\sbs h(B)$ for all $A$ and $B$ such that $A\sbs B\sbs D$.  If $h$ is
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   215
bounded by~$D$ and monotone then both operators yield fixedpoints:
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   216
\begin{eqnarray*}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   217
   \lfp(D,h)  & = & h(\lfp(D,h)) \\
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   218
   \gfp(D,h)  & = & h(\gfp(D,h)) 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   219
\end{eqnarray*}   
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   220
These equations are instances of the Knaster-Tarski theorem, which states
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   221
that every monotonic function over a complete lattice has a
6745
74e8f703f5f2 tuned manual.bib;
wenzelm
parents: 6637
diff changeset
   222
fixedpoint~\cite{davey-priestley}.  It is obvious from their definitions
3162
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   223
that $\lfp$ must be the least fixedpoint, and $\gfp$ the greatest.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   224
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   225
This fixedpoint theory is simple.  The Knaster-Tarski theorem is easy to
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   226
prove.  Showing monotonicity of~$h$ is trivial, in typical cases.  We must
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   227
also exhibit a bounding set~$D$ for~$h$.  Frequently this is trivial, as when
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   228
a set of theorems is (co)inductively defined over some previously existing set
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   229
of formul{\ae}.  Isabelle/\textsc{zf} provides suitable bounding sets for
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   230
infinitely-branching (co)datatype definitions; see~\S\ref{univ-sec}.  Bounding
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   231
sets are also called \defn{domains}.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   232
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   233
The powerset operator is monotone, but by Cantor's theorem there is no
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   234
set~$A$ such that $A=\pow(A)$.  We cannot put $A=\lfp(D,\pow)$ because
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   235
there is no suitable domain~$D$.  But \S\ref{acc-sec} demonstrates
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   236
that~$\pow$ is still useful in inductive definitions.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   237
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   238
\section{Elements of an inductive or coinductive definition}\label{basic-sec}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   239
Consider a (co)inductive definition of the sets $R_1$, \ldots,~$R_n$, in
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   240
mutual recursion.  They will be constructed from domains $D_1$,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   241
\ldots,~$D_n$, respectively.  The construction yields not $R_i\sbs D_i$ but
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   242
$R_i\sbs D_1+\cdots+D_n$, where $R_i$ is contained in the image of~$D_i$
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   243
under an injection.  Reasons for this are discussed
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   244
elsewhere~\cite[\S4.5]{paulson-set-II}.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   245
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   246
The definition may involve arbitrary parameters $\vec{p}=p_1$,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   247
\ldots,~$p_k$.  Each recursive set then has the form $R_i(\vec{p})$.  The
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   248
parameters must be identical every time they occur within a definition.  This
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   249
would appear to be a serious restriction compared with other systems such as
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   250
Coq~\cite{paulin-tlca}.  For instance, we cannot define the lists of
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   251
$n$ elements as the set $\listn(A,n)$ using rules where the parameter~$n$
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   252
varies.  Section~\ref{listn-sec} describes how to express this set using the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   253
inductive definition package.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   254
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   255
To avoid clutter below, the recursive sets are shown as simply $R_i$
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   256
instead of~$R_i(\vec{p})$.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   257
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   258
\subsection{The form of the introduction rules}\label{intro-sec}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   259
The body of the definition consists of the desired introduction rules.  The
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   260
conclusion of each rule must have the form $t\in R_i$, where $t$ is any term.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   261
Premises typically have the same form, but they can have the more general form
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   262
$t\in M(R_i)$ or express arbitrary side-conditions.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   263
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   264
The premise $t\in M(R_i)$ is permitted if $M$ is a monotonic operator on
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   265
sets, satisfying the rule 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   266
\[ \infer{M(A)\sbs M(B)}{A\sbs B} \]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   267
The user must supply the package with monotonicity rules for all such premises.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   268
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   269
The ability to introduce new monotone operators makes the approach
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   270
flexible.  A suitable choice of~$M$ and~$t$ can express a lot.  The
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   271
powerset operator $\pow$ is monotone, and the premise $t\in\pow(R)$
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   272
expresses $t\sbs R$; see \S\ref{acc-sec} for an example.  The \emph{list of}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   273
operator is monotone, as is easily proved by induction.  The premise
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   274
$t\in\lst(R)$ avoids having to encode the effect of~$\lst(R)$ using mutual
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   275
recursion; see \S\ref{primrec-sec} and also my earlier
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   276
paper~\cite[\S4.4]{paulson-set-II}.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   277
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   278
Introduction rules may also contain \defn{side-conditions}.  These are
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   279
premises consisting of arbitrary formul{\ae} not mentioning the recursive
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   280
sets. Side-conditions typically involve type-checking.  One example is the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   281
premise $a\in A$ in the following rule from the definition of lists:
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   282
\[ \infer{\Cons(a,l)\in\lst(A)}{a\in A & l\in\lst(A)} \]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   283
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   284
\subsection{The fixedpoint definitions}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   285
The package translates the list of desired introduction rules into a fixedpoint
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   286
definition.  Consider, as a running example, the finite powerset operator
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   287
$\Fin(A)$: the set of all finite subsets of~$A$.  It can be
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   288
defined as the least set closed under the rules
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   289
\[  \emptyset\in\Fin(A)  \qquad 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   290
    \infer{\{a\}\un b\in\Fin(A)}{a\in A & b\in\Fin(A)} 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   291
\]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   292
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   293
The domain in a (co)inductive definition must be some existing set closed
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   294
under the rules.  A suitable domain for $\Fin(A)$ is $\pow(A)$, the set of all
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   295
subsets of~$A$.  The package generates the definition
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   296
\[  \Fin(A) \equiv \lfp(\pow(A), \,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   297
  \begin{array}[t]{r@{\,}l}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   298
      \lambda X. \{z\in\pow(A). & z=\emptyset \disj{} \\
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   299
                  &(\exists a\,b. z=\{a\}\un b\conj a\in A\conj b\in X)\})
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   300
  \end{array}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   301
\]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   302
The contribution of each rule to the definition of $\Fin(A)$ should be
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   303
obvious.  A coinductive definition is similar but uses $\gfp$ instead
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   304
of~$\lfp$.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   305
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   306
The package must prove that the fixedpoint operator is applied to a
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   307
monotonic function.  If the introduction rules have the form described
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   308
above, and if the package is supplied a monotonicity theorem for every
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   309
$t\in M(R_i)$ premise, then this proof is trivial.\footnote{Due to the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   310
  presence of logical connectives in the fixedpoint's body, the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   311
  monotonicity proof requires some unusual rules.  These state that the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   312
  connectives $\conj$, $\disj$ and $\exists$ preserve monotonicity with respect
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   313
  to the partial ordering on unary predicates given by $P\sqsubseteq Q$ if and
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   314
  only if $\forall x.P(x)\imp Q(x)$.}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   315
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   316
The package returns its result as an \textsc{ml} structure, which consists of named
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   317
components; we may regard it as a record.  The result structure contains
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   318
the definitions of the recursive sets as a theorem list called {\tt defs}.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   319
It also contains some theorems; {\tt dom\_subset} is an inclusion such as 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   320
$\Fin(A)\sbs\pow(A)$, while {\tt bnd\_mono} asserts that the fixedpoint
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   321
definition is monotonic.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   322
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   323
Internally the package uses the theorem {\tt unfold}, a fixedpoint equation
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   324
such as
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   325
\[
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   326
  \begin{array}[t]{r@{\,}l}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   327
     \Fin(A) = \{z\in\pow(A). & z=\emptyset \disj{} \\
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   328
             &(\exists a\,b. z=\{a\}\un b\conj a\in A\conj b\in \Fin(A))\}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   329
  \end{array}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   330
\]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   331
In order to save space, this theorem is not exported.  
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   332
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   333
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   334
\subsection{Mutual recursion} \label{mutual-sec}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   335
In a mutually recursive definition, the domain of the fixedpoint construction
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   336
is the disjoint sum of the domain~$D_i$ of each~$R_i$, for $i=1$,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   337
\ldots,~$n$.  The package uses the injections of the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   338
binary disjoint sum, typically $\Inl$ and~$\Inr$, to express injections
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   339
$h_{1n}$, \ldots, $h_{nn}$ for the $n$-ary disjoint sum $D_1+\cdots+D_n$.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   340
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   341
As discussed elsewhere \cite[\S4.5]{paulson-set-II}, Isabelle/\textsc{zf} defines the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   342
operator $\Part$ to support mutual recursion.  The set $\Part(A,h)$
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   343
contains those elements of~$A$ having the form~$h(z)$:
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   344
\[ \Part(A,h)  \equiv \{x\in A. \exists z. x=h(z)\}. \]   
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   345
For mutually recursive sets $R_1$, \ldots,~$R_n$ with
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   346
$n>1$, the package makes $n+1$ definitions.  The first defines a set $R$ using
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   347
a fixedpoint operator. The remaining $n$ definitions have the form
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   348
\[ R_i \equiv \Part(R,h_{in}), \qquad i=1,\ldots, n.  \] 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   349
It follows that $R=R_1\un\cdots\un R_n$, where the $R_i$ are pairwise disjoint.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   350
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   351
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   352
\subsection{Proving the introduction rules}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   353
The user supplies the package with the desired form of the introduction
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   354
rules.  Once it has derived the theorem {\tt unfold}, it attempts
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   355
to prove those rules.  From the user's point of view, this is the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   356
trickiest stage; the proofs often fail.  The task is to show that the domain 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   357
$D_1+\cdots+D_n$ of the combined set $R_1\un\cdots\un R_n$ is
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   358
closed under all the introduction rules.  This essentially involves replacing
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   359
each~$R_i$ by $D_1+\cdots+D_n$ in each of the introduction rules and
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   360
attempting to prove the result.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   361
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   362
Consider the $\Fin(A)$ example.  After substituting $\pow(A)$ for $\Fin(A)$
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   363
in the rules, the package must prove
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   364
\[  \emptyset\in\pow(A)  \qquad 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   365
    \infer{\{a\}\un b\in\pow(A)}{a\in A & b\in\pow(A)} 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   366
\]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   367
Such proofs can be regarded as type-checking the definition.\footnote{The
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   368
  Isabelle/\textsc{hol} version does not require these proofs, as \textsc{hol}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   369
  has implicit type-checking.} The user supplies the package with
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   370
type-checking rules to apply.  Usually these are general purpose rules from
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   371
the \textsc{zf} theory.  They could however be rules specifically proved for a
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   372
particular inductive definition; sometimes this is the easiest way to get the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   373
definition through!
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   374
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   375
The result structure contains the introduction rules as the theorem list {\tt
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   376
intrs}.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   377
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   378
\subsection{The case analysis rule}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   379
The elimination rule, called {\tt elim}, performs case analysis.  It is a
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   380
simple consequence of {\tt unfold}.  There is one case for each introduction
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   381
rule.  If $x\in\Fin(A)$ then either $x=\emptyset$ or else $x=\{a\}\un b$ for
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   382
some $a\in A$ and $b\in\Fin(A)$.  Formally, the elimination rule for $\Fin(A)$
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   383
is written
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   384
\[ \infer{Q}{x\in\Fin(A) & \infer*{Q}{[x=\emptyset]}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   385
                 & \infer*{Q}{[x=\{a\}\un b & a\in A &b\in\Fin(A)]_{a,b}} }
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   386
\]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   387
The subscripted variables $a$ and~$b$ above the third premise are
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   388
eigenvariables, subject to the usual ``not free in \ldots'' proviso.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   389
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   390
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   391
\section{Induction and coinduction rules}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   392
Here we must consider inductive and coinductive definitions separately.  For
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   393
an inductive definition, the package returns an induction rule derived
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   394
directly from the properties of least fixedpoints, as well as a modified rule
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   395
for mutual recursion.  For a coinductive definition, the package returns a
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   396
basic coinduction rule.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   397
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   398
\subsection{The basic induction rule}\label{basic-ind-sec}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   399
The basic rule, called {\tt induct}, is appropriate in most situations.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   400
For inductive definitions, it is strong rule induction~\cite{camilleri92}; for
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   401
datatype definitions (see below), it is just structural induction.  
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   402
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   403
The induction rule for an inductively defined set~$R$ has the form described
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   404
below.  For the time being, assume that $R$'s domain is not a Cartesian
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   405
product; inductively defined relations are treated slightly differently.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   406
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   407
The major premise is $x\in R$.  There is a minor premise for each
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   408
introduction rule:
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   409
\begin{itemize}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   410
\item If the introduction rule concludes $t\in R_i$, then the minor premise
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   411
is~$P(t)$.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   412
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   413
\item The minor premise's eigenvariables are precisely the introduction
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   414
rule's free variables that are not parameters of~$R$.  For instance, the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   415
eigenvariables in the $\Fin(A)$ rule below are $a$ and $b$, but not~$A$.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   416
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   417
\item If the introduction rule has a premise $t\in R_i$, then the minor
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   418
premise discharges the assumption $t\in R_i$ and the induction
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   419
hypothesis~$P(t)$.  If the introduction rule has a premise $t\in M(R_i)$
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   420
then the minor premise discharges the single assumption
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   421
\[ t\in M(\{z\in R_i. P(z)\}). \] 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   422
Because $M$ is monotonic, this assumption implies $t\in M(R_i)$.  The
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   423
occurrence of $P$ gives the effect of an induction hypothesis, which may be
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   424
exploited by appealing to properties of~$M$.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   425
\end{itemize}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   426
The induction rule for $\Fin(A)$ resembles the elimination rule shown above,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   427
but includes an induction hypothesis:
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   428
\[ \infer{P(x)}{x\in\Fin(A) & P(\emptyset)
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   429
        & \infer*{P(\{a\}\un b)}{[a\in A & b\in\Fin(A) & P(b)]_{a,b}} }
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   430
\] 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   431
Stronger induction rules often suggest themselves.  We can derive a rule for
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   432
$\Fin(A)$ whose third premise discharges the extra assumption $a\not\in b$.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   433
The package provides rules for mutual induction and inductive relations.  The
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   434
Isabelle/\textsc{zf} theory also supports well-founded induction and recursion
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   435
over datatypes, by reasoning about the \defn{rank} of a
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   436
set~\cite[\S3.4]{paulson-set-II}.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   437
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   438
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   439
\subsection{Modified induction rules}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   440
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   441
If the domain of $R$ is a Cartesian product $A_1\times\cdots\times A_m$
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   442
(however nested), then the corresponding predicate $P_i$ takes $m$ arguments.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   443
The major premise becomes $\pair{z_1,\ldots,z_m}\in R$ instead of $x\in R$;
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   444
the conclusion becomes $P(z_1,\ldots,z_m)$.  This simplifies reasoning about
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   445
inductively defined relations, eliminating the need to express properties of
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   446
$z_1$, \ldots,~$z_m$ as properties of the tuple $\pair{z_1,\ldots,z_m}$.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   447
Occasionally it may require you to split up the induction variable
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   448
using {\tt SigmaE} and {\tt dom\_subset}, especially if the constant {\tt
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   449
  split} appears in the rule.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   450
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   451
The mutual induction rule is called {\tt
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   452
mutual\_induct}.  It differs from the basic rule in two respects:
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   453
\begin{itemize}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   454
\item Instead of a single predicate~$P$, it uses $n$ predicates $P_1$,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   455
\ldots,~$P_n$: one for each recursive set.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   456
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   457
\item There is no major premise such as $x\in R_i$.  Instead, the conclusion
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   458
refers to all the recursive sets:
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   459
\[ (\forall z.z\in R_1\imp P_1(z))\conj\cdots\conj
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   460
   (\forall z.z\in R_n\imp P_n(z))
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   461
\]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   462
Proving the premises establishes $P_i(z)$ for $z\in R_i$ and $i=1$,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   463
\ldots,~$n$.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   464
\end{itemize}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   465
%
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   466
If the domain of some $R_i$ is a Cartesian product, then the mutual induction
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   467
rule is modified accordingly.  The predicates are made to take $m$ separate
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   468
arguments instead of a tuple, and the quantification in the conclusion is over
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   469
the separate variables $z_1$, \ldots, $z_m$.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   470
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   471
\subsection{Coinduction}\label{coind-sec}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   472
A coinductive definition yields a primitive coinduction rule, with no
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   473
refinements such as those for the induction rules.  (Experience may suggest
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   474
refinements later.)  Consider the codatatype of lazy lists as an example.  For
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   475
suitable definitions of $\LNil$ and $\LCons$, lazy lists may be defined as the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   476
greatest set consistent with the rules
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   477
\[  \LNil\in\llist(A)  \qquad 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   478
    \infer[(-)]{\LCons(a,l)\in\llist(A)}{a\in A & l\in\llist(A)}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   479
\]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   480
The $(-)$ tag stresses that this is a coinductive definition.  A suitable
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   481
domain for $\llist(A)$ is $\quniv(A)$; this set is closed under the variant
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   482
forms of sum and product that are used to represent non-well-founded data
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   483
structures (see~\S\ref{univ-sec}).
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   484
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   485
The package derives an {\tt unfold} theorem similar to that for $\Fin(A)$. 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   486
Then it proves the theorem {\tt coinduct}, which expresses that $\llist(A)$
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   487
is the greatest solution to this equation contained in $\quniv(A)$:
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   488
\[ \infer{x\in\llist(A)}{x\in X & X\sbs \quniv(A) &
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   489
    \infer*{
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   490
     \begin{array}[b]{r@{}l}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   491
       z=\LNil\disj 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   492
       \bigl(\exists a\,l.\, & z=\LCons(a,l) \conj a\in A \conj{}\\
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   493
                             & l\in X\un\llist(A) \bigr)
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   494
     \end{array}  }{[z\in X]_z}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   495
\]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   496
This rule complements the introduction rules; it provides a means of showing
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   497
$x\in\llist(A)$ when $x$ is infinite.  For instance, if $x=\LCons(0,x)$ then
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   498
applying the rule with $X=\{x\}$ proves $x\in\llist(\nat)$.  (Here $\nat$
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   499
is the set of natural numbers.)
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   500
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   501
Having $X\un\llist(A)$ instead of simply $X$ in the third premise above
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   502
represents a slight strengthening of the greatest fixedpoint property.  I
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   503
discuss several forms of coinduction rules elsewhere~\cite{paulson-coind}.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   504
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   505
The clumsy form of the third premise makes the rule hard to use, especially in
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   506
large definitions.  Probably a constant should be declared to abbreviate the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   507
large disjunction, and rules derived to allow proving the separate disjuncts.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   508
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   509
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   510
\section{Examples of inductive and coinductive definitions}\label{ind-eg-sec}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   511
This section presents several examples from the literature: the finite
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   512
powerset operator, lists of $n$ elements, bisimulations on lazy lists, the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   513
well-founded part of a relation, and the primitive recursive functions.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   514
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   515
\subsection{The finite powerset operator}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   516
This operator has been discussed extensively above.  Here is the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   517
corresponding invocation in an Isabelle theory file.  Note that
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   518
$\cons(a,b)$ abbreviates $\{a\}\un b$ in Isabelle/\textsc{zf}.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   519
\begin{ttbox}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   520
Finite = Arith + 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   521
consts      Fin :: i=>i
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   522
inductive
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   523
  domains   "Fin(A)" <= "Pow(A)"
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   524
  intrs
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   525
    emptyI  "0 : Fin(A)"
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   526
    consI   "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"
6124
3aa7926f039a deleted the appendices because documentation exists in the HOL and ZF manuals
paulson
parents: 4265
diff changeset
   527
  type_intrs  empty_subsetI, cons_subsetI, PowI
3162
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   528
  type_elims "[make_elim PowD]"
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   529
end
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   530
\end{ttbox}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   531
Theory {\tt Finite} extends the parent theory {\tt Arith} by declaring the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   532
unary function symbol~$\Fin$, which is defined inductively.  Its domain is
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   533
specified as $\pow(A)$, where $A$ is the parameter appearing in the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   534
introduction rules.  For type-checking, we supply two introduction
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   535
rules:
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   536
\[ \emptyset\sbs A              \qquad
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   537
   \infer{\{a\}\un B\sbs C}{a\in C & B\sbs C}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   538
\]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   539
A further introduction rule and an elimination rule express both
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   540
directions of the equivalence $A\in\pow(B)\bimp A\sbs B$.  Type-checking
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   541
involves mostly introduction rules.  
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   542
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   543
Like all Isabelle theory files, this one yields a structure containing the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   544
new theory as an \textsc{ml} value.  Structure {\tt Finite} also has a
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   545
substructure, called~{\tt Fin}.  After declaring \hbox{\tt open Finite;} we
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   546
can refer to the $\Fin(A)$ introduction rules as the list {\tt Fin.intrs}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   547
or individually as {\tt Fin.emptyI} and {\tt Fin.consI}.  The induction
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   548
rule is {\tt Fin.induct}.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   549
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   550
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   551
\subsection{Lists of $n$ elements}\label{listn-sec}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   552
This has become a standard example of an inductive definition.  Following
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   553
Paulin-Mohring~\cite{paulin-tlca}, we could attempt to define a new datatype
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   554
$\listn(A,n)$, for lists of length~$n$, as an $n$-indexed family of sets.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   555
But her introduction rules
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   556
\[ \hbox{\tt Niln}\in\listn(A,0)  \qquad
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   557
   \infer{\hbox{\tt Consn}(n,a,l)\in\listn(A,\succ(n))}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   558
         {n\in\nat & a\in A & l\in\listn(A,n)}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   559
\]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   560
are not acceptable to the inductive definition package:
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   561
$\listn$ occurs with three different parameter lists in the definition.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   562
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   563
The Isabelle version of this example suggests a general treatment of
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   564
varying parameters.  It uses the existing datatype definition of
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   565
$\lst(A)$, with constructors $\Nil$ and~$\Cons$, and incorporates the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   566
parameter~$n$ into the inductive set itself.  It defines $\listn(A)$ as a
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   567
relation consisting of pairs $\pair{n,l}$ such that $n\in\nat$
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   568
and~$l\in\lst(A)$ and $l$ has length~$n$.  In fact, $\listn(A)$ is the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   569
converse of the length function on~$\lst(A)$.  The Isabelle/\textsc{zf} introduction
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   570
rules are
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   571
\[ \pair{0,\Nil}\in\listn(A)  \qquad
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   572
   \infer{\pair{\succ(n),\Cons(a,l)}\in\listn(A)}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   573
         {a\in A & \pair{n,l}\in\listn(A)}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   574
\]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   575
The Isabelle theory file takes, as parent, the theory~{\tt List} of lists.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   576
We declare the constant~$\listn$ and supply an inductive definition,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   577
specifying the domain as $\nat\times\lst(A)$:
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   578
\begin{ttbox}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   579
ListN = List +
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   580
consts  listn :: i=>i
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   581
inductive
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   582
  domains   "listn(A)" <= "nat*list(A)"
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   583
  intrs
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   584
    NilI  "<0,Nil>: listn(A)"
6631
ccae8c659762 changes for new manual.bib
paulson
parents: 6141
diff changeset
   585
    ConsI "[| a:A; <n,l>:listn(A) |] ==> <succ(n), Cons(a,l)>: listn(A)"
3162
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   586
  type_intrs "nat_typechecks @ list.intrs"
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   587
end
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   588
\end{ttbox}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   589
The type-checking rules include those for 0, $\succ$, $\Nil$ and $\Cons$.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   590
Because $\listn(A)$ is a set of pairs, type-checking requires the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   591
equivalence $\pair{a,b}\in A\times B \bimp a\in A \conj b\in B$.  The
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   592
package always includes the rules for ordered pairs.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   593
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   594
The package returns introduction, elimination and induction rules for
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   595
$\listn$.  The basic induction rule, {\tt listn.induct}, is
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   596
\[ \infer{P(z_1,z_2)}{\pair{z_1,z_2}\in\listn(A) & P(0,\Nil) &
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   597
             \infer*{P(\succ(n),\Cons(a,l))}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   598
                {[a\in A & \pair{n,l}\in\listn(A) & P(n,l)]_{a,l,n}}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   599
\]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   600
This rule lets the induction formula to be a 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   601
binary property of pairs, $P(n,l)$.  
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   602
It is now a simple matter to prove theorems about $\listn(A)$, such as
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   603
\[ \forall l\in\lst(A). \pair{\length(l),\, l}\in\listn(A) \]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   604
\[ \listn(A)``\{n\} = \{l\in\lst(A). \length(l)=n\} \]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   605
This latter result --- here $r``X$ denotes the image of $X$ under $r$
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   606
--- asserts that the inductive definition agrees with the obvious notion of
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   607
$n$-element list.  
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   608
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   609
A ``list of $n$ elements'' really is a list, namely an element of ~$\lst(A)$.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   610
It is subject to list operators such as append (concatenation).  For example,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   611
a trivial induction on $\pair{m,l}\in\listn(A)$ yields
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   612
\[ \infer{\pair{m\mathbin{+} m',\, l@l'}\in\listn(A)}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   613
         {\pair{m,l}\in\listn(A) & \pair{m',l'}\in\listn(A)} 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   614
\]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   615
where $+$ denotes addition on the natural numbers and @ denotes append.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   616
6637
57abed64dc14 pdf setup;
wenzelm
parents: 6631
diff changeset
   617
\subsection{Rule inversion: the function \texttt{mk\_cases}}
3162
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   618
The elimination rule, {\tt listn.elim}, is cumbersome:
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   619
\[ \infer{Q}{x\in\listn(A) & 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   620
          \infer*{Q}{[x = \pair{0,\Nil}]} &
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   621
          \infer*{Q}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   622
             {\left[\begin{array}{l}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   623
               x = \pair{\succ(n),\Cons(a,l)} \\
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   624
               a\in A \\
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   625
               \pair{n,l}\in\listn(A)
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   626
               \end{array} \right]_{a,l,n}}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   627
\]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   628
The \textsc{ml} function {\tt listn.mk\_cases} generates simplified instances of
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   629
this rule.  It works by freeness reasoning on the list constructors:
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   630
$\Cons(a,l)$ is injective in its two arguments and differs from~$\Nil$.  If
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   631
$x$ is $\pair{i,\Nil}$ or $\pair{i,\Cons(a,l)}$ then {\tt listn.mk\_cases}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   632
deduces the corresponding form of~$i$;  this is called rule inversion.  
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   633
Here is a sample session: 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   634
\begin{ttbox}
6141
a6922171b396 removal of the (thm list) argument of mk_cases
paulson
parents: 6124
diff changeset
   635
listn.mk_cases "<i,Nil> : listn(A)";
3162
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   636
{\out "[| <?i, []> : listn(?A); ?i = 0 ==> ?Q |] ==> ?Q" : thm}
6141
a6922171b396 removal of the (thm list) argument of mk_cases
paulson
parents: 6124
diff changeset
   637
listn.mk_cases "<i,Cons(a,l)> : listn(A)";
3162
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   638
{\out "[| <?i, Cons(?a, ?l)> : listn(?A);}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   639
{\out     !!n. [| ?a : ?A; <n, ?l> : listn(?A); ?i = succ(n) |] ==> ?Q }
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   640
{\out  |] ==> ?Q" : thm}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   641
\end{ttbox}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   642
Each of these rules has only two premises.  In conventional notation, the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   643
second rule is
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   644
\[ \infer{Q}{\pair{i, \Cons(a,l)}\in\listn(A) & 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   645
          \infer*{Q}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   646
             {\left[\begin{array}{l}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   647
               a\in A \\ \pair{n,l}\in\listn(A) \\ i = \succ(n)
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   648
               \end{array} \right]_{n}}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   649
\]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   650
The package also has built-in rules for freeness reasoning about $0$
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   651
and~$\succ$.  So if $x$ is $\pair{0,l}$ or $\pair{\succ(i),l}$, then {\tt
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   652
listn.mk\_cases} can deduce the corresponding form of~$l$. 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   653
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   654
The function {\tt mk\_cases} is also useful with datatype definitions.  The
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   655
instance from the definition of lists, namely {\tt list.mk\_cases}, can
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   656
prove that $\Cons(a,l)\in\lst(A)$ implies $a\in A $ and $l\in\lst(A)$:
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   657
\[ \infer{Q}{\Cons(a,l)\in\lst(A) & 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   658
                 & \infer*{Q}{[a\in A &l\in\lst(A)]} }
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   659
\]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   660
A typical use of {\tt mk\_cases} concerns inductive definitions of evaluation
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   661
relations.  Then rule inversion yields case analysis on possible evaluations.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   662
For example, Isabelle/\textsc{zf} includes a short proof of the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   663
diamond property for parallel contraction on combinators.  Ole Rasmussen used
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   664
{\tt mk\_cases} extensively in his development of the theory of
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   665
residuals~\cite{rasmussen95}.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   666
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   667
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   668
\subsection{A coinductive definition: bisimulations on lazy lists}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   669
This example anticipates the definition of the codatatype $\llist(A)$, which
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   670
consists of finite and infinite lists over~$A$.  Its constructors are $\LNil$
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   671
and~$\LCons$, satisfying the introduction rules shown in~\S\ref{coind-sec}.  
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   672
Because $\llist(A)$ is defined as a greatest fixedpoint and uses the variant
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   673
pairing and injection operators, it contains non-well-founded elements such as
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   674
solutions to $\LCons(a,l)=l$.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   675
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   676
The next step in the development of lazy lists is to define a coinduction
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   677
principle for proving equalities.  This is done by showing that the equality
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   678
relation on lazy lists is the greatest fixedpoint of some monotonic
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   679
operation.  The usual approach~\cite{pitts94} is to define some notion of 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   680
bisimulation for lazy lists, define equivalence to be the greatest
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   681
bisimulation, and finally to prove that two lazy lists are equivalent if and
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   682
only if they are equal.  The coinduction rule for equivalence then yields a
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   683
coinduction principle for equalities.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   684
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   685
A binary relation $R$ on lazy lists is a \defn{bisimulation} provided $R\sbs
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   686
R^+$, where $R^+$ is the relation
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   687
\[ \{\pair{\LNil,\LNil}\} \un 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   688
   \{\pair{\LCons(a,l),\LCons(a,l')} . a\in A \conj \pair{l,l'}\in R\}.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   689
\]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   690
A pair of lazy lists are \defn{equivalent} if they belong to some
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   691
bisimulation.  Equivalence can be coinductively defined as the greatest
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   692
fixedpoint for the introduction rules
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   693
\[  \pair{\LNil,\LNil} \in\lleq(A)  \qquad 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   694
    \infer[(-)]{\pair{\LCons(a,l),\LCons(a,l')} \in\lleq(A)}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   695
          {a\in A & \pair{l,l'}\in \lleq(A)}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   696
\]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   697
To make this coinductive definition, the theory file includes (after the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   698
declaration of $\llist(A)$) the following lines:
6631
ccae8c659762 changes for new manual.bib
paulson
parents: 6141
diff changeset
   699
\bgroup\leftmargini=\parindent
3162
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   700
\begin{ttbox}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   701
consts    lleq :: i=>i
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   702
coinductive
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   703
  domains "lleq(A)" <= "llist(A) * llist(A)"
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   704
  intrs
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   705
    LNil  "<LNil,LNil> : lleq(A)"
6631
ccae8c659762 changes for new manual.bib
paulson
parents: 6141
diff changeset
   706
    LCons "[| a:A; <l,l'>:lleq(A) |] ==> <LCons(a,l),LCons(a,l')>: lleq(A)"
3162
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   707
  type_intrs  "llist.intrs"
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   708
\end{ttbox}
6631
ccae8c659762 changes for new manual.bib
paulson
parents: 6141
diff changeset
   709
\egroup
3162
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   710
The domain of $\lleq(A)$ is $\llist(A)\times\llist(A)$.  The type-checking
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   711
rules include the introduction rules for $\llist(A)$, whose 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   712
declaration is discussed below (\S\ref{lists-sec}).
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   713
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   714
The package returns the introduction rules and the elimination rule, as
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   715
usual.  But instead of induction rules, it returns a coinduction rule.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   716
The rule is too big to display in the usual notation; its conclusion is
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   717
$x\in\lleq(A)$ and its premises are $x\in X$, 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   718
${X\sbs\llist(A)\times\llist(A)}$ and
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   719
\[ \infer*{z=\pair{\LNil,\LNil}\disj \bigl(\exists a\,l\,l'.\,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   720
     \begin{array}[t]{@{}l}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   721
       z=\pair{\LCons(a,l),\LCons(a,l')} \conj a\in A \conj{}\\
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   722
       \pair{l,l'}\in X\un\lleq(A) \bigr)
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   723
     \end{array}  
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   724
    }{[z\in X]_z}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   725
\]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   726
Thus if $x\in X$, where $X$ is a bisimulation contained in the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   727
domain of $\lleq(A)$, then $x\in\lleq(A)$.  It is easy to show that
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   728
$\lleq(A)$ is reflexive: the equality relation is a bisimulation.  And
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   729
$\lleq(A)$ is symmetric: its converse is a bisimulation.  But showing that
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   730
$\lleq(A)$ coincides with the equality relation takes some work.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   731
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   732
\subsection{The accessible part of a relation}\label{acc-sec}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   733
Let $\prec$ be a binary relation on~$D$; in short, $(\prec)\sbs D\times D$.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   734
The \defn{accessible} or \defn{well-founded} part of~$\prec$, written
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   735
$\acc(\prec)$, is essentially that subset of~$D$ for which $\prec$ admits
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   736
no infinite decreasing chains~\cite{aczel77}.  Formally, $\acc(\prec)$ is
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   737
inductively defined to be the least set that contains $a$ if it contains
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   738
all $\prec$-predecessors of~$a$, for $a\in D$.  Thus we need an
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   739
introduction rule of the form 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   740
\[ \infer{a\in\acc(\prec)}{\forall y.y\prec a\imp y\in\acc(\prec)} \]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   741
Paulin-Mohring treats this example in Coq~\cite{paulin-tlca}, but it causes
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   742
difficulties for other systems.  Its premise is not acceptable to the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   743
inductive definition package of the Cambridge \textsc{hol}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   744
system~\cite{camilleri92}.  It is also unacceptable to the Isabelle package
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   745
(recall \S\ref{intro-sec}), but fortunately can be transformed into the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   746
acceptable form $t\in M(R)$.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   747
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   748
The powerset operator is monotonic, and $t\in\pow(R)$ is equivalent to
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   749
$t\sbs R$.  This in turn is equivalent to $\forall y\in t. y\in R$.  To
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   750
express $\forall y.y\prec a\imp y\in\acc(\prec)$ we need only find a
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   751
term~$t$ such that $y\in t$ if and only if $y\prec a$.  A suitable $t$ is
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   752
the inverse image of~$\{a\}$ under~$\prec$.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   753
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   754
The definition below follows this approach.  Here $r$ is~$\prec$ and
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   755
$\field(r)$ refers to~$D$, the domain of $\acc(r)$.  (The field of a
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   756
relation is the union of its domain and range.)  Finally $r^{-}``\{a\}$
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   757
denotes the inverse image of~$\{a\}$ under~$r$.  We supply the theorem {\tt
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   758
  Pow\_mono}, which asserts that $\pow$ is monotonic.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   759
\begin{ttbox}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   760
consts    acc :: i=>i
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   761
inductive
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   762
  domains "acc(r)" <= "field(r)"
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   763
  intrs
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   764
    vimage  "[| r-``\{a\}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"
6124
3aa7926f039a deleted the appendices because documentation exists in the HOL and ZF manuals
paulson
parents: 4265
diff changeset
   765
  monos      Pow_mono
3162
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   766
\end{ttbox}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   767
The Isabelle theory proceeds to prove facts about $\acc(\prec)$.  For
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   768
instance, $\prec$ is well-founded if and only if its field is contained in
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   769
$\acc(\prec)$.  
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   770
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   771
As mentioned in~\S\ref{basic-ind-sec}, a premise of the form $t\in M(R)$
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   772
gives rise to an unusual induction hypothesis.  Let us examine the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   773
induction rule, {\tt acc.induct}:
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   774
\[ \infer{P(x)}{x\in\acc(r) &
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   775
     \infer*{P(a)}{\left[
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   776
                   \begin{array}{r@{}l}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   777
                     r^{-}``\{a\} &\, \in\pow(\{z\in\acc(r).P(z)\}) \\
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   778
                                a &\, \in\field(r)
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   779
                   \end{array}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   780
                   \right]_a}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   781
\]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   782
The strange induction hypothesis is equivalent to
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   783
$\forall y. \pair{y,a}\in r\imp y\in\acc(r)\conj P(y)$.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   784
Therefore the rule expresses well-founded induction on the accessible part
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   785
of~$\prec$.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   786
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   787
The use of inverse image is not essential.  The Isabelle package can accept
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   788
introduction rules with arbitrary premises of the form $\forall
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   789
\vec{y}.P(\vec{y})\imp f(\vec{y})\in R$.  The premise can be expressed
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   790
equivalently as 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   791
\[ \{z\in D. P(\vec{y}) \conj z=f(\vec{y})\} \in \pow(R) \] 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   792
provided $f(\vec{y})\in D$ for all $\vec{y}$ such that~$P(\vec{y})$.  The
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   793
following section demonstrates another use of the premise $t\in M(R)$,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   794
where $M=\lst$. 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   795
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   796
\subsection{The primitive recursive functions}\label{primrec-sec}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   797
The primitive recursive functions are traditionally defined inductively, as
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   798
a subset of the functions over the natural numbers.  One difficulty is that
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   799
functions of all arities are taken together, but this is easily
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   800
circumvented by regarding them as functions on lists.  Another difficulty,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   801
the notion of composition, is less easily circumvented.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   802
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   803
Here is a more precise definition.  Letting $\vec{x}$ abbreviate
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   804
$x_0,\ldots,x_{n-1}$, we can write lists such as $[\vec{x}]$,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   805
$[y+1,\vec{x}]$, etc.  A function is \defn{primitive recursive} if it
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   806
belongs to the least set of functions in $\lst(\nat)\to\nat$ containing
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   807
\begin{itemize}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   808
\item The \defn{successor} function $\SC$, such that $\SC[y,\vec{x}]=y+1$.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   809
\item All \defn{constant} functions $\CONST(k)$, such that
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   810
  $\CONST(k)[\vec{x}]=k$. 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   811
\item All \defn{projection} functions $\PROJ(i)$, such that
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   812
  $\PROJ(i)[\vec{x}]=x_i$ if $0\leq i<n$. 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   813
\item All \defn{compositions} $\COMP(g,[f_0,\ldots,f_{m-1}])$, 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   814
where $g$ and $f_0$, \ldots, $f_{m-1}$ are primitive recursive,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   815
such that
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   816
\[ \COMP(g,[f_0,\ldots,f_{m-1}])[\vec{x}] = 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   817
   g[f_0[\vec{x}],\ldots,f_{m-1}[\vec{x}]]. \] 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   818
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   819
\item All \defn{recursions} $\PREC(f,g)$, where $f$ and $g$ are primitive
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   820
  recursive, such that
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   821
\begin{eqnarray*}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   822
  \PREC(f,g)[0,\vec{x}] & = & f[\vec{x}] \\
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   823
  \PREC(f,g)[y+1,\vec{x}] & = & g[\PREC(f,g)[y,\vec{x}],\, y,\, \vec{x}].
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   824
\end{eqnarray*} 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   825
\end{itemize}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   826
Composition is awkward because it combines not two functions, as is usual,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   827
but $m+1$ functions.  In her proof that Ackermann's function is not
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   828
primitive recursive, Nora Szasz was unable to formalize this definition
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   829
directly~\cite{szasz93}.  So she generalized primitive recursion to
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   830
tuple-valued functions.  This modified the inductive definition such that
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   831
each operation on primitive recursive functions combined just two functions.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   832
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   833
\begin{figure}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   834
\begin{ttbox}
6631
ccae8c659762 changes for new manual.bib
paulson
parents: 6141
diff changeset
   835
Primrec_defs = Main +
ccae8c659762 changes for new manual.bib
paulson
parents: 6141
diff changeset
   836
consts SC :: i
ccae8c659762 changes for new manual.bib
paulson
parents: 6141
diff changeset
   837
 \(\vdots\)
3162
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   838
defs
6631
ccae8c659762 changes for new manual.bib
paulson
parents: 6141
diff changeset
   839
 SC_def    "SC == lam l:list(nat).list_case(0, \%x xs.succ(x), l)"
ccae8c659762 changes for new manual.bib
paulson
parents: 6141
diff changeset
   840
 \(\vdots\)
ccae8c659762 changes for new manual.bib
paulson
parents: 6141
diff changeset
   841
end
ccae8c659762 changes for new manual.bib
paulson
parents: 6141
diff changeset
   842
ccae8c659762 changes for new manual.bib
paulson
parents: 6141
diff changeset
   843
Primrec = Primrec_defs +
ccae8c659762 changes for new manual.bib
paulson
parents: 6141
diff changeset
   844
consts prim_rec :: i
3162
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   845
inductive
6631
ccae8c659762 changes for new manual.bib
paulson
parents: 6141
diff changeset
   846
 domains "primrec" <= "list(nat)->nat"
ccae8c659762 changes for new manual.bib
paulson
parents: 6141
diff changeset
   847
 intrs
ccae8c659762 changes for new manual.bib
paulson
parents: 6141
diff changeset
   848
   SC     "SC : primrec"
ccae8c659762 changes for new manual.bib
paulson
parents: 6141
diff changeset
   849
   CONST  "k: nat ==> CONST(k) : primrec"
ccae8c659762 changes for new manual.bib
paulson
parents: 6141
diff changeset
   850
   PROJ   "i: nat ==> PROJ(i) : primrec"
ccae8c659762 changes for new manual.bib
paulson
parents: 6141
diff changeset
   851
   COMP   "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec"
ccae8c659762 changes for new manual.bib
paulson
parents: 6141
diff changeset
   852
   PREC   "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"
ccae8c659762 changes for new manual.bib
paulson
parents: 6141
diff changeset
   853
 monos       list_mono
ccae8c659762 changes for new manual.bib
paulson
parents: 6141
diff changeset
   854
 con_defs    SC_def, CONST_def, PROJ_def, COMP_def, PREC_def
ccae8c659762 changes for new manual.bib
paulson
parents: 6141
diff changeset
   855
 type_intrs "nat_typechecks @ list.intrs @                      
ccae8c659762 changes for new manual.bib
paulson
parents: 6141
diff changeset
   856
             [lam_type, list_case_type, drop_type, map_type,    
ccae8c659762 changes for new manual.bib
paulson
parents: 6141
diff changeset
   857
              apply_type, rec_type]"
3162
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   858
end
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   859
\end{ttbox}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   860
\hrule
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   861
\caption{Inductive definition of the primitive recursive functions} 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   862
\label{primrec-fig}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   863
\end{figure}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   864
\def\fs{{\it fs}} 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   865
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   866
Szasz was using \textsc{alf}, but Coq and \textsc{hol} would also have
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   867
problems accepting this definition.  Isabelle's package accepts it easily
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   868
since $[f_0,\ldots,f_{m-1}]$ is a list of primitive recursive functions and
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   869
$\lst$ is monotonic.  There are five introduction rules, one for each of the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   870
five forms of primitive recursive function.  Let us examine the one for
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   871
$\COMP$:
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   872
\[ \infer{\COMP(g,\fs)\in\primrec}{g\in\primrec & \fs\in\lst(\primrec)} \]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   873
The induction rule for $\primrec$ has one case for each introduction rule.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   874
Due to the use of $\lst$ as a monotone operator, the composition case has
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   875
an unusual induction hypothesis:
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   876
 \[ \infer*{P(\COMP(g,\fs))}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   877
          {[g\in\primrec & \fs\in\lst(\{z\in\primrec.P(z)\})]_{\fs,g}} 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   878
\]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   879
The hypothesis states that $\fs$ is a list of primitive recursive functions,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   880
each satisfying the induction formula.  Proving the $\COMP$ case typically
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   881
requires structural induction on lists, yielding two subcases: either
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   882
$\fs=\Nil$ or else $\fs=\Cons(f,\fs')$, where $f\in\primrec$, $P(f)$, and
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   883
$\fs'$ is another list of primitive recursive functions satisfying~$P$.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   884
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   885
Figure~\ref{primrec-fig} presents the theory file.  Theory {\tt Primrec}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   886
defines the constants $\SC$, $\CONST$, etc.  These are not constructors of
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   887
a new datatype, but functions over lists of numbers.  Their definitions,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   888
most of which are omitted, consist of routine list programming.  In
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   889
Isabelle/\textsc{zf}, the primitive recursive functions are defined as a subset of
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   890
the function set $\lst(\nat)\to\nat$.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   891
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   892
The Isabelle theory goes on to formalize Ackermann's function and prove
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   893
that it is not primitive recursive, using the induction rule {\tt
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   894
  primrec.induct}.  The proof follows Szasz's excellent account.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   895
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   896
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   897
\section{Datatypes and codatatypes}\label{data-sec}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   898
A (co)datatype definition is a (co)inductive definition with automatically
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   899
defined constructors and a case analysis operator.  The package proves that
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   900
the case operator inverts the constructors and can prove freeness theorems
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   901
involving any pair of constructors.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   902
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   903
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   904
\subsection{Constructors and their domain}\label{univ-sec}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   905
A (co)inductive definition selects a subset of an existing set; a (co)datatype
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   906
definition creates a new set.  The package reduces the latter to the former.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   907
Isabelle/\textsc{zf} supplies sets having strong closure properties to serve
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   908
as domains for (co)inductive definitions.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   909
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   910
Isabelle/\textsc{zf} defines the Cartesian product $A\times
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   911
B$, containing ordered pairs $\pair{a,b}$; it also defines the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   912
disjoint sum $A+B$, containing injections $\Inl(a)\equiv\pair{0,a}$ and
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   913
$\Inr(b)\equiv\pair{1,b}$.  For use below, define the $m$-tuple
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   914
$\pair{x_1,\ldots,x_m}$ to be the empty set~$\emptyset$ if $m=0$, simply $x_1$
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   915
if $m=1$ and $\pair{x_1,\pair{x_2,\ldots,x_m}}$ if $m\geq2$.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   916
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   917
A datatype constructor $\Con(x_1,\ldots,x_m)$ is defined to be
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   918
$h(\pair{x_1,\ldots,x_m})$, where $h$ is composed of $\Inl$ and~$\Inr$.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   919
In a mutually recursive definition, all constructors for the set~$R_i$ have
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   920
the outer form~$h_{in}$, where $h_{in}$ is the injection described
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   921
in~\S\ref{mutual-sec}.  Further nested injections ensure that the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   922
constructors for~$R_i$ are pairwise distinct.  
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   923
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   924
Isabelle/\textsc{zf} defines the set $\univ(A)$, which contains~$A$ and
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   925
furthermore contains $\pair{a,b}$, $\Inl(a)$ and $\Inr(b)$ for $a$,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   926
$b\in\univ(A)$.  In a typical datatype definition with set parameters
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   927
$A_1$, \ldots, $A_k$, a suitable domain for all the recursive sets is
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   928
$\univ(A_1\un\cdots\un A_k)$.  This solves the problem for
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   929
datatypes~\cite[\S4.2]{paulson-set-II}.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   930
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   931
The standard pairs and injections can only yield well-founded
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   932
constructions.  This eases the (manual!) definition of recursive functions
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   933
over datatypes.  But they are unsuitable for codatatypes, which typically
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   934
contain non-well-founded objects.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   935
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   936
To support codatatypes, Isabelle/\textsc{zf} defines a variant notion of
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   937
ordered pair, written~$\pair{a;b}$.  It also defines the corresponding variant
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   938
notion of Cartesian product $A\otimes B$, variant injections $\QInl(a)$
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   939
and~$\QInr(b)$ and variant disjoint sum $A\oplus B$.  Finally it defines the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   940
set $\quniv(A)$, which contains~$A$ and furthermore contains $\pair{a;b}$,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   941
$\QInl(a)$ and $\QInr(b)$ for $a$, $b\in\quniv(A)$.  In a typical codatatype
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   942
definition with set parameters $A_1$, \ldots, $A_k$, a suitable domain is
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   943
$\quniv(A_1\un\cdots\un A_k)$.  Details are published
6631
ccae8c659762 changes for new manual.bib
paulson
parents: 6141
diff changeset
   944
elsewhere~\cite{paulson-mscs}.
3162
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   945
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   946
\subsection{The case analysis operator}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   947
The (co)datatype package automatically defines a case analysis operator,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   948
called {\tt$R$\_case}.  A mutually recursive definition still has only one
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   949
operator, whose name combines those of the recursive sets: it is called
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   950
{\tt$R_1$\_\ldots\_$R_n$\_case}.  The case operator is analogous to those
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   951
for products and sums.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   952
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   953
Datatype definitions employ standard products and sums, whose operators are
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   954
$\split$ and $\case$ and satisfy the equations
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   955
\begin{eqnarray*}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   956
  \split(f,\pair{x,y})  & = &  f(x,y) \\
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   957
  \case(f,g,\Inl(x))    & = &  f(x)   \\
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   958
  \case(f,g,\Inr(y))    & = &  g(y)
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   959
\end{eqnarray*}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   960
Suppose the datatype has $k$ constructors $\Con_1$, \ldots,~$\Con_k$.  Then
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   961
its case operator takes $k+1$ arguments and satisfies an equation for each
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   962
constructor:
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   963
\[ R\hbox{\_case}(f_1,\ldots,f_k, {\tt Con}_i(\vec{x})) = f_i(\vec{x}),
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   964
    \qquad i = 1, \ldots, k
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   965
\]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   966
The case operator's definition takes advantage of Isabelle's representation of
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   967
syntax in the typed $\lambda$-calculus; it could readily be adapted to a
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   968
theorem prover for higher-order logic.  If $f$ and~$g$ have meta-type $i\To i$
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   969
then so do $\split(f)$ and $\case(f,g)$.  This works because $\split$ and
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   970
$\case$ operate on their last argument.  They are easily combined to make
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   971
complex case analysis operators.  For example, $\case(f,\case(g,h))$ performs
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   972
case analysis for $A+(B+C)$; let us verify one of the three equations:
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   973
\[ \case(f,\case(g,h), \Inr(\Inl(b))) = \case(g,h,\Inl(b)) = g(b) \]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   974
Codatatype definitions are treated in precisely the same way.  They express
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   975
case operators using those for the variant products and sums, namely
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   976
$\qsplit$ and~$\qcase$.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   977
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   978
\medskip
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   979
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   980
To see how constructors and the case analysis operator are defined, let us
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   981
examine some examples.  Further details are available
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   982
elsewhere~\cite{paulson-set-II}.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   983
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   984
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   985
\subsection{Example: lists and lazy lists}\label{lists-sec}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   986
Here is a declaration of the datatype of lists, as it might appear in a theory
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   987
file:
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   988
\begin{ttbox} 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   989
consts  list :: i=>i
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   990
datatype "list(A)" = Nil | Cons ("a:A", "l: list(A)")
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   991
\end{ttbox}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   992
And here is a declaration of the codatatype of lazy lists:
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   993
\begin{ttbox}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   994
consts  llist :: i=>i
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   995
codatatype "llist(A)" = LNil | LCons ("a: A", "l: llist(A)")
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   996
\end{ttbox}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   997
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   998
Each form of list has two constructors, one for the empty list and one for
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   999
adding an element to a list.  Each takes a parameter, defining the set of
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1000
lists over a given set~$A$.  Each is automatically given the appropriate
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1001
domain: $\univ(A)$ for $\lst(A)$ and $\quniv(A)$ for $\llist(A)$.  The default
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1002
can be overridden.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1003
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1004
\ifshort
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1005
Now $\lst(A)$ is a datatype and enjoys the usual induction rule.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1006
\else
6631
ccae8c659762 changes for new manual.bib
paulson
parents: 6141
diff changeset
  1007
Since $\lst(A)$ is a datatype, it has a structural induction rule, {\tt
3162
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1008
  list.induct}:
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1009
\[ \infer{P(x)}{x\in\lst(A) & P(\Nil)
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1010
        & \infer*{P(\Cons(a,l))}{[a\in A & l\in\lst(A) & P(l)]_{a,l}} }
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1011
\] 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1012
Induction and freeness yield the law $l\not=\Cons(a,l)$.  To strengthen this,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1013
Isabelle/\textsc{zf} defines the rank of a set and proves that the standard
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1014
pairs and injections have greater rank than their components.  An immediate
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1015
consequence, which justifies structural recursion on lists
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1016
\cite[\S4.3]{paulson-set-II}, is
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1017
\[ \rank(l) < \rank(\Cons(a,l)). \]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1018
\par
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1019
\fi
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1020
But $\llist(A)$ is a codatatype and has no induction rule.  Instead it has
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1021
the coinduction rule shown in \S\ref{coind-sec}.  Since variant pairs and
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1022
injections are monotonic and need not have greater rank than their
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1023
components, fixedpoint operators can create cyclic constructions.  For
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1024
example, the definition
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1025
\[ \lconst(a) \equiv \lfp(\univ(a), \lambda l. \LCons(a,l)) \]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1026
yields $\lconst(a) = \LCons(a,\lconst(a))$.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1027
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1028
\ifshort
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1029
\typeout{****SHORT VERSION}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1030
\typeout{****Omitting discussion of constructors!}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1031
\else
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1032
\medskip
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1033
It may be instructive to examine the definitions of the constructors and
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1034
case operator for $\lst(A)$.  The definitions for $\llist(A)$ are similar.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1035
The list constructors are defined as follows:
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1036
\begin{eqnarray*}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1037
  \Nil       & \equiv & \Inl(\emptyset) \\
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1038
  \Cons(a,l) & \equiv & \Inr(\pair{a,l})
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1039
\end{eqnarray*}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1040
The operator $\lstcase$ performs case analysis on these two alternatives:
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1041
\[ \lstcase(c,h) \equiv \case(\lambda u.c, \split(h)) \]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1042
Let us verify the two equations:
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1043
\begin{eqnarray*}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1044
    \lstcase(c, h, \Nil) & = & 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1045
       \case(\lambda u.c, \split(h), \Inl(\emptyset)) \\
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1046
     & = & (\lambda u.c)(\emptyset) \\
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1047
     & = & c\\[1ex]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1048
    \lstcase(c, h, \Cons(x,y)) & = & 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1049
       \case(\lambda u.c, \split(h), \Inr(\pair{x,y})) \\
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1050
     & = & \split(h, \pair{x,y}) \\
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1051
     & = & h(x,y)
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1052
\end{eqnarray*} 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1053
\fi
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1054
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1055
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1056
\ifshort
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1057
\typeout{****Omitting mutual recursion example!}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1058
\else
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1059
\subsection{Example: mutual recursion}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1060
In mutually recursive trees and forests~\cite[\S4.5]{paulson-set-II}, trees
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1061
have the one constructor $\Tcons$, while forests have the two constructors
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1062
$\Fnil$ and~$\Fcons$:
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1063
\begin{ttbox}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1064
consts  tree, forest, tree_forest    :: i=>i
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1065
datatype "tree(A)"   = Tcons ("a: A",  "f: forest(A)")
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1066
and      "forest(A)" = Fnil  |  Fcons ("t: tree(A)",  "f: forest(A)")
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1067
\end{ttbox}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1068
The three introduction rules define the mutual recursion.  The
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1069
distinguishing feature of this example is its two induction rules.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1070
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1071
The basic induction rule is called {\tt tree\_forest.induct}:
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1072
\[ \infer{P(x)}{x\in\TF(A) & 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1073
     \infer*{P(\Tcons(a,f))}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1074
        {\left[\begin{array}{l} a\in A \\ 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1075
                                f\in\forest(A) \\ P(f)
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1076
               \end{array}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1077
         \right]_{a,f}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1078
     & P(\Fnil)
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1079
     & \infer*{P(\Fcons(t,f))}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1080
        {\left[\begin{array}{l} t\in\tree(A)   \\ P(t) \\
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1081
                                f\in\forest(A) \\ P(f)
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1082
                \end{array}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1083
         \right]_{t,f}} }
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1084
\] 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1085
This rule establishes a single predicate for $\TF(A)$, the union of the
6631
ccae8c659762 changes for new manual.bib
paulson
parents: 6141
diff changeset
  1086
recursive sets.  Although such reasoning can be useful
3162
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1087
\cite[\S4.5]{paulson-set-II}, a proper mutual induction rule should establish
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1088
separate predicates for $\tree(A)$ and $\forest(A)$.  The package calls this
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1089
rule {\tt tree\_forest.mutual\_induct}.  Observe the usage of $P$ and $Q$ in
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1090
the induction hypotheses:
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1091
\[ \infer{(\forall z. z\in\tree(A)\imp P(z)) \conj
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1092
          (\forall z. z\in\forest(A)\imp Q(z))}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1093
     {\infer*{P(\Tcons(a,f))}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1094
        {\left[\begin{array}{l} a\in A \\ 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1095
                                f\in\forest(A) \\ Q(f)
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1096
               \end{array}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1097
         \right]_{a,f}}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1098
     & Q(\Fnil)
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1099
     & \infer*{Q(\Fcons(t,f))}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1100
        {\left[\begin{array}{l} t\in\tree(A)   \\ P(t) \\
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1101
                                f\in\forest(A) \\ Q(f)
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1102
                \end{array}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1103
         \right]_{t,f}} }
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1104
\] 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1105
Elsewhere I describe how to define mutually recursive functions over trees and
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1106
forests \cite[\S4.5]{paulson-set-II}.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1107
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1108
Both forest constructors have the form $\Inr(\cdots)$,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1109
while the tree constructor has the form $\Inl(\cdots)$.  This pattern would
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1110
hold regardless of how many tree or forest constructors there were.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1111
\begin{eqnarray*}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1112
  \Tcons(a,l)  & \equiv & \Inl(\pair{a,l}) \\
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1113
  \Fnil        & \equiv & \Inr(\Inl(\emptyset)) \\
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1114
  \Fcons(a,l)  & \equiv & \Inr(\Inr(\pair{a,l}))
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1115
\end{eqnarray*} 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1116
There is only one case operator; it works on the union of the trees and
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1117
forests:
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1118
\[ {\tt tree\_forest\_case}(f,c,g) \equiv 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1119
    \case(\split(f),\, \case(\lambda u.c, \split(g))) 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1120
\]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1121
\fi
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1122
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1123
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1124
\subsection{Example: a four-constructor datatype}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1125
A bigger datatype will illustrate some efficiency 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1126
refinements.  It has four constructors $\Con_0$, \ldots, $\Con_3$, with the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1127
corresponding arities.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1128
\begin{ttbox}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1129
consts    data :: [i,i] => i
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1130
datatype  "data(A,B)" = Con0
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1131
                      | Con1 ("a: A")
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1132
                      | Con2 ("a: A", "b: B")
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1133
                      | Con3 ("a: A", "b: B", "d: data(A,B)")
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1134
\end{ttbox}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1135
Because this datatype has two set parameters, $A$ and~$B$, the package
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1136
automatically supplies $\univ(A\un B)$ as its domain.  The structural
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1137
induction rule has four minor premises, one per constructor, and only the last
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1138
has an induction hypothesis.  (Details are left to the reader.)
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1139
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1140
The constructors are defined by the equations
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1141
\begin{eqnarray*}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1142
  \Con_0         & \equiv & \Inl(\Inl(\emptyset)) \\
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1143
  \Con_1(a)      & \equiv & \Inl(\Inr(a)) \\
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1144
  \Con_2(a,b)    & \equiv & \Inr(\Inl(\pair{a,b})) \\
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1145
  \Con_3(a,b,c)  & \equiv & \Inr(\Inr(\pair{a,b,c})).
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1146
\end{eqnarray*} 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1147
The case analysis operator is
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1148
\[ {\tt data\_case}(f_0,f_1,f_2,f_3) \equiv 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1149
    \case(\begin{array}[t]{@{}l}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1150
          \case(\lambda u.f_0,\; f_1),\, \\
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1151
          \case(\split(f_2),\; \split(\lambda v.\split(f_3(v)))) )
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1152
   \end{array} 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1153
\]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1154
This may look cryptic, but the case equations are trivial to verify.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1155
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1156
In the constructor definitions, the injections are balanced.  A more naive
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1157
approach is to define $\Con_3(a,b,c)$ as $\Inr(\Inr(\Inr(\pair{a,b,c})))$;
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1158
instead, each constructor has two injections.  The difference here is small.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1159
But the \textsc{zf} examples include a 60-element enumeration type, where each
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1160
constructor has 5 or~6 injections.  The naive approach would require 1 to~59
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1161
injections; the definitions would be quadratic in size.  It is like the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1162
advantage of binary notation over unary.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1163
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1164
The result structure contains the case operator and constructor definitions as
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1165
the theorem list \verb|con_defs|. It contains the case equations, such as 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1166
\[ {\tt data\_case}(f_0,f_1,f_2,f_3,\Con_3(a,b,c)) = f_3(a,b,c), \]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1167
as the theorem list \verb|case_eqns|.  There is one equation per constructor.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1168
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1169
\subsection{Proving freeness theorems}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1170
There are two kinds of freeness theorems:
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1171
\begin{itemize}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1172
\item \defn{injectiveness} theorems, such as
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1173
\[ \Con_2(a,b) = \Con_2(a',b') \bimp a=a' \conj b=b' \]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1174
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1175
\item \defn{distinctness} theorems, such as
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1176
\[ \Con_1(a) \not= \Con_2(a',b')  \]
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1177
\end{itemize}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1178
Since the number of such theorems is quadratic in the number of constructors,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1179
the package does not attempt to prove them all.  Instead it returns tools for
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1180
proving desired theorems --- either manually or during
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1181
simplification or classical reasoning.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1182
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1183
The theorem list \verb|free_iffs| enables the simplifier to perform freeness
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1184
reasoning.  This works by incremental unfolding of constructors that appear in
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1185
equations.  The theorem list contains logical equivalences such as
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1186
\begin{eqnarray*}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1187
  \Con_0=c      & \bimp &  c=\Inl(\Inl(\emptyset))     \\
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1188
  \Con_1(a)=c   & \bimp &  c=\Inl(\Inr(a))             \\
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1189
                & \vdots &                             \\
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1190
  \Inl(a)=\Inl(b)   & \bimp &  a=b                     \\
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1191
  \Inl(a)=\Inr(b)   & \bimp &  {\tt False}             \\
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1192
  \pair{a,b} = \pair{a',b'} & \bimp & a=a' \conj b=b'
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1193
\end{eqnarray*}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1194
For example, these rewrite $\Con_1(a)=\Con_1(b)$ to $a=b$ in four steps.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1195
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1196
The theorem list \verb|free_SEs| enables the classical
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1197
reasoner to perform similar replacements.  It consists of elimination rules
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1198
to replace $\Con_0=c$ by $c=\Inl(\Inl(\emptyset))$ and so forth, in the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1199
assumptions.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1200
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1201
Such incremental unfolding combines freeness reasoning with other proof
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1202
steps.  It has the unfortunate side-effect of unfolding definitions of
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1203
constructors in contexts such as $\exists x.\Con_1(a)=x$, where they should
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1204
be left alone.  Calling the Isabelle tactic {\tt fold\_tac con\_defs}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1205
restores the defined constants.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1206
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1207
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1208
\section{Related work}\label{related}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1209
The use of least fixedpoints to express inductive definitions seems
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1210
obvious.  Why, then, has this technique so seldom been implemented?
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1211
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1212
Most automated logics can only express inductive definitions by asserting
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1213
axioms.  Little would be left of Boyer and Moore's logic~\cite{bm79} if their
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1214
shell principle were removed.  With \textsc{alf} the situation is more
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1215
complex; earlier versions of Martin-L\"of's type theory could (using
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1216
wellordering types) express datatype definitions, but the version underlying
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1217
\textsc{alf} requires new rules for each definition~\cite{dybjer91}.  With Coq
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1218
the situation is subtler still; its underlying Calculus of Constructions can
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1219
express inductive definitions~\cite{huet88}, but cannot quite handle datatype
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1220
definitions~\cite{paulin-tlca}.  It seems that researchers tried hard to
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1221
circumvent these problems before finally extending the Calculus with rule
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1222
schemes for strictly positive operators.  Recently Gim{\'e}nez has extended
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1223
the Calculus of Constructions with inductive and coinductive
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1224
types~\cite{gimenez-codifying}, with mechanized support in Coq.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1225
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1226
Higher-order logic can express inductive definitions through quantification
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1227
over unary predicates.  The following formula expresses that~$i$ belongs to the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1228
least set containing~0 and closed under~$\succ$:
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1229
\[ \forall P. P(0)\conj (\forall x.P(x)\imp P(\succ(x))) \imp P(i) \] 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1230
This technique can be used to prove the Knaster-Tarski theorem, which (in its
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1231
general form) is little used in the Cambridge \textsc{hol} system.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1232
Melham~\cite{melham89} describes the development.  The natural numbers are
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1233
defined as shown above, but lists are defined as functions over the natural
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1234
numbers.  Unlabelled trees are defined using G\"odel numbering; a labelled
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1235
tree consists of an unlabelled tree paired with a list of labels.  Melham's
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1236
datatype package expresses the user's datatypes in terms of labelled trees.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1237
It has been highly successful, but a fixedpoint approach might have yielded
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1238
greater power with less effort.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1239
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1240
Elsa Gunter~\cite{gunter-trees} reports an ongoing project to generalize the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1241
Cambridge \textsc{hol} system with mutual recursion and infinitely-branching
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1242
trees.  She retains many features of Melham's approach.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1243
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1244
Melham's inductive definition package~\cite{camilleri92} also uses
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1245
quantification over predicates.  But instead of formalizing the notion of
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1246
monotone function, it requires definitions to consist of finitary rules, a
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1247
syntactic form that excludes many monotone inductive definitions.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1248
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1249
\textsc{pvs}~\cite{pvs-language} is another proof assistant based on
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1250
higher-order logic.  It supports both inductive definitions and datatypes,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1251
apparently by asserting axioms.  Datatypes may not be iterated in general, but
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1252
may use recursion over the built-in $\lst$ type.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1253
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1254
The earliest use of least fixedpoints is probably Robin Milner's.  Brian
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1255
Monahan extended this package considerably~\cite{monahan84}, as did I in
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1256
unpublished work.\footnote{The datatype package described in my \textsc{lcf}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1257
  book~\cite{paulson87} does {\it not\/} make definitions, but merely asserts
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1258
  axioms.} \textsc{lcf} is a first-order logic of domain theory; the relevant
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1259
fixedpoint theorem is not Knaster-Tarski but concerns fixedpoints of
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1260
continuous functions over domains.  \textsc{lcf} is too weak to express
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1261
recursive predicates.  The Isabelle package might be the first to be based on
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1262
the Knaster-Tarski theorem.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1263
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1264
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1265
\section{Conclusions and future work}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1266
Higher-order logic and set theory are both powerful enough to express
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1267
inductive definitions.  A growing number of theorem provers implement one
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1268
of these~\cite{IMPS,saaltink-fme}.  The easiest sort of inductive
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1269
definition package to write is one that asserts new axioms, not one that
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1270
makes definitions and proves theorems about them.  But asserting axioms
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1271
could introduce unsoundness.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1272
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1273
The fixedpoint approach makes it fairly easy to implement a package for
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1274
(co)in\-duc\-tive definitions that does not assert axioms.  It is efficient:
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1275
it processes most definitions in seconds and even a 60-constructor datatype
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1276
requires only a few minutes.  It is also simple: The first working version took
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1277
under a week to code, consisting of under 1100 lines (35K bytes) of Standard
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1278
\textsc{ml}.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1279
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1280
In set theory, care is needed to ensure that the inductive definition yields
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1281
a set (rather than a proper class).  This problem is inherent to set theory,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1282
whether or not the Knaster-Tarski theorem is employed.  We must exhibit a
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1283
bounding set (called a domain above).  For inductive definitions, this is
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1284
often trivial.  For datatype definitions, I have had to formalize much set
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1285
theory.  To justify infinitely-branching datatype definitions, I have had to
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1286
develop a theory of cardinal arithmetic~\cite{paulson-gr}, such as the theorem
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1287
that if $\kappa$ is an infinite cardinal and $|X(\alpha)| \le \kappa$ for all
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1288
$\alpha<\kappa$ then $|\union\sb{\alpha<\kappa} X(\alpha)| \le \kappa$.  
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1289
The need for such efforts is not a drawback of the fixedpoint approach, for
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1290
the alternative is to take such definitions on faith.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1291
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1292
Care is also needed to ensure that the greatest fixedpoint really yields a
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1293
coinductive definition.  In set theory, standard pairs admit only well-founded
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1294
constructions.  Aczel's anti-foundation axiom~\cite{aczel88} could be used to
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1295
get non-well-founded objects, but it does not seem easy to mechanize.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1296
Isabelle/\textsc{zf} instead uses a variant notion of ordered pairing, which
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1297
can be generalized to a variant notion of function.  Elsewhere I have
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1298
proved that this simple approach works (yielding final coalgebras) for a broad
6631
ccae8c659762 changes for new manual.bib
paulson
parents: 6141
diff changeset
  1299
class of definitions~\cite{paulson-mscs}.
3162
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1300
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1301
Several large studies make heavy use of inductive definitions.  L\"otzbeyer
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1302
and Sandner have formalized two chapters of a semantics book~\cite{winskel93},
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1303
proving the equivalence between the operational and denotational semantics of
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1304
a simple imperative language.  A single theory file contains three datatype
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1305
definitions (of arithmetic expressions, boolean expressions and commands) and
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1306
three inductive definitions (the corresponding operational rules).  Using
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1307
different techniques, Nipkow~\cite{nipkow-CR} and Rasmussen~\cite{rasmussen95}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1308
have both proved the Church-Rosser theorem; inductive definitions specify
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1309
several reduction relations on $\lambda$-terms.  Recently, I have applied
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1310
inductive definitions to the analysis of cryptographic
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1311
protocols~\cite{paulson-markt}. 
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1312
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1313
To demonstrate coinductive definitions, Frost~\cite{frost95} has proved the
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1314
consistency of the dynamic and static semantics for a small functional
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1315
language.  The example is due to Milner and Tofte~\cite{milner-coind}.  It
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1316
concerns an extended correspondence relation, which is defined coinductively.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1317
A codatatype definition specifies values and value environments in mutual
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1318
recursion.  Non-well-founded values represent recursive functions.  Value
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1319
environments are variant functions from variables into values.  This one key
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1320
definition uses most of the package's novel features.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1321
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1322
The approach is not restricted to set theory.  It should be suitable for any
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1323
logic that has some notion of set and the Knaster-Tarski theorem.  I have
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1324
ported the (co)inductive definition package from Isabelle/\textsc{zf} to
6631
ccae8c659762 changes for new manual.bib
paulson
parents: 6141
diff changeset
  1325
Isabelle/\textsc{hol} (higher-order logic).  
3162
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1326
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1327
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1328
\begin{footnotesize}
6637
57abed64dc14 pdf setup;
wenzelm
parents: 6631
diff changeset
  1329
\bibliographystyle{plain}
6631
ccae8c659762 changes for new manual.bib
paulson
parents: 6141
diff changeset
  1330
\bibliography{../manual}
3162
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1331
\end{footnotesize}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1332
%%%%%\doendnotes
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1333
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
  1334
\end{document}