clarified current 'primrec' vs. old 'recdef';
updated examples from src/HOL/Induct;

--- a/doc-src/HOL/HOL.tex	Thu May 26 14:24:26 2011 +0200
+++ b/doc-src/HOL/HOL.tex	Thu May 26 15:56:39 2011 +0200
@@ -1589,7 +1589,7 @@
 \texttt{split_if} (see~{\S}\ref{subsec:HOL:case:splitting}).
 
 \texttt{List} provides a basic library of list processing functions defined by
-primitive recursion (see~{\S}\ref{sec:HOL:primrec}).  The recursion equations
+primitive recursion.  The recursion equations
 are shown in Figs.\ts\ref{fig:HOL:list-simps} and~\ref{fig:HOL:list-simps2}.
 
 \index{list@{\textit{list}} type|)}
@@ -1938,229 +1938,21 @@
 and \texttt{simps} are contained in a separate structure named $t@1_\ldots_t@n$.
 
 
-\section{Recursive function definitions}\label{sec:HOL:recursive}
-\index{recursive functions|see{recursion}}
-
-Isabelle/HOL provides two main mechanisms of defining recursive functions.
-\begin{enumerate}
-\item \textbf{Primitive recursion} is available only for datatypes, and it is
-  somewhat restrictive.  Recursive calls are only allowed on the argument's
-  immediate constituents.  On the other hand, it is the form of recursion most
-  often wanted, and it is easy to use.
-  
-\item \textbf{Well-founded recursion} requires that you supply a well-founded
-  relation that governs the recursion.  Recursive calls are only allowed if
-  they make the argument decrease under the relation.  Complicated recursion
-  forms, such as nested recursion, can be dealt with.  Termination can even be
-  proved at a later time, though having unsolved termination conditions around
-  can make work difficult.%
-  \footnote{This facility is based on Konrad Slind's TFL
-    package~\cite{slind-tfl}.  Thanks are due to Konrad for implementing TFL
-    and assisting with its installation.}
-\end{enumerate}
-
-Following good HOL tradition, these declarations do not assert arbitrary
-axioms.  Instead, they define the function using a recursion operator.  Both
-HOL and ZF derive the theory of well-founded recursion from first
-principles~\cite{paulson-set-II}.  Primitive recursion over some datatype
-relies on the recursion operator provided by the datatype package.  With
-either form of function definition, Isabelle proves the desired recursion
-equations as theorems.
-
-
-\subsection{Primitive recursive functions}
-\label{sec:HOL:primrec}
-\index{recursion!primitive|(}
-\index{*primrec|(}
-
-Datatypes come with a uniform way of defining functions, {\bf primitive
-  recursion}.  In principle, one could introduce primitive recursive functions
-by asserting their reduction rules as new axioms, but this is not recommended:
-\begin{ttbox}\slshape
-Append = Main +
-consts app :: ['a list, 'a list] => 'a list
-rules 
-   app_Nil   "app [] ys = ys"
-   app_Cons  "app (x#xs) ys = x#app xs ys"
-end
-\end{ttbox}
-Asserting axioms brings the danger of accidentally asserting nonsense, as
-in \verb$app [] ys = us$.
-
-The \ttindex{primrec} declaration is a safe means of defining primitive
-recursive functions on datatypes:
-\begin{ttbox}
-Append = Main +
-consts app :: ['a list, 'a list] => 'a list
-primrec
-   "app [] ys = ys"
-   "app (x#xs) ys = x#app xs ys"
-end
-\end{ttbox}
-Isabelle will now check that the two rules do indeed form a primitive
-recursive definition.  For example
-\begin{ttbox}
-primrec
-    "app [] ys = us"
-\end{ttbox}
-is rejected with an error message ``\texttt{Extra variables on rhs}''.
-
-\bigskip
-
-The general form of a primitive recursive definition is
-\begin{ttbox}
-primrec
-    {\it reduction rules}
-\end{ttbox}
-where \textit{reduction rules} specify one or more equations of the form
-\[ f \, x@1 \, \dots \, x@m \, (C \, y@1 \, \dots \, y@k) \, z@1 \,
-\dots \, z@n = r \] such that $C$ is a constructor of the datatype, $r$
-contains only the free variables on the left-hand side, and all recursive
-calls in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$.  There
-must be at most one reduction rule for each constructor.  The order is
-immaterial.  For missing constructors, the function is defined to return a
-default value.  
-
-If you would like to refer to some rule by name, then you must prefix
-the rule with an identifier.  These identifiers, like those in the
-\texttt{rules} section of a theory, will be visible at the \ML\ level.
-
-The primitive recursive function can have infix or mixfix syntax:
-\begin{ttbox}\underscoreon
-consts "@"  :: ['a list, 'a list] => 'a list  (infixr 60)
-primrec
-   "[] @ ys = ys"
-   "(x#xs) @ ys = x#(xs @ ys)"
-\end{ttbox}
-
-The reduction rules become part of the default simpset, which
-leads to short proof scripts:
-\begin{ttbox}\underscoreon
-Goal "(xs @ ys) @ zs = xs @ (ys @ zs)";
-by (induct\_tac "xs" 1);
-by (ALLGOALS Asm\_simp\_tac);
-\end{ttbox}
-
-\subsubsection{Example: Evaluation of expressions}
-Using mutual primitive recursion, we can define evaluation functions \texttt{evala}
-and \texttt{eval_bexp} for the datatypes of arithmetic and boolean expressions mentioned in
-{\S}\ref{subsec:datatype:basics}:
-\begin{ttbox}
-consts
-  evala :: "['a => nat, 'a aexp] => nat"
-  evalb :: "['a => nat, 'a bexp] => bool"
-
-primrec
-  "evala env (If_then_else b a1 a2) =
-     (if evalb env b then evala env a1 else evala env a2)"
-  "evala env (Sum a1 a2) = evala env a1 + evala env a2"
-  "evala env (Diff a1 a2) = evala env a1 - evala env a2"
-  "evala env (Var v) = env v"
-  "evala env (Num n) = n"
-
-  "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
-  "evalb env (And b1 b2) = (evalb env b1 & evalb env b2)"
-  "evalb env (Or b1 b2) = (evalb env b1 & evalb env b2)"
-\end{ttbox}
-Since the value of an expression depends on the value of its variables,
-the functions \texttt{evala} and \texttt{evalb} take an additional
-parameter, an {\em environment} of type \texttt{'a => nat}, which maps
-variables to their values.
-
-Similarly, we may define substitution functions \texttt{substa}
-and \texttt{substb} for expressions: The mapping \texttt{f} of type
-\texttt{'a => 'a aexp} given as a parameter is lifted canonically
-on the types \texttt{'a aexp} and \texttt{'a bexp}:
-\begin{ttbox}
-consts
-  substa :: "['a => 'b aexp, 'a aexp] => 'b aexp"
-  substb :: "['a => 'b aexp, 'a bexp] => 'b bexp"
-
-primrec
-  "substa f (If_then_else b a1 a2) =
-     If_then_else (substb f b) (substa f a1) (substa f a2)"
-  "substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)"
-  "substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)"
-  "substa f (Var v) = f v"
-  "substa f (Num n) = Num n"
-
-  "substb f (Less a1 a2) = Less (substa f a1) (substa f a2)"
-  "substb f (And b1 b2) = And (substb f b1) (substb f b2)"
-  "substb f (Or b1 b2) = Or (substb f b1) (substb f b2)"
-\end{ttbox}
-In textbooks about semantics one often finds {\em substitution theorems},
-which express the relationship between substitution and evaluation. For
-\texttt{'a aexp} and \texttt{'a bexp}, we can prove such a theorem by mutual
-induction, followed by simplification:
-\begin{ttbox}
-Goal
-  "evala env (substa (Var(v := a')) a) =
-     evala (env(v := evala env a')) a &
-   evalb env (substb (Var(v := a')) b) =
-     evalb (env(v := evala env a')) b";
-by (induct_tac "a b" 1);
-by (ALLGOALS Asm_full_simp_tac);
-\end{ttbox}
-
-\subsubsection{Example: A substitution function for terms}
-Functions on datatypes with nested recursion, such as the type
-\texttt{term} mentioned in {\S}\ref{subsec:datatype:basics}, are
-also defined by mutual primitive recursion. A substitution
-function \texttt{subst_term} on type \texttt{term}, similar to the functions
-\texttt{substa} and \texttt{substb} described above, can
-be defined as follows:
-\begin{ttbox}
-consts
-  subst_term :: "['a => ('a,'b) term, ('a,'b) term] => ('a,'b) term"
-  subst_term_list ::
-    "['a => ('a,'b) term, ('a,'b) term list] => ('a,'b) term list"
-
-primrec
-  "subst_term f (Var a) = f a"
-  "subst_term f (App b ts) = App b (subst_term_list f ts)"
-
-  "subst_term_list f [] = []"
-  "subst_term_list f (t # ts) =
-     subst_term f t # subst_term_list f ts"
-\end{ttbox}
-The recursion scheme follows the structure of the unfolded definition of type
-\texttt{term} shown in {\S}\ref{subsec:datatype:basics}. To prove properties of
-this substitution function, mutual induction is needed:
-\begin{ttbox}
-Goal
-  "(subst_term ((subst_term f1) o f2) t) =
-     (subst_term f1 (subst_term f2 t)) &
-   (subst_term_list ((subst_term f1) o f2) ts) =
-     (subst_term_list f1 (subst_term_list f2 ts))";
-by (induct_tac "t ts" 1);
-by (ALLGOALS Asm_full_simp_tac);
-\end{ttbox}
-
-\subsubsection{Example: A map function for infinitely branching trees}
-Defining functions on infinitely branching datatypes by primitive
-recursion is just as easy. For example, we can define a function
-\texttt{map_tree} on \texttt{'a tree} as follows:
-\begin{ttbox}
-consts
-  map_tree :: "('a => 'b) => 'a tree => 'b tree"
-
-primrec
-  "map_tree f (Atom a) = Atom (f a)"
-  "map_tree f (Branch ts) = Branch (\%x. map_tree f (ts x))"
-\end{ttbox}
-Note that all occurrences of functions such as \texttt{ts} in the
-\texttt{primrec} clauses must be applied to an argument. In particular,
-\texttt{map_tree f o ts} is not allowed.
-
-\index{recursion!primitive|)}
-\index{*primrec|)}
-
-
-\subsection{General recursive functions}
-\label{sec:HOL:recdef}
+\section{Old-style recursive function definitions}\label{sec:HOL:recursive}
 \index{recursion!general|(}
 \index{*recdef|(}
 
+Old-style recursive definitions via \texttt{recdef} requires that you
+supply a well-founded relation that governs the recursion.  Recursive
+calls are only allowed if they make the argument decrease under the
+relation.  Complicated recursion forms, such as nested recursion, can
+be dealt with.  Termination can even be proved at a later time, though
+having unsolved termination conditions around can make work
+difficult.%
+\footnote{This facility is based on Konrad Slind's TFL
+  package~\cite{slind-tfl}.  Thanks are due to Konrad for implementing
+  TFL and assisting with its installation.}
+
 Using \texttt{recdef}, you can declare functions involving nested recursion
 and pattern-matching.  Recursion need not involve datatypes and there are few
 syntactic restrictions.  Termination is proved by showing that each recursive

--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu May 26 14:24:26 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu May 26 15:56:39 2011 +0200
@@ -171,7 +171,30 @@
   \begin{description}
 
   \item @{command (HOL) "primrec"} defines primitive recursive
-  functions over datatypes, see also \cite{isabelle-HOL}.
+  functions over datatypes (see also @{command_ref (HOL) datatype} and
+  @{command_ref (HOL) rep_datatype}).  The given @{text equations}
+  specify reduction rules that are produced by instantiating the
+  generic combinator for primitive recursion that is available for
+  each datatype.
+
+  Each equation needs to be of the form:
+
+  @{text [display] "f x\<^sub>1 \<dots> x\<^sub>m (C y\<^sub>1 \<dots> y\<^sub>k) z\<^sub>1 \<dots> z\<^sub>n = rhs"}
+
+  such that @{text C} is a datatype constructor, @{text rhs} contains
+  only the free variables on the left-hand side (or from the context),
+  and all recursive occurrences of @{text "f"} in @{text "rhs"} are of
+  the form @{text "f \<dots> y\<^sub>i \<dots>"} for some @{text i}.  At most one
+  reduction rule for each constructor can be given.  The order does
+  not matter.  For missing constructors, the function is defined to
+  return a default value, but this equation is made difficult to
+  access for users.
+
+  The reduction rules are declared as @{attribute simp} by default,
+  which enables standard proof methods like @{method simp} and
+  @{method auto} to normalize expressions of @{text "f"} applied to
+  datatype constructions, by simulating symbolic computation via
+  rewriting.
 
   \item @{command (HOL) "function"} defines functions by general
   wellfounded recursion. A detailed description with examples can be
@@ -200,15 +223,12 @@
   \end{description}
 
   Recursive definitions introduced by the @{command (HOL) "function"}
-  command accommodate
-  reasoning by induction (cf.\ \secref{sec:cases-induct}): rule @{text
-  "c.induct"} (where @{text c} is the name of the function definition)
-  refers to a specific induction rule, with parameters named according
-  to the user-specified equations. Cases are numbered (starting from 1).
-
-  For @{command (HOL) "primrec"}, the induction principle coincides
-  with structural recursion on the datatype the recursion is carried
-  out.
+  command accommodate reasoning by induction (cf.\ @{method induct}):
+  rule @{text "f.induct"} refers to a specific induction rule, with
+  parameters named according to the user-specified equations. Cases
+  are numbered starting from 1.  For @{command (HOL) "primrec"}, the
+  induction principle coincides with structural recursion on the
+  datatype where the recursion is carried out.
 
   The equations provided by these packages may be referred later as
   theorem list @{text "f.simps"}, where @{text f} is the (collective)
@@ -237,6 +257,129 @@
   \end{description}
 *}
 
+subsubsection {* Example: evaluation of expressions *}
+
+text {* Subsequently, we define mutual datatypes for arithmetic and
+  boolean expressions, and use @{command primrec} for evaluation
+  functions that follow the same recursive structure. *}
+
+datatype 'a aexp =
+    IF "'a bexp"  "'a aexp"  "'a aexp"
+  | Sum "'a aexp"  "'a aexp"
+  | Diff "'a aexp"  "'a aexp"
+  | Var 'a
+  | Num nat
+and 'a bexp =
+    Less "'a aexp"  "'a aexp"
+  | And "'a bexp"  "'a bexp"
+  | Neg "'a bexp"
+
+
+text {* \medskip Evaluation of arithmetic and boolean expressions *}
+
+primrec evala :: "('a \<Rightarrow> nat) \<Rightarrow> 'a aexp \<Rightarrow> nat"
+  and evalb :: "('a \<Rightarrow> nat) \<Rightarrow> 'a bexp \<Rightarrow> bool"
+where
+  "evala env (IF b a1 a2) = (if evalb env b then evala env a1 else evala env a2)"
+| "evala env (Sum a1 a2) = evala env a1 + evala env a2"
+| "evala env (Diff a1 a2) = evala env a1 - evala env a2"
+| "evala env (Var v) = env v"
+| "evala env (Num n) = n"
+| "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
+| "evalb env (And b1 b2) = (evalb env b1 \<and> evalb env b2)"
+| "evalb env (Neg b) = (\<not> evalb env b)"
+
+text {* Since the value of an expression depends on the value of its
+  variables, the functions @{const evala} and @{const evalb} take an
+  additional parameter, an \emph{environment} that maps variables to
+  their values.
+
+  \medskip Substitution on expressions can be defined similarly.  The
+  mapping @{text f} of type @{typ "'a \<Rightarrow> 'a aexp"} given as a
+  parameter is lifted canonically on the types @{typ "'a aexp"} and
+  @{typ "'a bexp"}, respectively.
+*}
+
+primrec substa :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a aexp \<Rightarrow> 'b aexp"
+  and substb :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a bexp \<Rightarrow> 'b bexp"
+where
+  "substa f (IF b a1 a2) = IF (substb f b) (substa f a1) (substa f a2)"
+| "substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)"
+| "substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)"
+| "substa f (Var v) = f v"
+| "substa f (Num n) = Num n"
+| "substb f (Less a1 a2) = Less (substa f a1) (substa f a2)"
+| "substb f (And b1 b2) = And (substb f b1) (substb f b2)"
+| "substb f (Neg b) = Neg (substb f b)"
+
+text {* In textbooks about semantics one often finds substitution
+  theorems, which express the relationship between substitution and
+  evaluation.  For @{typ "'a aexp"} and @{typ "'a bexp"}, we can prove
+  such a theorem by mutual induction, followed by simplification.
+*}
+
+lemma subst_one:
+  "evala env (substa (Var (v := a')) a) = evala (env (v := evala env a')) a"
+  "evalb env (substb (Var (v := a')) b) = evalb (env (v := evala env a')) b"
+  by (induct a and b) simp_all
+
+lemma subst_all:
+  "evala env (substa s a) = evala (\<lambda>x. evala env (s x)) a"
+  "evalb env (substb s b) = evalb (\<lambda>x. evala env (s x)) b"
+  by (induct a and b) simp_all
+
+
+subsubsection {* Example: a substitution function for terms *}
+
+text {* Functions on datatypes with nested recursion are also defined
+  by mutual primitive recursion. *}
+
+datatype ('a, 'b) "term" = Var 'a | App 'b "('a, 'b) term list"
+
+text {* A substitution function on type @{typ "('a, 'b) term"} can be
+  defined as follows, by working simultaneously on @{typ "('a, 'b)
+  term list"}: *}
+
+primrec subst_term :: "('a \<Rightarrow> ('a, 'b) term) \<Rightarrow> ('a, 'b) term \<Rightarrow> ('a, 'b) term" and
+  subst_term_list :: "('a \<Rightarrow> ('a, 'b) term) \<Rightarrow> ('a, 'b) term list \<Rightarrow> ('a, 'b) term list"
+where
+  "subst_term f (Var a) = f a"
+| "subst_term f (App b ts) = App b (subst_term_list f ts)"
+| "subst_term_list f [] = []"
+| "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
+
+text {* The recursion scheme follows the structure of the unfolded
+  definition of type @{typ "('a, 'b) term"}.  To prove properties of this
+  substitution function, mutual induction is needed:
+*}
+
+lemma "subst_term (subst_term f1 \<circ> f2) t = subst_term f1 (subst_term f2 t)" and
+  "subst_term_list (subst_term f1 \<circ> f2) ts = subst_term_list f1 (subst_term_list f2 ts)"
+  by (induct t and ts) simp_all
+
+
+subsubsection {* Example: a map function for infinitely branching trees *}
+
+text {* Defining functions on infinitely branching datatypes by
+  primitive recursion is just as easy.
+*}
+
+datatype 'a tree = Atom 'a | Branch "nat \<Rightarrow> 'a tree"
+
+primrec map_tree :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a tree \<Rightarrow> 'b tree"
+where
+  "map_tree f (Atom a) = Atom (f a)"
+| "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
+
+text {* Note that all occurrences of functions such as @{text ts}
+  above must be applied to an argument.  In particular, @{term
+  "map_tree f \<circ> ts"} is not allowed here. *}
+
+text {* Here is a simple composition lemma for @{term map_tree}: *}
+
+lemma "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
+  by (induct t) simp_all
+
 
 subsection {* Proof methods related to recursive definitions *}
 

--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu May 26 14:24:26 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu May 26 15:56:39 2011 +0200
@@ -288,7 +288,32 @@
   \begin{description}
 
   \item \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} defines primitive recursive
-  functions over datatypes, see also \cite{isabelle-HOL}.
+  functions over datatypes (see also \indexref{HOL}{command}{datatype}\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}} and
+  \indexref{HOL}{command}{rep\_datatype}\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isaliteral{5F}{\isacharunderscore}}datatype}}}}).  The given \isa{equations}
+  specify reduction rules that are produced by instantiating the
+  generic combinator for primitive recursion that is available for
+  each datatype.
+
+  Each equation needs to be of the form:
+
+  \begin{isabelle}%
+{\isaliteral{22}{\isachardoublequote}}f\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m\ {\isaliteral{28}{\isacharparenleft}}C\ y\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ y\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{29}{\isacharparenright}}\ z\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ z\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{3D}{\isacharequal}}\ rhs{\isaliteral{22}{\isachardoublequote}}%
+\end{isabelle}
+
+  such that \isa{C} is a datatype constructor, \isa{rhs} contains
+  only the free variables on the left-hand side (or from the context),
+  and all recursive occurrences of \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{22}{\isachardoublequote}}} in \isa{{\isaliteral{22}{\isachardoublequote}}rhs{\isaliteral{22}{\isachardoublequote}}} are of
+  the form \isa{{\isaliteral{22}{\isachardoublequote}}f\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ y\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} for some \isa{i}.  At most one
+  reduction rule for each constructor can be given.  The order does
+  not matter.  For missing constructors, the function is defined to
+  return a default value, but this equation is made difficult to
+  access for users.
+
+  The reduction rules are declared as \hyperlink{attribute.simp}{\mbox{\isa{simp}}} by default,
+  which enables standard proof methods like \hyperlink{method.simp}{\mbox{\isa{simp}}} and
+  \hyperlink{method.auto}{\mbox{\isa{auto}}} to normalize expressions of \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{22}{\isachardoublequote}}} applied to
+  datatype constructions, by simulating symbolic computation via
+  rewriting.
 
   \item \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} defines functions by general
   wellfounded recursion. A detailed description with examples can be
@@ -316,14 +341,12 @@
   \end{description}
 
   Recursive definitions introduced by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}
-  command accommodate
-  reasoning by induction (cf.\ \secref{sec:cases-induct}): rule \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{2E}{\isachardot}}induct{\isaliteral{22}{\isachardoublequote}}} (where \isa{c} is the name of the function definition)
-  refers to a specific induction rule, with parameters named according
-  to the user-specified equations. Cases are numbered (starting from 1).
-
-  For \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}, the induction principle coincides
-  with structural recursion on the datatype the recursion is carried
-  out.
+  command accommodate reasoning by induction (cf.\ \hyperlink{method.induct}{\mbox{\isa{induct}}}):
+  rule \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{2E}{\isachardot}}induct{\isaliteral{22}{\isachardoublequote}}} refers to a specific induction rule, with
+  parameters named according to the user-specified equations. Cases
+  are numbered starting from 1.  For \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}, the
+  induction principle coincides with structural recursion on the
+  datatype where the recursion is carried out.
 
   The equations provided by these packages may be referred later as
   theorem list \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{2E}{\isachardot}}simps{\isaliteral{22}{\isachardoublequote}}}, where \isa{f} is the (collective)
@@ -353,6 +376,205 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\isamarkupsubsubsection{Example: evaluation of expressions%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Subsequently, we define mutual datatypes for arithmetic and
+  boolean expressions, and use \hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}} for evaluation
+  functions that follow the same recursive structure.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{datatype}\isamarkupfalse%
+\ {\isaliteral{27}{\isacharprime}}a\ aexp\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ \ \ IF\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ bexp{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ {\isaliteral{7C}{\isacharbar}}\ Sum\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ {\isaliteral{7C}{\isacharbar}}\ Diff\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ {\isaliteral{7C}{\isacharbar}}\ Var\ {\isaliteral{27}{\isacharprime}}a\isanewline
+\ \ {\isaliteral{7C}{\isacharbar}}\ Num\ nat\isanewline
+\isakeyword{and}\ {\isaliteral{27}{\isacharprime}}a\ bexp\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ \ \ Less\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ {\isaliteral{7C}{\isacharbar}}\ And\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ bexp{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ bexp{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ {\isaliteral{7C}{\isacharbar}}\ Neg\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ bexp{\isaliteral{22}{\isachardoublequoteclose}}%
+\begin{isamarkuptext}%
+\medskip Evaluation of arithmetic and boolean expressions%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{primrec}\isamarkupfalse%
+\ evala\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ aexp\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \isakeyword{and}\ evalb\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ bexp\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isakeyword{where}\isanewline
+\ \ {\isaliteral{22}{\isachardoublequoteopen}}evala\ env\ {\isaliteral{28}{\isacharparenleft}}IF\ b\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ evalb\ env\ b\ then\ evala\ env\ a{\isadigit{1}}\ else\ evala\ env\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}evala\ env\ {\isaliteral{28}{\isacharparenleft}}Sum\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ evala\ env\ a{\isadigit{1}}\ {\isaliteral{2B}{\isacharplus}}\ evala\ env\ a{\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}evala\ env\ {\isaliteral{28}{\isacharparenleft}}Diff\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ evala\ env\ a{\isadigit{1}}\ {\isaliteral{2D}{\isacharminus}}\ evala\ env\ a{\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}evala\ env\ {\isaliteral{28}{\isacharparenleft}}Var\ v{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ env\ v{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}evala\ env\ {\isaliteral{28}{\isacharparenleft}}Num\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}evalb\ env\ {\isaliteral{28}{\isacharparenleft}}Less\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}evala\ env\ a{\isadigit{1}}\ {\isaliteral{3C}{\isacharless}}\ evala\ env\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}evalb\ env\ {\isaliteral{28}{\isacharparenleft}}And\ b{\isadigit{1}}\ b{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}evalb\ env\ b{\isadigit{1}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ evalb\ env\ b{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}evalb\ env\ {\isaliteral{28}{\isacharparenleft}}Neg\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ evalb\ env\ b{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+\begin{isamarkuptext}%
+Since the value of an expression depends on the value of its
+  variables, the functions \isa{evala} and \isa{evalb} take an
+  additional parameter, an \emph{environment} that maps variables to
+  their values.
+
+  \medskip Substitution on expressions can be defined similarly.  The
+  mapping \isa{f} of type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequote}}} given as a
+  parameter is lifted canonically on the types \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequote}}} and
+  \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ bexp{\isaliteral{22}{\isachardoublequote}}}, respectively.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{primrec}\isamarkupfalse%
+\ substa\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ aexp{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ aexp\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \isakeyword{and}\ substb\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ aexp{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ bexp\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ bexp{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isakeyword{where}\isanewline
+\ \ {\isaliteral{22}{\isachardoublequoteopen}}substa\ f\ {\isaliteral{28}{\isacharparenleft}}IF\ b\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ IF\ {\isaliteral{28}{\isacharparenleft}}substb\ f\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}substa\ f\ a{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}substa\ f\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}substa\ f\ {\isaliteral{28}{\isacharparenleft}}Sum\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Sum\ {\isaliteral{28}{\isacharparenleft}}substa\ f\ a{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}substa\ f\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}substa\ f\ {\isaliteral{28}{\isacharparenleft}}Diff\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Diff\ {\isaliteral{28}{\isacharparenleft}}substa\ f\ a{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}substa\ f\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}substa\ f\ {\isaliteral{28}{\isacharparenleft}}Var\ v{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ v{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}substa\ f\ {\isaliteral{28}{\isacharparenleft}}Num\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Num\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}substb\ f\ {\isaliteral{28}{\isacharparenleft}}Less\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Less\ {\isaliteral{28}{\isacharparenleft}}substa\ f\ a{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}substa\ f\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}substb\ f\ {\isaliteral{28}{\isacharparenleft}}And\ b{\isadigit{1}}\ b{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ And\ {\isaliteral{28}{\isacharparenleft}}substb\ f\ b{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}substb\ f\ b{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}substb\ f\ {\isaliteral{28}{\isacharparenleft}}Neg\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Neg\ {\isaliteral{28}{\isacharparenleft}}substb\ f\ b{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+\begin{isamarkuptext}%
+In textbooks about semantics one often finds substitution
+  theorems, which express the relationship between substitution and
+  evaluation.  For \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ bexp{\isaliteral{22}{\isachardoublequote}}}, we can prove
+  such a theorem by mutual induction, followed by simplification.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ subst{\isaliteral{5F}{\isacharunderscore}}one{\isaliteral{3A}{\isacharcolon}}\isanewline
+\ \ {\isaliteral{22}{\isachardoublequoteopen}}evala\ env\ {\isaliteral{28}{\isacharparenleft}}substa\ {\isaliteral{28}{\isacharparenleft}}Var\ {\isaliteral{28}{\isacharparenleft}}v\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ evala\ {\isaliteral{28}{\isacharparenleft}}env\ {\isaliteral{28}{\isacharparenleft}}v\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ evala\ env\ a{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ a{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ {\isaliteral{22}{\isachardoublequoteopen}}evalb\ env\ {\isaliteral{28}{\isacharparenleft}}substb\ {\isaliteral{28}{\isacharparenleft}}Var\ {\isaliteral{28}{\isacharparenleft}}v\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ evalb\ {\isaliteral{28}{\isacharparenleft}}env\ {\isaliteral{28}{\isacharparenleft}}v\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ evala\ env\ a{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}induct\ a\ \isakeyword{and}\ b{\isaliteral{29}{\isacharparenright}}\ simp{\isaliteral{5F}{\isacharunderscore}}all%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ subst{\isaliteral{5F}{\isacharunderscore}}all{\isaliteral{3A}{\isacharcolon}}\isanewline
+\ \ {\isaliteral{22}{\isachardoublequoteopen}}evala\ env\ {\isaliteral{28}{\isacharparenleft}}substa\ s\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ evala\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ evala\ env\ {\isaliteral{28}{\isacharparenleft}}s\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ a{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ {\isaliteral{22}{\isachardoublequoteopen}}evalb\ env\ {\isaliteral{28}{\isacharparenleft}}substb\ s\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ evalb\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ evala\ env\ {\isaliteral{28}{\isacharparenleft}}s\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}induct\ a\ \isakeyword{and}\ b{\isaliteral{29}{\isacharparenright}}\ simp{\isaliteral{5F}{\isacharunderscore}}all%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isamarkupsubsubsection{Example: a substitution function for terms%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Functions on datatypes with nested recursion are also defined
+  by mutual primitive recursion.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{datatype}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{22}{\isachardoublequoteopen}}term{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{3D}{\isacharequal}}\ Var\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{7C}{\isacharbar}}\ App\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ term\ list{\isaliteral{22}{\isachardoublequoteclose}}%
+\begin{isamarkuptext}%
+A substitution function on type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ term{\isaliteral{22}{\isachardoublequote}}} can be
+  defined as follows, by working simultaneously on \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ term\ list{\isaliteral{22}{\isachardoublequote}}}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{primrec}\isamarkupfalse%
+\ subst{\isaliteral{5F}{\isacharunderscore}}term\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ term{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ term\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ term{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline
+\ \ subst{\isaliteral{5F}{\isacharunderscore}}term{\isaliteral{5F}{\isacharunderscore}}list\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ term{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ term\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ term\ list{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isakeyword{where}\isanewline
+\ \ {\isaliteral{22}{\isachardoublequoteopen}}subst{\isaliteral{5F}{\isacharunderscore}}term\ f\ {\isaliteral{28}{\isacharparenleft}}Var\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ a{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}subst{\isaliteral{5F}{\isacharunderscore}}term\ f\ {\isaliteral{28}{\isacharparenleft}}App\ b\ ts{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ App\ b\ {\isaliteral{28}{\isacharparenleft}}subst{\isaliteral{5F}{\isacharunderscore}}term{\isaliteral{5F}{\isacharunderscore}}list\ f\ ts{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}subst{\isaliteral{5F}{\isacharunderscore}}term{\isaliteral{5F}{\isacharunderscore}}list\ f\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}subst{\isaliteral{5F}{\isacharunderscore}}term{\isaliteral{5F}{\isacharunderscore}}list\ f\ {\isaliteral{28}{\isacharparenleft}}t\ {\isaliteral{23}{\isacharhash}}\ ts{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ subst{\isaliteral{5F}{\isacharunderscore}}term\ f\ t\ {\isaliteral{23}{\isacharhash}}\ subst{\isaliteral{5F}{\isacharunderscore}}term{\isaliteral{5F}{\isacharunderscore}}list\ f\ ts{\isaliteral{22}{\isachardoublequoteclose}}%
+\begin{isamarkuptext}%
+The recursion scheme follows the structure of the unfolded
+  definition of type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ term{\isaliteral{22}{\isachardoublequote}}}.  To prove properties of this
+  substitution function, mutual induction is needed:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}subst{\isaliteral{5F}{\isacharunderscore}}term\ {\isaliteral{28}{\isacharparenleft}}subst{\isaliteral{5F}{\isacharunderscore}}term\ f{\isadigit{1}}\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ f{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ t\ {\isaliteral{3D}{\isacharequal}}\ subst{\isaliteral{5F}{\isacharunderscore}}term\ f{\isadigit{1}}\ {\isaliteral{28}{\isacharparenleft}}subst{\isaliteral{5F}{\isacharunderscore}}term\ f{\isadigit{2}}\ t{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline
+\ \ {\isaliteral{22}{\isachardoublequoteopen}}subst{\isaliteral{5F}{\isacharunderscore}}term{\isaliteral{5F}{\isacharunderscore}}list\ {\isaliteral{28}{\isacharparenleft}}subst{\isaliteral{5F}{\isacharunderscore}}term\ f{\isadigit{1}}\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ f{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ ts\ {\isaliteral{3D}{\isacharequal}}\ subst{\isaliteral{5F}{\isacharunderscore}}term{\isaliteral{5F}{\isacharunderscore}}list\ f{\isadigit{1}}\ {\isaliteral{28}{\isacharparenleft}}subst{\isaliteral{5F}{\isacharunderscore}}term{\isaliteral{5F}{\isacharunderscore}}list\ f{\isadigit{2}}\ ts{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}induct\ t\ \isakeyword{and}\ ts{\isaliteral{29}{\isacharparenright}}\ simp{\isaliteral{5F}{\isacharunderscore}}all%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isamarkupsubsubsection{Example: a map function for infinitely branching trees%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Defining functions on infinitely branching datatypes by
+  primitive recursion is just as easy.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{datatype}\isamarkupfalse%
+\ {\isaliteral{27}{\isacharprime}}a\ tree\ {\isaliteral{3D}{\isacharequal}}\ Atom\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{7C}{\isacharbar}}\ Branch\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ tree{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isanewline
+\isacommand{primrec}\isamarkupfalse%
+\ map{\isaliteral{5F}{\isacharunderscore}}tree\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ tree\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ tree{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isakeyword{where}\isanewline
+\ \ {\isaliteral{22}{\isachardoublequoteopen}}map{\isaliteral{5F}{\isacharunderscore}}tree\ f\ {\isaliteral{28}{\isacharparenleft}}Atom\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Atom\ {\isaliteral{28}{\isacharparenleft}}f\ a{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}map{\isaliteral{5F}{\isacharunderscore}}tree\ f\ {\isaliteral{28}{\isacharparenleft}}Branch\ ts{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Branch\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ map{\isaliteral{5F}{\isacharunderscore}}tree\ f\ {\isaliteral{28}{\isacharparenleft}}ts\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+\begin{isamarkuptext}%
+Note that all occurrences of functions such as \isa{ts}
+  above must be applied to an argument.  In particular, \isa{{\isaliteral{22}{\isachardoublequote}}map{\isaliteral{5F}{\isacharunderscore}}tree\ f\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ ts{\isaliteral{22}{\isachardoublequote}}} is not allowed here.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Here is a simple composition lemma for \isa{map{\isaliteral{5F}{\isacharunderscore}}tree}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}map{\isaliteral{5F}{\isacharunderscore}}tree\ g\ {\isaliteral{28}{\isacharparenleft}}map{\isaliteral{5F}{\isacharunderscore}}tree\ f\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ map{\isaliteral{5F}{\isacharunderscore}}tree\ {\isaliteral{28}{\isacharparenleft}}g\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ f{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}induct\ t{\isaliteral{29}{\isacharparenright}}\ simp{\isaliteral{5F}{\isacharunderscore}}all%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
 \isamarkupsubsection{Proof methods related to recursive definitions%
 }
 \isamarkuptrue%