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

author | nipkow |

Wed, 30 Aug 2000 18:09:20 +0200 | |

changeset 9754 | a123a64cadeb |

parent 9753 | f25ac7194f71 |

child 9755 | 6fefedeb3428 |

*** empty log message ***

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