Case expression logic is implemented in Watson by the addition of special features to the tactic interpreter.

The execution order of the tactic interpreter is normally depth-first;
however, when called on a case expression `P || T , U`, the
hypothesis `P` is rewritten first. If `P` rewrites to the
form `true = X`, it is automatically further rewritten to `X`;
if the final form of the hypothesis is `true` or `false`, the
whole expression is rewritten to `T` or `U` respectively, and
the dropped alternative is never rewritten at all (this is the one
case in which the tactic interpreter is non-strict in its ``order of
evaluation'').

The tactic interpreter recognizes certain built-in tactics built with
numerals and the special operator `|-|`. These enable rewriting
with the hypotheses of case expressions in appropriate contexts. In a
tactic `m |-| n`, the numeral `m` will be 0, 1, or 2,
indicating the type of rewriting being done, and the numeral `n`
will indicate which hypothesis is being used. The hypothesis of the
largest case expression which contains the subterm being rewritten as
a subterm (not necessarily proper) of one of its branches is numbered
1; the hypothesis of the second largest such case expression is
numbered 2, and so forth.

The special tactic `0 |-| n` does rewriting in the positive branch
of the case expression whose hypothesis is numbered `n`. If the
hypothesis is of the form `A = B`, the tactic `0 |-| n` will
rewrite `A` to `B`; if it is introduced in the converse sense
it rewrites `B` to `A`. The target of this rewrite needs to
be identical to the appropriate side of the equation used to rewrite,
not just a match as in the case of rewriting with theorems. If the
hypothesis `X` is not an equation, it is treated just as if it
were the equation `true = X`.

The special tactic `1|-|n` rewrites case expressions `P || T ,
U`, in the case where the hypothesis `P` is the same as the hypothesis
numbered `n`, to `T` or `U` depending on whether the
subterm being rewritten is in the positive or negative branch of the
case expression with the `n`th hypothesis. The converse of this
rewrite rule rewrites the subterm to a new case expression with the
`n`th hypothesis, with the original form of the subterm as one
branch and a new variable as the other branch. The special tactic
`2 |-| n`, which is only used in the converse sense, rewrites the
subterm in the same way as the converse of `1 |-| n`, except that it
takes a parameter which is used in place of the new variable as the
new branch. Note that the new branch introduced by these converse
rewrite rules will have contradictory local hypotheses applicable to
it.

The special axioms

CASEINTRO: ?x = ?p || ?x , ?x EQUATION: (?a = ?b) = (?a = ?b) || true , falsewhich are provided in the logical preamble supplied by Watson to every theory, are used to introduce new case expressions.

It should be noted here that the fact that the meaning of built-in tactics referring to hypotheses of case expressions is context dependent necessitates a complication of the definition of substitution: when an expression containing such tactics is substituted into a context, it may be necessary for some of these tactics to be renumbered. The full definition of substitution will be given below.