| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Doc/Tutorial/Recdef/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 1 kB |
|
Quelle Nested1.thySprache: Isabelle |
|||||||||||||||
|
(*<*) theory Nested1 imports Nested0 begin (*>*) text‹\noindent the definition of @{term trev} below is quite natural, we will have overcome a minor difficulty in convincing Isabelle of its termination. is precisely this difficulty that is the \textit{raison d'\^etre} of subsection. @{term trev} by \isacommand{recdef} rather than \isacommand{primrec} matters because we are now free to use the recursion equation 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 that function @{term size} is defined for each \isacommand{datatype}. , the definition does not succeed. Isabelle complains about an termination condition {prop[display]"t : set ts --> size t < Suc (size_term_list ts)"} @{term set} returns the set of elements of a list ‹size_term_list :: term list ==> nat› is an auxiliary automatically defined by Isabelle while processing the declaration of ‹term›). Why does the call of @{const trev} lead to this ? Because \isacommand{recdef} knows that @{term map} apply @{const trev} only to elements of @{term ts}. Thus the expresses that the size of the argument @{prop"t : set ts"} of any call of @{const trev} is strictly less than @{term"size(App f ts)"}, equals @{term"Suc(size_term_list ts)"}. We will now prove the termination cond with our definition. Below we return to the question of how isacommand{recdef} knows about @{term map}. termination condition is easily proved by induction: (*<*) end (*>*)
¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet am 2026-06-10) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-06-09