Clemens Ballarin

Gerwin Klein

Overview:
This one-day tutorial gives an overview of the proof assistant Isabelle and its use. The tutorial aims at researchers in computer science and mathematics who want to use Isabelle for a particular formalisation task, or who want to get an overview of current proof assistant technology. The following themes are covered: introduction to natural deduction, specification tools, automated proof tools, readable proofs, Isabelle's module system, applications from verification and mathematical algebra. The tutorial was presented at IJCAR-2004 in Cork, Ireland.

The tutorial comprises four lectures, each followd by sessions where participants work with Isabelle. Isabelle supports various logics including Higher-Order Logic (HOL) and Zermelo-Fraenkel Set Theory (ZF). The tutorial is based on HOL, but most of the presented material also applies to ZF.

• Session I: Basics
  A brief introduction to Isabelle's basic calculus of natural deduction is followed by Isabelle's general automation for classical proofs and term rewriting. This session also covers essential technicalities needed to get started with Isabelle.
• Session II: Specification Tools & Readable Proofs
  Strong proof tools do not automatically make a proof assistant an effective tool for specification and verification. What is needed is support for routine specification tasks. Isabelle supports datatypes, general recursive functions and inductive definitions. An other important issue is readability of proofs. Since a specification of a device or the formalisation of a mathematical entity typically evolves over time, proofs change and proof scripts must be maintainable. Isabelle supports this through the ISAR proof format.
• Session III: More Readable Proofs & Modules
  The more advanced concepts of ISAR include calculational reasoning chains and derived operators that make writing proofs more convenient. Another tool for managing maintenance complexity and readability is the module system. Unlike other provers where modules are centered around theories, Isabelle's modules (called locales) are based on contexts. These can be seen as light-weight theories and, since they are key to ISAR, they can be interpreted not only at the level of theories, but within proofs, providing much finer granularity. Besides interpretation, locales provide operations for rename and merge.
• Session IV: Applications
  We present two medium sized applications of readable proofs in Isabelle from the areas of verification (a small expression compiler) and mathematical algebra (universal property of polynomial rings).

Target audience:
Doctoral students and researchers in computer science or mathematics who want to use Isabelle for a particular formalisation task, or who want to get an overview of the capabilities of a state-of-the-art proof assistant. Standard mathematical knowledge but no previous experience with formal methods is required.