*To*: Vadim Zaliva <vzaliva at cmu.edu>*Subject*: Re: [isabelle] Calculational reasoning proof structure*From*: Salomon Sickert <sickert at in.tum.de>*Date*: Tue, 19 Aug 2014 20:56:44 +0200*Cc*: Isabelle Users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <AAA5A771-0B93-4520-8FA1-84D6B13D95A3@cmu.edu>*References*: <AAA5A771-0B93-4520-8FA1-84D6B13D95A3@cmu.edu>

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? In such cases I often use the following pattern: have "x0 = x1" by ... also have "... = x2" proof ... show ?thesis by ... qed also have "... = x3" by ... finally have "x0 = x3" . I hope this solves your problem. Greetings, Salomon Sickert

**Attachment:
signature.asc**

**Attachment:
smime.p7s**

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

- Previous by Date: [isabelle] Calculational reasoning proof structure
- Next by Date: Re: [isabelle] Calculational reasoning proof structure
- Previous by Thread: [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