*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] question*From*: Peter Lammich <lammich at in.tum.de>*Date*: Sat, 25 Jan 2014 11:04:31 +0100*In-reply-to*: <52E2A5AE.7010405@in.tum.de>*References*: <866E7D87-1D8F-459E-808D-3DDE9D30EA11@cantab.net> <52E29F7A.4020408@illinois.edu> <52E2A5AE.7010405@in.tum.de>

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

**References**:**[isabelle] question***From:*John Wickerson

**Re: [isabelle] question***From:*Elsa L Gunter

**Re: [isabelle] question***From:*Manuel Eberl

- Previous by Date: Re: [isabelle] Enter MATCH
- Next by Date: [isabelle] New in the Archive of Formal Proofs
- Previous by Thread: Re: [isabelle] question
- Next by Thread: Re: [isabelle] question
- Cl-isabelle-users January 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list