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:

>Hi Vadim,
>
>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.