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?

Reopened! Let's start over with the comments, shall we? – Andrew Barber May 23 '13 at 20:18 — Andrew Barber, May 23 '13 at 20:18

score 6 · Accepted Answer · answered May 18 '13 at 23:16

6

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

answered May 18 '13 at 23:16

Christoph Lange

595
2
13

NB: This fails if you re-order the cases (as pointed out by @LarsNoschinsiki in a comment to my answer). – Joachim Breitner Sep 04 '13 at 12:38

score 5 · Answer 2 · answered May 19 '13 at 09:41

5

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

answered May 19 '13 at 09:41

Joachim Breitner

25,395
6
78
139

1

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.) – chris May 19 '13 at 12:03
1

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). – Lars Noschinski Jun 08 '13 at 22:31
I did not not even know that you can use `cases` without an parameter :-) – Joachim Breitner Jun 09 '13 at 14:28

score 2 · Answer 3 · answered Oct 09 '13 at 19:39

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

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

3 Answers3