2. Interacting with Isabelle

Using Isabelle with Isamode, you interact in a shell-like buffer based on the Emacs command-interpreter package, comint. The same package lies behind the shell mode in Emacs. The comint package has many useful features. For example, there is a command history ring, accessed with the keys M-p (comint-previous-input) and M-n (comint-next-input). Another feature is context-sensitive completion, used in Isamode for filenames and ML identifiers.

You can find out more about comint by reading the documentation in the file `comint.el' or, as usual, using C-h m (describe-mode) to show the keys and commands available. Many of the commands are also available on pull-down menus.

The main command to start Isabelle is M-x isabelle.

Command: isabelle

Prompt for a logic name, and then create or switch to an Isabelle process for the chosen logic. The isabelle session takes place in an interaction buffer, named *logic*.

See below for more details about how to select a logic.

M-x isabelle behaves as other similar Emacs commands: if there is already a buffer *logic*, then isabelle logic will switch to that buffer (and its associated buffers). But it is perfectly possible to have more than one Isabelle session with the same logic -- you simply rename the first buffer.

2.1 Choosing which Logic

If you type M-x isabelle you are prompted for a logic name; you may hit SPC for a list of possibilities. Alternatively, selecting `Session' from the Isabelle menu will also display a sub-menu of logic names. The list shown will contain all the object logics found when Isamode was started. Object logics are searched for using the Isabelle tool isatool findlogics.

If you want to use a newly built logic which isn't in the completion list, typing C-u M-x isabelle will run the command isatool findlogics again to update the internal record of object logics available. (Note: this doesn't rebuild the menu at present).

The command M-x isabelle calls the internal function isabelle-session, which may be useful if you wish to write special start-up scripts for Emacs to fire-up Isabelle, or define keys to switch to a particular logic session.

Internal Function: isabelle-session logic

Create or switch to an Isabelle process in an interaction buffer with the base logic logic. The buffer is named *logic*.

2.2 Startup Sequence

Variable: isa-session-prelude

If non-nil, an ML string to issue at the start of every Isabelle session.
Handy for setting options inside Isabelle (for example, the load path for logics), or for loading a personal startup file that does such configuration.

The default value is set via the Isabelle settings environment, to be the value of the environment variable ISAMODE_prelude. An example setting is:

   ISAMODE_PRELUDE='use "/home/da/isabelle/startup.ML";'

which attempts to read in a file `startup.ML' from my Isabelle directory. You might set this variable in the private settings file `$ISABELLE_HOME_user/etc/settings'.

note: the string is sent silently; make sure it is properly terminated and doesn't lead to errors - you won't see the results of executing it!

2.3 Completion

Command: comint-dynamic-complete

The primary completion command in the Isabelle interaction buffer, usually bound to TAB. If the point is inside an ML string, completion will assume you are asking for a filename, otherwise that you are completing some ML identifier.

Constant: isa-completion-list

This constant contains the table used for ML identifier completion. Completion is provided for identifiers denoting tactics, tacticals and proof commands. See the file `isa-rules.el'.

Completion is not implemented for rule names because typically they are short, and may be displayed in a rule table anyway (see section 4. Rule tables).

2.4 Backslashes

Isabelle uses ML strings to represent types and terms of the meta-logic. Terms and types can be very long strings which are easier to read, type and edit if they span several lines. ML strings which span lines must contain the escape sequence `\ \' to indicate to the ML parser that the carriage return is not part of the string and that the string will be continued on the next line.

When you are inputting such strings it is annoying to need to remember to include these backslashes. So Isamode makes the job easy for you by doing it automatically, both in interaction buffers, and inside `.thy' files (see section 6.1 Editing theory files).

If you type RET at the end of a line which contains an unclosed string, Isamode will insert a backslash (if you haven't done already) before sending it to the ML process. Another backslash will be inserted on the following line.

If you don't like this behaviour, you can disable it by customizing isa-auto-backslashes.

Variable: isa-auto-backslashes

If non-nil, Isamode will attempt to automatically add backslashes for long strings. See function isa-send-input in `isa-mode.el'.

2.5 Menus

Isamode provides a main menu, called `Isabelle', which appears by default in Isabelle interaction buffers and theory file buffers. After loading Isamode, it will also appear in ML buffers, if you use sml-mode (see section 6.2 Editing ML files). To add the main menu to the menubar of the current buffer in other cases, there is a command, M-x isa-menus.

Command: isa-menus

Add main `Isabelle' menu to current menubar.

The main menu has options for starting Isabelle sessions, displaying documentation, or engaging various editing functions (see section 6. Theory and ML files). In addition to the `Isabelle' menu, there are four menus provided for interaction mode.

`Option'

allows you to activate or switch to buffers associated with this one, or adjust various Isabelle parameters. There is a quit option here.

`Goal'

`Prover'

`Tactic'

are menus providing short-cuts for typing frequently used Isabelle commands. Each item in these menus inserts text into the Isabelle buffer. Most have key bindings too, so you can save many keystrokes.

The convention for the Isabelle command key sequences is:

C-c C-t key

for tactics...

C-c C-r key

for rewriting tactics...

C-c C-p key

for prover tactics...

C-c C-s key

for goal commands... (remember goal `s'tack or `s'tart proof)

The commands are shown in full in section 2.6 Interaction mode menu operations.

2.6 Interaction mode menu operations

Here's a list of the Isamode interaction buffer commands in the `Goal', `Prover' and `Tactic' menus. We show the text they insert, and the keystrokes bound to the commands by default. In the table, d stands for the designated subgoal (see section 3.1 Proofstate Commands -- don't forget C-up and C-down). rules, thmname, etc, stand for some data that must be typed to complete the command. If there is no data needed, the text may be sent immediately to Isabelle; otherwise you should type something followed by RET.

2.6.1 Primary Tactics

isa-resolve_tac

by (resolve_tac [rules] d);
key: C-c C-t C-r

isa-resolve_tac-prems

by (resolve_tac prems d);
key: C-c C-t C-p

isa-assume_tac

by (assume_tac d);
key: C-c C-t C-a

isa-eresolve_tac

by (eresolve_tac [rules] d);
key: C-c C-t C-e

isa-dresolve_tac

by (dresolve_tac [rules] d);
key: C-c C-t C-d

isa-forward_tac

by (forward_tac [rules] d);
key: C-c C-t C-f

isa-match_tac

by (match_tac [rules] d);
key: C-c C-t r

isa-match_tac-prems

by (match_tac prems d);
key: C-c C-t p

isa-eq_assume_tac

by (eq_assume_tac [rules] d);
key: C-c C-t a

isa-ematch_tac

by (ematch_tac [rules] d);
key: C-c C-t e

isa-dmatch_tac

by (dmatch_tac [rules] d);
key: C-c C-t d

2.6.2 Rewriting Tactics

isa-rewrite_goals_tac

by (rewrite_goals_tac [rules]);
key: C-c C-r g

isa-rewrite_tac

by (rewrite_tac [rules]);
key: C-c C-r w

isa-fold_goals_tac

by (fold_goals_tac [rules]);
key: C-c C-r f

isa-cut_facts_tac

by (cut_facts_tac [rules] d);
key: C-c C-r c

isa-cut_facts_tac-prems

by (cut_facts_tac prems d);
key: C-c C-r p

2.6.3 Prover Tactics

isa-simp_tac

by (simp_tac simpset_ss d);
key: C-c C-p C-s

isa-asm_simp_tac

by (asm_simp_tac simpset_ss d);
key: C-c C-p C-a

isa-asm_full_simp_tac

by (asm_full_simp_tac simpset_ss d);
key: C-c C-p C-f

isa-fast_tac

by (fast_tac claset_cs d);
key: C-c C-p f

isa-best_tac

by (best_tac claset_cs d);
key: C-c C-p b

isa-step_tac

by (step_tac claset_cs d);
key: C-c C-p s

isa-contr_tac

by (contr_tac d);

isa-mp_tac

by (mp_tac d);

isa-eq_mp_tac

by (eq_mp_tac d);

2.6.4 Goal Commands

isa-undo

undo();
key: C-c C-s u

isa-back

back();
key: C-c C-s b

isa-chop

chop();
key: C-c C-s c

isa-choplev

choplev lev;
(unbound)

isa-goal-thy

val prems = goal thy "goal";
key: C-c C-s g

isa-goalw-thy

val prems = goalw thy rewrites "goal";
key: C-c C-s w

isa-result

val thmname = result();
key: C-c C-s r

isa-push-proof

push_proof();
key: C-c C-s p

isa-pop-proof

val prems = pop_proof();
key: C-c C-s o

isa-rotate-proofs

val prems = rotate_proof();
key: C-c C-s n

Go to the first, previous, next, last section, table of contents.