As well as providing facilities for interacting with Isabelle, Isamode
has an in-built mode for editing Isabelle's `.thy' files. This
mode understands the syntax for ML strings (and will insert and correct
backslashes) and allows convenient switching to sml-mode in the
"ML" section of theory files. It provides templates to help remind you
of the syntax for theory files.
auto-mode-alist.
The theory mode understands the sections in theory files and provides
several commands to use them. C-c C-n
(isa-thy-goto-next-section) moves to the next section, C-c
C-p (isa-thy-goto-previous-section) moves to the previous
section. You can also use CTRL with the up and down arrow keys
for this.
C-c C-t (isa-thy-insert-template) provides a template for
the file or current section. This is useful if you can't remember the
syntax for theory files; you will be asked for text. The templates do
not cover all the possible variations for theory files and should be
considered merely as prompts for each section: you are advised to read
the Isabelle Reference Manual to understand the full situation.
C-c C-u (isa-thy-use-buffer) sends the buffer to an
Isabelle process with use_thy (remember that this may trigger the
Isabelle theory reading mechanism to load other files). This is the
same key that is used by sml-mode.
The interaction buffer chosen (or created) by C-c C-u is determined by parsing the file. For reliable results, you should include a special comment towards the start of the file, which has the form:
Logic Image: logic-name
Then the use functions will send text to the buffer that would be selected by M-x isabelle RET logic-name RET.
The TAB key indents the current line. Indentation includes the automatic insertion of backslashes in strings that span more than one line. This is handy because axioms are ML strings which are often long, and it is tedious to have to remember to put backslashes in the correct places (see the discussion in section 2.4 Backslashes).
The key RET is by default bound to newline-and-indent so
that backslashes are inserted automatically when you type RET at
the end of a line containing an open string. See section 6.4 Theory mode User Options for details of how to control the backslashing and indentation
behaviour.
C-k is bound to isa-thy-kill-line which behaves in the same
way as the usual kill-line, except there is some attempt to
interpret continuation backslashes inside strings. For example,
C-k in the middle of a line which is continued will only delete up
to the terminating backslash, not the end of line; C-k anywhere
after the final non-whitespace character on the line will delete
continuation backslashes when joining lines.
If you find the automatic treatment of backslashes distracting and would rather deal with them manually, you can revert to the usual key bindings by putting this code in your `.emacs':
(add-hook 'isa-thy-mode-hook
(function (lambda ()
(define-key isa-thy-mode-map "\C-k"
'kill-line)
(define-key isa-thy-mode-map "\C-m"
'newline))))
If isa-thy-use-sml-mode is non-nil, C-c C-c invokes
sml-mode as a minor mode in the ML section. This is done
automatically by TAB.
C-c C-o finds and switches to the associated ML file, that is, the file with the same base name but extension `.ML' in place of `.thy'.
use_thy. The choice
of Isabelle interaction buffer can be influenced with a special `Logic Image:'
comment.
Theory files may have associated ML files, typically containing proofs
of some basic consequences of a theory's axioms. Further ML files may
be used with Isabelle, containing big proofs, proof procedures, and so
on. Isamode is intended to be used in conjunction with the Emacs mode
for editing ML files, which is called sml-mode.
If you visit a theory file before an ML file, sml-mode will be
customized to work with Isamode.
You can use C-c C-o (isa-thy-find-other-file) to visit the
theory file corresponding to an ML file -- the opposite operation to
C-c C-o in theory mode.
Uses of C-c C-u (isa-thy-use-buffer), C-c C-r
(isa-thy-use-region), C-c C-l (isa-thy-use-line)
will send the buffer, region or line to an Isabelle interaction buffer.
The first two of these keys normally send text to an ML process buffer.
The logic chosen can be directed in the same way as for theory files,
i.e., with a Logic Image: comment towards the start of the file
see section 6.1 Editing theory files.
isa-thy-use-line is intended for copying lines of interactive
proofs, to replay them. A line is understood to be the text starting on
current line and extending to the next semi-colon (thus it may span more
than one buffer line). Semi-colons inside strings and comments are
ignored.
use. The choice of
Isabelle interaction buffer can be influenced with a special `Logic Image:'
comment.
use. The choice of Isabelle interaction buffer can be
influenced with a special `Logic Image:' comment.
Isabelle has two forms of proof script which may be kept in ML files.
These are interactive proofs, which begin with goal, and
batch proofs, which begin with prove_goal. Interactive
proofs update the proof state at each step, when a tactic is applied
using `by'. Batch proofs involve no state; they execute in a single
step without output and can be stored in ML structures. Batch proofs
might be considered as a `final' form for debugged proofs; lemmas in
many of the distributed object logics are proved with batch proofs.
Isamode has functions to help you convert between interactive and batch
proofs. isa-batchify creates a batch proof from an interactive
one and isa-unbatchify goes the other way. The original versions
of these functions were supplied in an emacs file distributed with Isabelle
called `goalify.el', which is superseded by Isamode.
Here is an example of an interactive proof:
val prems = goal FOL.thy "P & Q --> P";
by (resolve_tac [impI] 1);
by (eresolve_tac [conjE] 1);
by (assume_tac 1);
qed "easy_theorem";
and here is a corresponding batch proof:
qed_goal "easy_theorem" FOL.thy "P & Q --> P"
(fn prems =>
[
(rtac impI 1),
(etac conjE 1),
(assume_tac 1)
]);
I created the batch proof above by typing in the interactive proof line
by line into a *FOL* buffer, cutting the text from the
*FOL-listener* and then using isa-batchify on the region.
To do this, you must set the mark at the start of the proof with
C-SPC, and move to the end (after result), before using
M-x isa-batchify.
Notice that the tactics involving single rules were replaced with short forms. The command M-x isa-expandshorts can be used to do this without converting the form of a proof.
Using M-x isa-unbatchify on the above region converts back into an interactive proof:
val prems = goal FOL.thy "P & Q --> P"; by (rtac impI 1); by (etac conjE 1); by (assume_tac 1); val easy_theorem = result();
If you write batch proofs in ML files, it may be wise to write them in a regular form such as the above, so that it is possible to convert them back into interactive proofs in the future if you need to (for example, to adapt them to different theorems).
ba,br,...) are expanded and
long-forms with singleton arguments (resolve_tac [rule])
are contracted (to rtac rule).
I hope future versions of these functions will be easier to use (without needing to set a region to use them) and more reliable -- at present they are a bit fussy about the format of the proofs, which should be pretty much as shown above.
Here are some options you may use to control the layout of theory files and behaviour when editing theory files.
You may wish to disable indenting inside strings if your logic uses any of the usual bracket characters in unusual ways.
The default value is nil.
Theory files can be automatically highlighted using font-lock,
which is integrated with XEmacs. If you have font-locking enabled by
default (via the menu Options->Syntax Highlighting), theory files should
be automatically syntax-highlighted with section heading, string and
comment highlighting when you load and edit them.
If you wish, the highlighting can be configured by adjusting the
variable isa-thy-mode-font-lock-keywords.
isa-thy-mode.isa-thy-headings-regexp.
This as a value for font-lock-keywords, see the documentation
of that variable for more details.
matcher (matcher . match) (matcher . facename) (matcher . highlight) (matcher highlight ...) (eval . form)
where highlight should be either match-highlight or match-anchored.
form is an expression, whose value should be a keyword element, evaluated when the keyword is (first) used in a buffer. This feature can be used to provide a keyword that can only be generated when Font Lock mode is actually turned on.
For highlighting single items, typically only match-highlight is required. However, if an item or (typically) items is to be highlighted following the instance of another item (the anchor) then match-anchored may be required.
match-highlight should be of the form:
(match facename override laxmatch)
Where matcher can be either the regexp to search for, a variable containing the regexp to search for, or the function to call to make the search (called with one argument, the limit of the search). match is the subexpression of matcher to be highlighted. facename is either a symbol naming a face, or an expression whose value is the face name to use. If you want facename to be a symbol that evaluates to a face, use a form like "(progn sym)".
override and laxmatch are flags. If override is t, existing fontification may be overwritten. If `keep', only parts not already fontified are highlighted. If `prepend' or `append', existing fontification is merged with the new, in which the new or existing fontification, respectively, takes precedence. If laxmatch is non-nil, no error is signalled if there is no match in matcher.
For example, an element of the form highlights (if not already highlighted):
"\\<foo\\>" Discrete occurrences of "foo" in the value of the variable `font-lock-keyword-face'. ("fu\\(bar\\)" . 1) Substring "bar" within all occurrences of "fubar" in the value of `font-lock-keyword-face'. ("fubar" . fubar-face) Occurrences of "fubar" in the value of `fubar-face'. ("foo\\|bar" 0 foo-bar-face t) Occurrences of either "foo" or "bar" in the value of `foo-bar-face', even if already highlighted.
match-anchored should be of the form:
(matcher pre-match-form post-match-form match-highlight ...)
Where matcher is as for match-highlight with one exception; see below. pre-match-form and post-match-form are evaluated before the first, and after the last, instance MATCH-ANCHORED's matcher is used. Therefore they can be used to initialise before, and cleanup after, matcher is used. Typically, pre-match-form is used to move to some position relative to the original matcher, before starting with MATCH-ANCHORED's matcher. post-match-form might be used to move, before resuming with MATCH-ANCHORED's parent's matcher.
For example, an element of the form highlights (if not already highlighted):
("\\<anchor\\>" (0 anchor-face) ("\\<item\\>" nil nil (0 item-face)))
Discrete occurrences of "anchor" in the value of `anchor-face', and subsequent
discrete occurrences of "item" (on the same line) in the value of `item-face'.
(Here pre-match-form and post-match-form are nil. Therefore "item" is
initially searched for starting from the end of the match of "anchor", and
searching for subsequent instance of "anchor" resumes from where searching
for "item" concluded.)
The above-mentioned exception is as follows. The limit of the matcher search defaults to the end of the line after pre-match-form is evaluated. However, if pre-match-form returns a position greater than the position after pre-match-form is evaluated, that position is used as the limit of the search. It is generally a bad idea to return a position greater than the end of the line, i.e., cause the matcher search to span lines.
Note that the match-anchored feature is experimental; in the future, we may replace it with other ways of providing this functionality.
These regular expressions should not match text which spans lines. While
M-x font-lock-fontify-buffer handles multi-line patterns correctly, updating
when you edit the buffer does not, since it considers text one line at a time.
Be very careful composing regexps for this list; the wrong pattern can dramatically slow things down!
Go to the first, previous, next, last section, table of contents.