# HG changeset patch
# User nipkow
# Date 966587648 -7200
# Node ID 6b0b6b471855b3751d87f21f0efee35091dc0506
# Parent  c94db1a96f4ec43a87aa4cce84cfed9c6949f9ea
*** empty log message ***

diff -r c94db1a96f4e -r 6b0b6b471855 doc-src/TutorialI/Datatype/Fundata.thy
--- a/doc-src/TutorialI/Datatype/Fundata.thy	Thu Aug 17 21:07:25 2000 +0200
+++ b/doc-src/TutorialI/Datatype/Fundata.thy	Fri Aug 18 10:34:08 2000 +0200
@@ -36,7 +36,7 @@
 The following lemma has a canonical proof  *}
 
 lemma "map_bt (g o f) T = map_bt g (map_bt f T)";
-apply(induct_tac "T", auto).
+by(induct_tac "T", auto)
 
 text{*\noindent
 but it is worth taking a look at the proof state after the induction step
diff -r c94db1a96f4e -r 6b0b6b471855 doc-src/TutorialI/Datatype/Nested.thy
--- a/doc-src/TutorialI/Datatype/Nested.thy	Thu Aug 17 21:07:25 2000 +0200
+++ b/doc-src/TutorialI/Datatype/Nested.thy	Fri Aug 18 10:34:08 2000 +0200
@@ -46,12 +46,15 @@
 
 primrec
   "subst s (Var x) = s x"
+  subst_App:
   "subst s (App f ts) = App f (substs s ts)"
 
   "substs s [] = []"
   "substs s (t # ts) = subst s t # substs s ts";
 
 text{*\noindent
+You should ignore the label \isa{subst\_App} for the moment.
+
 Similarly, when proving a statement about terms inductively, we need
 to prove a related statement about term lists simultaneously. For example,
 the fact that the identity substitution does not change a term needs to be
@@ -80,6 +83,69 @@
 strengthen it, and prove it. (Note: \ttindexbold{o} is function composition;
 its definition is found in theorem \isa{o_def}).
 \end{exercise}
+\begin{exercise}\label{ex:trev-trev}
+  Define a function \isa{trev} of type @{typ"('a,'b)term => ('a,'b)term"} that
+  recursively reverses the order of arguments of all function symbols in a
+  term. Prove that \isa{trev(trev t) = t}.
+\end{exercise}
+
+The experienced functional programmer may feel that our above definition of
+\isa{subst} is unnecessarily complicated in that \isa{substs} is completely
+unnecessary. The @{term"App"}-case can be defined directly as
+\begin{quote}
+@{term[display]"subst s (App f ts) = App f (map (subst s) ts)"}
+\end{quote}
+where @{term"map"} is the standard list function such that
+\isa{map f [x1,...,xn] = [f x1,...,f xn]}. This is true, but Isabelle insists
+on the above fixed format. Fortunately, we can easily \emph{prove} that the
+suggested equation holds:
+*}
+
+lemma [simp]: "subst s (App f ts) = App f (map (subst s) ts)"
+by(induct_tac ts, auto)
+
+text{*
+What is more, we can now disable the old defining equation as a
+simplification rule:
+*}
+
+lemmas [simp del] = subst_App
+
+text{*
+The advantage is that now we have replaced @{term"substs"} by @{term"map"},
+we can profit from the large number of pre-proved lemmas about @{term"map"}.
+We illustrate this with an example, reversing terms:
+*}
+
+consts trev  :: "('a,'b)term => ('a,'b)term"
+       trevs :: "('a,'b)term list => ('a,'b)term list"
+primrec   "trev (Var x) = Var x"
+trev_App: "trev (App f ts) = App f (trevs ts)"
+
+          "trevs [] = []"
+          "trevs (t#ts) = trevs ts @ [trev t]"
+
+text{*\noindent
+Following the above methodology, we re-express \isa{trev\_App}:
+*}
+
+lemma [simp]: "trev (App f ts) = App f (rev(map trev ts))"
+by(induct_tac ts, auto)
+lemmas [simp del] = trev_App
+
+text{*\noindent
+Now it becomes quite easy to prove @{term"trev(trev t) = t"}, except that we
+still have to come up with the second half of the conjunction:
+*}
+
+lemma "trev(trev t) = (t::('a,'b)term) &
+        map trev (map trev ts) = (ts::('a,'b)term list)";
+by(induct_tac t and ts, auto simp add:rev_map);
+
+text{*\noindent
+Getting rid of this second conjunct requires deriving a new induction schema
+for \isa{term}, which is beyond what we have learned so far. Please stay
+tuned, we will solve this final problem in \S\ref{sec:der-ind-schemas}.
 
 Of course, you may also combine mutual and nested recursion. For example,
 constructor \isa{Sum} in \S\ref{sec:datatype-mut-rec} could take a list of
diff -r c94db1a96f4e -r 6b0b6b471855 doc-src/TutorialI/Datatype/ROOT.ML
--- a/doc-src/TutorialI/Datatype/ROOT.ML	Thu Aug 17 21:07:25 2000 +0200
+++ b/doc-src/TutorialI/Datatype/ROOT.ML	Fri Aug 18 10:34:08 2000 +0200
@@ -1,4 +1,4 @@
 use_thy "ABexpr";
 use_thy "unfoldnested";
-use_thy "Nested";
+use_thy "Nested2";
 use_thy "Fundata";
diff -r c94db1a96f4e -r 6b0b6b471855 doc-src/TutorialI/Datatype/document/ABexpr.tex
--- a/doc-src/TutorialI/Datatype/document/ABexpr.tex	Thu Aug 17 21:07:25 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex	Fri Aug 18 10:34:08 2000 +0200
@@ -102,7 +102,7 @@
 \end{ttbox}
 
 \begin{exercise}
-  Define a function \isa{norma} of type \isa{'a\ aexp\ {\isasymRightarrow}\ 'a\ aexp} that
+  Define a function \isa{norma} of type \isa{\mbox{'a}\ aexp\ {\isasymRightarrow}\ \mbox{'a}\ aexp} that
   replaces \isa{IF}s with complex boolean conditions by nested
   \isa{IF}s where each condition is a \isa{Less} --- \isa{And} and
   \isa{Neg} should be eliminated completely. Prove that \isa{norma}
diff -r c94db1a96f4e -r 6b0b6b471855 doc-src/TutorialI/Datatype/document/Fundata.tex
--- a/doc-src/TutorialI/Datatype/document/Fundata.tex	Thu Aug 17 21:07:25 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/Fundata.tex	Fri Aug 18 10:34:08 2000 +0200
@@ -11,7 +11,7 @@
 \begin{quote}
 
 \begin{isabelle}%
-Branch\ 0\ ({\isasymlambda}i.\ Branch\ i\ ({\isasymlambda}n.\ Tip))
+Branch\ 0\ ({\isasymlambda}\mbox{i}.\ Branch\ \mbox{i}\ ({\isasymlambda}\mbox{n}.\ Tip))
 \end{isabelle}%
 
 \end{quote}
@@ -29,15 +29,15 @@
 \noindent This is a valid \isacommand{primrec} definition because the
 recursive calls of \isa{map_bt} involve only subtrees obtained from
 \isa{F}, i.e.\ the left-hand side. Thus termination is assured.  The
-seasoned functional programmer might have written \isa{map\_bt\ f\ {\isasymcirc}\ F}
-instead of \isa{{\isasymlambda}i.\ map\_bt\ f\ (F\ i)}, but the former is not accepted by
+seasoned functional programmer might have written \isa{map\_bt\ \mbox{f}\ {\isasymcirc}\ \mbox{F}}
+instead of \isa{{\isasymlambda}\mbox{i}.\ map\_bt\ \mbox{f}\ (\mbox{F}\ \mbox{i})}, but the former is not accepted by
 Isabelle because the termination proof is not as obvious since
 \isa{map_bt} is only partially applied.
 
 The following lemma has a canonical proof%
 \end{isamarkuptext}%
 \isacommand{lemma}\ {"}map\_bt\ (g\ o\ f)\ T\ =\ map\_bt\ g\ (map\_bt\ f\ T){"}\isanewline
-\isacommand{apply}(induct\_tac\ {"}T{"},\ auto)\isacommand{.}%
+\isacommand{by}(induct\_tac\ {"}T{"},\ auto)%
 \begin{isamarkuptext}%
 \noindent
 but it is worth taking a look at the proof state after the induction step
diff -r c94db1a96f4e -r 6b0b6b471855 doc-src/TutorialI/Datatype/document/Nested.tex
--- a/doc-src/TutorialI/Datatype/document/Nested.tex	Thu Aug 17 21:07:25 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex	Fri Aug 18 10:34:08 2000 +0200
@@ -13,7 +13,7 @@
 the command \isacommand{term}.
 Parameter \isa{'a} is the type of variables and \isa{'b} the type of
 function symbols.
-A mathematical term like $f(x,g(y))$ becomes \isa{App\ f\ [Var\ x,\ App\ g\ [Var\ y]]}, where \isa{f}, \isa{g}, \isa{x}, \isa{y} are
+A mathematical term like $f(x,g(y))$ becomes \isa{App\ \mbox{f}\ [Var\ \mbox{x},\ App\ \mbox{g}\ [Var\ \mbox{y}]]}, where \isa{f}, \isa{g}, \isa{x}, \isa{y} are
 suitable values, e.g.\ numbers or strings.
 
 What complicates the definition of \isa{term} is the nested occurrence of
@@ -41,12 +41,15 @@
 \isanewline
 \isacommand{primrec}\isanewline
 \ \ {"}subst\ s\ (Var\ x)\ =\ s\ x{"}\isanewline
+\ \ subst\_App:\isanewline
 \ \ {"}subst\ s\ (App\ f\ ts)\ =\ App\ f\ (substs\ s\ ts){"}\isanewline
 \isanewline
 \ \ {"}substs\ s\ []\ =\ []{"}\isanewline
 \ \ {"}substs\ s\ (t\ \#\ ts)\ =\ subst\ s\ t\ \#\ substs\ s\ ts{"}%
 \begin{isamarkuptext}%
 \noindent
+You should ignore the label \isa{subst\_App} for the moment.
+
 Similarly, when proving a statement about terms inductively, we need
 to prove a related statement about term lists simultaneously. For example,
 the fact that the identity substitution does not change a term needs to be
@@ -58,7 +61,7 @@
 \begin{isamarkuptext}%
 \noindent
 Note that \isa{Var} is the identity substitution because by definition it
-leaves variables unchanged: \isa{subst\ Var\ (Var\ x)\ =\ Var\ x}. Note also
+leaves variables unchanged: \isa{subst\ Var\ (Var\ \mbox{x})\ =\ Var\ \mbox{x}}. Note also
 that the type annotations are necessary because otherwise there is nothing in
 the goal to enforce that both halves of the goal talk about the same type
 parameters \isa{('a,'b)}. As a result, induction would fail
@@ -74,6 +77,66 @@
 strengthen it, and prove it. (Note: \ttindexbold{o} is function composition;
 its definition is found in theorem \isa{o_def}).
 \end{exercise}
+\begin{exercise}\label{ex:trev-trev}
+  Define a function \isa{trev} of type \isa{(\mbox{'a},\ \mbox{'b})\ term\ {\isasymRightarrow}\ (\mbox{'a},\ \mbox{'b})\ term} that
+  recursively reverses the order of arguments of all function symbols in a
+  term. Prove that \isa{trev(trev t) = t}.
+\end{exercise}
+
+The experienced functional programmer may feel that our above definition of
+\isa{subst} is unnecessarily complicated in that \isa{substs} is completely
+unnecessary. The \isa{App}-case can be defined directly as
+\begin{quote}
+
+\begin{isabelle}%
+subst\ \mbox{s}\ (App\ \mbox{f}\ \mbox{ts})\ =\ App\ \mbox{f}\ (map\ (subst\ \mbox{s})\ \mbox{ts})
+\end{isabelle}%
+
+\end{quote}
+where \isa{map} is the standard list function such that
+\isa{map f [x1,...,xn] = [f x1,...,f xn]}. This is true, but Isabelle insists
+on the above fixed format. Fortunately, we can easily \emph{prove} that the
+suggested equation holds:%
+\end{isamarkuptext}%
+\isacommand{lemma}\ [simp]:\ {"}subst\ s\ (App\ f\ ts)\ =\ App\ f\ (map\ (subst\ s)\ ts){"}\isanewline
+\isacommand{by}(induct\_tac\ ts,\ auto)%
+\begin{isamarkuptext}%
+What is more, we can now disable the old defining equation as a
+simplification rule:%
+\end{isamarkuptext}%
+\isacommand{lemmas}\ [simp\ del]\ =\ subst\_App%
+\begin{isamarkuptext}%
+The advantage is that now we have replaced \isa{substs} by \isa{map},
+we can profit from the large number of pre-proved lemmas about \isa{map}.
+We illustrate this with an example, reversing terms:%
+\end{isamarkuptext}%
+\isacommand{consts}\ trev\ \ ::\ {"}('a,'b)term\ =>\ ('a,'b)term{"}\isanewline
+\ \ \ \ \ \ \ trevs\ ::\ {"}('a,'b)term\ list\ =>\ ('a,'b)term\ list{"}\isanewline
+\isacommand{primrec}\ \ \ {"}trev\ (Var\ x)\ =\ Var\ x{"}\isanewline
+trev\_App:\ {"}trev\ (App\ f\ ts)\ =\ App\ f\ (trevs\ ts){"}\isanewline
+\isanewline
+\ \ \ \ \ \ \ \ \ \ {"}trevs\ []\ =\ []{"}\isanewline
+\ \ \ \ \ \ \ \ \ \ {"}trevs\ (t\#ts)\ =\ trevs\ ts\ @\ [trev\ t]{"}%
+\begin{isamarkuptext}%
+\noindent
+Following the above methodology, we re-express \isa{trev\_App}:%
+\end{isamarkuptext}%
+\isacommand{lemma}\ [simp]:\ {"}trev\ (App\ f\ ts)\ =\ App\ f\ (rev(map\ trev\ ts)){"}\isanewline
+\isacommand{by}(induct\_tac\ ts,\ auto)\isanewline
+\isacommand{lemmas}\ [simp\ del]\ =\ trev\_App%
+\begin{isamarkuptext}%
+\noindent
+Now it becomes quite easy to prove \isa{trev\ (trev\ \mbox{t})\ =\ \mbox{t}}, except that we
+still have to come up with the second half of the conjunction:%
+\end{isamarkuptext}%
+\isacommand{lemma}\ {"}trev(trev\ t)\ =\ (t::('a,'b)term)\ \&\isanewline
+\ \ \ \ \ \ \ \ map\ trev\ (map\ trev\ ts)\ =\ (ts::('a,'b)term\ list){"}\isanewline
+\isacommand{by}(induct\_tac\ t\ \isakeyword{and}\ ts,\ auto\ simp\ add:rev\_map)%
+\begin{isamarkuptext}%
+\noindent
+Getting rid of this second conjunct requires deriving a new induction schema
+for \isa{term}, which is beyond what we have learned so far. Please stay
+tuned, we will solve this final problem in \S\ref{sec:der-ind-schemas}.
 
 Of course, you may also combine mutual and nested recursion. For example,
 constructor \isa{Sum} in \S\ref{sec:datatype-mut-rec} could take a list of
diff -r c94db1a96f4e -r 6b0b6b471855 doc-src/TutorialI/Ifexpr/document/Ifexpr.tex
--- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Thu Aug 17 21:07:25 2000 +0200
+++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Fri Aug 18 10:34:08 2000 +0200
@@ -13,7 +13,7 @@
 \noindent
 The two constants are represented by \isa{Const\ True} and
 \isa{Const\ False}. Variables are represented by terms of the form
-\isa{Var\ n}, where \isa{n} is a natural number (type \isa{nat}).
+\isa{Var\ \mbox{n}}, where \isa{\mbox{n}} is a natural number (type \isa{nat}).
 For example, the formula $P@0 \land \neg P@1$ is represented by the term
 \isa{And\ (Var\ 0)\ (Neg\ (Var\ 1))}.
 
@@ -83,8 +83,8 @@
 More interesting is the transformation of If-expressions into a normal form
 where the first argument of \isa{IF} cannot be another \isa{IF} but
 must be a constant or variable. Such a normal form can be computed by
-repeatedly replacing a subterm of the form \isa{IF\ (IF\ b\ x\ y)\ z\ u} by
-\isa{IF\ b\ (IF\ x\ z\ u)\ (IF\ y\ z\ u)}, which has the same value. The following
+repeatedly replacing a subterm of the form \isa{IF\ (IF\ \mbox{b}\ \mbox{x}\ \mbox{y})\ \mbox{z}\ \mbox{u}} by
+\isa{IF\ \mbox{b}\ (IF\ \mbox{x}\ \mbox{z}\ \mbox{u})\ (IF\ \mbox{y}\ \mbox{z}\ \mbox{u})}, which has the same value. The following
 primitive recursive functions perform this task:%
 \end{isamarkuptext}%
 \isacommand{consts}\ normif\ ::\ {"}ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex{"}\isanewline
diff -r c94db1a96f4e -r 6b0b6b471855 doc-src/TutorialI/IsaMakefile
--- a/doc-src/TutorialI/IsaMakefile	Thu Aug 17 21:07:25 2000 +0200
+++ b/doc-src/TutorialI/IsaMakefile	Fri Aug 18 10:34:08 2000 +0200
@@ -67,7 +67,8 @@
 HOL-Datatype: HOL $(LOG)/HOL-Datatype.gz
 
 $(LOG)/HOL-Datatype.gz: $(OUT)/HOL Datatype/ROOT.ML Datatype/ABexpr.thy \
-  Datatype/Nested.thy Datatype/unfoldnested.thy Datatype/Fundata.thy
+  Datatype/Nested.thy Datatype/Nested2.thy Datatype/unfoldnested.thy \
+  Datatype/Fundata.thy
 	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Datatype
 	@rm -f tutorial.dvi
 
@@ -86,7 +87,8 @@
 HOL-Recdef: HOL $(LOG)/HOL-Recdef.gz
 
 $(LOG)/HOL-Recdef.gz: $(OUT)/HOL Recdef/examples.thy Recdef/termination.thy \
-  Recdef/simplification.thy Recdef/Induction.thy
+  Recdef/simplification.thy Recdef/Induction.thy \
+  Recdef/Nested0.thy Recdef/Nested1.thy 
 	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Recdef
 	@rm -f tutorial.dvi
 
@@ -99,7 +101,7 @@
   Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/types.thy Misc/prime_def.thy \
   Misc/arith1.thy Misc/arith2.thy Misc/arith3.thy Misc/arith4.thy \
   Misc/def_rewr.thy Misc/let_rewr.thy Misc/cond_rewr.thy Misc/case_splits.thy \
-  Misc/trace_simp.thy Misc/Itrev.thy Misc/asm_simp.thy
+  Misc/trace_simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy Misc/asm_simp.thy
 	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Misc
 	@rm -f tutorial.dvi
 
diff -r c94db1a96f4e -r 6b0b6b471855 doc-src/TutorialI/Misc/Itrev.thy
--- a/doc-src/TutorialI/Misc/Itrev.thy	Thu Aug 17 21:07:25 2000 +0200
+++ b/doc-src/TutorialI/Misc/Itrev.thy	Fri Aug 18 10:34:08 2000 +0200
@@ -84,6 +84,13 @@
 provability of the goal. Because it is not always required, and may even
 complicate matters in some cases, this heuristic is often not
 applied blindly.
+
+In general, if you have tried the above heuristics and still find your
+induction does not go through, and no obvious lemma suggests itself, you may
+need to generalize your proposition even further. This requires insight into
+the problem at hand and is beyond simple rules of thumb. In a nutshell: you
+will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind}
+to learn about some advanced techniques for inductive proofs.
 *};
 
 (*<*)
diff -r c94db1a96f4e -r 6b0b6b471855 doc-src/TutorialI/Misc/ROOT.ML
--- a/doc-src/TutorialI/Misc/ROOT.ML	Thu Aug 17 21:07:25 2000 +0200
+++ b/doc-src/TutorialI/Misc/ROOT.ML	Fri Aug 18 10:34:08 2000 +0200
@@ -16,4 +16,5 @@
 use_thy "case_splits";
 use_thy "trace_simp";
 use_thy "Itrev";
+use_thy "AdvancedInd";
 use_thy "asm_simp";
diff -r c94db1a96f4e -r 6b0b6b471855 doc-src/TutorialI/Misc/document/Itrev.tex
--- a/doc-src/TutorialI/Misc/document/Itrev.tex	Thu Aug 17 21:07:25 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex	Fri Aug 18 10:34:08 2000 +0200
@@ -47,7 +47,7 @@
 \begin{isamarkuptxt}%
 \noindent
 If \isa{ys} is replaced by \isa{[]}, the right-hand side simplifies to
-\isa{rev\ xs}, just as required.
+\isa{rev\ \mbox{xs}}, just as required.
 
 In this particular instance it was easy to guess the right generalization,
 but in more complex situations a good deal of creativity is needed. This is
@@ -64,7 +64,7 @@
 The induction hypothesis is still too weak, but this time it takes no
 intuition to generalize: the problem is that \isa{ys} is fixed throughout
 the subgoal, but the induction hypothesis needs to be applied with
-\isa{a\ \#\ ys} instead of \isa{ys}. Hence we prove the theorem
+\isa{\mbox{a}\ \#\ \mbox{ys}} instead of \isa{ys}. Hence we prove the theorem
 for all \isa{ys} instead of a fixed one:%
 \end{isamarkuptxt}%
 \isacommand{lemma}\ {"}{\isasymforall}ys.\ itrev\ xs\ ys\ =\ rev\ xs\ @\ ys{"}%
@@ -79,7 +79,14 @@
 This prevents trivial failures like the above and does not change the
 provability of the goal. Because it is not always required, and may even
 complicate matters in some cases, this heuristic is often not
-applied blindly.%
+applied blindly.
+
+In general, if you have tried the above heuristics and still find your
+induction does not go through, and no obvious lemma suggests itself, you may
+need to generalize your proposition even further. This requires insight into
+the problem at hand and is beyond simple rules of thumb. In a nutshell: you
+will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind}
+to learn about some advanced techniques for inductive proofs.%
 \end{isamarkuptxt}%
 \end{isabelle}%
 %%% Local Variables:
diff -r c94db1a96f4e -r 6b0b6b471855 doc-src/TutorialI/Misc/document/asm_simp.tex
--- a/doc-src/TutorialI/Misc/document/asm_simp.tex	Thu Aug 17 21:07:25 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/asm_simp.tex	Fri Aug 18 10:34:08 2000 +0200
@@ -8,9 +8,9 @@
 \isacommand{by}\ simp%
 \begin{isamarkuptext}%
 \noindent
-The second assumption simplifies to \isa{xs\ =\ []}, which in turn
-simplifies the first assumption to \isa{zs\ =\ ys}, thus reducing the
-conclusion to \isa{ys\ =\ ys} and hence to \isa{True}.
+The second assumption simplifies to \isa{\mbox{xs}\ =\ []}, which in turn
+simplifies the first assumption to \isa{\mbox{zs}\ =\ \mbox{ys}}, thus reducing the
+conclusion to \isa{\mbox{ys}\ =\ \mbox{ys}} and hence to \isa{True}.
 
 In some cases this may be too much of a good thing and may lead to
 nontermination:%
@@ -19,7 +19,7 @@
 \begin{isamarkuptxt}%
 \noindent
 cannot be solved by an unmodified application of \isa{simp} because the
-simplification rule \isa{f\ x\ =\ g\ (f\ (g\ x))} extracted from the assumption
+simplification rule \isa{\mbox{f}\ \mbox{x}\ =\ \mbox{g}\ (\mbox{f}\ (\mbox{g}\ \mbox{x}))} extracted from the assumption
 does not terminate. Isabelle notices certain simple forms of
 nontermination but not this one. The problem can be circumvented by
 explicitly telling the simplifier to ignore the assumptions:%
diff -r c94db1a96f4e -r 6b0b6b471855 doc-src/TutorialI/Misc/document/cond_rewr.tex
--- a/doc-src/TutorialI/Misc/document/cond_rewr.tex	Thu Aug 17 21:07:25 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/cond_rewr.tex	Fri Aug 18 10:34:08 2000 +0200
@@ -10,7 +10,7 @@
 \noindent
 Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a
 sequence of methods. Assuming that the simplification rule
-\isa{(rev\ xs\ =\ [])\ =\ (xs\ =\ [])}
+\isa{(rev\ \mbox{xs}\ =\ [])\ =\ (\mbox{xs}\ =\ [])}
 is present as well,%
 \end{isamarkuptext}%
 \isacommand{lemma}\ {"}xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd(rev\ xs)\ \#\ tl(rev\ xs)\ =\ rev\ xs{"}%
diff -r c94db1a96f4e -r 6b0b6b471855 doc-src/TutorialI/Misc/document/natsum.tex
--- a/doc-src/TutorialI/Misc/document/natsum.tex	Thu Aug 17 21:07:25 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex	Fri Aug 18 10:34:08 2000 +0200
@@ -6,7 +6,7 @@
 \begin{quote}
 
 \begin{isabelle}%
-case\ n\ of\ 0\ {\isasymRightarrow}\ 0\ |\ Suc\ m\ {\isasymRightarrow}\ m
+case\ \mbox{n}\ of\ 0\ {\isasymRightarrow}\ 0\ |\ Suc\ \mbox{m}\ {\isasymRightarrow}\ \mbox{m}
 \end{isabelle}%
 
 \end{quote}
diff -r c94db1a96f4e -r 6b0b6b471855 doc-src/TutorialI/Misc/document/pairs.tex
--- a/doc-src/TutorialI/Misc/document/pairs.tex	Thu Aug 17 21:07:25 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/pairs.tex	Fri Aug 18 10:34:08 2000 +0200
@@ -15,8 +15,8 @@
 In addition to explicit $\lambda$-abstractions, tuple patterns can be used in
 most variable binding constructs. Typical examples are
 \begin{quote}
-\isa{let\ (x,\ y)\ =\ f\ z\ in\ (y,\ x)}\\
-\isa{case\ xs\ of\ []\ {\isasymRightarrow}\ 0\ |\ (x,\ y)\ \#\ zs\ {\isasymRightarrow}\ x\ +\ y}
+\isa{let\ (\mbox{x},\ \mbox{y})\ =\ \mbox{f}\ \mbox{z}\ in\ (\mbox{y},\ \mbox{x})}\\
+\isa{case\ \mbox{xs}\ of\ []\ {\isasymRightarrow}\ 0\ |\ (\mbox{x},\ \mbox{y})\ \#\ \mbox{zs}\ {\isasymRightarrow}\ \mbox{x}\ +\ \mbox{y}}
 \end{quote}
 Further important examples are quantifiers and sets (see~\S\ref{quant-pats}).%
 \end{isamarkuptext}%
diff -r c94db1a96f4e -r 6b0b6b471855 doc-src/TutorialI/Recdef/ROOT.ML
--- a/doc-src/TutorialI/Recdef/ROOT.ML	Thu Aug 17 21:07:25 2000 +0200
+++ b/doc-src/TutorialI/Recdef/ROOT.ML	Fri Aug 18 10:34:08 2000 +0200
@@ -1,2 +1,3 @@
 use_thy "termination";
 use_thy "Induction";
+(*use_thy "Nested1";*)
diff -r c94db1a96f4e -r 6b0b6b471855 doc-src/TutorialI/Recdef/document/examples.tex
--- a/doc-src/TutorialI/Recdef/document/examples.tex	Thu Aug 17 21:07:25 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/examples.tex	Fri Aug 18 10:34:08 2000 +0200
@@ -11,13 +11,13 @@
 \begin{isamarkuptext}%
 \noindent
 The definition of \isa{fib} is accompanied by a \bfindex{measure function}
-\isa{{\isasymlambda}n.\ n} which maps the argument of \isa{fib} to a
+\isa{{\isasymlambda}\mbox{n}.\ \mbox{n}} which maps the argument of \isa{fib} to a
 natural number. The requirement is that in each equation the measure of the
 argument on the left-hand side is strictly greater than the measure of the
 argument of each recursive call. In the case of \isa{fib} this is
 obviously true because the measure function is the identity and
-\isa{Suc\ (Suc\ x)} is strictly greater than both \isa{x} and
-\isa{Suc\ x}.
+\isa{Suc\ (Suc\ \mbox{x})} is strictly greater than both \isa{x} and
+\isa{Suc\ \mbox{x}}.
 
 Slightly more interesting is the insertion of a fixed element
 between any two elements of a list:%
diff -r c94db1a96f4e -r 6b0b6b471855 doc-src/TutorialI/Recdef/document/simplification.tex
--- a/doc-src/TutorialI/Recdef/document/simplification.tex	Thu Aug 17 21:07:25 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex	Fri Aug 18 10:34:08 2000 +0200
@@ -18,7 +18,7 @@
 \begin{quote}
 
 \begin{isabelle}%
-n\ {\isasymnoteq}\ 0\ {\isasymLongrightarrow}\ m\ mod\ n\ <\ n
+\mbox{n}\ {\isasymnoteq}\ 0\ {\isasymLongrightarrow}\ \mbox{m}\ mod\ \mbox{n}\ <\ \mbox{n}
 \end{isabelle}%
 
 \end{quote}
@@ -33,7 +33,7 @@
 \begin{quote}
 
 \begin{isabelle}%
-gcd\ (m,\ n)\ =\ k
+gcd\ (\mbox{m},\ \mbox{n})\ =\ \mbox{k}
 \end{isabelle}%
 
 \end{quote}
@@ -41,7 +41,7 @@
 \begin{quote}
 
 \begin{isabelle}%
-(if\ n\ =\ 0\ then\ m\ else\ gcd\ (n,\ m\ mod\ n))\ =\ k
+(if\ \mbox{n}\ =\ 0\ then\ \mbox{m}\ else\ gcd\ (\mbox{n},\ \mbox{m}\ mod\ \mbox{n}))\ =\ \mbox{k}
 \end{isabelle}%
 
 \end{quote}
@@ -49,11 +49,11 @@
 \begin{quote}
 
 \begin{isabelle}%
-(n\ =\ 0\ {\isasymlongrightarrow}\ m\ =\ k)\ {\isasymand}\ (n\ {\isasymnoteq}\ 0\ {\isasymlongrightarrow}\ gcd\ (n,\ m\ mod\ n)\ =\ k)
+(\mbox{n}\ =\ 0\ {\isasymlongrightarrow}\ \mbox{m}\ =\ \mbox{k})\ {\isasymand}\ (\mbox{n}\ {\isasymnoteq}\ 0\ {\isasymlongrightarrow}\ gcd\ (\mbox{n},\ \mbox{m}\ mod\ \mbox{n})\ =\ \mbox{k})
 \end{isabelle}%
 
 \end{quote}
-Since the recursive call \isa{gcd\ (n,\ m\ mod\ n)} is no longer protected by
+Since the recursive call \isa{gcd\ (\mbox{n},\ \mbox{m}\ mod\ \mbox{n})} is no longer protected by
 an \isa{if}, it is unfolded again, which leads to an infinite chain of
 simplification steps. Fortunately, this problem can be avoided in many
 different ways.
diff -r c94db1a96f4e -r 6b0b6b471855 doc-src/TutorialI/ToyList/document/ToyList.tex
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Thu Aug 17 21:07:25 2000 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Fri Aug 18 10:34:08 2000 +0200
@@ -22,11 +22,11 @@
 datatype declaration is annotated with an alternative syntax: instead of
 \isa{Nil} and \isa{Cons x xs} we can write
 \isa{[]}\index{$HOL2list@\texttt{[]}|bold} and
-\isa{x\ \#\ xs}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
+\isa{\mbox{x}\ \#\ \mbox{xs}}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
 alternative syntax is the standard syntax. Thus the list \isa{Cons True
 (Cons False Nil)} becomes \isa{True\ \#\ False\ \#\ []}. The annotation
 \isacommand{infixr}\indexbold{*infixr} means that \isa{\#} associates to
-the right, i.e.\ the term \isa{x\ \#\ y\ \#\ z} is read as \isa{x
+the right, i.e.\ the term \isa{\mbox{x}\ \#\ \mbox{y}\ \#\ \mbox{z}} is read as \isa{x
 \# (y \# z)} and not as \isa{(x \# y) \# z}.
 
 \begin{warn}
@@ -47,7 +47,7 @@
 restriction, the order of items in a theory file is unconstrained.) Function
 \isa{app} is annotated with concrete syntax too. Instead of the prefix
 syntax \isa{app xs ys} the infix
-\isa{xs\ @\ ys}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
+\isa{\mbox{xs}\ @\ \mbox{ys}}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
 form. Both functions are defined recursively:%
 \end{isamarkuptext}%
 \isacommand{primrec}\isanewline
@@ -183,7 +183,7 @@
 The {\it assumptions} are the local assumptions for this subgoal and {\it
   conclusion} is the actual proposition to be proved. Typical proof steps
 that add new assumptions are induction or case distinction. In our example
-the only assumption is the induction hypothesis \isa{rev\ (rev\ list)\ =\ list}, where \isa{list} is a variable name chosen by Isabelle. If there
+the only assumption is the induction hypothesis \isa{rev\ (rev\ \mbox{list})\ =\ \mbox{list}}, where \isa{list} is a variable name chosen by Isabelle. If there
 are multiple assumptions, they are enclosed in the bracket pair
 \indexboldpos{\isasymlbrakk}{$Isabrl} and
 \indexboldpos{\isasymrbrakk}{$Isabrr} and separated by semicolons.
diff -r c94db1a96f4e -r 6b0b6b471855 doc-src/TutorialI/fp.tex
--- 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 @@
 
 \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}
@@ -301,6 +312,7 @@
 
 
 \subsection{Natural numbers}
+\label{sec:nat}
 \index{arithmetic|(}
 
 \input{Misc/document/fakenat.tex}
@@ -694,8 +706,9 @@
 \input{Datatype/document/ABexpr.tex}
 
 \subsection{Nested recursion}
+\label{sec:nested-datatype}
 
-\input{Datatype/document/Nested.tex}
+{\makeatother\input{Datatype/document/Nested.tex}}
 
 
 \subsection{The limits of nested recursion}
@@ -828,13 +841,25 @@
 
 \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}
diff -r c94db1a96f4e -r 6b0b6b471855 doc-src/TutorialI/tutorial.tex
--- a/doc-src/TutorialI/tutorial.tex	Thu Aug 17 21:07:25 2000 +0200
+++ b/doc-src/TutorialI/tutorial.tex	Fri Aug 18 10:34:08 2000 +0200
@@ -1,3 +1,4 @@
+% pr(latex xsymbols symbols)
 \documentclass[11pt,a4paper]{report}
 \usepackage{isabelle,isabellesym}
 \usepackage{latexsym,verbatim,graphicx,../iman,extra,comment}