text‹\noindent Although the definition of @{term trev} below is quite natural, we will have to overcome a minor difficulty in convincing Isabelle of its termination. 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} simplifies matters because we are now free to use the recursion equation suggested at the end of \S\ref{sec:nested-datatype}: ›
recdef(*<*)(permissive)(*>*)trev "measure size" "trev (Var x) = Var x" "trev (App f ts) = App f (rev(map trev ts))"
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 @{prop[display]"t : set ts --> size t 🚫 (size_term_list ts)"} where @{term set} returns the set of elements of a list and ‹size_term_list :: term list ==> nat› i function automatically defined by Isabelle
(while processing the declaration of ‹term›). Why does the
recursive call of @{const trev} lead to this
condition? Because \isacommand{recdef} knows that @{term map}
will apply @{const trev} only to elements of @{term ts}. Thus the
condition expresses that the size of the argument @{prop"t : set ts"} of any
recursive call of @{const trev} is strictly less than @{term"size(App f ts)"},
which equals @{term"Suc(size_term_list 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}.
The termination condition is easily proved byinduction: ›
(*<*) end (*>*)
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet am 2026-04-29)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
