author | nipkow |
Fri, 26 Jan 1996 20:25:39 +0100 | |
changeset 1454 | d0266c81a85e |
parent 294 | 058343877e3a |
permissions | -rw-r--r-- |
\contentsline {section}{\numberline {1}Introduction}{1} \contentsline {section}{\numberline {2}Fixedpoint operators}{1} \contentsline {section}{\numberline {3}Elements of an inductive or coinductive definition}{2} \contentsline {subsection}{\numberline {3.1}The form of the introduction rules}{2} \contentsline {subsection}{\numberline {3.2}The fixedpoint definitions}{3} \contentsline {subsection}{\numberline {3.3}Mutual recursion}{3} \contentsline {subsection}{\numberline {3.4}Proving the introduction rules}{4} \contentsline {subsection}{\numberline {3.5}The elimination rule}{4} \contentsline {section}{\numberline {4}Induction and coinduction rules}{4} \contentsline {subsection}{\numberline {4.1}The basic induction rule}{4} \contentsline {subsection}{\numberline {4.2}Mutual induction}{5} \contentsline {subsection}{\numberline {4.3}Coinduction}{5} \contentsline {section}{\numberline {5}Examples of inductive and coinductive definitions}{6} \contentsline {subsection}{\numberline {5.1}The finite set operator}{6} \contentsline {subsection}{\numberline {5.2}Lists of $n$ elements}{6} \contentsline {subsection}{\numberline {5.3}A coinductive definition: bisimulations on lazy lists}{7} \contentsline {subsection}{\numberline {5.4}The accessible part of a relation}{8} \contentsline {subsection}{\numberline {5.5}The primitive recursive functions}{9} \contentsline {section}{\numberline {6}Datatypes and codatatypes}{11} \contentsline {subsection}{\numberline {6.1}Constructors and their domain}{11} \contentsline {subsection}{\numberline {6.2}The case analysis operator}{11} \contentsline {section}{\numberline {7}Conclusions and future work}{12}