by
op bossLib.by : term quotation * tactic -> tactic
Prove and place a theorem on the assumptions of the goal.
An invocation tm by tac, when applied to goal A ?- g, applies tac
to goal A ?- tm. If tm is thereby proved, it is added to A,
yielding the new goal A,tm ?- g. If tm is not proved by tac, then
the application fails.
When tm is added to the existing assumptions A, it is "stripped",
i.e., broken apart by eliminating existentials, conjunctions, and
disjunctions. This can lead to case splitting.
Failure
Fails if tac fails when applied to A ?- tm, or if tac fails to
prove that goal.
Example
Given the goal {x <= y, w < x} ?- P, suppose that the fact
?n. y = n + w would help in eventually proving P. Invoking
`?n. y = n + w` by (EXISTS_TAC ``y-w`` THEN DECIDE_TAC)
yields the goal {y = n + w, x <= y, w < x} ?- P in which the proved
fact has been added to the assumptions after its existential quantifier
is eliminated. Note the parentheses around the tactic: this is needed
for the example because by binds more tightly than THEN.
Comments
Use of by can be more convenient than IMP_RES_TAC and RES_TAC when
they would generate many useless assumptions.
See also
bossLib.subgoal,
bossLib.suffices_by,
Tactical.SUBGOAL_THEN,
Tactic.IMP_RES_TAC,
Tactic.RES_TAC,
Tactic.STRIP_ASSUME_TAC