Next: More sophisticated tactics Up: Implementing algebraic logic in Previous: The tactic language introduced

### An simple example of tactic development

```- axiom "ZERO" "0+?x" "?x";     (* declarations made above
still in force *)
(* 0 is a numeral, so
predeclared *)

- declarepretheorem "ZEROES";   (* declare intention
of proving a theorem
ZEROES *)

- s "0+?x";                     (* display omitted *)
- ri "ZERO"; ex();

{?x}                            (* the expected display *)
?x

- ri "ZEROES";

{ZEROES => ?x}                  (* we leave the intention
hanging; after all,
ZEROES => ?x                    what does ZEROES do? *)

- prove "ZEROES";

ZEROES:                         (* the ``theorem'' *)

0 + ?x  =
ZEROES => ?x                    (* note presence of
recursion *)

ZERO , 0                        (* axioms used *)

(* now we test it *)

- s "0+0+0+?x";                 (* display omitted *)
- ri "ZEROES"; ex();

{?x}                            (* the final display *)
?x

(* demonstration of trace feature *)

- startover();                  (* this command resets
both sides of the equation
to the left side *)

{0 + 0 + 0 + ?x}
0 + 0 + 0 + ?x

- ri "ZEROES"; steps();         (* the steps command
traces tactic execution *)

ZEROES => 0 + 0 + 0 + ?x        (* display traced steps *)
ZEROES => 0 + 0 + ?x
ZEROES => 0 + ?x
ZEROES => ?x
?x                              (* note that the embedded
theorem is simply dropped
when it does not apply;
this makes termination
possible *)
```

This extremely simple example gives the basic idea of Watson's tactic language; ZEROES as an equational theorem is certainly true (this follows from the axiom ZERO and the fact that embedded theorems have no effect on term reference); as seen here, this ``equational theorem'' has execution behavior more general than can be achieved with any single application of a rewrite rule.

Randall Holmes
2000-11-03