How can I use rules suggested by solve_direct? (by (rule …) doesn't always work)

Question

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.

Answer 1

Personally, I just tend to just use:

apply (metis thm)

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:

apply (rule thm)                 (* If "thm" has no premises. *)
apply (erule thm)                (* If "thm" has a single premise. *)
apply (erule thm, assumption+)   (* If "thm" has multiple premises. *)

Why is there no one single answer? The answer is a little complex:

Internally, solve_direct calls find_theorems solves, which then performs the following:

fun etacn thm i = Seq.take (! tac_limit) o etac thm i;
(* ... *)
if Thm.no_prems thm then rtac thm 1 goal
else (etacn thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal;

This is the ML code for something similar to rule thm if there are no premises on the rule, or:

apply (erule thm, assumption+)

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:

ML {*
  fun solve_direct_tac thm ctxt goal =
  if Thm.no_prems thm then rtac thm 1 goal
  else (etac thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal;
*}

method_setup solve =
  {* Attrib.thm >> (fn thm => fn ctxt =>
        SIMPLE_METHOD' (K (solve_direct_tac thm ctxt ))) *}
  "directly solve a rule"

This could then be used as follows:

lemma "⟦ a; b ⟧ ⟹ a ∧ b"
  by (solve conjI)

which should hopefully solve anything solve_direct throws at you.

Answer 2

I found another way of using solve_direct's suggestions with by rule. When certain very basic rules from the library, such as Hilbert_Choice.someI2, are suggested, it seems that one of the facts in context actually is a rule itself, which may be applicable. The following worked for me at least in two concrete situations (source):

1. re-examine the “rule-like” fact, the other facts (if any) and the goal
2. if necessary, reorder the other facts
3. do the proof using <other_facts> ... by (rule <rule-like-fact>)

Answer 3

You can try fact or rule_tac. If I recall correctly, rule sometimes fails to apply a given rule in the presence of other facts and I am not entirely sure why; that question will have to be answered by someone who is more familiar with the implementation details of these methods than I am.