*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Calculational reasoning proof structure*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Wed, 20 Aug 2014 07:40:43 +0200*In-reply-to*: <AAA5A771-0B93-4520-8FA1-84D6B13D95A3@cmu.edu>*References*: <AAA5A771-0B93-4520-8FA1-84D6B13D95A3@cmu.edu>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Icedove/24.4.0

Hi Vadim, On 19.08.2014 20:35, Vadim Zaliva wrote: > 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? I often follow the pattern outlined by Salomon or put the intermediate facts before the calculational chain (actually, one could even put them at the very end of the proof, using "presume" -- is there anybody using that?) BTW, your problem stems not from "..." (which is just an abbreviation for the last right-hand-side -- you could also enter it manually). Howevere, there is no sensible place for the "also" (which takes the facts "calculation" and "this" to produce a new "calculation"). However, you can use "note" to manipulate "this"; but I am not sure I like this idea (because it destroys the nice calculation sequence). Something like the following should work: have "x0 = x1" also have *: "... = x2" have "some fact" note * also have "... = x3" using s2 ... finally have "x0=xN" -- Lars

**Attachment:
signature.asc**

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

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