Re: [isabelle] Length of Proofs

On Sat, 24 Nov 2012, Jeremy Dawson wrote:

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

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

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.

The thread is indeed getting long and tedious, and it is unclear if it ever ends. When I say "ML" or "Isabelle/ML", it practically always means the ML that is embedded into Isar. This is what you use for professional applications these days.

There is also a raw ML bootstrap environment to get the Isabelle/Pure implementation to the point where it can run the Isar toplevel with this embedded ML. In the 1990-ies, the user would continue with that raw ML toplevel to do proofs, but hardly anybody on the mailing list would remember that today.

Insisting to work with the raw ML toplevel is like traveling on a train like this:

This technique works for a tramway to some extent, but not on the high-speed train that Isabelle has become in recent years, where you better sit comfortably inside. And to get on such a train you merely purchase a ticket, you don't come with its technical manuals and take the engine apart while it is moving.


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