Thm_cont.REPEAT

STRUCTURE

SYNOPSIS

Repeatedly applies a theorem-tactical until it fails when applied to the theorem.

DESCRIPTION

When applied to a theorem-tactical, a theorem-tactic and a theorem:

   REPEAT_TCL ttl ttac th

REPEAT_TCL repeatedly modifies the theorem according to ttl until it fails when given to the theorem-tactic ttac.

FAILURE

Fails iff the theorem-tactic fails immediately when applied to the theorem.

EXAMPLE

It is often desirable to repeat the action of basic theorem-tactics. For example CHOOSE_THEN strips off a single existential quantification, so one might use REPEAT_TCL CHOOSE_THEN to get rid of them all.

Alternatively, one might want to repeatedly break apart a theorem which is a nested conjunction and apply the same theorem-tactic to each conjunct. For example the following goal:

   ?- ((0 = w) /\ (0 = x)) /\ (0 = y) /\ (0 = z) ==> (w + x + y + z = 0)

might be solved by

   DISCH_THEN (REPEAT_TCL CONJUNCTS_THEN (SUBST1_TAC o SYM)) THEN
   REWRITE_TAC[ADD_CLAUSES]

SEEALSO

REPEAT_GTCL, THEN_TCL