[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
        
What I don’t like about this is that the main proof (..) is indented
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.