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


Am Sonntag, den 19.05.2013, 20:18 +0900 schrieb Christian Sternagel:
> Instead, you could write:
> lemma "Q S --> P S"
> proof
>    assume "Q S"
>    show "P S"
>    proof (cases "S = {}")
>      assume "S ~= {}"
>      then obtain "x : S" by auto
>      ...
>      show "P S"
>    qed simp
> qed
> which looks (I guess) very similar to what you suggested:
> >      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
> >
> Maybe I do not get your main point?

It does look similar, but I still have to start the proof by stating
what I want to show (which I would not do in the pen-and-paper proof),
and I still have to have two nested blocks.

I also have cases in mind where the „trivial“ proof is a bit more
involved than something that you would put after qed, but still much
shorter than the „main proof“.

Also, putting it after the qed almost completely hides that the case is
handled. Compare this with the pen-and-paper-proof: The trivial case is
mentioned beforehand (and then discharged as uninteresting).

I know that my arguing is very much on the „personal preference and
perception“ level, and getting proofs to look good and to be a pleasant
read is a very subjective thing...

Maybe I could also state my idea this way, which does not talk about
style any more and might allow other uses as well:

        Would it be possible to get a variant of obtains where the proof
        obligation is not an abstract "this", but rather the actually
        goal shown afterwards?
This introduces a non-linearity into the proof that might feel very
wrong in ProofGeneral, but with the parallel style of jedit, this might
actually make sense. One would probably start with a proof of "sorry"
for the proof, continue the rest, and then finish the obtains proof when
the conclusion correctly known.

Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

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

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