op suffices_by : term quotation * tactic -> tactic
STRUCTURE
SYNOPSIS
Replace the goal’s conclusion with a sufficient alternative.
DESCRIPTION
A call to the tactic q suffices_by tac will first attempt to parse the quotation q in the context of the current goal. Assuming this generates a term qt of boolean type, it will then generate two sub-goals. Assuming the current goal is asl ?- g, the first new sub-goal will be that qt implies g, thus asl ?- qt ==> g. The second goal will be asl ?- qt.

The system next applies tac to the first sub-goal (the implication). If tac solves the goal (the common or at least, desired, case), the user will then be presented with one goal, where the original g has been replaced with qt. In this way, the user has adjusted the goal, replacing the old g with a qt that is sufficient to prove it.

FAILURE
A call to q suffices_by tac will fail if the quotation q does not parse to a term of boolean type. This parsing is done in the context of the whole goal (asl,g), using the parse_in_context function. The call will also fail if tac does not solve the newly generated subgoal.
EXAMPLE
If the current goal is
   f n m = f m n
   ------------------------------------
     0.  m <= n
     1.  n <= m
then the tactic `m = n` suffices_by SIMP_TAC bool_ss [] will result in the goal
   m = n
   ------------------------------------
     0.  m <= n
     1.  n <= m
where the call to SIMP_TAC has successfully proved the theorem
   |- (m = n) ==> (f m n = f n m)
eliminating the first of the two sub-goals that was generated.
COMMENTS
The tactic suffices_by is designed to support a backwards style of reasoning. Superficially, it appears to be dual to the tactic by, which provides a forward-reasoning facility. In fact, both are implementing a backwards application of the sequent calculus’s “cut” rule; the difference is which of the two premises to the rule is worked on by the provided tactics.
SEEALSO
HOL  Trindemossen-1