--- a/doc-src/TutorialI/Advanced/Partial.thy Fri Sep 28 20:08:05 2001 +0200
+++ b/doc-src/TutorialI/Advanced/Partial.thy Fri Sep 28 20:08:28 2001 +0200
@@ -64,7 +64,7 @@
consts divi :: "nat \<times> nat \<Rightarrow> nat"
recdef (permissive) divi "measure(\<lambda>(m,n). m)"
"divi(m,n) = (if n = 0 then arbitrary else
- if m < n then 0 else divi(m-n,n)+1)" (* FIXME permissive!? *)
+ if m < n then 0 else divi(m-n,n)+1)" (* FIXME hide permissive!? *)
text{*\noindent Of course we could also have defined
@{term"divi(m,0)"} to be some specific number, for example 0. The
--- a/doc-src/TutorialI/Advanced/WFrec.thy Fri Sep 28 20:08:05 2001 +0200
+++ b/doc-src/TutorialI/Advanced/WFrec.thy Fri Sep 28 20:08:28 2001 +0200
@@ -67,7 +67,7 @@
*}
consts f :: "nat \<Rightarrow> nat"
-recdef (*<*)(permissive)(*<*)f "{(i,j). j<i \<and> i \<le> (#10::nat)}"
+recdef (*<*)(permissive)(*>*)f "{(i,j). j<i \<and> i \<le> (#10::nat)}"
"f i = (if #10 \<le> i then 0 else i * f(Suc i))"
text{*\noindent
--- a/doc-src/TutorialI/Advanced/document/WFrec.tex Fri Sep 28 20:08:05 2001 +0200
+++ b/doc-src/TutorialI/Advanced/document/WFrec.tex Fri Sep 28 20:08:28 2001 +0200
@@ -65,7 +65,57 @@
of a recursive function that calls itself with increasing values up to ten:%
\end{isamarkuptext}%
\isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
-\isacommand{recdef}\ \end{isabellebody}%
+\isacommand{recdef}\ f\ {\isachardoublequote}{\isacharbraceleft}{\isacharparenleft}i{\isacharcomma}j{\isacharparenright}{\isachardot}\ j{\isacharless}i\ {\isasymand}\ i\ {\isasymle}\ {\isacharparenleft}{\isacharhash}{\isadigit{1}}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharbraceright}{\isachardoublequote}\isanewline
+{\isachardoublequote}f\ i\ {\isacharequal}\ {\isacharparenleft}if\ {\isacharhash}{\isadigit{1}}{\isadigit{0}}\ {\isasymle}\ i\ then\ {\isadigit{0}}\ else\ i\ {\isacharasterisk}\ f{\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
+\begin{isamarkuptext}%
+\noindent
+Since \isacommand{recdef} is not prepared for the relation supplied above,
+Isabelle rejects the definition. We should first have proved that
+our relation was well-founded:%
+\end{isamarkuptext}%
+\isacommand{lemma}\ wf{\isacharunderscore}greater{\isacharcolon}\ {\isachardoublequote}wf\ {\isacharbraceleft}{\isacharparenleft}i{\isacharcomma}j{\isacharparenright}{\isachardot}\ j{\isacharless}i\ {\isasymand}\ i\ {\isasymle}\ {\isacharparenleft}N{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharbraceright}{\isachardoublequote}%
+\begin{isamarkuptxt}%
+\noindent
+The proof is by showing that our relation is a subset of another well-founded
+relation: one given by a measure function.\index{*wf_subset (theorem)}%
+\end{isamarkuptxt}%
+\isacommand{apply}\ {\isacharparenleft}rule\ wf{\isacharunderscore}subset\ {\isacharbrackleft}of\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}k{\isacharcolon}{\isacharcolon}nat{\isachardot}\ N{\isacharminus}k{\isacharparenright}{\isachardoublequote}{\isacharbrackright}{\isacharcomma}\ blast{\isacharparenright}%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isacharbraceleft}{\isacharparenleft}i{\isacharcomma}\ j{\isacharparenright}{\isachardot}\ j\ {\isacharless}\ i\ {\isasymand}\ i\ {\isasymle}\ N{\isacharbraceright}\ {\isasymsubseteq}\ measure\ {\isacharparenleft}op\ {\isacharminus}\ N{\isacharparenright}%
+\end{isabelle}
+
+\noindent
+The inclusion remains to be proved. After unfolding some definitions,
+we are left with simple arithmetic:%
+\end{isamarkuptxt}%
+\isacommand{apply}\ {\isacharparenleft}clarify{\isacharcomma}\ simp\ add{\isacharcolon}\ measure{\isacharunderscore}def\ inv{\isacharunderscore}image{\isacharunderscore}def{\isacharparenright}%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ b{\isachardot}\ {\isasymlbrakk}b\ {\isacharless}\ a{\isacharsemicolon}\ a\ {\isasymle}\ N{\isasymrbrakk}\ {\isasymLongrightarrow}\ N\ {\isacharminus}\ a\ {\isacharless}\ N\ {\isacharminus}\ b%
+\end{isabelle}
+
+\noindent
+And that is dispatched automatically:%
+\end{isamarkuptxt}%
+\isacommand{by}\ arith%
+\begin{isamarkuptext}%
+\noindent
+
+Armed with this lemma, we use the \attrdx{recdef_wf} attribute to attach a
+crucial hint to our definition:%
+\end{isamarkuptext}%
+{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}wf{\isacharcolon}\ wf{\isacharunderscore}greater{\isacharparenright}%
+\begin{isamarkuptext}%
+\noindent
+Alternatively, we could have given \isa{measure\ {\isacharparenleft}{\isasymlambda}k{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isacharhash}{\isadigit{1}}{\isadigit{0}}{\isacharminus}k{\isacharparenright}} for the
+well-founded relation in our \isacommand{recdef}. However, the arithmetic
+goal in the lemma above would have arisen instead in the \isacommand{recdef}
+termination proof, where we have less control. A tailor-made termination
+relation makes even more sense when it can be used in several function
+declarations.%
+\end{isamarkuptext}%
+\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Recdef/Nested1.thy Fri Sep 28 20:08:05 2001 +0200
+++ b/doc-src/TutorialI/Recdef/Nested1.thy Fri Sep 28 20:08:28 2001 +0200
@@ -13,7 +13,7 @@
suggested at the end of \S\ref{sec:nested-datatype}:
*}
-recdef (*<*)(permissive)(*<*)trev "measure size"
+recdef (*<*)(permissive)(*>*)trev "measure size"
"trev (Var x) = Var x"
"trev (App f ts) = App f (rev(map trev ts))"
--- a/doc-src/TutorialI/Recdef/document/Nested1.tex Fri Sep 28 20:08:05 2001 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested1.tex Fri Sep 28 20:08:28 2001 +0200
@@ -13,7 +13,31 @@
simplifies matters because we are now free to use the recursion equation
suggested at the end of \S\ref{sec:nested-datatype}:%
\end{isamarkuptext}%
-\isacommand{recdef}\ \end{isabellebody}%
+\isacommand{recdef}\ trev\ {\isachardoublequote}measure\ size{\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}%
+\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
+\begin{isabelle}%
+\ \ \ \ \ t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}%
+\end{isabelle}
+where \isa{set} returns the set of elements of a list
+and \isa{term{\isacharunderscore}list{\isacharunderscore}size\ {\isacharcolon}{\isacharcolon}\ term\ list\ {\isasymRightarrow}\ nat} is an auxiliary
+function automatically defined by Isabelle
+(while processing the declaration of \isa{term}). Why does the
+recursive call of \isa{trev} lead to this
+condition? Because \isacommand{recdef} knows that \isa{map}
+will apply \isa{trev} only to elements of \isa{ts}. Thus the
+condition expresses that the size of the argument \isa{t\ {\isasymin}\ set\ ts} of any
+recursive call of \isa{trev} is strictly less than \isa{size\ {\isacharparenleft}App\ f\ ts{\isacharparenright}},
+which equals \isa{Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ 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:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Recdef/document/termination.tex Fri Sep 28 20:08:05 2001 +0200
+++ b/doc-src/TutorialI/Recdef/document/termination.tex Fri Sep 28 20:08:28 2001 +0200
@@ -17,7 +17,69 @@
recursive call. Let us try the following artificial function:%
\end{isamarkuptext}%
\isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
-\isacommand{recdef}\ \end{isabellebody}%
+\isacommand{recdef}\ f\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}f{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymle}\ y\ then\ x\ else\ f{\isacharparenleft}x{\isacharcomma}y{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
+\begin{isamarkuptext}%
+\noindent
+Isabelle prints a
+\REMARK{error or warning? change this part? rename g to f?}
+message showing you what it was unable to prove. You will then
+have to prove it as a separate lemma before you attempt the definition
+of your function once more. In our case the required lemma is the obvious one:%
+\end{isamarkuptext}%
+\isacommand{lemma}\ termi{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ x\ {\isasymle}\ y\ {\isasymLongrightarrow}\ x\ {\isacharminus}\ Suc\ y\ {\isacharless}\ x\ {\isacharminus}\ y{\isachardoublequote}%
+\begin{isamarkuptxt}%
+\noindent
+It was not proved automatically because of the awkward behaviour of subtraction
+on type \isa{nat}. This requires more arithmetic than is tried by default:%
+\end{isamarkuptxt}%
+\isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline
+\isacommand{done}%
+\begin{isamarkuptext}%
+\noindent
+Because \isacommand{recdef}'s termination prover involves simplification,
+we include in our second attempt a hint: the \attrdx{recdef_simp} attribute
+says to use \isa{termi{\isacharunderscore}lem} as
+a simplification rule.%
+\end{isamarkuptext}%
+\isacommand{consts}\ g\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
+\isacommand{recdef}\ g\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}g{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymle}\ y\ then\ x\ else\ g{\isacharparenleft}x{\isacharcomma}y{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
+{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}\ termi{\isacharunderscore}lem{\isacharparenright}%
+\begin{isamarkuptext}%
+\noindent
+This time everything works fine. Now \isa{g{\isachardot}simps} contains precisely
+the stated recursion equation for \isa{g}, which has been stored as a
+simplification rule. Thus we can automatically prove results such as this one:%
+\end{isamarkuptext}%
+\isacommand{theorem}\ {\isachardoublequote}g{\isacharparenleft}{\isadigit{1}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ g{\isacharparenleft}{\isadigit{1}}{\isacharcomma}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
+\isacommand{done}%
+\begin{isamarkuptext}%
+\noindent
+More exciting theorems require induction, which is discussed below.
+
+If the termination proof requires a new lemma that is of general use, you can
+turn it permanently into a simplification rule, in which case the above
+\isacommand{hint} is not necessary. But our \isa{termi{\isacharunderscore}lem} is not
+sufficiently general to warrant this distinction.
+
+The attentive reader may wonder why we chose to call our function \isa{g}
+rather than \isa{f} the second time around. The reason is that, despite
+the failed termination proof, the definition of \isa{f} did not
+fail, and thus we could not define it a second time. However, all theorems
+about \isa{f}, for example \isa{f{\isachardot}simps}, carry as a precondition
+the unproved termination condition. Moreover, the theorems
+\isa{f{\isachardot}simps} are not stored as simplification rules.
+However, this mechanism
+allows a delayed proof of termination: instead of proving
+\isa{termi{\isacharunderscore}lem} up front, we could prove
+it later on and then use it to remove the preconditions from the theorems
+about \isa{f}. In most cases this is more cumbersome than proving things
+up front.
+\REMARK{FIXME, with one exception: nested recursion.}%
+\end{isamarkuptext}%
+\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Recdef/termination.thy Fri Sep 28 20:08:05 2001 +0200
+++ b/doc-src/TutorialI/Recdef/termination.thy Fri Sep 28 20:08:28 2001 +0200
@@ -17,7 +17,7 @@
recursive call. Let us try the following artificial function:*}
consts f :: "nat\<times>nat \<Rightarrow> nat"
-recdef (*<*)(permissive)(*<*)f "measure(\<lambda>(x,y). x-y)"
+recdef (*<*)(permissive)(*>*)f "measure(\<lambda>(x,y). x-y)"
"f(x,y) = (if x \<le> y then x else f(x,y+1))"
text{*\noindent