Re: [isabelle] Length of Proofs
On Sat, 24 Nov 2012, Jeremy Dawson wrote:
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
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")
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and