# Re: [isabelle] Isar-Level cases command

I think this "use-case" is covered by raw proof blocks. In general I often find that proofs get much more readable when using those (of cause the caveat is that we often have to restate assumptions/their negations, but this can all be handled by tasteful use of "let ?x = ..." before). So here is what I would write:
```
lemma "length (filter P xs) ≤ length xs"
proof (induction xs)
case (Cons x xs)
{ assume "P x"
```
with Cons have "length (filter P (x#xs)) = Suc (length (filter P xs))" by simp
```    also note Cons.IH
also have "Suc (length xs) = length (x#xs)" by simp
finally have ?case by simp }
moreover
{ assume "¬ P x"
```
with Cons have "length (filter P (x#xs)) = length (filter P xs)" by simp
```    also note Cons.IH
also have "length xs ≤ length (x#xs)" by simp
finally have ?case . }
ultimately show ?case by cases
qed simp

cheers

chris

On 11/25/2014 10:15 AM, Joachim Breitner wrote:
```
```Dear Isabelle-users,

we (rightfully) pride ourselves with how natural nicely written Isar
proofs are. But things are (always) not perfect, and there is always
room for careful improvements.

Consider this rather idiomatic proof:

lemma "length (filter P xs) ≤ length xs"
proof(induction xs)
case Nil thus ?case by simp
next
case (Cons x xs)
show ?case
proof(cases "P x")
case True with Cons
have "length (filter P (x#xs)) = Suc (length (filter P xs))" by simp
also note Cons.IH
also have "Suc (length xs) = length (x#xs)" by simp
finally show ?thesis by this simp
next
case False with Cons
have "length (filter P (x#xs)) = length (filter P xs)" by simp
also note Cons.IH
also have "length xs ≤ length (x#xs)" by simp
finally show ?thesis .
qed
qed

It is a nicely written structural proof and easy to follow. But there is
a wart: The case distinction!

* I have to write "show ?case" to initiate a case distinction. But
this is not natural: At this point, the final result is not what
is on my mind. And in a manually written proof, I would not
re-state the current goal at this point.
* If I had not used the "case" command I would actually have to
copy’n’paste the current goal here; obviously not very nice.
Especially if there are multiple case distinction, each
requiring me to copy that.
* The goal was conveniently named ?case, but suddenly I have to
write ?thesis. I (believe I) understand the techical reasons,
but again, this is a violation of the principle of least
surprise.

What I would like to be able to write is something like

lemma "length (filter P xs) ≤ length xs"
proof(induction xs)
case Nil thus ?case by simp
next
case (Cons x xs)

cases("P x")
case True with Cons
have "length (filter P (x#xs)) = Suc (length (filter P xs))" by simp
also note Cons.IH
also have "Suc (length xs) = length (x#xs)" by simp
finally show ?case by this simp
next
case False with Cons
have "length (filter P (x#xs)) = length (filter P xs)" by simp
also note Cons.IH
also have "length xs ≤ length (x#xs)" by simp
finally show ?case .
qed
qed

No seemingly redundant statement of the subgoals, the ability to simply
use ?case and the conventional flow of thoughts and facts in such a
proof.

This would also open the way to conveniently discharge multiple subgoals
in one case distinction:

lemma "A" and "B"
proof-
have "C" sorry

cases ("D")
case True
from `C` show A using True sorry
thus B using True sorry
next
case False
from `C` show B using False sorry
thus A using False sorry
qed
qed

(Note that in this case, no ?thesis is available, and
show A and B proof (cases "D")
does not do the right thing, as it apply the cases rule only to the
first subgoal, so it becomes messy to do this proof right now.)

This is the users mailing list, so I’ll refrain from making wild
assumptions about if and how this could be implemented, and whether
there is a similarity to the obtains command, but instead ask you for
feedback on the user-facing design of this feature:

Is it something you’d want as well?
Is the syntax nice?
What could be the closing keyword, if not qed?

Greetings,
Joachim

```
```

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.