Is there a way to use sledgehammer in Isar proofs?

Question

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).

Answer 1

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