doc-src/TutorialI/Inductive/inductive.tex

A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.

\chapter{Inductively Defined Sets} \label{chap:inductive}
\index{inductive definitions|(}

This chapter is dedicated to the most important definition principle after
recursive functions and datatypes: inductively defined sets.

We start with a simple example: the set of even numbers.  A slightly more
complicated example, the reflexive transitive closure, is the subject of
{\S}\ref{sec:rtc}. In particular, some standard induction heuristics are
discussed. Advanced forms of inductive definitions are discussed in
{\S}\ref{sec:adv-ind-def}. To demonstrate the versatility of inductive
definitions, the chapter closes with a case study from the realm of
context-free grammars. The first two sections are required reading for anybody
interested in mathematical modelling.

\input{Inductive/even-example}
\input{Inductive/document/Mutual}
\input{Inductive/document/Star}

\section{Advanced Inductive Definitions}
\label{sec:adv-ind-def}
\input{Inductive/advanced-examples}

\input{Inductive/document/AB}

\index{inductive definitions|)}