Isabelle: Switching between "structured" and "apply-style" proofs

Question

There are two styles of proof in Isabelle: the old "apply" style, where a proof is just a chain of

apply (this method) 
apply (that method)

statements, and the new "structured" Isar style. Myself, I find both useful; "apply" style is more concise, and so is handy for uninteresting technical lemmas, while "structured" style is handy for the major theorems.

Sometimes I like to switch from one style to the other, mid-proof. Switching from "apply" style to "structured" style is easy: I just insert

proof -

in my apply-chain. My question is: how can I switch from "structured" style back to "apply" style?

To give a more concrete example: suppose I have five subgoals. I issue some "apply" instructions to despatch the first two subgoals. Then I launch into a structured proof to dispense with the third. I have two subgoals remaining: how do I return to "apply" style for these?

Answer 1

You can continue in "apply" style within a structured proof by using apply_end instead of apply, but this is rarely seen in practice and only during explorative work. In a polished proof, you would just pick the subgoals that merit an Isar proof and finish off all the remaining subgoals in one method call after the qed, as there is no need to deal with the subgoals in any specific order.

Alternatively, you can use defer before you start the structured proof with proof and continue immediately with the other subgoals in "apply" style, i.e., you defer the goals with structured proofs until the end.

And finally, you can of course re-state your goal in the structured proof with fix/assume/show and continue with "apply" style there. But you have to do this for each remaining subgoal separately, so this might be a bit tedious. The default case names goal1, goal2, etc. help a bit with typing, but such proofs are typically hard to maintain (especially as apply_end changes the goal numbering for goal<n>).