# Re: [isabelle] Isar-Level cases command

```Dear Joachim,

```
Personally, I do not mind having to state the "show ?case" part, because it makes clear that you really need to do the case distinction to prove the whole case. In fact, I think that your case distinction in the example is not as it should be, because you only need it to for the unfolding of filter. The remaining reasoning is essentially the same, and I would prefer if that could be expressed more easily.
```
Here's what I would like to see as the proof structure:

lemma "length (filter P xs) ≤ length xs"
proof(induction xs)
case Nil thus ?case by simp
next
case (Cons x xs)
let ?n = "if P x then 1 else 0"
have "length (filter P (x#xs)) = ?n + length (filter P xs)"
by(cases "P x") simp_all
also note Cons.IH
also have "?n + length xs <= length (x # xs)"
by(cases "P x") simp_all
finally show ?case .
qed

```
Unfortunately, Isabelle does not provide good syntax to express such expression. I think this is the reason for having so many proofs in the style of show ?case proof(cases ...).
```
```
As Christian Sternagel mentioned, raw proof blocks are sometimes an option, but I do not like them much either. If you have multiple goals, you can use "case_tac [!] ..." instead of "cases ..." to do a case distinction on all of them. Unfortunately, this does not give you the case names.
```
Andreas

On 25/11/14 10:15, 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.