# HG changeset patch # User lcp # Date 764432501 -3600 # Node ID 058343877e3af286c68d25953d299fc0e589cf36 # Parent 63a0077dd9f27b76a1ea7eacbb6acf5b6c544495 final CADE version diff -r 63a0077dd9f2 -r 058343877e3a doc-src/ind-defs.toc --- a/doc-src/ind-defs.toc Wed Mar 23 13:05:12 1994 +0100 +++ b/doc-src/ind-defs.toc Wed Mar 23 15:21:41 1994 +0100 @@ -1,33 +1,22 @@ \contentsline {section}{\numberline {1}Introduction}{1} -\contentsline {section}{\numberline {2}Fixedpoint operators}{2} -\contentsline {section}{\numberline {3}Elements of an inductive or co-inductive definition}{2} +\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}{4} +\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 co-induction rules}{5} -\contentsline {subsection}{\numberline {4.1}The basic induction rule}{5} +\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}Co-induction}{6} -\contentsline {section}{\numberline {5}Examples of inductive and co-inductive definitions}{6} -\contentsline {subsection}{\numberline {5.1}The finite set operator}{7} -\contentsline {subsection}{\numberline {5.2}Lists of $n$ elements}{7} -\contentsline {subsection}{\numberline {5.3}A demonstration of {\ptt mk\unhbox \voidb@x \kern .06em \vbox {\hrule width.3em}cases}}{9} -\contentsline {subsection}{\numberline {5.4}A co-inductive definition: bisimulations on lazy lists}{9} -\contentsline {subsection}{\numberline {5.5}The accessible part of a relation}{10} -\contentsline {subsection}{\numberline {5.6}The primitive recursive functions}{11} -\contentsline {section}{\numberline {6}Datatypes and co-datatypes}{13} -\contentsline {subsection}{\numberline {6.1}Constructors and their domain}{13} -\contentsline {subsection}{\numberline {6.2}The case analysis operator}{14} -\contentsline {subsection}{\numberline {6.3}Example: lists and lazy lists}{15} -\contentsline {subsection}{\numberline {6.4}Example: mutual recursion}{16} -\contentsline {subsection}{\numberline {6.5}A four-constructor datatype}{18} -\contentsline {subsection}{\numberline {6.6}Proving freeness theorems}{19} -\contentsline {section}{\numberline {7}Conclusions and future work}{20} -\contentsline {section}{\numberline {A}Inductive and co-inductive definitions: users guide}{22} -\contentsline {subsection}{\numberline {A.1}The result structure}{22} -\contentsline {subsection}{\numberline {A.2}The argument structure}{23} -\contentsline {section}{\numberline {B}Datatype and co-datatype definitions: users guide}{24} -\contentsline {subsection}{\numberline {B.1}The result structure}{24} -\contentsline {subsection}{\numberline {B.2}The argument structure}{24} +\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}