Re: [isabelle] question

For algorithm verification, I usually try to understand the algorithm
intuitively, sketching it on paper. Then I try sketching the
invariants, still on paper. Only then I start formalizing it, and see
how to strengthen the invariants to go through.

For proofs that require more intricate arguments (in my case, decidable
abstract models for parallel programs) I usually have a proof sketch on
paper first, and then try to encode it in Isabelle. 

However, as more advanced you get in Isabelle, as more can you prove by
just typing it into Isabelle and follow your "instinct" (supported by
sledgehammer&co) to prove it.

-- Peter

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