--- 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
+(*>*)