doc-src/ind-defs.toc
 author paulson Fri Nov 27 11:24:27 1998 +0100 (1998-11-27) changeset 5979 11cbf236ca16 parent 294 058343877e3a permissions -rw-r--r--
Addition of Hyperreal theories Zorn and Filter
 lcp@104 ` 1` ```\contentsline {section}{\numberline {1}Introduction}{1} ``` lcp@294 ` 2` ```\contentsline {section}{\numberline {2}Fixedpoint operators}{1} ``` lcp@294 ` 3` ```\contentsline {section}{\numberline {3}Elements of an inductive or coinductive definition}{2} ``` lcp@104 ` 4` ```\contentsline {subsection}{\numberline {3.1}The form of the introduction rules}{2} ``` lcp@104 ` 5` ```\contentsline {subsection}{\numberline {3.2}The fixedpoint definitions}{3} ``` lcp@294 ` 6` ```\contentsline {subsection}{\numberline {3.3}Mutual recursion}{3} ``` lcp@104 ` 7` ```\contentsline {subsection}{\numberline {3.4}Proving the introduction rules}{4} ``` lcp@104 ` 8` ```\contentsline {subsection}{\numberline {3.5}The elimination rule}{4} ``` lcp@294 ` 9` ```\contentsline {section}{\numberline {4}Induction and coinduction rules}{4} ``` lcp@294 ` 10` ```\contentsline {subsection}{\numberline {4.1}The basic induction rule}{4} ``` lcp@104 ` 11` ```\contentsline {subsection}{\numberline {4.2}Mutual induction}{5} ``` lcp@294 ` 12` ```\contentsline {subsection}{\numberline {4.3}Coinduction}{5} ``` lcp@294 ` 13` ```\contentsline {section}{\numberline {5}Examples of inductive and coinductive definitions}{6} ``` lcp@294 ` 14` ```\contentsline {subsection}{\numberline {5.1}The finite set operator}{6} ``` lcp@294 ` 15` ```\contentsline {subsection}{\numberline {5.2}Lists of \$n\$ elements}{6} ``` lcp@294 ` 16` ```\contentsline {subsection}{\numberline {5.3}A coinductive definition: bisimulations on lazy lists}{7} ``` lcp@294 ` 17` ```\contentsline {subsection}{\numberline {5.4}The accessible part of a relation}{8} ``` lcp@294 ` 18` ```\contentsline {subsection}{\numberline {5.5}The primitive recursive functions}{9} ``` lcp@294 ` 19` ```\contentsline {section}{\numberline {6}Datatypes and codatatypes}{11} ``` lcp@294 ` 20` ```\contentsline {subsection}{\numberline {6.1}Constructors and their domain}{11} ``` lcp@294 ` 21` ```\contentsline {subsection}{\numberline {6.2}The case analysis operator}{11} ``` lcp@294 ` 22` ```\contentsline {section}{\numberline {7}Conclusions and future work}{12} ```