Re: [isabelle] Length of Proofs



Makarius,

I'm not clear on the significance of your discussion about the meaning of "ML" but when I say Standard ML I mean any use of it.

Thanks for the link to (apparently) a German travelogue - it's a change to the tedium, if nothing else.

I'm left guessing what the discussion about trams and high-speed trains is really about, but it may be worth noting that there is an intermediate level of awareness which can actually be quite useful, such as timetables, route maps, destination signs on trains and so forth.

But if you like railway analogies - have you ever been to Karlsruhe? The city trams and high-speed trains actually use the same tracks.

Cheers,

Jeremy

On 11/26/2012 09:27 PM, Makarius wrote:
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")
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

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: http://gehcrew.blogspot.fr/2010_03_01_archive.html

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.


Makarius






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