A rule table buffer displays a formatted table of ML identifiers, typically including rule names, simplifier sets, classical rule sets and tactics. You can use the table for reference purposes, or actively: there are commands to copy the names into the interaction buffer, to build tactics based on the names, or to display the rule.
Isamode comes supplied with basic rule tables for the standard object logics. You can easily extend these to add your favourite rules and tactics, or create new rule tables for your own theories, by writing `.rules' files.
The command to show a rule table is M-x ruletable, normally
bound to the key C-c M-l (which is useful in single frame mode).
Rule table files are searched for in directories in the list
isa-ruletable-paths.
The default value is found using the isatool program; either it
is set from ISAMODE_RULETABLE_PATH, if that variable set, or
it is set to be the single directory ISAMODE_HOME/ruletables.
You should set ISAMODE_RULETABLE_PATH to be a colon-separated
sequence of paths, as usual for Unix path variables.
Just as for object logics, Isamode keeps an internal record of the rule tables available and their file names. If you type C-u M-x ruletable, this internal record will be re-built.
There may be any number of rule table buffers associated with a single Isabelle interaction buffer. When running under a window system, the first 3 (by default) will receive their own windows. The modeline at the bottom of rule table buffer displays both the name of the logic it is associated with, and the name of the theory for which it is a table.
The cursor keys are used to move amongst the rule names, or you can use the mouse to highlight a rule name. Hitting SPC or pressing the left mouse button, button-1, will insert the rule name into the interaction buffer, possibly preceded by a comma. This allows you to quickly construct lists of rules.
The middle mouse button, button-2, can be used to execute a tactic:
by (rtac rule d);
by (dtac rule d);
by (etac rule d);
where d is the designated subgoal (see section 3.1 Proofstate Commands).
Pressing RET or the right mouse button, button-3, displays
the rule in a temporary buffer using prth -- hit q
immediately afterward to remove it. If the name denotes something other
than a rule, it may be displayed correctly if what it denotes can be
guessed from its name, See section 4.3 Rule Categories. Otherwise, you may just
see a type error!
The key TAB toggles the display mode of the table. The display can be in short form, where descriptive headings for rule tables are not displayed and lines are concatenated (this is useful for single frame mode), or long form, where all headings and grouping is shown. TAB also reformats the table, so it is useful if you re-size the Emacs window.
When you write your own theories and logics, you may want to extend or create rule tables. This is very easy to do. Choose a name for your rule table (typically, the name of the theory or logic it documents), and create a text file `name.rules'.
The text file should consist of headings and identifiers. Here's a fragment of `FOL.rules':
Equality refl sym trans subst ssubst Propositions conjI conjunct1 conjunct2 conjE disjI1 disjI2 disjE impI mp impE Quantifiers allI spec allE all_dupE
Headings begin at the start of a line and should not contain whitespace; nothing should follow a heading. Identifiers should be valid ML identifiers, and be separated by tabs or spaces. A line of identifiers begins with some whitespace.
When the rule table file is loaded by Isamode, it is parsed and stored internally; the headings and position of line breaks are recorded. This allows rule tables to be shown in both long and short form: the short form just breaks the line at headings, and concatenates lines of identifiers between headings. More details of the internal format of rule tables are in section 4.4 Rule table internals.
At present there is no mechanism for automatic generation of rule tables. In the future there should be ways of building tables using the theorem database, although it will still be useful to design and edit tables by hand, because of the ability to add headings and comment text in the tables; presently Isabelle's theorem database is too primitive to provide useful meta-comments about theorems.
Rule tables are not limited to containing rule names, they may display
any ML identifier. Rules (ML type thm), tactics (ML type
tactic or int->tactic), rule sets
(simpset,claset) are all candidates. The more
logic-dependent names that are shown in a rule table, the less a user
has to remember or refer to documentation for.
We can also take the opportunity to make use of all these
logic-dependent things. One use is by building appropriate tactics
automatically inside Emacs to apply during proof: typically with
something of type claset one might use fast_tac, or
simp_tac with a simpset, etc. For rules, we'd like to
distinguish between introduction rules (to use resolve_tac) and
elimination rules (to use eresolve_tac), for example.
Isamode does some `automatic tactic building' from the rule table, but it isn't very flexible as yet. Clicking with the middle mouse key on a name in a rule table executes a command which guesses which tactic to apply based on the name. In XEmacs, this default tactic is displayed when you move the pointer over the rule.
Emacs decides what kind of entity something in a rule table is, and then which tactic to apply, by pattern matching on its name. This works most of the time, as many identifiers used in Isabelle follow a regular naming convention.
Here are the categories of identifier that you might want to include in ruletables, together with the patterns used to distinguish them and the default tactics they trigger.
n stands for a digit 0-9, d for a subgoal
number, and rl for some characters in a rule name.
rlI or rlIn
rtac rl d
rlE or rlEn
etac rl d
rlD or rlDn
dtac rl d
rtac rl d
rl_def
rewrite_goals_tac [rl]
rl_rls
resolve_tac rl d
rl_ss
asm_full_simp_tac rl d
rl_cs
fast_tac rl d
rl_tac
rl d
rl
For example, iffD2 will be recognised as a destruction rule,
whereas iffI will be recognised as an introduction rule. A name
such as trans that matches none of the patterns given is assumed
to be an `Arbitrary rule' to be used with resolve_tac. Often
this isn't what you want; the heuristic is maybe correct for about
70% of the identifiers used in the built-in object logics. It's a good
idea to follow the convention for your own logics.
See section Rule table categories for some discussion on future improvements to these features.
This final section is for lisp hackers only, who may wish to manipulate rule tables at the lisp level (for example, to automatically generate them from `.thy' files).
The ruletable data is held in the variable isa-theory-rules. The
functions isa-add-theory-rules and
isa-add-theory-rulegroup may be called to extend the ruletable
variable.
A list of lists, one per theory or logic, like this:
((theory-name rulegroup rulegroup ...)
...
... )
where theory-name is a string. Each rulegroup has the form:
(rulegroup-name . [rule rule ...])
here rulegroup-name is a string that must contain a single word.
Each rule is either a string of a single word, or nil; the
latter represents a further (unnamed) subgrouping of the rules in the
table, and will cause a line-break in the table.
An alternative form for a theory entry is:
(theory-name . rules-filename)
Where rules-filename is a full filename for a `.rules' file which contains the ruletable for theory-name.
isa-theory-rules.
isa-theory-rules.
Go to the first, previous, next, last section, table of contents.