Isabelle/Isar — a Generic Framework for Human-Readable Proof Documents

Abstract

Isabelle/Isar is a generic framework for human-readable formal proof documents, both like and unlike Mizar. The Isar proof language provides general principles that may be instantiated to particular object-logics and applications. The design of Isar has emerged from careful analysis of some inherent virtues of the existing logical framework of Isabelle/Pure, notably composition of higher-order natural deduction rules, which is a generalization of Gentzen’s original calculus. Thus Isar proof texts may be understood as structured compositions of formal entities of the Pure framework, namely propositions, facts, and goals. This paper provides an extensive overview of the combined Pure + Isar framework, including a full object-logic definition as a working example. Hereby we hope to illustrate the present stage of our particular journey from insight into the logical framework, to proofs written in Isabelle/Isar.