Skip to content
Snippets Groups Projects
Select Git revision
  • main default
  • scala-2.13
  • github/fork/mario-bucev/more-instantiation
  • github/fork/SolalPirelli/sp/minimizer
  • scala-2.12.13
  • add-blocker-graph-debug
  • add-map-equal-value-keys
  • fix-stainless-1135
  • github/fork/jad-hamza/replaceFromSymbols-positions
  • refactor-parser
  • dotty-compat
  • v1.1.5
  • v1.1.0
  • v1.0.2
  • v1.0.1
  • v1.0
16 results
Blame Permalink
isabelle.rst 9.32 KiB

Isabelle

Isabelle is an interactive theorem prover. It comes with an IDE where users can type mathematical specifications and proofs which will be checked continuously. Specifications consist of a sequence of type and value definitions. All high-level tools inside Isabelle must justify their proofs and constructions against a small inference kernel. This greatly diminishes the risk of unsound proofs.

Additionally, Isabelle features powerful proof automation, for example:

  • classical and equational reasoning
  • decision procedures (e.g. for linear arithmetic)
  • interfaces to automated provers (e.g. Z3 and CVC4)

However, most non-trivial proofs will require the user to give proof hints. In general, interactive provers like Isabelle trade better guarantees for weaker automation.

Normally, users write Isabelle specifications manually. Leon comes with a bridge to Isabelle which allows it to be used as a solver for program verification.

Installation

You can obtain a copy of Isabelle for your operating system at its website, then follow the installation instructions. The installation path needs to be passed to Leon via the --isabelle:base command line option. (The path will end in Isabelle2015. Depending on your operating system, this folder might be some levels into the installation tree.)

On Linux, you can skip this step. Leon is able to download and install Isabelle itself. During the first start, you just need to pass the command line option --isabelle:download=true. You may specify --isabelle:base, but don't have to.

Additionally, you need to instruct Git to fetch all the referenced repositories via git submodule update --init --recursive.

Basic usage

For most purposes, Isabelle behaves like any other solver. When running :ref:`verification`, you can pass isabelle as a solver (see :ref:`cmdlineoptions` for details). Isabelle is a bit slower to start up than the other solvers, so please be patient.

Advanced usage

Isabelle has some peculiarities. To accomodate for those, there are a set of specific annotations in the object leon.annotation.isabelle.

Mapping Leon entities to Isabelle entities

Isabelle -- or it's standard logic HOL, to be precise -- ships with a rather large existing library. By default, the Isabelle backend would just translate all Leon definitions into equivalent Isabelle definitions, which means that existing proofs about them are not applicable. For example, Isabelle/HOL already has a concatenation function for lists and an associativity proof for it. The annotations @typ, @constructor and @function allow the user to declare a mapping to existing Isabelle entities. For lists and their append function, this looks like this: