Interactive Proof: Introduction to Isabelle/HOL

摘要

This paper introduces interactive theorem proving with the Isabelle/HOL system [3]. The following topics are covered: 1. Verified functional programming: The logic HOL contains an ML-style functional programming language. It is shown how to verify functional programs in this language by induction and simplification. 2. Predicate logic: Formulas of predicate logic and set theory are introduced, together with methods for proof automation. 3. Inductively defined predicates. 4. Structured proofs: We introduce the proof language Isar and show how to write structured proofs that are readable by both the machine and the human. We assume basic familiarity with some functional programming language of the ML or Haskell family, in particular with recursive data types and pattern matching. No specific background in logic is necessary beyond the ability to read predicate logic formulas.