Re: [isabelle] Length of Proofs
Lawrence Paulson wrote:
There is no doubt that the APIs have changed rapidly over the years, in large part to accommodate user requests (in particular, for all declarations to work within locales). It certainly does make life difficult for developers.
There is a significant philosophical difference between Isabelle and HOL. I had always intended (perhaps even in 1986) that users should not have to write code in order to prove theorems. So I had no difficulty with a non-programmable notation for proofs, especially structured proofs, which (once you get the hang of them) make complicated proofs easier to write, understand and modify.
This being so, it's very fortunate that you did such a good job of
producing a programmable notation for proofs, in which one can write
code in order to prove theorems, when necessary (granted that it's
mostly not necessary).
Given that in HOL (as in Isabelle, both pre and post Isar) one can
always use proof procedures coded by someone else, this seems to sum up
to saying that Isabelle/Isar is like HOL, minus the capacity to code
one's own proof procedures, plus -- what ??
Mike Gordon expressed the difference between HOL and Isabelle succinctly: HOL can be seen as an API for coding proof procedures, while Isabelle is an interactive theorem prover that you use right out of the box. I know that this doesn't help at all with your situation.
On 21 Nov 2012, at 02:50, Jeremy Dawson <jeremy at rsise.anu.edu.au> wrote:
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?
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and