changeset 9644 6b0b6b471855
parent 9541 d17c0b34d5c8
child 9673 1b2d4f995b13
--- a/doc-src/TutorialI/fp.tex	Thu Aug 17 21:07:25 2000 +0200
+++ b/doc-src/TutorialI/fp.tex	Fri Aug 18 10:34:08 2000 +0200
@@ -185,6 +185,16 @@
 during proofs by simplification.  The same is true for the equations in
 primitive recursive function definitions.
+Every datatype $t$ comes equipped with a \isa{size} function from $t$ into
+the natural numbers (see~\S\ref{sec:nat} below). For lists, \isa{size} is
+just the length, i.e.\ \isa{size [] = 0} and \isa{size(x \# xs) = size xs +
+  1}.  In general, \isa{size} returns \isa{0} for all constructors that do
+not have an argument of type $t$, and for all other constructors \isa{1 +}
+the sum of the sizes of all arguments of type $t$. Note that because
+\isa{size} is defined on every datatype, it is overloaded; on lists
+\isa{size} is also called \isa{length}, which is not overloaded.
 \subsection{Primitive recursion}
 Functions on datatypes are usually defined by recursion. In fact, most of the
@@ -267,7 +277,8 @@
   Induction is only allowed on free (or \isasymAnd-bound) variables that
-  should not occur among the assumptions of the subgoal.  Case distinction
+  should not occur among the assumptions of the subgoal; see
+  \S\ref{sec:ind-var-in-prems} for details. Case distinction
   (\isa{case_tac}) works for arbitrary terms, which need to be
   quoted if they are non-atomic.
@@ -301,6 +312,7 @@
 \subsection{Natural numbers}
@@ -694,8 +706,9 @@
 \subsection{Nested recursion}
 \subsection{The limits of nested recursion}
@@ -828,13 +841,25 @@
 \index{recursion induction|(}
 \index{recursion induction|)}
+%\subsection{Advanced forms of recursion}
+\section{Advanced induction techniques}