HYP : (thm list -> tactic) -> string -> thm list -> tactic
Augments a tactic's theorem list with named assumptions.
If tac is a tactic that expects a list of theorems as its arguments, e.g.
MESON_TAC, REWRITE_TAC or SET_TAC, then HYP tac s converts it to a
tactic where that list is augmented by the goal's assumptions specified in the
string argument s, which is a list of alphanumeric identifiers separated by
whitespace, e.g. "lab1 lab2".
- FAILURE CONDITIONS
When fully applied to a goal, it will fail if the string specifying the labels
is ill-formed, if any of the specified assumption labels are not found in
the goal, or if the tactic itself fails on the combined list of theorems.
With the following trivial goal
We may start by assuming and labelling the hypotheses, which may conveniently
be done using INTRO_TAC:
# g `p /\ q /\ r ==> r /\ q`;;
The resulting goal can trivially be solved in any number of ways, but if we
want to ensure that MESON_TAC uses exactly the assumptions relating to q
and r and no extraneous ones, we could do:
# e(INTRO_TAC "asm_p asm_q asm_r");;
val it : goalstack = 1 subgoal (1 total)
0 [`p`] (asm_p)
1 [`q`] (asm_q)
2 [`r`] (asm_r)
`r /\ q`
# e(HYP MESON_TAC "asm_r asm_q" );;
val it : goalstack = No subgoals
- SEE ALSO
ASM, ASSUM_LIST, FREEZE_THEN, LABEL_TAC, MESON_TAC, REMOVE_THEN, REWRITE_TAC,