--- 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}%
--- 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"
--- 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"
--- 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"