# HG changeset patch # User wenzelm # Date 1001700508 -7200 # Node ID 0bec857c98715ddece25e45eeb32af9198109510 # Parent fd242f857508881dfe273bd9a9b2dbd7d57ad5dd oops; diff -r fd242f857508 -r 0bec857c9871 doc-src/TutorialI/Advanced/Partial.thy --- 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 \ nat \ nat" recdef (permissive) divi "measure(\(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 diff -r fd242f857508 -r 0bec857c9871 doc-src/TutorialI/Advanced/WFrec.thy --- 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 \ nat" -recdef (*<*)(permissive)(*<*)f "{(i,j). j i \ (#10::nat)}" +recdef (*<*)(permissive)(*>*)f "{(i,j). j i \ (#10::nat)}" "f i = (if #10 \ i then 0 else i * f(Suc i))" text{*\noindent diff -r fd242f857508 -r 0bec857c9871 doc-src/TutorialI/Advanced/document/WFrec.tex --- 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" diff -r fd242f857508 -r 0bec857c9871 doc-src/TutorialI/Recdef/Nested1.thy --- 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))" diff -r fd242f857508 -r 0bec857c9871 doc-src/TutorialI/Recdef/document/Nested1.tex --- 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" diff -r fd242f857508 -r 0bec857c9871 doc-src/TutorialI/Recdef/document/termination.tex --- 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" diff -r fd242f857508 -r 0bec857c9871 doc-src/TutorialI/Recdef/termination.thy --- 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\nat \ nat" -recdef (*<*)(permissive)(*<*)f "measure(\(x,y). x-y)" +recdef (*<*)(permissive)(*>*)f "measure(\(x,y). x-y)" "f(x,y) = (if x \ y then x else f(x,y+1))" text{*\noindent