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 of identity is made *)

**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}