| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Doc/Tutorial/document/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 1 kB |
|
Quelle inductive0.tex Sprache: Latech |
|||||||||
|
\chapter{Inductively Defined Sets} \label{chap:inductive}
\index{inductive definitions|(} This chapter is dedicated to the most important definition principle after recursive functions and datatypes: inductively defined sets. We start with a simple example: the set of even numbers. A slightly more complicated example, the reflexive transitive closure, is the subject of {\S}\ref{sec:rtc}. In particular, some standard induction heuristics are discussed. Advanced forms of inductive definitions are discussed in {\S}\ref{sec:adv-ind-def}. To demonstrate the versatility of inductive definitions, the chapter closes with a case study from the realm of context-free grammars. The first two sections are required reading for anybody interested in mathematical modelling. \begin{warn} Predicates can also be defined inductively. See {\S}\ref{sec:ind-predicates}. \end{warn} \input{Even} \input{Mutual} \input{Star} \section{Advanced Inductive Definitions} \label{sec:adv-ind-def} \input{Advanced} \input{AB} \index{inductive definitions|)} ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28