# Re: [isabelle] Calculational reasoning proof structure

```Of course, the last "..." needs to be replaced by "x2". If you don't want to copy the term, you can also use term bindings with have:

have "t1 = f t2" (is "_ = f ?t")

This binds the term t2 to ?t.

Lars Noschinski <noschinl at in.tum.de> schrieb:

>
>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
>
```

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