*To*: Isabelle Users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Calculational reasoning proof structure*From*: Vadim Zaliva <vzaliva at cmu.edu>*Date*: Tue, 19 Aug 2014 11:35:49 -0700*Sender*: Vadim Zaliva <vadim.zaliva at west.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? 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: vzaliva

**Follow-Ups**:**Re: [isabelle] Calculational reasoning proof structure***From:*Salomon Sickert

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

**Re: [isabelle] Calculational reasoning proof structure***From:*Lars Noschinski

**Re: [isabelle] Calculational reasoning proof structure***From:*Joachim Breitner

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