Re: [isabelle] Calculational reasoning proof structure



Hi,


Am Dienstag, den 19.08.2014, 11:35 -0700 schrieb Vadim Zaliva:
> 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"

I use {...} for that:

have "A = B" sorry
also
have "… = C" sorry
also
{ have "foo" sorry
  hence "bar" sorry
}
hence "… = D" sorry
also
have "… = E" sorry
finally have "A = E".


Greetings,
Joachim

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

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



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