Next: Implementing case expression logic Up: Implementing algebraic logic in Previous: An simple example of

### More sophisticated tactics

In this subsubsection and the following example, we discuss operations on tactics and tactics with parameters.

introduction of new variables:
When a rewrite introduces new free variables, they are automatically supplied with a numerical subscript as ``new'' variables. Something more complex may happen if the new variable is introduced inside an abstraction (bracketed) term; see below. The introduction of new variables can always be avoided by the use of parameterized versions of theorems which supply values to the new variables; see examples below.

```(* example of introduction of new variables *)

- declareunary "-";            (* declare - as a
prefix operator *)
- axiom "INV" "?x + -?x" "0";

- s "0";
- rri "INV";                   (* rri = revruleintro
applies converse of
theorem *)

{INV <= 0}                     (* display *)
INV <= 0

- ex();

{?x_82 + - ?x_82}              (* note appearance
?x_82 + - ?x_82                of new variables *)
```

control structures:
The special infix operators =>>, <<=, *> and <* allow one to apply a rewrite rule (or its converse) depending on whether the application of a preceding rewrite rule succeeded or failed.

The complex rewrite rules thm1 =>> thm2 and thm1 <<= ?thm2 have the effect of applying thm1 then applying thm2 (resp. its converse) only if the application of thm1 fails. (the handling of these infixes by Watson is quite different from their former handling by Mark2: a chain of alternatives applied to a term which Watson represents as (thm1 =>> thm2 =>> ... =>> thmn) => term was represented by Mark2 as thmn =>> ... thm2 =>> thm1 => term). The commands altruleintro (ari) and altrevruleintro (arri) introduce these ``alternative rule infixes'' (their use is illustrated in the examples below).

The complex rewrite rules thm1 *> thm2 and thm1 <* thm2 have the effect of first applying thm1, then applying thm2 only if the application of thm1 succeeded.

For either of the above kinds of operator, if the theorem thm1 happens to be a built-in operator (e.g., the abstraction and reduction tactics BIND and EVAL introduced below), thm1 is said to ``succeed'' if it makes a change in the target term, and ``fail'' otherwise. For theorems of the usual kind, success or failure depends on whether the appropriate side of the theorem matches the target term.

In the following example, we illustrate the application of =>> to fine-tune the behavior of a tactic. We prove a theorem which applies the identity of addition on either side.

```(* a preliminary result *)

- s "?x+0";                (* displays suppressed *)
- ri "COMM"; ri "ZERO";
- prove "COMMZERO";

COMMZERO:
?x + 0  =
ZERO => COMM => ?x + 0
0                          (* no axiom was used
in proving this,
though some
were mentioned *)

(* the tactic to apply identity on either side --
naive version *)

- s "?x+?y";
- ri "ZERO"; ri "COMMZERO";
- p "EITHERZERO";

EITHERZERO:
?x + ?y  =
COMMZERO => ZERO => ?x + ?y
0

(* the problem with this *)

- s "0+?x+0";
- ri "EITHERZERO"; ex();

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

(* the difficulty is that successive applications
of theorems cannot be relied upon to serve as
alternatives; one may apply and then another after
it in the list *)

(* we modify the tactic *)

- s "?x+?y";
- ri "ZERO"; ari "COMMZERO"; (* ari =
altrevruleintro
introduces an
alternative
theorem to be
applied if COMM fails *)
- reprove "EITHERZERO";

EITHERZERO:
?x + ?y  =
(ZERO =>> COMMZERO) => ?x + ?y  (* note the
syntactical
0                               effect of ari *)

(* we repeat the test above *)

- s "0+?x+0";
- ri "EITHERZERO"; ex();

{?x + 0}                   (* the final display:
?x + 0                     only one application
```

tactics with parameters; operators as tactics
Watson allows the user to develop tactics with parameters, which may be used to pass terms or other theorems or tactics as data to a tactic. The prove command will take parameter lists built with the predeclared function application infix ``@'' and pairing infix ``,''; it will match the parameter list against actual embedded occurrences of the theorem, which needs to have parameters matching the original parameter list in order to be used successfully for rewriting. Watson also allows operators (prefix or infix) to be ``proved'' as (necessarily parameterized) tactics.

```(* an example of parameterized and operator theorems:
simple structural tactics *)

- declareopaque "^+";           (* variable operator
declaration will be
explained below
(sect. ??) *)
- s "?x^+?y";
- right(); ri "?thm";
- p "RIGHT@?thm";

RIGHT @ ?thm:
?x ^+ ?y  =
?x ^+ ?thm => ?y
0

(* a test *)

- s "?x+?y+?z";
- ri "RIGHT@COMM"; steps();

(RIGHT @ COMM) => ?x + ?y + ?z (* display of
?x + COMM => ?y + ?z           rewriting steps *)
?x + ?z + ?y

(* operators as theorems *)

- s "?x";
- ri "?thm1";
- ri "?thm2";
- p "?thm1**?thm2";

?thm1 ** ?thm2:
?x  =
?thm2 => ?thm1 => ?x
0

(* a test *)

- s "?x+?y+?z";
- ri "COMM**ASSOC"; ex();

{?y + ?z + ?x}                 (* final display *)
?y + ?z + ?x
```

The prefix operator !@ can be applied to a theorem whose application introduces new variables to produce a parameterized theorem to which values of these new variables can be supplied; the operator !\$ applied to a theorem whose converse introduces new variables produces a parameterized theorem with the same effect as the converse of the original theorem.

In the following example, we develop a tactic converse of a theorem which eliminates variables using parameters and using the built-in operator !\$.

```(* parameterized converse theorem *)

- s "0";
- initializecounter();     (* initializes suffixes
of new variables *)
- rri "INV"; ex();

{?x_1 + - ?x_1}            (* display *)
?x_1 + - ?x_1

- assign "?x_1" "?x";      (* rename new variable
using global assignment *)
- prove "INV_INVERSE@?x";

INV_INVERSE @ ?x:
0  =
?x + - ?x
INV , 0

- s "0";
- ri "INV_INVERSE@3"; ex();

{3 + - 3}                  (* final display *)
3 + - 3

(* the same effect using a built in operator *)

- s "0";
- ri "(!\$ INV)@3"; ex();

{3 + - 3}                  (* final display *)
3 + - 3
```

We close the section with a not altogether trivial example.

```- declarepretheorem "ASSOCS";

- s "(?x+?y)+?z";
- ri "ASSOC"; ex();
- ri "ASSOCS";
- p "ASSOCS";

(* ASSOCS applies associativity
as many times as possible at the top *)

ASSOCS:
(?x + ?y) + ?z  =
ASSOCS => ?x + ?y + ?z
ASSOC , 0

(* a test *)

- s "((?x+?y)+?z)+(?u+?v)+?w";
- ri "ASSOCS"; ex();

{?x + ?y + ?z + (?u + ?v) + ?w}  (* the final display *)
?x + ?y + ?z + (?u + ?v) + ?w

(* the full tactic *)

- declarepretheorem "ALLASSOCS";

- s "?x+?y";
- ri "ASSOCS"; ri "RIGHT@ALLASSOCS";
- p "ALLASSOCS";

ALLASSOCS:
?x + ?y  =
(RIGHT @ ALLASSOCS) => ASSOCS => ?x + ?y
0                              (* no axiom dependencies
because no axiom was
actually used to rewrite *)

(* test *)

s "(((?x+(?y+?z)+?w)+(?u+?v)+?w)+
((?u+?v)+?w)+?e)+(?u+?v)+?e+?f";

{(((?x + (?y + ?z) + ?w) + (?u + ?v) + ?w) + ((?u
+ ?v) + ?w) + ?e) + (?u + ?v) + ?e + ?f}

(* duplication of displays suppressed *)

- ri "ALLASSOCS"; ex();

(* the final display -- intermediate and duplicate
displays suppressed *)

{?x + ?y + ?z + ?w + ?u + ?v + ?w + ?u + ?v + ?w + ?e
+ ?u + ?v + ?e + ?f}
```

Next: Implementing case expression logic Up: Implementing algebraic logic in Previous: An simple example of
Randall Holmes
2000-11-03