doc-src/TutorialI/fp.tex

 Laws about datatypes, such as \isa{[] \isasymnoteq~x\#xs} and
 \isa{(x\#xs = y\#ys) = (x=y \isasymand~xs=ys)}, are used automatically
 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
 time they are defined by what is called \bfindex{primitive recursion}.
 The keyword \isacommand{primrec}\indexbold{*primrec} is followed by a list of

 Note that we do not need to give a lemma a name if we do not intend to refer
 to it explicitly in the future.
 
 \begin{warn}
   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.
 \end{warn}
 
 

 
 \section{Some basic types}
 
 
 \subsection{Natural numbers}
+\label{sec:nat}
 \index{arithmetic|(}
 
 \input{Misc/document/fakenat.tex}
 \input{Misc/document/natsum.tex}
 

 \label{sec:datatype-mut-rec}
 
 \input{Datatype/document/ABexpr.tex}
 
 \subsection{Nested recursion}
-
-\input{Datatype/document/Nested.tex}
+\label{sec:nested-datatype}
+
+{\makeatother\input{Datatype/document/Nested.tex}}
 
 
 \subsection{The limits of nested recursion}
 
 How far can we push nested recursion? By the unfolding argument above, we can

 
 \subsection{Simplification with recdef}
 
 \input{Recdef/document/simplification.tex}
 
-
 \subsection{Induction}
 \index{induction!recursion|(}
 \index{recursion induction|(}
 
 \input{Recdef/document/Induction.tex}
+\label{sec:recdef-induction}
 
 \index{induction!recursion|)}
 \index{recursion induction|)}
+
+%\subsection{Advanced forms of recursion}
+
+%\input{Recdef/document/Nested0.tex}
+%\input{Recdef/document/Nested1.tex}
+
 \index{*recdef|)}
+
+\section{Advanced induction techniques}
+\label{sec:advanced-ind}
+\input{Misc/document/AdvancedInd.tex}
+
+\input{Datatype/document/Nested2.tex}