The aim of this thesis is to provide an infrastructure for general recursive function definitions in a proof assistant based on higher-order logic (HOL) that has no native support for recursion or pattern matching. In the first part we develop a tool that automates recursive function definitions and provides appropriate proof rules for them. Compared to previous work, our package supports the definition of partial functions, modeling the domain of the function by an inductive domain predicate. An automatically-generated partial induction rule makes partial correctness proofs independent from termination proofs. This modularity considerably facilitates termination arguments for nested recursions. The second part addresses the problem of automatically solving the termination proof obligations that arise from function definitions. Methods from the literature can be applied, but require significant adaptation to the specific needs of our setting: They must produce full formal proofs and work relative to a rich interactive theory. Our approach encompasses a rule-based selection of measure functions, a simple control-flow analysis inspired by the dependency-pairs approach, and a modified version of the size-change principle based on certificates. A formalization of the full size-change principle is also provided. In the third part we discuss how pattern matching, which occurs frequently in functional programming, can be supported in HOL function definitions. We present a very general form of pattern matching, where arbitrary expressions can serve as patterns. We show how such patterns can be encoded using a custom matching combinator and how their consistency can be expressed in proof obligations. We also study the problem of transforming ML-style sequential pattern matching into minimal sets of independent equations, such that they are consistent in HOL. We relate the problem to the minimization problem for propositional DNF formulas and show that it is $\Sigma_2^P$-complete. We then develop a concrete algorithm that computes minimal patterns. As another application of the new set of tools, we show how user-specified induction schemes can be generated from simpler properties, which often makes their proofs fully automatic.      «

The aim of this thesis is to provide an infrastructure for general recursive function definitions in a proof assistant based on higher-order logic (HOL) that has no native support for recursion or pattern matching. In the first part we develop a tool that automates recursive function definitions and provides appropriate proof rules for them. Compared to previous work, our package supports the definition of partial functions, modeling the domain of the function by an inductive domain predica...     »

Ziel dieser Arbeit ist die Entwicklung einer Infrastruktur für rekursive Funktionsdefinitionen in einem interaktiven Theorembeweiser, in dem Rekursion und Pattern-Matching nicht von Haus aus unterstützt werden. Wir arbeiten im Kontext höherstufiger Logik (higher-order logic, HOL). Im ersten Teil entwickeln wir ein Werkzeug, welches Funktionsdefinitionen automatisiert und geeignete Beweisregeln dafür bereitstellt. Im Gegensatz zu existierenden Ansätzen unterstützt unser Verfahren auch partielle Funktionen, die mit Hilfe eines induktiven Domainprädikats modelliert werden. Eine automatisch generierte Induktionsregel erlaubt partielle Korrektheitsbeweise unabhängig von der Terminierung der Funktion. Diese modulare Struktur erleichtert insbesondere die Behandlung von geschachtelter Rekursion. Der zweite Teil behandelt automatische Terminierungsbeweise, um die aus Funktionsdefinitionen entstehenden Beweisverpflichtungen automatisch zu lösen. Dabei verwenden wir Methoden aus der Literatur, die allerdings an die spezifischen Anforderungen unseres Szenarios angepasst werden müssen. Unser Ansatz beinhaltet eine regelbasierte Auswahl von Maßfunktionen, eine einfache Kontrollflussanalyse ähnlich der Dependency-Pairs-Methode, und eine Variante des Size-Change-Kriteriums mit Zertifikaten. Eine Formalisierung des vollen Size-Change-Kriteriums wird ebenfalls entwickelt. Im dritten Teil untersuchen wir, wie das in der funktionalen Programmierung gebräuchliche Pattern-Matching in HOL unterstützt werden kann. Wir entwickeln eine sehr allgemeine Form von Pattern-Matching in der Logik, welches beliebige Terme als Patterns erlaubt und mit Hilfe eines speziellen Kombinators in der Logik ausgedrückt werden kann. Die Konsistenz der Spezifikation wird durch spezielle Beweisverpflichtungen sichergestellt. Außerdem untersuchen wir das Problem, Spezifikationen mit sequenziellem Pattern-Matching in reine Gleichungsspezifikationen mit möglichst wenigen Glei­chungen umzuwandeln. Wir ziehen eine Parallele zum Problem der Minimierung Boolescher Ausdrücke in DNF und zeigen, dass das Minimierungsproblem für Patterns $S_2^P$-vollständig ist. Wir geben auch einen konkreten Algorithmus zur Minimierung von Patterns an. Als weitere Anwendung der neuen Werkzeuge zeigen wir, wie sich vom Benutzer vorgegebene Induktionsschemata automatisch auf einfachere Beweisziele reduzieren lassen, wodurch sich der Beweis solcher Schemata oft weitgehend automatisieren lässt.      «

Ziel dieser Arbeit ist die Entwicklung einer Infrastruktur für rekursive Funktionsdefinitionen in einem interaktiven Theorembeweiser, in dem Rekursion und Pattern-Matching nicht von Haus aus unterstützt werden. Wir arbeiten im Kontext höherstufiger Logik (higher-order logic, HOL). Im ersten Teil entwickeln wir ein Werkzeug, welches Funktionsdefinitionen automatisiert und geeignete Beweisregeln dafür bereitstellt. Im Gegensatz zu existierenden Ansätzen unterstützt unser Verfahren auch partielle...     »