Isabelle Light

HOL Light is a modern theorem proving system characterised by its powerful, low level interface that allows for flexibility and programmability. However, considerable effort is required to become accustomed to the system and to reach a point where one can comfortably achieve simple natural deduction proofs.

Isabelle is another powerful and widely used theorem prover that provides useful features for natural deduction proofs, including its meta-logic and its four main natural deduction tactics.

In this project we attempt to emulate some of these features of Isabelle in HOL Light. One of our aims is to decrease the learning curve of HOL Light and make it more accessible and usable by a range of users, while preserving its programmability.

The resulting Isabelle Light library introduces a range of tactics for forwards and backwards application of custom inference rules as well as other quality of life tools inspired from Isabelle, including simplification, case splitting, and assumption matching tactics.

The code is available HERE under the MIT License.

The library has also been released in the main HOL Light repository.