Re: [isabelle] Calculational reasoning proof structure



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?

In such cases I often use the following pattern:

have "x0 = x1" 
  by ...
also 
have "... = x2"
proof 
  ...
  show ?thesis
    by ...
qed
also
have "... = x3"
  by ...
finally 
have "x0 = x3" .

I hope this solves your problem.

Greetings,
Salomon Sickert

Attachment: signature.asc
Description: This is a digitally signed message part

Attachment: smime.p7s
Description: S/MIME cryptographic signature



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