Re: [isabelle] Calculational reasoning proof structure



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

Attachment: signature.asc
Description: OpenPGP digital signature



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