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?

Episcopacy

Reopened! Let's start over with the comments, shall we? – Sewell

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

Episcopacy

NB: This fails if you re-order the cases (as pointed out by @LarsNoschinsiki in a comment to my answer). – Swivel

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

Swivel

In general, if the property on which we do case analysis is very short (like in n = 0), I would always prefer the explicit version instead of case False, case True, for readability. (Funnily, from a compositionality viewpoint the opposite is true.) – Aldos

Note that you can only reorder the cases if you call the cases method with a parameter. If you use the form proof cases assume P ... next assume "~P" ... then the negated case must be the second (as there are schematics in the goal which are instantiated by the first show command). – Brio

I did not not even know that you can use cases without an parameter :-) – Swivel

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

Thallium