Here we give an account of how you may conduct a
Jape session with the small theory of functions and lists
supplied with the distribution.
Find out where Jape has been installed on your system (we'll call the place
`$JAPEHOME` in what follows). Start Jape in the usual way by
giving the shell command

$JAPEHOME/bin/jape $JAPEHOME/EXAMPLES/functions.jt(or some suitable euphemism for it) in an X terminal window.

After a short time Jape will start to give an account of what it's doing to the terminal window -- look for something along the following lines

Jape: release 3.0b [$JAPEHOME/bin/japeserver] [OPENING "$JAPEHOME/EXAMPLES/functions.jt"] [OPENING "$JAPEHOME/EXAMPLES/equality_rules.j"] [CLOSING "$JAPEHOME/EXAMPLES/equality_rules.j"] [OPENING "$JAPEHOME/EXAMPLES/equality_menus.j"] [CLOSING "$JAPEHOME/EXAMPLES/equality_menus.j"] [OPENING "$JAPEHOME/EXAMPLES/functions_rules.j"] [CLOSING "$JAPEHOME/EXAMPLES/functions_rules.j"] [OPENING "$JAPEHOME/EXAMPLES/functions_menus.j"] [CLOSING "$JAPEHOME/EXAMPLES/functions_menus.j"] [CLOSING "$JAPEHOME/EXAMPLES/functions.jt"] Jape Interface Server $JAPEHOME/bin/japeserver [$JAPEHOME/bin/japeserver.ob] [Looked for an option file named /users/sufrin/Jape.options] [Looked for an option file named ./Jape.options]Once it has gotten this far, Jape will place a gaggle of windows on your screen, in roughly the following order:

**The Session window:****The Definitions Panel:****The Conjectures Panel:**-
**The Provisos window:**

The first thing to do is to place these top-level windows in
convenient places on your display. The Session window is the one
which is going to require most of your attention. Most of your
mouse clicks will be directed at the Definitions and Conjectures
panels and the Rules menus from the Session window.
(Incidentally, you can use the
commands on the **File** menu to save yourself the
trouble of rearranging windows whenever you're going to work
again with a theory.)

Move to the Conjectures panel, and select (by clicking on it) a conjecture to prove: the conjecture will be displayed with foreground and background colours reversed.

Once we've selected it, we press that panel's **Prove**
button: this tells Jape that we want to prove the selected
conjecture, whereupon the Session window changes to look like
this:

The box around the line labelled `1:` indicates that our
current goal is to prove this conjecture; the ellipsis (`...`)
just above it is intended to indicate that
we have to fill in the rest of the proof. In fact
the conjecture relates
the functions `zip`, `map`, and
-- which are defined in a theory
of *cat*-lists by the laws

In the absence of any special information relating
these functions, the first step we shall take is
to use the * extensionality *rule. We would normally do so
by selecting it from the Rules menu in the Session
window. But since it's likely that we will be using
that menu several times we shall tear it off
the menu bar. We do so by clicking on the dotted-line
entry at the top of the
menu which pops up when we press on the
Rules menu button. Shortly after we click on the
dotted-line, a new window appears, leaving the
session looking something like
this

The new window is the Rules menu, and it can be moved around the screen using your X window manager's usual facilities for doing such things. It's a good idea to do that now, because we don't want to obscure our view of the session.

Clicking on the fifth entry on the rules menu invokes the simple extensionality rule, and leaves the proof record looking like this:

We're now going to use the fact that the theory designer has
kindly provided a button which will repeatedly unfold
subexpressions in the goal which match the left-hand-sides
of certain definitions and theorems. We press the **Unfold ***
button on the Conjectures panel, and a few moments later the proof
record changes to:

What's happened is that the definitions of composition
and
have been used to rewrite appropriate
subexpressions in our goal. The reason lines
2, 3, and 4 are ``greyed out'' is that
they may not themselves be used in
the proof of the currently-selected goal,
which is labelled `1:`. If you
deselect the goal (by clicking
outside the region of the proof record), then
the proof record is coloured uniformly:

Next we'll be using list induction on `x`.
So we text-select (by dragging
with the middle button) all instances of `x`,

If we click on the formula on line 4 of the proof, then all formulae except for the hypotheses which may be used during the proof of that formula) will be greyed-out. Conversely, if we click on one of the hypotheses on line 3, all formulae save those at which the hypothesis is in scope will be greyed out. Try this yourself.

Now let's make a mistake. Select
line 4, and one of the hpotheses on line 3
by clicking on them. Now invoke ** BoolCases** from the Rule menu.
An error notification pops up, looking something like
this:

You can dismiss it by clicking on the
--
indeed you * must * dismiss it before you you can do anything
else at all in Jape.

Now deselect everything (by clicking anywhere outside the proof
record). Double click on line 1 -- this uses the definition
of `map` to rewrite the right hand side of the equation
to the empty list.
Now double click again on (the new) line 1, and notice that
the leftmost `map` term on the left hand side has
also been reduced to the empty list.

The designer of the theory of functions and lists
decided to bind the double
click gesture to a Jape tactic which searches
the current goal formula for a subterm which matches
the left hand side of one of the laws accessible
from the *search list*. The *search list*
is controlled by the menu labelled ** Searching **,
which is shown below:

The rules (and conjectures) defined in this theory are grouped by subject. A group's laws are made part of the search list by pressing the appropriate ``enable'' button; they are withdrawn from the search list by pressing the appropriate ``disable'' button. Hypotheses currently in scope are treated as a group for the purposes of this facility.

We're now impatient to finish the proof, so we
invoke **Unfold *** three times -- wating,
after each invocation, for the proof record to
show what progress has been made. After the third
invocation, the proof record looks something like this:

We now need to prove that the lengths of the two
lists `map F xs` and `map G xs`
are the same. We recall that there's a conjecture
relating * length* and *map*

So we try to transform this goal into that form. We do so
by selecting the composition symbol (*o*) on the
Definitions panel, and pressing the **Fold**
button on that panel twice. The interesting part of the proof
is now

We can't be bothered proving the conjecture, so we move
to the Edit menu and enable the application of
Conjectures by pressing **Apply both conjectures and theorems**.

Next we select

in the Conjectures panel, and press the **Unfold**
button twice. This not only completes the proof
of the antecedent of the third rule of the
definition of `zip`, it conceals the detail
of this sub-proof from us.

If we wish to, we can reveal the detail by double clicking on
the explanation of the line numbered 14, or by selecting
the equation on that line and invoking the ** Expand/Contract detail **
command on the Edit menu.

There's not much more to do now, and ** Unfold * **
can do it all for us. Try it yourself, and see what happens.

When the proof you are conducting is
finished, you may invoke the ** Done **
command on the Edit menu to record it as the ``definitive''
proof of its root sequent. The ** Done **
command is greyed out unless the proof really is complete.

In every Jape window there is an ``information please'' button, which looks something like this

You can start a new proof of any conjecture (including one
you're in the middle of proving, or one you've already proved)
at any stage. Just go to a Conjectures panel, select the conjecture,
and press the **Prove** button on that panel. If there's
a proof already active, then that is suspended, and the
new conjecture is placed in the session window. The
** Proof Selection ** window
allows you to switch between the proofs
which are currently in progress. When there's a single proof
in progress it will look something like this:

when more than one proof is in progress, it will look something like
the picture below. You can switch between proofs by pressing
the appropriate button, and you can abandon a proof
by switching to it, then pressing the **Close**
button.

The edit menu (shown below) provides several commands which are commonly used for navigation within a proof.

Documentation for most of these commands can be obtained by clicking on the Edit menu button while holding down a modifier key (Control, Shift, or Meta).

The designer of the theory of functions and lists chose to add some non-standard mode buttons to the Edit menu. These are:**Box/Tree Display Style**- these buttons switch between the box style of proof presentation, and the proof tree style. You can switch between these styles whenever you wish. The tree style takes much more real estate.
**Automatic/Manual Goal Selection**- The user can switch between open goals in a proof at any stage. When automatic goal selection is enabled, Jape suggests a new goal whenever a proof move is made; when manual goal selection is enabled, Jape doesn't presume -- it leaves goal selection to the user.
**Apply (both conjectures and theorems / only theorems)**-
Unproved conjectures may not normally be used in the proof
of a conjecture. But when Jape is in the
mode established by pressing
**Apply both conjectures and theorems**it relaxes this restriction, and permits unproven conjectures to be used.

At any stage in the evolution of
a proof you can capture the record
by invoking the ** Output printable proof**
entry on the File menu. This pops up
a window which looks something like this

You are being invited to choose the name for a file in which to save a printable version of the Jape proof record which is currently visible in the session. If it's not obvious to you what to do next, then you can always press the button. This results in a scrollable information box appearing, which tells you what you'll need to know.

If you have several proof states to record, then you keep this
file selection window alive (don't press cancel). Every time you
press the **OK** button on it, the currently
visible proof record is saved in the file whose
name is in the **File:** entry box.

A `.pjp` file isn't directly printable but it
can be used to generate Latex source text for inclusion
in a Latex document. The program which performs
this magic is `$JAPEHOME/bin/jape2tex` --
its source (in Standard ML) is also available in
the directory `$JAPEHOME/Jape2Tex`
if you wish to generate different forms of output.

You can change the font sizes in which
proofs (and Panel entries) are rendered by using
the Sizes control panel -- this is raised by
clicking on the ** Set Font Sizes ** entry of the
File menu. This pops up a window which looks something like
the one below: pressing the appropriate ``radio button''
changes the size of the font in the proof session to
a point size which *approximates* the number on
the button. It changes the size of the size of the font used in the
Panels proportionately. The `OHP` entry means
``choose a size suitable for projection''.

If at any point you want to leave Jape, you can do so
by clicking on ** Close ** or ** Quit Jape **
from the File menu. The ** Close ** entry will be
greyed out if it really isn't a good idea for you to leave Jape right now,
but the ** Quit Jape ** entry can always be used.

If there are proofs in progress, or proofs which have been completed since the last time you saved your proofs in this Jape Session, then Jape will pop up the following invitation

The QMW Jape Web site Oxford