[isabelle] Calculational reasoning proof structure


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"


Vadim Zaliva

CMU ECE PhD student
Mobile: +1(510)220-1060
Skype: vzaliva

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.