*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Calculational reasoning proof structure*From*: David Cock <davec at cse.unsw.edu.au>*Date*: Wed, 20 Aug 2014 11:03:39 +1000*In-reply-to*: <BE960C69-52D9-4984-85CE-B5113C02AE61@cmu.edu>*References*: <AAA5A771-0B93-4520-8FA1-84D6B13D95A3@cmu.edu> <BE960C69-52D9-4984-85CE-B5113C02AE61@cmu.edu>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Icedove/24.6.0

That pops up sometimes if you've flipped one of the inequalities e.g. have "a = b" . also have "c = b" . Dave On 20/08/14 08:21, Vadim Zaliva wrote:

Somehow related question: Why switching from second form to calculation one (using "also have") I ocaasionally get "*** Vacuous calculation result" error. Any common reasons for such problem? Vadim On Aug 19, 2014, at 11:35 , Vadim Zaliva <vzaliva at cmu.edu> wrote: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" Thanks! Sincerely, Vadim Zaliva -- CMU ECE PhD student Mobile: +1(510)220-1060 Skype: vzalivaSincerely, Vadim Zaliva -- CMU ECE PhD student Mobile: +1(510)220-1060 Skype: vzaliva

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

**Re: [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