doc-src/ind-defs.toc
author paulson
Thu, 05 Jun 1997 13:22:25 +0200
changeset 3403 6cc663f6d62e
parent 294 058343877e3a
permissions -rw-r--r--
A slight simplification of optstring The new "simpset" keyword in the "recdef" declaration
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     1
\contentsline {section}{\numberline {1}Introduction}{1}
294
058343877e3a final CADE version
lcp
parents: 104
diff changeset
     2
\contentsline {section}{\numberline {2}Fixedpoint operators}{1}
058343877e3a final CADE version
lcp
parents: 104
diff changeset
     3
\contentsline {section}{\numberline {3}Elements of an inductive or coinductive definition}{2}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     4
\contentsline {subsection}{\numberline {3.1}The form of the introduction rules}{2}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     5
\contentsline {subsection}{\numberline {3.2}The fixedpoint definitions}{3}
294
058343877e3a final CADE version
lcp
parents: 104
diff changeset
     6
\contentsline {subsection}{\numberline {3.3}Mutual recursion}{3}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     7
\contentsline {subsection}{\numberline {3.4}Proving the introduction rules}{4}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     8
\contentsline {subsection}{\numberline {3.5}The elimination rule}{4}
294
058343877e3a final CADE version
lcp
parents: 104
diff changeset
     9
\contentsline {section}{\numberline {4}Induction and coinduction rules}{4}
058343877e3a final CADE version
lcp
parents: 104
diff changeset
    10
\contentsline {subsection}{\numberline {4.1}The basic induction rule}{4}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    11
\contentsline {subsection}{\numberline {4.2}Mutual induction}{5}
294
058343877e3a final CADE version
lcp
parents: 104
diff changeset
    12
\contentsline {subsection}{\numberline {4.3}Coinduction}{5}
058343877e3a final CADE version
lcp
parents: 104
diff changeset
    13
\contentsline {section}{\numberline {5}Examples of inductive and coinductive definitions}{6}
058343877e3a final CADE version
lcp
parents: 104
diff changeset
    14
\contentsline {subsection}{\numberline {5.1}The finite set operator}{6}
058343877e3a final CADE version
lcp
parents: 104
diff changeset
    15
\contentsline {subsection}{\numberline {5.2}Lists of $n$ elements}{6}
058343877e3a final CADE version
lcp
parents: 104
diff changeset
    16
\contentsline {subsection}{\numberline {5.3}A coinductive definition: bisimulations on lazy lists}{7}
058343877e3a final CADE version
lcp
parents: 104
diff changeset
    17
\contentsline {subsection}{\numberline {5.4}The accessible part of a relation}{8}
058343877e3a final CADE version
lcp
parents: 104
diff changeset
    18
\contentsline {subsection}{\numberline {5.5}The primitive recursive functions}{9}
058343877e3a final CADE version
lcp
parents: 104
diff changeset
    19
\contentsline {section}{\numberline {6}Datatypes and codatatypes}{11}
058343877e3a final CADE version
lcp
parents: 104
diff changeset
    20
\contentsline {subsection}{\numberline {6.1}Constructors and their domain}{11}
058343877e3a final CADE version
lcp
parents: 104
diff changeset
    21
\contentsline {subsection}{\numberline {6.2}The case analysis operator}{11}
058343877e3a final CADE version
lcp
parents: 104
diff changeset
    22
\contentsline {section}{\numberline {7}Conclusions and future work}{12}