7
$\begingroup$

I tried to use the sledgehammer command in Isabelle/HOL (2021) after the proof command, and got an error:

Illegal application of proof command in "state" mode

If I use it before the Isar proof command, then sledgehammer works. My question is:

Suppose a proof generates several sub-goals, having proved the first sub-goal somehow, is there a way to use sledgehammer in the middle of the proof process to try to prove the other sub-goals?

The more general question is:

Is sledgehammer designed for the old tactics and not suitable for use inside Isar proofs.

(I first asked this in SO; but did not get a definitive answer. Therefore, I am posting the question here, and deleting it there).

$\endgroup$

1 Answer 1

4
$\begingroup$

It will work in an Isar proof, however you will want to pull a subgoal into focus. Unless your most recent tactic is something like induction, you will find goal_cases handy. As an example

lemma A B C
proof goal_cases

will output a clickable (like with induction):

  case 1
  then show ?case sorry  (* goal: A *)
next
  case 2
  then show ?case sorry  (* goal: B *)
next
  case 3
  then show ?case sorry (* goal: C *)
qed

(obviously, the comments are not part of the output)

Then you can use sledgehammer after a show ?case statement.

Is sledgehammer designed for the old tactics and not suitable for use inside Isar proofs.

I would not say that apply-scripts are old/outdated, but indeed sledgehammer only works where you could also write an apply-style tactic (ignoring the fact that proof can take a tactic to open the Isar proof).


Of course, you could also write something like this:

   ... (* proved subgoal somehow *)
next
   show B
     sledgehammer
$\endgroup$
2
  • 2
    $\begingroup$ It might be convenient to highlight that a proof in Isabelle/Isar cycles through different modes (Isar Reference p. 131). This was very misleading to me at first. Commands like lemma put a goal in a prove mode, which is preserved after an apply command. On the other hand, the proof command leaves you in a state mode, in which there are no active goals, so to speak--you have to state them using have or show; this will put you in prove mode again (that's why the answer works). Finally, commands like from and then set the mode to chain (1/2) $\endgroup$ Commented Feb 17, 2022 at 0:04
  • 1
    $\begingroup$ (cont'd) which is similar to state, but with the addition of previous facts to the active goal. A detailed example is in the Isar Reference Manual, p. 37. (2/2) $\endgroup$ Commented Feb 17, 2022 at 0:07

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.