I have a proof by structural induction where several (28 of 29) cases can be proved directly with a terminal backward proof:

```
by cases auto (* which is just syntactic sugar for: proof cases qed auto *)
```

Now I'd like to omit these cases and just use a single method after the top level `qed`

. Is there a way to translate this simple terminal proof into a single method that does all the goal refinement normally done by `by`

and which can be used directly with `qed`

?

To clarify:

```
proof(induction _)
qed (cases; auto)
```

does not work?

No, unfortunately not.

Ah, of course that does not work. What about

```
proof(induction _; cases)
qed auto
```

or

```
proof(induction _)
qed ((cases; auto)+)
```

I was able to change the setup of a few elimination rules in the meantime and now at least some of the subgoals can be proven with `auto`

. Yet, there are still some which require `cases auto`

and together with these your other suggestions also don't work.

While it would be very helpful to see the lemma you are trying to prove, I could suggest trying

```
proof(induction _; cases)
qed (auto | assumption)+
```

as `by`

makes implicit calls to `assumption`

after applying the proof method

Well, nevermind what I wrote above.. assumption are of course being resolved in the simplification process of auto.. my bad!

Thanks for the input. Unfortunately, by putting `cases`

after `induction`

, Isabelle only splits the value of some undefined predicate instead of splitting the correct data.

The formalization I'm working on is a bit too involved to post in one piece and not yet published to a public repository, but it's a rather direct port of the Iris framework's HeapLang formalization and the corresponding Coq lemma can be found here.

I just published the first draft of the port and the corresponding lemma can now be found here.

Last updated: Aug 15 2022 at 02:13 UTC