# [isabelle] Discharging one (trivial) case without nesting the proof

```Dear Isabelle users (and devs),

Chrisoph’s question (http://stackoverflow.com/questions/16629417) proofs
by cases reminded me of a feature wish that I wanted to talk about for a
while.

In pen-and-paper proofs, if there are corner cases for which the result
is immediate, I just mention them at the beginning and continue with the
interesting cases:

Lemma: Every set that has property Q also has property P.

Proof: Let S be a set with property Q. Clearly, empty sets have
property P, so assume x ∈ S.
[long proof]
So S has property P.

In Isar, I would have to write:

lemma "Q S → P S"
proof
assume "Q S"
show "P S"
proof(cases "S = {}")
assume True thus "P S" by simp
next
assume False
then obtain "x ∈ S" by auto
..
show "P S"
qed
qed

deeper than it is in my mental model of the proof.

Note that if I could conclude False from "S = {}" and my current facts,
I could write the proof without additional indenting, e.g. using obtain.
But showing False or showing that the result holds is not a huge
difference in my understanding of a particular proof, so what I would
like to see is, for example,

lemma "Q S → P S"
proof
assume "Q S"

trivially "S ~= {}"
proof
assume "~ ~ S = {}"
show "P S" by simp
qed
then obtain "x ∈ S" by auto
..
show "P S"
qed

where (attention, obviously inaccurate understanding of Isar’s workings
under the hood following:) "trivially P" opens a proof goal "~P ==> ?P",
and the user is expected to finish this proof with "show Q" where Q is
the same result that he will show in the outer block. After the
"trivially P" command, P is added to the facts and to this. Note the
similarity with the obtain command, where I have to shown an abstract
"that".

I know that this is but a small reshuffling of the statements that I’d
have to write with "show Q proof(cases P)...", but it does make a
difference for the readability of the proof.

Bonus points if somehow inside the proof block opened by tivially the
statement to be shown is somehow inferred, so that I can just write

lemma "Q S → P S"
proof
assume "Q S"

trivially "S ~= {}" by simp
then obtain "x ∈ S" by auto
..
show "P S"
qed

Greetings and happy Whitsun,
Joachim

--
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner
```

Attachment: signature.asc
Description: This is a digitally signed message part

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