# HG changeset patch # User wenzelm # Date 1001697526 -7200 # Node ID abf9cda4a4d20ef928f553f11d864201b4c2bea8 # Parent 0dbfb578bf7571dd9e6c4a7971496e246c33d7a7 updated; diff -r 0dbfb578bf75 -r abf9cda4a4d2 doc-src/TutorialI/Advanced/document/Partial.tex --- a/doc-src/TutorialI/Advanced/document/Partial.tex Fri Sep 28 19:17:01 2001 +0200 +++ b/doc-src/TutorialI/Advanced/document/Partial.tex Fri Sep 28 19:18:46 2001 +0200 @@ -64,7 +64,7 @@ As a simple example we define division on \isa{nat}:% \end{isamarkuptext}% \isacommand{consts}\ divi\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline -\isacommand{recdef}\ divi\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}{\isachardot}\ m{\isacharparenright}{\isachardoublequote}\isanewline +\isacommand{recdef}\ {\isacharparenleft}\isakeyword{permissive}{\isacharparenright}\ divi\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}{\isachardot}\ m{\isacharparenright}{\isachardoublequote}\isanewline \ \ {\isachardoublequote}divi{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ n\ {\isacharequal}\ {\isadigit{0}}\ then\ arbitrary\ else\isanewline \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ if\ m\ {\isacharless}\ n\ then\ {\isadigit{0}}\ else\ divi{\isacharparenleft}m{\isacharminus}n{\isacharcomma}n{\isacharparenright}{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptext}% diff -r 0dbfb578bf75 -r abf9cda4a4d2 doc-src/TutorialI/Advanced/document/WFrec.tex --- a/doc-src/TutorialI/Advanced/document/WFrec.tex Fri Sep 28 19:17:01 2001 +0200 +++ b/doc-src/TutorialI/Advanced/document/WFrec.tex Fri Sep 28 19:18:46 2001 +0200 @@ -65,57 +65,7 @@ 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}\ 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}% +\isacommand{recdef}\ \end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 0dbfb578bf75 -r abf9cda4a4d2 doc-src/TutorialI/Recdef/document/Nested1.tex --- a/doc-src/TutorialI/Recdef/document/Nested1.tex Fri Sep 28 19:17:01 2001 +0200 +++ b/doc-src/TutorialI/Recdef/document/Nested1.tex Fri Sep 28 19:18:46 2001 +0200 @@ -13,31 +13,7 @@ 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}\ 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}% +\isacommand{recdef}\ \end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 0dbfb578bf75 -r abf9cda4a4d2 doc-src/TutorialI/Recdef/document/termination.tex --- a/doc-src/TutorialI/Recdef/document/termination.tex Fri Sep 28 19:17:01 2001 +0200 +++ b/doc-src/TutorialI/Recdef/document/termination.tex Fri Sep 28 19:18:46 2001 +0200 @@ -17,69 +17,7 @@ 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}\ 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}% +\isacommand{recdef}\ \end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root"