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