*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] question*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Fri, 24 Jan 2014 18:41:02 +0100*In-reply-to*: <52E29F7A.4020408@illinois.edu>*References*: <866E7D87-1D8F-459E-808D-3DDE9D30EA11@cantab.net> <52E29F7A.4020408@illinois.edu>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.1.0

Hallo, while I am not an old time Isabelle user (~3 years) and am still at least four-ish years away from a PhD, I can wholeheartedly agree to what Elsa said. While formalisation is, of course, much easier when you already have a solid idea of /why/ the theorem you're trying to prove holds, I often find it very helpful to just write down a theorem statement in Isabelle and prove away even if I don't have the first idea why it should hold. For instance, in my Bachelor's thesis, I had to prove that some invariant (that I first had to find, so I wasn't even sure if it was the right one) is preserved throughout a loop. Isabelle told me precisely what facts I could use and what I had to prove – which is hard to keep track of in your head with a large proof such as this – and I proved everything in a short amount of time; by simply exploring “forward”, i.e. deriving everything I could think of from the assumptions I had, and “backwards”, i.e. reducing what I had to prove to simpler statements, until everything fell into place. It was only much later that I actually understood /intuitively/ what I had proven. This is probably a rare case, normally you first understand something and then formalise it, but Isabelle can help you to develop a proof from scratch as well. I also found it very useful during homework, most recently in social choice theory. Nitpick is particularly useful to avoid wasting time trying to prove things that are simply wrong, and it is also very useful for exercises such as “Prove or disprove X“ or “Show that in general, X does not hold”. Cheers, Manuel On 01/24/2014 06:14 PM, Elsa L Gunter wrote: > Dear John, > I am an old time Isabelle user, and someone with a PhD in math > (abstract algebra), and I always do my work in Isabelle straight out. > It's my scratch pad. I make lots of lemmas and start with a heavy use > of sorry, but the use of Isabelle as a record keeper when you are > thrashing out a proof is considerable. It is true that you will > probably make a very messy proof at best if you try to use Isabelle to > bludgeoned the proof to death or just start failing with the > connectives. Also, I basically never use auto, and only use clarsimp > when I know what I want it to do and what it will do. But through the > use of lemmas and subgoals, you can use Isabelle to help you > interactively discover the proof of theorems you are trying to prove. > ---Elsa > > On 1/24/14 10:54 AM, John Wickerson wrote: >> Hi all, >> >> I wonder if I might invite comment on the following statement? >> >> "Don't even *think* about firing up Isabelle until you've completed a >> really solid pencil-and-paper proof of the theorem you want to >> mechanise." >> >> Thanks! >> John >> >

**Follow-Ups**:**Re: [isabelle] question***From:*Peter Lammich

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

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

- Previous by Date: [isabelle] Fwd: question
- Next by Date: Re: [isabelle] question
- 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