REPEAT_TCL : thm_tactical -> thm_tactical
Repeatedly applies a theorem-tactical until it fails when applied to the
When applied to a theorem-tactical, a theorem-tactic and a theorem:
REPEAT_TCL repeatedly modifies the theorem according to ttl
until it fails when given to the theorem-tactic ttac.
- FAILURE CONDITIONS
Fails iff the theorem-tactic fails immediately when applied to the theorem.
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:
might be solved by
# g `(0 = w /\ 0 = x) /\ 0 = y /\ 0 = z ==> w + x + y + z = 0`;;
Warning: Free variables in goal: w, x, y, z
val it : goalstack = 1 subgoal (1 total)
`(0 = w /\ 0 = x) /\ 0 = y /\ 0 = z ==> w + x + y + z = 0`
# e(DISCH_THEN (REPEAT_TCL CONJUNCTS_THEN (SUBST1_TAC o SYM)) THEN
- SEE ALSO