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

# 10. Isabelle Proof General

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

It is important to note that there are actually two different versions of Isabelle Proof General: for "classic" Isabelle and for Isabelle/Isar. An old-style Isabelle theory typically consists of ``.thy'` and correspondent ``.ML'` files, while Isabelle/Isar theories usually have a new-style ``.thy'` only, which has a slightly different syntax and may contain both definitions and proofs.

While Isabelle is able to manage both classic and Isar theories at the same time (the theory loader determines the source format automatically), Proof General does not admit to work on both kinds of Isabelle source files at the same time! Proof General treats `isa` and `isar` as different instances; there is no way to switch modes once Proof General has been started.

The classic version of Isabelle Proof General includes a mode for editing theory files taken from David Aspinall's Isamode interface, see http://proofgeneral.inf.ed.ac.uk/~isamode. Detailed documentation for the theory file mode is included with `Isamode`, there are some notes on the special functions available and customization settings below.

Note that in "classic" Isabelle, ``.thy'` files contain definitions and declarations for a theory, while ``.ML'` contain proof scripts. So most of Proof General's functions only make sense in ``.ML'` files, and there is no toolbar and only a short menu for ``.thy'` files.

In Isabelle/Isar, on the other hand, ``.thy'` files contain proofs as well as definitions for theories, so scripting takes place there and you see the usual toolbar and scripting functions of Proof General.

Most Isabelle users now use Isabelle/Isar because it is more convenient, even if working with tactic-based scripts. For this reason, the default Emacs mode setup of Proof General prefers the `isar` instance over the `isa` instance. To load the "classic" Isabelle mode, you can either make sure to visit a ``.ML'` before a ``.thy'` file, or set the environment variable `PROOFGENERAL_ASSISTANTS=isa` before starting Emacs in order to prevent loading of the Isabelle/Isar mode. Another way of forcing classic Isabelle is to put a special modeline like this:

      (* -*- isa -*- *)

near the top of your Isabelle ``.thy'` files (or at least, the first file you visit). This Emacs feature overrides the default choice of mode based on the file extension.

Isabelle provides yet another way to invoke Proof General via the `Isabelle` script. The standard installation of Isabelle also makes the `isar` version of Proof General its default user interface: running plain `Isabelle` starts an Emacs session with Isabelle/Isar Proof General; giving an option `-I false` refers to the classic version instead. The defaults may be changed by editing the Isabelle settings, see the Isabelle documentation for details.

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

## 10.1 Classic Isabelle

Proof General for classic Isabelle primarily manages ``.ML'` files containing proof scripts. There is a separate mode for editing old-style ``.thy'` files, which supports batch mode only.

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

### 10.1.1 ML files

In Isabelle, ML files are used to hold proof scripts, as well as definitions of tactics, proof procedures, etc. So ML files are the normal domain of Proof General. But there are some things to be wary of.

Proof General does not understand full ML syntax, so ideally you should only use Proof General's scripting commands on ``.ML'` files which contain proof commands (no ML functions, structures, etc).

If you do use files with Proof General which declare functions, structures, etc, you should be okay provided your code doesn't include non top-level semi-colons (which will confuse Proof General's simplistic parser), and provided all value declarations (and other non proof-steps) occur outside proofs. This is because within proofs, Proof General considers every ML command to be a proof step which is undoable.

For example, do this:

       structure S = struct
         val x = 3
         val y = 4
       end;

instead of this:

       structure S = struct
         val x = 3;
         val y = 4;
       end

In the second case, just the first binding in the structure body will be sent to Isabelle and Proof General will wait indefinitely.

And do this:

        val intros1 = REPEAT (resolve_tac [impI,allI] 1);
        Goal "Q(x) --> (ALL x. P(x) --> P(x))";
        br impI 1;
        by intros1;
        ba 1;
        qed "mythm";

instead of this:

        Goal "Q(x) --> (ALL x. P(x) --> P(x))";
        br impI 1;
        val intros1 = REPEAT (resolve_tac [impI,allI] 1);
        by intros1;
        ba 1;
        qed "mythm";

In the last case, when you undo, Proof General wrongly considers the `val` declaration to be a proof step, and it will issue an `undo` to Isabelle to undo it. This leads to a loss of synchronization. To fix things when this happens, simply retract to some point before the `Goal` command and rearrange your script.

Having ML as a top-level, Isabelle even lets you redefine the entire proof command language, which will certainly confuse Proof General. Stick to using the standard functions, tactics, and tacticals and there should be no problems. (In fact, there should be no problems provided you don't use your own "goal" or "qed" forms, which Proof General recognizes. As the example above shows, Proof General makes no attempt to recognize arbitrary tactic applications).

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

### 10.1.2 Theory files

As well as locking ML files, Isabelle Proof General locks theory files when they are loaded. Theory files are always completely locked or completely unlocked, because they are processed atomically.

Proof General tries to load the theory file for a ``.ML'` file automatically before you start scripting. This relies on support especially for Proof General built into Isabelle's theory loader.

However, because scripting cannot begin until the theory is loaded, and it should not begin if an error occurs during loading the theory, Proof General blocks waiting for the theory loader to finish. If you have a theory file which takes a long time to load, you might want to load it directly, from the ``.thy'` buffer. Extra commands are provided in theory mode for this:

The key `C-c C-b` (`isa-process-thy-file`) will cause Isabelle to read the theory file being edited. This causes the file and all its children (both theory and ML files) to be read. Any top-level ML file associated with this theory file is not read, in contrast with the `use_thy` command of Isabelle.

The key `C-c C-u` (`isa-retract-thy-file`) will retract (unlock) the theory file being edited. This unlocks the file and all its children (theory and ML files); no changes occur in Isabelle itself.

Command: isa-process-thy-file

  Process the theory file file. If interactive, use `buffer-file-name`.

Command: isa-retract-thy-file

  Retract the theory file file. If interactive, use `buffer-file-name`.
  To prevent inconsistencies, scripting is deactivated before doing this. So if scripting is active in an ML file which is not completely processed, you will be asked to retract the file or process the remainder of it.

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

### 10.1.3 General commands for Isabelle

This section has some notes on the instantiation of the generic part of Proof General for Isabelle. (The generic part of Proof General applies to all proof assistants supported, and is described in detail in the rest of this manual).

Find theorems. This toolbar/menu command invokes a special version of `thms_containing`. To give several constants, separate their names with commas.

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

### 10.1.4 Specific commands for Isabelle

This section mentions some commands which are added specifically to the Isabelle Proof General instance.

In Isabelle proof script mode, `C-c C-o` (`thy-find-other-file`) finds and switches to the associated theory file, that is, the file with the same base name but extension ``.thy'` swapped for ``.ML'`.

The same function (and key-binding) switches back to an ML file from the theory file.

Command: thy-find-other-file &optional samewindow

  Find associated .ML or .thy file.
  Finds and switch to the associated ML file (when editing a theory file) or theory file (when editing an ML file). If samewindow is non-nil (interactively, with an optional argument) the other file replaces the one in the current window.

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

### 10.1.5 Isabelle customizations

Here are some of the 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.

User Option: thy-use-sml-mode

  If non-nil, invoke `sml-mode` inside "ML" section of theory files.
  This option is left-over from Isamode. Really, it would be more useful if the script editing mode of Proof General itself could be based on `sml-mode`, but at the moment there is no way to do this.

  The default value is `nil`.

User Option: thy-indent-level

  Indentation level for Isabelle theory files. An integer.

  The default value is `2`.

Variable: thy-sections

  Names of theory file sections and their templates.
  Each item in the list is a pair of a section name and a template. A template is either a string to insert or a function. Useful functions are: `thy-insert-header`, `thy-insert-class`, `thy-insert-default-sort`,

        thy-insert-const, thy-insert-rule.
      The nil template does nothing.

  You can add extra sections to theory files by extending this variable.

Variable: thy-template

  Template for theory files.
  Contains a default selection of sections in a traditional order. You can use the following format characters:

  ``%t'` -- replaced by theory name.

  ``%p'` -- replaced by names of parents, separated by ``+'` characters.

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

## 10.2 Isabelle/Isar

Proof General for Isabelle/Isar manages Isar ``.thy'` files, which may contain both definitions and proofs. Proofs may be human readable proof texts as well as traditional tactic scripts adjusted to follow the Isar syntax.

The syntax of Isabelle/Isar 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/Isar process. The caveats of ``.ML'` files discussed for the classic Isabelle version (see section Classic Isabelle) do not apply here.

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

### 10.2.1 General commands for Isabelle/Isar

Find theorems. This toolbar/menu command invokes `thms_containing`. Several term arguments may be given, separated by white space as usual in Isar.

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

### 10.2.2 Specific commands for Isabelle/Isar

The Isabelle/Isar 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 `refute` on the current subgoal. Only available in HOL and derived logics.

`C-c C-a C-q`

  Invokes `quickcheck` on the current subgoal.

`C-c C-a C-d`

  Displays 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/Isar's outer syntax.

`C-c C-a h t`

  Shows theorems stored in the current theory node.

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 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 r`

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

Command termination via ``;`' is an optional feature of Isar syntax. Neither Isabelle/Isar 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 Logics and Settings

The prover specific menu (the same on both Isabelle variants of Proof General) offers a way to select the invoked object logic, and also access to numerous settings of Isabelle.

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`, so you should check that Proof General can find the `isatool` program for it to operate correctly. (Similarly, the documentation menu is partly generated from `isatool doc`).

The logics menu 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).

The prover specific 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.

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

This document was generated by David Aspinall on November, 7 2006 using texi2html 1.76.