- 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.