1. The Basics

Abstract

This book is a tutorial on how to use the theorem prover Isabelle/HOL as a specification and verification system. Isabelle is a generic system for implementing logical formalisms, and Isabelle/HOL is the specialization of Isabelle for HOL,which abbreviates Higher-Order Logic. We introduce HOL step by step following the equation HOL = Functional Programming+ Logic.

We do not assume that you are familiar with mathematical logic. However,we do assume that you are used to logical and set theoretic notation,as covered in a good discrete mathematics course [31],and that you are familiar with the basic concepts of functional programming [5],[13],[27],[32] . Although this tutorial initially concentrates on functional programming, do not be misled: HOL can express most mathematical concepts, and functional programming is just one particularly simple and ubiquitous instance.

Isabelle [26] is implemented in ML [17]. This has influenced some of Isabelle/ HOL’s concrete syntax but is otherwise irrelevant for us: this tutorial is based on Isabelle/Isar [33],an extension of Isabelle which hides the implementation language almost completely. Thus the full name of the system should be Isabelle/Isar/HOL, but that is a bit of a mouthful.

There are other implementations of HOL,in particular the one by Mike Gordon et al.,which is usually referred to as “the HOL system” [10]. For us,HOL refers to the logical system, and sometimes its incarnation Isabelle/ HOL.