IF
Tactical.IF : tactic -> tactic -> tactic -> tactic
Implements an if-then-else for tactics, using exceptions as failure.
Applying the tactic IF gt tt et to a goal g first applies gt to
g. If this tactic application succeeds (does not throw an exception),
then the tactic tt is applied to all of the generated sub-goals. (If
there are none because gt has completely proved the goal, this has no
effect and the result is a proved goal.) If gt g raises an exception,
then et is applied to g.
Failure
The application of IF to three tactic arguments never fails. The
resulting tactic will fail on a goal g if gt g succeeds and tt
fails on one of the resulting subgoals, or if gt g and et g both
fail.
Example
> IF CONJ_TAC CONJ_TAC DISCH_TAC ([], “(p1 ∧ p2) ∧ (q1 ∧ q2)”);
val it = ([([], “p1”), ([], “p2”), ([], “q1”), ([], “q2”)], fn):
goal list * validation
> IF CONJ_TAC CONJ_TAC DISCH_TAC ([], “p ⇒ q”);
val it = ([([“p”], “q”)], fn): goal list * validation
> IF CONJ_TAC CONJ_TAC DISCH_TAC ([], ``(p1 ∧ p2) ∧ q``);
Exception- HOL_ERR at Tactic.CONJ_TAC: raised
> IF CONJ_TAC CONJ_TAC DISCH_TAC ([], “p ∨ q”);
Exception- HOL_ERR at Tactic.DISCH_TAC: raised
Comments
A call to IF gt tt et does not behave the same as
(gt THEN tt) ORELSE et because the latter catches possible errors in
the application of tt to the goals generated by gt.