Running Tactics 2

Type-checking subgoals for basic propositional and predicate logic can always be dealt with automatically, and we have a tactic Auto for that purpose.

Return to the proof editor window using , and click on the tactic D 0 which you just typed in. A term-editor window opens up again. Click after the 0 and enter:

The rule window should look like:

To run the tactic, enter $\langle$C-Z$\rangle$. The rule window closes and once the tactic has executed, the proof window should look like:

$$\vdash \forall {\Bbb{P}} \forall {\Bbb{P}} \neg \wedge \Longleftrightarrow \neg \vee \neg$$ D 0 THENW Auto

$${\Bbb{P}}$$

$$\vdash \forall {\Bbb{P}} \neg \wedge \Longleftrightarrow \neg \vee \neg$$

THENW is a tactical, a combinator for composing tactics. It has been declared to be an ML infix function, so one argument comes before and one after. Nearly all ML infix functions have names of more than one character, with all upper-case characters. To look at its type, enter

in the ML Top Loop. $THENW is a version of THENW which behaves like other ML functions in that all its arguments are placed to its right. What gets printed out should be:

THENW is a sequencing tactical; The tactic T₁ THENW T₂ first runs T₁ on some goal, and then runs T₂ on any well-formedness subgoals generated by T₂ . When doing Nuprl proofs you should add THENW Auto after any other tactics which generate well-formedness subgoals. Well-formedness subgoals are pretty easy to recognize; they always have a conclusion of form $\ulcorner$e $\in$T $\urcorner$where e is some expression, and T is a type. The type universes $\Bbb{U}${i}are themselves considered types. Other examples of types which you will encounter later are $\Bbb{Z}$, the integers, and $\Bbb{B}$, the booleans.

The first time you run a new tactic, or an existing tactic which might act in a new way, it is worth running it without the THENW Auto just to see how it works. Thereafter, always use the THENW Auto. From here on in the tutorial, we always include the THENW Auto if it is necessary, but feel free to try leaving it out first.