Re: [isabelle] Calculational reasoning proof structure



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: vzaliva
> 

Sincerely,
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.