*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Calculational reasoning proof structure*From*: Joachim Breitner <breitner at kit.edu>*Date*: Wed, 20 Aug 2014 07:30:06 -0700*In-reply-to*: <AAA5A771-0B93-4520-8FA1-84D6B13D95A3@cmu.edu>*References*: <AAA5A771-0B93-4520-8FA1-84D6B13D95A3@cmu.edu>

Hi, Am Dienstag, den 19.08.2014, 11:35 -0700 schrieb Vadim Zaliva: > Hi! > > I am doing a proof which includes series of steps. Something like this: > > have "x0 = x1" > also have "... = x2" > also have "... = x3" > ... > finally have "x0=xN" > > The proof is rather long and sometimes I need to prove some intermediate facts > between the steps to get to the next one. This breaks the computation chain and I could not > use "..." in the next step. What is the common way of dealing with such proofs? > Right now I am forced to do something like this: > > > have "x0 = x1" > hence s2:"x0=x2" > > have "some fact" > > hence "x0 = x3" using s2 > ... > hence "x0=xN" I use {...} for that: have "A = B" sorry also have "… = C" sorry also { have "foo" sorry hence "bar" sorry } hence "… = D" sorry also have "… = E" sorry finally have "A = E". Greetings, Joachim -- Dipl.-Math. Dipl.-Inform. Joachim Breitner Wissenschaftlicher Mitarbeiter http://pp.ipd.kit.edu/~breitner

**Attachment:
signature.asc**

**References**:**[isabelle] Calculational reasoning proof structure***From:*Vadim Zaliva

- Previous by Date: Re: [isabelle] Isabelle2014-RC4: Isabelle/jEdit action for C-hover
- Next by Date: Re: [isabelle] Isabelle2014-RC4: Isabelle/jEdit action for C-hover
- Previous by Thread: Re: [isabelle] Calculational reasoning proof structure
- Next by Thread: Re: [isabelle] Calculational reasoning proof structure
- Cl-isabelle-users August 2014 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