summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Fri, 18 Aug 2000 10:34:08 +0200 | |

changeset 9644 | 6b0b6b471855 |

parent 9643 | c94db1a96f4e |

child 9645 | 20ae97cd2a16 |

*** empty log message ***

--- 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

--- 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

--- 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";

--- 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}

--- 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

--- 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

--- 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

--- 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

--- 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. *}; (*<*)

--- 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";

--- 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:

--- 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:%

--- 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{"}%

--- 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}

--- 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}%

--- 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";*)

--- 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:%

--- 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.

--- 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.

--- 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}

--- 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}