doc-src/TutorialI/Inductive/inductive.tex
 author paulson Wed, 25 Oct 2000 17:44:59 +0200 changeset 10327 19214ac381cf parent 10242 028f54cd2cc9 child 10371 4015fdd0bcf0 permissions -rw-r--r--
inputs Even.tex
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
 10219 eb28637c72ce *** empty log message *** nipkow parents: diff changeset 1 \chapter{Inductively Defined Sets} 10242 028f54cd2cc9 *** empty log message *** nipkow parents: 10225 diff changeset 2 \index{inductive definition|(} 028f54cd2cc9 *** empty log message *** nipkow parents: 10225 diff changeset 3 \index{*inductive|(} 028f54cd2cc9 *** empty log message *** nipkow parents: 10225 diff changeset 4 028f54cd2cc9 *** empty log message *** nipkow parents: 10225 diff changeset 5 This chapter is dedicated to the most important definition principle after 028f54cd2cc9 *** empty log message *** nipkow parents: 10225 diff changeset 6 recursive functions and datatypes: inductively defined sets. 028f54cd2cc9 *** empty log message *** nipkow parents: 10225 diff changeset 7 10327 19214ac381cf inputs Even.tex paulson parents: 10242 diff changeset 8 We start with a simple example: the set of even numbers. 19214ac381cf inputs Even.tex paulson parents: 10242 diff changeset 9 A slightly more complicated example, the 10242 028f54cd2cc9 *** empty log message *** nipkow parents: 10225 diff changeset 10 reflexive transitive closure, is the subject of {\S}\ref{sec:rtc}. In particular, 028f54cd2cc9 *** empty log message *** nipkow parents: 10225 diff changeset 11 some standard induction heuristics are discussed. To demonstrate the 028f54cd2cc9 *** empty log message *** nipkow parents: 10225 diff changeset 12 versatility of inductive definitions, {\S}\ref{sec:CFG} presents a case study 028f54cd2cc9 *** empty log message *** nipkow parents: 10225 diff changeset 13 from the realm of context-free grammars. The chapter closes with a discussion 028f54cd2cc9 *** empty log message *** nipkow parents: 10225 diff changeset 14 of advanced forms of inductive definitions. 10219 eb28637c72ce *** empty log message *** nipkow parents: diff changeset 15 10327 19214ac381cf inputs Even.tex paulson parents: 10242 diff changeset 16 \input{Inductive/Even} 10225 b9fd52525b69 *** empty log message *** nipkow parents: 10219 diff changeset 17 \input{Inductive/document/Star} 10219 eb28637c72ce *** empty log message *** nipkow parents: diff changeset 18 \input{Inductive/document/AB} 10242 028f54cd2cc9 *** empty log message *** nipkow parents: 10225 diff changeset 19 028f54cd2cc9 *** empty log message *** nipkow parents: 10225 diff changeset 20 \index{inductive definition|)} 028f54cd2cc9 *** empty log message *** nipkow parents: 10225 diff changeset 21 \index{*inductive|)} 028f54cd2cc9 *** empty log message *** nipkow parents: 10225 diff changeset 22 028f54cd2cc9 *** empty log message *** nipkow parents: 10225 diff changeset 23 \section{Advanced inductive definitions}