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
     {message = "", origin_function = "CONJ_TAC", origin_structure =
      "Tactic", source_location = <??>} raised

> IF CONJ_TAC CONJ_TAC DISCH_TAC ([], “p ∨ q”);
Exception-
   HOL_ERR
     {message = "", origin_function = "DISCH_TAC", origin_structure =
      "Tactic", source_location = <??>} 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.

See also

Tactical.ORELSE, Tactical.THEN