doc-src/ind-defs-slides.tex
author paulson
Fri, 17 Jan 1997 12:49:31 +0100
changeset 2516 4d68fbe6378b
parent 1144 5a62ecf80126
permissions -rw-r--r--
Now with Andy Gordon's treatment of freshness to replace newN/K
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1144
5a62ecf80126 converted to LaTeX-2e
lcp
parents: 541
diff changeset
     1
%process by     latex ind-defs-slides; dvips -Plime ind-defs-slides
5a62ecf80126 converted to LaTeX-2e
lcp
parents: 541
diff changeset
     2
%               ghostview -magstep -2 -landscape ind-defs-slides.ps
5a62ecf80126 converted to LaTeX-2e
lcp
parents: 541
diff changeset
     3
%  $Id$
5a62ecf80126 converted to LaTeX-2e
lcp
parents: 541
diff changeset
     4
\documentclass[a4,slidesonly,semlayer]{seminar}
541
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
     5
1144
5a62ecf80126 converted to LaTeX-2e
lcp
parents: 541
diff changeset
     6
\usepackage{fancybox}
5a62ecf80126 converted to LaTeX-2e
lcp
parents: 541
diff changeset
     7
\usepackage{semhelv}
5a62ecf80126 converted to LaTeX-2e
lcp
parents: 541
diff changeset
     8
\usepackage{epsf}
541
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
     9
\def\printlandscape{\special{landscape}}    % Works with dvips.
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    10
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    11
\slidesmag{5}\articlemag{2}    %the difference is 3 instead of 4!
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    12
\extraslideheight{30pt}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    13
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    14
\renewcommand\slidefuzz{6pt}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    15
\sloppy\hfuzz2pt   %sloppy defines \hfuzz0.5pt but it's mainly for text
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    16
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    17
\newcommand\sbs{\subseteq}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    18
\newcommand\Pow{{\cal P}}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    19
\newcommand\lfp{\hbox{\tt lfp}}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    20
\newcommand\gfp{\hbox{\tt gfp}}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    21
\newcommand\lst{\hbox{\tt list}}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    22
\newcommand\term{\hbox{\tt term}}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    23
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    24
\newcommand\heading[1]{%
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    25
  \begin{center}\large\bf\shadowbox{#1}\end{center}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    26
  \vspace{1ex minus 1ex}}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    27
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    28
\newpagestyle{mine}%
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    29
  {L. Paulson\hfil A Fixedpoint Approach to (Co)Inductive Definitions\hfil
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    30
      \thepage}%
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    31
  {\hfil\special{psfile=cuarms.eps hscale=20 vscale=20 voffset=-6
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    32
      hoffset=-14}\hfil}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    33
\pagestyle{mine}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    34
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    35
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    36
\begin{document}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    37
\slidefonts
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    38
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    39
\begin{slide}\centering
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    40
\shadowbox{% 
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    41
    \begin{Bcenter}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    42
    {\Large\bf A Fixedpoint Approach to}\\[2ex]
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    43
    {\Large\bf (Co)Inductive Definitions}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    44
    \end{Bcenter}}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    45
\bigskip
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    46
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    47
    \begin{Bcenter}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    48
    Lawrence C. Paulson\\
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    49
    Computer Laboratory\\
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    50
    University of Cambridge\\
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    51
    England\\[1ex]
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    52
    \verb|lcp@cl.cam.ac.uk|
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    53
    \end{Bcenter}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    54
\bigskip
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    55
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    56
{\footnotesize Thanks: SERC grants GR/G53279, GR/H40570; ESPRIT Project 6453
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    57
  `Types'} 
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    58
\end{slide}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    59
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    60
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    61
\begin{slide}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    62
\heading{Inductive Definitions}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    63
\begin{itemize}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    64
  \item {\bf datatypes}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    65
    \begin{itemize}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    66
      \item finite lists, trees
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    67
      \item syntax of expressions, \ldots
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    68
    \end{itemize}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    69
  \item {\bf inference systems}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    70
    \begin{itemize}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    71
      \item transitive closure of a relation
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    72
      \item transition systems
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    73
      \item structural operational semantics
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    74
    \end{itemize}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    75
\end{itemize}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    76
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    77
Supported by Boyer/Moore, HOL, Coq, \ldots, Isabelle/ZF
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    78
\end{slide}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    79
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    80
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    81
\begin{slide}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    82
\heading{Coinductive Definitions}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    83
\begin{itemize}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    84
  \item {\bf codatatypes}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    85
    \begin{itemize}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    86
      \item {\it infinite\/} lists, trees
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    87
      \item  syntax of {\it infinite\/} expressions, \ldots
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    88
    \end{itemize}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    89
  \item {\bf bisimulation relations}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    90
    \begin{itemize}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    91
      \item process equivalence
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    92
      \item uses in functional programming (Abramksy, Howe)
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    93
    \end{itemize}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    94
\end{itemize}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    95
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    96
Supported by \ldots ?, \ldots, Isabelle/ZF
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    97
\end{slide}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    98
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
    99
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   100
\begin{slide}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   101
\heading{The Knaster-Tarksi Fixedpoint Theorem}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   102
$h$ a monotone function
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   103
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   104
$D$ a set such that $h(D)\sbs D$
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   105
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   106
The {\bf least} fixedpoint $\lfp(D,h)$ yields {\bf inductive} definitions
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   107
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   108
The {\bf greatest} fixedpoint $\gfp(D,h)$ yields {\bf coinductive} definitions
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   109
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   110
{\it A general approach\/}:
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   111
\begin{itemize}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   112
  \item handles all provably monotone definitions
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   113
  \item works for set theory, higher-order logic, \ldots
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   114
\end{itemize}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   115
\end{slide}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   116
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   117
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   118
\begin{slide}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   119
\heading{An Implementation in Isabelle/ZF}\centering
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   120
\begin{itemize}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   121
  \item {\bf Input} 
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   122
     \begin{itemize}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   123
      \item description of {\it introduction rules\/} \& tree's {\it
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   124
          constructors\/} 
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   125
      \item {\it theorems\/} implying that the definition is {\it monotonic\/}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   126
    \end{itemize}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   127
  \item {\bf Output} 
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   128
     \begin{itemize}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   129
      \item (co)induction rules
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   130
      \item case analysis rule and {\it rule inversion\/} tools, \ldots
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   131
    \end{itemize}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   132
\end{itemize}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   133
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   134
\vfill
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   135
{\it flexible, secure, \ldots but fast\/}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   136
\end{slide}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   137
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   138
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   139
\begin{slide}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   140
\heading{Working Examples}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   141
\begin{itemize}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   142
  \item lists
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   143
  \item terms recursive over lists: $\term(A) = A\times\lst(\term(A))$
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   144
  \item primitive recursive functions
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   145
  \item lazy lists
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   146
  \item bisimulations for lazy lists
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   147
  \item combinator reductions; Church-Rosser Theorem
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   148
  \item mutually recursive trees \& forests
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   149
\end{itemize}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   150
\end{slide}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   151
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   152
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   153
\begin{slide}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   154
\heading{Other Work Using Fixedpoints}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   155
{\bf The HOL system}:
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   156
\begin{itemize}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   157
  \item Melham's induction package: special case of Fixedpoint Theorem
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   158
  \item Andersen \& Petersen's induction package
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   159
  \item (no HOL datatype package uses fixedpoints)
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   160
\end{itemize}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   161
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   162
{\bf Coq and LEGO}:
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   163
\begin{itemize}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   164
  \item (Co)induction {\it almost\/} expressible in base logic (CoC)
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   165
  \item \ldots{} inductive definitions are built-in
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   166
\end{itemize}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   167
\end{slide}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   168
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   169
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   170
\begin{slide}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   171
\heading{Limitations \& Future Developments}\centering
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   172
\begin{itemize}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   173
  \item {\bf infinite-branching trees}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   174
    \begin{itemize}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   175
      \item justification requires proof
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   176
      \item would be easier to {\it build them in\/}!
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   177
    \end{itemize}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   178
  \item {\bf recursive function definitions}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   179
    \begin{itemize}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   180
      \item use {\it well-founded\/} recursion
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   181
      \item distinct from datatype definitions
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   182
    \end{itemize}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   183
  \item {\bf port to Isabelle/HOL}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   184
\end{itemize}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   185
\end{slide}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   186
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   187
\end{document}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   188
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   189
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   190
{\it flat\/} ordered pairs used to define infinite lists, \ldots
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   191
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   192
\begin{slide}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   193
\heading{}\centering
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   194
\end{slide}
be4c4ba87143 overheads for inductive definitions, originally for CADE-12
lcp
parents:
diff changeset
   195