[isabelle] Fwd: question



I would add that if you are into Isar structured proofs and the structure
of the proof is not trivial then a proof sketch
using pencil and paper (or maybe even using "sorry")  seems essential.
Actually, I only accept apply scripts
in proof exploration. In a early version of Tobias tutorial on Isar there
was this nice remark:

"structure does not emerge automatically but needs to
be understood and imposed".

Best!
---------- Forwarded message ----------
From: Alfio Martini <alfio.martini at acm.org>
Date: Fri, Jan 24, 2014 at 3:04 PM
Subject: Re: [isabelle] question
To: John Wickerson <johnwickerson at cantab.net>
Cc: "isabelle-users at cl.cam.ac.uk Mailinglist" <isabelle-users at cl.cam.ac.uk>


Hi John,

I can say that I "hate" firing up Isabelle before having made at least a
proof sketch of the statement
I want to prove. I don´t feel comfortable with automation unless I know
what is going on.

Best!


On Fri, Jan 24, 2014 at 2:54 PM, John Wickerson <johnwickerson at cantab.net>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
>



-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
www.inf.pucrs.br/alfio
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil



-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
www.inf.pucrs.br/alfio
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil



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