Sometimes <statement> solve_direct
(which I usually invoke via <statement> try
) lists a number of library theorems and says “The current goal can be solved directly with: …”.
Let <theorem>
be one search result of solve_direct
, then in most cases I can prove <statement> by (rule theorem)
.
Sometimes, however, such a proof is not accepted, resulting in the error message “Failed to apply initial proof method”.
Is there a general, different technique for reusing theorems found by solve_direct
?
Or does it depend on the individual situation? I could try to work out a minimal example and attach it to this question.
Personally, I just tend to just use:
which works most of the time without forcing me to think very hard (but will still occasionally fail if tricky resolution is required).
Other methods that will also typically work include:
Why is there no one single answer? The answer is a little complex:
Internally,
solve_direct
callsfind_theorems solves
, which then performs the following:This is the ML code for something similar to
rule thm
if there are no premises on the rule, or:if there are multiple premises on the rule. As commented by Brian on your question, the above might still fail if there are complex meta-logical connectives in the assumptions (which the
norm_hhf_tac
deals with, but is not directly exposed as an Isabelle method as far as I am aware).If you wanted, you could write a new method that exposes the tactic used by
find_theorems
directly, as follows:This could then be used as follows:
which should hopefully solve anything
solve_direct
throws at you.