Re: [isabelle] Length of Proofs



On 11/22/2012 11:42 PM, Makarius wrote:
On Thu, 22 Nov 2012, Jeremy Dawson 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 ??

 From where did you get the "minus"? Certainly not from this thread,
where I've pointed to the method_setup command of Isabelle/Isar already.
It is document in the "isar-ref" manual, as all other Isar commands. The
"implementation" manual has further documentation about what proof
methods are, compared to bare-bones tactics (which are also documented
there).

Makarius,

In another post I alluded to the fact that trying to mix ML and Isar so frequently made things not work. But I acknowledge that it may be a useful feature for someone that understands the system (in particular, I think, how Isar handles theories).

I see that the "implementation" manual has had a section on proof methods added since 2009 - I think that was a good thing to do. I haven't got to studying it yet.

The "plus" is much more than be discussed on such a mail thread. It also
depends on the imagination of users, what they make out of the vast
formal environment that Isabelle gives you today (as of current
Isabelle2012).

There is an ambiguity here between Isar (the language and its grammar) and Isar (the design/structure, ie, methods, facts, etc). Obviously, nothing that has been implemented in Standard ML couldn't be packaged in a way to make it convenient for users to use by calling Standard ML functions. The fact that the developers have not done so doesn't add to the merits of Isar (the language and its grammar).

Jeremy

Makarius






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