doc-src/TutorialI/Recdef/Nested1.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Recdef/Nested1.thy	Fri Aug 18 11:14:23 2000 +0200
@@ -0,0 +1,42 @@
+(*<*)
+theory Nested1 = Nested0:
+(*>*)
+consts trev  :: "('a,'b)term => ('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
+this subsection.
+
+Defining @{term"trev"} by \isacommand{recdef} rather than \isacommand{primrec}
+simplifies matters because we are now free to use the recursion equation
+suggested at the end of \S\ref{sec:nested-datatype}:
+*}
+ML"Prim.Add_recdef_congs [map_cong]";
+ML"Prim.print_recdef_congs(Context.the_context())";
+
+recdef trev "measure size"
+ "trev (Var x) = Var x"
+ "trev (App f ts) = App f (rev(map trev ts))";
+ML"Prim.congs []";
+congs map_cong;
+thm trev.simps;
+(*<*)ML"Pretty.setmargin 60"(*>*)
+text{*
+FIXME: recdef should complain and generate unprovable termination condition!
+
+The point is that the above termination condition is unprovable because it
+ignores some crucial information: the recursive call of @{term"trev"} will
+not involve arbitrary terms but only those in @{term"ts"}. This is expressed
+by theorem \isa{map\_cong}:
+\begin{quote}
+@{thm[display]"map_cong"}
+\end{quote}
+*}
+
+(*<*)
+end
+(*>*)
+
+