--- a/doc-src/TutorialI/Misc/Itrev.thy Wed Aug 30 18:05:20 2000 +0200
+++ b/doc-src/TutorialI/Misc/Itrev.thy Wed Aug 30 18:09:20 2000 +0200
@@ -2,25 +2,29 @@
theory Itrev = Main:;
(*>*)
-text{* Function \isa{rev} has quadratic worst-case running time
-because it calls function \isa{\at} for each element of the list and
-\isa{\at} is linear in its first argument. A linear time version of
-\isa{rev} reqires an extra argument where the result is accumulated
-gradually, using only \isa{\#}:*}
+text{*
+Function @{term"rev"} has quadratic worst-case running time
+because it calls function @{term"@"} for each element of the list and
+@{term"@"} is linear in its first argument. A linear time version of
+@{term"rev"} reqires an extra argument where the result is accumulated
+gradually, using only @{name"#"}:
+*}
consts itrev :: "'a list \\<Rightarrow> 'a list \\<Rightarrow> 'a list";
primrec
"itrev [] ys = ys"
"itrev (x#xs) ys = itrev xs (x#ys)";
-text{*\noindent The behaviour of \isa{itrev} is simple: it reverses
+text{*\noindent
+The behaviour of @{term"itrev"} is simple: it reverses
its first argument by stacking its elements onto the second argument,
and returning that second argument when the first one becomes
-empty. Note that \isa{itrev} is tail-recursive, i.e.\ it can be
+empty. Note that @{term"itrev"} is tail-recursive, i.e.\ it can be
compiled into a loop.
-Naturally, we would like to show that \isa{itrev} does indeed reverse
-its first argument provided the second one is empty: *};
+Naturally, we would like to show that @{term"itrev"} does indeed reverse
+its first argument provided the second one is empty:
+*};
lemma "itrev xs [] = rev xs";
@@ -37,47 +41,46 @@
\end{isabelle}
Just as predicted above, the overall goal, and hence the induction
hypothesis, is too weak to solve the induction step because of the fixed
-\isa{[]}. The corresponding heuristic:
+@{term"[]"}. The corresponding heuristic:
\begin{quote}
-{\em 3. Generalize goals for induction by replacing constants by variables.}
+\emph{Generalize goals for induction by replacing constants by variables.}
\end{quote}
-
-Of course one cannot do this na\"{\i}vely: \isa{itrev xs ys = rev xs} is
+Of course one cannot do this na\"{\i}vely: @{term"itrev xs ys = rev xs"} is
just not true---the correct generalization is
*};
(*<*)oops;(*>*)
lemma "itrev xs ys = rev xs @ ys";
txt{*\noindent
-If \isa{ys} is replaced by \isa{[]}, the right-hand side simplifies to
+If @{term"ys"} is replaced by @{term"[]"}, the right-hand side simplifies to
@{term"rev 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
the main source of complications in inductive proofs.
-Although we now have two variables, only \isa{xs} is suitable for
+Although we now have two variables, only @{term"xs"} is suitable for
induction, and we repeat our above proof attempt. Unfortunately, we are still
not there:
\begin{isabelle}
~1.~{\isasymAnd}a~list.\isanewline
~~~~~~~itrev~list~ys~=~rev~list~@~ys~{\isasymLongrightarrow}\isanewline
-~~~~~~~itrev~list~(a~\#~ys)~=~rev~list~@~a~\#~ys%
+~~~~~~~itrev~list~(a~\#~ys)~=~rev~list~@~a~\#~ys
\end{isabelle}
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
+intuition to generalize: the problem is that @{term"ys"} is fixed throughout
the subgoal, but the induction hypothesis needs to be applied with
-@{term"a # ys"} instead of \isa{ys}. Hence we prove the theorem
-for all \isa{ys} instead of a fixed one:
+@{term"a # ys"} instead of @{term"ys"}. Hence we prove the theorem
+for all @{term"ys"} instead of a fixed one:
*};
(*<*)oops;(*>*)
lemma "\\<forall>ys. itrev xs ys = rev xs @ ys";
txt{*\noindent
-This time induction on \isa{xs} followed by simplification succeeds. This
+This time induction on @{term"xs"} followed by simplification succeeds. This
leads to another heuristic for generalization:
\begin{quote}
-{\em 4. Generalize goals for induction by universally quantifying all free
+\emph{Generalize goals for induction by universally quantifying all free
variables {\em(except the induction variable itself!)}.}
\end{quote}
This prevents trivial failures like the above and does not change the
--- a/doc-src/TutorialI/Misc/document/Itrev.tex Wed Aug 30 18:05:20 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex Wed Aug 30 18:09:20 2000 +0200
@@ -38,9 +38,8 @@
hypothesis, is too weak to solve the induction step because of the fixed
\isa{[]}. The corresponding heuristic:
\begin{quote}
-{\em 3. Generalize goals for induction by replacing constants by variables.}
+\emph{Generalize goals for induction by replacing constants by variables.}
\end{quote}
-
Of course one cannot do this na\"{\i}vely: \isa{itrev xs ys = rev xs} is
just not true---the correct generalization is%
\end{isamarkuptxt}%
@@ -74,7 +73,7 @@
This time induction on \isa{xs} followed by simplification succeeds. This
leads to another heuristic for generalization:
\begin{quote}
-{\em 4. Generalize goals for induction by universally quantifying all free
+\emph{Generalize goals for induction by universally quantifying all free
variables {\em(except the induction variable itself!)}.}
\end{quote}
This prevents trivial failures like the above and does not change the
--- a/doc-src/TutorialI/Recdef/Nested0.thy Wed Aug 30 18:05:20 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Nested0.thy Wed Aug 30 18:09:20 2000 +0200
@@ -15,9 +15,7 @@
you needed to reprove many lemmas reminiscent of similar lemmas about
@{term"rev"}. We will now show you how \isacommand{recdef} can simplify
definitions and proofs about nested recursive datatypes. As an example we
-chose exercise~\ref{ex:trev-trev}:
-
-FIXME: declare trev now!
+choose exercise~\ref{ex:trev-trev}:
*}
(* consts trev :: "('a,'b)term => ('a,'b)term" *)
(*<*)
--- a/doc-src/TutorialI/Recdef/Nested1.thy Wed Aug 30 18:05:20 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Nested1.thy Wed Aug 30 18:09:20 2000 +0200
@@ -1,12 +1,12 @@
(*<*)
theory Nested1 = Nested0:;
(*>*)
-consts trev :: "('a,'b)term => ('a,'b)term";
+consts trev :: "('a,'b)term \<Rightarrow> ('a,'b)term";
text{*\noindent
Although the definition of @{term"trev"} is quite natural, we will have
overcome a minor difficulty in convincing Isabelle of is termination.
-It is precisely this difficulty that is the \textit{rasion d'\^etre} of
+It is precisely this difficulty that is the \textit{raison d'\^etre} of
this subsection.
Defining @{term"trev"} by \isacommand{recdef} rather than \isacommand{primrec}
@@ -15,30 +15,30 @@
*};
recdef trev "measure size"
- "trev (Var x) = Var x"
+ "trev (Var x) = Var x"
"trev (App f ts) = App f (rev(map trev ts))";
-text{*
-FIXME: recdef should complain and generate unprovable termination condition!
-moveto todo
-
+text{*\noindent
Remember that function @{term"size"} is defined for each \isacommand{datatype}.
-However, the definition does not succeed. Isabelle complains about an unproved termination
-condition
+However, the definition does not succeed. Isabelle complains about an
+unproved termination condition
\begin{quote}
-@{term[display]"t : set ts --> size t < Suc (term_size ts)"}
+@{term[display]"t : set ts --> size t < Suc (term_list_size ts)"}
\end{quote}
-where @{term"set"} returns the set of elements of a list---no special knowledge of sets is
-required in the following.
-First we have to understand why the recursive call of @{term"trev"} underneath @{term"map"} leads
-to the above condition. The reason is that \isacommand{recdef} ``knows'' that @{term"map"} will
-apply @{term"trev"} only to elements of @{term"ts"}. Thus the above condition expresses that
-the size of the argument @{term"t : set ts"} of any recursive call of @{term"trev"} is strictly
-less than @{term"size(App f ts) = Suc(term_size ts)"}.
-We will now prove the termination condition and continue with our definition.
-Below we return to the question of how \isacommand{recdef} ``knows'' about @{term"map"}.
+where @{term"set"} returns the set of elements of a list (no special
+knowledge of sets is required in the following) and @{name"term_list_size ::
+term list \<Rightarrow> nat"} is an auxiliary function automatically defined by Isabelle
+(when @{name"term"} was defined). First we have to understand why the
+recursive call of @{term"trev"} underneath @{term"map"} leads to the above
+condition. The reason is that \isacommand{recdef} ``knows'' that @{term"map"}
+will apply @{term"trev"} only to elements of @{term"ts"}. Thus the above
+condition expresses that the size of the argument @{term"t : set ts"} of any
+recursive call of @{term"trev"} is strictly less than @{term"size(App f ts) =
+Suc(term_list_size ts)"}. We will now prove the termination condition and
+continue with our definition. Below we return to the question of how
+\isacommand{recdef} ``knows'' about @{term"map"}.
*};
(*<*)
end;
-(*>*)
\ No newline at end of file
+(*>*)
--- a/doc-src/TutorialI/Recdef/Nested2.thy Wed Aug 30 18:05:20 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Nested2.thy Wed Aug 30 18:09:20 2000 +0200
@@ -7,7 +7,7 @@
The termintion condition is easily proved by induction:
*};
-lemma [simp]: "t \\<in> set ts \\<longrightarrow> size t < Suc(term_size ts)";
+lemma [simp]: "t \<in> set ts \<longrightarrow> size t < Suc(term_list_size ts)";
by(induct_tac ts, auto);
(*<*)
recdef trev "measure size"
@@ -19,7 +19,7 @@
applies it automatically and the above definition of @{term"trev"}
succeeds now. As a reward for our effort, we can now prove the desired
lemma directly. The key is the fact that we no longer need the verbose
-induction schema for type \isa{term} but the simpler one arising from
+induction schema for type @{name"term"} but the simpler one arising from
@{term"trev"}:
*};
@@ -38,8 +38,8 @@
text{*\noindent
If the proof of the induction step mystifies you, we recommend to go through
-the chain of simplification steps in detail, probably with the help of
-\isa{trace\_simp}.
+the chain of simplification steps in detail; you will probably need the help of
+@{name"trace_simp"}.
%\begin{quote}
%{term[display]"trev(trev(App f ts))"}\\
%{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\
@@ -50,9 +50,9 @@
%{term[display]"App f ts"}
%\end{quote}
-The above definition of @{term"trev"} is superior to the one in \S\ref{sec:nested-datatype}
-because it brings @{term"rev"} into play, about which already know a lot, in particular
-@{prop"rev(rev xs) = xs"}.
+The above definition of @{term"trev"} is superior to the one in
+\S\ref{sec:nested-datatype} because it brings @{term"rev"} into play, about
+which already know a lot, in particular @{prop"rev(rev xs) = xs"}.
Thus this proof is a good example of an important principle:
\begin{quote}
\emph{Chose your definitions carefully\\
@@ -64,9 +64,9 @@
like @{term"map"}. For a start, if nothing were known about @{term"map"},
@{term"map trev ts"} might apply @{term"trev"} to arbitrary terms, and thus
\isacommand{recdef} would try to prove the unprovable @{term"size t < Suc
-(term_size ts)"}, without any assumption about \isa{t}. Therefore
+(term_list_size ts)"}, without any assumption about @{term"t"}. Therefore
\isacommand{recdef} has been supplied with the congruence theorem
-\isa{map\_cong}:
+@{name"map_cong"}:
\begin{quote}
@{thm[display,margin=50]"map_cong"[no_vars]}
\end{quote}
--- a/doc-src/TutorialI/Recdef/document/Nested0.tex Wed Aug 30 18:05:20 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested0.tex Wed Aug 30 18:09:20 2000 +0200
@@ -13,9 +13,7 @@
you needed to reprove many lemmas reminiscent of similar lemmas about
\isa{rev}. We will now show you how \isacommand{recdef} can simplify
definitions and proofs about nested recursive datatypes. As an example we
-chose exercise~\ref{ex:trev-trev}:
-
-FIXME: declare trev now!%
+choose exercise~\ref{ex:trev-trev}:%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Recdef/document/Nested1.tex Wed Aug 30 18:05:20 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested1.tex Wed Aug 30 18:09:20 2000 +0200
@@ -1,11 +1,11 @@
%
\begin{isabellebody}%
-\isacommand{consts}\ trev\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ {\isacharequal}{\isachargreater}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}%
+\isacommand{consts}\ trev\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
Although the definition of \isa{trev} is quite natural, we will have
overcome a minor difficulty in convincing Isabelle of is termination.
-It is precisely this difficulty that is the \textit{rasion d'\^etre} of
+It is precisely this difficulty that is the \textit{raison d'\^etre} of
this subsection.
Defining \isa{trev} by \isacommand{recdef} rather than \isacommand{primrec}
@@ -13,31 +13,30 @@
suggested at the end of \S\ref{sec:nested-datatype}:%
\end{isamarkuptext}%
\isacommand{recdef}\ trev\ {\isachardoublequote}measure\ size{\isachardoublequote}\isanewline
-\ {\isachardoublequote}trev\ {\isacharparenleft}Var\ x{\isacharparenright}\ {\isacharequal}\ Var\ x{\isachardoublequote}\isanewline
+\ {\isachardoublequote}trev\ {\isacharparenleft}Var\ x{\isacharparenright}\ \ \ \ {\isacharequal}\ Var\ x{\isachardoublequote}\isanewline
\ {\isachardoublequote}trev\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}rev{\isacharparenleft}map\ trev\ ts{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
-FIXME: recdef should complain and generate unprovable termination condition!
-moveto todo
-
+\noindent
Remember that function \isa{size} is defined for each \isacommand{datatype}.
-However, the definition does not succeed. Isabelle complains about an unproved termination
-condition
+However, the definition does not succeed. Isabelle complains about an
+unproved termination condition
\begin{quote}
\begin{isabelle}%
-\mbox{t}\ {\isasymin}\ set\ \mbox{ts}\ {\isasymlongrightarrow}\ size\ \mbox{t}\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}size\ \mbox{ts}{\isacharparenright}
+\mbox{t}\ {\isasymin}\ set\ \mbox{ts}\ {\isasymlongrightarrow}\ size\ \mbox{t}\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ \mbox{ts}{\isacharparenright}
\end{isabelle}%
\end{quote}
-where \isa{set} returns the set of elements of a list---no special knowledge of sets is
-required in the following.
-First we have to understand why the recursive call of \isa{trev} underneath \isa{map} leads
-to the above condition. The reason is that \isacommand{recdef} ``knows'' that \isa{map} will
-apply \isa{trev} only to elements of \isa{\mbox{ts}}. Thus the above condition expresses that
-the size of the argument \isa{\mbox{t}\ {\isasymin}\ set\ \mbox{ts}} of any recursive call of \isa{trev} is strictly
-less than \isa{size\ {\isacharparenleft}App\ \mbox{f}\ \mbox{ts}{\isacharparenright}\ {\isacharequal}\ Suc\ {\isacharparenleft}term{\isacharunderscore}size\ \mbox{ts}{\isacharparenright}}.
-We will now prove the termination condition and continue with our definition.
-Below we return to the question of how \isacommand{recdef} ``knows'' about \isa{map}.%
+where \isa{set} returns the set of elements of a list (no special
+knowledge of sets is required in the following) and \isa{term{\isacharunderscore}list{\isacharunderscore}size\ {\isacharcolon}{\isacharcolon}\ term\ list\ {\isasymRightarrow}\ nat} is an auxiliary function automatically defined by Isabelle
+(when \isa{term} was defined). First we have to understand why the
+recursive call of \isa{trev} underneath \isa{map} leads to the above
+condition. The reason is that \isacommand{recdef} ``knows'' that \isa{map}
+will apply \isa{trev} only to elements of \isa{\mbox{ts}}. Thus the above
+condition expresses that the size of the argument \isa{\mbox{t}\ {\isasymin}\ set\ \mbox{ts}} of any
+recursive call of \isa{trev} is strictly less than \isa{size\ {\isacharparenleft}App\ \mbox{f}\ \mbox{ts}{\isacharparenright}\ {\isacharequal}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ \mbox{ts}{\isacharparenright}}. We will now prove the termination condition and
+continue with our definition. Below we return to the question of how
+\isacommand{recdef} ``knows'' about \isa{map}.%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Recdef/document/Nested2.tex Wed Aug 30 18:05:20 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested2.tex Wed Aug 30 18:09:20 2000 +0200
@@ -5,7 +5,7 @@
\noindent
The termintion condition is easily proved by induction:%
\end{isamarkuptext}%
-\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc{\isacharparenleft}term{\isacharunderscore}size\ ts{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc{\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}{\isachardoublequote}\isanewline
\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ ts{\isacharcomma}\ auto{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
@@ -36,8 +36,8 @@
\begin{isamarkuptext}%
\noindent
If the proof of the induction step mystifies you, we recommend to go through
-the chain of simplification steps in detail, probably with the help of
-\isa{trace\_simp}.
+the chain of simplification steps in detail; you will probably need the help of
+\isa{trace{\isacharunderscore}simp}.
%\begin{quote}
%{term[display]"trev(trev(App f ts))"}\\
%{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\
@@ -48,9 +48,9 @@
%{term[display]"App f ts"}
%\end{quote}
-The above definition of \isa{trev} is superior to the one in \S\ref{sec:nested-datatype}
-because it brings \isa{rev} into play, about which already know a lot, in particular
-\isa{rev\ {\isacharparenleft}rev\ \mbox{xs}{\isacharparenright}\ {\isacharequal}\ \mbox{xs}}.
+The above definition of \isa{trev} is superior to the one in
+\S\ref{sec:nested-datatype} because it brings \isa{rev} into play, about
+which already know a lot, in particular \isa{rev\ {\isacharparenleft}rev\ \mbox{xs}{\isacharparenright}\ {\isacharequal}\ \mbox{xs}}.
Thus this proof is a good example of an important principle:
\begin{quote}
\emph{Chose your definitions carefully\\
@@ -61,9 +61,9 @@
sensible termination conditions in the presence of higher-order functions
like \isa{map}. For a start, if nothing were known about \isa{map},
\isa{map\ trev\ \mbox{ts}} might apply \isa{trev} to arbitrary terms, and thus
-\isacommand{recdef} would try to prove the unprovable \isa{size\ \mbox{t}\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}size\ \mbox{ts}{\isacharparenright}}, without any assumption about \isa{t}. Therefore
+\isacommand{recdef} would try to prove the unprovable \isa{size\ \mbox{t}\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ \mbox{ts}{\isacharparenright}}, without any assumption about \isa{\mbox{t}}. Therefore
\isacommand{recdef} has been supplied with the congruence theorem
-\isa{map\_cong}:
+\isa{map{\isacharunderscore}cong}:
\begin{quote}
\begin{isabelle}%
--- a/doc-src/TutorialI/Recdef/document/simplification.tex Wed Aug 30 18:05:20 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex Wed Aug 30 18:09:20 2000 +0200
@@ -26,7 +26,7 @@
is provded automatically because it is already present as a lemma in the
arithmetic library. Thus the recursion equation becomes a simplification
rule. Of course the equation is nonterminating if we are allowed to unfold
-the recursive call inside the \isa{else} branch, which is why programming
+the recursive call inside the \isa{if} branch, which is why programming
languages and our simplifier don't do that. Unfortunately the simplifier does
something else which leads to the same problem: it splits \isa{if}s if the
condition simplifies to neither \isa{True} nor \isa{False}. For
@@ -59,11 +59,10 @@
simplification steps. Fortunately, this problem can be avoided in many
different ways.
-The most radical solution is to disable the offending
-\isa{split_if} as shown in the section on case splits in
-\S\ref{sec:SimpFeatures}.
-However, we do not recommend this because it means you will often have to
-invoke the rule explicitly when \isa{if} is involved.
+The most radical solution is to disable the offending \\isa{split{\isacharunderscore}if} as
+shown in the section on case splits in \S\ref{sec:Simplification}. However,
+we do not recommend this because it means you will often have to invoke the
+rule explicitly when \isa{if} is involved.
If possible, the definition should be given by pattern matching on the left
rather than \isa{if} on the right. In the case of \isa{gcd} the
@@ -76,7 +75,7 @@
\begin{isamarkuptext}%
\noindent
Note that the order of equations is important and hides the side condition
-\isa{n \isasymnoteq\ 0}. Unfortunately, in general the case distinction
+\isa{\mbox{n}\ {\isasymnoteq}\ \isadigit{0}}. Unfortunately, in general the case distinction
may not be expressible by pattern matching.
A very simple alternative is to replace \isa{if} by \isa{case}, which
--- a/doc-src/TutorialI/Recdef/simplification.thy Wed Aug 30 18:05:20 2000 +0200
+++ b/doc-src/TutorialI/Recdef/simplification.thy Wed Aug 30 18:09:20 2000 +0200
@@ -7,7 +7,7 @@
equations become simplification rules, just as with
\isacommand{primrec}. In most cases this works fine, but there is a subtle
problem that must be mentioned: simplification may not
-terminate because of automatic splitting of \isa{if}.
+terminate because of automatic splitting of @{name"if"}.
Let us look at an example:
*}
@@ -24,10 +24,10 @@
is provded automatically because it is already present as a lemma in the
arithmetic library. Thus the recursion equation becomes a simplification
rule. Of course the equation is nonterminating if we are allowed to unfold
-the recursive call inside the \isa{else} branch, which is why programming
+the recursive call inside the @{name"if"} branch, which is why programming
languages and our simplifier don't do that. Unfortunately the simplifier does
-something else which leads to the same problem: it splits \isa{if}s if the
-condition simplifies to neither \isa{True} nor \isa{False}. For
+something else which leads to the same problem: it splits @{name"if"}s if the
+condition simplifies to neither @{term"True"} nor @{term"False"}. For
example, simplification reduces
\begin{quote}
@{term[display]"gcd(m,n) = k"}
@@ -41,18 +41,17 @@
@{term[display]"(n=0 --> m=k) & (n ~= 0 --> gcd(n, m mod n)=k)"}
\end{quote}
Since the recursive call @{term"gcd(n, m mod n)"} is no longer protected by
-an \isa{if}, it is unfolded again, which leads to an infinite chain of
+an @{name"if"}, it is unfolded again, which leads to an infinite chain of
simplification steps. Fortunately, this problem can be avoided in many
different ways.
-The most radical solution is to disable the offending
-\isa{split_if} as shown in the section on case splits in
-\S\ref{sec:SimpFeatures}.
-However, we do not recommend this because it means you will often have to
-invoke the rule explicitly when \isa{if} is involved.
+The most radical solution is to disable the offending \@{name"split_if"} as
+shown in the section on case splits in \S\ref{sec:Simplification}. However,
+we do not recommend this because it means you will often have to invoke the
+rule explicitly when @{name"if"} is involved.
If possible, the definition should be given by pattern matching on the left
-rather than \isa{if} on the right. In the case of \isa{gcd} the
+rather than @{name"if"} on the right. In the case of @{term"gcd"} the
following alternative definition suggests itself:
*}
@@ -64,11 +63,11 @@
text{*\noindent
Note that the order of equations is important and hides the side condition
-\isa{n \isasymnoteq\ 0}. Unfortunately, in general the case distinction
+@{prop"n ~= 0"}. Unfortunately, in general the case distinction
may not be expressible by pattern matching.
-A very simple alternative is to replace \isa{if} by \isa{case}, which
-is also available for \isa{bool} but is not split automatically:
+A very simple alternative is to replace @{name"if"} by @{name"case"}, which
+is also available for @{typ"bool"} but is not split automatically:
*}
consts gcd2 :: "nat*nat \\<Rightarrow> nat";
@@ -79,7 +78,7 @@
In fact, this is probably the neatest solution next to pattern matching.
A final alternative is to replace the offending simplification rules by
-derived conditional ones. For \isa{gcd} it means we have to prove
+derived conditional ones. For @{term"gcd"} it means we have to prove
*}
lemma [simp]: "gcd (m, 0) = m";
--- a/doc-src/TutorialI/fp.tex Wed Aug 30 18:05:20 2000 +0200
+++ b/doc-src/TutorialI/fp.tex Wed Aug 30 18:09:20 2000 +0200
@@ -405,16 +405,12 @@
Simplification is one of the central theorem proving tools in Isabelle and
many other systems. The tool itself is called the \bfindex{simplifier}. The
-purpose of this section is twofold: to introduce the many features of the
-simplifier (\S\ref{sec:SimpFeatures}) and to explain a little bit how the
-simplifier works (\S\ref{sec:SimpHow}). Anybody intending to use HOL should
-read \S\ref{sec:SimpFeatures}, and the serious student should read
-\S\ref{sec:SimpHow} as well in order to understand what happened in case
-things do not simplify as expected.
-
-
-\subsection{Using the simplifier}
-\label{sec:SimpFeatures}
+purpose of this section is introduce the many features of the simplifier.
+Anybody intending to use HOL should read this section. Later on
+(\S\ref{sec:simplification-II}) we explain some more advanced features and a
+little bit of how the simplifier works. The serious student should read that
+section as well, in particular in order to understand what happened if things
+do not simplify as expected.
\subsubsection{What is simplification}
@@ -572,11 +568,11 @@
inductive proofs. The first one we have already mentioned in our initial
example:
\begin{quote}
-{\em 1. Theorems about recursive functions are proved by induction.}
+\emph{Theorems about recursive functions are proved by induction.}
\end{quote}
In case the function has more than one argument
\begin{quote}
-{\em 2. Do induction on argument number $i$ if the function is defined by
+\emph{Do induction on argument number $i$ if the function is defined by
recursion in argument number $i$.}
\end{quote}
When we look at the proof of {\makeatother\isa{(xs @ ys) @ zs = xs @ (ys @
@@ -598,8 +594,8 @@
side, the simpler \isa{rev} on the right-hand side. This constitutes
another, albeit weak heuristic that is not restricted to induction:
\begin{quote}
- {\em 5. The right-hand side of an equation should (in some sense) be
- simpler than the left-hand side.}
+ \emph{The right-hand side of an equation should (in some sense) be simpler
+ than the left-hand side.}
\end{quote}
The heuristic is tricky to apply because it is not obvious that
\isa{rev xs \at\ ys} is simpler than \isa{itrev xs ys}. But see what
--- a/doc-src/TutorialI/tricks.tex Wed Aug 30 18:05:20 2000 +0200
+++ b/doc-src/TutorialI/tricks.tex Wed Aug 30 18:09:20 2000 +0200
@@ -1,6 +1,7 @@
\chapter{The Tricks of the Trade}
\section{Simplification}
+\label{sec:simplification-II}
\index{simplification|(}
\subsection{Advanced features}