\doc{Induction rules}
\ref{induction-rules}
\ref{basis-generators}
\ref{inductive-generators}
\ref{generators}
\ref{generated}
\ref{freely}
\ref{well-founded}

An \def{induction rule} is logically equivalent to an infinite set of formulas,
which justify the use of proofs by induction.

\head{2}{\dlink{../symbols/syntax}{Syntax}}
\begin{verbatim}
\sd{induction-rule} ::= \f{sort} \slink{sort}{sort} \f{generated} [ \f{freely} ] \f{by} \slink{operator}{operator}+,
                       | \f{well founded} \slink{operator}{operator}
\end{verbatim}

\head{2}{Examples}
\begin{verbatim}
sort Nat generated freely by 0, s
sort Set generated by {}, insert
sort Set generated by {}, {__}, \U
well founded <
\end{verbatim}

\head{2}{Usage}

Users can \clink{assert} or \dlink{../proof/of-ir}{prove} induction rules.
\p
Assertions like \fq{sort Nat generated by 0, s} specify sets of generators for
use in \dlink{../proof/by-induction}{proofs by structural induction}.  The
listed operators (e.g, \fq{0} and \fq{s}) must have the named sort (e.g.,
\fq{Nat}) as their range.  If none of the domain sorts of an operator is the 
same as its range sort, the operator is a \def{basis generator} (e.g., \fq{0});
otherwise, it is an \def{inductive generator} (e.g, \fq{s}).  Structural
induction rules are logically equivalent to infinite sets of first-order
formulas of the form
\begin{verbatim}
P(0) /\ \A x (P(x) => P(s(x))) => \A x P(x)
\end{verbatim}
where \f{P} is an arbitrary first-order formula.  
\p
The use of \fq{freely} supplements a structural induction rule with a set of
formulas asserting that the named operators are one-to-one and have disjoint
ranges.  For example, \fq{sort Nat generated freely by 0, s} gives rise to the
formulas \fq{s(x) = s(y) <=> x = y} and \fq{0 ~= s(x)}.
\p
Assertions like \fq{well founded <} specify a binary relation for use in
\dlink{../proof/by-induction}{proofs by well-founded induction}.  The listed 
operator must have a signature of the form \fq{S,S->Bool} for some sort \f{S}.
Well-founded induction rules are logically equivalent to infinite sets of
first-order formulas of the form
\begin{verbatim}
\A x (\A y (y < x => P(y)) => P(x)) => \A x P(x)
\end{verbatim}
where \f{P} is an arbitrary first-order formula.  
\p
To \clink{display} the induction rules that LP currently has available for use,
type \fq{display induction-rules} (or \fq{disp i-r} for short).