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 nth hypothesis. The converse of this rewrite rule rewrites the subterm to a new case expression with the nth 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.