Re: [isabelle] Length of Proofs



On 11/22/2012 10:32 PM, Lawrence Paulson wrote:
You still have the capacity to code your own proof procedures; ML is just one level down. And you get a much more readable proof language.

Larry,

While this is true, I did a lot of it a few years ago, and kept finding things not working. Mostly to do with theories - in one way or another. Impossible (for me or, in one case, for the developer I spoke to) to work out exactly what was going on.

Some years ago, I translated a lot of proofs from HOL to Isabelle. The HOL proofs were opaque blocks of tactics, while in the corresponding structure proof you could see (even if you knew little of the Isar language) which local facts were available for use and what had to be proved. And almost certainly, creating those opaque blocks of tactics required much more effort, because the old ML style (whether in HOL or Isabelle) isn't very good at forward reasoning.

You're certainly right about opaque blocks of tactics - but having to execute a proof to see the intermediate steps has got to be the price you pay for not having to write down all those intermediate steps. This whole thread started with the topic of an (I assume) Isar proof which was too long to be readable.

I don't know what local facts (or indeed facts generally) are. I suspect it's part of the larger question of what the state of a part completed Isar proof consists of, and how it related to what you see on the screen. I understood (a year or two ago) that this was not documented.

Jeremy

Larry

On 21 Nov 2012, at 22:31, Jeremy Dawson<jeremy at rsise.anu.edu.au>  wrote:

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 ??







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