Re: [isabelle] question



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





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