[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

# 10. Isabelle Proof General

Isabelle Proof General supports major generic features of Proof General, including integration with Isabelle's theory loader for proper automatic multiple file handling. Support for tags and proof-by-pointing is missing.

In this version, support for the old-style “classic” Isabelle theory files has been removed; in Isabelle2007 only Isar style theory files are supported.

Isabelle provides its own way to invoke Proof General via the `Isabelle` script. Running `Isabelle` starts an Emacs session with Isabelle Proof General. The defaults may be changed by editing the Isabelle settings, see the Isabelle documentation for details.

Proof General for Isabelle manages Isar ‘`.thy`’ files. The syntax of Isabelle input is technically simple, enabling Proof General to provide reliable control over incremental execution of the text. Thus it is very hard to let Proof General lose synchronization with the Isabelle process.

[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

## 10.1 Choosing logic and starting isabelle

When you load an Isabelle theory file into Proof General, you may be prompted for the path to the program `isatool` if it is not on the system `PATH` already. This is used to generate further information for invoking Isabelle, in particular, the list of available logics.

The Isabelle menu offers an easy way to select the invoked object logic. If you look at the menu:

            Isabelle -> Logics ->

you should see the list of logics available to Isabelle. This menu is generated from the output of the command `isatool findlogics`. (Similarly, the documentation menu is partly generated from `isatool doc`). Instead of the menu, you can use the keyboard command `isabelle-chose-logic` to choose from the list.

The logics list is refreshed dynamically so you can select any newly built heap images in the same Emacs session. However, notice that the choices are greyed out while Isabelle is actually runnning — you can only switch to a new logic if you first exit Isabelle (similarly to Proof General, Isabelle operates with only one logic at a time).

Another way to set the logic before Isabelle is launched is using an Emacs local variable setting inside a comment at the top of the file, see the documentation of `isabelle-chosen-logic` below.

In case you do not have the `isatool` program available or want to override its behaviour, you may set the variable `isabelle-program-name-override` to define the name of the executable used to start Isabelle. The standard options are and logic name are still appended.

User Option: isabelle-program-name-override

  Name of executable program to run Isabelle.

  You can set customize this in case the automatic settings mechanism (based on isatool) does not work for you. One reason to do this is if you are running Isabelle remotely, or using windows and avoiding isatool.

  A possible value when running under Windows looks like this:

        C:\sml\bin\.run\run.x86-win32.exe @SMLload=C:\Isabelle\

  This expects SML/NJ in C:\sml and Isabelle images in C:Isabelle. The logic image name is tagged onto the end.

  The default value is `nil`.

User Option: isabelle-chosen-logic

  Choice of logic to use with Isabelle.
  If non-nil, added onto the Isabelle command line for invoking Isabelle.

  You can set this as a file local variable, using a special comment at the top of your theory file, like this:

         (* -*- isabelle-chosen-logic: "ZF" -*- *)

  The default value is `nil`.

Command: isabelle-choose-logic logic

  Adjust `isabelle-prog-name` and `proof-prog-name` for running logic.

[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

## 10.2 Isabelle commands

The Isabelle instance of Proof General supplies several specific help key bindings; these functions are offered within the prover help menu as well.

`C-c C-a r`

  Invokes Isar command `refute` on the current subgoal. Only available in HOL and derived logics.

`C-c C-a C-q`

  Invokes Isar command `quickcheck` on the current subgoal.

`C-c C-a C-d`

  Displays a draft document of the current theory.

`C-c C-a C-p`

  Prints a draft document of the current theory.

`C-c C-a h A`

  Shows available antiquotation commands and options.

`C-c C-a h C`

  Shows the current Classical Reasoner context.

`C-c C-a h I`

  Shows the current set of induct/cases rules.

`C-c C-a h S`

  Shows the current Simplifier context.

`C-c C-a h T`

  Shows the current set of transitivity rules (for calculational reasoning).

`C-c C-a h a`

  Shows attributes available in current theory context.

`C-c C-a h b`

  Shows all local term bindings.

`C-c C-a h c`

  Shows all named local contexts (cases).

`C-c C-a h f`

  Shows all local facts.

`C-c C-a h i`

  Shows inner syntax of the current theory context (for types and terms).

`C-c C-a h m`

  Shows proof methods available in current theory context.

`C-c C-a h o`

  Shows all available commands of Isabelle's outer syntax.

`C-c C-a h t`

  Shows theorems stored in the current theory node.

`C-c C-a C-s`

  Invoke sledgehammer on first subgoal.

`C-c C-a C-m`

  Find theorems containing given arguments (prompt in minibuffer). Invokes the `thms_containing` command. Arguments are separated by white space as usual in Isar.

`C-c C-a C-f`

  Find theorems containing (argument in form)

`C-c C-f`

  Find theorems: either of the above.

The following shortcuts insert control sequences into the text, modifying the appearance of individual symbols (single letters, mathematical entities etc.); the X-Symbol package will provide immediate visual feedback.

`C-c C-a b`

  Inserts "\<^bold>"

`C-c C-a C-b`

  Inserts "\<^loc>"

`C-c C-a C-u`

  Inserts "\<^sup>" (superscript character)

`C-c C-a C-l`

  Inserts "\<^sub>" (subscript character)

`C-c C-a u`

  Inserts "\<^bsup> \<^esup>" (superscript string)

`C-c C-a l`

  Inserts "\<^bsub> \<^esub>" (subscript string)

`C-c C-a C-i`

  Inserts "\<^isub>" (identifier subscript letter)

`C-c C-a C-r`

  Inserts "\<^raw:>" (raw LaTeX text)

`C-c C-a C-a`

  Inserts "@{text ""}" (anti-quotation).

`C-c C-a C-x`

  Inserts "ML {* *}" (inline ML code).

Command termination via ``;`' is an optional feature of Isar syntax. Neither Isabelle nor Proof General require semicolons to do their job. The following command allows to get rid of command terminators in existing texts.

Command: isar-strip-terminators

  Remove explicit Isabelle/Isar command terminators ‘`;`’ from the buffer.

[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

## 10.3 Isabelle settings

The Isabelle menu also contains a `Settings` submenu, which allows you to configure things such as the behaviour of Isabelle's term pretty printer (display of types, sorts, etc). Note that you won't see this sub-menu until Isabelle has been started, because it is generated by Isabelle itself. Proof General, on the other hand, is responsible for recording any settings that are configured when you select `Isabelle -> Settings -> Save Settings`. They are stored along with the other Emacs customization settings.

[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

## 10.4 Isabelle customizations

Here are some of the other user options specific to Isabelle. You can set these as usual with the customization mechanism.

Variable: isabelle-web-page

  URL of web page for Isabelle.

[ << ] | [ >> ] |  |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

This document was generated by David Aspinall on July, 24 2008 using texi2html 1.78.