Re: [isabelle] Length of Proofs



Larry,

I don't suppose the legacy code simply can't be ported, any more than it can't be translated into HOL. But when I started to port it from Isabelle2005 to Isabelle2007 (still using ML tactics) I quickly gave up. I expect it would be much worse now.

And although it seems as though the documentation is more extensive now than it was then, to learn Isar I would anticipate having some questions. And the sort of answers I've had in the past to questions ("look at Makarius's thesis") aren't encouraging. The point is that to contemplate converting everything to Isar I need to _know_ that help will be available.

And anyway, what is the point of a system where you write tactics and then wrap them up as required to give them the type required by method_setup, rather than just write tactics? (This is of course a question to which the answer might be apparent if there was a more accessible description of the structure of an Isar proof than Makarius's thesis). Or learning something as totally weird as the grammar of the Isar language?

Cheers,

Jeremy


Lawrence Paulson wrote:
I think it's a great pity that you are using such an elderly version of Isabelle.

If you have a lot of legacy code that simply can't be ported, or an application where it works really well, okay. But for general proofs, there is simply no comparison between the Isabelle of today and one that is seven years old. Sledgehammer, counterexample finding, a very powerful function definition package, lots and lots of AFP theories… You shouldn't forego all of those.

Larry






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