How to make the assumption of the second case of an Isabelle/Isar proof by cases explicit right in place?

Question

I have an Isabelle proof structured as follows:

proof (cases "n = 0")
  case True
  (* lots of stuff here *)
  show ?thesis sorry
next
  case False
  (* lots of stuff here too *)
  show ?thesis sorry
qed

The first case is actually several pages long, so when reading the second case it's no longer clear to a casual reader, not even to myself, what the False refers to. (Well, it actually is, but not from reading, only in an interactive environment: If, e.g., in Isabelle/jEdit, you place the cursor after case False, you'll see n ≠ 0 under "this" in the Output panel.)

So is there a syntax that allows for making the assumption of the "False" case explicit, so that the reader neither has to interact with the IDE, nor to scroll up to the proof keyword, but can see the assumption right in place?

Answer 1

In this case the proof becomes more readable by stating the assumption of each case explicitly:

proof cases
  assume "n = 0"
  show ?thesis sorry
next
  assume "n ≠ 0"
  show ?thesis sorry
qed

Answer 2

If the False case is shorter, just put it first. The order of proofs in an Isar block does not matter:

proof (cases "n = 0")
  case False
  show ?thesis sorry
next
  case True
  show ?thesis sorry
qed

Answer 3

Isar allows many variations on the same theme. Keeping the original outline, you can make intermediate facts explicit like this:

proof (cases "n = 0")
  case True
  (* lots of stuff here *)
  from `n = 0` show ?thesis sorry
next
  case False
  (* lots of stuff here too *)
  from `n ≠ 0` show ?thesis sorry
qed

This is a conservative extension of the original proof outline, i.e. it does not introduce any change in the policies of checking, unification, search etc.

Generally, the form

note `prop`

is equivalent to

have "prop" by fact