author  paulson 
Thu, 21 Mar 1996 13:02:26 +0100  
changeset 1601  0ef6ea27ab15 
parent 1144  5a62ecf80126 
permissions  rwrr 
1144  1 
%process by latex inddefsslides; dvips Plime inddefsslides 
2 
% ghostview magstep 2 landscape inddefsslides.ps 

3 
% $Id$ 

4 
\documentclass[a4,slidesonly,semlayer]{seminar} 

541
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

5 

1144  6 
\usepackage{fancybox} 
7 
\usepackage{semhelv} 

8 
\usepackage{epsf} 

541
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

9 
\def\printlandscape{\special{landscape}} % Works with dvips. 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

10 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

11 
\slidesmag{5}\articlemag{2} %the difference is 3 instead of 4! 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

12 
\extraslideheight{30pt} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

13 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

14 
\renewcommand\slidefuzz{6pt} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

15 
\sloppy\hfuzz2pt %sloppy defines \hfuzz0.5pt but it's mainly for text 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

16 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

17 
\newcommand\sbs{\subseteq} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

18 
\newcommand\Pow{{\cal P}} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

19 
\newcommand\lfp{\hbox{\tt lfp}} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

20 
\newcommand\gfp{\hbox{\tt gfp}} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

21 
\newcommand\lst{\hbox{\tt list}} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

22 
\newcommand\term{\hbox{\tt term}} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

23 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

24 
\newcommand\heading[1]{% 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

25 
\begin{center}\large\bf\shadowbox{#1}\end{center} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

26 
\vspace{1ex minus 1ex}} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

27 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

28 
\newpagestyle{mine}% 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

29 
{L. Paulson\hfil A Fixedpoint Approach to (Co)Inductive Definitions\hfil 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

30 
\thepage}% 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

31 
{\hfil\special{psfile=cuarms.eps hscale=20 vscale=20 voffset=6 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

32 
hoffset=14}\hfil} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

33 
\pagestyle{mine} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

34 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

35 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

36 
\begin{document} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

37 
\slidefonts 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

38 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

39 
\begin{slide}\centering 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

40 
\shadowbox{% 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

41 
\begin{Bcenter} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

42 
{\Large\bf A Fixedpoint Approach to}\\[2ex] 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

43 
{\Large\bf (Co)Inductive Definitions} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

44 
\end{Bcenter}} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

45 
\bigskip 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

46 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

47 
\begin{Bcenter} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

48 
Lawrence C. Paulson\\ 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

49 
Computer Laboratory\\ 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

50 
University of Cambridge\\ 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

51 
England\\[1ex] 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

52 
\verblcp@cl.cam.ac.uk 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

53 
\end{Bcenter} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

54 
\bigskip 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

55 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

56 
{\footnotesize Thanks: SERC grants GR/G53279, GR/H40570; ESPRIT Project 6453 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

57 
`Types'} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

58 
\end{slide} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

59 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

60 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

61 
\begin{slide} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

62 
\heading{Inductive Definitions} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

63 
\begin{itemize} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

64 
\item {\bf datatypes} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

65 
\begin{itemize} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

66 
\item finite lists, trees 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

67 
\item syntax of expressions, \ldots 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

68 
\end{itemize} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

69 
\item {\bf inference systems} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

70 
\begin{itemize} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

71 
\item transitive closure of a relation 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

72 
\item transition systems 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

73 
\item structural operational semantics 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

74 
\end{itemize} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

75 
\end{itemize} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

76 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

77 
Supported by Boyer/Moore, HOL, Coq, \ldots, Isabelle/ZF 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

78 
\end{slide} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

79 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

80 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

81 
\begin{slide} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

82 
\heading{Coinductive Definitions} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

83 
\begin{itemize} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

84 
\item {\bf codatatypes} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

85 
\begin{itemize} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

86 
\item {\it infinite\/} lists, trees 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

87 
\item syntax of {\it infinite\/} expressions, \ldots 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

88 
\end{itemize} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

89 
\item {\bf bisimulation relations} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

90 
\begin{itemize} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

91 
\item process equivalence 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

92 
\item uses in functional programming (Abramksy, Howe) 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

93 
\end{itemize} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

94 
\end{itemize} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

95 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

96 
Supported by \ldots ?, \ldots, Isabelle/ZF 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

97 
\end{slide} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

98 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

99 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

100 
\begin{slide} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

101 
\heading{The KnasterTarksi Fixedpoint Theorem} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

102 
$h$ a monotone function 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

103 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

104 
$D$ a set such that $h(D)\sbs D$ 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

105 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

106 
The {\bf least} fixedpoint $\lfp(D,h)$ yields {\bf inductive} definitions 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

107 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

108 
The {\bf greatest} fixedpoint $\gfp(D,h)$ yields {\bf coinductive} definitions 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

109 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

110 
{\it A general approach\/}: 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

111 
\begin{itemize} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

112 
\item handles all provably monotone definitions 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

113 
\item works for set theory, higherorder logic, \ldots 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

114 
\end{itemize} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

115 
\end{slide} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

116 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

117 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

118 
\begin{slide} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

119 
\heading{An Implementation in Isabelle/ZF}\centering 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

120 
\begin{itemize} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

121 
\item {\bf Input} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

122 
\begin{itemize} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

123 
\item description of {\it introduction rules\/} \& tree's {\it 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

124 
constructors\/} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

125 
\item {\it theorems\/} implying that the definition is {\it monotonic\/} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

126 
\end{itemize} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

127 
\item {\bf Output} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

128 
\begin{itemize} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

129 
\item (co)induction rules 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

130 
\item case analysis rule and {\it rule inversion\/} tools, \ldots 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

131 
\end{itemize} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

132 
\end{itemize} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

133 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

134 
\vfill 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

135 
{\it flexible, secure, \ldots but fast\/} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

136 
\end{slide} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

137 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

138 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

139 
\begin{slide} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

140 
\heading{Working Examples} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

141 
\begin{itemize} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

142 
\item lists 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

143 
\item terms recursive over lists: $\term(A) = A\times\lst(\term(A))$ 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

144 
\item primitive recursive functions 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

145 
\item lazy lists 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

146 
\item bisimulations for lazy lists 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

147 
\item combinator reductions; ChurchRosser Theorem 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

148 
\item mutually recursive trees \& forests 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

149 
\end{itemize} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

150 
\end{slide} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

151 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

152 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

153 
\begin{slide} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

154 
\heading{Other Work Using Fixedpoints} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

155 
{\bf The HOL system}: 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

156 
\begin{itemize} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

157 
\item Melham's induction package: special case of Fixedpoint Theorem 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

158 
\item Andersen \& Petersen's induction package 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

159 
\item (no HOL datatype package uses fixedpoints) 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

160 
\end{itemize} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

161 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

162 
{\bf Coq and LEGO}: 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

163 
\begin{itemize} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

164 
\item (Co)induction {\it almost\/} expressible in base logic (CoC) 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

165 
\item \ldots{} inductive definitions are builtin 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

166 
\end{itemize} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

167 
\end{slide} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

168 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

169 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

170 
\begin{slide} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

171 
\heading{Limitations \& Future Developments}\centering 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

172 
\begin{itemize} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

173 
\item {\bf infinitebranching trees} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

174 
\begin{itemize} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

175 
\item justification requires proof 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

176 
\item would be easier to {\it build them in\/}! 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

177 
\end{itemize} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

178 
\item {\bf recursive function definitions} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

179 
\begin{itemize} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

180 
\item use {\it wellfounded\/} recursion 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

181 
\item distinct from datatype definitions 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

182 
\end{itemize} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

183 
\item {\bf port to Isabelle/HOL} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

184 
\end{itemize} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

185 
\end{slide} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

186 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

187 
\end{document} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

188 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

189 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

190 
{\it flat\/} ordered pairs used to define infinite lists, \ldots 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

191 

be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

192 
\begin{slide} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

193 
\heading{}\centering 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

194 
\end{slide} 
be4c4ba87143
overheads for inductive definitions, originally for CADE12
lcp
parents:
diff
changeset

195 