*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Discharging one (trivial) case without nesting the proof*From*: Joachim Breitner <breitner at kit.edu>*Date*: Sun, 19 May 2013 13:35:48 +0200*In-reply-to*: <5198B50A.6080307@gmail.com>*References*: <1368957723.4087.29.camel@kirk> <5198B50A.6080307@gmail.com>

Hi, 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. Greetings, Joachim -- Dipl.-Math. Dipl.-Inform. Joachim Breitner Wissenschaftlicher Mitarbeiter http://pp.ipd.kit.edu/~breitner

**Attachment:
signature.asc**

**References**:**[isabelle] Discharging one (trivial) case without nesting the proof***From:*Joachim Breitner

**Re: [isabelle] Discharging one (trivial) case without nesting the proof***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] Discharging one (trivial) case without nesting the proof
- Next by Date: Re: [isabelle] Contributing some Q&A to StackOverflow; please help me to gain reputation
- Previous by Thread: Re: [isabelle] Discharging one (trivial) case without nesting the proof
- Next by Thread: [isabelle] record in a locale?
- Cl-isabelle-users May 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list