doc-src/ind-defs.tex
author lcp
Fri, 19 Nov 1993 11:31:10 +0100
changeset 130 c035b6b9eafc
parent 103 30bd42401ab2
child 179 ceb948cefb93
permissions -rw-r--r--
Many edits suggested by Grundy & Thompson
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
     1
\documentstyle[12pt,a4,proof,lcp,alltt,amssymbols]{article}
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
     2
%CADE version should use 11pt and the Springer style
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
     3
\newif\ifCADE
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
     4
\CADEfalse
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
     5
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
     6
\title{A Fixedpoint Approach to Implementing (Co)Inductive
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
     7
   Definitions\thanks{Jim Grundy and Simon Thompson made detailed comments on
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
     8
   a draft.  Research funded by the SERC (grants GR/G53279,
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
     9
    GR/H40570) and by the ESPRIT Basic Research Action 6453 `Types'.}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    10
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    11
\author{{\em Lawrence C. Paulson}\\ 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    12
        Computer Laboratory, University of Cambridge}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    13
\date{\today} 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    14
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    15
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    16
\def\picture #1 by #2 (#3){% pictures: width by height (name)
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    17
  \message{Picture #3}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    18
  \vbox to #2{\hrule width #1 height 0pt depth 0pt
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    19
    \vfill \special{picture #3}}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    20
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    21
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    22
\newcommand\sbs{\subseteq}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    23
\newcommand\List[1]{\lbrakk#1\rbrakk}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    24
\let\To=\Rightarrow
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    25
\newcommand\Var[1]{{?\!#1}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    26
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    27
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    28
%%%\newcommand\Pow{{\tt Pow}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    29
\let\pow=\wp
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    30
\newcommand\RepFun{{\tt RepFun}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    31
\newcommand\pair[1]{\langle#1\rangle}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    32
\newcommand\cons{{\tt cons}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    33
\def\succ{{\tt succ}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    34
\newcommand\split{{\tt split}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    35
\newcommand\fst{{\tt fst}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    36
\newcommand\snd{{\tt snd}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    37
\newcommand\converse{{\tt converse}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    38
\newcommand\domain{{\tt domain}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    39
\newcommand\range{{\tt range}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    40
\newcommand\field{{\tt field}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    41
\newcommand\bndmono{\hbox{\tt bnd\_mono}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    42
\newcommand\lfp{{\tt lfp}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    43
\newcommand\gfp{{\tt gfp}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    44
\newcommand\id{{\tt id}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    45
\newcommand\trans{{\tt trans}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    46
\newcommand\wf{{\tt wf}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    47
\newcommand\wfrec{\hbox{\tt wfrec}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    48
\newcommand\nat{{\tt nat}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    49
\newcommand\natcase{\hbox{\tt nat\_case}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    50
\newcommand\transrec{{\tt transrec}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    51
\newcommand\rank{{\tt rank}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    52
\newcommand\univ{{\tt univ}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    53
\newcommand\Vrec{{\tt Vrec}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    54
\newcommand\Inl{{\tt Inl}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    55
\newcommand\Inr{{\tt Inr}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    56
\newcommand\case{{\tt case}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    57
\newcommand\lst{{\tt list}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    58
\newcommand\Nil{{\tt Nil}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    59
\newcommand\Cons{{\tt Cons}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    60
\newcommand\lstcase{\hbox{\tt list\_case}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    61
\newcommand\lstrec{\hbox{\tt list\_rec}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    62
\newcommand\length{{\tt length}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    63
\newcommand\listn{{\tt listn}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    64
\newcommand\acc{{\tt acc}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    65
\newcommand\primrec{{\tt primrec}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    66
\newcommand\SC{{\tt SC}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    67
\newcommand\CONST{{\tt CONST}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    68
\newcommand\PROJ{{\tt PROJ}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    69
\newcommand\COMP{{\tt COMP}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    70
\newcommand\PREC{{\tt PREC}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    71
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    72
\newcommand\quniv{{\tt quniv}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    73
\newcommand\llist{{\tt llist}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    74
\newcommand\LNil{{\tt LNil}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    75
\newcommand\LCons{{\tt LCons}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    76
\newcommand\lconst{{\tt lconst}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    77
\newcommand\lleq{{\tt lleq}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    78
\newcommand\map{{\tt map}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    79
\newcommand\term{{\tt term}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    80
\newcommand\Apply{{\tt Apply}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    81
\newcommand\termcase{{\tt term\_case}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    82
\newcommand\rev{{\tt rev}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    83
\newcommand\reflect{{\tt reflect}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    84
\newcommand\tree{{\tt tree}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    85
\newcommand\forest{{\tt forest}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    86
\newcommand\Part{{\tt Part}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    87
\newcommand\TF{{\tt tree\_forest}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    88
\newcommand\Tcons{{\tt Tcons}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    89
\newcommand\Fcons{{\tt Fcons}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    90
\newcommand\Fnil{{\tt Fnil}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    91
\newcommand\TFcase{\hbox{\tt TF\_case}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    92
\newcommand\Fin{{\tt Fin}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    93
\newcommand\QInl{{\tt QInl}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    94
\newcommand\QInr{{\tt QInr}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    95
\newcommand\qsplit{{\tt qsplit}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    96
\newcommand\qcase{{\tt qcase}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    97
\newcommand\Con{{\tt Con}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    98
\newcommand\data{{\tt data}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
    99
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   100
\sloppy
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   101
\binperiod     %%%treat . like a binary operator
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   102
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   103
\begin{document}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   104
\pagestyle{empty}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   105
\begin{titlepage}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   106
\maketitle 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   107
\begin{abstract}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   108
  Several theorem provers provide commands for formalizing recursive
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   109
  datatypes and/or inductively defined sets.  This paper presents a new
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   110
  approach, based on fixedpoint definitions.  It is unusually general:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   111
  it admits all monotone inductive definitions.  It is conceptually simple,
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   112
  which has allowed the easy implementation of mutual recursion and other
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   113
  conveniences.  It also handles coinductive definitions: simply replace
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   114
  the least fixedpoint by a greatest fixedpoint.  This represents the first
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   115
  automated support for coinductive definitions.
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   116
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   117
  The method has been implemented in Isabelle's formalization of ZF set
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   118
  theory.  It should
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   119
  be applicable to any logic in which the Knaster-Tarski Theorem can be
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   120
  proved.  The paper briefly describes a method of formalizing
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   121
  non-well-founded data structures in standard ZF set theory.
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   122
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   123
  Examples include lists of $n$ elements, the accessible part of a relation
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   124
  and the set of primitive recursive functions.  One example of a
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   125
  coinductive definition is bisimulations for lazy lists.  \ifCADE\else
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   126
  Recursive datatypes are examined in detail, as well as one example of a
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   127
  {\bf codatatype}: lazy lists.  The appendices are simple user's manuals
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   128
  for this Isabelle/ZF package.\fi
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   129
\end{abstract}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   130
%
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   131
\begin{center} Copyright \copyright{} \number\year{} by Lawrence C. Paulson
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   132
\end{center}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   133
\thispagestyle{empty} 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   134
\end{titlepage}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   135
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   136
\tableofcontents
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   137
\cleardoublepage
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   138
\pagenumbering{arabic}\pagestyle{headings}
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   139
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   140
\section{Introduction}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   141
Several theorem provers provide commands for formalizing recursive data
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   142
structures, like lists and trees.  Examples include Boyer and Moore's shell
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   143
principle~\cite{bm79} and Melham's recursive type package for the HOL
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   144
system~\cite{melham89}.  Such data structures are called {\bf datatypes}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   145
below, by analogy with {\tt datatype} definitions in Standard~ML\@.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   146
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   147
A datatype is but one example of an {\bf inductive definition}.  This
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   148
specifies the least set closed under given rules~\cite{aczel77}.  The
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   149
collection of theorems in a logic is inductively defined.  A structural
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   150
operational semantics~\cite{hennessy90} is an inductive definition of a
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   151
reduction or evaluation relation on programs.  A few theorem provers
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   152
provide commands for formalizing inductive definitions; these include
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   153
Coq~\cite{paulin92} and again the HOL system~\cite{camilleri92}.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   154
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   155
The dual notion is that of a {\bf coinductive definition}.  This specifies
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   156
the greatest set closed under given rules.  Important examples include
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   157
using bisimulation relations to formalize equivalence of
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   158
processes~\cite{milner89} or lazy functional programs~\cite{abramsky90}.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   159
Other examples include lazy lists and other infinite data structures; these
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   160
are called {\bf codatatypes} below.
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   161
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   162
Most existing implementations of datatype and inductive definitions accept
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   163
an artificially narrow class of inputs, and are not easily extended.  The
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   164
shell principle and Coq's inductive definition rules are built into the
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   165
underlying logic.  Melham's packages derive datatypes and inductive
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   166
definitions from specialized constructions in higher-order logic.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   167
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   168
This paper describes a package based on a fixedpoint approach.  Least
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   169
fixedpoints yield inductive definitions; greatest fixedpoints yield
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   170
coinductive definitions.  The package is uniquely powerful:
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   171
\begin{itemize}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   172
\item It accepts the largest natural class of inductive definitions, namely
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   173
  all that are provably monotone.
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   174
\item It accepts a wide class of datatype definitions.
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   175
\item It handles coinductive and codatatype definitions.  Most of
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   176
  the discussion below applies equally to inductive and coinductive
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   177
  definitions, and most of the code is shared.  To my knowledge, this is
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   178
  the only package supporting coinductive definitions.
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   179
\item Definitions may be mutually recursive.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   180
\end{itemize}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   181
The package is implemented in Isabelle~\cite{isabelle-intro}, using ZF set
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   182
theory \cite{paulson-set-I,paulson-set-II}.  However, the fixedpoint
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   183
approach is independent of Isabelle.  The recursion equations are specified
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   184
as introduction rules for the mutually recursive sets.  The package
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   185
transforms these rules into a mapping over sets, and attempts to prove that
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   186
the mapping is monotonic and well-typed.  If successful, the package
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   187
makes fixedpoint definitions and proves the introduction, elimination and
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   188
(co)induction rules.  The package consists of several Standard ML
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   189
functors~\cite{paulson91}; it accepts its argument and returns its result
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   190
as ML structures.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   191
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   192
Most datatype packages equip the new datatype with some means of expressing
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   193
recursive functions.  This is the main thing lacking from my package.  Its
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   194
fixedpoint operators define recursive sets, not recursive functions.  But
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   195
the Isabelle/ZF theory provides well-founded recursion and other logical
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   196
tools to simplify this task~\cite{paulson-set-II}.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   197
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   198
{\bf Outline.}  \S2 briefly introduces the least and greatest fixedpoint
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   199
operators.  \S3 discusses the form of introduction rules, mutual recursion and
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   200
other points common to inductive and coinductive definitions.  \S4 discusses
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   201
induction and coinduction rules separately.  \S5 presents several examples,
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   202
including a coinductive definition.  \S6 describes datatype definitions, while
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   203
\S7 draws brief conclusions.  \ifCADE\else The appendices are simple user's
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   204
manuals for this Isabelle/ZF package.\fi
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   205
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   206
Most of the definitions and theorems shown below have been generated by the
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   207
package.  I have renamed some variables to improve readability.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   208
 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   209
\section{Fixedpoint operators}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   210
In set theory, the least and greatest fixedpoint operators are defined as
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   211
follows:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   212
\begin{eqnarray*}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   213
   \lfp(D,h)  & \equiv & \inter\{X\sbs D. h(X)\sbs X\} \\
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   214
   \gfp(D,h)  & \equiv & \union\{X\sbs D. X\sbs h(X)\}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   215
\end{eqnarray*}   
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   216
Let $D$ be a set.  Say that $h$ is {\bf bounded by}~$D$ if $h(D)\sbs D$, and
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   217
{\bf monotone below~$D$} if
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   218
$h(A)\sbs h(B)$ for all $A$ and $B$ such that $A\sbs B\sbs D$.  If $h$ is
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   219
bounded by~$D$ and monotone then both operators yield fixedpoints:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   220
\begin{eqnarray*}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   221
   \lfp(D,h)  & = & h(\lfp(D,h)) \\
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   222
   \gfp(D,h)  & = & h(\gfp(D,h)) 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   223
\end{eqnarray*}   
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   224
These equations are instances of the Knaster-Tarski theorem, which states
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   225
that every monotonic function over a complete lattice has a
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   226
fixedpoint~\cite{davey&priestley}.  It is obvious from their definitions
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   227
that  $\lfp$ must be the least fixedpoint, and $\gfp$ the greatest.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   228
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   229
This fixedpoint theory is simple.  The Knaster-Tarski theorem is easy to
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   230
prove.  Showing monotonicity of~$h$ is trivial, in typical cases.  We must
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   231
also exhibit a bounding set~$D$ for~$h$.  Sometimes this is trivial, as
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   232
when a set of ``theorems'' is (co)inductively defined over some previously
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   233
existing set of ``formulae.''  But defining the bounding set for
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   234
(co)datatype definitions requires some effort; see~\S\ref{univ-sec} below.
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   235
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   236
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   237
\section{Elements of an inductive or coinductive definition}\label{basic-sec}
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   238
Consider a (co)inductive definition of the sets $R_1$, \ldots,~$R_n$, in
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   239
mutual recursion.  They will be constructed from previously existing sets
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   240
$D_1$, \ldots,~$D_n$, respectively, which are called their {\bf domains}. 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   241
The construction yields not $R_i\sbs D_i$ but $R_i\sbs D_1+\cdots+D_n$, where
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   242
$R_i$ is contained in the image of~$D_i$ under an
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   243
injection.  Reasons for this are discussed
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   244
elsewhere~\cite[\S4.5]{paulson-set-II}.
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   245
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   246
The definition may involve arbitrary parameters $\vec{p}=p_1$,
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   247
\ldots,~$p_k$.  Each recursive set then has the form $R_i(\vec{p})$.  The
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   248
parameters must be identical every time they occur within a definition.  This
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   249
would appear to be a serious restriction compared with other systems such as
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   250
Coq~\cite{paulin92}.  For instance, we cannot define the lists of
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   251
$n$ elements as the set $\listn(A,n)$ using rules where the parameter~$n$
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   252
varies.  \S\ref{listn-sec} describes how to express this set using the
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   253
inductive definition package.
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   254
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   255
To avoid clutter below, the recursive sets are shown as simply $R_i$
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   256
instead of $R_i(\vec{p})$.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   257
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   258
\subsection{The form of the introduction rules}\label{intro-sec}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   259
The body of the definition consists of the desired introduction rules,
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   260
specified as strings.  The conclusion of each rule must have the form $t\in
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   261
R_i$, where $t$ is any term.  Premises typically have the same form, but
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   262
they can have the more general form $t\in M(R_i)$ or express arbitrary
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   263
side-conditions.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   264
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   265
The premise $t\in M(R_i)$ is permitted if $M$ is a monotonic operator on
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   266
sets, satisfying the rule 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   267
\[ \infer{M(A)\sbs M(B)}{A\sbs B} \]
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   268
The user must supply the package with monotonicity rules for all such premises.
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   269
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   270
Because any monotonic $M$ may appear in premises, the criteria for an
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   271
acceptable definition is semantic rather than syntactic.  A suitable choice
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   272
of~$M$ and~$t$ can express a lot.  The powerset operator $\pow$ is
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   273
monotone, and the premise $t\in\pow(R)$ expresses $t\sbs R$; see
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   274
\S\ref{acc-sec} for an example.  The `list of' operator is monotone, as is
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   275
easily proved by induction.  The premise $t\in\lst(R)$ avoids having to
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   276
encode the effect of~$\lst(R)$ using mutual recursion; see \S\ref{primrec-sec}
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   277
and also my earlier paper~\cite[\S4.4]{paulson-set-II}.
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   278
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   279
Introduction rules may also contain {\bf side-conditions}.  These are
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   280
premises consisting of arbitrary formulae not mentioning the recursive
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   281
sets. Side-conditions typically involve type-checking.  One example is the
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   282
premise $a\in A$ in the following rule from the definition of lists:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   283
\[ \infer{\Cons(a,l)\in\lst(A)}{a\in A & l\in\lst(A)} \]
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   284
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   285
\subsection{The fixedpoint definitions}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   286
The package translates the list of desired introduction rules into a fixedpoint
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   287
definition.  Consider, as a running example, the finite set operator
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   288
$\Fin(A)$: the set of all finite subsets of~$A$.  It can be
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   289
defined as the least set closed under the rules
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   290
\[  \emptyset\in\Fin(A)  \qquad 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   291
    \infer{\{a\}\un b\in\Fin(A)}{a\in A & b\in\Fin(A)} 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   292
\]
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   293
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   294
The domain in a (co)inductive definition must be some existing set closed
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   295
under the rules.  A suitable domain for $\Fin(A)$ is $\pow(A)$, the set of all
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   296
subsets of~$A$.  The package generates the definition
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   297
\begin{eqnarray*}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   298
  \Fin(A) & \equiv &  \lfp(\pow(A), \;
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   299
  \begin{array}[t]{r@{\,}l}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   300
      \lambda X. \{z\in\pow(A). & z=\emptyset \disj{} \\
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   301
                  &(\exists a\,b. z=\{a\}\un b\conj a\in A\conj b\in X)\})
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   302
  \end{array}
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   303
\end{eqnarray*} 
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   304
The contribution of each rule to the definition of $\Fin(A)$ should be
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   305
obvious.  A coinductive definition is similar but uses $\gfp$ instead
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   306
of~$\lfp$.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   307
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   308
The package must prove that the fixedpoint operator is applied to a
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   309
monotonic function.  If the introduction rules have the form described
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   310
above, and if the package is supplied a monotonicity theorem for every
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   311
$t\in M(R_i)$ premise, then this proof is trivial.\footnote{Due to the
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   312
  presence of logical connectives in the fixedpoint's body, the
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   313
  monotonicity proof requires some unusual rules.  These state that the
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   314
  connectives $\conj$, $\disj$ and $\exists$ preserve monotonicity with respect
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   315
  to the partial ordering on unary predicates given by $P\sqsubseteq Q$ if and
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   316
  only if $\forall x.P(x)\imp Q(x)$.}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   317
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   318
The result structure contains the definitions of the recursive sets as a theorem
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   319
list called {\tt defs}.  It also contains, as the theorem {\tt unfold}, a
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   320
fixedpoint equation such as 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   321
\begin{eqnarray*}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   322
  \Fin(A) & = &
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   323
  \begin{array}[t]{r@{\,}l}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   324
     \{z\in\pow(A). & z=\emptyset \disj{} \\
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   325
             &(\exists a\,b. z=\{a\}\un b\conj a\in A\conj b\in \Fin(A))\}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   326
  \end{array}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   327
\end{eqnarray*}
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   328
It also contains, as the theorem {\tt dom\_subset}, an inclusion such as 
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   329
$\Fin(A)\sbs\pow(A)$.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   330
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   331
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   332
\subsection{Mutual recursion} \label{mutual-sec}
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   333
In a mutually recursive definition, the domain of the fixedpoint construction
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   334
is the disjoint sum of the domain~$D_i$ of each~$R_i$, for $i=1$,
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   335
\ldots,~$n$.  The package uses the injections of the
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   336
binary disjoint sum, typically $\Inl$ and~$\Inr$, to express injections
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   337
$h_{1n}$, \ldots, $h_{nn}$ for the $n$-ary disjoint sum $D_1+\cdots+D_n$.
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   338
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   339
As discussed elsewhere \cite[\S4.5]{paulson-set-II}, Isabelle/ZF defines the
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   340
operator $\Part$ to support mutual recursion.  The set $\Part(A,h)$
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   341
contains those elements of~$A$ having the form~$h(z)$:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   342
\begin{eqnarray*}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   343
   \Part(A,h)  & \equiv & \{x\in A. \exists z. x=h(z)\}.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   344
\end{eqnarray*}   
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   345
For mutually recursive sets $R_1$, \ldots,~$R_n$ with
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   346
$n>1$, the package makes $n+1$ definitions.  The first defines a set $R$ using
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   347
a fixedpoint operator. The remaining $n$ definitions have the form
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   348
\begin{eqnarray*}
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   349
  R_i & \equiv & \Part(R,h_{in}), \qquad i=1,\ldots, n.
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   350
\end{eqnarray*} 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   351
It follows that $R=R_1\un\cdots\un R_n$, where the $R_i$ are pairwise disjoint.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   352
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   353
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   354
\subsection{Proving the introduction rules}
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   355
The user supplies the package with the desired form of the introduction
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   356
rules.  Once it has derived the theorem {\tt unfold}, it attempts
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   357
to prove those rules.  From the user's point of view, this is the
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   358
trickiest stage; the proofs often fail.  The task is to show that the domain 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   359
$D_1+\cdots+D_n$ of the combined set $R_1\un\cdots\un R_n$ is
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   360
closed under all the introduction rules.  This essentially involves replacing
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   361
each~$R_i$ by $D_1+\cdots+D_n$ in each of the introduction rules and
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   362
attempting to prove the result.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   363
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   364
Consider the $\Fin(A)$ example.  After substituting $\pow(A)$ for $\Fin(A)$
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   365
in the rules, the package must prove
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   366
\[  \emptyset\in\pow(A)  \qquad 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   367
    \infer{\{a\}\un b\in\pow(A)}{a\in A & b\in\pow(A)} 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   368
\]
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   369
Such proofs can be regarded as type-checking the definition.  The user
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   370
supplies the package with type-checking rules to apply.  Usually these are
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   371
general purpose rules from the ZF theory.  They could however be rules
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   372
specifically proved for a particular inductive definition; sometimes this is
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   373
the easiest way to get the definition through!
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   374
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   375
The result structure contains the introduction rules as the theorem list {\tt
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   376
intrs}.
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   377
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   378
\subsection{The elimination rule}
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   379
The elimination rule, called {\tt elim}, performs case analysis: a
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   380
case for each introduction rule.  The elimination rule
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   381
for $\Fin(A)$ is
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   382
\[ \infer{Q}{x\in\Fin(A) & \infer*{Q}{[x=\emptyset]}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   383
                 & \infer*{Q}{[x=\{a\}\un b & a\in A &b\in\Fin(A)]_{a,b}} }
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   384
\]
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   385
This rule states that if $x\in\Fin(A)$ then either $x=\emptyset$ or else
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   386
$x=\{a\}\un b$ for some $a\in A$ and $b\in\Fin(A)$; it is a simple consequence
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   387
of {\tt unfold}.
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   388
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   389
\ifCADE\typeout{****Omitting mk_cases from CADE version!}\else
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   390
The package also returns a function {\tt mk\_cases}, for generating simplified
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   391
instances of the elimination rule.  However, {\tt mk\_cases} only works for
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   392
datatypes and for inductive definitions involving datatypes, such as an
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   393
inductively defined relation between lists.  It instantiates {\tt elim}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   394
with a user-supplied term, then simplifies the cases using the freeness of
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   395
the underlying datatype.
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   396
See \S\ref{mkcases} for an example.
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   397
\fi
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   398
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   399
\section{Induction and coinduction rules}
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   400
Here we must consider inductive and coinductive definitions separately.
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   401
For an inductive definition, the package returns an induction rule derived
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   402
directly from the properties of least fixedpoints, as well as a modified
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   403
rule for mutual recursion and inductively defined relations.  For a
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   404
coinductive definition, the package returns a basic coinduction rule.
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   405
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   406
\subsection{The basic induction rule}\label{basic-ind-sec}
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   407
The basic rule, called {\tt induct}, is appropriate in most situations.
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   408
For inductive definitions, it is strong rule induction~\cite{camilleri92}; for
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   409
datatype definitions (see below), it is just structural induction.  
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   410
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   411
The induction rule for an inductively defined set~$R$ has the following form.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   412
The major premise is $x\in R$.  There is a minor premise for each
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   413
introduction rule:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   414
\begin{itemize}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   415
\item If the introduction rule concludes $t\in R_i$, then the minor premise
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   416
is~$P(t)$.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   417
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   418
\item The minor premise's eigenvariables are precisely the introduction
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   419
rule's free variables that are not parameters of~$R$.  For instance, the
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   420
eigenvariables in the $\Fin(A)$ rule below are $a$ and $b$, but not~$A$.
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   421
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   422
\item If the introduction rule has a premise $t\in R_i$, then the minor
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   423
premise discharges the assumption $t\in R_i$ and the induction
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   424
hypothesis~$P(t)$.  If the introduction rule has a premise $t\in M(R_i)$
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   425
then the minor premise discharges the single assumption
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   426
\[ t\in M(\{z\in R_i. P(z)\}). \] 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   427
Because $M$ is monotonic, this assumption implies $t\in M(R_i)$.  The
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   428
occurrence of $P$ gives the effect of an induction hypothesis, which may be
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   429
exploited by appealing to properties of~$M$.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   430
\end{itemize}
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   431
The induction rule for $\Fin(A)$ resembles the elimination rule shown above,
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   432
but includes an induction hypothesis:
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   433
\[ \infer{P(x)}{x\in\Fin(A) & P(\emptyset)
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   434
        & \infer*{P(\{a\}\un b)}{[a\in A & b\in\Fin(A) & P(b)]_{a,b}} }
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   435
\] 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   436
Stronger induction rules often suggest themselves.  In the case of
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   437
$\Fin(A)$, the Isabelle/ZF theory proceeds to derive a rule whose third
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   438
premise discharges the extra assumption $a\not\in b$.  Most special induction
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   439
rules must be proved manually, but the package proves a rule for mutual
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   440
induction and inductive relations.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   441
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   442
\subsection{Mutual induction}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   443
The mutual induction rule is called {\tt
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   444
mutual\_induct}.  It differs from the basic rule in several respects:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   445
\begin{itemize}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   446
\item Instead of a single predicate~$P$, it uses $n$ predicates $P_1$,
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   447
\ldots,~$P_n$: one for each recursive set.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   448
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   449
\item There is no major premise such as $x\in R_i$.  Instead, the conclusion
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   450
refers to all the recursive sets:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   451
\[ (\forall z.z\in R_1\imp P_1(z))\conj\cdots\conj
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   452
   (\forall z.z\in R_n\imp P_n(z))
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   453
\]
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   454
Proving the premises simultaneously establishes $P_i(z)$ for $z\in
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   455
R_i$ and $i=1$, \ldots,~$n$.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   456
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   457
\item If the domain of some $R_i$ is the Cartesian product
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   458
$A_1\times\cdots\times A_m$, then the corresponding predicate $P_i$ takes $m$
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   459
arguments and the corresponding conjunct of the conclusion is
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   460
\[ (\forall z_1\ldots z_m.\pair{z_1,\ldots,z_m}\in R_i\imp P_i(z_1,\ldots,z_m))
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   461
\]
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   462
\end{itemize}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   463
The last point above simplifies reasoning about inductively defined
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   464
relations.  It eliminates the need to express properties of $z_1$,
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   465
\ldots,~$z_m$ as properties of the tuple $\pair{z_1,\ldots,z_m}$.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   466
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   467
\subsection{Coinduction}\label{coind-sec}
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   468
A coinductive definition yields a primitive coinduction rule, with no
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   469
refinements such as those for the induction rules.  (Experience may suggest
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   470
refinements later.)  Consider the codatatype of lazy lists as an example.  For
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   471
suitable definitions of $\LNil$ and $\LCons$, lazy lists may be defined as the
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   472
greatest fixedpoint satisfying the rules
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   473
\[  \LNil\in\llist(A)  \qquad 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   474
    \infer[(-)]{\LCons(a,l)\in\llist(A)}{a\in A & l\in\llist(A)}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   475
\]
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   476
The $(-)$ tag stresses that this is a coinductive definition.  A suitable
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   477
domain for $\llist(A)$ is $\quniv(A)$, a set closed under variant forms of
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   478
sum and product for representing infinite data structures
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   479
(see~\S\ref{univ-sec}).  Coinductive definitions use these variant sums and
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   480
products.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   481
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   482
The package derives an {\tt unfold} theorem similar to that for $\Fin(A)$. 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   483
Then it proves the theorem {\tt co\_induct}, which expresses that $\llist(A)$
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   484
is the greatest solution to this equation contained in $\quniv(A)$:
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   485
\[ \infer{x\in\llist(A)}{x\in X & X\sbs \quniv(A) &
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   486
    \infer*{z=\LNil\disj \bigl(\exists a\,l.\,
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   487
      \begin{array}[t]{@{}l}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   488
        z=\LCons(a,l) \conj a\in A \conj{}\\
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   489
        l\in X\un\llist(A) \bigr)
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   490
      \end{array}  }{[z\in X]_z}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   491
\]
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   492
This rule complements the introduction rules; it provides a means of showing
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   493
$x\in\llist(A)$ when $x$ is infinite.  For instance, if $x=\LCons(0,x)$ then
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   494
applying the rule with $X=\{x\}$ proves $x\in\llist(\nat)$.  Here $\nat$
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   495
is the set of natural numbers.
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   496
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   497
Having $X\un\llist(A)$ instead of simply $X$ in the third premise above
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   498
represents a slight strengthening of the greatest fixedpoint property.  I
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   499
discuss several forms of coinduction rules elsewhere~\cite{paulson-coind}.
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   500
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   501
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   502
\section{Examples of inductive and coinductive definitions}\label{ind-eg-sec}
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   503
This section presents several examples: the finite set operator,
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   504
lists of $n$ elements, bisimulations on lazy lists, the well-founded part
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   505
of a relation, and the primitive recursive functions.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   506
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   507
\subsection{The finite set operator}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   508
The definition of finite sets has been discussed extensively above.  Here
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   509
is the corresponding ML invocation (note that $\cons(a,b)$ abbreviates
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   510
$\{a\}\un b$ in Isabelle/ZF):
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   511
\begin{ttbox}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   512
structure Fin = Inductive_Fun
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   513
 (val thy = Arith.thy addconsts [(["Fin"],"i=>i")];
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   514
  val rec_doms = [("Fin","Pow(A)")];
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   515
  val sintrs = 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   516
          ["0 : Fin(A)",
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   517
           "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"];
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   518
  val monos = [];
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   519
  val con_defs = [];
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   520
  val type_intrs = [empty_subsetI, cons_subsetI, PowI];
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   521
  val type_elims = [make_elim PowD]);
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   522
\end{ttbox}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   523
The parent theory is obtained from {\tt Arith.thy} by adding the unary
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   524
function symbol~$\Fin$.  Its domain is specified as $\pow(A)$, where $A$ is
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   525
the parameter appearing in the introduction rules.  For type-checking, the
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   526
package supplies the introduction rules:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   527
\[ \emptyset\sbs A              \qquad
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   528
   \infer{\{a\}\un B\sbs C}{a\in C & B\sbs C}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   529
\]
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   530
A further introduction rule and an elimination rule express the two
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   531
directions of the equivalence $A\in\pow(B)\bimp A\sbs B$.  Type-checking
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   532
involves mostly introduction rules.  When the package returns, we can refer
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   533
to the $\Fin(A)$ introduction rules as {\tt Fin.intrs}, the induction rule
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   534
as {\tt Fin.induct}, and so forth.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   535
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   536
\subsection{Lists of $n$ elements}\label{listn-sec}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   537
This has become a standard example in the
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   538
literature.  Following Paulin-Mohring~\cite{paulin92}, we could attempt to
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   539
define a new datatype $\listn(A,n)$, for lists of length~$n$, as an $n$-indexed
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   540
family of sets.  But her introduction rules
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   541
\[ {\tt Niln}\in\listn(A,0)  \qquad
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   542
   \infer{{\tt Consn}(n,a,l)\in\listn(A,\succ(n))}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   543
         {n\in\nat & a\in A & l\in\listn(A,n)}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   544
\]
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   545
are not acceptable to the inductive definition package:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   546
$\listn$ occurs with three different parameter lists in the definition.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   547
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   548
\begin{figure}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   549
\begin{small}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   550
\begin{verbatim}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   551
structure ListN = Inductive_Fun
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   552
 (val thy = ListFn.thy addconsts [(["listn"],"i=>i")];
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   553
  val rec_doms = [("listn", "nat*list(A)")];
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   554
  val sintrs = 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   555
      ["<0,Nil> : listn(A)",
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   556
       "[| a: A;  <n,l> : listn(A) |] ==> 
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   557
        <succ(n), Cons(a,l)> : listn(A)"];
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   558
  val monos = [];
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   559
  val con_defs = [];
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   560
  val type_intrs = nat_typechecks @ List.intrs @ [SigmaI];
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   561
  val type_elims = [SigmaE2]);
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   562
\end{verbatim}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   563
\end{small}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   564
\hrule
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   565
\caption{Defining lists of $n$ elements} \label{listn-fig}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   566
\end{figure} 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   567
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   568
There is an obvious way of handling this particular example, which may suggest
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   569
a general approach to varying parameters.  Here, we can take advantage of an
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   570
existing datatype definition of $\lst(A)$, with constructors $\Nil$
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   571
and~$\Cons$.  Then incorporate the number~$n$ into the inductive set itself,
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   572
defining $\listn(A)$ as a relation.  It consists of pairs $\pair{n,l}$ such
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   573
that $n\in\nat$ and~$l\in\lst(A)$ and $l$ has length~$n$.  In fact,
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   574
$\listn(A)$ turns out to be the converse of the length function on~$\lst(A)$. 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   575
The Isabelle/ZF introduction rules are
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   576
\[ \pair{0,\Nil}\in\listn(A)  \qquad
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   577
   \infer{\pair{\succ(n),\Cons(a,l)}\in\listn(A)}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   578
         {a\in A & \pair{n,l}\in\listn(A)}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   579
\]
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   580
Figure~\ref{listn-fig} presents the ML invocation.  A theory of lists,
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   581
extended with a declaration of $\listn$, is the parent theory.  The domain
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   582
is specified as $\nat\times\lst(A)$.  The type-checking rules include those
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   583
for 0, $\succ$, $\Nil$ and $\Cons$.  Because $\listn(A)$ is a set of pairs,
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   584
type-checking also requires introduction and elimination rules to express
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   585
both directions of the equivalence $\pair{a,b}\in A\times B \bimp a\in A
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   586
\conj b\in B$. 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   587
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   588
The package returns introduction, elimination and induction rules for
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   589
$\listn$.  The basic induction rule, {\tt ListN.induct}, is
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   590
\[ \infer{P(x)}{x\in\listn(A) & P(\pair{0,\Nil}) &
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   591
             \infer*{P(\pair{\succ(n),\Cons(a,l)})}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   592
                {[a\in A & \pair{n,l}\in\listn(A) & P(\pair{n,l})]_{a,l,n}}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   593
\]
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   594
This rule requires the induction formula to be a 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   595
unary property of pairs,~$P(\pair{n,l})$.  The alternative rule, {\tt
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   596
ListN.mutual\_induct}, uses a binary property instead:
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   597
\[ \infer{\forall n\,l. \pair{n,l}\in\listn(A) \imp P(n,l)}
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   598
         {P(0,\Nil) &
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   599
          \infer*{P(\succ(n),\Cons(a,l))}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   600
                {[a\in A & \pair{n,l}\in\listn(A) & P(n,l)]_{a,l,n}}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   601
\]
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   602
It is now a simple matter to prove theorems about $\listn(A)$, such as
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   603
\[ \forall l\in\lst(A). \pair{\length(l),\, l}\in\listn(A) \]
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   604
\[ \listn(A)``\{n\} = \{l\in\lst(A). \length(l)=n\} \]
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   605
This latter result --- here $r``X$ denotes the image of $X$ under $r$
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   606
--- asserts that the inductive definition agrees with the obvious notion of
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   607
$n$-element list.  
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   608
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   609
Unlike in Coq, the definition does not declare a new datatype.  A `list of
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   610
$n$ elements' really is a list and is subject to list operators such
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   611
as append (concatenation).  For example, a trivial induction on
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   612
$\pair{m,l}\in\listn(A)$ yields
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   613
\[ \infer{\pair{m\mathbin{+} m,\, l@l'}\in\listn(A)}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   614
         {\pair{m,l}\in\listn(A) & \pair{m',l'}\in\listn(A)} 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   615
\]
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   616
where $+$ here denotes addition on the natural numbers and @ denotes append.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   617
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   618
\ifCADE\typeout{****Omitting mk_cases from CADE version!}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   619
\else
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   620
\subsection{A demonstration of {\tt mk\_cases}}\label{mkcases}
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   621
The elimination rule, {\tt ListN.elim}, is cumbersome:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   622
\[ \infer{Q}{x\in\listn(A) & 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   623
          \infer*{Q}{[x = \pair{0,\Nil}]} &
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   624
          \infer*{Q}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   625
             {\left[\begin{array}{l}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   626
               x = \pair{\succ(n),\Cons(a,l)} \\
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   627
               a\in A \\
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   628
               \pair{n,l}\in\listn(A)
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   629
               \end{array} \right]_{a,l,n}}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   630
\]
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   631
The ML function {\tt ListN.mk\_cases} generates simplified instances of this
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   632
rule.  It works by freeness reasoning on the list constructors: $\Cons$ is
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   633
injective and $\Cons(a,l)\not=\Nil$. If $x$ is $\pair{i,\Nil}$ or
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   634
$\pair{i,\Cons(a,l)}$ then {\tt ListN.mk\_cases} deduces the corresponding
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   635
form of~$i$.  For example,
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   636
\begin{ttbox}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   637
ListN.mk_cases List.con_defs "<i,Cons(a,l)> : listn(A)"
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   638
\end{ttbox}
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   639
yields a rule with only two premises:
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   640
\[ \infer{Q}{\pair{i, \Cons(a,l)}\in\listn(A) & 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   641
          \infer*{Q}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   642
             {\left[\begin{array}{l}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   643
               i = \succ(n) \\ a\in A \\ \pair{n,l}\in\listn(A)
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   644
               \end{array} \right]_{n}}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   645
\]
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   646
The package also has built-in rules for freeness reasoning about $0$
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   647
and~$\succ$.  So if $x$ is $\pair{0,l}$ or $\pair{\succ(i),l}$, then {\tt
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   648
ListN.mk\_cases} can similarly deduce the corresponding form of~$l$. 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   649
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   650
The function {\tt mk\_cases} is also useful with datatype definitions
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   651
themselves.  The version from the definition of lists, namely {\tt
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   652
List.mk\_cases}, can prove the rule
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   653
\[ \infer{Q}{\Cons(a,l)\in\lst(A) & 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   654
                 & \infer*{Q}{[a\in A &l\in\lst(A)]} }
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   655
\]
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   656
The most important uses of {\tt mk\_cases} concern inductive definitions of
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   657
evaluation relations.  Then {\tt mk\_cases} supports case analysis on
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   658
possible evaluations, for example to prove that evaluation is
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   659
functional.
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   660
\fi  %CADE
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   661
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   662
\subsection{A coinductive definition: bisimulations on lazy lists}
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   663
This example anticipates the definition of the codatatype $\llist(A)$, which
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   664
consists of finite and infinite lists over~$A$.  Its constructors are $\LNil$
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   665
and
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   666
$\LCons$, satisfying the introduction rules shown in~\S\ref{coind-sec}.  
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   667
Because $\llist(A)$ is defined as a greatest fixedpoint and uses the variant
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   668
pairing and injection operators, it contains non-well-founded elements such as
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   669
solutions to $\LCons(a,l)=l$.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   670
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   671
The next step in the development of lazy lists is to define a coinduction
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   672
principle for proving equalities.  This is done by showing that the equality
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   673
relation on lazy lists is the greatest fixedpoint of some monotonic
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   674
operation.  The usual approach~\cite{pitts94} is to define some notion of 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   675
bisimulation for lazy lists, define equivalence to be the greatest
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   676
bisimulation, and finally to prove that two lazy lists are equivalent if and
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   677
only if they are equal.  The coinduction rule for equivalence then yields a
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   678
coinduction principle for equalities.
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   679
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   680
A binary relation $R$ on lazy lists is a {\bf bisimulation} provided $R\sbs
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   681
R^+$, where $R^+$ is the relation
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   682
\[ \{\pair{\LNil,\LNil}\} \un 
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   683
   \{\pair{\LCons(a,l),\LCons(a,l')} . a\in A \conj \pair{l,l'}\in R\}.
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   684
\]
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   685
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   686
A pair of lazy lists are {\bf equivalent} if they belong to some bisimulation. 
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   687
Equivalence can be coinductively defined as the greatest fixedpoint for the
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   688
introduction rules
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   689
\[  \pair{\LNil,\LNil} \in\lleq(A)  \qquad 
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   690
    \infer[(-)]{\pair{\LCons(a,l),\LCons(a,l')} \in\lleq(A)}
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   691
          {a\in A & \pair{l,l'}\in \lleq(A)}
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   692
\]
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   693
To make this coinductive definition, we invoke \verb|CoInductive_Fun|:
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   694
\begin{ttbox}
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   695
structure LList_Eq = CoInductive_Fun
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   696
(val thy = LList.thy addconsts [(["lleq"],"i=>i")];
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   697
 val rec_doms = [("lleq", "llist(A) * llist(A)")];
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   698
 val sintrs = 
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   699
   ["<LNil, LNil> : lleq(A)",
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   700
    "[| a:A; <l,l'>: lleq(A) |] ==> 
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   701
     <LCons(a,l), LCons(a,l')>: lleq(A)"];
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   702
 val monos = [];
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   703
 val con_defs = [];
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   704
 val type_intrs = LList.intrs @ [SigmaI];
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   705
 val type_elims = [SigmaE2]);
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   706
\end{ttbox}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   707
Again, {\tt addconsts} declares a constant for $\lleq$ in the parent theory. 
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   708
The domain of $\lleq(A)$ is $\llist(A)\times\llist(A)$.  The type-checking
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   709
rules include the introduction rules for lazy lists as well as rules
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   710
for both directions of the equivalence
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   711
$\pair{a,b}\in A\times B \bimp a\in A \conj b\in B$.
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   712
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   713
The package returns the introduction rules and the elimination rule, as
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   714
usual.  But instead of induction rules, it returns a coinduction rule.
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   715
The rule is too big to display in the usual notation; its conclusion is
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   716
$x\in\lleq(A)$ and its premises are $x\in X$, 
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   717
${X\sbs\llist(A)\times\llist(A)}$ and
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   718
\[ \infer*{z=\pair{\LNil,\LNil}\disj \bigl(\exists a\,l\,l'.\,
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   719
      \begin{array}[t]{@{}l}
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   720
        z=\pair{\LCons(a,l),\LCons(a,l')} \conj a\in A \conj{}\\
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   721
        \pair{l,l'}\in X\un\lleq(A) \bigr)
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   722
      \end{array}  }{[z\in X]_z}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   723
\]
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   724
Thus if $x\in X$, where $X$ is a bisimulation contained in the
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   725
domain of $\lleq(A)$, then $x\in\lleq(A)$.  It is easy to show that
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   726
$\lleq(A)$ is reflexive: the equality relation is a bisimulation.  And
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   727
$\lleq(A)$ is symmetric: its converse is a bisimulation.  But showing that
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   728
$\lleq(A)$ coincides with the equality relation takes some work.
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   729
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   730
\subsection{The accessible part of a relation}\label{acc-sec}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   731
Let $\prec$ be a binary relation on~$D$; in short, $(\prec)\sbs D\times D$.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   732
The {\bf accessible} or {\bf well-founded} part of~$\prec$, written
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   733
$\acc(\prec)$, is essentially that subset of~$D$ for which $\prec$ admits
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   734
no infinite decreasing chains~\cite{aczel77}.  Formally, $\acc(\prec)$ is
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   735
inductively defined to be the least set that contains $a$ if it contains
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   736
all $\prec$-predecessors of~$a$, for $a\in D$.  Thus we need an
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   737
introduction rule of the form 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   738
\[ \infer{a\in\acc(\prec)}{\forall y.y\prec a\imp y\in\acc(\prec)} \]
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   739
Paulin-Mohring treats this example in Coq~\cite{paulin92}, but it causes
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   740
difficulties for other systems.  Its premise does not conform to 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   741
the structure of introduction rules for HOL's inductive definition
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   742
package~\cite{camilleri92}.  It is also unacceptable to Isabelle package
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   743
(\S\ref{intro-sec}), but fortunately can be transformed into the acceptable
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   744
form $t\in M(R)$.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   745
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   746
The powerset operator is monotonic, and $t\in\pow(R)$ is equivalent to
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   747
$t\sbs R$.  This in turn is equivalent to $\forall y\in t. y\in R$.  To
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   748
express $\forall y.y\prec a\imp y\in\acc(\prec)$ we need only find a
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   749
term~$t$ such that $y\in t$ if and only if $y\prec a$.  A suitable $t$ is
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   750
the inverse image of~$\{a\}$ under~$\prec$.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   751
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   752
The ML invocation below follows this approach.  Here $r$ is~$\prec$ and
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   753
$\field(r)$ refers to~$D$, the domain of $\acc(r)$.  (The field of a
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   754
relation is the union of its domain and range.)  Finally
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   755
$r^{-}``\{a\}$ denotes the inverse image of~$\{a\}$ under~$r$.  The package is
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   756
supplied the theorem {\tt Pow\_mono}, which asserts that $\pow$ is monotonic.
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   757
\begin{ttbox}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   758
structure Acc = Inductive_Fun
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   759
 (val thy = WF.thy addconsts [(["acc"],"i=>i")];
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   760
  val rec_doms = [("acc", "field(r)")];
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   761
  val sintrs = 
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   762
      ["[| r-``\{a\}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"];
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   763
  val monos = [Pow_mono];
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   764
  val con_defs = [];
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   765
  val type_intrs = [];
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   766
  val type_elims = []);
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   767
\end{ttbox}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   768
The Isabelle theory proceeds to prove facts about $\acc(\prec)$.  For
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   769
instance, $\prec$ is well-founded if and only if its field is contained in
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   770
$\acc(\prec)$.  
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   771
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   772
As mentioned in~\S\ref{basic-ind-sec}, a premise of the form $t\in M(R)$
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   773
gives rise to an unusual induction hypothesis.  Let us examine the
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   774
induction rule, {\tt Acc.induct}:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   775
\[ \infer{P(x)}{x\in\acc(r) &
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   776
     \infer*{P(a)}{[r^{-}``\{a\}\in\pow(\{z\in\acc(r).P(z)\}) & 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   777
                   a\in\field(r)]_a}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   778
\]
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   779
The strange induction hypothesis is equivalent to
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   780
$\forall y. \pair{y,a}\in r\imp y\in\acc(r)\conj P(y)$.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   781
Therefore the rule expresses well-founded induction on the accessible part
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   782
of~$\prec$.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   783
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   784
The use of inverse image is not essential.  The Isabelle package can accept
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   785
introduction rules with arbitrary premises of the form $\forall
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   786
\vec{y}.P(\vec{y})\imp f(\vec{y})\in R$.  The premise can be expressed
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   787
equivalently as 
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   788
\[ \{z\in D. P(\vec{y}) \conj z=f(\vec{y})\} \in \pow(R) \] 
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   789
provided $f(\vec{y})\in D$ for all $\vec{y}$ such that~$P(\vec{y})$.  The
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   790
following section demonstrates another use of the premise $t\in M(R)$,
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   791
where $M=\lst$. 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   792
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   793
\subsection{The primitive recursive functions}\label{primrec-sec}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   794
The primitive recursive functions are traditionally defined inductively, as
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   795
a subset of the functions over the natural numbers.  One difficulty is that
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   796
functions of all arities are taken together, but this is easily
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   797
circumvented by regarding them as functions on lists.  Another difficulty,
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   798
the notion of composition, is less easily circumvented.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   799
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   800
Here is a more precise definition.  Letting $\vec{x}$ abbreviate
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   801
$x_0,\ldots,x_{n-1}$, we can write lists such as $[\vec{x}]$,
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   802
$[y+1,\vec{x}]$, etc.  A function is {\bf primitive recursive} if it
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   803
belongs to the least set of functions in $\lst(\nat)\to\nat$ containing
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   804
\begin{itemize}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   805
\item The {\bf successor} function $\SC$, such that $\SC[y,\vec{x}]=y+1$.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   806
\item All {\bf constant} functions $\CONST(k)$, such that
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   807
  $\CONST(k)[\vec{x}]=k$. 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   808
\item All {\bf projection} functions $\PROJ(i)$, such that
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   809
  $\PROJ(i)[\vec{x}]=x_i$ if $0\leq i<n$. 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   810
\item All {\bf compositions} $\COMP(g,[f_0,\ldots,f_{m-1}])$, 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   811
where $g$ and $f_0$, \ldots, $f_{m-1}$ are primitive recursive,
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   812
such that
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   813
\begin{eqnarray*}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   814
  \COMP(g,[f_0,\ldots,f_{m-1}])[\vec{x}] & = & 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   815
  g[f_0[\vec{x}],\ldots,f_{m-1}[\vec{x}]].
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   816
\end{eqnarray*} 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   817
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   818
\item All {\bf recursions} $\PREC(f,g)$, where $f$ and $g$ are primitive
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   819
  recursive, such that
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   820
\begin{eqnarray*}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   821
  \PREC(f,g)[0,\vec{x}] & = & f[\vec{x}] \\
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   822
  \PREC(f,g)[y+1,\vec{x}] & = & g[\PREC(f,g)[y,\vec{x}],\, y,\, \vec{x}].
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   823
\end{eqnarray*} 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   824
\end{itemize}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   825
Composition is awkward because it combines not two functions, as is usual,
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   826
but $m+1$ functions.  In her proof that Ackermann's function is not
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   827
primitive recursive, Nora Szasz was unable to formalize this definition
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   828
directly~\cite{szasz93}.  So she generalized primitive recursion to
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   829
tuple-valued functions.  This modified the inductive definition such that
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   830
each operation on primitive recursive functions combined just two functions.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   831
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   832
\begin{figure}
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   833
\begin{small}\begin{verbatim}
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   834
structure Primrec = Inductive_Fun
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   835
 (val thy = Primrec0.thy;
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   836
  val rec_doms = [("primrec", "list(nat)->nat")];
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   837
  val ext = None;
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   838
  val sintrs = 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   839
      ["SC : primrec",
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   840
       "k: nat ==> CONST(k) : primrec",
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   841
       "i: nat ==> PROJ(i) : primrec",
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   842
       "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec",
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   843
       "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"];
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   844
  val monos = [list_mono];
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   845
  val con_defs = [SC_def,CONST_def,PROJ_def,COMP_def,PREC_def];
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   846
  val type_intrs = pr0_typechecks;
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   847
  val type_elims = []);
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   848
\end{verbatim}\end{small}
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   849
\hrule
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   850
\caption{Inductive definition of the primitive recursive functions} 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   851
\label{primrec-fig}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   852
\end{figure}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   853
\def\fs{{\it fs}} 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   854
Szasz was using ALF, but Coq and HOL would also have problems accepting
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   855
this definition.  Isabelle's package accepts it easily since
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   856
$[f_0,\ldots,f_{m-1}]$ is a list of primitive recursive functions and
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   857
$\lst$ is monotonic.  There are five introduction rules, one for each of
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   858
the five forms of primitive recursive function.  Note the one for $\COMP$:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   859
\[ \infer{\COMP(g,\fs)\in\primrec}{g\in\primrec & \fs\in\lst(\primrec)} \]
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   860
The induction rule for $\primrec$ has one case for each introduction rule.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   861
Due to the use of $\lst$ as a monotone operator, the composition case has
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   862
an unusual induction hypothesis:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   863
 \[ \infer*{P(\COMP(g,\fs))}
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   864
          {[g\in\primrec & \fs\in\lst(\{z\in\primrec.P(z)\})]_{\fs,g}} \]
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   865
The hypothesis states that $\fs$ is a list of primitive recursive functions
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   866
satisfying the induction formula.  Proving the $\COMP$ case typically requires
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   867
structural induction on lists, yielding two subcases: either $\fs=\Nil$ or
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   868
else $\fs=\Cons(f,\fs')$, where $f\in\primrec$, $P(f)$, and $\fs'$ is
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   869
another list of primitive recursive functions satisfying~$P$.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   870
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   871
Figure~\ref{primrec-fig} presents the ML invocation.  Theory {\tt
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   872
  Primrec0.thy} defines the constants $\SC$, etc.; their definitions
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   873
consist of routine list programming and are omitted.  The Isabelle theory
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   874
goes on to formalize Ackermann's function and prove that it is not
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   875
primitive recursive, using the induction rule {\tt Primrec.induct}.  The
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   876
proof follows Szasz's excellent account.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   877
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   878
ALF and Coq treat inductive definitions as datatypes, with a new
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   879
constructor for each introduction rule.  This forced Szasz to define a
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   880
small programming language for the primitive recursive functions, and then
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   881
define their semantics.  But the Isabelle/ZF formulation defines the
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   882
primitive recursive functions directly as a subset of the function set
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   883
$\lst(\nat)\to\nat$.  This saves a step and conforms better to mathematical
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   884
tradition.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   885
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   886
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   887
\section{Datatypes and codatatypes}\label{data-sec}
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   888
A (co)datatype definition is a (co)inductive definition with automatically
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   889
defined constructors and a case analysis operator.  The package proves that the
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   890
case operator inverts the constructors, and can also prove freeness theorems
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   891
involving any pair of constructors.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   892
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   893
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   894
\subsection{Constructors and their domain}\label{univ-sec}
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   895
Conceptually, our two forms of definition are distinct: a (co)inductive
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   896
definition selects a subset of an existing set, but a (co)datatype
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   897
definition creates a new set.  But the package reduces the latter to the
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   898
former.  A set having strong closure properties must serve as the domain
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   899
of the (co)inductive definition.  Constructing this set requires some
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   900
theoretical effort.  Consider first datatypes and then codatatypes.
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   901
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   902
Isabelle/ZF defines the standard notion of Cartesian product $A\times B$,
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   903
containing ordered pairs $\pair{a,b}$.  Now the $m$-tuple
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   904
$\pair{x_1,\ldots\,x_m}$ is the empty set~$\emptyset$ if $m=0$, simply
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   905
$x_1$ if $m=1$, and $\pair{x_1,\pair{x_2,\ldots\,x_m}}$ if $m\geq2$.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   906
Isabelle/ZF also defines the disjoint sum $A+B$, containing injections
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   907
$\Inl(a)\equiv\pair{0,a}$ and $\Inr(b)\equiv\pair{1,b}$.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   908
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   909
A datatype constructor $\Con(x_1,\ldots\,x_m)$ is defined to be
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   910
$h(\pair{x_1,\ldots\,x_m})$, where $h$ is composed of $\Inl$ and~$\Inr$.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   911
In a mutually recursive definition, all constructors for the set~$R_i$ have
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   912
the outer form~$h_{in}$, where $h_{in}$ is the injection described
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   913
in~\S\ref{mutual-sec}.  Further nested injections ensure that the
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   914
constructors for~$R_i$ are pairwise distinct.  
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   915
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   916
Isabelle/ZF defines the set $\univ(A)$, which contains~$A$ and
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   917
furthermore contains $\pair{a,b}$, $\Inl(a)$ and $\Inr(b)$ for $a$,
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   918
$b\in\univ(A)$.  In a typical datatype definition with set parameters
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   919
$A_1$, \ldots, $A_k$, a suitable domain for all the recursive sets is
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   920
$\univ(A_1\un\cdots\un A_k)$.  This solves the problem for
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   921
datatypes~\cite[\S4.2]{paulson-set-II}.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   922
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   923
The standard pairs and injections can only yield well-founded
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   924
constructions.  This eases the (manual!) definition of recursive functions
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   925
over datatypes.  But they are unsuitable for codatatypes, which typically
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   926
contain non-well-founded objects.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   927
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   928
To support codatatypes, Isabelle/ZF defines a variant notion of ordered
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   929
pair, written~$\pair{a;b}$.  It also defines the corresponding variant
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   930
notion of Cartesian product $A\otimes B$, variant injections $\QInl(a)$
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   931
and~$\QInr(b)$, and variant disjoint sum $A\oplus B$.  Finally it defines
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   932
the set $\quniv(A)$, which contains~$A$ and furthermore contains
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   933
$\pair{a;b}$, $\QInl(a)$ and $\QInr(b)$ for $a$, $b\in\quniv(A)$.  In a
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   934
typical codatatype definition with set parameters $A_1$, \ldots, $A_k$, a
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   935
suitable domain is $\quniv(A_1\un\cdots\un A_k)$.  This approach using
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   936
standard ZF set theory\footnote{No reference is available.  Variant pairs
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   937
  are defined by $\pair{a;b}\equiv (a+b) \equiv (\{0\}\times a) \un
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   938
  (\{1\}\times b)$, where $\times$ is the Cartesian product for standard
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   939
  ordered pairs.  Now
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   940
  $\pair{a;b}$ is injective and monotonic in its two arguments.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   941
  Non-well-founded constructions, such as infinite lists, are constructed
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   942
  as least fixedpoints; the bounding set typically has the form
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   943
  $\univ(a_1\un\cdots\un a_k)$, where $a_1$, \ldots, $a_k$ are specified
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   944
  elements of the construction.}
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   945
is an alternative to adopting Aczel's Anti-Foundation
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   946
Axiom~\cite{aczel88}.
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   947
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   948
\subsection{The case analysis operator}
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   949
The (co)datatype package automatically defines a case analysis operator,
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   950
called {\tt$R$\_case}.  A mutually recursive definition still has only
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   951
one operator, called {\tt$R_1$\_\ldots\_$R_n$\_case}.  The case operator is
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   952
analogous to those for products and sums.  
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   953
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   954
Datatype definitions employ standard products and sums, whose operators are
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   955
$\split$ and $\case$ and satisfy the equations
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   956
\begin{eqnarray*}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   957
  \split(f,\pair{x,y})  & = &  f(x,y) \\
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   958
  \case(f,g,\Inl(x))    & = &  f(x)   \\
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   959
  \case(f,g,\Inr(y))    & = &  g(y)
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   960
\end{eqnarray*}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   961
Suppose the datatype has $k$ constructors $\Con_1$, \ldots,~$\Con_k$.  Then
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   962
its case operator takes $k+1$ arguments and satisfies an equation for each
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   963
constructor:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   964
\begin{eqnarray*}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   965
  R\hbox{\_case}(f_1,\ldots,f_k, {\tt Con}_i(\vec{x})) & = & f_i(\vec{x}),
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   966
    \qquad i = 1, \ldots, k
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   967
\end{eqnarray*}
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   968
The case operator's definition takes advantage of Isabelle's representation
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   969
of syntax in the typed $\lambda$-calculus; it could readily be adapted to a
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   970
theorem prover for higher-order logic.  If $f$ and~$g$ have meta-type
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   971
$i\To i$ then so do $\split(f)$ and
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   972
$\case(f,g)$.  This works because $\split$ and $\case$ operate on their last
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   973
argument.  They are easily combined to make complex case analysis
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   974
operators.  Here are two examples:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   975
\begin{itemize}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   976
\item $\split(\lambda x.\split(f(x)))$ performs case analysis for
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   977
$A\times (B\times C)$, as is easily verified:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   978
\begin{eqnarray*}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   979
  \split(\lambda x.\split(f(x)), \pair{a,b,c}) 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   980
    & = & (\lambda x.\split(f(x))(a,\pair{b,c}) \\
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   981
    & = & \split(f(a), \pair{b,c}) \\
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   982
    & = & f(a,b,c)
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   983
\end{eqnarray*}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   984
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   985
\item $\case(f,\case(g,h))$ performs case analysis for $A+(B+C)$; let us
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   986
verify one of the three equations:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   987
\begin{eqnarray*}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   988
  \case(f,\case(g,h), \Inr(\Inl(b))) 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   989
    & = & \case(g,h,\Inl(b)) \\
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   990
    & = & g(b)
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   991
\end{eqnarray*}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   992
\end{itemize}
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   993
Codatatype definitions are treated in precisely the same way.  They express
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   994
case operators using those for the variant products and sums, namely
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   995
$\qsplit$ and~$\qcase$.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   996
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   997
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
   998
\ifCADE The package has processed all the datatypes discussed in my earlier
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
   999
paper~\cite{paulson-set-II} and the codatatype of lazy lists.  Space
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1000
limitations preclude discussing these examples here, but they are
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1001
distributed with Isabelle.  
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1002
\typeout{****Omitting datatype examples from CADE version!} \else
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1003
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1004
To see how constructors and the case analysis operator are defined, let us
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1005
examine some examples.  These include lists and trees/forests, which I have
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1006
discussed extensively in another paper~\cite{paulson-set-II}.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1007
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1008
\begin{figure}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1009
\begin{ttbox} 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1010
structure List = Datatype_Fun
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1011
 (val thy = Univ.thy;
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1012
  val rec_specs = 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1013
      [("list", "univ(A)",
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1014
          [(["Nil"],    "i"), 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1015
           (["Cons"],   "[i,i]=>i")])];
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1016
  val rec_styp = "i=>i";
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1017
  val ext = None;
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1018
  val sintrs = 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1019
      ["Nil : list(A)",
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1020
       "[| a: A;  l: list(A) |] ==> Cons(a,l) : list(A)"];
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1021
  val monos = [];
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1022
  val type_intrs = datatype_intrs;
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1023
  val type_elims = datatype_elims);
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1024
\end{ttbox}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1025
\hrule
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1026
\caption{Defining the datatype of lists} \label{list-fig}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1027
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1028
\medskip
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1029
\begin{ttbox}
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1030
structure LList = CoDatatype_Fun
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1031
 (val thy = QUniv.thy;
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1032
  val rec_specs = 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1033
      [("llist", "quniv(A)",
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1034
          [(["LNil"],   "i"), 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1035
           (["LCons"],  "[i,i]=>i")])];
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1036
  val rec_styp = "i=>i";
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1037
  val ext = None;
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1038
  val sintrs = 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1039
      ["LNil : llist(A)",
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1040
       "[| a: A;  l: llist(A) |] ==> LCons(a,l) : llist(A)"];
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1041
  val monos = [];
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1042
  val type_intrs = codatatype_intrs;
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1043
  val type_elims = codatatype_elims);
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1044
\end{ttbox}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1045
\hrule
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1046
\caption{Defining the codatatype of lazy lists} \label{llist-fig}
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1047
\end{figure}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1048
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1049
\subsection{Example: lists and lazy lists}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1050
Figures \ref{list-fig} and~\ref{llist-fig} present the ML definitions of
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1051
lists and lazy lists, respectively.  They highlight the (many) similarities
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1052
and (few) differences between datatype and codatatype definitions.
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1053
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1054
Each form of list has two constructors, one for the empty list and one for
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1055
adding an element to a list.  Each takes a parameter, defining the set of
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1056
lists over a given set~$A$.  Each uses the appropriate domain from a
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1057
Isabelle/ZF theory:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1058
\begin{itemize}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1059
\item $\lst(A)$ specifies domain $\univ(A)$ and parent theory {\tt Univ.thy}.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1060
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1061
\item $\llist(A)$ specifies domain $\quniv(A)$ and parent theory {\tt
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1062
QUniv.thy}.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1063
\end{itemize}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1064
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1065
Since $\lst(A)$ is a datatype, it enjoys a structural induction rule, {\tt
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1066
  List.induct}:
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1067
\[ \infer{P(x)}{x\in\lst(A) & P(\Nil)
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1068
        & \infer*{P(\Cons(a,l))}{[a\in A & l\in\lst(A) & P(l)]_{a,l}} }
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1069
\] 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1070
Induction and freeness yield the law $l\not=\Cons(a,l)$.  To strengthen this,
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1071
Isabelle/ZF defines the rank of a set and proves that the standard pairs and
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1072
injections have greater rank than their components.  An immediate consequence,
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1073
which justifies structural recursion on lists \cite[\S4.3]{paulson-set-II},
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1074
is
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1075
\[ \rank(l) < \rank(\Cons(a,l)). \]
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1076
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1077
Since $\llist(A)$ is a codatatype, it has no induction rule.  Instead it has
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1078
the coinduction rule shown in \S\ref{coind-sec}.  Since variant pairs and
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1079
injections are monotonic and need not have greater rank than their
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1080
components, fixedpoint operators can create cyclic constructions.  For
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1081
example, the definition
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1082
\begin{eqnarray*}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1083
  \lconst(a) & \equiv & \lfp(\univ(a), \lambda l. \LCons(a,l))
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1084
\end{eqnarray*}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1085
yields $\lconst(a) = \LCons(a,\lconst(a))$.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1086
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1087
\medskip
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1088
It may be instructive to examine the definitions of the constructors and
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1089
case operator for $\lst(A)$.  The definitions for $\llist(A)$ are similar.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1090
The list constructors are defined as follows:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1091
\begin{eqnarray*}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1092
  \Nil       & = & \Inl(\emptyset) \\
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1093
  \Cons(a,l) & = & \Inr(\pair{a,l})
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1094
\end{eqnarray*}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1095
The operator $\lstcase$ performs case analysis on these two alternatives:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1096
\begin{eqnarray*}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1097
  \lstcase(c,h) & \equiv & \case(\lambda u.c, \split(h)) 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1098
\end{eqnarray*}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1099
Let us verify the two equations:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1100
\begin{eqnarray*}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1101
    \lstcase(c, h, \Nil) & = & 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1102
       \case(\lambda u.c, \split(h), \Inl(\emptyset)) \\
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1103
     & = & (\lambda u.c)(\emptyset) \\
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1104
     & = & c\\[1ex]
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1105
    \lstcase(c, h, \Cons(x,y)) & = & 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1106
       \case(\lambda u.c, \split(h), \Inr(\pair{x,y})) \\
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1107
     & = & \split(h, \pair{x,y}) \\
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1108
     & = & h(x,y)
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1109
\end{eqnarray*} 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1110
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1111
\begin{figure}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1112
\begin{small}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1113
\begin{verbatim}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1114
structure TF = Datatype_Fun
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1115
 (val thy = Univ.thy;
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1116
  val rec_specs = 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1117
      [("tree", "univ(A)",
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1118
          [(["Tcons"],  "[i,i]=>i")]),
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1119
       ("forest", "univ(A)",
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1120
          [(["Fnil"],   "i"),
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1121
           (["Fcons"],  "[i,i]=>i")])];
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1122
  val rec_styp = "i=>i";
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1123
  val ext = None;
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1124
  val sintrs = 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1125
          ["[| a:A;  f: forest(A) |] ==> Tcons(a,f) : tree(A)",
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1126
           "Fnil : forest(A)",
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1127
           "[| t: tree(A);  f: forest(A) |] ==> Fcons(t,f) : forest(A)"];
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1128
  val monos = [];
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1129
  val type_intrs = datatype_intrs;
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1130
  val type_elims = datatype_elims);
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1131
\end{verbatim}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1132
\end{small}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1133
\hrule
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1134
\caption{Defining the datatype of trees and forests} \label{tf-fig}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1135
\end{figure}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1136
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1137
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1138
\subsection{Example: mutual recursion}
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1139
In mutually recursive trees and forests~\cite[\S4.5]{paulson-set-II}, trees
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1140
have the one constructor $\Tcons$, while forests have the two constructors
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1141
$\Fnil$ and~$\Fcons$.  Figure~\ref{tf-fig} presents the ML
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1142
definition.  It has much in common with that of $\lst(A)$, including its
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1143
use of $\univ(A)$ for the domain and {\tt Univ.thy} for the parent theory.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1144
The three introduction rules define the mutual recursion.  The
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1145
distinguishing feature of this example is its two induction rules.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1146
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1147
The basic induction rule is called {\tt TF.induct}:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1148
\[ \infer{P(x)}{x\in\TF(A) & 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1149
     \infer*{P(\Tcons(a,f))}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1150
        {\left[\begin{array}{l} a\in A \\ 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1151
                                f\in\forest(A) \\ P(f)
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1152
               \end{array}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1153
         \right]_{a,f}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1154
     & P(\Fnil)
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1155
     & \infer*{P(\Fcons(t,f))}
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1156
        {\left[\begin{array}{l} t\in\tree(A)   \\ P(t) \\
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1157
                                f\in\forest(A) \\ P(f)
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1158
                \end{array}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1159
         \right]_{t,f}} }
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1160
\] 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1161
This rule establishes a single predicate for $\TF(A)$, the union of the
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1162
recursive sets.  
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1163
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1164
Although such reasoning is sometimes useful
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1165
\cite[\S4.5]{paulson-set-II}, a proper mutual induction rule should establish
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1166
separate predicates for $\tree(A)$ and $\forest(A)$.   The package calls this
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1167
rule {\tt TF.mutual\_induct}.  Observe the usage of $P$ and $Q$ in the
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1168
induction hypotheses:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1169
\[ \infer{(\forall z. z\in\tree(A)\imp P(z)) \conj
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1170
          (\forall z. z\in\forest(A)\imp Q(z))}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1171
     {\infer*{P(\Tcons(a,f))}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1172
        {\left[\begin{array}{l} a\in A \\ 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1173
                                f\in\forest(A) \\ Q(f)
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1174
               \end{array}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1175
         \right]_{a,f}}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1176
     & Q(\Fnil)
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1177
     & \infer*{Q(\Fcons(t,f))}
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1178
        {\left[\begin{array}{l} t\in\tree(A)   \\ P(t) \\
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1179
                                f\in\forest(A) \\ Q(f)
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1180
                \end{array}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1181
         \right]_{t,f}} }
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1182
\] 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1183
As mentioned above, the package does not define a structural recursion
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1184
operator.  I have described elsewhere how this is done
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1185
\cite[\S4.5]{paulson-set-II}.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1186
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1187
Both forest constructors have the form $\Inr(\cdots)$,
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1188
while the tree constructor has the form $\Inl(\cdots)$.  This pattern would
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1189
hold regardless of how many tree or forest constructors there were.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1190
\begin{eqnarray*}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1191
  \Tcons(a,l)  & = & \Inl(\pair{a,l}) \\
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1192
  \Fnil        & = & \Inr(\Inl(\emptyset)) \\
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1193
  \Fcons(a,l)  & = & \Inr(\Inr(\pair{a,l}))
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1194
\end{eqnarray*} 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1195
There is only one case operator; it works on the union of the trees and
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1196
forests:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1197
\begin{eqnarray*}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1198
  {\tt tree\_forest\_case}(f,c,g) & \equiv & 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1199
    \case(\split(f),\, \case(\lambda u.c, \split(g)))
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1200
\end{eqnarray*}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1201
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1202
\begin{figure}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1203
\begin{small}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1204
\begin{verbatim}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1205
structure Data = Datatype_Fun
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1206
 (val thy = Univ.thy;
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1207
  val rec_specs = 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1208
      [("data", "univ(A Un B)",
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1209
          [(["Con0"],   "i"),
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1210
           (["Con1"],   "i=>i"),
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1211
           (["Con2"],   "[i,i]=>i"),
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1212
           (["Con3"],   "[i,i,i]=>i")])];
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1213
  val rec_styp = "[i,i]=>i";
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1214
  val ext = None;
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1215
  val sintrs = 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1216
          ["Con0 : data(A,B)",
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1217
           "[| a: A |] ==> Con1(a) : data(A,B)",
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1218
           "[| a: A; b: B |] ==> Con2(a,b) : data(A,B)",
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1219
           "[| a: A; b: B;  d: data(A,B) |] ==> Con3(a,b,d) : data(A,B)"];
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1220
  val monos = [];
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1221
  val type_intrs = datatype_intrs;
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1222
  val type_elims = datatype_elims);
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1223
\end{verbatim}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1224
\end{small}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1225
\hrule
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1226
\caption{Defining the four-constructor sample datatype} \label{data-fig}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1227
\end{figure}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1228
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1229
\subsection{A four-constructor datatype}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1230
Finally let us consider a fairly general datatype.  It has four
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1231
constructors $\Con_0$, \ldots, $\Con_3$, with the
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1232
corresponding arities.  Figure~\ref{data-fig} presents the ML definition. 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1233
Because this datatype has two set parameters, $A$ and~$B$, it specifies
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1234
$\univ(A\un B)$ as its domain.  The structural induction rule has four
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1235
minor premises, one per constructor:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1236
\[ \infer{P(x)}{x\in\data(A,B) & 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1237
    P(\Con_0) &
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1238
    \infer*{P(\Con_1(a))}{[a\in A]_a} &
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1239
    \infer*{P(\Con_2(a,b))}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1240
      {\left[\begin{array}{l} a\in A \\ b\in B \end{array}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1241
       \right]_{a,b}} &
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1242
    \infer*{P(\Con_3(a,b,d))}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1243
      {\left[\begin{array}{l} a\in A \\ b\in B \\
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1244
                              d\in\data(A,B) \\ P(d)
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1245
              \end{array}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1246
       \right]_{a,b,d}} }
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1247
\] 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1248
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1249
The constructor definitions are
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1250
\begin{eqnarray*}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1251
  \Con_0         & = & \Inl(\Inl(\emptyset)) \\
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1252
  \Con_1(a)      & = & \Inl(\Inr(a)) \\
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1253
  \Con_2(a,b)    & = & \Inr(\Inl(\pair{a,b})) \\
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1254
  \Con_3(a,b,c)  & = & \Inr(\Inr(\pair{a,b,c})).
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1255
\end{eqnarray*} 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1256
The case operator is
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1257
\begin{eqnarray*}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1258
  {\tt data\_case}(f_0,f_1,f_2,f_3) & \equiv & 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1259
    \case(\begin{array}[t]{@{}l}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1260
          \case(\lambda u.f_0,\; f_1),\, \\
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1261
          \case(\split(f_2),\; \split(\lambda v.\split(f_3(v)))) )
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1262
   \end{array} 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1263
\end{eqnarray*}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1264
This may look cryptic, but the case equations are trivial to verify.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1265
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1266
In the constructor definitions, the injections are balanced.  A more naive
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1267
approach is to define $\Con_3(a,b,c)$ as
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1268
$\Inr(\Inr(\Inr(\pair{a,b,c})))$; instead, each constructor has two
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1269
injections.  The difference here is small.  But the ZF examples include a
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1270
60-element enumeration type, where each constructor has 5 or~6 injections.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1271
The naive approach would require 1 to~59 injections; the definitions would be
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1272
quadratic in size.  It is like the difference between the binary and unary
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1273
numeral systems. 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1274
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1275
The result structure contains the case operator and constructor definitions as
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1276
the theorem list \verb|con_defs|. It contains the case equations, such as 
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1277
\begin{eqnarray*}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1278
  {\tt data\_case}(f_0,f_1,f_2,f_3,\Con_3(a,b,c)) & = & f_3(a,b,c),
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1279
\end{eqnarray*}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1280
as the theorem list \verb|case_eqns|.  There is one equation per constructor.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1281
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1282
\subsection{Proving freeness theorems}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1283
There are two kinds of freeness theorems:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1284
\begin{itemize}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1285
\item {\bf injectiveness} theorems, such as
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1286
\[ \Con_2(a,b) = \Con_2(a',b') \bimp a=a' \conj b=b' \]
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1287
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1288
\item {\bf distinctness} theorems, such as
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1289
\[ \Con_1(a) \not= \Con_2(a',b')  \]
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1290
\end{itemize}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1291
Since the number of such theorems is quadratic in the number of constructors,
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1292
the package does not attempt to prove them all.  Instead it returns tools for
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1293
proving desired theorems --- either explicitly or `on the fly' during
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1294
simplification or classical reasoning.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1295
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1296
The theorem list \verb|free_iffs| enables the simplifier to perform freeness
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1297
reasoning.  This works by incremental unfolding of constructors that appear in
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1298
equations.  The theorem list contains logical equivalences such as
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1299
\begin{eqnarray*}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1300
  \Con_0=c      & \bimp &  c=\Inl(\Inl(\emptyset))     \\
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1301
  \Con_1(a)=c   & \bimp &  c=\Inl(\Inr(a))             \\
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1302
                & \vdots &                             \\
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1303
  \Inl(a)=\Inl(b)   & \bimp &  a=b                     \\
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1304
  \Inl(a)=\Inr(b)   & \bimp &  {\tt False}             \\
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1305
  \pair{a,b} = \pair{a',b'} & \bimp & a=a' \conj b=b'
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1306
\end{eqnarray*}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1307
For example, these rewrite $\Con_1(a)=\Con_1(b)$ to $a=b$ in four steps.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1308
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1309
The theorem list \verb|free_SEs| enables the classical
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1310
reasoner to perform similar replacements.  It consists of elimination rules
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1311
to replace $\Con_0=c$ by $c=\Inl(\Inl(\emptyset))$, and so forth, in the
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1312
assumptions.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1313
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1314
Such incremental unfolding combines freeness reasoning with other proof
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1315
steps.  It has the unfortunate side-effect of unfolding definitions of
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1316
constructors in contexts such as $\exists x.\Con_1(a)=x$, where they should
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1317
be left alone.  Calling the Isabelle tactic {\tt fold\_tac con\_defs}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1318
restores the defined constants.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1319
\fi  %CADE
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1320
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1321
\section{Conclusions and future work}
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1322
The fixedpoint approach makes it easy to implement a powerful
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1323
package for inductive and coinductive definitions.  It is efficient: it
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1324
processes most definitions in seconds and even a 60-constructor datatype
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1325
requires only two minutes.  It is also simple: the package consists of
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1326
under 1100 lines (35K bytes) of Standard ML code.  The first working
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1327
version took under a week to code.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1328
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1329
The approach is not restricted to set theory.  It should be suitable for
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1330
any logic that has some notion of set and the Knaster-Tarski Theorem.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1331
Indeed, Melham's inductive definition package for the HOL
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1332
system~\cite{camilleri92} implicitly proves this theorem.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1333
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1334
Datatype and codatatype definitions furthermore require a particular set
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1335
closed under a suitable notion of ordered pair.  I intend to use the
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1336
Isabelle/ZF package as the basis for a higher-order logic one, using
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1337
Isabelle/HOL\@.  The necessary theory is already
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1338
mechanized~\cite{paulson-coind}.  HOL represents sets by unary predicates;
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1339
defining the corresponding types may cause complication.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1340
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1341
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1342
\bibliographystyle{plain}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1343
\bibliography{atp,theory,funprog,isabelle}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1344
%%%%%\doendnotes
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1345
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1346
\ifCADE\typeout{****Omitting appendices from CADE version!}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1347
\else
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1348
\newpage
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1349
\appendix
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1350
\section{Inductive and coinductive definitions: users guide}
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1351
The ML functors \verb|Inductive_Fun| and \verb|CoInductive_Fun| build
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1352
inductive and coinductive definitions, respectively.  This section describes
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1353
how to invoke them.  
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1354
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1355
\subsection{The result structure}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1356
Many of the result structure's components have been discussed
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1357
in~\S\ref{basic-sec}; others are self-explanatory.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1358
\begin{description}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1359
\item[\tt thy] is the new theory containing the recursive sets.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1360
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1361
\item[\tt defs] is the list of definitions of the recursive sets.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1362
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1363
\item[\tt bnd\_mono] is a monotonicity theorem for the fixedpoint operator.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1364
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1365
\item[\tt unfold] is a fixedpoint equation for the recursive set (the union of
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1366
the recursive sets, in the case of mutual recursion).
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1367
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1368
\item[\tt dom\_subset] is a theorem stating inclusion in the domain.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1369
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1370
\item[\tt intrs] is the list of introduction rules, now proved as theorems, for
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1371
the recursive sets.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1372
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1373
\item[\tt elim] is the elimination rule.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1374
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1375
\item[\tt mk\_cases] is a function to create simplified instances of {\tt
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1376
elim}, using freeness reasoning on some underlying datatype.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1377
\end{description}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1378
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1379
For an inductive definition, the result structure contains two induction rules,
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1380
{\tt induct} and \verb|mutual_induct|.  For a coinductive definition, it
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1381
contains the rule \verb|coinduct|.
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1382
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1383
Figure~\ref{def-result-fig} summarizes the two result signatures,
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1384
specifying the types of all these components.
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1385
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1386
\begin{figure}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1387
\begin{ttbox}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1388
sig
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1389
val thy          : theory
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1390
val defs         : thm list
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1391
val bnd_mono     : thm
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1392
val unfold       : thm
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1393
val dom_subset   : thm
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1394
val intrs        : thm list
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1395
val elim         : thm
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1396
val mk_cases     : thm list -> string -> thm
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1397
{\it(Inductive definitions only)} 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1398
val induct       : thm
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1399
val mutual_induct: thm
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1400
{\it(Coinductive definitions only)}
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1401
val coinduct    : thm
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1402
end
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1403
\end{ttbox}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1404
\hrule
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1405
\caption{The result of a (co)inductive definition} \label{def-result-fig}
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1406
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1407
\medskip
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1408
\begin{ttbox}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1409
sig  
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1410
val thy          : theory
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1411
val rec_doms     : (string*string) list
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1412
val sintrs       : string list
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1413
val monos        : thm list
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1414
val con_defs     : thm list
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1415
val type_intrs   : thm list
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1416
val type_elims   : thm list
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1417
end
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1418
\end{ttbox}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1419
\hrule
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1420
\caption{The argument of a (co)inductive definition} \label{def-arg-fig}
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1421
\end{figure}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1422
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1423
\subsection{The argument structure}
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1424
Both \verb|Inductive_Fun| and \verb|CoInductive_Fun| take the same argument
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1425
structure (Figure~\ref{def-arg-fig}).  Its components are as follows:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1426
\begin{description}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1427
\item[\tt thy] is the definition's parent theory, which {\it must\/}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1428
declare constants for the recursive sets.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1429
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1430
\item[\tt rec\_doms] is a list of pairs, associating the name of each recursive
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1431
set with its domain.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1432
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1433
\item[\tt sintrs] specifies the desired introduction rules as strings.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1434
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1435
\item[\tt monos] consists of monotonicity theorems for each operator applied
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1436
to a recursive set in the introduction rules.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1437
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1438
\item[\tt con\_defs] contains definitions of constants appearing in the
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1439
introduction rules.  The (co)datatype package supplies the constructors'
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1440
definitions here.  Most direct calls of \verb|Inductive_Fun| or
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1441
\verb|CoInductive_Fun| pass the empty list; one exception is the primitive
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1442
recursive functions example (\S\ref{primrec-sec}).
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1443
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1444
\item[\tt type\_intrs] consists of introduction rules for type-checking the
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1445
  definition, as discussed in~\S\ref{basic-sec}.  They are applied using
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1446
  depth-first search; you can trace the proof by setting
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1447
  \verb|trace_DEPTH_FIRST := true|.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1448
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1449
\item[\tt type\_elims] consists of elimination rules for type-checking the
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1450
definition.  They are presumed to be `safe' and are applied as much as
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1451
possible, prior to the {\tt type\_intrs} search.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1452
\end{description}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1453
The package has a few notable restrictions:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1454
\begin{itemize}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1455
\item The parent theory, {\tt thy}, must declare the recursive sets as
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1456
  constants.  You can extend a theory with new constants using {\tt
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1457
    addconsts}, as illustrated in~\S\ref{ind-eg-sec}.  If the inductive
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1458
  definition also requires new concrete syntax, then it is simpler to
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1459
  express the parent theory using a theory file.  It is often convenient to
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1460
  define an infix syntax for relations, say $a\prec b$ for $\pair{a,b}\in
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1461
  R$.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1462
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1463
\item The names of the recursive sets must be identifiers, not infix
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1464
operators.  
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1465
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1466
\item Side-conditions must not be conjunctions.  However, an introduction rule
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1467
may contain any number of side-conditions.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1468
\end{itemize}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1469
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1470
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1471
\section{Datatype and codatatype definitions: users guide}
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1472
The ML functors \verb|Datatype_Fun| and \verb|CoDatatype_Fun| define datatypes
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1473
and codatatypes, invoking \verb|Datatype_Fun| and
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1474
\verb|CoDatatype_Fun| to make the underlying (co)inductive definitions. 
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1475
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1476
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1477
\subsection{The result structure}
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1478
The result structure extends that of (co)inductive definitions
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1479
(Figure~\ref{def-result-fig}) with several additional items:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1480
\begin{ttbox}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1481
val con_thy   : theory
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1482
val con_defs  : thm list
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1483
val case_eqns : thm list
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1484
val free_iffs : thm list
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1485
val free_SEs  : thm list
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1486
val mk_free   : string -> thm
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1487
\end{ttbox}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1488
Most of these have been discussed in~\S\ref{data-sec}.  Here is a summary:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1489
\begin{description}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1490
\item[\tt con\_thy] is a new theory containing definitions of the
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1491
(co)datatype's constructors and case operator.  It also declares the
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1492
recursive sets as constants, so that it may serve as the parent
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1493
theory for the (co)inductive definition.
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1494
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1495
\item[\tt con\_defs] is a list of definitions: the case operator followed by
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1496
the constructors.  This theorem list can be supplied to \verb|mk_cases|, for
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1497
example.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1498
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1499
\item[\tt case\_eqns] is a list of equations, stating that the case operator
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1500
inverts each constructor.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1501
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1502
\item[\tt free\_iffs] is a list of logical equivalences to perform freeness
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1503
reasoning by rewriting.  A typical application has the form
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1504
\begin{ttbox}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1505
by (asm_simp_tac (ZF_ss addsimps free_iffs) 1);
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1506
\end{ttbox}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1507
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1508
\item[\tt free\_SEs] is a list of `safe' elimination rules to perform freeness
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1509
reasoning.  It can be supplied to \verb|eresolve_tac| or to the classical
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1510
reasoner:
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1511
\begin{ttbox} 
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1512
by (fast_tac (ZF_cs addSEs free_SEs) 1);
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1513
\end{ttbox}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1514
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1515
\item[\tt mk\_free] is a function to prove freeness properties, specified as
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1516
strings.  The theorems can be expressed in various forms, such as logical
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1517
equivalences or elimination rules.
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1518
\end{description}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1519
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1520
The result structure also inherits everything from the underlying
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1521
(co)inductive definition, such as the introduction rules, elimination rule,
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1522
and induction/coinduction rule.
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1523
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1524
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1525
\begin{figure}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1526
\begin{ttbox}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1527
sig
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1528
val thy       : theory
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1529
val rec_specs : (string * string * (string list*string)list) list
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1530
val rec_styp  : string
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1531
val ext       : Syntax.sext option
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1532
val sintrs    : string list
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1533
val monos     : thm list
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1534
val type_intrs: thm list
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1535
val type_elims: thm list
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1536
end
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1537
\end{ttbox}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1538
\hrule
130
c035b6b9eafc Many edits suggested by Grundy & Thompson
lcp
parents: 103
diff changeset
  1539
\caption{The argument of a (co)datatype definition} \label{data-arg-fig}
103
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1540
\end{figure}
30bd42401ab2 Initial revision
lcp
parents:
diff changeset
  1541
30bd42401ab2 Initial revision
lcp
parents:
diff changeset