104

1 
\contentsline {section}{\numberline {1}Introduction}{1}


2 
\contentsline {section}{\numberline {2}Fixedpoint operators}{2}


3 
\contentsline {section}{\numberline {3}Elements of an inductive or coinductive definition}{2}


4 
\contentsline {subsection}{\numberline {3.1}The form of the introduction rules}{2}


5 
\contentsline {subsection}{\numberline {3.2}The fixedpoint definitions}{3}


6 
\contentsline {subsection}{\numberline {3.3}Mutual recursion}{4}


7 
\contentsline {subsection}{\numberline {3.4}Proving the introduction rules}{4}


8 
\contentsline {subsection}{\numberline {3.5}The elimination rule}{4}


9 
\contentsline {section}{\numberline {4}Induction and coinduction rules}{5}


10 
\contentsline {subsection}{\numberline {4.1}The basic induction rule}{5}


11 
\contentsline {subsection}{\numberline {4.2}Mutual induction}{5}


12 
\contentsline {subsection}{\numberline {4.3}Coinduction}{6}


13 
\contentsline {section}{\numberline {5}Examples of inductive and coinductive definitions}{6}


14 
\contentsline {subsection}{\numberline {5.1}The finite set operator}{7}


15 
\contentsline {subsection}{\numberline {5.2}Lists of $n$ elements}{7}


16 
\contentsline {subsection}{\numberline {5.3}A demonstration of {\ptt mk\unhbox \voidb@x \kern .06em \vbox {\hrule width.3em}cases}}{9}


17 
\contentsline {subsection}{\numberline {5.4}A coinductive definition: bisimulations on lazy lists}{9}


18 
\contentsline {subsection}{\numberline {5.5}The accessible part of a relation}{10}


19 
\contentsline {subsection}{\numberline {5.6}The primitive recursive functions}{11}


20 
\contentsline {section}{\numberline {6}Datatypes and codatatypes}{13}


21 
\contentsline {subsection}{\numberline {6.1}Constructors and their domain}{13}


22 
\contentsline {subsection}{\numberline {6.2}The case analysis operator}{14}


23 
\contentsline {subsection}{\numberline {6.3}Example: lists and lazy lists}{15}


24 
\contentsline {subsection}{\numberline {6.4}Example: mutual recursion}{16}


25 
\contentsline {subsection}{\numberline {6.5}A fourconstructor datatype}{18}


26 
\contentsline {subsection}{\numberline {6.6}Proving freeness theorems}{19}


27 
\contentsline {section}{\numberline {7}Conclusions and future work}{20}


28 
\contentsline {section}{\numberline {A}Inductive and coinductive definitions: users guide}{22}


29 
\contentsline {subsection}{\numberline {A.1}The result structure}{22}


30 
\contentsline {subsection}{\numberline {A.2}The argument structure}{23}


31 
\contentsline {section}{\numberline {B}Datatype and codatatype definitions: users guide}{24}


32 
\contentsline {subsection}{\numberline {B.1}The result structure}{24}


33 
\contentsline {subsection}{\numberline {B.2}The argument structure}{24}
