| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Doc/Tutorial/Recdef/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 858 B |
|
Quelle Nested0.thySprache: Isabelle |
|||||||||||||||
|
(*<*) theory Nested0 imports Main begin (*>*) text‹ \index{datatypes!nested}% In \S\ref{sec:nested-datatype} we defined the datatype of terms › datatype ('a,'b)"term" = Var 'a | App 'b "('a,'b)term list" text‹\noindent and closed with the observation that the associated schema for the definition of primitive recursive functions leads to overly verbose definitions. Moreover, if you have worked exercise~\ref{ex:trev-trev} you will have noticed that you needed to declare essentially the same function as @{term"rev"} and prove many standard properties of list reversal all over again. We will now show you how \isacommand{recdef} can simplify definitions and proofs about nested recursive datatypes. As an example we choose exercise~\ref{ex:trev-trev}: › consts trev :: "('a,'b)term ==> ('a,'b)term" (*<*)end(*>*)
¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet am 2026-04-29) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26