\( \DeclareMathOperator{\tr}{tr} \newcommand\D{\mathrm{d}} \newcommand\E{\mathrm{e}} \newcommand\I{\mathrm{i}} \newcommand\bigOh{\mathcal{O}} \newcommand{\cat}[1]{\mathbf{#1}} \newcommand\curl{\vec{\nabla}\times} \newcommand{\CC}{\mathbb{C}} \newcommand{\NN}{\mathbb{N}} \newcommand{\QQ}{\mathbb{Q}} \newcommand{\RR}{\mathbb{R}} \newcommand{\ZZ}{\mathbb{Z}} % For +---- metric \newcommand{\BDpos}{} \newcommand{\BDneg}{-} \newcommand{\BDposs}{\phantom{-}} \newcommand{\BDnegg}{-} \newcommand{\BDplus}{+} \newcommand{\BDminus}{-} % For -+++ metric \newcommand{\BDpos}{-} \newcommand{\BDposs}{-} \newcommand{\BDneg}{} \newcommand{\BDnegg}{\phantom{-}} \newcommand{\BDplus}{-} \newcommand{\BDminus}{+} \)
UP | HOME

Isabelle

Table of Contents

1. Introduction

Isabelle is a metalogical logical framework (but Isabelle/HOL is a metalogical framework, which is a logical framework that allows us to prove results about deductive systems; this is because HOL is a metalogical framework). Recall, logical frameworks reason within deductive systems. Isabelle is a bit like a tool to create proof assistants, which is why we often see things like Isabelle/X for various choices of X.

2. Earley Parsing

The "object logic" is parsed using an Earley parser, as noted in the section "Parsing and unparsing" of Documentation about Syntax (Chapter 3 of the PDF version of the documentation):

Actual parsing is based on traditional lexical analysis and Earley parsing for arbitrary context-free grammars.

I always wondered if the rumours were true about Isabelle using an Earley parser, now we know.

3. Symbols and Strings

The basic unit of text is a "symbol" (roughly analogous to a "character" in most other languages). A symbol is one of the following:

  1. An ASCII character
  2. A codepoint according to UTF-8
  3. A regular symbol \<ident> for things like Greek letters in a TeX-like format
  4. A control symbol \<^ident> for things like bold, emphasis, etc.

This was introduced in Isabelle98 according to Wenzel's "Isabelle as Document-oriented Proof Assistant" (2011).

The 1998 version can still be accessed on the Older Isabelle Releases page.

See also:

  • Yves Bertot and Laurent Théry,
    "A generic approach to building user interfaces for theorem provers."
    Journal of Symbolic Computation 25, no. 2 (1998) 161–194.

Asynchronous Proof Processing with Isabelle-Scala and Isabelle-jEdit.

4. References

4.1. Early Papers

  • Lawrence Paulson,
    "The Foundation of a Generic Theorem Prover".
    arXiv:cs/9301105, 37 pages.
    • Introduces Isabelle/Pure as a fragment of intuitionistic higher-order logic.
  • Lawrence Paulson,
    "Isabelle: The Next 700 Theorem Provers".
    arXiv:cs/9301106
  • Lawrence Paulson,
    "Natural Deduction as Higher-Order Resolution".
    arXiv:cs/9301104

4.2. Set Theory in Isabelle

  • Florian Rabe and Mihnea Iancu,
    "A Formalized Set-Theoretical Semantics of Isabelle/HOL".
    PDF, 20 pages
  • Bohua Zhan,
    "Formalization of the fundamental group in untyped set theory using auto2".
    arXiv:1707.04757, 17 pages.
    • One of the few formalizations using both untyped set theory and Isabelle

Last Updated: Sat, 26 Oct 2024 13:34:37 -0700