| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Doc/Tutorial/Recdef/ (Isabelle Prover 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}% \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 closed with the observation that the associated schema for the definition primitive recursive functions leads to overly verbose definitions. Moreover, you have worked exercise~\ref{ex:trev-trev} you will have noticed that needed to declare essentially the same function as @{term"rev"} prove many standard properties of list reversal all over again. will now show you how \isacommand{recdef} can simplify and proofs about nested recursive datatypes. As an example we exercise~\ref{ex:trev-trev}: › consts trev :: "('a,'b)term → ('a,'b)term" (*<*)end(*>*)
¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet am 2026-06-29) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-07-09