author nipkow Fri Aug 18 10:34:08 2000 +0200 (2000-08-18) changeset 9644 6b0b6b471855 parent 9643 c94db1a96f4e child 9645 20ae97cd2a16
*** empty log message ***
     1.1 --- a/doc-src/TutorialI/Datatype/Fundata.thy	Thu Aug 17 21:07:25 2000 +0200
1.2 +++ b/doc-src/TutorialI/Datatype/Fundata.thy	Fri Aug 18 10:34:08 2000 +0200
1.3 @@ -36,7 +36,7 @@
1.4  The following lemma has a canonical proof  *}
1.5
1.6  lemma "map_bt (g o f) T = map_bt g (map_bt f T)";
1.7 -apply(induct_tac "T", auto).
1.8 +by(induct_tac "T", auto)
1.9
1.10  text{*\noindent
1.11  but it is worth taking a look at the proof state after the induction step

     2.1 --- a/doc-src/TutorialI/Datatype/Nested.thy	Thu Aug 17 21:07:25 2000 +0200
2.2 +++ b/doc-src/TutorialI/Datatype/Nested.thy	Fri Aug 18 10:34:08 2000 +0200
2.3 @@ -46,12 +46,15 @@
2.4
2.5  primrec
2.6    "subst s (Var x) = s x"
2.7 +  subst_App:
2.8    "subst s (App f ts) = App f (substs s ts)"
2.9
2.10    "substs s [] = []"
2.11    "substs s (t # ts) = subst s t # substs s ts";
2.12
2.13  text{*\noindent
2.14 +You should ignore the label \isa{subst\_App} for the moment.
2.15 +
2.16  Similarly, when proving a statement about terms inductively, we need
2.17  to prove a related statement about term lists simultaneously. For example,
2.18  the fact that the identity substitution does not change a term needs to be
2.19 @@ -80,6 +83,69 @@
2.20  strengthen it, and prove it. (Note: \ttindexbold{o} is function composition;
2.21  its definition is found in theorem \isa{o_def}).
2.22  \end{exercise}
2.23 +\begin{exercise}\label{ex:trev-trev}
2.24 +  Define a function \isa{trev} of type @{typ"('a,'b)term => ('a,'b)term"} that
2.25 +  recursively reverses the order of arguments of all function symbols in a
2.26 +  term. Prove that \isa{trev(trev t) = t}.
2.27 +\end{exercise}
2.28 +
2.29 +The experienced functional programmer may feel that our above definition of
2.30 +\isa{subst} is unnecessarily complicated in that \isa{substs} is completely
2.31 +unnecessary. The @{term"App"}-case can be defined directly as
2.32 +\begin{quote}
2.33 +@{term[display]"subst s (App f ts) = App f (map (subst s) ts)"}
2.34 +\end{quote}
2.35 +where @{term"map"} is the standard list function such that
2.36 +\isa{map f [x1,...,xn] = [f x1,...,f xn]}. This is true, but Isabelle insists
2.37 +on the above fixed format. Fortunately, we can easily \emph{prove} that the
2.38 +suggested equation holds:
2.39 +*}
2.40 +
2.41 +lemma [simp]: "subst s (App f ts) = App f (map (subst s) ts)"
2.42 +by(induct_tac ts, auto)
2.43 +
2.44 +text{*
2.45 +What is more, we can now disable the old defining equation as a
2.46 +simplification rule:
2.47 +*}
2.48 +
2.49 +lemmas [simp del] = subst_App
2.50 +
2.51 +text{*
2.52 +The advantage is that now we have replaced @{term"substs"} by @{term"map"},
2.53 +we can profit from the large number of pre-proved lemmas about @{term"map"}.
2.54 +We illustrate this with an example, reversing terms:
2.55 +*}
2.56 +
2.57 +consts trev  :: "('a,'b)term => ('a,'b)term"
2.58 +       trevs :: "('a,'b)term list => ('a,'b)term list"
2.59 +primrec   "trev (Var x) = Var x"
2.60 +trev_App: "trev (App f ts) = App f (trevs ts)"
2.61 +
2.62 +          "trevs [] = []"
2.63 +          "trevs (t#ts) = trevs ts @ [trev t]"
2.64 +
2.65 +text{*\noindent
2.66 +Following the above methodology, we re-express \isa{trev\_App}:
2.67 +*}
2.68 +
2.69 +lemma [simp]: "trev (App f ts) = App f (rev(map trev ts))"
2.70 +by(induct_tac ts, auto)
2.71 +lemmas [simp del] = trev_App
2.72 +
2.73 +text{*\noindent
2.74 +Now it becomes quite easy to prove @{term"trev(trev t) = t"}, except that we
2.75 +still have to come up with the second half of the conjunction:
2.76 +*}
2.77 +
2.78 +lemma "trev(trev t) = (t::('a,'b)term) &
2.79 +        map trev (map trev ts) = (ts::('a,'b)term list)";
2.80 +by(induct_tac t and ts, auto simp add:rev_map);
2.81 +
2.82 +text{*\noindent
2.83 +Getting rid of this second conjunct requires deriving a new induction schema
2.84 +for \isa{term}, which is beyond what we have learned so far. Please stay
2.85 +tuned, we will solve this final problem in \S\ref{sec:der-ind-schemas}.
2.86
2.87  Of course, you may also combine mutual and nested recursion. For example,
2.88  constructor \isa{Sum} in \S\ref{sec:datatype-mut-rec} could take a list of

     3.1 --- a/doc-src/TutorialI/Datatype/ROOT.ML	Thu Aug 17 21:07:25 2000 +0200
3.2 +++ b/doc-src/TutorialI/Datatype/ROOT.ML	Fri Aug 18 10:34:08 2000 +0200
3.3 @@ -1,4 +1,4 @@
3.4  use_thy "ABexpr";
3.5  use_thy "unfoldnested";
3.6 -use_thy "Nested";
3.7 +use_thy "Nested2";
3.8  use_thy "Fundata";

     4.1 --- a/doc-src/TutorialI/Datatype/document/ABexpr.tex	Thu Aug 17 21:07:25 2000 +0200
4.2 +++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex	Fri Aug 18 10:34:08 2000 +0200
4.3 @@ -102,7 +102,7 @@
4.4  \end{ttbox}
4.5
4.6  \begin{exercise}
4.7 -  Define a function \isa{norma} of type \isa{'a\ aexp\ {\isasymRightarrow}\ 'a\ aexp} that
4.8 +  Define a function \isa{norma} of type \isa{\mbox{'a}\ aexp\ {\isasymRightarrow}\ \mbox{'a}\ aexp} that
4.9    replaces \isa{IF}s with complex boolean conditions by nested
4.10    \isa{IF}s where each condition is a \isa{Less} --- \isa{And} and
4.11    \isa{Neg} should be eliminated completely. Prove that \isa{norma}

     5.1 --- a/doc-src/TutorialI/Datatype/document/Fundata.tex	Thu Aug 17 21:07:25 2000 +0200
5.2 +++ b/doc-src/TutorialI/Datatype/document/Fundata.tex	Fri Aug 18 10:34:08 2000 +0200
5.3 @@ -11,7 +11,7 @@
5.4  \begin{quote}
5.5
5.6  \begin{isabelle}%
5.7 -Branch\ 0\ ({\isasymlambda}i.\ Branch\ i\ ({\isasymlambda}n.\ Tip))
5.8 +Branch\ 0\ ({\isasymlambda}\mbox{i}.\ Branch\ \mbox{i}\ ({\isasymlambda}\mbox{n}.\ Tip))
5.9  \end{isabelle}%
5.10
5.11  \end{quote}
5.12 @@ -29,15 +29,15 @@
5.13  \noindent This is a valid \isacommand{primrec} definition because the
5.14  recursive calls of \isa{map_bt} involve only subtrees obtained from
5.15  \isa{F}, i.e.\ the left-hand side. Thus termination is assured.  The
5.16 -seasoned functional programmer might have written \isa{map\_bt\ f\ {\isasymcirc}\ F}
5.17 -instead of \isa{{\isasymlambda}i.\ map\_bt\ f\ (F\ i)}, but the former is not accepted by
5.18 +seasoned functional programmer might have written \isa{map\_bt\ \mbox{f}\ {\isasymcirc}\ \mbox{F}}
5.19 +instead of \isa{{\isasymlambda}\mbox{i}.\ map\_bt\ \mbox{f}\ (\mbox{F}\ \mbox{i})}, but the former is not accepted by
5.20  Isabelle because the termination proof is not as obvious since
5.21  \isa{map_bt} is only partially applied.
5.22
5.23  The following lemma has a canonical proof%
5.24  \end{isamarkuptext}%
5.25  \isacommand{lemma}\ {"}map\_bt\ (g\ o\ f)\ T\ =\ map\_bt\ g\ (map\_bt\ f\ T){"}\isanewline
5.26 -\isacommand{apply}(induct\_tac\ {"}T{"},\ auto)\isacommand{.}%
5.27 +\isacommand{by}(induct\_tac\ {"}T{"},\ auto)%
5.28  \begin{isamarkuptext}%
5.29  \noindent
5.30  but it is worth taking a look at the proof state after the induction step

     6.1 --- a/doc-src/TutorialI/Datatype/document/Nested.tex	Thu Aug 17 21:07:25 2000 +0200
6.2 +++ b/doc-src/TutorialI/Datatype/document/Nested.tex	Fri Aug 18 10:34:08 2000 +0200
6.3 @@ -13,7 +13,7 @@
6.4  the command \isacommand{term}.
6.5  Parameter \isa{'a} is the type of variables and \isa{'b} the type of
6.6  function symbols.
6.7 -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
6.8 +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
6.9  suitable values, e.g.\ numbers or strings.
6.10
6.11  What complicates the definition of \isa{term} is the nested occurrence of
6.12 @@ -41,12 +41,15 @@
6.13  \isanewline
6.14  \isacommand{primrec}\isanewline
6.15  \ \ {"}subst\ s\ (Var\ x)\ =\ s\ x{"}\isanewline
6.16 +\ \ subst\_App:\isanewline
6.17  \ \ {"}subst\ s\ (App\ f\ ts)\ =\ App\ f\ (substs\ s\ ts){"}\isanewline
6.18  \isanewline
6.19  \ \ {"}substs\ s\ []\ =\ []{"}\isanewline
6.20  \ \ {"}substs\ s\ (t\ \#\ ts)\ =\ subst\ s\ t\ \#\ substs\ s\ ts{"}%
6.21  \begin{isamarkuptext}%
6.22  \noindent
6.23 +You should ignore the label \isa{subst\_App} for the moment.
6.24 +
6.25  Similarly, when proving a statement about terms inductively, we need
6.26  to prove a related statement about term lists simultaneously. For example,
6.27  the fact that the identity substitution does not change a term needs to be
6.28 @@ -58,7 +61,7 @@
6.29  \begin{isamarkuptext}%
6.30  \noindent
6.31  Note that \isa{Var} is the identity substitution because by definition it
6.32 -leaves variables unchanged: \isa{subst\ Var\ (Var\ x)\ =\ Var\ x}. Note also
6.33 +leaves variables unchanged: \isa{subst\ Var\ (Var\ \mbox{x})\ =\ Var\ \mbox{x}}. Note also
6.34  that the type annotations are necessary because otherwise there is nothing in
6.35  the goal to enforce that both halves of the goal talk about the same type
6.36  parameters \isa{('a,'b)}. As a result, induction would fail
6.37 @@ -74,6 +77,66 @@
6.38  strengthen it, and prove it. (Note: \ttindexbold{o} is function composition;
6.39  its definition is found in theorem \isa{o_def}).
6.40  \end{exercise}
6.41 +\begin{exercise}\label{ex:trev-trev}
6.42 +  Define a function \isa{trev} of type \isa{(\mbox{'a},\ \mbox{'b})\ term\ {\isasymRightarrow}\ (\mbox{'a},\ \mbox{'b})\ term} that
6.43 +  recursively reverses the order of arguments of all function symbols in a
6.44 +  term. Prove that \isa{trev(trev t) = t}.
6.45 +\end{exercise}
6.46 +
6.47 +The experienced functional programmer may feel that our above definition of
6.48 +\isa{subst} is unnecessarily complicated in that \isa{substs} is completely
6.49 +unnecessary. The \isa{App}-case can be defined directly as
6.50 +\begin{quote}
6.51 +
6.52 +\begin{isabelle}%
6.53 +subst\ \mbox{s}\ (App\ \mbox{f}\ \mbox{ts})\ =\ App\ \mbox{f}\ (map\ (subst\ \mbox{s})\ \mbox{ts})
6.54 +\end{isabelle}%
6.55 +
6.56 +\end{quote}
6.57 +where \isa{map} is the standard list function such that
6.58 +\isa{map f [x1,...,xn] = [f x1,...,f xn]}. This is true, but Isabelle insists
6.59 +on the above fixed format. Fortunately, we can easily \emph{prove} that the
6.60 +suggested equation holds:%
6.61 +\end{isamarkuptext}%
6.62 +\isacommand{lemma}\ [simp]:\ {"}subst\ s\ (App\ f\ ts)\ =\ App\ f\ (map\ (subst\ s)\ ts){"}\isanewline
6.63 +\isacommand{by}(induct\_tac\ ts,\ auto)%
6.64 +\begin{isamarkuptext}%
6.65 +What is more, we can now disable the old defining equation as a
6.66 +simplification rule:%
6.67 +\end{isamarkuptext}%
6.68 +\isacommand{lemmas}\ [simp\ del]\ =\ subst\_App%
6.69 +\begin{isamarkuptext}%
6.70 +The advantage is that now we have replaced \isa{substs} by \isa{map},
6.71 +we can profit from the large number of pre-proved lemmas about \isa{map}.
6.72 +We illustrate this with an example, reversing terms:%
6.73 +\end{isamarkuptext}%
6.74 +\isacommand{consts}\ trev\ \ ::\ {"}('a,'b)term\ =>\ ('a,'b)term{"}\isanewline
6.75 +\ \ \ \ \ \ \ trevs\ ::\ {"}('a,'b)term\ list\ =>\ ('a,'b)term\ list{"}\isanewline
6.76 +\isacommand{primrec}\ \ \ {"}trev\ (Var\ x)\ =\ Var\ x{"}\isanewline
6.77 +trev\_App:\ {"}trev\ (App\ f\ ts)\ =\ App\ f\ (trevs\ ts){"}\isanewline
6.78 +\isanewline
6.79 +\ \ \ \ \ \ \ \ \ \ {"}trevs\ []\ =\ []{"}\isanewline
6.80 +\ \ \ \ \ \ \ \ \ \ {"}trevs\ (t\#ts)\ =\ trevs\ ts\ @\ [trev\ t]{"}%
6.81 +\begin{isamarkuptext}%
6.82 +\noindent
6.83 +Following the above methodology, we re-express \isa{trev\_App}:%
6.84 +\end{isamarkuptext}%
6.85 +\isacommand{lemma}\ [simp]:\ {"}trev\ (App\ f\ ts)\ =\ App\ f\ (rev(map\ trev\ ts)){"}\isanewline
6.86 +\isacommand{by}(induct\_tac\ ts,\ auto)\isanewline
6.87 +\isacommand{lemmas}\ [simp\ del]\ =\ trev\_App%
6.88 +\begin{isamarkuptext}%
6.89 +\noindent
6.90 +Now it becomes quite easy to prove \isa{trev\ (trev\ \mbox{t})\ =\ \mbox{t}}, except that we
6.91 +still have to come up with the second half of the conjunction:%
6.92 +\end{isamarkuptext}%
6.93 +\isacommand{lemma}\ {"}trev(trev\ t)\ =\ (t::('a,'b)term)\ \&\isanewline
6.94 +\ \ \ \ \ \ \ \ map\ trev\ (map\ trev\ ts)\ =\ (ts::('a,'b)term\ list){"}\isanewline
6.95 +\isacommand{by}(induct\_tac\ t\ \isakeyword{and}\ ts,\ auto\ simp\ add:rev\_map)%
6.96 +\begin{isamarkuptext}%
6.97 +\noindent
6.98 +Getting rid of this second conjunct requires deriving a new induction schema
6.99 +for \isa{term}, which is beyond what we have learned so far. Please stay
6.100 +tuned, we will solve this final problem in \S\ref{sec:der-ind-schemas}.
6.101
6.102  Of course, you may also combine mutual and nested recursion. For example,
6.103  constructor \isa{Sum} in \S\ref{sec:datatype-mut-rec} could take a list of

     7.1 --- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Thu Aug 17 21:07:25 2000 +0200
7.2 +++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Fri Aug 18 10:34:08 2000 +0200
7.3 @@ -13,7 +13,7 @@
7.4  \noindent
7.5  The two constants are represented by \isa{Const\ True} and
7.6  \isa{Const\ False}. Variables are represented by terms of the form
7.7 -\isa{Var\ n}, where \isa{n} is a natural number (type \isa{nat}).
7.8 +\isa{Var\ \mbox{n}}, where \isa{\mbox{n}} is a natural number (type \isa{nat}).
7.9  For example, the formula $P@0 \land \neg P@1$ is represented by the term
7.10  \isa{And\ (Var\ 0)\ (Neg\ (Var\ 1))}.
7.11
7.12 @@ -83,8 +83,8 @@
7.13  More interesting is the transformation of If-expressions into a normal form
7.14  where the first argument of \isa{IF} cannot be another \isa{IF} but
7.15  must be a constant or variable. Such a normal form can be computed by
7.16 -repeatedly replacing a subterm of the form \isa{IF\ (IF\ b\ x\ y)\ z\ u} by
7.17 -\isa{IF\ b\ (IF\ x\ z\ u)\ (IF\ y\ z\ u)}, which has the same value. The following
7.18 +repeatedly replacing a subterm of the form \isa{IF\ (IF\ \mbox{b}\ \mbox{x}\ \mbox{y})\ \mbox{z}\ \mbox{u}} by
7.19 +\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
7.20  primitive recursive functions perform this task:%
7.21  \end{isamarkuptext}%
7.22  \isacommand{consts}\ normif\ ::\ {"}ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex{"}\isanewline

     8.1 --- a/doc-src/TutorialI/IsaMakefile	Thu Aug 17 21:07:25 2000 +0200
8.2 +++ b/doc-src/TutorialI/IsaMakefile	Fri Aug 18 10:34:08 2000 +0200
8.3 @@ -67,7 +67,8 @@
8.4  HOL-Datatype: HOL $(LOG)/HOL-Datatype.gz 8.5 8.6$(LOG)/HOL-Datatype.gz: $(OUT)/HOL Datatype/ROOT.ML Datatype/ABexpr.thy \ 8.7 - Datatype/Nested.thy Datatype/unfoldnested.thy Datatype/Fundata.thy 8.8 + Datatype/Nested.thy Datatype/Nested2.thy Datatype/unfoldnested.thy \ 8.9 + Datatype/Fundata.thy 8.10 @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Datatype 8.11 @rm -f tutorial.dvi 8.12 8.13 @@ -86,7 +87,8 @@ 8.14 HOL-Recdef: HOL$(LOG)/HOL-Recdef.gz
8.15
8.16  $(LOG)/HOL-Recdef.gz:$(OUT)/HOL Recdef/examples.thy Recdef/termination.thy \
8.17 -  Recdef/simplification.thy Recdef/Induction.thy
8.18 +  Recdef/simplification.thy Recdef/Induction.thy \
8.19 +  Recdef/Nested0.thy Recdef/Nested1.thy
8.20  	@$(ISATOOL) usedir -i true -d dvi -D document$(OUT)/HOL Recdef
8.21  	@rm -f tutorial.dvi
8.22
8.23 @@ -99,7 +101,7 @@
8.24    Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/types.thy Misc/prime_def.thy \
8.25    Misc/arith1.thy Misc/arith2.thy Misc/arith3.thy Misc/arith4.thy \
8.26    Misc/def_rewr.thy Misc/let_rewr.thy Misc/cond_rewr.thy Misc/case_splits.thy \
8.27 -  Misc/trace_simp.thy Misc/Itrev.thy Misc/asm_simp.thy
8.28 +  Misc/trace_simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy Misc/asm_simp.thy
8.29  	@$(ISATOOL) usedir -i true -d dvi -D document$(OUT)/HOL Misc
8.30  	@rm -f tutorial.dvi
8.31

     9.1 --- a/doc-src/TutorialI/Misc/Itrev.thy	Thu Aug 17 21:07:25 2000 +0200
9.2 +++ b/doc-src/TutorialI/Misc/Itrev.thy	Fri Aug 18 10:34:08 2000 +0200
9.3 @@ -84,6 +84,13 @@
9.4  provability of the goal. Because it is not always required, and may even
9.5  complicate matters in some cases, this heuristic is often not
9.6  applied blindly.
9.7 +
9.8 +In general, if you have tried the above heuristics and still find your
9.9 +induction does not go through, and no obvious lemma suggests itself, you may
9.10 +need to generalize your proposition even further. This requires insight into
9.11 +the problem at hand and is beyond simple rules of thumb. In a nutshell: you
9.12 +will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind}
9.13 +to learn about some advanced techniques for inductive proofs.
9.14  *};
9.15
9.16  (*<*)

    10.1 --- a/doc-src/TutorialI/Misc/ROOT.ML	Thu Aug 17 21:07:25 2000 +0200
10.2 +++ b/doc-src/TutorialI/Misc/ROOT.ML	Fri Aug 18 10:34:08 2000 +0200
10.3 @@ -16,4 +16,5 @@
10.4  use_thy "case_splits";
10.5  use_thy "trace_simp";
10.6  use_thy "Itrev";
10.8  use_thy "asm_simp";

    11.1 --- a/doc-src/TutorialI/Misc/document/Itrev.tex	Thu Aug 17 21:07:25 2000 +0200
11.2 +++ b/doc-src/TutorialI/Misc/document/Itrev.tex	Fri Aug 18 10:34:08 2000 +0200
11.3 @@ -47,7 +47,7 @@
11.4  \begin{isamarkuptxt}%
11.5  \noindent
11.6  If \isa{ys} is replaced by \isa{[]}, the right-hand side simplifies to
11.7 -\isa{rev\ xs}, just as required.
11.8 +\isa{rev\ \mbox{xs}}, just as required.
11.9
11.10  In this particular instance it was easy to guess the right generalization,
11.11  but in more complex situations a good deal of creativity is needed. This is
11.12 @@ -64,7 +64,7 @@
11.13  The induction hypothesis is still too weak, but this time it takes no
11.14  intuition to generalize: the problem is that \isa{ys} is fixed throughout
11.15  the subgoal, but the induction hypothesis needs to be applied with
11.16 -\isa{a\ \#\ ys} instead of \isa{ys}. Hence we prove the theorem
11.17 +\isa{\mbox{a}\ \#\ \mbox{ys}} instead of \isa{ys}. Hence we prove the theorem
11.18  for all \isa{ys} instead of a fixed one:%
11.19  \end{isamarkuptxt}%
11.20  \isacommand{lemma}\ {"}{\isasymforall}ys.\ itrev\ xs\ ys\ =\ rev\ xs\ @\ ys{"}%
11.21 @@ -79,7 +79,14 @@
11.22  This prevents trivial failures like the above and does not change the
11.23  provability of the goal. Because it is not always required, and may even
11.24  complicate matters in some cases, this heuristic is often not
11.25 -applied blindly.%
11.26 +applied blindly.
11.27 +
11.28 +In general, if you have tried the above heuristics and still find your
11.29 +induction does not go through, and no obvious lemma suggests itself, you may
11.30 +need to generalize your proposition even further. This requires insight into
11.31 +the problem at hand and is beyond simple rules of thumb. In a nutshell: you
11.32 +will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind}
11.33 +to learn about some advanced techniques for inductive proofs.%
11.34  \end{isamarkuptxt}%
11.35  \end{isabelle}%
11.36  %%% Local Variables:

    12.1 --- a/doc-src/TutorialI/Misc/document/asm_simp.tex	Thu Aug 17 21:07:25 2000 +0200
12.2 +++ b/doc-src/TutorialI/Misc/document/asm_simp.tex	Fri Aug 18 10:34:08 2000 +0200
12.3 @@ -8,9 +8,9 @@
12.4  \isacommand{by}\ simp%
12.5  \begin{isamarkuptext}%
12.6  \noindent
12.7 -The second assumption simplifies to \isa{xs\ =\ []}, which in turn
12.8 -simplifies the first assumption to \isa{zs\ =\ ys}, thus reducing the
12.9 -conclusion to \isa{ys\ =\ ys} and hence to \isa{True}.
12.10 +The second assumption simplifies to \isa{\mbox{xs}\ =\ []}, which in turn
12.11 +simplifies the first assumption to \isa{\mbox{zs}\ =\ \mbox{ys}}, thus reducing the
12.12 +conclusion to \isa{\mbox{ys}\ =\ \mbox{ys}} and hence to \isa{True}.
12.13
12.14  In some cases this may be too much of a good thing and may lead to
12.15  nontermination:%
12.16 @@ -19,7 +19,7 @@
12.17  \begin{isamarkuptxt}%
12.18  \noindent
12.19  cannot be solved by an unmodified application of \isa{simp} because the
12.20 -simplification rule \isa{f\ x\ =\ g\ (f\ (g\ x))} extracted from the assumption
12.21 +simplification rule \isa{\mbox{f}\ \mbox{x}\ =\ \mbox{g}\ (\mbox{f}\ (\mbox{g}\ \mbox{x}))} extracted from the assumption
12.22  does not terminate. Isabelle notices certain simple forms of
12.23  nontermination but not this one. The problem can be circumvented by
12.24  explicitly telling the simplifier to ignore the assumptions:%

    13.1 --- a/doc-src/TutorialI/Misc/document/cond_rewr.tex	Thu Aug 17 21:07:25 2000 +0200
13.2 +++ b/doc-src/TutorialI/Misc/document/cond_rewr.tex	Fri Aug 18 10:34:08 2000 +0200
13.3 @@ -10,7 +10,7 @@
13.4  \noindent
13.5  Note the use of \ttindexboldpos{,}{$Isar}'' to string together a 13.6 sequence of methods. Assuming that the simplification rule 13.7 -\isa{(rev\ xs\ =\ [])\ =\ (xs\ =\ [])} 13.8 +\isa{(rev\ \mbox{xs}\ =\ [])\ =\ (\mbox{xs}\ =\ [])} 13.9 is present as well,% 13.10 \end{isamarkuptext}% 13.11 \isacommand{lemma}\ {"}xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd(rev\ xs)\ \#\ tl(rev\ xs)\ =\ rev\ xs{"}%   14.1 --- a/doc-src/TutorialI/Misc/document/natsum.tex Thu Aug 17 21:07:25 2000 +0200 14.2 +++ b/doc-src/TutorialI/Misc/document/natsum.tex Fri Aug 18 10:34:08 2000 +0200 14.3 @@ -6,7 +6,7 @@ 14.4 \begin{quote} 14.5 14.6 \begin{isabelle}% 14.7 -case\ n\ of\ 0\ {\isasymRightarrow}\ 0\ |\ Suc\ m\ {\isasymRightarrow}\ m 14.8 +case\ \mbox{n}\ of\ 0\ {\isasymRightarrow}\ 0\ |\ Suc\ \mbox{m}\ {\isasymRightarrow}\ \mbox{m} 14.9 \end{isabelle}% 14.10 14.11 \end{quote}   15.1 --- a/doc-src/TutorialI/Misc/document/pairs.tex Thu Aug 17 21:07:25 2000 +0200 15.2 +++ b/doc-src/TutorialI/Misc/document/pairs.tex Fri Aug 18 10:34:08 2000 +0200 15.3 @@ -15,8 +15,8 @@ 15.4 In addition to explicit$\lambda$-abstractions, tuple patterns can be used in 15.5 most variable binding constructs. Typical examples are 15.6 \begin{quote} 15.7 -\isa{let\ (x,\ y)\ =\ f\ z\ in\ (y,\ x)}\\ 15.8 -\isa{case\ xs\ of\ []\ {\isasymRightarrow}\ 0\ |\ (x,\ y)\ \#\ zs\ {\isasymRightarrow}\ x\ +\ y} 15.9 +\isa{let\ (\mbox{x},\ \mbox{y})\ =\ \mbox{f}\ \mbox{z}\ in\ (\mbox{y},\ \mbox{x})}\\ 15.10 +\isa{case\ \mbox{xs}\ of\ []\ {\isasymRightarrow}\ 0\ |\ (\mbox{x},\ \mbox{y})\ \#\ \mbox{zs}\ {\isasymRightarrow}\ \mbox{x}\ +\ \mbox{y}} 15.11 \end{quote} 15.12 Further important examples are quantifiers and sets (see~\S\ref{quant-pats}).% 15.13 \end{isamarkuptext}%   16.1 --- a/doc-src/TutorialI/Recdef/ROOT.ML Thu Aug 17 21:07:25 2000 +0200 16.2 +++ b/doc-src/TutorialI/Recdef/ROOT.ML Fri Aug 18 10:34:08 2000 +0200 16.3 @@ -1,2 +1,3 @@ 16.4 use_thy "termination"; 16.5 use_thy "Induction"; 16.6 +(*use_thy "Nested1";*)   17.1 --- a/doc-src/TutorialI/Recdef/document/examples.tex Thu Aug 17 21:07:25 2000 +0200 17.2 +++ b/doc-src/TutorialI/Recdef/document/examples.tex Fri Aug 18 10:34:08 2000 +0200 17.3 @@ -11,13 +11,13 @@ 17.4 \begin{isamarkuptext}% 17.5 \noindent 17.6 The definition of \isa{fib} is accompanied by a \bfindex{measure function} 17.7 -\isa{{\isasymlambda}n.\ n} which maps the argument of \isa{fib} to a 17.8 +\isa{{\isasymlambda}\mbox{n}.\ \mbox{n}} which maps the argument of \isa{fib} to a 17.9 natural number. The requirement is that in each equation the measure of the 17.10 argument on the left-hand side is strictly greater than the measure of the 17.11 argument of each recursive call. In the case of \isa{fib} this is 17.12 obviously true because the measure function is the identity and 17.13 -\isa{Suc\ (Suc\ x)} is strictly greater than both \isa{x} and 17.14 -\isa{Suc\ x}. 17.15 +\isa{Suc\ (Suc\ \mbox{x})} is strictly greater than both \isa{x} and 17.16 +\isa{Suc\ \mbox{x}}. 17.17 17.18 Slightly more interesting is the insertion of a fixed element 17.19 between any two elements of a list:%   18.1 --- a/doc-src/TutorialI/Recdef/document/simplification.tex Thu Aug 17 21:07:25 2000 +0200 18.2 +++ b/doc-src/TutorialI/Recdef/document/simplification.tex Fri Aug 18 10:34:08 2000 +0200 18.3 @@ -18,7 +18,7 @@ 18.4 \begin{quote} 18.5 18.6 \begin{isabelle}% 18.7 -n\ {\isasymnoteq}\ 0\ {\isasymLongrightarrow}\ m\ mod\ n\ <\ n 18.8 +\mbox{n}\ {\isasymnoteq}\ 0\ {\isasymLongrightarrow}\ \mbox{m}\ mod\ \mbox{n}\ <\ \mbox{n} 18.9 \end{isabelle}% 18.10 18.11 \end{quote} 18.12 @@ -33,7 +33,7 @@ 18.13 \begin{quote} 18.14 18.15 \begin{isabelle}% 18.16 -gcd\ (m,\ n)\ =\ k 18.17 +gcd\ (\mbox{m},\ \mbox{n})\ =\ \mbox{k} 18.18 \end{isabelle}% 18.19 18.20 \end{quote} 18.21 @@ -41,7 +41,7 @@ 18.22 \begin{quote} 18.23 18.24 \begin{isabelle}% 18.25 -(if\ n\ =\ 0\ then\ m\ else\ gcd\ (n,\ m\ mod\ n))\ =\ k 18.26 +(if\ \mbox{n}\ =\ 0\ then\ \mbox{m}\ else\ gcd\ (\mbox{n},\ \mbox{m}\ mod\ \mbox{n}))\ =\ \mbox{k} 18.27 \end{isabelle}% 18.28 18.29 \end{quote} 18.30 @@ -49,11 +49,11 @@ 18.31 \begin{quote} 18.32 18.33 \begin{isabelle}% 18.34 -(n\ =\ 0\ {\isasymlongrightarrow}\ m\ =\ k)\ {\isasymand}\ (n\ {\isasymnoteq}\ 0\ {\isasymlongrightarrow}\ gcd\ (n,\ m\ mod\ n)\ =\ k) 18.35 +(\mbox{n}\ =\ 0\ {\isasymlongrightarrow}\ \mbox{m}\ =\ \mbox{k})\ {\isasymand}\ (\mbox{n}\ {\isasymnoteq}\ 0\ {\isasymlongrightarrow}\ gcd\ (\mbox{n},\ \mbox{m}\ mod\ \mbox{n})\ =\ \mbox{k}) 18.36 \end{isabelle}% 18.37 18.38 \end{quote} 18.39 -Since the recursive call \isa{gcd\ (n,\ m\ mod\ n)} is no longer protected by 18.40 +Since the recursive call \isa{gcd\ (\mbox{n},\ \mbox{m}\ mod\ \mbox{n})} is no longer protected by 18.41 an \isa{if}, it is unfolded again, which leads to an infinite chain of 18.42 simplification steps. Fortunately, this problem can be avoided in many 18.43 different ways.   19.1 --- a/doc-src/TutorialI/ToyList/document/ToyList.tex Thu Aug 17 21:07:25 2000 +0200 19.2 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Fri Aug 18 10:34:08 2000 +0200 19.3 @@ -22,11 +22,11 @@ 19.4 datatype declaration is annotated with an alternative syntax: instead of 19.5 \isa{Nil} and \isa{Cons x xs} we can write 19.6 \isa{[]}\index{$HOL2list@\texttt{[]}|bold} and
19.7 -\isa{x\ \#\ xs}\index{$HOL2list@\texttt{\#}|bold}. In fact, this 19.8 +\isa{\mbox{x}\ \#\ \mbox{xs}}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
19.9  alternative syntax is the standard syntax. Thus the list \isa{Cons True
19.10  (Cons False Nil)} becomes \isa{True\ \#\ False\ \#\ []}. The annotation
19.11  \isacommand{infixr}\indexbold{*infixr} means that \isa{\#} associates to
19.12 -the right, i.e.\ the term \isa{x\ \#\ y\ \#\ z} is read as \isa{x
19.13 +the right, i.e.\ the term \isa{\mbox{x}\ \#\ \mbox{y}\ \#\ \mbox{z}} is read as \isa{x
19.14  \# (y \# z)} and not as \isa{(x \# y) \# z}.
19.15
19.16  \begin{warn}
19.17 @@ -47,7 +47,7 @@
19.18  restriction, the order of items in a theory file is unconstrained.) Function
19.19  \isa{app} is annotated with concrete syntax too. Instead of the prefix
19.20  syntax \isa{app xs ys} the infix
19.21 -\isa{xs\ @\ ys}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred 19.22 +\isa{\mbox{xs}\ @\ \mbox{ys}}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
19.23  form. Both functions are defined recursively:%
19.24  \end{isamarkuptext}%
19.25  \isacommand{primrec}\isanewline
19.26 @@ -183,7 +183,7 @@
19.27  The {\it assumptions} are the local assumptions for this subgoal and {\it
19.28    conclusion} is the actual proposition to be proved. Typical proof steps
19.29  that add new assumptions are induction or case distinction. In our example
19.30 -the only assumption is the induction hypothesis \isa{rev\ (rev\ list)\ =\ list}, where \isa{list} is a variable name chosen by Isabelle. If there
19.31 +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
19.32  are multiple assumptions, they are enclosed in the bracket pair
19.33  \indexboldpos{\isasymlbrakk}{$Isabrl} and 19.34 \indexboldpos{\isasymrbrakk}{$Isabrr} and separated by semicolons.

    20.1 --- a/doc-src/TutorialI/fp.tex	Thu Aug 17 21:07:25 2000 +0200
20.2 +++ b/doc-src/TutorialI/fp.tex	Fri Aug 18 10:34:08 2000 +0200
20.3 @@ -185,6 +185,16 @@
20.4  during proofs by simplification.  The same is true for the equations in
20.5  primitive recursive function definitions.
20.6
20.7 +Every datatype $t$ comes equipped with a \isa{size} function from $t$ into
20.8 +the natural numbers (see~\S\ref{sec:nat} below). For lists, \isa{size} is
20.9 +just the length, i.e.\ \isa{size [] = 0} and \isa{size(x \# xs) = size xs +
20.10 +  1}.  In general, \isa{size} returns \isa{0} for all constructors that do
20.11 +not have an argument of type $t$, and for all other constructors \isa{1 +}
20.12 +the sum of the sizes of all arguments of type $t$. Note that because
20.13 +\isa{size} is defined on every datatype, it is overloaded; on lists
20.14 +\isa{size} is also called \isa{length}, which is not overloaded.
20.15 +
20.16 +
20.17  \subsection{Primitive recursion}
20.18
20.19  Functions on datatypes are usually defined by recursion. In fact, most of the
20.20 @@ -267,7 +277,8 @@
20.21
20.22  \begin{warn}
20.23    Induction is only allowed on free (or \isasymAnd-bound) variables that
20.24 -  should not occur among the assumptions of the subgoal.  Case distinction
20.25 +  should not occur among the assumptions of the subgoal; see
20.26 +  \S\ref{sec:ind-var-in-prems} for details. Case distinction
20.27    (\isa{case_tac}) works for arbitrary terms, which need to be
20.28    quoted if they are non-atomic.
20.29  \end{warn}
20.30 @@ -301,6 +312,7 @@
20.31
20.32
20.33  \subsection{Natural numbers}
20.34 +\label{sec:nat}
20.35  \index{arithmetic|(}
20.36
20.37  \input{Misc/document/fakenat.tex}
20.38 @@ -694,8 +706,9 @@
20.39  \input{Datatype/document/ABexpr.tex}
20.40
20.41  \subsection{Nested recursion}
20.42 +\label{sec:nested-datatype}
20.43
20.44 -\input{Datatype/document/Nested.tex}
20.45 +{\makeatother\input{Datatype/document/Nested.tex}}
20.46
20.47
20.48  \subsection{The limits of nested recursion}
20.49 @@ -828,13 +841,25 @@
20.50
20.51  \input{Recdef/document/simplification.tex}
20.52
20.53 -
20.54  \subsection{Induction}
20.55  \index{induction!recursion|(}
20.56  \index{recursion induction|(}
20.57
20.58  \input{Recdef/document/Induction.tex}
20.59 +\label{sec:recdef-induction}
20.60
20.61  \index{induction!recursion|)}
20.62  \index{recursion induction|)}
20.63 +
20.64 +%\subsection{Advanced forms of recursion}
20.65 +
20.66 +%\input{Recdef/document/Nested0.tex}
20.67 +%\input{Recdef/document/Nested1.tex}
20.68 +
20.69  \index{*recdef|)}
20.70 +
20.71 +\section{Advanced induction techniques}

    21.1 --- a/doc-src/TutorialI/tutorial.tex	Thu Aug 17 21:07:25 2000 +0200