*** empty log message ***
authornipkow
Fri Aug 18 10:34:08 2000 +0200 (2000-08-18)
changeset 96446b0b6b471855
parent 9643 c94db1a96f4e
child 9645 20ae97cd2a16
*** empty log message ***
doc-src/TutorialI/Datatype/Fundata.thy
doc-src/TutorialI/Datatype/Nested.thy
doc-src/TutorialI/Datatype/ROOT.ML
doc-src/TutorialI/Datatype/document/ABexpr.tex
doc-src/TutorialI/Datatype/document/Fundata.tex
doc-src/TutorialI/Datatype/document/Nested.tex
doc-src/TutorialI/Ifexpr/document/Ifexpr.tex
doc-src/TutorialI/IsaMakefile
doc-src/TutorialI/Misc/Itrev.thy
doc-src/TutorialI/Misc/ROOT.ML
doc-src/TutorialI/Misc/document/Itrev.tex
doc-src/TutorialI/Misc/document/asm_simp.tex
doc-src/TutorialI/Misc/document/cond_rewr.tex
doc-src/TutorialI/Misc/document/natsum.tex
doc-src/TutorialI/Misc/document/pairs.tex
doc-src/TutorialI/Recdef/ROOT.ML
doc-src/TutorialI/Recdef/document/examples.tex
doc-src/TutorialI/Recdef/document/simplification.tex
doc-src/TutorialI/ToyList/document/ToyList.tex
doc-src/TutorialI/fp.tex
doc-src/TutorialI/tutorial.tex
     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.7 +use_thy "AdvancedInd";
    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}
   20.72 +\label{sec:advanced-ind}
   20.73 +\input{Misc/document/AdvancedInd.tex}
   20.74 +
   20.75 +\input{Datatype/document/Nested2.tex}
    21.1 --- a/doc-src/TutorialI/tutorial.tex	Thu Aug 17 21:07:25 2000 +0200
    21.2 +++ b/doc-src/TutorialI/tutorial.tex	Fri Aug 18 10:34:08 2000 +0200
    21.3 @@ -1,3 +1,4 @@
    21.4 +% pr(latex xsymbols symbols)
    21.5  \documentclass[11pt,a4paper]{report}
    21.6  \usepackage{isabelle,isabellesym}
    21.7  \usepackage{latexsym,verbatim,graphicx,../iman,extra,comment}