Re: [isabelle] Length of Proofs



Makarius,

On 11/24/2012 02:25 AM, Makarius wrote:
On Fri, 23 Nov 2012, Jeremy Dawson wrote:


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

The Isar proof method called "tactic" actually presents the ML name
space to the user in a way that you can write nostalgic tactic
expressions right into your Isar proofs. E.g. like this:

lemma "A & B --> B & A"
apply (tactic "rtac impI 1")
apply (tactic "etac conjE 1")
apply (tactic "rtac conjI 1")
apply (tactic "ALLGOALS atac")
done

Another misunderstanding, I'm afraid. The above is about using ML from within Isar. I'm referring to the theoretical possibility of calling features of the Isar structure/framework from within ML. Such as, for example, as discussed in Feb 2010 in the thread called

Giving a name to a tactics-expression,

I would want the ML code that does something like

val meth4 = EVERY [(TRY (REPEAT1 meth1)), meth2, meth3 ] ;

made accessible.


So it is basically the same like in 1993, just with some extra boiler
plate. There is no practical point to use the above in reality, though.

No practical point ?? I think this email thread is getting too long - my first post was of stuff that I asserted (and still do) that you can't imagine how to do it sensibly other than in Standard ML. (And the only suggestion that has been contributed at all was from you, in previous emails, to wrap Standard ML in Isar via method-setup)

Jeremy


Makarius






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